Model-Agnostic Counterfactual Explanations for Consequential Decisions

Amir-Hossein Karimi; Gilles Barthe; Borja Balle; Isabel Valera

Source-linked AI summary

Model-Agnostic Counterfactual Explanations for Consequential Decisions

Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera

arXiv:1905.11190v5May 27, 2019cs.LGcs.AIcs.LOstat.ML

TL;DR

Consequential decision systems need actionable counterfactual explanations, but existing methods are often limited by model, distance, and plausibility assumptions. The paper introduces MACE, which encodes predictive models and distance objectives as logic formulae and solves satisfiability problems. Across real-world datasets and predictive models, MACE achieves perfect coverage and more favorable distances than existing optimization-based approaches.

Problem
Existing counterfactual methods are often restricted to particular models or differentiable and convex distances, while plausible feature changes matter in consequential decisions.
Method
MACE compiles predictive models into formulae and conjuncts them with distance, plausibility, and diversity constraints for satisfiability solving.
Results
MACE achieves perfect coverage and generates counterfactuals at more favorable distances than existing optimization-based approaches across three real-world datasets and four predictive models.
Takeaways & Limitations
MACE provides model-agnostic counterfactual explanations that can incorporate heterogeneous features and actionable or immutable-feature constraints.
Takeaways & Limitations
The paper identifies accounting for statistical correlations and unmeasured confounding among features as future work for realizability.

Abstract

from arXiv · show

Predictive models are being increasingly used to support consequential decision making at the individual level in contexts such as pretrial bail and loan approval. As a result, there is increasing social and legal pressure to provide explanations that help the affected individuals not only to understand why a prediction was output, but also how to act to obtain a desired outcome. To this end, several works have proposed optimization-based methods to generate nearest counterfactual explanations. However, these methods are often restricted to a particular subset of models (e.g., decision trees or linear models) and differentiable distance functions. In contrast, we build on standard theory and tools from formal verification and propose a novel algorithm that solves a sequence of satisfiability problems, where both the distance function (objective) and predictive model (constraints) are represented as logic formulae. As shown by our experiments on real-world data, our algorithm is: i) model-agnostic ({non-}linear, {non-}differentiable, {non-}convex); ii) data-type-agnostic (heterogeneous features); iii) distance-agnostic ($\ell_0, \ell_1, \ell_\infty$, and combinations thereof); iv) able to generate plausible and diverse counterfactuals for any sample (i.e., 100% coverage); and v) at provably optimal distances.

1 Introduction

The paper targets actionable counterfactual explanations for consequential individual-level decisions, addressing limitations in existing methods through MACE, a flexible satisfiability-based approach.

Motivation: Consequential decision systems create pressure for explanations that clarify both predictions and how individuals can obtain desired outcomes.The motivating contexts include hiring, loan approval, and pretrial bail.
Problem: Nearest counterfactual explanations identify minimally distant feature changes that produce a desired prediction.The paper focuses on answering what features need to change, rather than why the original prediction was produced.
Problem: Existing approaches are restricted by model classes, differentiability, convexity, and missing optimality guarantees.Reported limitations include decision-tree-specific methods, classical optimization for convex models and distances, and gradient-based methods for differentiable models.
Approach: MACE maps nearest-counterfactual generation to a sequence of satisfiability problems using logic formulae for models, distances, plausibility, and diversity.The approach supports heterogeneous numerical and nominal features and additional plausibility constraints.
Results: 100% coverage is reported, while MACE generates significantly closer counterfactuals than previous approaches on real-world datasets.The experiments also present qualitative examples of actionable counterfactuals with restrictions on changeable features.

2 First-order predicate logic

The paper introduces first-order predicate-logic building blocks for representing model behavior and checking whether resulting formulae have valid assignments.

Logic primitives: Function symbols construct expressions, while predicate symbols construct atomic formulae such as equalities and inequalities.Examples include arithmetic expressions and relations between expressions.
Formulae: Quantifier-free formulae are Boolean combinations of atomic formulae using conjunction, disjunction, and negation.These formulae receive interpretations over their intended domains.
Interpretation: A real-valued formula denotes a subset of R^n obtained by assigning values to its variables.A concrete assignment satisfies the formula when the resulting statement is true.
Satisfiability: A formula is satisfiable when its interpretation is non-empty, and SMT solvers can check satisfiability automatically.The paper names Z3 and CVC4 as example solvers.
Solver theory: The paper’s formulae lie in the linear theory-of-reals fragment and can be decided efficiently using Fourier-Motzkin elimination.This characterization concerns expressions of degree 1 as multivariate polynomials.

3 Counterfactual spaces for predictive models

MACE represents counterfactual spaces and predictive models as logical formulae, then uses program-verification techniques to support diverse model types.

Counterfactual space: For a binary model, counterfactuals are inputs whose predictions differ from the factual input’s prediction.The counterfactual set is the preimage of the opposite binary output.
Characteristic formula: A characteristic formula is valid exactly when a model maps an input x to an output y, enabling a logical counterfactual formula.The counterfactual formula selects the opposite prediction from the factual output.
Scope: The binary-classifier formulation is stated to generalize to regression and other output domains.The paper explicitly notes that its displayed setup assumes binary predictor models.
Construction: Constructing the counterfactual formula requires the model’s characteristic formula and the factual output value.The approach assumes models can be represented as programs with assignments, conditionals, bounded loops, and returns.
Decision trees: For decision trees, each leaf contributes a clause formed from the conditions along its root-to-leaf path.The full characteristic formula combines the resulting leaf clauses.
Neural networks: For ReLU neural networks, characteristic-formula clauses encode node computations, nonlinear activations, and output thresholding.The formula includes variables for hidden-node values before and after ReLU transformation.

4 Finding the nearest counterfactual

MACE finds nearest counterfactuals by reducing the search to satisfiability checks over model, distance, and plausibility constraints. Binary search provides ε-accurate solutions, while the framework supports heterogeneous data, diverse explanations, and optimality certificates.

Main algorithm: MACE combines the counterfactual, distance, and plausibility requirements into satisfiability problems checked by an SMT oracle.A satisfying assignment is a counterfactual within the chosen distance threshold.
Main algorithm: Binary search over the distance threshold finds a counterfactual within ε of the optimal distance using at most O(log(1/ε)) oracle calls.The returned solution satisfies d(ˆxϵ, ˆx) ≤ d(ˆx∗, ˆx) + ε.
Generality: The approach is agnostic to predictive-model and distance details, including differentiable and non-differentiable models such as logistic regression, multilayer perceptrons, decision trees, and random forests.The model and distance need only be expressible in a sufficiently general programming language.
Main algorithm: An unsatisfiable threshold supplies a lower-bound certificate showing that no counterfactual exists at any smaller distance.The certificate follows from the solver’s proof that the corresponding formula is unsatisfiable.
Distance, plausibility, and diversity: Feature-specific distances support heterogeneous numerical, categorical, and ordinal inputs, while plausibility constraints enforce valid ranges, encodings, immutable features, and monotonic changes.The framework can also add constraints that guide explanations toward desired properties.
Distance, plausibility, and diversity: Iterative constraint formulas generate diverse counterfactuals by requiring each new explanation to differ sufficiently from previous ones.A 0-norm separation of at least 1 can prevent repetitive counterfactuals.

5 Experiments

Experiments on three real-world datasets and multiple predictive models evaluate MACE for coverage, distance, plausibility, and diverse counterfactual generation. MACE consistently provides broad coverage and closer counterfactuals while supporting additional plausibility and diversity constraints.

Experimental set-up: The evaluation uses Adult, Credit, and COMPAS datasets spanning loan approval and pretrial bail, with decision trees, random forests, logistic regression, and multilayer perceptrons.Nearest counterfactuals are evaluated on 500 held-out negative instances using ℓ0, ℓ1, and ℓ∞ distances.
Coverage and distance results: MACE and MO achieve 100% coverage by definition and design, while PFT fails on roughly 15% of Credit and COMPAS cases and both PFT and AR have minimal coverage on Adult.Coverage measures the percentage of factual samples receiving plausible counterfactuals under data-range and data-type constraints.
Coverage and distance results: 70.2% average distance reduction occurs on Adult, 75.4% on Credit, and 21.1% on COMPAS when comparing MACE with competing approaches on shared plausible cases.The reported reductions indicate that MACE generates significantly closer counterfactual explanations than PFT and AR in these comparisons.
Plausibility constraints: Adding an age constraint increases the distance to the nearest counterfactual, especially for ℓ1 and ℓ∞, because these norms account for the magnitude of feature changes.Under ℓ0, distance counts changed features without measuring how much each feature changes.
Plausibility constraints: MACE supports plausibility constraints that restrict changes to semantically meaningful features, including protected attributes such as age, race, and gender.The experiments examine constraints preventing age changes and discuss their relevance to assessing whether predictions meet fairness-related desiderata.
Diversity constraints: Successive runs of MACE generate diverse actionable suggestions, including different debt-payment strategies or providing documents confirming a graduate degree.The Credit example applies plausibility constraints on age, sex, and marital status together with an ℓ0 diversity clause.

6 Conclusions

The paper presents MACE, a formal-verification approach for counterfactual explanations, and reports perfect coverage with more favorable distances than existing optimization-based methods. It also identifies future work on plausibility, diversity, scalability, and broader predictive settings.

MACE compiles predictive models into formulae and combines model, distance, plausibility, and diversity constraints for SMT-based verification.
On three real-world datasets and four popular predictive models, MACE achieves perfect coverage and more favorable counterfactual distances than existing optimization-based approaches.
MACE can provide explanations to affected individuals and inform administrators about potentially unfair reliance on protected attributes.
Future work includes extending MACE to multi-class classification and regression scenarios.
Future plausibility work should account for statistical correlations and unmeasured confounding factors to address realizability.
MACE's running time depends directly on SMT-solver efficiency, motivating scalability work for large models.

B Experiment Details

The experiments evaluate MACE across four model classes and note several boundaries for future empirical investigation. The study prioritizes broad applicability to already trained models rather than exhaustive model and dataset coverage.

Experiments evaluate decision trees, random forests, logistic regression, and multilayer perceptrons.
The selected model parametrizations were intended to provide good performance on the considered datasets while testing counterfactual generation across model classes.
Future work includes larger feature spaces, more complex models such as deeper MLPs, and additional SMT solvers.

B.2 Datasets

The study uses the Adult, COMPAS, and Credit datasets, retaining heterogeneous feature representations and reporting their sample and dimensionality statistics. These datasets are established in fairness and interpretability research on consequential decisions.

Adult and COMPAS use default features, Credit uses preprocessing from prior work, and samples with missing data were dropped.
The COMPAS dataset contains 5,278 samples and five features, or seven after one-hot encoding.
The Adult dataset contains 45,222 samples and 12 features, or 51 after one-hot encoding.
The Credit dataset contains 29,623 samples and 14 features, or 20 after one-hot encoding.
Dataset variables include integer, real, categorical, and ordinal types, including financial, demographic, education, and overdue-payment features.

B.3 Handling Mixed Data Types

MACE naturally handles mixed data types, whereas compared methods have restrictions involving real-valued variables, categorical encodings, mutually exclusive features, and ordinal variables. The comparison methods therefore require post-processing to restore valid variable types.

MACE handles mixed data types directly, while Feature Tweaking is restricted to real-valued variables in its described implementation.
The compared implementation converts some categorical columns to binary, drops more complex categorical columns, and does not support ordinal variables.
Post-processing rounds integer variables and selects the maximally activated category to enforce valid counterfactual variable types.

C.1 Comprehensive Distance δ Results

Across all tested combinations of approaches, models, norms, and datasets, MACE achieves counterfactual distances at least as good as competing methods.

MACE results are at least as good as any other approach in every tested setup.The comparison covers approaches, predictive models, distance norms, and datasets.

C.2 Quality vs Complexity

MACE trades higher desired accuracy for more SAT-solver calls and runtime while preserving 100% coverage. Its runtime varies substantially by model, reflecting a quality–complexity trade-off and the implementation’s emphasis on broad applicability.

Quality vs Complexity: O(log(1/ϵ)) SAT-solver calls provide higher accuracy, with counterfactual distance in [δ∗, δ∗+ ϵ] and unchanged 100% coverage.As ϵ approaches zero, distance improves while runtime increases.
Quality vs Complexity: MACE takes less than 5 seconds for logistic regression, 5–60 seconds for decision trees and random forests, and 1 minute–3 hours for multilayer perceptrons.These are final runtimes upon termination; multilayer-perceptron means did not exclude outliers.
Quality vs Complexity: Competing approaches require at most 30 seconds when successful, but AR and PFT often have below-100% coverage, and only MACE handles multilayer perceptrons.MO additionally requires access to training data.
Quality vs Complexity: MACE’s broader model support, heterogeneous-feature handling, closeness guarantees, and 100% coverage are presented as compensating for slower runtime in some settings.The stated compensation applies at least to decision trees, random forests, and logistic regression.
Quality vs Complexity: MACE’s current implementation emphasizes generating counterfactuals across broad settings rather than efficiency, with future efficiency improvements planned for multilayer-perceptron models.The authors point to state-of-the-art SMT tools as a possible avenue for improvement.
Quality vs Complexity: The choice of ϵ should reflect desired distance granularity, feature dimensionality and ranges, and the selected distance norm.For ℓ0, any ϵ < 1/J is sufficient for an optimal counterfactual when J is the data dimensionality.
Quality vs Complexity: Very fine continuous-ℓ1 granularity can yield changes that users may distrust, although such cases may help administrators assess classifier robustness and safety.The example concerns changing only a few dollars in an account-balance feature.

C.3 Additional Constrained Results

Additional experiments show that plausibility constraints can redirect counterfactual changes, while distance distributions remain favorable for MACE across the compared models.

Additional Constrained Results: For 18 factual samples requiring age reduction under unrestricted MACE, prohibiting age decreases preserves ℓ0 distance while redirecting changes to work class or education level.Work class changes occurred in 5/18 cases and education level changes in 4/18.
Additional Constrained Results: The no-age-reduction constraint significantly increases nearest-counterfactual distance, with larger effects under ℓ1 and ℓ∞ norms.The experiment uses a random forest trained on the Adult dataset.
Additional Constrained Results: Figure 4 compares final counterfactual-distance distributions for decision trees, random forests, logistic regression, and multilayer perceptrons.Lower distance is better, and absent bars indicate Ω = 0.
Additional Constrained Results: Figure 5 tracks average distance and runtime during Algorithm 1 against the number of SAT-solver calls.Lower distance and lower runtime are preferred.