自动化康德伦理学：一种忠实的实现

随着我们在医疗、警务和驾驶等场景中赋予人工智能越来越多的权力与独立性，AI 面临着道德困境却缺乏解决它们的工具。监管者、哲学家与计算机科学家关于不道德人工智能危险的警告，激发了人们对自动化伦理——即开发能够进行伦理推理的机器——的兴趣。然而，先前的自动化伦理研究很少与哲学文献互动。哲学家们已就道德困境争论了数个世纪，因此当自动化伦理借鉴哲学文献时，它将最为细腻、一致且可靠。在本文中，我提出了一种忠实于康德哲学传统的自动化康德伦理学实现。我将康德的绝对命令形式化为二元道义逻辑（Dyadic Deontic Logic），在 Isabelle 定理证明器中实现该形式化，并开发了一个测试框架来评估我的实现与康德伦理学预期属性的一致程度。我的系统朝向哲学上成熟的伦理 AI 智能体迈出了早期一步，并且由于扎根于哲学文献，它能在复杂伦理困境中作出细腻判断。由于我使用了交互式定理证明器，我的系统的判断是可解释的。