Axiomatic Foundations of Counterfactual Explanations

TL;DR

This paper develops an axiomatic framework for counterfactual explanations, revealing five distinct types that encompass both local and global explanations, and formalizing their properties, limitations, and computational aspects.

Contribution

It introduces a systematic axiomatic approach to classify and analyze different types of counterfactual explanations, including global and local variants, filling a gap in the theoretical understanding.

Findings

Identifies five fundamental types of counterfactual explanations.

Proves impossibility theorems for certain axiom combinations.

Characterizes existing explainers within the new taxonomy.

Abstract

Explaining autonomous and intelligent systems is critical in order to improve trust in their decisions. Counterfactuals have emerged as one of the most compelling forms of explanation. They address ``why not'' questions by revealing how decisions could be altered. Despite the growing literature, most existing explainers focus on a single type of counterfactual and are restricted to local explanations, focusing on individual instances. There has been no systematic study of alternative counterfactual types, nor of global counterfactuals that shed light on a system's overall reasoning process. This paper addresses the two gaps by introducing an axiomatic framework built on a set of desirable properties for counterfactual explainers. It proves impossibility theorems showing that no single explainer can satisfy certain axiom combinations simultaneously, and fully characterizes all compatible sets. Representation theorems then establish five one-to-one correspondences between specific subsets of axioms and the families of explainers that satisfy them. Each family gives rise to a distinct type of counterfactual explanation, uncovering five fundamentally different types of counterfactuals. Some of these correspond to local explanations, while others capture global explanations. Finally, the framework situates existing explainers within this taxonomy, formally characterizes their behavior, and analyzes the computational complexity of generating such explanations.