Deontic Temporal Logic for Formal Verification of AI Ethics
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.
Code (0)
등록된 구현이 없습니다.
Tasks
EthicsFairnessSimilar Papers 제목 키워드 기반
Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle Obligations
We develop a formal framework for automatic reasoning about the obligations of autonomous cyber-physical systems, including their social and ethical obligations. Obligations, permissions and prohibitions are distinct fro…
EthicsSelf-Driving CarsOn Quantified Modal Theorem Proving for Modeling Ethics
In the last decade, formal logics have been used to model a wide range of ethical theories and principles with the goal of using these models within autonomous systems. Logics for modeling ethical theories, and their aut…
Automated Theorem ProvingEthicsAutomated Reasoning for Robot Ethics
Deontic logic is a very well researched branch of mathematical logic and philosophy. Various kinds of deontic logics are considered for different application domains like argumentation theory, legal reasoning, and acts i…
EthicsLegal ReasoningPhilosophyNormative Conditional Reasoning as a Fragment of HOL
We report on the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. Our mechanization is achieved via a shallow semantic…
EthicsPersuasivenessPhilosophyAutomated Kantian Ethics: A Faithful Implementation
As we grant artificial intelligence increasing power and independence in contexts like healthcare, policing, and driving, AI faces moral dilemmas but lacks the tools to solve them. Warnings from regulators, philosophers,…
Ethics