Space Explanations of Neural Network Classification

AI summary

Overview

Research area: Explainable AI (XAI) and formal methods for neural network verification, specifically provable explanations of classifier behavior.

Technical level: Advanced. The paper assumes familiarity with neural network architectures, SMT solving, Craig interpolation, unsatisfiable cores, and the difference between sample-based and space-based guarantees.

One-sentence scope: The paper introduces "Space Explanations"—logic formulas that serve as provably correct sufficient conditions for a neural network's classification over continuous regions of the input space—and demonstrates how Craig interpolation can automatically generate them.

What This Paper Is About

Most formal explainability methods for neural networks describe decisions in terms of isolated features (e.g., "age > 50 AND cholesterol < 200"), which produces axis-aligned boxes that cannot capture relationships between features and therefore fail to approximate the curved decision boundaries real classifiers produce. This paper proposes Space Explanations: logic formulas whose shape is unrestricted, allowing them to describe complex regions of input space, encode genuine multi-feature relationships, and closely approximate the true decision boundary while retaining provable correctness guarantees.

Key Contributions

1. A new formal explanation concept. Space Explanations are defined as logic formulas φ such that every point satisfying φ is guaranteed to be classified into a given class c. They generalize prior "abductive" and "interval" explanations, which are special cases with restricted (axis-aligned or zero-volume) shapes.

2. An interpolation-based generation framework. The method encodes a trained network, its input domains, and the negation of the target class into a single SMT formula. Given a sample point known to be classified as c, the resulting conjunction is unsatisfiable, and a Craig interpolant of this unsatisfiability is itself a Space Explanation. This requires only one solver query, rather than one verification query per feature.

3. A flexible strategy toolkit. Three composable strategies are introduced: Generalize (apply different Craig interpolation algorithms with varying logical strengths), Reduce (weaken and shrink explanations using unsatisfiable cores, optionally minimized), and Capture (partition the formula to expose relationships between selected feature pairs and approximate decision boundaries). Strategies can be applied cumulatively, e.g. G∘I∘A.

4. A prototype tool and empirical study. The authors implement SpEXplAIn on top of the interpolating SMT solver OpenSMT2, evaluate it on heart-attack, obesity, and MNIST models, and compare against the state-of-the-art abductive explainer VeriX and interval-based explanations, showing greater generality, more meaningful feature relations, and better scaling with input size.

Main Findings

• Feature relationships emerge naturally. Interpolation-derived explanations capture dependencies between features (e.g., the heart-attack model connects increasing age with decreasing blood pressure for high risk), whereas interval-based explanations can only produce rectangles, lines, or single points.

• Explanations are strictly more general. Subset-comparison experiments consistently show that Space Explanations often subsume interval explanations, and even when they only intersect (not comparable), they approximate the decision boundary more closely.

• One query vs. many. SpEXplAIn generates an explanation with a single SMT query; VeriX and similar tools require one verification query per feature, which drives exponential blow-up.

• Choice of interpolation algorithm matters. Stronger interpolants relax few or no features (sometimes returning the original sample point), while weaker interpolants cover much larger spaces. Intermediate algorithms (e.g., f-parameterized) offer a useful middle ground.

• Reduction is a trade-off. Unsatisfiable-core reduction (R) cheaply simplifies formulas; exhaustive minimization (R_min) shrinks them dramatically but is expensive and frequently times out on larger models (Obesity, MNIST).

• Scalability is asymmetric. SpEXplAIn scales well with input dimension (better than VeriX on MNIST at increasing image sizes) but degrades more quickly with network depth, because the prototype lacks depth-aware solver optimizations.

• Capture outperforms Generalize in targeted slices. When focusing on selected feature pairs, C-based explanations followed by R_min consistently cover larger spaces within the slice than G-based ones, because C isolates fixed features from the relaxed ones.

Methodology in Plain English

The authors start by encoding a trained neural network, its valid input domain, and the statement "the output is not class c" into one big logic formula. A sample point that is known to belong to class c, when plugged in, makes this formula unsatisfiable—there is no way to keep the input identical and get a different class.

The key insight is that this unsatisfiability proof contains information about why the classification cannot change. Craig interpolation extracts a formula from that proof which (a) is implied by the original sample, (b) still contradicts "not class c," and (c) only refers to input features—making it a valid explanation. Because interpolation algorithms come in different strengths, you can tune how much the explanation generalizes beyond the sample.

The authors then add two refinements. Reduce uses unsatisfiable cores to strip away unnecessary constraints, yielding smaller, more readable formulas. Capture deliberately partitions the formula so that only some features are relaxed, which forces the interpolant to reveal how those features interact—this is what makes decision-boundary approximation visible (as in the heart-attack age-versus-cholesterol plots). All of this runs on a standard SMT solver extended with interpolation support, and the output is a formula over the same features as the input.

Why This Matters

Impact on research. The paper shifts formal XAI from sample-anchored, axis-aligned explanations to arbitrary-shaped, provably correct regions of feature space. This gives the XAI community a richer object to reason about and a natural bridge between verification engines and interpretive tools. It also reframes Craig interpolation—well known in software verification—as a computational engine for explanation.

Real-world applications:

• Medical risk prediction: The heart-attack classifier example shows explanations like "risk rises with older age combined with altered blood pressure," which can be directly communicated to clinicians.
• Safety-critical autonomy: Any system that must justify why an input is guaranteed to produce a given output (e.g., avoiding a collision label, reporting a safe condition) benefits from provable region-based explanations.
• Regulatory compliance: Frameworks such as the EU AI Act require explanations with guarantees; Space Explanations provide exactly that form of certificate.
• Debugging deployed models: The ability to compare explanation spaces across models or input clusters helps engineers detect where a network's reasoning is fragile or surprising.

Industry relevance. Since the method plugs into standard SMT infrastructure and requires only one solver call per sample, it is practical for audit pipelines. The scalability caveats on deep networks are solvable with network-specific optimizations, suggesting a viable path toward production tooling.

Future Directions

• Depth-aware scalability. The prototype's runtime grows quickly with network depth because it lacks neural-network-specific optimizations in the underlying solver; adding such optimizations is the most immediate engineering target.

• Convolutional and other architectures. Extending beyond fully connected ReLU networks to CNNs and other common structures would broaden applicability to image and time-series models.

• Clustering and misclassification analysis. The authors propose using Space Explanations to approximate decision boundaries across clusters of the feature space and to identify systematic reasons why inputs are misclassified.

• Layer-wise analysis. Understanding how the explanation space evolves through hidden layers would open the door to introspecting internal representations, not just input-output behavior.

• Richer quality metrics. The paper notes that comparing high-dimensional spaces is hard; better quantitative measures (volume approximations, projection-based comparisons) remain an open research problem.

Target Audience

Researchers and practitioners in formal verification, SMT-based reasoning, and explainable AI who are comfortable with logic, neural network encodings, and interpolation-based verification. Applied ML engineers working on safety-critical or regulated systems will find the case studies and tooling directly useful. Students or practitioners new to formal methods will need background reading in Craig interpolation and SMT to fully engage with the technical core.

Authors’ abstract

We present a novel logic-based concept called Space Explanations for classifying neural networks that gives provable guarantees of the behavior of the network in continuous areas of the input feature space. To automatically generate space explanations, we leverage a range of flexible Craig interpolation algorithms and unsatisfiable core generation. Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the generated explanations are more meaningful than those computed by state-of-the-art.