As we grant artificial intelligence increasing power and independence in contexts like healthcare, policing, and driving, AI faces moral dilemmas but lacks the tools to solve them. Warnings from regulators, philosophers, and computer scientists about the dangers of unethical artificial intelligence have spurred interest in automated ethics-i.e., the development of machines that can perform ethical reasoning. However, prior work in automated ethics rarely engages with philosophical literature. Philosophers have spent centuries debating moral dilemmas so automated ethics will be most nuanced, consistent, and reliable when it draws on philosophical literature. In this paper, I present an implementation of automated Kantian ethics that is faithful to the Kantian philosophical tradition. I formalize Kant's categorical imperative in Dyadic Deontic Logic, implement this formalization in the Isabelle theorem prover, and develop a testing framework to evaluate how well my implementation coheres with expected properties of Kantian ethic. My system is an early step towards philosophically mature ethical AI agents and it can make nuanced judgements in complex ethical dilemmas because it is grounded in philosophical literature. Because I use an interactive theorem prover, my system's judgements are explainable.
翻译:当我们赋予人工智能在医疗保健、警务和驾驶等环境中增加权力和独立性时,AI面临道德难题,但却缺乏解决这些难题的工具。监管者、哲学家和计算机科学家关于不道德人工智能危险的警告激发了人们对自动伦理学(即,能进行道德推理的机器的开发)的兴趣。然而,以前在自动化伦理学方面的工作很少与哲学文献接触。哲学家花几个世纪辩论道德难题,因此,自动化伦理学在引用哲学文献时将是最微妙、一致和可靠的。在本文中,我介绍了一个忠于Kantian哲学传统的自动Kantian伦理学的实施。我在Dyadic Deontic Locic中将Kant绝对的迫切要求正式化为Dyadic Deontic Loc,在Isabelle theorem验证中实施这种正规化,并开发一个测试框架来评价我的执行与Kantian伦理学的预期特性之间的良好关系。我的系统是走向哲学上成熟的伦理学代理人的早期一步,它可以在复杂的伦理难题中作出细微的判断,因为它是哲学文献中的基础。因为我使用了互动的判断,所以可以解释我的系统。