Despite significant progress in post-hoc explanation methods for neural networks, many remain heuristic and lack provable guarantees. A key approach for obtaining explanations with provable guarantees is by identifying a cardinally-minimal subset of input features which by itself is provably sufficient to determine the prediction. However, for standard neural networks, this task is often computationally infeasible, as it demands a worst-case exponential number of verification queries in the number of input features, each of which is NP-hard. In this work, we show that for Neural Additive Models (NAMs), a recent and more interpretable neural network family, we can efficiently generate explanations with such guarantees. We present a new model-specific algorithm for NAMs that generates provably cardinally-minimal explanations using only a logarithmic number of verification queries in the number of input features, after a parallelized preprocessing step with logarithmic runtime in the required precision is applied to each small univariate NAM component. Our algorithm not only makes the task of obtaining cardinally-minimal explanations feasible, but even outperforms existing algorithms designed to find the relaxed variant of subset-minimal explanations - which may be larger and less informative but easier to compute - despite our algorithm solving a much more difficult task. Our experiments demonstrate that, compared to previous algorithms, our approach provides provably smaller explanations than existing works and substantially reduces the computation time. Moreover, we show that our generated provable explanations offer benefits that are unattainable by standard sampling-based techniques typically used to interpret NAMs.
Figures & tables
Figure 1: Comparison of a subset-minimal explanation and a cardinally-minimal explanation of a NAM. Both explanations (in yellow) in (b) and (c) are minimal, as perturbing any additional feature can lead the overall output to become negative.
Figure 2: Sufficient explanations in NAMs: (a) Users must examine the neighborhood of an input for proper interpretation; e.g, users might wrongly conclude that feature 1 from the FICO HELOC dataset alone determines a positive output, but small changes in features 15 or 18 can flip the classification. (b) Outputs of continuous neighborhoods can be misleading if not verified, since sampling may miss extrema. For example, users might wrongly believe based on sampling that all features but feature 1 only have positive outputs and thus fixing feature 1 will always lead to a positive output of the entire NAM; however, the output of feature 2 can become so negative to flip the classification.
Breast Cancer
CREDIT
FICO HELOC
Method
Size ( ↓ )
Time [s] ( ↓ )
Size ( ↓ )
Time [s] ( ↓ )
Size ( ↓ )
Time [s] ( ↓ )
Ours
4.00±
4.24
35.60±
1.34
3.76±
2.62
132.67±
36.76
5.59±
1.80
317.92±
222.07
Lexicographic
16.58±
5.44
634.92±
77.23
12.42±
6.45
473.63±
128.38
15.60±
7.53
146.16±
188.07
Sensitivity
16.27±
5.57
636.79±
87.44
3.82±
1.84
407.93±
126.63
9.45±
5.90
250.09±
148.44
Table 1: Comparison of average explanation size and computation time.
Figure 3: Explanation size over time for all datasets.
CREDIT
FICO HELOC
Method
Size ( ↓ )
Time [s] ( ↓ )
Sufficiency [%] ( ↑ )
Size ( ↓ )
Time [s] ( ↓ )
Sufficiency [%] ( ↑ )
Ours
3.76±
2.62
132.67±
36.76
100.00
5.59±
1.80
317.92±
222.07
100.00
Sampling
2.67±
3.10
5.10±
0.26
131.37
3.04±
3.05
6.89±
2.57
125.49
Table 2: Comparison against a purely sampling-based approach.
Appendix figures & tables7 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 4: The computation of the binary decomposition defined in Equation 33 , with input x and the output vector o0,…,on−1 representing the binary decomposition.
Breast Cancer
CREDIT
FICO HELOC
ϵ
Size ( ↓ )
Time [s] ( ↓ )
Size ( ↓ )
Time [s] ( ↓ )
Size ( ↓ )
Time [s] ( ↓ )
0.01
4.00±
4.24
35.60±
1.34
—
—
—
—
0.1
4.45±
3.98
115.08±
73.48
1.79±
1.07
76.76±
88.21
2.77±
1.62
131.31±
141.90
0.2
6.29±
3.50
143.81±
121.27
2.80±
2.07
97.16±
34.45
3.88±
1.58
136.82±
77.97
0.5
9.76±
2.75
146.01±
64.76
3.76±
2.62
132.67±
36.76
5.59±
1.80
317.92±
222.07
Appendix
Table 3: Varying perturbation radius ϵ on all datasets.
Figure 5: Number of processed features over time.
Figure 6: A comparison of explanation generation with different number of processors ρ .
Figure 7: Frequencies of the required precision to sort the features according to their importance.
Figure 8: Impact of the required precision on the sorting time.
Bias Shift
Sorting Time [s]
1
0.08
0.1
7.58
0.01
12.71
0.001
16.24
0.0001
20.95
0.00001
28.37
Appendix
Table 4: Influence of near identical features on the sorting time on synthetic example.
We propose FAME (Formal Abstract Minimal Explanations), a new class of abductive explanations grounded in abstract interpretation. FAME is the first method to scale to large neural networks while reducing explanation size. Our main contribution is the design of dedicated perturbation domains that eliminate the need for traversal order. FAME progressively shrinks these domains and leverages LiRPA-based bounds to discard irrelevant features, ultimately converging to a formal abstract minimal explanation. To assess explanation quality, we introduce a procedure that measures the worst-case distance between an abstract minimal explanation and a true minimal explanation. This procedure combines adversarial attacks with an optional VERIX+ refinement step. We benchmark FAME against VERIX+ and demonstrate consistent gains in both explanation size and runtime on medium- to large-scale neural networks.
Ryma Boumazouza, Raya Elsaleh, Melanie Ducoffe +2
Airbus SAS, France · IRT Saint-Exupery, France · The Hebrew University of Jerusalem, Israel
Formal explainability provides mathematically grounded justifications for individual predictions. However, abductive explanations often exceed human cognitive limits by involving too many features, while probabilistic relaxations have remained largely limited to categorical classification. We present a unified framework for probabilistic explainability based on sparse, anchored linear models, applicable to both binary classification and continuous regression. By mapping instances to the Boolean hypercube, our linear explanations strictly generalize subset-based approaches: they capture both the magnitude and direction of feature contributions while enforcing a prescribed sparsity budget k. We show that minimizing the relevance error for such explanations is \ClassNPPP-hard when the underlying model is a neural network, and we relate this intractable objective to a tractable surrogate---the fidelity error. For a parameterized family of local distributions, the relevance error of any k-sparse explanation is bounded by its fidelity error up to a multiplicative factor that remains small locally. We address the resulting empirical problem using two complementary approaches: a Mixed Integer Programming (MIP) formulation that yields provably optimal empirical solutions while maintaining polynomial sample complexity, and a polynomial-time Iterative Hard Thresholding (IHT) algorithm with provable approximation guarantees. Empirical evaluations show that, unlike state-of-the-art baselines such as LIME and MAPLE, our explanations satisfy both the anchoring and sparsity constraints by construction, while consistently achieving lower relevance error.
Frederic Koriche, Jean-Marie Lagniez, Chi Tran
Computer science Research Institute of Lens (CRIL), UMR CNRS 8188, University of Artois, Rue Jean Souvraz SP 18, Lens, F-62307, France
Formal explainability of classifying neural networks (NNs) is an active area of research, providing explanations with provable guarantees of the classification within continuous regions of the input feature space. However, the existing techniques are either limited to individual input features without guarantees on their relations or the provided solutions fail to scale to deep architectures. This paper addresses these issues by introducing a flexible symbolic framework for an efficient, guided computation of explanations of the NN behavior, parametrized by the activations of internal neurons, and using logical engines such as SMT solvers. Unlike prior methods that rely on specialized NN verifiers, our method yields explanations that are not restricted in shape. Our algorithm is implementable on top of a general-purpose logical solver, isolating the NN-specific encoding from the algorithmic framework. We experimented with a wide range of benchmarks from the domains of image recognition and medicine, illustrating the advantages of the new method, particularly in computational efficiency. Notably, our approach enables logical explanation of deep networks not amenable to prior logic-based methods.
Tomáš Kolárik, Faezeh Labbaf, Fabrizio Leopardi +3
University of Lugano (USI), Lugano, Switzerland · Florida State University, United States of America · SUPSI, IDSIA, Lugano, Switzerland