标题： AI伦理形式验证的规范时间逻辑 显示英文标题

标题： Deontic Temporal Logic for Formal Verification of AI Ethics

摘要： 确保在人工智能（AI）系统日益普遍和影响力扩大的情况下保持伦理行为是全球关注的重大问题。 在AI伦理中使用形式化方法可能是指定和验证AI系统伦理行为的关键方法。 本文提出了一种基于义务逻辑的形式化方法，用于定义和评估AI系统的伦理行为，重点在于系统级规范，为实现这一重要目标做出贡献。 它引入了公理和定理来捕捉与公平性和可解释性相关的伦理要求。 该形式化方法结合了时间算子，以推理AI系统随时间变化的伦理行为。 作者通过评估现实世界中的COMPAS和贷款预测AI系统的伦理来验证这种形式化方法的有效性。 使用义务逻辑公式对COMPAS和贷款预测系统的各种伦理属性进行编码，从而可以使用自动定理证明器验证这些系统是否满足定义的属性。 形式化验证表明，这两个系统未能满足与公平性和非歧视相关的某些关键伦理属性，这证明了所提出的形式化方法在识别现实世界AI应用中潜在伦理问题方面的有效性。 显示英文摘要

摘要： Ensuring ethical behavior in Artificial Intelligence (AI) systems amidst their increasing ubiquity and influence is a major concern the world over. The use of formal methods in AI ethics is a possible crucial approach for specifying and verifying the ethical behavior of AI systems. This paper proposes a formalization based on deontic logic to define and evaluate the ethical behavior of AI systems, focusing on system-level specifications, contributing to this important goal. It introduces axioms and theorems to capture ethical requirements related to fairness and explainability. The formalization incorporates temporal operators to reason about the ethical behavior of AI systems over time. The authors evaluate the effectiveness of this formalization by assessing the ethics of the real-world COMPAS and loan prediction AI systems. Various ethical properties of the COMPAS and loan prediction systems are encoded using deontic logical formulas, allowing the use of an automated theorem prover to verify whether these systems satisfy the defined properties. The formal verification reveals that both systems fail to fulfill certain key ethical properties related to fairness and non-discrimination, demonstrating the effectiveness of the proposed formalization in identifying potential ethical issues in real-world AI applications.