# Deontic Temporal Logic for Formal Verification of AI Ethics

arXiv: https://arxiv.org/abs/2501.05765 · HTML: https://mlsanity.com/paper/2501.05765/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 106 references that are in the map.
- First posted on arXiv 10 Jan 2025.

## Builds on (most cited first, 14 of 14)

- [A Survey on Bias and Fairness in Machine Learning](https://mlsanity.com/paper/1908.09635/) (2019)
- [Man is to Computer Programmer as Woman is to Homemaker? Debiasing Word Embeddings](https://mlsanity.com/paper/1607.06520/) (2016)
- [Counterfactual Fairness](https://mlsanity.com/paper/1703.06856/) (2017)
- [Mitigating Unwanted Biases with Adversarial Learning](https://mlsanity.com/paper/1801.07593/) (2018)
- [Opportunities and Challenges in Explainable Artificial Intelligence (XAI): A Survey](https://mlsanity.com/paper/2006.11371/) (2020)
- [Bias Mitigation for Machine Learning Classifiers: A Comprehensive Survey](https://mlsanity.com/paper/2207.07068/) (2022)
- [Fairness Under Unawareness: Assessing Disparity When Protected Class Is Unobserved](https://mlsanity.com/paper/1811.11154/) (2018)
- [ProPublica's COMPAS Data Revisited](https://mlsanity.com/paper/1906.04711/) (2019)
- [Lifelong Learning for Sentiment Classification](https://mlsanity.com/paper/1801.02808/) (2018)
- [Towards Verifiably Ethical Robot Behaviour](https://mlsanity.com/paper/1504.03592/) (2015)
- [Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle Obligations](https://mlsanity.com/paper/2105.02851/) (2021)
- [A Deontic Logic Analysis of Autonomous Systems' Safety](https://mlsanity.com/paper/2009.00738/) (2020)
- [Ensuring trustworthy and ethical behaviour in intelligent logical agents](https://mlsanity.com/paper/2402.07547/) (2024)
- [Automated Reasoning in Deontic Logic](https://mlsanity.com/paper/1411.4823/) (2014)

## Built on by (most cited first, 2 of 2)

- [Towards an Agent Operating System - Lessons from Classical and Cloud OS](https://mlsanity.com/paper/2607.25076/) (2026)
- [Mechanical Conscience: A Mathematical Framework for Dependability of Machine Intelligence](https://mlsanity.com/paper/2605.03847/) (2026)

## Abstract (arXiv)

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.