Source-linked AI summary
Abduction-Based Explanations for Machine Learning Models
Alexey Ignatiev, Nina Narodytska, Joao Marques-Silva
TL;DR
The paper addresses the lack of quality guarantees in heuristic explanations for ML predictions. It proposes model-agnostic abductive reasoning over constraint encodings, with entailment-oracle support for minimal explanations. Experiments report scalable computation of small, high-quality explanations across benchmark datasets.
Problem
Many ML explanation methods are heuristic and provide no guarantees that explanations are cardinality-minimal or subset-minimal.
Method
The approach uses abductive reasoning over constraint representations of ML models, with entailment queries answered by a dedicated oracle.
Results
The experiments demonstrate scalability and confirm that small explanations can be computed in practice.
Takeaways & Limitations
The constraint-agnostic framework can apply to any ML model representable with suitable constraints and decidable entailment queries.
Takeaways & Limitations
The approach relies on oracle-based abductive reasoning, whose associated complexity raises concerns about robustness and scalability.
Abstract
from arXiv · showhide
The growing range of applications of Machine Learning (ML) in a multitude of settings motivates the ability of computing small explanations for predictions made. Small explanations are generally accepted as easier for human decision makers to understand. Most earlier work on computing explanations is based on heuristic approaches, providing no guarantees of quality, in terms of how close such solutions are from cardinality- or subset-minimal explanations. This paper develops a constraint-agnostic solution for computing explanations for any ML model. The proposed solution exploits abductive reasoning, and imposes the requirement that the ML model can be represented as sets of constraints using some target constraint reasoning system for which the decision problem can be answered with some oracle. The experimental results, obtained on well-known datasets, validate the scalability of the proposed approach as well as the quality of the computed solutions.
Introduction
The paper addresses the need for understandable ML prediction explanations by proposing a principled, model-agnostic approach with formal minimality guarantees. It represents models as constraints and uses an entailment oracle, illustrating the approach on neural networks.
- ML applications motivate both validation of model results and explanation of their predictions.
- Existing explanation methods for many important ML models are largely heuristic and provide no guarantees about explanation quality.
- The proposed abductive approach computes cardinality-minimal or subset-minimal explanations while remaining model-agnostic.
- The approach requires encoding the ML model as constraints and answering entailment queries with a suitable reasoning system.
- The paper illustrates the framework using neural networks encoded into mixed integer linear programming and evaluated with SMT solvers.
- Experimental results demonstrate scalability and show that small explanations can be computed in practice.
Background
The background formalizes prime implicants, abductive explanations, constraint theories, and hitting sets as foundations for minimum-size explanation computation.
- Propositional Formulas, Implicants and Abduction: A term is an implicant when it entails a propositional formula, and a prime implicant has no proper subset that remains an implicant.
- Propositional Abduction: A propositional abduction problem consists of variables, hypotheses, manifestations, background theory, and a clause-cost function.
- Propositional Abduction: An explanation must be consistent with the background theory and entail the manifestations; minimum-cost explanations minimize the assigned cost.
- Propositional Formulas, Implicants and Abduction: A smallest prime implicant is a prime implicant of minimum size and can be related to a minimum satisfying assignment.
- First Order Logic and Prime Implicants: SMT restricts first-order logic to often-decidable fragments, and MILP variables may be real, integer, or Boolean.
- Minimal Hitting Sets: A minimal hitting set intersects every set in a collection, while none of its subsets does.
ML Explanations as Abductive Reasoning
The paper casts ML explanations as abductive reasoning over constraint encodings, targeting subset-minimal and cardinality-minimal explanations through oracle-based procedures.
- The framework represents an ML model with constraints and assumes an oracle that answers entailment queries.
- Explanation quality is associated with the number of specified features, motivating cardinality-minimal and subset-minimal explanations.
- Propositional Case: In the propositional case, features become hypothesis literals, the prediction becomes the manifestation, and the encoded model becomes the background formula.
- General Case: The general formulation supports arbitrary real, integer, or Boolean feature values by relating abductive explanations to prime implicants.
- Computing Explanations: Algorithm 1 computes a subset-minimal explanation by iteratively removing literals while testing entailment with a T-oracle.
- Computing Explanations: Algorithm 2 adapts propositional abduction to compute a smallest explanation using an implicit hitting-set process and oracle tests.
Encoding Neural Networks with MILP
The paper encodes sequential neural-network blocks as MILP constraints, representing a linear transformation followed by a RELU operation. Indicator constraints and auxiliary variables capture RELU branches without Big-M notation, while final softmax normalization can be omitted for prediction encoding.
- Each network block applies a linear transformation x′ = Ax + b followed by the nonlinear transformation y = RELU(x′) = max(x′, 0).
- The MILP encoding introduces Boolean variables z and auxiliary real variables s to represent the RELU conditions and outputs.
- Indicator constraints encode the RELU branches natively in modern MILP solvers, avoiding Big-M notation and its requirement for tight bounds.
- When z_i = 1, the constraints force y_i = 0; when z_i = 0, they force s_i = 0 and y_i to equal the affine transformation.
- The final softmax normalization need not be encoded because it does not change the maximum output value that determines the network prediction.
- A two-input, two-output example instantiates the encoding with auxiliary variables, binary indicators, nonnegative outputs and slacks, and explicit linear constraints.
Experimental Results
Experiments evaluate scalability and explanation quality across UCI, PennML, and MNIST datasets using SMT and MILP oracles. MILP generally performs better, while subset-minimal explanations offer a practical compromise between size and computational cost.
- Setup: The evaluation covers UCI, PennML, and MNIST datasets, using a Python prototype with SMT and MILP solvers under fixed time and memory limits.The benchmark setup used a MacBook Pro, an 1800-second time limit, and 4 GByte of memory.
- Tabular datasets: MILP consistently outperforms SMT, computing subset-minimal explanations for the tabular datasets in a fraction of a second and explaining two more datasets in another comparison.The results identify MILP as the preferred oracle across the reported experiments.
- Tabular datasets: 28.5% to 86.7%: relative subset-minimal explanation sizes across tabular datasets, with a 60.5% mean and substantial variation by dataset.Some samples require only one feature, while others cannot be reduced at all.
- Minimality trade-offs: Cardinality-minimal explanations are smaller in general but substantially more expensive to compute, with some datasets not fully explained within 1800 seconds.The reported computational cost makes subset-minimal explanations a practical alternative.
- MNIST digits: 63.92%: mean subset-minimal explanation size for MNIST, while no cardinality-minimal explanation was computed within one hour.MILP required about 52.86 seconds per reported MNIST explanation; SMT produced none within the one-hour limit.
- MNIST digits: The MNIST explanations are logically minimal but can be visually unintuitive because pixel-removal order may preserve regions that do not resemble the digit’s shape.Alternative traversal policies produce more human-interpretable explanations, and pixels irrelevant to one digit may be needed to exclude another class.
- Comparison with prior work: The approach produces reasonably smaller explanations than the state of the art for neural-network classifiers and may therefore be more interpretable to human decision makers.The comparison uses the Congressional Voting Records dataset and contrasts the approach with Bayesian-network explanations.
- Overall findings: MILP and SMT experiments support scalability, while the paper concludes that subset-minimal explanations are preferable because they are usually only slightly larger than cardinality-minimal ones.This conclusion reflects the trade-off between explanation size and the high cost of computing smallest-size explanations.
Related Work
Prior heuristic explanation work either approximates a complex model with an interpretable model or explains individual predictions using local feature perturbations.
- Heuristic-based explanations: One research line explains a complex ML model as a whole by transforming it into an interpretable model such as a decision tree.This line assumes the transformation preserves the original model’s accuracy.
- Heuristic-based explanations: A second line explains individual predictions by learning important input features from local perturbations, as in LIME.The example considers explaining why a neural network classifies an image as a car.
Discussion and Future Work
The paper presents its approach as a general, constraint-agnostic framework whose robustness and scalability can be addressed through explanation enumeration, preferences, alternative oracles, and abstraction refinement. It also positions the principled method as a benchmark and validation basis for heuristic approaches.
- Discussion and Future Work: Enumerating multiple minimal or minimum explanations can address robustness concerns by offering users alternatives.The oracle-based framework can also accommodate preferences over explanations, including feature weights.
- Discussion and Future Work: The prototype is a proof of concept that produces small, reasonable explanations across all studied benchmark sets.The approach can use oracles other than an ILP solver without conceptual modification.
- Discussion and Future Work: The principled approach can benchmark heuristic explanation methods, help develop faster heuristics, and validate or further minimize their explanations.This creates a reference point for comparing heuristic solutions with exact methods.
- Discussion and Future Work: The same general approach applies to any ML model representable with first-order logic constraints, with higher-order logics offering broader scope but potential decidability and scalability costs.The paper emphasizes that the framework is independent of a concrete ML model.
Conclusions
The paper uses abductive reasoning to compute subset- or cardinality-minimal explanations through a constraint-agnostic framework. Its experiments demonstrate explanation quality while highlighting a computational tradeoff between the two forms of minimality.
- Conclusions: Abductive reasoning computes shortest prime implicants that provide subset- or cardinality-minimal explanations.The approach is independent of the ML model, provided constraint representation and entailment queries are supported by an oracle.
- Conclusions: Subset-minimal explanations are computationally easier to find, whereas cardinality-minimal explanations can be much harder but use the fewest specified features.The paper identifies this as an important quality-versus-computation tradeoff.
- Conclusions: Future work includes other ML models, model encodings, entailment-query methods, and additional benchmark suites.