Source-linked AI summary
On The Reasons Behind Decisions
Adnan Darwiche, Auguste Hirth
TL;DR
The paper asks how to explain decisions made by Boolean classifiers and assess their dependence on protected features. It formalizes decision reasons and counterfactuals, then gives efficient algorithms based on tractable Boolean circuits. The resulting framework supports decision explanation, counterfactual evaluation, and bias identification, while prime-implicant covers may yield incomplete explanations and the bias-inference method is not complete.
Problem
The paper addresses the need for a theory that explains decisions of Boolean classifiers and distinguishes decision bias from classifier bias.
Method
It defines sufficient, necessary, and complete reasons plus counterfactual and bias notions, using prime implicants and tractable Boolean circuits for computation.
Results
The framework applies reasons to explain decisions, evaluate “even if ... because ...” counterfactuals, and identify decision and classifier bias with polytime and linear-time algorithms for most notions.
Takeaways & Limitations
Reasons behind decisions can support practical analysis of counterfactual behavior and protected-feature dependence in Boolean classifiers.
Takeaways & Limitations
Prime-implicant covers may produce incomplete explanations, and the method inferring classifier bias from one unbiased decision is not complete.
Abstract
from arXiv · showhide
Recent work has shown that some common machine learning classifiers can be compiled into Boolean circuits that have the same input-output behavior. We present a theory for unveiling the reasons behind the decisions made by Boolean classifiers and study some of its theoretical and practical implications. We define notions such as sufficient, necessary and complete reasons behind decisions, in addition to classifier and decision bias. We show how these notions can be used to evaluate counterfactual statements such as "a decision will stick even if ... because ... ." We present efficient algorithms for computing these notions, which are based on new advances on tractable Boolean circuits, and illustrate them using a case study.
1 Introduction
The paper develops a theory for explaining Boolean-classifier decisions, including reasons, counterfactuals, and bias, building on classifier compilation into behaviorally equivalent circuits.
- 1 Introduction: Boolean circuits can represent some Bayesian-network and neural-network classifiers while preserving their input-output decisions.Prior work also used compiled circuits to explain and verify numeric classifiers.
- 1 Introduction: The theory explains specific decisions by identifying properties that support them and by evaluating counterfactual statements about what would change or preserve a decision.The motivating admissions examples distinguish alternative reasons and “even if ... because ...” claims.
- 1 Introduction: It formalizes sufficient, necessary, and complete reasons, along with decision bias and classifier bias.These notions are introduced to explain decisions and analyze protected-feature dependence.
- 1 Introduction: The approach uses prime implicants for semantics and tractable Boolean circuits for efficient computation of explanations.The paper also develops new results extending tractable circuits to explanation computation.
2 Classifiers, Decisions and Prime Implicants
The paper represents Boolean classifiers as propositional formulas whose models are positive instances, then uses prime implicants and related operations to formalize decision reasoning.
- 2 Classifiers, Decisions and Prime Implicants: A classifier is represented by a propositional formula whose satisfying assignments are positive instances, while its negation characterizes negative instances.The decision on an instance is determined by whether it satisfies the classifier formula or its negation.
- 2 Classifiers, Decisions and Prime Implicants: A literal is a variable or its negation, and a term is a consistent conjunction of literals that describes an instance property.Terms are treated as sets of literals, with subsumption defined by literal inclusion.
- 2 Classifiers, Decisions and Prime Implicants: A prime implicant is an implicant that is not subsumed by another implicant; a prime-implicant cover may omit redundant prime implicants.Because covers can exclude prime implicants, they may produce incomplete classifier explanations.
- 2 Classifiers, Decisions and Prime Implicants: The paper introduces sufficient, complete, and necessary reasons as foundations for explaining decisions, evaluating counterfactuals, and defining bias.These notions are developed in subsequent sections.
3 Sufficient Reasons
A sufficient reason is a minimal instance property that supports a classifier decision, and such reasons can explain decisions while revealing broader classifier behavior.
- 3 Sufficient Reasons: A sufficient reason is an instance property that is also a prime implicant of the formula representing the observed decision.It is minimal: no strict subset can justify the decision.
- 3 Sufficient Reasons: Every decision has at least one sufficient reason.This follows because the decision formula has a prime implicant satisfied by the instance.
- 3 Sufficient Reasons: A classifier may give the same decision for two instances through different sufficient reasons.Sufficient reasons need not be shared even when the decisions are equal.
- 3 Sufficient Reasons: If two decisions share a sufficient reason, their outputs must be equal.The shared consistent term is a prime implicant of both decision formulas.
- 3 Sufficient Reasons: Sufficient reasons can provide insights beyond explaining individual decisions, and related systems such as LIME and Anchor compute approximations of them.Prime implicants have also been used in model-based diagnosis.
4 Complete Reasons
The complete reason aggregates all sufficient reasons for a decision, capturing exactly which properties of the given instance can trigger that decision and distinguishing decisions with different explanatory bases.
- 4 Complete Reasons: The complete reason is the disjunction of all sufficient reasons for a decision.It is a unique logical representation and can enumerate the decision’s sufficient reasons through its prime implicants.
- 4 Complete Reasons: The complete reason captures every property of the instance, and only properties of that instance, that can trigger the particular decision.It therefore precisely characterizes why that decision is made.
- 4 Complete Reasons: If another instance with the same decision does not satisfy the complete reason, none of its sufficient reasons can be a property of the original instance.The theorem separates the explanatory properties associated with the two instances.
- 4 Complete Reasons: For the admissions classifier C1, Greg’s complete reason is E ∧(¬F ∨W), meaning admission follows from passing the entrance exam plus applying before or having work experience.Susan’s admission has a different sufficient reason, E ∧G, and she does not satisfy Greg’s complete reason.
5 Necessary Properties and Reasons
Necessary characteristics are those appearing in every sufficient reason, while the necessary property collects them and may be empty. The complete reason captures exactly the instance properties that can trigger the decision, making it both necessary and sufficient.
- A characteristic is necessary iff it appears in every sufficient reason; the necessary property is the set of all necessary characteristics.
- The necessary property is unique but can be empty when no characteristic is necessary.
- Changing one necessary characteristic guarantees a different decision, whereas changing multiple necessary characteristics may preserve the decision for completely different reasons.
- If two instances disagree on at least one necessary characteristic, their decisions have disjoint sufficient reasons.
- The complete reason contains enough information to compute necessary characteristics and the necessary property.
- Unlike a necessary reason, which may not exist, the complete reason is always a necessary and sufficient condition for explaining the decision.
6 Decision Counterfactuals
The paper formalizes counterfactual explanations by identifying conditions that preserve a decision after specified characteristics are flipped. These conditions support “even if ... because ...” statements and distinguish cases where no single property explains an outcome.
- For Greg, no single property can be pinpointed as triggering admission, so the paper does not issue a single “because” statement.
- A decision is made “because τ” iff τ is its complete reason, equivalently its necessary reason and only sufficient reason.
- “Even if ρ because τ” means τ remains the complete reason after property ρ is flipped in the instance.
- The formal counterfactual requires the changed property and explaining property to be disjoint, while preserving the original decision.
- Susan would still be admitted after losing her high GPA because her rich hometown and entrance-exam result form the complete reason.
7 Decision Bias and Classifier Bias
The paper defines decision bias through sensitivity to protected features and classifier bias through the existence of at least one biased decision. Sufficient and complete reasons yield conditions for detecting both forms, including from an unbiased decision in some cases.
- A classifier can be biased even when a particular decision is unbiased, because another sufficient reason may expose bias on a different instance.
- A decision is biased iff every sufficient reason contains at least one protected feature.
- If every sufficient reason contains a protected feature, changing only protected features can change the decision for some instance.
- Some decisions remain unbiased when protected features do not affect admission or denial, such as admission with good GPA and a passed entrance exam.
- A classifier is biased iff at least one decision is biased, and equivalently iff some sufficient reason includes a protected feature.
- Decision bias can be detected from the complete reason when existentially quantifying all unprotected features does not yield a valid condition.
- Classifier bias can sometimes be detected from one decision’s complete reason when substituting a protected feature’s values changes that reason.
8 Computing Reasons and Related Queries
The paper computes complete reasons for decisions from Decision-DNNF circuits by applying consensus followed by instance filtering. The resulting tractable circuits characterize sufficient reasons and support efficient queries.
- Approach motivation: Earlier prime-implicant enumeration methods are incomplete and lack a known complexity bound, motivating a circuit-based approach.The proposed method computes a complete reason first, then derives sufficient reasons and other queries from it.
- Circuit representation: Decision-DNNF circuits generalize OBDDs through decomposable AND gates and decision-shaped OR gates, and can be obtained with existing compilers.OBDD nodes map to fragments of the form (X ∧µ) ∨(¬X ∧ν).
- Computing complete reasons: The complete reason is computed by consensus then filtering and represented as a tractable circuit, enabling efficient queries even when sufficient reasons are exponentially numerous.Monotone NNF operations and prime-implicant extraction support the stated algorithms.
- Consensus and filtering: Consensus adds µ ∧ν to each decision OR gate without changing the circuit’s satisfying assignments, and can be constructed in linear time.The added term captures assignments satisfying both branches while preserving models.
- Consensus and filtering: Filtering replaces literals absent from instance α with 0; the resulting circuit contains only literals from α and is monotone with respect to agreement with α.Filtering is defined for consensus circuits satisfied by α and removes nodes or edges made irrelevant by replacement with 0.
- Computing complete reasons: For a satisfied Decision-DNNF circuit, a term is a sufficient reason exactly when it is a prime implicant of the filtered consensus circuit.This equivalence is the key correctness result for computing complete reasons.
9 Another Admissions Classifier
The case study applies the Boolean-classifier theory to a refined admissions classifier, using reason circuits and sufficient reasons to analyze bias and counterfactual decisions. It shows that bias findings can differ across applicants and that reason circuits support efficient analysis.
- 9 Another Admissions Classifier: The refined classifier values passing the entrance exam and first-time application but gives rich-hometown applicants an alternative path to acceptance.The classifier is non-monotone and is represented by the stated Boolean formula and six prime implicants.
- 9 Another Admissions Classifier: The case study represents applicants Scott, Robin and April with complete reason circuits derived from Definition 12.The circuits are simplified by propagating and removing constants while remaining satisfiable for the underlying decisions.
- 9 Another Admissions Classifier: Scott’s decision is biased because every sufficient reason contains the protected feature R.Changing R to ¬R flips the decision, yielding denial because Scott is not a first-time applicant and lacks a rich hometown.
- 9 Another Admissions Classifier: Robin’s decision is not biased because two sufficient reasons omit protected feature R, although the classifier is biased elsewhere.The same sufficient reasons also imply that some other applicant must receive a biased decision.
- 9 Another Admissions Classifier: The bias-inference method is not complete: a classifier may remain biased even when no protected feature appears in a sufficient reason for one decision.Thus, an unbiased decision can sometimes reveal classifier bias, but failure to reveal it does not establish absence of bias.
- 9 Another Admissions Classifier: April’s decision is not biased despite R appearing in the reason circuit, and E and F are necessary characteristics for that decision.Flipping either necessary characteristic is guaranteed to flip the decision.
- 9 Another Admissions Classifier: April’s admission would stick without work experience because E, G and F remain satisfied, but violating one of these characteristics would cause denial.This instantiates the paper’s counterfactual interpretation of sufficient and necessary reasons.
10 Conclusion
The paper develops a theory for reasoning about Boolean-classifier decisions through sufficient, necessary and complete reasons. It applies the theory to explanations, counterfactuals and bias, with tractable circuits enabling polytime and linear-time computation of most notions.
- 10 Conclusion: The theory explains Boolean-classifier decisions using sufficient, necessary and complete reasons.
- 10 Conclusion: The framework supports explaining decisions, evaluating counterfactual statements, and identifying decision and classifier bias.
- 10 Conclusion: Polytime and linear-time algorithms compute most introduced notions using the new tractable class of reason circuits.