Automated Kantian Ethics: A Faithful Implementation

TL;DR

This paper develops a formal, explainable AI system based on Kantian ethics, formalized in logic and implemented in a theorem prover, to address ethical dilemmas in AI with philosophical rigor.

Contribution

It introduces a formalization of Kantian ethics in Dyadic Deontic Logic and implements it in Isabelle, bridging philosophy and automated ethical reasoning.

Findings

The system can make nuanced ethical judgments in complex dilemmas.

It is grounded in Kantian philosophy, ensuring philosophical consistency.

Judgments are explainable due to the use of a theorem prover.

Abstract

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, and computer scientists about the dangers of unethical artificial intelligence have spurred interest in automated ethics-i.e., the development of machines that can perform ethical reasoning. However, prior work in automated ethics rarely engages with philosophical literature. Philosophers have spent centuries debating moral dilemmas so automated ethics will be most nuanced, consistent, and reliable when it draws on philosophical literature. In this paper, I present an implementation of automated Kantian ethics that is faithful to the Kantian philosophical tradition. I formalize Kant's categorical imperative in Dyadic Deontic Logic, implement this formalization in the Isabelle theorem prover, and develop a testing framework to evaluate how well my implementation coheres with expected properties of Kantian ethic. My system is an early step towards philosophically mature ethical AI agents and it can make nuanced judgements in complex ethical dilemmas because it is grounded in philosophical literature. Because I use an interactive theorem prover, my system's judgements are explainable.