用逻辑形式化康德义务论，让AI能自主判断行为对错。
Formalizing Kantian Ethics: Formula of the Universal Law Logic (FULL)
- 构建多类型模态逻辑FULL，形式化康德第一定言命令。
- 在3个伦理案例中验证，无需预设道德直觉即可推理行为正当性。
- 适合研究可解释AI伦理与形式化哲学的学者使用。
机器伦理旨在构建人工智能道德主体（AMAs），以更深入理解道德并提升AI安全性。现有方法将人类道德直觉编码为行动公理（如‘不可伤害’、‘应帮助他人’），但存在两重局限：一未考虑行动者的目的；二假设人类可穷举自身道德直觉。本文探索一种缓解此问题的道德程序形式化方法，聚焦康德伦理学，提出一种名为公式普遍法则逻辑（FULL）的多类型量化模态逻辑。FULL形式化康德第一定言命令——普遍法则公式（FUL），并包含因果性与代理等概念。我们在三个康德伦理案例中证明，只要具备充分的非规范性背景知识，FULL即可在不依赖内置道德直觉的前提下，对具有特定目的的代理人行为进行推理评估。因此，FULL为更稳健、自主的AMAs提供了支持，并推动了康德伦理的形式化理解。
原文摘要 · Abstract (English)
The field of machine ethics aims to build Artificial Moral Agents (AMAs) to better understand morality and make AI agents safer. To do so, many approaches encode human moral intuition as a set of axioms on actions e.g., do not harm, you must help others. However, this introduces (at least) two limitations for future AMAs. First, it does not consider the agent's purposes in performing the action. Second, it assumes that we humans can enumerate our moral intuition. This paper explores formalizing a moral procedure that alleviates these two limitations. We specifically consider Kantian ethics and present a multi-sorted quantified modal logic we call the Formula of the Universal Law Logic (FULL). The FULL formalizes Kant's first formulation of the categorical imperative, the Formula of the Universal Law (FUL), and concepts such as causality and agency. We demonstrate on three cases from Kantian ethics that the FULL can reason to evaluate agents' actions for certain purposes without built-in moral intuition, given that it has sufficient (non-normative) background knowledge. Therefore, the FULL is a contribution towards more robust and autonomous AMAs, and a more formal understanding of Kantian ethics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。