Deontic Temporal Logic for Formal Verification of AI Ethics

要約

人工知能（AI）システムの倫理的行動を確保することは、遍在性と影響力の増加の中で、世界中の大きな関心事です。
AI倫理における正式な方法の使用は、AIシステムの倫理的行動を指定および検証するための重要なアプローチです。
このペーパーでは、システムレベルの仕様に焦点を当て、この重要な目標に貢献し、AIシステムの倫理的行動を定義および評価するために、デオンティックロジックに基づく形式化を提案します。
公平性と説明可能性に関連する倫理的要件を把握するために、公理と定理を導入します。
この形式化には、時間の経過とともにAIシステムの倫理的行動について推論するために、一時的な演算子が組み込まれています。
著者は、現実世界のコンパとローン予測AIシステムの倫理を評価することにより、この形式化の有効性を評価します。
コンパスおよびローン予測システムのさまざまな倫理的特性は、デオンティック論理式を使用してエンコードされているため、自動定理用プーバーを使用して、これらのシステムが定義されたプロパティを満たすかどうかを確認できます。
正式な検証は、両方のシステムが公平性と非差別に関連する特定の重要な倫理的特性を満たしていないことを明らかにしており、実際の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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google