FAME: Formal Abstract Minimal Explanation for Neural Networks

Ryma Boumazouza; Raya Elsaleh; Melanie Ducoffe; Shahaf Bassan; Guy Katz

cs.AIMar 11, 2026

FAME: Formal Abstract Minimal Explanation for Neural Networks

Authors: Ryma Boumazouza, Raya Elsaleh, Melanie Ducoffe, Shahaf Bassan, Guy Katz

Organizations: Airbus SAS, France · IRT Saint-Exupery, France · The Hebrew University of Jerusalem, Israel

Abstract

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.

Figures & tables

Figure 1: FAME Framework. The pipeline operates in two main phases (1) Abstract Pruning (Green) phase leverages abstract interpretation (LiRPA) to simultaneously free a large number of irrelevant (pixels that are certified to have no influence on the model’s decision) features based on a batch certificate (Section 4.2 ). This iterative process operates within a refined, cardinality-constrained perturbation domain, $\Omega^{m}(x,A)$ (Eq. 5 ) to progressively tighten the domain ; To ensure that the final explanation is as small as possible, the remaining features that could not be freed in batches are tested individually (Section 5 ). (2) Exact Refinement (Orange) phase identifies the final necessary features using singleton addition attacks and, if needed, a final run of VERIX+ (Section 6 ). The difference in size, $\lvert\text{$\text{wAXp}^{A^{\star}}$}\rvert-\lvert\text{AXp}\rvert$ , serves as an evaluation metric of phase 1. — Figure 1: FAME Framework. The pipeline operates in two main phases (1) Abstract Pruning (Green) phase leverages abstract interpretation (LiRPA) to simultaneously free a large number of irrelevant (pixels that are certified to have no influence on the model’s decision) features based on a batch certificate (Section 4.2 ). This iterative process operates within a refined, cardinality-constrained perturbation domain, $\Omega^{m}(x,A)$ (Eq. 5 ) to progressively tighten the domain ; To ensure that the final explanation is as small as possible, the remaining features that could not be freed in batches are tested individually (Section 5 ). (2) Exact Refinement (Orange) phase identifies the final necessary features using singleton addition attacks and, if needed, a final run of VERIX+ (Section 6 ). The difference in size, $\lvert\text{$ \text{wAXp}^{A^{\star}} $}\rvert-\lvert\text{AXp}\rvert$ , serves as an evaluation metric of phase 1.

	VERIX+ (alone)		FAME: Single-round				FAME: Iterative refinement				FAME-accelerated VERIX+
Traversal order	bounds		/				/				/ + bounds
Search procedure	binary		MILP		Greedy		MILP		Greedy		Greedy + binary
Metrics ↓	$\|$ AXp $\|$	time	$\|$ $\text{wAXp}^{A}$ $\|$	time	$\|$ $\text{wAXp}^{A}$ $\|$	time	$\|$ $\text{wAXp}^{A}$ $\|$	time	$\|$ $\text{wAXp}^{A}$ $\|$	time	$\\|$ candidate-set $\\|$	$\|\textit{AXp}\|$	time
MNIST-FC	280.16	13.87	441.05	4.4	448.37	0.35	229.73	14.30	225.14	8.78	44.21	224.41	13.72
MNIST-CNN	159.78	56.72	181.24	5.59	190.29	0.51	124.9	12.35	122.09	5.6	104.09	113.53	33.75
GTSRB-FC	313.42	56.18	236.85	9.68	243.18	0.97	331.84	12.28	332.74	5.26	11.93	332.66	9.26

Table 1: Average explanation size and generation time (in seconds) are compared for FAME (single-round and iterative MILP/Greedy) with FAME-accelerated VERIX+ to achieve minimality.

Panel of Figure 2 — Figure 2: FAME’s iterative refinement approach against the VERIX+ baseline . The left plot compares the size of the final explanations. The right plot compares the runtime (in $seconds$ ). The data points for each model are distinguished by color, and the use of circles (card=True) and squares (card=False) indicates whether a cardinality constraint ( $||x-x^{\prime}||_{0}\leq m$ ) was applied.

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 3 — Figure 3: Toy example illustrating the asymmetry between adding and freeing features.

Feature	Normalized Cost for Class 1	Normalized Cost for Class 2	Maximum Normalized Cost
( $j$ )	( $c_{1,j}/(-\overline{b}^{1})$ )	( $c_{2,j}/(-\overline{b}^{2})$ )	( $\max_{i}$ )
$j_{1}$	$2/10=0.2$	$8/20=0.4$	0.4
$j_{2}$	$7/10=0.7$	$4/20=0.2$	0.7
$j_{3}$	$3/10=0.3$	$3/20=0.15$	0.3

Appendix

Table 2: Example of Greedy Heuristic Decision Making

Layer Type	Input Shape	Output Shape	Activation
Flatten	$28\times 28\times 1$	784	-
Fully Connected	784	10	ReLU
Fully Connected	10	10	ReLU
Output	10	10	-

Appendix

Table 3: Architecture of the MNIST-FC model.

Layer Type	Input Shape	Output Shape	Activation
Convolution 2D	$28\times 28\times 1$	$13\times 13\times 4$	-
Convolution 2D	$13\times 13\times 4$	$6\times 6\times 4$	-
Flatten	$6\times 6\times 4$	144	-
Fully Connected	144	20	ReLU
Output	20	10	-

Appendix

Table 4: Architecture of the MNIST-CNN model.

Layer Type	Input Shape	Output Shape	Activation
Flatten	$32\times 32\times 3$	3072	-
Fully Connected	3072	10	ReLU
Fully Connected	10	10	ReLU
Output	10	10	-

Appendix

Table 5: Architecture of the GTSRB-FC model.

Layer Type	Input Shape	Output Shape	Activation
Convolution 2D	$32\times 32\times 3$	$15\times 15\times 4$	-
Convolution 2D	$15\times 15\times 4$	$7\times 7\times 4$	-
Flatten	$7\times 7\times 4$	196	-
Fully Connected	196	20	ReLU
Output	20	10	-

Appendix

Table 6: Architecture of the GTSRB-CNN model.

Layer Type	Input Shape	Output Shape	Activation
Reshape	3072	$32\times 32\times 3$	-
Convolution 2D	$32\times 32\times 3$	$16\times 16\times 8$	ReLU
Residual Block (Downsample)	$16\times 16\times 8$	$8\times 8\times 16$	ReLU
Residual Block	$8\times 8\times 16$	$8\times 8\times 16$	ReLU
Flatten	$8\times 8\times 16$	1024	-
Fully Connected	1024	100	ReLU

Appendix

Table 7: Architecture of the ResNet-2B model (CIFAR-10).

Panel of Figure 6 — Figure 6: Performance Comparison of FAME’s Abstract Batch Freeing Methods. These three plots compare the greedy heuristic against the exact MILP solver for the iterative refinement task for all the models. The first plot shows the runtime comparison of the two methods on a log-log scale. The second plot compares the size of the freed feature set for both methods. The third plot illustrates the distribution of the optimality gap (MILP size - Greedy size).

Explore similar work

Provably Explaining Neural Additive Models
Feb 19, 2026Shahaf Bassan, Yizhak Yisrael Elboher, Tobias Ladner +4Interpretable ML Neural Network Interpretability
Hebrew University of Jerusalem, Israel · Technical University of Munich, Germany · Masaryk University, Czech Republic
Beyond $L_2$ : Generalizing Abductive Latent Explanations to Diverse Prototype-Based Architectures
Aug 17, 2026Jules Soria, Alban Grastien, Romain Xu-Darme +3Explainable Artificial Intelligence Neural Network Interpretability
Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France
Neuron Activation-based Computation of Logical Explanations for Deep Neural Networks
Sep 12, 2026Tomáš Kolárik, Faezeh Labbaf, Fabrizio Leopardi +3Explainable Artificial Intelligence Neural Network Interpretability
University of Lugano (USI), Lugano, Switzerland · Florida State University, United States of America · SUPSI, IDSIA, Lugano, Switzerland

Feb 19, 2026J/K move · Enter open · S save

Provably Explaining Neural Additive Models

Shahaf Bassan, Yizhak Yisrael Elboher, Tobias Ladner, Volkan Şahin+3

Hebrew University of Jerusalem, Israel · Technical University of Munich, Germany · Masaryk University, Czech Republic

Interpretable ML Neural Network Interpretability

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

Provably Explaining Neural Additive Models

Beyond L2L_2L2​: Generalizing Abductive Latent Explanations to Diverse Prototype-Based Architectures

Neuron Activation-based Computation of Logical Explanations for Deep Neural Networks

Beyond $L_2$ : Generalizing Abductive Latent Explanations to Diverse Prototype-Based Architectures