FAME: Formal Abstract Minimal Explanation for Neural Networks
Authors: Ryma Boumazouza
Raya Elsaleh
Melanie Ducoffe
Shahaf Bassan
Guy Katz
Venue: ICLR 2026 Poster (2026)
Keywords: abductive explanations
abstract interpretation
robustness
NN verification
Primary area: interpretability and explainable AI
TL;DR: We introduce FAME, a novel method grounded in abstract interpretation that efficiently generates formal, minimal explanations for large neural networks by leveraging dedicated perturbation domains.

Abstract: We propose $\textbf{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 $\textbf{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 $VERI{\large X}+$ refinement step. We benchmark FAME against $VERI{\large X}+$ and demonstrate consistent gains in both explanation size and runtime on medium- to large-scale neural networks.

Published as a conference paper at ICLR 2026
FAME: FORMAL ABSTRACT MINIMAL EXPLANATION FOR NEURAL NETWORKS
Ryma Boumazouza" 1,2 Raya Elsaleh*3 Melanie Ducoffe Shahaf Bassan and Guy Katz² 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 ab- ductive explanations grounded in abstract interpretation. FAME is the first method to scale to large neural networks while reducing explanation size. Our main contri- bution 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 formal abstract minimal explanation. To assess explanation quality, we introduce procedure that measures the worst-case distance between an abstract minimal ex- planation and 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.
INTRODUCTION
Breaking the Sequential Bottleneck
From Abstruct Explanction Minimality
Loop
Loug
Relined Perlurbetion
Domain (cardiratty (r.44)
Abstract Singleton
Attack
Singllln
Accttoon
VERIX+
LIRPA Batch Cerlfiable Freeing
Dist i IwXXp*) [oxp
XAI
wAXpp
wAXp*
AXp
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 influence on the model's decision) features based on batch certificate (Section 4.2). This iterative process operates within a refined, cardinality- constrained perturbation domain, 22Th 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, |wAXp<"1 4" |AXp], serves as an evaluation metric of phase 1.
Neural network-based systems are being applied across wide range of domains. Given AI tools' strong capabilities complex analytical tasks, a significant portion of these applications now in- volves tasks that require reasoning. These tools often achieve impressive results in problems quiring intricate analysis to reach correct conclusions. Despite these successes, a critical challenge remains: understanding the reasoning behind neural network decisions. The internal logic of a neural network is often opaque, with its conclusions presented without accompanying justifications. This lack of transparency undermines the trustworthiness and reliability of neural networks, especially in high-stakes or regulated environments. Consequently, the need for interpretable and explainable AI (XAI) has become a growing focus in recent research.
"Equal contribution.

---

Published as a conference paper at ICLR 2026
Two main approaches have emerged to address this challenge. The first employs statistical and heuristic techniques to infer explanations based on network's s internal representations (Fel et al., 2022). While these methods estimate feature importance, that require empirical evaluation (such as the y--Fidelity metric (Bhatt et al., 2020)), the second approach leverages automated reasoners and formal verification provide provably correct explanations grounded in logical reasoning.
We ground our work in the formal definition of Abductive Explanations (AXp) (Ignatiev et al,, 2019), concept belonging to the broader family of "formal XAI" which includes minimal explana- tions, also known as local-minimal, minimal unsatisfiable subsets (Marques-Silva, 2010) and prime implicants (Shih et al., 2018). An AXp is a subset of features guaranteed to maintain the model's prediction under any perturbation within defined domain. In a machine learning context, these explanations characterize feature sets where removing any single feature invalidates the guarantee, effectively representing subsets that preserve the decision's 's robustness. However, a major hurdle for formal XAI is high computational cost due to the complexity of reasoning, preventing it from scaling to large neural networks (NNs) (Marques-Silva, 2023b). This limitation, combined with the scarcity of open-source libraries, significantly hinders its adoption. Initial hybrid approaches, such the EVA method (Fel et al., 2023), have attempted to combine formal and statistical methods, but these often fail to preserve the mathematical properties of the explanation. However, robustness- based approaches address the scalability challenges of formal XAI for NN by leveraging funda- mental connection between AXps and adversarial examples (Huang & Marques-Silva, 2023).
In this work, we present FAME, scalable framework for formal XAI that addresses the limi- tations of existing methods. Our contributions are fourfold:
Formal abstract explanations. We introduce the first class of abductive explanations derived from abstract interpretation, enabling explanation algorithms to handle high- dimensional NNs.
Eliminating traversal order. We design perturbation domains and a recursive refinement procedure that leverage Linear Relaxation based Perturbation Analysis (LiRPA)- cer- tificates to simultaneously discard multiple irrelevant features. This removes the sequential bottleneck inherent in prior work and yields an abstract minimal explanation.
Provable quality guarantees. We provide the first procedure to measure the worst-case gap between abstract minimal explanations and true minimal abductive explanations, com- bining adversarial search with optional VERIX+ refinement.
Scalable evaluation. We benchmark FAME medium- and large-scale neural networks, showing consistent improvements in both explanation size and runtime over VERIX+. No- tably, we produce the first abstract formal abductive explanations for ResNet architecture on CIFAR-10, demonstrating scalability where exact methods become intractable.
ABDUCTIVE EXPLANATIONS & VERIFICATION
2.1 NOTATIONS
Scalars are denoted by lower-case letters (e.g., I), and the set of real numbers by R. Vectors are denoted by bold lower-case letters (e.g., x), and matrices by upper-case letters (e.g.. W). The i-th component of a vector x (resp. line of matrix W) is written as x; (resp. W,). The matrix W (resp. 5 represents the same matrix with only nonnegative (resp. nonpositive) weights. Sets are written in calligraphic font (e.g., S). We denote the perturbation domain by Ω and the property to be verified by P.
2.2 THE VERIFICATION CONTEXT
We consider neural network as a function f R + R The core task of verification is to determine whether the network's 's output f(z') satisfies a given property P for every possible input I' within specified domain ②(x) RR. When verification fails, it means there is at least one input I' in the domain ②(x) that violates the property P (a counterexample). The verification task can be written as: Va' 2(r), does f(x') satisfy P? This requires defining two components:
2

---

Published as a conference paper at ICLR 2026
1. The Perturbation Domain (S2): This domain defines the set of perturbations. It is often an 1p-norm ball around a nominal imput z, such as an lec ball for modeling imperceptible noise: 52 = {x' E R ||x - <c.
x'
2. The Property (P): This is the specification the network must satisfy. For a classification task where the network correctly classifies an input x into class e, the standard robustness property P asserts that the logit for class c cremains the highest for any perturbed input x':
P(x')
= min (Ja(x)) fi(x') > 0 kfc
(1)
For instance, given an MNIST image x of '7' and a perturbation radius the property P holds if the network's 's logit for class '7' provably exceeds all other logits for every perturbed image x' E ((()).
A large body of work has investigated formal verification of NNs, with adversarial robustness be- ing the most widely studied property (Urban & Miné, 2021). Numerous verification tools are now available off-the-shelf, and for piecewise-linedt models f with corresponding input domains and properties, exact verification is possible (Katz et al., 2017; Botoeva et al., 2020). In practice, how- ever, exact methods quickly become intractable for realistic networks. To address this, rely on Abstract Interpretation, a theory of sound approximation. Specifically, we utilize Linear Relaxation- based Perturbation Analysis (LiRPA) (Zhang et al., 2018: Singh al., 2019) which efficiently over- approximates the network's 's output by enclosing it between linear upper and lower bounds. Such abstractions enable sound but conservative verification: if the relaxed property holds, the original one is guaranteed to hold as well. We provide a comprehensive background in Appendix A.
2.3 ABDUCTIVE EXPLANATIONS: PINPOINTING THE "WHY"
Understanding Model Robustness with Formal Explanations: Neural networks often exhibit sensitivity to minor input perturbations, a phenomenon that certified training can mitigate but not eliminate (De Palma et al., 2025). Even robustly trained models may only have provably safe regions spanning few pixels for complex tasks like ImageNet classification (Serrurier et al., 2021). To build more reliable systems, it is crucial to understand why a model's prediction robust (or not) within given context. Formal explainability provides a rigorous framework for this analysis.
We focus on ubductive explanations (AXps, also called distance-restricted explanations (e-AXp) (gnaatev et al., 2019; Huang & Marques-Silva, 2023), which identify subset of input features that are sufficient to guarantee that the property P holds. Formally, a local formal abductive explanation is defined as a subset of input features that, if collapsed to their nominal values (i.e., the sample x), ensure that the local perturbation domain f2 surrounding the sample contains no counterexamples. Definition 2.1 (Weak Abductive Explanation (wAXp) ). Formally, given triple (x, S2, P), an planation is a subset of feature indices X' F (1,....n) such that
(A(x' (x'1 - (xx==x)) VEX
wAXp: Vx E ((x),
- {(X)
(2)
While many such explanations may exist (the set of all features F is a trivial one), the most useful explanations are the most concise ones (Bassan & Katz, 2023). We distinguish three levels:
Minimal Explanation: An explanation X' is minimal if removing any single feature from it would break the guarantee (i.e., X') \ {5} is no longer an explanation for any j E 2¹). These are also known as minimal unsatisfiable subsets(Ignatiev et al., 2016; Bassan & Katz, 2023).
Minimum Explanation: An explanation X minimum if has the smallest possible number of features (cardinality) among all possible minimal explanations.
The concept of an abductive explanation is illustrated using classification task (details in Appendix D.I, Figure 4). The goal is to find minimal subset of fixed features (2²) that guarantees sample's classification within its perturbation domain. For the analyzed sample, fixing X2 alone is insufficient due to the existence of counterexample (Figure 5). However, fixing the set X = {x2, x3) creates 'safe' subdomain without counterexamples, confirming it is an abductive explanation. This explana- tion is minimal (neither x2 x3 work alone) but not minimum in cardinality, as X' {x: } is also
a valid minimal explanation. In the rest of this paper, we will use the terms abductive explanation or formal explanation and the notation WAXp to refer to Definition 2.1.
3

---

Published as a conference paper at ICLR 2026
3 RELATED WORK
Substantial progress has been made in the practical efficiency of computing formal explanations. While finding an abductive explanation (AXp) is tractable for some classifiers (Marques-Silva, 2023a; Darwiche & Ji, 2022: Huang et al., 2022; 2021; Izza et al., 2020; Marques-Silva et al., 2020; 2021), it becomes computationally hard for complex models like random forests and neural networks (Ignatiev& & Marques-Sin Silva, 2021; Izza & Marques-Sile Silva, 2021). To address this inherent complexity, these methods typically encode the problem as a logical formula, leveraging automated reasoners like SAT, SMT, and Mixed Integer Linear Programming (MILP) solvers (Audemard et al., 2022; Ignatiev, 2020; Ignatiev et al., 2022: Ignatiev & Marques-Silva, 2021; Izza & Marques-Sii -Sila,, 2021). Early approaches. such as deletion-bast -baeed (Chinneck & Dravnicks, 1991) and insertion- -based (de Siqueira, 1988) algorithms. are inherently sequential, thus requiring an ordering of the input fea- tures traditionally denoted as traversal ordering. They require number of costly verification calls linear with the number of features, which prevents effective parallelization. As an alternative, sur- rogate models have been used to compute formal explanations for complex models (Boumazouza et al., 2021: 2023), but the guarantee does not necessary hold on the original model.
Recent work aims to break the sequential bottleneck, by linking explainability to adversarial robust- ness and formal verification. DistanceAXp Xp (Huang & Marques-Silva, 2023; La Malfa et al., 2021) is a key example, aligning with our definition of AXp and enabling the use of verification tools.
The latest literature focuses on breaking the sequential bottleneck using several strategies that in- clude parallelization. This is achieved either by looking for several counterexamples at once (Izza et al., 2024; Bassan & Katz, 2023; La Malfa et al., 2021: Bassan et al., 2023) or by identifying a set of irrelevant features simultaneously, as seen in VERIX (Wu et al., 2023), VERIX+ (Wu et al., 2024b), and prior work (Bassan & Katz, 2023). For instance, VERIX+ introduced stronger traversal strategies to alleviate the sequential botrleneck. Their binary search approach splits the remaining feature set and searches for batches of consecutive irrelevant features, yielding the same result as se- quential deletion but with fewer solver calls. They also adapted QuickXplain (Junker, 2004), which can produce even smaller explanations at the cost of additional runtime by verifying both halves. Concurrently, (Bassan & Katz, 2023) proposed strategies like the singleton heuristic to reuse verifi- cation results and derived provable size bounds, but their approach remains significantly slower than VERIX+ and lacks publicly available code.
The identified limitations are twofold. First, existing methods rely heavily on exact solvers such as Marabou (Katz et al., 2019; Wu et al., 2024a), which do not scale to large NNs and are restricted to CPU execution. Recent verification benchmarks (Brix et al., 2023; Ducoffe et al., 2024; Zhao al., 2022) consistently demonstrate that GPU acceleration and distributed verification are indispensable for achieving scalability. Second, these approaches critically depend on traversal order. As shown in VERIX, the chosen order of feature traversal strongly impacts both explanation size and runtime. Yet, determining an effective order requires prior knowledge of feature importance, precisely the information that explanations are meant to uncover, thus introducing circular dependency. Never- theless, VERIX+ currently represents the SOTA for abductive explanations in NNs, achieving the best trade-off between explanation size and computation time.
Our work builds on this foundation by directly addressing the sequential bottleneck of formal ex- planation without requiring traversal order, a first in formal XAI. We demonstrate that leveraging incomplete verification methods and GPU hardware is essential for practical scalability. Our ap- proach offers a new solution to the core scalability issues, complementing other methods that aim to reduce explanation cost through different means (Bassan al., 2025b:a).
4 FAME: FORMAL ABSTRACT MINIMAL EXPLANATION
In this section, we introduce FAME, a framework that builds abstract abductive explanations (Def- inition 4.1). FAME proposes novel strategies to provide sound abstract abductive explanations (wAXp^) such as an Abstract Batch Certificate using Knapsack formulation, and Recursive Re- finement, relying on raw bounds provided by a formal framework (we use LiRPA in this paper).
Definition 4.1 (Abstract Abductive Explanation (wAXp^)). Formally, given a triple (x, P), an abstract abductive explanation is subset of feature indices X C F (1,..., n) such that, under
4

---

Published as a conference paper at ICLR 2026
an abstract interpretation f of the model f. the following holds:
(
A (Axx (x': (xx==xx) = FP VEXA
wAXp Vx' E [((x),
(3)
Here, / = LiRPA(J; Q2) denotes the sound over-approximated bounds of the model outputs on the domain Ω2 as computed by the LiRPA method. If Eq. (3) holds, any feature outside X can be considered irrelevant with respect to the abstract domain. This ensures that the concrete implication f(x') = P also holds for all x' E Ω. In line with the concept of abductive explanations, we define an abstract minimal explanation as an abstract abductive explanation (wAXp") A') a set of features X from which feature can be removed without violating Eq. (3).
Due to the over-approximation as detailed Section 2.2, any abstruct abductive explanation is a weak abductive explanation for the model f. In the following we present the first steps described in Figure to build such a wAXp".
4.1 THE ASYMMETRY OF PARALLEL FEATURE SELECTION
In the context of formal explanations, adding a feature means identifying it as essential to a model's decision (causes the model to violate the desired property P), so its value must be fixed in the expla- nation.Comm Conversely. freeing a feature means identifying it as irrelevant, allowing it to vary without affecting the prediction. A key insight is the asymmetry between these two actions: while adding necessary features can be parallelized naively, freeing features cannot due to complex interactions.
Proposition 4.1 (Simultaneous Freeing). it is unsound to free multiple features at once based only on individual verification as two features may be individually irrelevant yet jointly critical.
Parallelizing feature freeing based on individual verification queries is unsound due to hidden fea- ture dependencies that stem from treating the verifier as simple binary oracle (SAT/UNSAT; see Appendix A for formal definitions) (Proposition 4. To solve this, we introduce the Abstract Batch Certificate (AA) (Definition 4.2). Unlike naive binary checks, ((.A) leverages abstract interpreta- tion to compute joint upper bound the worst-case contribution of the entire set A simultane- ously. If & (AA) & 0, it mathematically guarantees that simultancously freeing A is sound, explicitly accounting for their combined interactions. The formal propositions detailing this asymmetry is provided in the Appendix B.
4.2 ABSTRACT INTERPRETATION FOR SIMULTANEOUS FREEING
Standard solvers act as "binary oracle" and their outcomes (SAT/UNSAT) are insufficient to certify batches of features for freeing without a traversal order. This is because of feature dependencies and the nature of the verification process. We address this by leveraging inexact verifiers based on abstract interpretation (LiRPA) to extract proof objects (linear bounds) that conservatively track the contribution of any feature set. Specifically, we use CROWN (Zhang al., 2018) define an abstract batch certificate & in Definition 4.2. If one succeeds in freeing a set of features A given Φ, we denote such an explanation as a formal abstract explanation that satisfies Proposition 4.2.
Definition 4.2 (Abstract Batch Certificate). Let A be a set of features and Ω any perturbation do- main. The abstract batch certificate defined as:
(AA
max (1(x)+ (())=Eas))
ifc
JEA
where the baseline bias (worst-case margin of the model's output) at x is T (a) = W xx + w
20 (i, x,), W: (z) - m4)) and the contribution of each feature j E A is Ctj = max W J
with ž, = max(2'; (z/}- : x'' E [(x)} and z; = minfaz x' E [(x)). The weights W and biases
w are obtained from LiRPA bounds, which guarantee for each target class i * with being the groundtruth class:
Va' E M(x), f(x') fc(x') s (T)((')) W o wo.
5

---

Published as a conference paper at ICLR 2026
Proposition 4.2 (Batch-Certifaable Freeing). If (() I 0, then FF A is weak abductive explanation (wAXp).
Lemma 4.1. If ((A) < 0, freeing all features in A is sound; that is, the property P holds for every x E'E (2()) with { IR)KEAAA
The proof of Proposition 4.2 is given in Appendix B. The trivial case A = always satisfies the certificate, but our goal is efficiently certify large feature sets. The abstract batch certificate also highlights two extreme scenarii. In the first, if (FF I O, all features are irrelevant, meaning the property holds across Q without fixing any inputs. In the second, if 0' (ar) 2 for some + e, then ( 0 and no feature can be safely freed; this situation arises when the abstract relaxation too loose, producing vacuous bounds. Avoiding this degenerate case requires careful selection of the perturbation domain, consideration highlight for the first time in the context of abductive explanations. The choice of abstract domain is discussed in Section 5.
4.3 MINIMIZING THE SIZE OF AN ABSTRACT EXPLANATION VIA A KNAPSACK FORMULATION
Between the trivial and degenerate cases lies the nontrivial setting: finding a maximal set of irrele- vant features A free given the abstract batch certificate $. Let denote the index of features. Maximizing |A| can be naturally formulated as 0/1 Multidimensional Knapsack Problem (MKP). For each feature j E F, we introduce a binary decision variable yJ indicating whether the feature is selected. The optimization problem then reads:
S iEL,
max 9
yj s.t.
JEF
JEF
where Gij represents the contribution of feature j to constraint i, and -b'(x) is the corresponding knapsack capacity. The complexity of this MKP depends on the number of output classes. For binary classification (k 2), the problem is linear'. In the standard multiclass setting (k > 2). however, the MKP is NP-hard. While moderately sized instances can be solved exactly using a MILP solver, this approach does not scale to large feature spaces. To ensure scalability, we propose a simple and efficient greedy heuristic, formalized in Algorithm heuristic iteratively selects the feature j* that is least likely to violate any of the k- constraints, by minimizing the maximum normalized cost across all classes. An example is provided Appendix D.2. This procedure is highly parallelizable, since all costs can be computed simultaneously. While suboptimal by design, it produces a set A such that ((A;; Q2) S O. A key advantage of this greedy batch approach is its computational efficiency. The cost is dominated by the computation of feature contributions G.j- This requires a single backward pass through the abstract network, which has complexity of OT. N) (where T. is depth and N is neurons) and is highly parallelizable GPUs. In contrast, exact solvers require solving an NP-hard problem for each feature or batch. In Section 7, we compare the performance of this greedy approach against the optimal MILP solution, demonstrating that it achieves competitive results with dramatically improved scalability.
Rather than solving the full MKP, the
Algorithm Greedy Abstract Batch Freeing (One Step)
1: Input: model f. perturbation domain Ω² candidate set F
2: Initialize: <- 0, linear bounds (W', w' = LiRPA(J, (f))
3: Do: compute Cryy in parallel
4: while ((A) < and [Fl > 0 do
5: pick j = arg min maxişe Gi. (-b;)
D Parallel reduction
6: if de (AAU {}* < 0 and |A| S m then
7:
A + AU {1*}
8:
end
9:
F+ F\ {i*}
> Remove candidate
10:
end while
11:
Return: A
lt can be solved optimally in (nn) time by sorting features by ascending contribution cı,j and greedily adding them until the capacity is exhausted.

---

Published as a conference paper at ICLR 2026
5 REFINING THE PERTURBATION DOMAIN FOR ABDUCTIVE EXPLANATION
Previous approaches for batch freeing reduce the perturbation domain using a traversal order n, defining (x) {x' _ ||x x'1 E, x' Xx. These methods only consider freeing dimensions up to certain order. However, as discussed previously. determining an effective order requires prior knowledge of feature importance, the very information that explanations aim to uncover. introducing a circular dependency. This reliance stems from the combinatorial explosion: the number of possible subsets of input features grows exponentially, making naive enumeration of abstract domains intractable.
To address this, we introduce a new perturbation domain, denoted the cardinality-constranned per- turbation domain. For instance, one can restrict to to fo-bounded perturbations:
2 (x) = {x' E R" ||x - x' ol Se, |x - x x'1oo S m].
which ensures that at most m features may vary simultaneously. This concept is closely related to the norm and has been studied in verification (Xu al., 2020), but, to the best of our knowledge, it is applied here for the first time in the context of abductive explanations. The greedy procedure in Algorithm can then certify batch of irrelevant features under this domain. Once set A is freed, the feasible perturbation domain becomes strictly smaller, enabling tighter bounds and the identification of additional irrelevant features. We formalize this as the refined abstruct domain that ensures that at most m features can vary in addition to the set of previously seclected ones A:
12Th (x; 22 A) = (x' E R" ||x - x' Se, |XFIAA - x' x'alllo S m)}
By construction, 2TTh (x; A) S Q (x)+, so any free set derived from (x;" A) remains sound for the original budget strictly smaller abstract explanation. This refinement naturally suggests a recursive strategy: after one round of greedy batch freeing, we restrict the domain to Q ( A)) A), recompute LiRPA bounds, and reapply Algorithm for m = 1... JI....FF.... Al. Unlike the static traversal of prior work (e.g., VERIX+), FAME employs dynamic. cost-based selection by re-evaluating abstract costs CLj at each recursive step. This process functions as an adaptive abstraction mechanism: iteratively en- foreing cardinality constraints tightens the domain, reducing LiRPA's over-approximation error and enabling the recovery of additional frecable features initially masked by loose bounds. As detailed in Algorithm 2, this process can be iterated, progressively shrinking the domain and expanding A. In practice, recursion terminates once no new features can be freed. Finally, any remaining candi- date features can be tested individually using the binary search approach proposed by VeriX+ but replacing Marabou by CROWN (see Algorithm 5). This final step ensures that obtain formal abstract minimal explanation, as defined in Definition 4.1
[AI. Recomputing linear bounds this tighter domain often yields
Algorithm Recursive Abstract Batch Freeing
1: Input: model f, input x, candidate set F
2: Initialize: A 0
certified free set
3: repeat
4: Abest
0
5: for m = 1 IF..FFy Al do
6:
Am + GREDXAABSTTACBBBBCCERRENN S2Th (x"; AF
7:
if Aml > Abestt then
8:
Abest &- Am
9:
end if
10: end for
11:
A A AU Abest
12: until Abest =
13:
A= ITERATIVE SINGLETON FREE(F, A)
> refine by testing remaining features
14: Return: A
6 DISTANCE FROM ABSTRACT EXPLANATION TO MINIMALITY
Algorithm returns a minimal abstract explanation: with respect to the chosen LiRPA relaxation, the certified free set A cannot be further enlarged. This guarantee is strietly weaker than minimality

---

Published as a conference paper at ICLR 2026
in the exact sense. The remaining features may still include irrelevant coordinates that abstract interpretation fails to certify, due to the coarseness of the relaxation. In other words, minimality is relative to the verifier: stronger but more expensive verifiers (e.g., Verix+ with Marabou) are still required to converge to a true minimal explanation.
We achieve this via two-phase pipeline (Figure 1). Phase (Abstract Pruning) generates sound abstract explanation wAXp Phase (Exact Refinement) minimizes this candidate using VERIX+, ensuring the final output is guaranteed minimal. The gap arises from the tradeoff between verifier accuracy and domain size. Abstract methods become more conservative as the perturbation domain grows, while exact methods remain sound but scale poorly. This motivates hybrid strategies that combine fast but incomplete relaxations with targeted calls exact solvers. As an additional acceleration step, adversarial attacks can be used. By Lemma B.I, if attacks identify features that must belong to the explanation, they can be added simultaneously (see Algorithm 4). Unlike abstract interpretation, the effectiveness of adversarial search typically increases with the domain size: larger regions make it easier to find counterexamples.
Towards minimal explanations. In formal XAI, fidelity is hard constraint guaranteed by the verifier. Therefore, the explanation cardinality (minimality) becomes the only metric to compare formal abductive explanations. A smaller explanation is strietly better, provided it remains sufficient. Our strategy is use the minimal abstract explanation (wAXp"") as starting point, and then search for the closest minimal explanation. Concretely, we aim to identify the largest candidate set of potentially irrelevant features that, if freed together, would allow all remaining features to be safely added to the explanation at once. A good traversal order of the candidate space is crucial here, as determines how efficiently such irrelevant features can be pinpointed. Formally, if X denotes the minimal abstract explanation and X' the closest minimal explanation, we define the absolute distance to minimality as the number of irrelevant features not captured by the abstract method: d(xeA, x²1) x X
7 EXPERIMENTS
To evaluate the benefits and reliability of our proposed explainability method, FAME, we performed series of experiments comparing its performance against the SoTA VERIX+ implementation. We assessed the quality of the explanations generated by FAME by comparing them to those of VERIX+ across four distinct models, including both fully connected and convolutional neural net- works (CNNs). We considered two primary performance metrics: the runtime required to compute single explanation and the size (cardinality) of the resulting explanation.
Our experiments, as in VERIX+ (Wu et al., 2024b), were conducted on two widely-used image classification datasets: MNIST (Yann, 2010) and GTSRB (Stallkamp et al., 2012). Each score was averaged over non-robust samples from the 100 samples of each dataset. For the comparison results, the explanations were generated using the FAME framework only, and with final run of VERIX+ to ensure minimality (See Figure 1).
VERIX- (olone)
FAME: Single-mund
FAME: Hemiiie refinement
FAMF-acceleraeed VERIX. / bounds
Traversal onder
bounds
Search prucedure
binary
MILP
Greedy boAXyy
MILP
Greedy [w4Xyy'
Gready + binzry
Metrics
|4Xpl
time
IoAXp"
time
[candiddse-sstt
[AXpl
time
MNIST-C
280.16
13.87
441.05
448.37
0.35
239.75 73
14.30
225.14
8.78
44.21
224.41
13.72
MNIST-CNN
56.72
5.59
190.29
124.9
122.09
5.6
113.53
GTSRB-PC
313.42
56.18
236.85
9.68
243.18
0.97
331,84
12.28
392,74
5.26
11.98
332.66
9.26
GTSRB-CNN
338.28
185.03
372.66
12.45
379.34
1.35
322 42
17.63
322,42
7,42
219.57
322.42
138.12
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.
Experimental Setup All experiments were carried out on a machine equipped with an Apple M2 Pro processor and 16 GB of memory. The analysis is conducted on fully connected (-FC) and convolutional (-CNN) models from the MNIST and GTSRB datasets, with set to 0.05 and 0.01 respectively. The verified perturbation analysis was performed using the DECOMON library². ap-
Phans:/ggtthhh.mmmaiiits//ccooom
8

---

Published as a conference paper at ICLR 2026
Explaration size: Veris Fame
Explonation Fame
1200
IC can
Insi cad- Tue cantefabee
MNST cardetres
MAET CaN candetube
tnavct -adi
Uiska cart-ratee
GTSRD can cardnitue
onaea coscadd-nn
taronfale
30 100
133 200
250
300
350
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 cardinality constraint (|1 x' z'Ilo S m) applied.
plying the CROWN method with normo.. The NN verifier Marabou (Katz al., 2019) used within VERIX+. We included a sensitivity analysis covering: (1) Solver Choice, confirming the Greedy heuristic's near-optimality vs. MILP (Table 1); (2) Cardinality Constraints, showing that card-True yields significantly smaller explanations (Figure 2); and (3) Perturbation Magnitude (e), which we fixed baseline used by VERIX+ for direct comparison. We include additional experi- mental results on the ResNet-2B architecture (CIFAR-10) from the VNN-COMP benchmark (Wang al., 2021) to demonstrate scalability on deeper models. The complete set of hyperparameters and the detailed architectures of the models used provided in Appendix E for full reproducibility.
7.1 GREEDY VS. MILP FOR ABSTRACT BATCH FREEING
Performance in Single Round This experiment, in the 'FAME: Single Round' column of Table 1, compares the runtime and size of the largest free set obtained in single round using the greedy method versus an exact MILP solver for the abstract batch freeing (Algorithm 1).
Across all models, the greedy heuristic consistently provided significant speedup (ranging from 9x to 12x) while achieving an abstract explanation size very close (fewer than 9 features average) to that of the optimal MILP solver. This demonstrates that, for single-round batch freeing, the greedy method offers a more practical and scalable solution.
Performance with Iterative Refinement This experiment compares the methods in iterative setting of the abstract batch freeing, where the perturbation domain is progressively refined (Sec- tion 5). For the iterative refinement process, the greedy approach maintained a substantial runtime advantage over the MILP solver, with a speedup up to 2.4x on the GTSRB-CNN CNN model, while producing abstract explanations that were consistently close in size to the optimal solution. The distinction between the circle and square markers is significant in Figure 2. The square markers (card=False) tend to lie closer to or even above the diagonal line. This suggests that the cardinality- constrained domain, when successful, is highly effective at finding more compact explanations.
Impact Iterative Refinement: Comparing 'FAME: Single-round' vs. 'FAME: Iterative refine- ment' in Table 1 isolates the impact of Algorithm 2. For MNIST-CNN, iterative refinement reduces explanation size by 36% (190.29 to 122.09). This highlights the trade-off: a modest increase in runtime yields significantly more compact explanations.
7.2 COMPARISON WITH STATE-OF-THE-ART (VERIX+)
We compare in this section the results of VERIX+ (alone) vs. FAME-accelerated VERIX+
Explanation Size and Runtime: FAME consistently produces smaller explanations than VERIX+ while being significantly faster, mainly due to FAME's iterative refinement approach, as visually confirmed by the plots in Figure 2 that show majority of data points falling below the diagonal line

---

Published as a conference paper at ICLR 2026
for both size and time comparisons. The runtime gains are particularly substantial for the GTSRB models (green and red markers), where FAME's s runtime often only a small fraction of VERIX+'s
as shown in Table 1. In some cases, FAME delivers a non-minimal set that is smaller than VERIX+
's minimal set, with up to a 25x speedup (322.42 features in 7.4s compared to 338.28 in 185.03s
for the GTSRB-CNN model) while producing wAXp that were consistently close in size to the
optimal solution.
The Role of Abstract Freeing:
The effectiveness of FAME'S approach is further supported by the "distance to minimality" metric. The average distance to minimality was 44.21 for MNIST-FC and 104.09 for MNIST-CNN. An important observation from our experiments is that when the abstract domains in FAME are effective, they yield abstract abductive explanations wAXp" that are smaller than the abductive explanations (AXp) from VERIX+ This is not immediately obvious from the summary table, as the final explanations may differ. Conversely, when FAME's abstract domains fail to find a valid free set, our method defaults to binary search approach similar to VERIX+. However, since we do not use the Marabou solver in this phase, the resulting wAXp" is larger than the AXp provided by Marabou. This highlights the trade-off and the hybrid nature our approach.
Finally, to demonstrate the generality of our framework beyond standard benchmarks, in Appendix F we provide additional experiments on the ResNet-2B architecture Wang al. (2021) trained on CIFAR-10. 10. These results represent, to the best of our knowledge, the first formal explanations gen- erated for such a complex architecture, highlighting FAME as an enabling technology for scalability.
CONCLUSION AND DISCUSSION
In this work, we introduced FAME (Formal Abstract Minimal Explanations), a novel framework for computing abductive explanations that effectively scales to large neural networks. By leveraging a hybrid strategy grounded in abstract interpretation and dedicated perturbation domains, we success- fully addressed the long-standing sequential bottleneck traditional formal explanation methods.
Our main contribution is a new approach that eliminates the need for traversal order by progressively shrinking dedicated perturbation domains and using LiRPA-based bounds to efficiently discard ir- relevant features. The core of our method relies on greedy heuristic for batch freeing that, as analysis shows, is significantly faster than an exact MILP solver while yielding comparable expla- nation sizes.
Our experimental results demonstrate that the full hybrid FAME pipeline outperforms the current tfate-of-the-ar VERIX+ baseline, providing superior trade-off between computation time and explanation quality. We consistently observed significant reductions in runtime while producing explanations that close to true minimality. This success highlights the feasibility of computing formal explanations for larger models and validates the effectiveness of our hybrid strategy.
Beyond its performance benefits, the FAME framework is highly generalizable. Although our eval- uation focused on classification tasks, the framework can be extended to other machine learning applications, such as regression. While we focused on robustness in continuous domains, FAME'S high-level algorithms (batch certificate, greedy selection) support discrete features (see Appendix B). LiRPA natively handles discrete variables (e.g., one-hot encodings) via contiguous interval bounds. Furthermore, the framework can support other properties like local stability. Additionally, FAME can be configured to use exact solvers for the final refinement step, ensuring its adaptability and robustness for various use cases.
Finally, we demonstrated FAME's scalability on the ResNet-2B 10F architecture. Although the abstraction gap naturally widens with depth, FAME's ability to rapidly prune irrelevant features establishes it as a critical enabling step for applying formal XAI to complex models where exact-only methods are currently intractable. By designing framework that natively leverages certificates from modern, GPU-enabled verifiers, this work effectively bridges the gap between formal guarantees and practical scalability.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGEMENTS
Our work has benefited from the Al Cluster ANITI and the research program DEEL. ANITI is funded by the France 2030 program under the Grant agreement n² MANR-23-IAAL--AA
DEEL an integrative program of the Al Cluster ANITI, designed and operated jointly with IRT Saint Exupéry, with the financial support from its industrial and academic partners and the France 2030 program un- der the Grant agreement n" APAAN- AAR-10-AATR O0-ARR--0.. Within the DEEL program, we are especially grateful to Franck MAMALET for their constant encouragement, valuable discussions, and insightful feed- back throughout the development of this work. The work of Elsalch, Bassan, and Katz partially funded by the European Union (ERC, VeriDeL, 101112713). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them. The work of Elsaleh, Bassan, and Katz was additionally supported by a grant from the Israeli Science Foundation (grant number 558/24). Elsaleh is also supported by the Ariane de Rothschild Women Doctoral Program.
REFERENCES
Gilles Audemard. Steve Bellart, Louenas Bounia, Frédéric Koriche, Jean-Maric Lagniez, and Pierre Marquis. Trading complexity for sparsity in random forest explanations. In Proceedings of the AAAI Conference Artificial Intelligence, volume 36, pp. 5461-5469, 2022.
Bassan, Yizhak Yisrael Elboher, Tobias Ladner, Matthias Althoff, and Guy Katz. Explaining. Fast and Slow: Abstraction and Refinement of Provable Explanations. In Proc. 42nd Int. Conf. on Machine Learning (ICML), 2025a.
Shahaf Bassan and Guy Katz. Towards formal xai: formally approximate minimal explanations of neural networks. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 187-207. Springer, 2023.
Shahaf Bassan, Guy Amir, Davide Corsi, Idan Refaeli, and Guy Katz. Formally Explaining Neural Networks Within Reactive Systems. In Proc. 23rd Int. Conf. on Formal Methods in Computer- Aided Design (FMCAD), pp. 1-13, 2023.
Shahaf Bassan, Ron Eliav, and Shlomit Gur. Explain Yourself. Briefly! Self-Explainnng Neural Networks with Concise Sufficient Reasons. In Proc. 13th Int. Conf. on Learning Representations (ICLR), 2025b.
Umang Bhatt, Adrian Weller, and José M. F. Moura. Evaluating and aggregating feature-basse model explanations. In Christian Bessiere (ed.), Proceedings of the Twenty-inth International Joint Conference Artificial Intelligence, IJCAI-20, pp. 3016-3022. International Joint Con- doi: 10.24963/jcci. https:///ol/ org/10.../.o.o..... 249634 /tt///jcaa.... 2020/ 417. Main track.
ferences on Artificial Intelligence Organization, 7 2020.
URL
Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. Efficient neural networks via dependency analysis. Proceedings of the AAAI
verification of Conference on Artificial Intelligence, 34(00):3291 5729. URL teattps://oo/ aaai .rgg indexiiixxi///m www..ppp//apa. /AAI/ http///rttcclleee/////////
Apr. 2020. doi: 10. /..69//aai.v34400
Ryma Boumazouza, Fahima Cheikh-Alili, Bertrand Mazure, and Karim Tabia. Asteryx: A model- agnostic sat-based approach for symbolic and score-based explanations. Proceedings of the 30th ACM International Conference on Information & Knowledge Management, pp. 120-129, 2021.
Ryma Boumazouza, Fahima Cheikh-Alili, Bertrand Mazure, and Karim Tabia. Symbolic explana- tions for multi-label classification. In 15th International Conference on Agents and Artificial Intelligence (ICAART 2023), volume 3, pp. 342-349. SCITEPRESS-Seiene and Technology Publications, 2023.
httpp::/ htts:///wwwdwee aii/
11

---

Published as a conference paper at ICLR 2026
Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The fourth international ver- ification of neural networks competition (VNN-COMP 2023): Summary and results. CoRR, abs/2312.16760, 2023. doi: ID48550/ARXIV.312..6666 URL attps:///ol. or. 48550/arXis 2.31 2, 6760.
John W Chinneck and Erik W Dravnicks. Locating minimal infeasible constraint sets in linear programs. ORSA Journal on Computing, 3(2):157-166, 1991.
Adnan Darwiche and Chunxi Ji. On the computation of necessary and sufficient explanations. In Proceedings of the AAAI Conference Artificial Intelligence, volume 36, pp. 5582-5591, 2022.
Alessandro De Palma, Serge Durand, Zakaria Chihani, and Caterina Urban. On Using Certified Training towards Empirical Robustness. Transactions on Machine Learning Research Journal, 2025. URL https: inria.iiii. hal. scienceeeaaaa -0044-08884448
de Siqueira. Jl, and puget. j.-f. 1988. explanationbased generalisation of failures. In Proceedings of the Eighth European Conference Artificial Intelligence (ECAI'88) pp. 339-344, 1988.
Mélanie Ducoffe, Guillaume Povéda, Audrey Galametz, Ryma Boumazouza, Marion Cécile Martin, Julien Baris, Derk Daverschot, and Eugene O'Higgins. Surrogate neural networks local stability for aircraft predictive maintenance. In International Conference on Formal Methods for Industrial Critical Systems, pp. 258. Springer, 2024.
Thomas Fel, Lucas Hervier, David Vigouroux, Antonin Poche, Justin Plakoo, Remi Cadene, Math- ieu Chalvidal, Julien Colin, Thibaut Boissin, Louis Bethune, et al. Xplique: deep learning explainability toolbox. arXiv preprint arXiv:2206.044 04394,, 2022.
Thomas Fel, Melanie Ducoffe, David Vigouroux, Rémi Cadène, Mikaël Capelle, Claire Nicodème, and Thomas Serre. Don't lie to me! robust and efficient explainability with verified perturbation analysis. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recogni- tion (CVPR), pp. 16153-16163, June 2023.
X. Huang, Y. Izza, A. Ignatiev, and J. Marques-Silva. On Efficiently Explaining Graph-Based Clas- sifiers. Proc. 18th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR), 2021.
Xuanxiang Huang and Joao Marques-Silva, From robustness to explainability and back again. arXiv preprint arXiv:2306.0334 03048, 2023.
Xuanxiang Huang. Yacine Izza, Alexey Ignatiev, Martin Cooper, Nicholas Asher, and Joao Marques- Silva. Tractable explanations for d-dnnf classifiers. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 36, pp. 571--7788 2022.
Alexey Ignatiev. Towards trustable explainable ai. In International Joint Conference on Artificial Intelligence-Pacife Rim International Conference on Artificial Intelligence 2020, pp. 5154-5158. Association for the Advancement of Artificial Intelligence (AAAI), 2020.
Alexey Ignatiev and Joao Marques-Sitee Silva. Sat-based rigorous explanations for decision lists. In Inter- national Conference on Theory and Applications of Satisfiability Testing, pp. 251-269. Springer, 2021.
Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. Propositional abduction with implicit hitting sets. In ECAI 2016, pp. 1327-1335. IOS Press, 2016.
Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silve Abduction-baasee explanations for ma- chine learning models. In Proceedings of the AAAI Conference on Artificial Intelligence, vol- ume 33, pp. 1511-1519, 2019.
Alexey Ignatiev, Yacine Izza, Peter Stuckey, and Joao Marques-Sikee Silva. Using MaxSAT for Efficient Explanations of Tree Ensembles. In Proc. of the 36 th AAAI Conf. on Artificial Intelligence, pp- 3776-3785, 2022.
12

---

Published as a conference paper at ICLR 2026
Yacine Izza and Joao Marques-Siie Sarques-Silva. On explaining random forests with sat. In Zhi Hua Zhou (ed.), Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21, pp. 2584-2591. International Joint Conferences Artificial Intelligence Organization, 8 2021. URL https::tp..... : /doi. org /10 24963/496392 24s63/ijcciiii. jea .202. 356.
doi:
Main Track.
Yacine Izza, Alexey Ignatiev, and Joao Marques-Silva. On explaining decision trees. arXiv preprini arXiv:2010.11034 2020.
Yacine Izza, Xuanxiang Huang, Antonio Morgado, Jordi Planes, Alexey Ignatiev, and Joao Marques- Silva. Restrrcced Explanations: Theoretical Underpinnings Efficient Implementation. In Proceedings of the 2 2s International Conference Principles of Knowledge Representation and Reasoning, pp. 475-486, 2024. doi: 10.24966/kr.2024445. URL https: /ooi. .org/
10. L...4993/KK2 /rr//////// 2024/2202/44..
UIrich Junker. Quickxplain: Preferred explanations and relaxations for over-constrained problems. In Proceedings of the 19th national conference on Artifical intelligence, pp. 167-172, 2004.
Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International conference on computer aided verification, pp. 97-117. Springer, 2017.
Guy Katz, Derek A Huang, Duligur lbeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, al. The marabou framework for ver- ification and analysis of deep neural networks. In International conference on computer aided verification, pp. 443 452. Springer, 2019.
Emanuele La Malfa, Rhiannon Michelmore, Agnieszka M. Zhrzezny, Nicola Paoletti, and Marta Kwiatkowska. On guaranteed optimal robust explanations for nlp models. In Zhi-Hua Zhou (ed.), Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21, pp.
International Joint Conferences Artificial Intelligence Organization, 8 2021. doi: 00.24963/jecai2222///66 URL htttts:////att orq /10 23933/ /a/e6///jjaa. jjaai 2021 366. Main Track.
João Marques-Silva, Minimal unsatisfiability: Models, algorithms and applications (invited paper). In 40th IEEE International Symposium on Multiple-Valuue Valued Logic, ISMVL 2010, Barcelona, Spain, 26-28 May 2010, pp. 9-14. IEEE Computer Society, 2010. doi: 00.1109/5MVL..2000.11. URL
https: /oii org/10 1109 SMVLL 2010.11.
Joao Marques-Silva. Disproving xai myths with formal tichods-inition results. In 2023 27th Inter- national Conference on Engineering of Complex Computer Systems (ICECCS), pp. 12-21. IEEE, 2023a.
Joao Marques-Silva. Logic-based explainability in machine learning. In Reasoning Web. Causal- ity, Explanations and Declarative Knowledge: 18th International Summer School 2022, Berlin, Germany, September 27-30, 2022, Tutorial Lectures, pp. 24-104, Springer, 2023b.
Joao Marques-Silva, Thomas Gerspacher, Martin Cooper, Alexey Ignatiev, and Nina Narodytska. Explaining naive bayes and other linear classifiers with polynomial time and delay. Advances in Neural Information Processing Systems, 33:20590-20600. 2020.
Joao Marques-Sikye Thomas Gerspacher, Martin Cooper. Alexey Ignatiev, and Nina Narodytska. Explanations for monotonic classifiers. In International Conference on Machine Learning, pp- 7469-7479. PMLR, 2021.
Mathieu Semurier, Franck Mamalet, Alberto González-Sanz, Thibaut Boissin, Jean-Michel Loubes, and Eustasio Del Barrio. Achieving robustness in classification using optimal transport with hinge regularization. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, 2021.
Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian net- work classifiers. In Proceedings of the 27th International Joinr Conference on Artificial Intelli- gence, UCCAI'1, 18, pp. 5103-5111, AAAI Press, 2018. ISBN 9780999241127.
13

---

Published as a conference paper at ICLR 2026
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for cer- tifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL): 2019.
Johannes Stallkamp, Marc Schlipsing, Jan Salmen, and Christian Igel. Man vs. computer: Bench- marking machine learning algorithms for traffic sign recognition. Neural networks, 32:323-332, 2012.
Caterina Urban and Antoine Miné. A review of formal methods applied machine learn- ing. ArXiv, abs/2104.02466, 2021. URL
CorpusID:2330333
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Sekhar Jana, Cho-Jui Hsieh, and Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In Neural Information Processing Systems, 2021. URL httpt:///aap
semanticscholar.oomm
Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, et al. Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In Proc. 36th Int. Conf. on Computer Aided Verification (CAV), pp. 249-264, 2024a.
Min Wu, Haoze Wu, and Clark Barrett. Verix: towards verified explainability of deep neural net- works. Advances in Neural Information Processing Systems, 36:22247-22266 2023.
Min Wu, Xiaofu Li, Haoze Wu, and Clark W. Barrett. Better verified explanations with applications incorrectness and out-of-distribution detection. CoRR, 0tbp//249.030000 2024b. doi: 10.48550/ 04499.03000
ARXIV.2409.03061 030060 URL https: /tt::://d/o..../
10. 48550/
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsich. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33:1 124-11,,,,,, 2020.
LeCun Yann. Mnist handwritten digit database. ATT Labs., 2010.
Huan Zhang, Tsui-We Weng, Pin- Yu Chen. Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems, 31, 2018.
Zhe Zhao, Yedi Zhang. Guangke Chen, Fu Song, Taolue Chen, and Jiaxiang Liu. Cleverest: ac- celerating cegar- cegar-based neural network verification via adversarial attacks. In International Static Analysis Symposium, pp. 449-473, Springer, 2022.
14


Reviews:
[{"review_id": "cT2BpALUa3", "reviewer": "Reviewer_Y1Ta", "summary": "The paper introduces FAME (Formal Abstract Minimal Explanations), a scalable framework for generating abductive explanations in neural networks. FAME leverages abstract interpretation and dedicated perturbation domains to eliminate the need for traversal order in formal explanations. It also introduces a procedure for measuring the quality of these explanations by comparing them to true minimal explanations. The authors demonstrate that FAME consistently outperforms the state-of-the-art (VERIX+) in terms of explanation size and runtime, particularly for medium- and large-scale networks. This framework is designed to handle the scalability challenges of formal explainability methods for neural networks and is made publicly available for further research.", "questions": "Please see the weaknesses.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "1. The paper presents a novel approach to formal explanations, eliminating the traditional traversal order bottleneck. This is a significant step forward in making formal XAI methods scalable to large networks.\n\n2. The proposed FAME framework is sound, and the experiments demonstrate its potential to scale well with complex networks.\n\n3. The writing is generally clear, and the method is presented in an organized way. The diagrams and figures help illustrate key points effectively.", "weaknesses": "**Traversal Order Issue:** The paper claims to eliminate traversal relationships, but the algorithm still performs multiple rounds of feature selection, which can be considered a form of traversal. This method needs further clarification to truly eliminate traversal relationships.\n\n**Impact of Feature Order:** The paper underestimates the significant impact that the order of feature selection has on the results. A more thorough discussion and empirical validation are required. Specifically, when removing feature A, feature B may still play a role, and vice versa. This interdependency should be addressed.\n\n**Attack Boundaries:** The approach only provides a lower bound or instance-based gap for attack robustness, making it difficult to achieve a global worst-case upper bound. This limitation needs clearer discussion.\n\n**Greedy Method Guarantee:** The greedy approach used in the paper lacks an approximation guarantee, which limits its theoretical robustness. An approximation guarantee would strengthen the argument for its practicality.\n\n**Simplicity of Dataset:** The dataset used is relatively simple. Most explainability techniques are validated on more complex datasets like ImageNet. It would enhance the credibility of the method if it were tested on more challenging datasets.\n\n**Complexity Analysis:** The paper lacks a detailed analysis of the algorithm's complexity, especially concerning GPU acceleration and distributed verification. A more detailed discussion of these aspects would provide a clearer understanding of the scalability of the method.\n\n**Hyperparameter Sensitivity:** The paper does not sufficiently address the sensitivity of the results to hyperparameters. A more comprehensive analysis of this sensitivity would help understand the stability and robustness of the approach.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "EMJQg2Blqh", "reviewer": "Reviewer_BXZg", "summary": "Formal explainability paper that presents FAME, a method to generate *abductive* explanations for neural networks. Novelty is in the adoption of LiRPA bounds to discard irrelevant features and in not relying on ordered features, thus achieving faster results.", "questions": "- Could you clarify what is the proposed delta over LiRPA?\n- How can FAME support discrete features?\n- Is VERIX+ the only baseline you can compare against?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- Formally computing explanations with guarantees for neural networks is a critical and important research problem, with room for novel contribution.\n- The approach is described in coherent manner, and paper storytelling is linear.", "weaknesses": "- Coming from a different community, I found hard to familiarize with the jargon, as some key concepts are left without definition (e.g. abstract interpretation, LiRPA). They may be second nature for the authors, but gently introducing them would help clarify and broaden up the audience.\n- The paper could use some examples, to ease the understanding from a broader audience (e.g. when introducing the verification task, 99-102, or by providing additional examples properties to verify $P$ - other than adversarial robustness).\n- (minor): definition identifiers in the main corpus do not match (e.g. line 162, 219). Citation style not compliant with ICLR guidelines.\n- Evaluation covers only vision scenarios (MNIST, GTSRB) and does not cover tabular data (a critical use case for certified explanations).\n- Experimental results w.r.t baseline: neither explanation size or response time are dramatically smaller (i.e. better) than VERIX+.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "w4fmXNllLO", "reviewer": "Reviewer_Wn1a", "summary": "This paper introduces FAME, a new framework for computing formal abductive explanations for neural networks. The core of the method formulates 'batch freeing' as a multidimensional knapsack problem, which is then solved efficiently using a greedy heuristic. Experiments on MNIST and GTSRB models (both FC and CNN) demonstrate that FAME consistently outperforms the VERIX+ baseline.", "questions": "* Could the authors provide results on a more complex dataset (e.g., CIFAR-10) and a deeper architecture (e.g., a small ResNet) to more robustly demonstrate scalability?\n* What percentage of the total runtime does the \"optional VERIX+ refinement step\" account for, on average, across the reported experiments?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "* The paper shows a novel approach to breaking the 'sequential bottleneck' in formal XAI.\n* Using LiRPA-based abstract interpretation (which is GPU-accelerated), instead of CPU-bound solvers, is practical. This can speed up and improve scalability.\n* The formulation of batch freeing as a knapsack problem is a clever and effective", "weaknesses": "### 1. Data\nThe experiments are limited to MNIST and GTSRB. These are relatively small-scale and low-dimensional datasets. The paper's claim to \"scale to large neural networks\" is not fully substantiated by this evidence. The scalability of FAME on high-dimensional data (e.g., CIFAR-100 or ImageNet) is a major open question.\n\n### 2. Model\nSimilarly, the models used (small FC and CNNs) are not \"large-scale\" by modern standards (e.g., ResNets, Transformers). The quality of LiRPA bounds is known to degrade with network depth. The paper does not investigate how the \"gap\" between the abstract explanation and the true minimal explanation scales with model depth. If this gap becomes too large, the abstract-first approach may lose its advantage, as the final refinement step would become computationally dominant.\n\n\n### 3. Metric\nThe \"distance to minimality\" (Section 6) is a good concept, but the paper does not fully explore the failure modes. The paper notes in Section 4.2 that if bounds are too loose (e.g., for complex models or large epsilons), the abstract method may fail to free any features. This \"failure mode\" is not empirically characterized.\n\n### Minor\n* format: It seems the paper format is not the ICLR format (e.g., references)\n* Suggest improving clarity and making the explanation less dense for readers to get the idea. Also, I can’t get the idea from Figure 1 at first; maybe improving this can be helpful for the readers.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "PFq276FBPo", "reviewer": "Reviewer_CJQr", "summary": "This paper proposes FAME (Formal Abstract Minimal Explanations), a framework for generating formally verified minimal explanations for neural network predictions. The method combines abstract interpretation with LiRPA (Linear Relaxation based Perturbation Analysis) to efficiently identify the minimal subset of input features responsible for a model’s decision. FAME removes the traversal-order dependency in prior formal explanation methods through an abstraction-based parallel mechanism that eliminates multiple irrelevant features simultaneously. Experiments on MNIST and GTSRB show that FAME produces more compact explanations and up to 25× faster runtime compared to VERIX+, supporting its theoretical claims.", "questions": "1. I do not fully understand the validation setup described in Section 7.2, where the authors claim that FAME achieves formally minimal explanations but provide no direct comparison against exhaustive search or exact verification results. What metric was used to assess proximity to the true minimal set, and how do the authors justify that this indirect evaluation sufficiently demonstrates minimality?\n2. The paper reports in Section 6 that FAME relies on LiRPA-derived abstract bounds to identify irrelevant features. However, recent work has shown that local linear relaxations may miss globally relevant feature interactions (see Lu et al., 2024, ICML — EiG-Search: Generating Edge-Induced Subgraphs for GNN Explanation in Linear Time). Could such limitations affect the completeness of FAME’s explanations, and have the authors considered adaptive or hierarchical abstraction domains to mitigate this risk?", "limitations": "", "rating": 4, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The paper introduces a novel and theoretically grounded framework, FAME (Formal Abstract Minimal Explanations), that advances formal explainable AI by combining abstract interpretation with LiRPA for efficient and provably minimal explanations.\n2. It effectively removes the traversal-order dependency that limits prior formal XAI methods and achieves substantial improvements in explanation compactness and runtime on benchmark datasets.", "weaknesses": "1. The paper introduces formal minimal explanations as a novel interpretability construct, yet the theoretical operationalization of “interpretability” remains vague. The framework lacks a precise articulation of how its formal minimality relates to established interpretive criteria, such as faithfulness or epistemic transparency, which weakens the clarity of its conceptual contribution.\n2. The evaluation is limited to MNIST and GTSRB, which are too simple to validate FAME’s scalability or general effectiveness. More representative benchmarks such as CIFAR-10 for visual interpretability or COMPAS for tabular reasoning would better demonstrate the framework’s robustness across domains.\n3. Although the paper asserts improved explanation quality, the experiments report only efficiency-related metrics (runtime and explanation size). Without fidelity- or stability-based evaluation, the claimed enhancement in explanation quality is not empirically supported.\n4. The iterative optimization in Abstract Batch Freeing is described as a key component of the framework, but its contribution has not been empirically isolated. No ablation or comparative results are provided to verify whether this step improves efficiency or explanation compactness. Without such analysis, the practical impact of this mechanism remains speculative.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)