用于AI伦理正式验证的义务时序逻辑

在AI系统日益普及和影响力日益增大的背景下，确保其伦理行为成为全球关注的重大议题。正式方法在AI伦理中发挥着可能至关重要的作用，用于指定和验证AI系统的伦理行为。本文提出一种基于义务逻辑的正式化方法，用于定义和评估AI系统的伦理行为，侧重于系统层面的规格说明，为实现这一重要目标作出贡献。该正式化引入公理和定理来捕捉与公平性和可解释性相关的伦理要求。该正式化将时序算子纳入其中，以对AI系统随时间的伦理行为进行推理。作者通过评估真实世界的COMPAS和贷款预测AI系统的伦理行为来评估该正式化的有效性。将COMPAS和贷款预测系统的各种伦理属性编码为义务逻辑公式，允许使用自动定理证明器来验证这些系统是否满足定义的属性。正式验证结果表明，这两个系统未能满足与公平性和非歧视相关的若干关键伦理属性，表明该正式化在识别真实世界AI应用中的潜在伦理问题方面具有有效性。