arXiv:2501.05765v2 通告类型: 替换 摘要: 随着人工智能（AI）系统日益普及和影响力增强，在这些系统中确保伦理行为是一个全球性的重大关切。使用形式化方法来研究AI伦理是一种可能的关键手段，用于定义和验证AI系统的伦理行为。本文提出了一种基于义务逻辑的形式化方法，以定义和评估AI系统的伦理行为，强调系统级别的规范，从而为实现这一重要目标做出贡献。本文引入公理和定理来捕捉与公平性和可解释性相关的伦理要求。形式化方法引入了时间操作符，以便随着时间推移对AI系统的伦理行为进行推理。作者通过评估实际世界的COMPAS和贷款预测AI系统的伦理性来评估这种形式化方法的有效性。使用义务逻辑公式对COMPAS和贷款预测系统的各种伦理属性进行编码，从而可以使用自动定理证明器验证这些系统是否满足所定义的属性。形式化验证表明，这两个系统未能满足与公平性和非歧视性相关的某些关键伦理属性，证明了所提出的形式化方法在识别实际AI应用中的潜在伦理问题方面的有效性。