Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Authors: Shahaf Bassan
Yizhak Yisrael Elboher
Tobias Ladner
Matthias Althoff
Guy Katz
Venue: ICML 2025 poster (2025)
Keywords: explainability
XAI
explainable AI
Primary area: social_aspects->accountability_transparency_and_interpretability

Abstract: Despite significant advancements in post-hoc explainability techniques for neural networks, 
many current methods rely on heuristics and do not provide formally provable guarantees over the explanations provided. 
Recent work has shown that it is possible to obtain explanations with formal guarantees by identifying subsets of input features 
that are sufficient to determine that predictions remain unchanged
using neural network verification techniques.
Despite the appeal of these explanations, their computation faces significant scalability challenges. 
In this work, we address this gap by proposing a novel abstraction-refinement technique for efficiently computing provably sufficient explanations of neural network predictions. 
Our method *abstracts* the original large neural network by constructing a substantially reduced network, 
where a sufficient explanation of the reduced network is also *provably sufficient* for the original network, 
hence significantly speeding up the verification process. 
If the explanation is insufficient on the reduced network, we iteratively *refine* the network size by gradually increasing it until convergence.
Our experiments demonstrate that our approach enhances the efficiency of obtaining provably sufficient explanations for neural network predictions while additionally providing a fine-grained interpretation of the network's predictions across different abstraction levels.

Explaining, Fast and Slow:
Abstraction and Refinement of Provable Explanations
Shahaf Bassan" I
Yizhak Yisrael Elboher"
1
Tobias Ladner"
2 Matthias 2 Guy Katz
Abstract
methods have been proposed to explain neural network predictions. Classic additive feature attributions such as LIME (Ribeiro et al., 2016), SHAP (Lundberg & Lee, 2017), and integrated gradients (Sundararajan et al., 2017) assume that neural networks exhibit near-linear behavior a lo- cal region around the interpreted instance. Following these works, methods like Anchors (Ribeiro et al., 2018) and SIS (Carter et al., 2019) aim to compute subset of input features that is (nearly) sufficient to determine the predic- tion. We refer to this subset of features as an explanation of the prediction. A common assumption in the literature is that a smaller explanation provides better interpretation, thus, the minimality of the explanation is also a desired property (Ignatiev al., 2019; Carter et al., 2019; Darwiche & Hirth, 2020; Ribeiro et al., 2018; 8; Barceló et al., 2020).
Despite significant advancements in post-hoc ex- plainability techniques for neural networks, many current methods rely on heuristies and do not pro- vide formally provable guarantees over the expla- nations provided. Recent work has shown that it is possible to obtain explanations with formal guarantees by identifying subsets of input features that are sufficient to determine that predictions re- main unchanged using neural network verification techniques. Despite the appeal of these explana- tions, their computation faces significant scala- bility challenges. In this work, we address this gap by proposing a novel technique for efficiently computing provably suf- ficient explanations of neural network predictions. Our method abstracts the original large neural network by constructing a substantially reduced network, where sufficient explanation of the re- duced network is also provably sufficient for the original network, hence significantly speeding up the verification process. If the explanation is in- sufficient on the reduced network, we iteratively refine the network size by gradually increasing it until convergence. Our experiments demonstrate that our approach enhances the efficiency of ob- taining provably sufficient explanations for neural network predictions while additionally providing fine-graines interpretation of the network's 's pre- dictions across different abstraction levels.
Methods like Anchors and SIS rely on probabilistic sam- pling of the input space and lack formally provable guar- antees for the sufficiency of the subsets they identify. In contrast, recent approaches have demonstrated that incorpo- rating neural network verification tools can produce expla- nations that are provably certified sufficient (Wu et al., 2023; Bassan & Katz, 2023; La Malfa et al., 2021; Izza et al., 2024). This makes such explanations more suitable for safety-critical domains where formally certifying the explanation is vital (Marques-Sinl Silva & Ignatiev, 2022).
Although such explanations are compelling, producing them is computationally expensive for large neural net- works (Barceló et al., 2020) they are obtained by solving neural network verification queries, which were shown to be NP-complete (Katz et al., 2017; Sälzer & Lange, 2021). While there have been rapid advances in the scalability of neural network verification techniques in recent years (Wang et al., 2021b; Brix et al., 2023), scalability remains major challenge. Furthermore, providing minimal sufficient expla- nations requires invoking multiple verification queries: for example, methods suggested by previous research (Bassan & Katz, 2023; Wu et al., 2023) dispatch linear number of queries relative to the input dimension, making these tasks particularly difficult for high-dimensional input spaces.
1. Introduction
Despite the widespread use of deep neural networks, they remain uninterpretable black boxes to humans. Various
'Equal contribution 'Hebrew University of Jerusalem "Technical University of Munich. Correspondence to: <sha- haf bassan @ mail. wwi..muji.a...... huji.ac.ilz, <yizhak.elbohere huji.a..j. etobias.Jadnerre @ tem.de>.
Our Contributions. In this work, we propose a novel algorithm that significantly enhances the efficiency of gen- erating provably sufficient explanations for neural networks.
Proceedings of the 42nd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Network p
10%
20%
30%
40%
50%
60%
70%
90%
100%
(n) Original image
(b) S 10%
(0) E 30%
(d) P S 50%
(e) S 80%
(1) Original network
Explamation size increases
Network size and computation time incresses
Figure 1: Demonstration of an abstraction-basees explanation process. As the size of the abstract network increases, the size of the explanation (uncolored pixels) decreases. Notably, the majority of the explanation can be derived using only a small percentage of the network (b)-(e), reducing the time required to compute the explanation and offering more insight compared to using only the original network (f). Further visualizations are provided Appendix
Our algorithm is based on an abstraction refinement tech- nique (Clarke al., 2000; Wang al., 2006; Flanagan & Qadeer, 2002), which is widely used to improve the scalabil- ity of formal verification and model checking. In abstraction- refinement, a complex model with many states is efficiently optimized through two steps: (i) abstraction, which sim- plifies the model by grouping states, and (ii) refinement, which increases the precision of the abstraction to better approximate the original model.
explanations will gradually decrease until finally converging to a minimal explanation for some reduced network, which is also provably minimal for the original neural network. An illustration of this entire process is shown in Fig. 1.
We evaluate our algorithm on various benchmarks and show that significantly outperforms existing verification based methods by producing much smaller explanations and doing so substantially more efficiently. Additionally, we com- pare our results to heuristic-brie based approaches and show that these methods do not provide sufficient explanations in most cases, whereas the explanations of our approach are guaranteed to be sufficient. An additional advantage of our method is that it enables the progressive convergence the refined explanations to the final explanation, as illustrated in Fig. 1. This approach allows practitioners to observe minimal subsets across various reduced networks, offering fine- gree-graied interpretation of the model's prediction. Ad- ditionally, it provides the possibility of halting the process once the explanation meets some desired criteria.
In the context of explainability, we propose an algorithm that constructs an abstract neural network - a substantially reduced model compared to the original. This reduction is achieved by merging neurons within each layer that exhibit similar behavior. The key component of this approach is to design the reduction such that a sufficient explanation for the abstract network is also provably sufficient for the original network. Hence, we define an explanation for the abstract neural network as an abstract explanation. Verifying the sufficiency of explanations for an abstract neural network is much more efficient than for the original model due to its reduced dimensionality. However, if a subset is found to be insufficient for the abstract network, its sufficiency for the original model is undetermined. Consequently, while suffi- cient explanations for the abstract network will be sufficient for the original network, minimal sufficient explanations for the abstract network, though sufficient, may not be minimal for the original network.
Besides these practical aspects, we view this work as a novel proof-of-concept for using cestraction-refinmmnn based techniques in explainability, obtaining formally prov- able explanations over abstract neural networks, which allow significantly more efficient verification and fine-grained in- terpretation over abstracted and refined networks. We hence consider this work a significant step in exploring explana- tions with formal guarantees for neural networks.
To address this issue, we incorporate a refinement compo- techniques: We
nent as typical in construct an intermediate abstract network, which is slightly larger than the initial abstract network but still significantly smaller than the original. The explanations computed for this refined network are still provably sufficient for the orig- inal network and are also guaranteed to be a subset of the explanation from the initial abstract network. Hence, this phase produces a refined explanation based on the refined network. After several refinement steps, the sizes of the neu- ral networks will gradually increase while the sizes of the
2. Preliminaries
2.1. Notation
We denote scalars with lower-case letters, vectors with bold lower-case letters, matrices with bold upper-case letters, and sets in calligraphic font. The i-th dimension of a vector x is denoted by x Given some n E N, let [n] == {1,...,,1] n...
Given a set C R" and a function f: R" + R we define f(S) = (f(s) E
2

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
2.2. Neural Network Verification
Definition 1 (Sufficient Explanation). Given a neural net- work f, an input E RR, a perturbation radius Ep E R, and subset S S [n], we say that S is a sufficient explanation concerning the query (f. x, S. cp) on an f--norm ball B of radius Ep E RR+ around x iff it holds that:
We specify a generic neural network classifier architecture that can utilize any element-wise nonlinear activation func- tion. For input x E I", the neural network classifier is denoted as f: I - IR. Numerous tools have been pro- posed for formally verifying properties of neural networks, with adversarial robustness being the most frequently ex- amined property (Brix et al., 2023). The neural network verification query can be formalized as follows:
Vi E B (x): jarg max ((xs; = arg max (x)
j with BB = (8 E RD ||- واا s.) -
We define suff(,, x, = iff S constitutes sufficient explanation with respect to the query (f, x, S, Cp), and suff(f, x, S, Cp) = 0 otherwise.
Neural Network Verification (Problem Statement):
Input: A neural network f, such y fxx), with an in-
put specification t'in (x). and an unsafe output specification Wy)
Def. can be formulated as a neural network verification query. This method has been proposed by prior studies, which employed these techniques to validate the sufficiency of specific subsets (Wu et al., 2023; Bassan & Katz, 2023; La Malfa et al., 2021; Izza et al., 2024).
Output: No, if there exists some x E R² such that vhin (x)
and (y both hold, and Yes otherwise.
There exist many off-the-shelf neural network verifiers (Brix et al., 2023). If the input specifications (i (x), output spec- ifications (v), and model f are piecewise- -inear (e.g., f uses ReLU activations), this task can be solved exactly (Katz et al., 2017). However, the problem is often relaxed for efficiency, and the output is enclosed by bounding all ap- proximation errors (see Sec. 6).
Minimal Explanations. Clearly, if the subset S is cho- sen as the entire input set, i.e., S == [n], it is a sufficient explanation. However, a common view the literature sug- gests that smaller subsets are more meaningful than larger ones (Ribeiro et al., 2018; Carter et al., 2019; Barceló et al., 2020; Ignatiev et al., 2019). Therefore, there is focus on identifying subsets that not only are sufficient but also meet a criterion for minimality:
2.3. Formally Provable Minimal Sufficient Explanations
Definition 2 (Minimal Sufficient Explanation), Given a neural network f. an imput x E IR",, and a subset S S [m], we say that S is a minimal sufficient explanation concern- ing the query (f, x, S, cp) on Bş" of radius Ep iff S is sufficient explanation, and for any i E S, S \ {i} is not sufficient explanation. We define min-suff(f, x, S, (p) = if S satisfies both sufficiency and minimality concerning (f, x, S, Ep), and min-suff(f, x, S, Ep) = 0 otherwise.
In this study, we concentrate on local post-hoc explanations for neural network classifiers. Specifically, for a neural net- work classifier f: IR" R and given local input E R predicting class == arg max, (x) E [c], our objective is to explain why/ f classified x as class t. For regression tasks, a similar formulation can be found by limiting the deviation by some threshold d E TR., (Appendix D).
Sufficient Explanations. A common method for interpret- ing the decisions of classifiers involves identifying subsets of input features S C [m] such that fixing these features to their specific values guarantees the prediction remains unchanged. Specifically, these techmiques guarantee that the classification result remains consistent across any poten- tial assignment within the complementary set S := [n] \ S, thereby allowing for the formal verification of the explana- tions' soundness. While in the classic setting features in the complementary set S are allowed to take on any possi- ble feature values (Ignatiev et al., 2019; Darwiche & Hirth, 2020; Bassan & Katz, 2023), a more feasible and general- izable version restricts the possible assignments for S to a bounded re-region (Wu et al., 2023; La Malfa et al., 2021; Izza et al., 2024). We use (xg; E R" to denote an as- signment where the features of S are set to the values of the
Minimal sufficient explanations can also be determined us- ing neural network verifiers. Unlike simply verifying the sufficiency of specific subset, this process requires execut- ing multiple verification queries to ensure the minimality of the subset. Alg. I outlines such a procedure (similar methods are discussed in (Ignatiev et al., 2019; Wu et al., 2023; Bassan & Katz, 2023)). The algorithm begins with S encompassing the entire feature set [m] and iteratively tries to exclude a feature i from S, each time checking whether S (i} remains sufficient. If S \ (i) is still sufficient, fea- ture i is removed; otherwise, it is retained in the explanation. This process is repeated until a minimal subset is obtained.
3. From Abstract Neural Networks to Abstract Explanations
vector x E R² and the features of 8 are set to the values of another vector ă E R= within the rp-region. Formally, we define a sufficient explanation S as follows:
A primary challenge in obtaining minimal sufficient explana- tions in neural networks is the high computational complex- ity involved, as verifying the sufficiency of subset through
3

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Algorithm 1 Minimal Explanation Search
Neuron-Merging- Abstraction. Various strategies can be employed to abstract neural network to reduce its size. In this work, we abstract neural networks by merging neurons that exhibit similar behavior within the network for some bounded input set. For instance, numerous sigmoid neurons may become fully saturated, producing outputs close to 1. Hence, we can merge these saturated neurons and establish corresponding error bounds for the given in- put set. This can be realized without large computational overhead to desired reduction rate P [0, 1] such that the overall verification time, including abstraction, mainly depends on the remaining number of neurons. By using the construction suggested by (Ladner & Althoff, 2023), where merged neurons are replaced by single one and the ap- proximation error is bounded with set propagation, we can prove the important sufficiency implication property. We give details about the precise construction in Appendix A. For convenience, we define p as the original network.
Input: Neural network f: I= + R. input x E IK", pertur- bation radius Cp E RR
1: S [n]] [n]
2: for each feature i E [n] do D suff(S, x, S, ep) holds
3: if Sffff(f, x, S {i), sp) then S {i}
4:
5: end if
6: end for
7:
return S
min holds
a neural network verification query is NP-Complete (Katz et al., 2017), making especially difficult for larger net- works (Brix et al., 2023). Obtaining a minimal subset also requires linear number of verification queries relative to the input size (Alg. 1), making the process computationally intensive for large inputs. One potential solution is to re- place the original neural network f with a much smaller, abstract neural network f', and then run verification queries on f' instead of f. However, a key challenge here is to ensure that sufficient explanation for I' is also a sufficient explanation for f. Although similar ideas of such abstrac- tion techniques have been applied to improve the efficiency of adversarial robustness verification (Elboher et al., 2020; Cohen et al., 2023; Ladner& & Althoff, 2023; Liu et al., 2024), to our knowledge, we are the first to use an approach of this form to obtain provable explanations for neural networks.
We are now ready to establish the following claim on suffi- cient explanations for the query (f', x, S, cp):
Proposition 1 (Explanation Under Abstraction). Given a neural network f, an input x, a perturbation radius Ep and a subset S C [n], let f' be an abstract network constructed by neuron merging concerning the query (f, x, S, e,)). Then, it holds that:
suff( Cuff(f', x, Ep) = suff( x, ep).
Abstract Neural Networks. When abstracting neural net- work, rather than using a traditional network f: R" + IR, it is common to employ an abstract neural network f' that outputs a set that encloses the actual output of f (Ladner & Althoff, 2023; Prabhakar& & Rahimi Afzal, 2019; Boudard- ara et al., 2022). This approach facilitates a more flexible propagation through the neural network, capturing the er- due the abstraction. More formally, we define the domain of our abstract network f': R + 2(89), where 2x*)) denotes the power set of RRC In the simplest case, this means that f' outputs c-dimensional interval rather than a c-dimensional vector.
Proof. The proof can be found in Appendix A.2.
However, while a sufficient explanation S for the query (f', S, 6p) is also provably sufficient for the query (f, x, S, sp). if S is insufficient for (J', x, S, <p), it does not necessarily mean it is insufficient for (f. x, S, ep)). To more clearly highlight the explanation S within the context of the abstract network f', we introduce an intermediate type of explanation, termed abstract sufficient explanation. This is a provably sufficient explanation for (f', x, S, ep) and, by extension (Prop. 1), also provably sufficient for (S, x, S, 6p)):
Definition 4 (Abstract Sufficient Explanation). We define sufficient explanation S concerning the query (f', x,, S, ep) as an abstract sufficient explanation concerning the query (J, x, S, pp)
Since our abstract network I' now outputs a set, we must de- fine a sufficient explanation for an abstract network. Specif- ically, we define a sufficient explanation for f' and target class è [c] as subset S C [r)] such that when the features in S are fixed to their values in x, the lower bound for the target class t consistently exceeds the upper bound of all other classes j # t:
Running example. We demonstrate these concepts using toy ReLU network with positive weights and biases in Fig. 2, allowing for exact bounds via simplified interval- bound propagation. While intentionally simplified, the ex- ample serves to illustrate the procedure:
Definition (Sufficient Explanation for Abstract Network). S S [n] is a sufficient explanation of an abstract network f' concerning the query (f", x, S, (p) iff # E [c]:
Fig. 2a shows the network and the interpreted input (0, 1, 1). Biases are 0 except for the lower output neuron, which has bias of 10. Propagating (0, 1, 1) gives outputs of 15 (class
Vi E B5 (x): [mini( (xs; 2 max (xs: with (x5(()) == { E R²" ||x 1|1 S 5
4

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
(a) Original network
(b.1) Original network with sufficient explanation of size 2
(b.2) Abstract network with sufficient explanation of size 2
Ingut
Hidden
Output
Input
Hidden
Output
Input
Hidden
Output
Maraed ncaness
[
10. 1]
[5.6
[0.1]
[1.5]
[1.. 22)
[12. 28)
[0
[1]
[0.8
[1]
[3,
[46]
[46. 55]
[31. 8o]
[6]
[1]
16.
[1]
10
Figure 2: Running example. a) Original network with winner class 2 (green). b) Sufficient explanations (yellow) of original
network (b.1) and abstract network (b.2).
1) and 46 (class 2). predicting class? 2. Fig, 2b.1 shows explanation that includes features 2 and 3 (yellow): We fix these features to their original values of 1, restricting their domains to [1, I]. Feature 1 is not in the explanation and hence is allowed to vary freely within [o, 1]. We then compute bounds via interval propagation. For example, the top hidden neuron gets an input range of [3, 5), from lower bound of 0 x 2 1
previously constructed abstract network f by splitting some of the merged neurons, resulting in larger reduction rate p" > p'. The refined abstract network f" is still substan- tially smaller than the original network f but slightly larger than f', allowing us to generate a smaller explanation: Proposition 2 (Refined Abstract Network). Given neural network f. an input x, perturbation radius Ep E IR.,, subset S S [m], and an abstract network f' with reduction rate p' E [0, 11, we can construct a refined abstract network f" from f. with reduction rate p" > >p', p'. which holds:
+ 1 = 3 and upper bound of 1 x 2 x 2 + 1 x 1- = 5. These bounds are propagated to the output layer using the weights. For example, the top output neuron's range is [15, 22). calculated as: lower bound is 3 x 2 + 3 x 1 + 6 1 = 15 and upper bound is 5x1++x1++111+ = 22. Overall, the output range for class 2 ([46, 55) strictly above that of class 1 ([15, 22)). Thus, fixing features 2 and 3 is sufficient guarantee that class 2 remains the predicted class- making it valid explanation.
Vi E B (x): ((xs; E J (x): C ('(xx;:)))
Proof. The proof can be found in Appendix A.3.
Considering refined abstract network s" in relation to and f' with p" > p', the following property holds for the explanations generated for these networks:
In Fig. 2b.2, we show how three hidden neurons are merged by first unifying their intervals and then computing a weighted sum. While this process is not sound in general, we simplify the process here for clarity (See Appendix B.1 for the full example). For instance, the top neuron yields the interval [12, 28] from 3- (2 + 1 1) and 7- (2 + 1 1). As this lies strictly below [31, 59], features 2 and form abstract explanation per Def. 3.
Proposition 3 (Intermediate Sufficient Explanation). Let there be a neural network f, an abstract network f', and refined neural network s" Then, it holds that:
suff( x, S, Ep) = suff(f", x, S, Ep) and suff( x, S, cp) = suff( x, S, (p).
Proof. The proof can be found in Appendix A.4.
Although we now have a framework that enables us to obtain explanations S for a neural network f more effi- ciently - since queries on the smaller abstract network are faster- there is still an issue. The explanation S generated from the abstract network f' might not be minimal for the original network f, even if it is minimal with respect to (f', x, S, <p). In order to guarantee the minimality of the explanation in the original network, we apply refinement.
We observe that any sufficient explanation S for the query (f" x, S, (p) is also sufficient for the query (f, x, S, cp) but might not be for (f",, x, S, <p) (Prop. 3). Thus, the inter- mediate explanation of a refined network is subset of the explanation of the abstract network. Consequently, we de- fine, in manner akin to abstract sufficient explanations, an intermediate category termed refined sufficient explanations: Definition (Refined Sufficient Explanation). We define a sufficient explanation S concerning (J" x, S, <p) as a refined sufficient explanation, where the refined abstract network f" is constructed with respect to (f. f', x, S, cp) for neural network f. and an abstract network J".
4. From Refining Neural Networks to Refining Explanations
To produce an explanation that is both sufficient and mini- mal, we apply an iterative refinement process. In each step, we construct a slightly larger refined network f" than the
The observation that a sufficient explanation for (f", x, S, {p) is subset of the one for (s', x, S, cp)
5

---

approach to Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
suggests the following characteristic about the minimality of sufficient explanations:
necessarily provably minimal (Prop. 4). If we cannot be certain whether subset S is sufficient for the abstract net- work (lines 7 to 15), we check whether feature i is indeed not in the explanation by extracting a counterexample and checking its output in the original network (lines 8 to 9). If the counterexample is spurious due to the abstraction in f', we refine the abstract neural network and thus produce a slightly larger network f" (line 12). Using this refined net- work f we acquire refined sufficient explanation relative to it, which allows us to remove additional features from the explanation as the abstraction error is smaller (Prop. 2). As we remove additional features from the explanation, the verification query to test whether the current subset is a sufficient explanation becomes harder as additional features can be perturbed. Thus, network in line 3 to level for which the verification query was still successful, i.c., use the reduction rate of f" This process continues, with each iteration slightly enlarging the abstract network through refinement and consequently reducing the size of S.
Proposition 4 (Intermediate Minimal Sufficient Explana- tion). Let there be neural network f. an abstract net- work f'. and refined neural network fr. Then, if S is a sufficient explanation concerning J. J", and f", it holds that:
min-suff(J, x, S, Ep) = min-suff([ (S"; X, S, tp) and min-suff(f" (f" x. S, cp) = min-suff(f'. x, S₁ cp).
Proof. The proof can be found in Appendix A.5.
We note that the implication chain in Prop. is in reverse order compared the implication chain in Prop. Intu- itively, refining the abstract network I' to f" incremenallly produces larger neural networks, which in turn generates progressively smaller explanations, until ultimately converg- ing to minimal explanation for some refined network as it converges to the original network. We harness this iterative process and propose an produce such minimal subsets in Alg. 2.
sensible to only abstract the
Proposition 5 (Greedy Minimal Sufficient Explanation
Search). Alg. 2 produces provably sufficient and minimal explanation S concerning the query {J, x, S, Ep), which converges to the same explanation as obtained by Alg. 1.
Algorithm 2 Minimal Abstract Explanation Search
Input: Neural network f: R" - RR input E " target t arg max, (1) [c], perturbation radius cp E R 1: Init S + [m], [n]
Proof. The proof can be found in Appendix A.6.
While Alg. 2 converges to the same explanation S as Alg. 1, it operates on smaller networks and thus returns smaller explanation if timeout is applied. In addition, one obtains a fine-grained interpretation of the network's 's prediction across different abstraction levels (Fig. 1).
2: for each feature i E F do
P suff(f, x, S, 6p) holds f' + Abstract f w.r.t suff(f, x, S (i), cp)
3:
4:
do
5:
if sufff(ff' .x, (i], ep) then
Def. 3 > Feature i is not in minimal explanation
6:
S S {i]; break
Complexity. The runtime of Algorithm 2 is bounded by 0( + E) max,), where n is the number of features, & the number of refinement queries, and max; the maximum time required to certify single query. A higher value of & cor- responds to more fine-grat fine-grained refinement process, which typically reduces max, by allowing more features to be handled through coarser abstractions. Conversely, smaller values of & imply fewer refinement steps and thus longer certification queries - for instance, { = 1 corresponds to a single verification query over the full, unabstracted network.
7:
else
8:
x + Obtain counterexample
w.r.t suff(f' suff(f f
x, S\ {i)), cp)
9:
if arg max, (x) * then
D Feature must be in explanation F+F \ij; break
10:
11:
else
> Abstraction too coarse
12:
8" - RReine f' f f"
> Prop. 2 b Update abstract network
13:
14:
end if
15:
end if
Running example (cont.). We continue our rumning ex- ample from Fig. 2 in Fig. 3: Fig. 3c. show that feature 3 alone is also an explanation. While it is a sufficient ex- planation for the original network, it is not sufficient for the abstract network (Fig. 3c.2), since [4, 28] and [17,59] overlap violating Def. 3. This indicates that although every abstract explanation is valid for the original network, the reverse is not necessarily true. Consequently, minimal explanations for the abstract network, while sufficient, may not remain minimal when applied to the original network.
16:
while true
> Repeat with refined network
17:
end for
18:
return S
> min-suff(f, S, 6p) holds
The algorithm starts with coarse abstract network f' and derives an abstract sufficient explanation S by progressively removing features from S, akin to the method described in Alg. 1. All following line numbers are with respect to Alg. 2. While the abstract sufficient explanation is prov- ably sufficient for the original network (Prop. 3), it is not
Fig. 3d shows refinement merging only the first two neu-
6

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
(c.1) Original network with (c.2) Abstract network with (d.1) Original network with sufficient explanation of size 1
(d.2) Refined network with sufficient explanation of size 1
sufficient explanation of size
insufficient explanation of size
Iidiee
Oupua
Bapat
Hidles
Ougut
Tapur
Hillco
Ouper
Eapat
HRAles
Oxiit
0.
0.
18 23
|4.28
18 23)
[1
8.28
M.44
[1.7]
14F 58
[P. 30
[5
[ST. .6]
H
14
12
Figure 3: Running example (cont.). c) Minimal sufficient explanation for the original network (c.1) which is insufficient for the abstract network (c.2). d) Refining the abstract network results in sufficent explanation.
rons, yielding one merged neuron for them and another for the third. The output interval [37, 55] remains strictly above [8, 22]. confirming that fixing only feature 3 is a sufficient explanation for both the refined and original network.
Table 1:
Mean explanation size with a timeout of 100s, 10 and 10ts for MNIST, CIFAR-10, and GTSRB, respectively.
Explanation size CIFAR-10
Method
MNIST
GTSRB
5. Experimental Results
Ours
204.41129.2
308.2 408.2.123666
230.6 6.234.33
Standard
408.71336.6
448.71138.4
502.41101.7
Experimental Setup. We implemented the algorithms using CORA (Althoff, 2015) as the backend neural net- work verifier. We performed our experiments on three im- age classification benchmarks: (a) MNIST (LeCun, 1998), (b) CIFAR-10 (Krizhevsky& & Hinton, 2009), and (c) GT- SRB (Stallkamp et al., 2012). Comprehensive details about the models and their training are provided in Appendix B, and additional experiments, ablation studies, and extensions to other domains are provided in Appendix C and D.
= 10%
507.3+141.3
850.6+288.9
502.4=101.7
20%
420.6:1149.4
806.4157.4
704.6
P = 30%
340.0:115.00
687.1+130.8
605.0=203.1
P 50%
285.5+-98.0
316.3+22994
392.6-210.1
= 70%
325.6:64.5
311.5+233.0
292.6=225.2
P 90%
372.7+46.8
310.6+233.1
333.7=188.4
5.2. Explanations at Different Abstraction Levels
5.1. Comparison to Standard Verification-Base Explanations
Besides improving computation time and reducing explana- tion size, the Dbstraction-refinemmen refinement method allows users to observe the progressive decrease in explanation size at each abstraction level. Although networks with significant re- ductions initially provide larger explanations, refining these networks obtains explanations of decreasing size. These ex- planations at different abstraction levels may provide users with deeper insights and transparency into the prediction mechanism. Furthermore, it offers the flexibility to halt the process when the explanation is provably sufficient, even if not provably minimal. This fine tie-ggrinedd process is illus- trated in Fig. 5, where small explanations can be obtained with low reduction rates (p s 50% of the neurons).
In our initial experiment, we aimed to evaluate the abstraction-reffinmmen method proposed in Alg. 2 against the traditional approach described in Alg. for deriving provably sufficient explanations for neural networks, as implemented in previous studies (see (Wu et al., 2023; Bassan & Katz, 2023; La Malfa et al., 2021)). Complete details about the implementation of the refinement process are available in Appendix B. We assessed the effectiveness of both approaches using the two most prevalent metrics for evaluating sufficient explanations, as documented in (Wu et al., 2023; Ignatiev et al., 2019; Bassan & Katz, 2023): (i) the size of the explanation, with smaller sizes indicating higher meaningfulness, and (ii) the computation time.
5.3. Effect of Reduction Rates
Fig. 4 shows the explanation size over time for each bench- approach significantly outperforms the standard greedy method in computation time (-41% % for MNIST, -36% for CIFAR-10, -56% for GTSRB). We also implemented a timeout for each dataset and assessed the explanation size for each method under the timeout. These results are presented in Tab. 1 and demonstrate the substantial improvements in explanation size achieved with our ibbstraction-rffiemmen approach.
For a more detailed analysis of our findings, we present addi- tional results on the computation of explanations at varying reduction rates within our abstraction process. In Fig. 6, we illustrate the percentage of processed features verified to be included or excluded from the explanation per reduc- tion rate for MNIST, CIFAR-IO, and GTSRB. These results highlight that the majority of the explanation processing occurs at coarser abstractions, i.c., smaller network sizes p. resulting in improved computation time.
mark. We observed that the Dostractiio-rrfinemnn
7

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Abstractercfine (ours)
Original network
Timmouu
1,000
1,000
600
Explanation
600
600
400
400
400
200
1,000
2,000
10,000
20,000
Cumulattive time [s] MINST
Cumulative CIFAR-10
Cumulative [s]
GTSRB
Figure 4: The explanation size over cumulative time for MNIST, CIFARIO, and GTSRB, throughout the entire abstraction- refinement algorithm, or using the standard verification algorithm the original network. The standard deviation is shown shaded region.
Network size
10%
20%
30%
10%
50%
60%
70%
80%
90%
100%
S
100
Figure Examples of explanations at varying reduction rates for MNIST, CIFAR- 10, and GTSRB.
Abstract+relinee (ours)
Original network
10%
20%
30%
40%
50%
60%
70%
80%
Time per feamue [s]
40
0.3
0.2
20
0.1
200
400
600
200
400
600
800
1,000
200
400
600
800
1,000
Nr. of processed features MNIST
Nr. processed features
Nr. of processed fentures
CIFAR-10
(c) GTSRR
Figure 6: The percentage of processed features either included excluded from the explanation- over cumulative time, segmented reduction rate, throughout the abstraction-refiiemmnn algorithm, using the standard verification algorithm on the original network.
Table 2: Comparison with heuristic-based approaches, measuring sufficiency and average computation time over 100 images. Heuristic methods are faster but lack sufficiency, while our method consistently provides sufficient explanations (Prop. 5).
MNIST
CIFAR-10
GTSRB
Method
Suff.
Time
Suff.
Time
Suff.
Time
Anchors (Ribeiro al., 2018)
25%
0.56s
3%
1.17s
17%
0.14s
SIS (Carter al., 2019)
22%
322.72s
0%
553.92s
6%
95.13s
Original network
100%
207.80s
100%
1, 838.38.
100%
23, 504s
Abstract+refine (ours)
100%
121.95s
100%
1, 180.5s
100%
10, 235s
8

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
5.4. Comparison to Heuristic-Based Approaches
et al., 2020; 2022; Ladner & Althoff, 2023; Liu et al., 2024; Siddiqui et al., 2024). However, the best of our knowl- edge, our work is the first to use an abstraction-recinmmmnt technique to reduce neural network sizes for obtaining prov- able explanations of neural network predictions. Lastly, while similar ideas of model pruning leveraging probabilis- tic or uncertainty concepts have improved scalability in feature attribution generation (e.g., (Ancona al., 2019)), our non-probabilistic method offers stronger guarantees on continuous domains. Additionally, our novel refinement method ensures provable guarantees of minimality.
In our final experiment, we compare our explanations with two widely used non-verffication-beee based methods for suffi- cient explanations: (i) Anchors (Ribeiro et al., 2018) and (ii) SIS (Carter et al., 2019). Although these methods op- erate relatively efficiently, they do not formally verify the sufficiency of the explanations, relying instead on a sam- pling heuristic across the complement. We depicted the comparisons between our verified explanations and those generated by Anchors and SIS in Tab. 2. These results highlight that while faster, these methods produce far fewer sufficient explanations ($ 25%).
7. Limitations and Future Work
6. Related Work
A limitation of our framework, as with any method solving this task, is its dependence on neural network verification queries. Verification techniques, although still currently limited for state-of-the-an models, are rapidly advancing in scalability (Wang et al., 2021b; Brix et al., 2023). Our method adds an orthogonal step in using these tools to de- rive provable explanations for neural network decisions. Hence, as the scalability of verification tools improves, so will that of our approach. Importantly, compared to meth- ods addressing the same task, our approach is significantly more efficient and handles much larger models. Moreover, while we focus on minimal sufficient explanations, future work could extend our abstraction other provable explanations. To demonstrate the broader applicability of our method, we discuss several extensions in Appendix D. These include: (i) regression tasks, (ii) ex- pansions into language domains, and (iii) various enhance- ments to our algorithm, such as different feature orderings and certain scalabilit--suffiienn, trade-offs.
Formal XAL Our work is closely related to formal XAI (Marques-Silvaa 2023), which aims to provide explana- tions with formal guarantees. Previous research has focused on deriving provable sufficient explanations for decision trees (Huang et al., 2021; Izza et al., 2022; Bounia & Ko- riche, 2023; Arenas et al., 2022), linear models (Marques- Silva et al., 2020; Subercaseaux et al., 2025), monotonic et al., 2021; El Harzli et al., 2022), and tree ensembles (Izza& & Barques-Silva. 2021; Ignatiev et al., 2022: Boumazouza al., 2021; Audemard et al., 2022; 2023; Bassan et al., 2025a). More closely related to our work are methods that derive minimal sufficient expla- nations for neural networks (Bassan& & Katz, 2023; La Malfa et al., 2021; Wu et al., 2023; Bassan et al., 2023; Izza et al., 2024; Azzolin al., 2025), which often rely on verification tools. While these tools have improved in scalability (Wu et al., 2024; Wang et al., 2021b; Brix et al., 2023), com- puting provable explanations remains computationally ex- pensive (Barceló et al., 2020; Wäldchen et al., 2021; Adolfi et al., 2025; Bassan et al., 2024; Ordyniak et al., 2023; Marzouk & De La Higuera, 2024; Marzouk et al., 2025; Amir et al., 2024; Huang et al., 2023) and typically requires multiple verification queries (Ignatiev et al., 2019). Other approaches mitigate these computational challenges by re- defining sufficiency (Jin et al., 2025; Izza al., 2023; Wang et al., 202 a; Chockler et al., 2024; Jin et al., 2025), apply- ing smoothing (Xue et al.. 2023), or using self-explaining methods (Bassan et al., 2025b; Alvarez Melis & Jaakkola, 2018; Bassan et al., 2025c).
classifiers (Marques-Sii)
strategies to
8. Conclusion
Obtaining minimal sufficient explanations for neural net- works offers promising way to provide explanations with formally verifiable guarantees. However, the scalability of generating such explanations is hindered by the need to invoke multiple neural network verification queries. Our abstraction-refinemnnn approach addresses this by starting with a significantly smaller network and refining it as needed. This ensures that the explanations are provably sufficient for the original network and, ultimately, both provably mini- mal and sufficient. Our method also produces intermediate explanations, allowing for an efficient early stop when suffi- cient but non-minimal explanations are reached, while also offering a more fine-grained interpretation of the model pre- diction across abstractions. Our experiments demonstrate that our approach generates minimal sufficient explanations substantially more efficiently than traditional methods, rep- resenting significant step forward in producing explana- tions for neural network predictions with formal guarantees.
A Abstraction-refinement abstraction--efiinmmett, technique commonly used to hance the efficiency of symbolic model checking (Clarke et al., 2000; Wang et al., 2006), and applied in software (Jhala & Majumdar, 2009; Flanagan & Qadeer, 2002), hard- ware (Andraus et al., 2007), and hybrid systems verification (Alur et al., 2000). Recently, abstraction-refinemees has been used to improve the efficiency of certifying adversar- ial robustness by abstracting neural network sizes (Elboher
Our algorithm leverages

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Impact Statement
Andraus, Z.., Liffiton, M., and Sakallah, K. CEGAR-Based
Formal Hardware Verification: A Case Study. Ann Arbor, 1001:48, 2007.
Since our work contributes to advancing both the practical and theoretical dimensions of explainability, it encounters implications common to other frameworks in the field, in- cluding susceptibility to adversarial attacks, privacy con- cerns, oversimplifications,, and potential biases. By priori- tizing explanations with provable guarantees, we strive to improve trustworthiness. However, as the primary focus of our work lies on systematic and methodological aspects, we believe it does not have any immediate or direct social ramifications.
Arenas, M., Barceló, P., Romero Orth, M., and Suber- caseaux, B. On Computing Probabilistic Explanations for Decision Trees. In Proc. 35th Inf. Conf. on the Advances in Neural Information Processing Systems (NeurIPS), pp. 18695-28700 2022.
Audemard, G., Bellart, S., Bounia, L.,, Koriche, F., Lagniez, J.-M., and Marquis, P. Trading Complexity for Sparsity in Random Forest Explanations. In Proc. 36th AAAI Conf. on Artificial Intelligence, pp. 5461-5469, 2022.
Acknowledgements
Audemard, G., Lagniez, J.-M., Marquis, P., and Szezepan- ski, N. Computing Abductive Explanations for Boosted Trees. In Proc. Int. Conf. on Artificial Intelligence and Statistics (AISTATS), pp. 4699-4711, 2023,
This work was partially funded by the European Union (ERC, VeriDel., 1011 (01113..)) Views and opinions expressed are however those of the author(s) only and do not neces- sarily 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. This research was additionally supported by grant from the Israeli Science Foundation (grant number 558/24) and from the project FAT (No. 286525601) funded by the German Research Foundation (Deutsche Forschungs- gemeinschaft, DFG).
Azzolin, S., Malhotra, S., Passerini, A., and Teso, S. Be- yond Topological Self-Explainable GNNs: A Formal Explainability Perspective, 2025. Technical Report.
https://arXiv:2555 021502..271... 02719.
Barceló, P., Monet, M., Pérez, J., and Subercaseaux, B. Model Interpretability Through the Lens of Computa- tional Complexity. Proc. 33rd Inf. Conf. on Advances in Neural Information Processing Systems (NeurIPS), pp. 15487-15498, 2020.
References
Adolfi, F., Vilas, M., and Wareham, T. The Computational Complexity of Circuit Discovery for Inner Interpretabilityy In Proc. 13th Int. Conf. on Learning Representations (ICLR), 2025.
Bassan, S. and Katz, G. Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks. In Proc. 29th Int. Conf. on Tools and Algorithmss for the Construction and Analysis of Systems (TACAS), pp. 187- 207, 2023.
Althoff, M. An Introduction to CORA 2015. In Proc. 1st and 2nd Int. Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH), pp. 120-151, 2015.
Bassan, S., Amir, G., Corsi, D., Refaeli, I., and Katz, G. Formally Explaining Neural Networks Within Reactive Systems. In Proc. 23rd Int. Conf. Formal Methods in Computer-Aided Design (FMCAD), pp. 1-13, 2023.
Alur, R., Henzinger, T., Lafferriere, G., and Pappas, G. Discrete Abstractions of Hybrid Systems. In Proc. of the IEEE, pp. 971-984, 2000.
Bassan, S., Amir, G., and Katz, G. Local vs. Global Inter- pretability: A Computational Complexity Perspective. In Proc. 41st Int. Conf. Machine Learning (ICML), pp. 3133-3167, 2024.
Alvarez Melis, D. and Jaakkola, T. Towards Robust In- terpretability with Self Self-Exxlaining Neural Networks. In Proc. 31 Ini. Conf. on Advances in neural information processing systems (NeurIPS), 2018
Bassan, S., Amir, G., Zehavi, M., and Katz, G. What makes Ensemble (Un) Interpretable? In Proc. 42nd Int. Conf. on Machine Learning (ICML), 2025a.
Amir G., Bassan, S., and Katz, G. Hard to Explain: On the Computational Hardness of In- nn-Distribution Model Interpretation. In Proc. 27th European Conf. on Artifical Intelligence (ECAI), 2024.
Bassan, S., Eliav, R., and Gur, S. Explain Yourself, Briefly! Explainnn Neural Networks with Concise Sufficient Reasons. In Proc. 13th Int. Conf. on Learning Represen- tations (ICLR), 2025b.
Ancona, M., Oztireli, C., and Gross, M. Explaining Deep Neural Networks with a Polynomial Time Algorithm for Shapley Value Approximation. In Proc. 38th Int. Conf. on Machine Learning (ICMI.), pp. 272-281, 2019.
Bassan, S., Gur, S., Zeltyn, S., Mavrogiorgos, K., Eliay, R., and Kyriazis, D. Self-Explaining Neural Networks for
10

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Business Process Monitoring, 2025c. Technical Report. https: / http://aaxvvv::.:.13.3 18067.
Darwiche, A. and Hirth, A. On the Reasons Behind Deci- sions. In Proc. 24th European Conf. on Artifical Intelli- gence (ECAI), pp. 712-720, 2020.
Boudardara, F., Boussif, A., Ghazel, M., and Meyer, P.- J. Deep Neural Networks Abstraction using An Inter- val Weights Based Approach, 2022. Technical Report. ht http:::/haa..cciencce/aal---- wwweeenceeha-044220000
EI Harzli, O., Grau, B. C., and Horrocks, I. Cardinality- Minimal Explanations for Monotonic Neural Networks.
In Proc. 31st Int. Joint Conf. on Artificial Intelligence (IJCAI), 2022.
Boumazouza, R., Cheikh-Alili, F., Mazure, B., and Tabia, K. ASTERYX: A model-Agnostic SaT-basEEd appRoach for sYmbolic and score-based eXplanations. In Proc. 30th ACM Int. Conf. on Information & Knowledge Manage- ment (CIKM). pp. 220-129,22 2021.
Elboher, Y., Goutschlich, J., and Katz, G. An Abstraction- Based Framework for Neural Network Verification. In Proc. 32nd Inf. Conf. on Computer Aided Verification (CAV), pp. 43-65, 2020.
Elboher, Y., Cohen, E., and Katz, G. Neural Network Verification Using Residual Reasoning. In Proc. 20th Int. Conf. on Software Engineering and Formal Methods (SEFM), pp. 173-189, 2022.
Bounia, I.. and Koriche, F. Approximating Probabilistic Explanations via Supermodular Minimization. In Proc. 39th Int. Conf. on Uncertainty in Artificial Intelligence (UAI), pp. 216-225, 2023.
Flanagan, C. and Qadeer, S. Predicate abstraction for soft- ware verification. In Proc. of the 29th ACM SIGPLAN- SIGACT symposium on Principles of programming lan- guages (POPL), pp. 191-202, 2002.
Brix, C.,, Müller, M., Bak, S., Johnson, T., and Liu, C. First Three Years of the International Verification of Neural Networks Competition (VNN-COMP). Int. Journal on Software Tools for Technology Transfer (STTT), pp. 329- 339, 2023.
Huang, X., Izza, Y., Ignatiev, A., and Marques- -Silva, J. On Efficiently Explaining Graph-Basee Based Classifiers. In Proc. 18th Int. Conf. on Principles of Knowledge Representa- tion and Reasoning (KR), 2021.
Carter, B., Mueller, J., Jain, S., and Gifford, D. What Made You Do This? Understanding Black-Box Decisions with Sufficient Input Subsets. In Proc. 22nd Int. Conf. on Artificial Intelligence and Statistics (AISTATS), pp. 567- 576, 2019.
Huang, X., Cooper, M., Morgado, A., Planes, J., and Feature Necessity Relevancy in ML Classifier Explanations. In Proc. 29th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 167-186, 2023.
Marques-
Carter, B., Jain, S., Mueller, J. W., and Gifford, D. Overinter- pretation Reveals Image Classification Model Pathologies. In Proc. 34th Int. Conf. on Advances in Neural Informa- tion Processing Systems (NeurIPS), pp. 15395-15407, 2021.
Ignatiev, A., Narodytska, N., and Marques-Silee J. Abduction Basedd Explanations for Machine Learning Models. In Proc. AAAI Conf. on Artificial Intelligence, pp. 1511 1519, 2019.
Casadio, M., Dinkar, T., Komendantskaya, E., Arnaboldi, L., Daggitt, M., Isac, O., Katz, G., Rieser, V., and Lemon, O. NLP Verification: Towards a General Methodology for Certifying Robustness. European Journal of Applied Mathematics, pp. 1-58, 2025.
Ignatiev, A., Izza, Y., Stuckey, P., and Marques-Sine J. Us- ing MaxSAT for efficient explanations of tree ensembles. In Proc. 36th AAAI Conf. on Artificial Intelligence, pp. 3776-3785, 2022.
Chockler, H., Kelly, D., Kroening, D., and Sun, Y. Causal Explanations for Image Classifiers. 2024. Technical Report. https::t///..... attpaaaiivvii1.i11.. 08875.
Izza, Y. and Marques-Sile Silva, J. On Explaining Random Forests with SAT. In Proc. 30th Int. Joint Conf. on Artifi- cal Intelligence (IJCAI), 2021.
Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. Couttrexample-GGidee Abstraction Refinement. In Proc. 12th Int. Conf. on Computer Aided Verification (CAV), pp. 154-169, 2000.
Izza, Y., Ignatiev, A., and Marques-Silva, J. On Tackling Explanation Redundancy in Decision Trees. Journal of Artificial Intelligence Research (JAIR), pp. 261-321, 2022.
Cohen, E.,, Elboher, Y. Y., Barrett, C., and Katz, G. Tighter Abstract Queries in Neural Network Verification. In Proc. of 24th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (L.PAR), pp. 124-143, 2023.
Izza, Y., Huang, X., Ignatiev, A., Narodytska, N., Cooper, M., and Marques-Silva,, J. On Computing Probabilistic Abductive Explanations. Int. Journal of Approximate Reasoning (IJAR), pp. 108939, 2023.

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Izza, Y., Huang, X., Morgado, A., Planes, J., Ignatiev, A., and Marques-Silva, J. Sestance-Restrctter Explanations: Theoretical Underpinnings & Efficient implementation. In Proc. 21st Int. Conf. on Principles of Knowledge Rep- resentation and Reasoning (KR), pp. 475-486, 2024.
Marques- SSilva, and Ignatiev, A. Delivering Trustworthy AT Through Formal XAI. In Proc. 36th AAAI Conf. on Artificial Intelligence, pp. 12342-12350, 2022.
Marques-Sine Silva,, J., Gerspacher, T., Cooper, M., Ignatiev, A., and Narodytska, N. Explaining Naive Bayes and Other Linear Classifiers with Polynomial Time and Delay. In Proc. 33rd Int. Conf. on Advances in Neural Information Processing Systems (NeurIPS), pp. 20590-20600, 2020,
Jhala, R. and Majumdar, R. Software Model Checking. ACM Computing Surveys, pp. 1-54, 2009.
Jin, H.. Xue. A., You, W., Goel, S., and Wong, E. Probabilis- tic Stability Guarantees for Feature Attributions. 2025. Technical Report.
Marques-Silva, J., Gerspacher, T.,, Cooper, M., Ignatiev, A., and Narodytska, N. Explanations for monotonic clas- sifiers. In Proc. 38th Int. Conf. on Machine Learning (ICML), pp. 7469-7479, 2021.
13787.
Julian, K., Lee, R., and Kochenderfer, M. Validation of Image-Based Neural Network Controllers through Adap- tive Stress Testing. In 2Proc. 23rd IEEE Int. Conf. on Intelligent Transportation Systems (ITSC), pp. 1-7, 2020.
Marzouk, R. and De La Higuera, C. On the Tractability of SHAP Explanations under Markovian Distributions. In Proc. 41st Int. Conf. on Machine Learning (ICML), pp. 34961 -34966, 2024.
Katz, G., Barrett, C., Dill, D. L.. Julian, K., and Kochen- derfer, M. J. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Proc. 29th Int. Conf. Computer Aided Verification (CAV), pp. 97-117, 2017.
Marzouk, R., Bassan, S., Katz, G., and la Higuera, D. On the Computational Tractability of the (Many) Shapley Values. In Pruc. 28th Inf. Conf. on Artificial Intelligence and Statistics (AISTATS), 2025.
Krizhevsky, A. and Hinton, G. Learning Multiple Layers of Features from Tiny Images, 2009. Tech- nical Report. https: / /www. cs. toronto......oo... edd// akriz/learning-- features 2009-00.020.-00 pdf.
Ordyniak, S., Paesani, G., and Szeider, S. The Parameter- ized Complexity of Finding Concise Local Explanations. In Proc. 32nd Int. Joint Conf. on Artificial Intelligence (IJCAI), 2023.
La Malfa, E., Zbrzezny, A., Michelmore, R., Paoletti, N., and Kwiatkowska, M. On Guaranteed Optimal Robust Explanations for NLP Models. In Proc. Int. Joint Conf. on Artificial Intelligence (IJCAI), pp. 2658-2665, 2021.
Prabhakar, and Rahimi Afzal, Z. Abstraction Based Out- put Range Analysis for Neural Networks. In Proc. 32nd Int. Conf. Advances in Neural Information Processing Systems (NeurIPS), 2019.
Ladner, T. and Althoff, M. Fully Automatic Neural Net- work Reduction for Formal Verification, 2023. Technical Report. https: wwwpiv:xvvvv///// 2305. 01932.
Ribeiro, M., Singh, S., and Guestrin, C. "Why Should I Trust You?" Explaining the predictions of any classifier. In Proc. 22nd Int. Conf. on Knowledge Discovery and Data Mining (SIGKDD), pp. 1135-1144, 2016.
LeCun, Y. The MNIST Database of Handwritten Digits, 1998. http:/ //yann. Lecun, cwt. eexcb/mnniieeeee
Ribeiro, M., Singh, S., and Guestrin, C. Anchors: High- Precision Model-Agnostic Explanations. In Proc. 32nd AAAI Conf. on Artificial Intelligence, 2018.
Liu, J., Xing. Y., Shi, X., Song, F., Xu, Z., and Ming, Z. Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks. ACM Transactions on Software Engineering and Methodology (TOSEM), pp- 1-35, 2024.
Sälzer, M. and Lange, M. Reachability is NP-Complete even for the Simplest Neural Networks. In Proc. 15th Int. Conf. on Reachability Problems (RP), pp. 149-164, 2021.
Lundberg, S. M. and Lee, S.-I. A Unified Approach to Interpreting Model Predictions. In Proc. 30th Int. Conf. on Advances in Neural Information Processing Systems (NeurIPS), 2017.
Siddiqui. S., Mukhopadhyay, D., Afzal, M., Karmarkar, H., and Madhukar, K. Unifying Syntactic and Semantic Abstractions for Deep Neural Networks. In Proc. Formal Methods for Industrial Critical Systems (FMICS), pp. 201-219, 2024.
Marques-Silva. J. Logic-Based Explainability in Machine Learning. In Reasoning Web. Causality, Explanations and Declarative Knowledge: 18th Int. Summer School 2022, Berlin, Germany, September 27-30, 2022, Tutorial Lectures, pp. 24-104 104. 2023.
Stallkamp, J., Schlipsing, M., Salmen, J., and Igel, C. Man vs. Computer: Benchmarking Machine Learning Algo- rithms for Traffic Sign Recognition. Neural Networks, pp. 323-332, 2012.
12

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Subercaseaux, B., Arenas, M., and Meel, K. Probabilistic Explanations for Linear Models. In Proc. 39th AAAI Conference on Artificial Intellignce, pp. 20655-20662, 2025.
Sundararajan, M., Taly, A., and Yan, Q. Axiomatic Attri- bution for Deep Networks. In Proc. 34th Int. Conf. Machine Learning (ICML), pp. 13-83328, 2017.
Wäldchen, S., Macdonald, J., Hauch, S., and Kutyniok, G. The Computational Complexity of Understanding Binary Classifier Decisions. Journal of Artificial Intellignnce Research (JAIR), pp. 351-387, 2021.
Wang, C., Hachtel, G., and Somenzi, Abstraction Refine- ment for Large Scale Model Checking. Springer Science & Business Media, 2006.
Wang, E., Khosravi, P., and Van den Broeck, G. Probabilistic Sufficient Explanations. Proc. 30th Int. Joint Conf. on Artificial Intelligence (IJCAI), 2021a.
Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., and Kolter, J. Z. Beta-Crown: Efficient Bound Propagation with Per-Neuron Split Constraints for Neural Network Robustness Verification. Proc. 34th Int. Conf. on Advances in Neural Information Processing Systems (NeurIPS), pp. 29909-299999999 29921, 2021b.
Wu, H., Isac, O., Zeljić, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I,, Amir, G., Julian, K., Bassan, S., et al. Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In Proc. 36th Int. Conf. Computer Aided Verification (CAV), pp. 249-264, 2024.
Wu, M., WU, H., and Barrett, Verix: Towards Verified Explainability of Deep Neural Networks. Proc. 36th Int. Conf. on Advances in Neural Information Processing Systems (NeurIPS), 2023.
Xue, A., Alur, R., and Wong, Stability Guarantees for Feature Attributions with Multiplicative Smoothing. In Proc. 36th Int. Conf. on Advances in Neural Information Processing Systems (NeurIPS), pp. 62388-62413 2023.
13

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Appendix
The appendix includes supplementary experimental results, implementation details, and proofs.
Appendix A contains all proofs of this paper along with further details on the abstraction method.
Appendix contains implementation details.
Appendix C contains additional experiments and ablation studies. Appendix D discusses the extension other domains than image classification, including regression and language tasks.
A. Proofs
In this section, we provide the missing proofs in the same order as they appear in the main paper.
A.1. Preliminary Definitions and Lemmas
To prove Prop. 1, we define both a neural network and an abstract neural network layer-by-layer, as described in Sec. 3. Definition 6 (Neural Network). Letx e Ro be the input of neural network f with layers, its output y f(x) e R is obtained as follows:
ho: x, hs =- LA (hi-1), y hN: k E [x],
where Lg: R 1 - R represents the operation of layer is and is given by Lk (ha-1) := o (Waha-1 + by) with weight matrix WE E T bias by TR activation function a: Te -> R and number of neurons E N.
An abstract network is then described by: Definition 7 (Abstract Neural Network). Letx Rh be the imput of abstract neural network f with layers, its output y f'(x) C I== is obtained as follows:
Hyg [x}. H4 == L'g (Ha-)), y= Hy, k [
where T/:: 2(R" - 200%) represents the operation of the abstract layer & and is given by Tig (H/--) = o (W +
b()) with weight matrix W R" bias b'g E W activation function σ: IR. R number of neurons n/. E N.
n/= no. n/. nw and @ denoting the Minkowski sum (Given two sets S1 TR. then S₁ S2 {81 + 82 81
S1. $2 S2))
Let X' C R" be the set of points satisfying the input specification (x) for point x E R" (Sec. 2.2). As mentioned in Sec. 2.2, the exact output ) f(X) is often infeasible compute, and an enclosure y y is computed instead by bounding all approximation errors. This is realized by iteratively propagating X' through all layers and enclosing the output of each layer. For example, given an input set H4-1 C HE-1 to layer k; we obtain the output Hs 3 La (Ha-1) = Hi. with Hli = Ho = X' and y = Hn. Let Hys y and Hg Y denote the enclosures the sets Hig V' using the original network and the abstract network f', respectively. In this work, we use a neuron pauronnerggig construction defined by (Ladner & Althoff, 2023):
Lemma (Neuron-Merging Construction (Ladner Althoff, 2023, Prop. 4)). Given a layer E [N - 1] of network f, output bounds In R set of neurons merge B& S [mx]. and the indices of the remaining neurons B₁ == [nx]]Bs the layer k and is are constructed as follows:
W% W b/g = DA(BL))
W k++ W (K41),))) b/441 = -b4t + 1
where W (T) is the approximation error. The construction ensures that Hitt C HH
Given a neural network f. an input perturbation radius Ep, and a subset S C [n], we say that f is an abstract network constructed by neuron merging with respect to the query (f,, x, S, c,) if we define the input set X' == B," (xx: and recursively apply the neuron-men meruing construction as described in Lemma for any two layers L and Lg- We can now provide an explicit proof of Prop.
14

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
A.2. Proof of Prop. 1
Proposition (Explanation Under Abstraction). Given neural network an input x, a perturbation radius Ep and subset S _ [m], let f' be abstract network constructed by neuron merging concerning the query (f, S, cp)- Then, it holds that:
suff(f',, S. cp) = suff S. (p).
Proof. We prove this statement by contradiction: Assume that S is a sufficient explanation for the abstract network, i.e., for (f", ,x Gp), but not for the original network, i.e., for (f,x, Gp) Given that a sufficient explanation for (f", , xp)) the following holds (Def. 3):
Vj ft VI (x)( [min (xss((((s: 2 max(f((xs:sss
(1)
where f == arg max; (z) is the target class. Moreover, since S is not a suffcient explanation concerning (f,x, fp) it follows that (Def. I):
EF'S E (x): arr max f(xs:&'s) # arg max f(x) = tl.
(2)
Since Eq. (1) is valid for any x Bp"(x) (x), it explicitly applies to E B (x) well. Specifically, have:
vj E [d) (xx:(((((s: mxx(
(3)
We now assert that to establish the correctness of the proposition, it suffices to demonstrate that:
f'xs;K') E (xxs:''s)
(4)
The rationale is as follows: Eq. (4) holds, it would directly contradict our initial assumption. To begin, observe that Eq. (4)
directly leads to:
Vj [c], (min(("(xs (xx::'ss I max(f((ss:
(5)
and therefore, based on Eq. (3), it will directly follow that:
Vj E [e]{t, (f(xs:)'s)) 2 (xs+(((s: 2 max(f(xs::&))) 2 f(xs;
(6)
Now, specifically, given that the following condition satisfied:
Vj f [c],
(f(s):&)) 2 f(xs;
This indicates that arg max, ((xs::'ss())) = I,, which contradicts the assumption stated in Eq. (2).
We are now left to prove that fxxs; E f'x::: Let h& and HC be as defined in Def. 6 and Def. 7, respectively, for the input (xs;''s) E X, where X' = B (xs; Recall that this is defined since the merging is performed with respect to the query (f.x, ep). We show by induction that the statement (xs:;'')) e f'(s::'')) holds:
Induction hypothesis. is E [k]: The condition h2 E Hl is satisfied if a neuron merging operation was performed between any two layers up to and including layer l 1.
Induction base. k = 0: Trivially holds (Def. 7).
Induction step. k + k + 1: We need to show that h&41 E H4+1- Let Bg, In be as in Lemma and H'S the output set of layer before merging. Thus, I H' holds. From the induction hypothesis, we know that hy E Hi holds. Recall from
15

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Def. 6 that hx+1 = ( k+1 bx+1). Doing the for Hig (Def. and applying the neuron merging construction (Lemma gives us:
h++1 E oWW++1HH @ bx+1) = (W H
(K(B,) + W (++((.B.) H
k(Ba)) + bx+1)
- [o JR(B) ① W M441 H (BB, ① Bb+11)
= =1++1
which proves the induction step. As the induction hypothesis holds for k K, conclude that f'xx: E ('xstt's) must be true. This, as previously explained, implies that arg maxj ((xs: t, which contradicts assumption in Eq. (2).
A.3. Proof of Prop. 2
Proposition 2 (Refined Abstract Network). Given neural network J, an input x, a perturbation radius Cp E TR a subset S S [n], and an abstract network f' with reduction rate p' E [0, we can construct refined abstract network f" from J. with reduction rate p" >> for which holds:
VI E (x) f(x::tg) E (xs: C f'(:;tzs) f
Proof. The containment of (g) follows using an analogous proof as for Prop. 1. While the subset relation does not hold in general when applying the abstraction (Lemma 1) using p" instead of pf as different neurons might be merged, one can restrict the neurons that are allowed to be merged to the subset neurons A' = Ukg(x-1155 that were merged to obtain f'. Using this restriction and as p" > p' holds, C N' holds. Then, as all additionally merged neurons A' \ s" induce outer approximations and everything else is equal, the subset relation holds.
A.4. Proof of Prop. 3
Proposition (Intermediate Sufficient Explanation). Let there be a neural network f, an abstract network f', and a refined neural network f" Then, it holds that:
suff(f', x, S, Ep) = suff(f", x, S, Ep) and suff(f, x, S, cp).
suff(f" x, S, cp)
We show the first implication by contradiction: Let us assume that S is a sufficient explanation for f' but not for f" Thus, the query (f", x, S pp) does not fulfill Def. 3. However, ("xxx::g)) (x(xx; holds due Prop. the query (f', x, S, ep) can also not fulfill Def. 3, which contradicts our assumption. The proof for the second implication is analogous.
Proof.
A.5. Proof of Prop. 4
Proposition 4 (Intermediate Minimal Sufficient Explanation). Let there be neural network f, an abstract network f', and refined neural network f" Then, i S is sufficient explanation concerning f. f', and f", it holds that:
min-suff( (f, x, S, Gp) = min-suff(f" xx S, (p) and min-suff( S, cp) = min-suff( x, S, cp)
Proof. The statement is shown by contradiction for the relation of f and f": Let us assume that the explanation S is minimal for f but not for l Thus, there must be a S' C which is minimal for f" However, this cannot be an explanation for f as is already minimal for f. From Prop. it follows that is also minimal explanation for f. which contradicts our assumption that S is minimal. Analogous reasoning holds for f" and f".
A.6. Proof of Prop.
Proposition (Greedy Minimal Sufficient Explanation Search). Alg. produces a provably sufficient and minimal explanation concerning the query (f, x. S, 6p), which converges to the same explanation as obtained by Alg. I.
16

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Proof. All line numbers are with respect to Alg. 2: The invariant described in line 2 holds due Prop. 3. Thus, the final explanation S is sufficient concerning the original network f-
We show the minimality by contradiction: Let us assume the final explanation S is not minimal: There exists feature i e [n] such that S \ {i} is still sufficient (Def. 2). It follows that we cannot have found a counterexample in line 8, Thus, to break the do-while loop, the sufficiency check in line 5 must have passed either on an abstract network or eventually after all refinement steps on the original network. However, this would remove feature from the explanation, which violates our assumption.
We converge to the same explanation Alg. we process the features in the same order, Prop. 3 holds, and if removing feature results in non-sufficient explanation and no counterexample on the original network can be found, we refine the abstract networks until we converge to the original network.
B. Implementation Details
In this section, we offer further technical details about the implementation of our algorithms and provide specifics on the model architectures and training methods used in this study.
B.1. Details on Abstract Explanations
In the running example in Sec. 3 and Sec. 4, we use a simplified process for merging neurons to illustrate the abstraction for clarity. However, as discussed in both Sec. 3, Sec. 4, and Appendix A, the actual method employs the Minkowski sum (Lemma 1), which is sound and obtains tight bound while preserving the abstraction properties. For completeness, provide here a simple version of the running example that reflects the use of this bound.
Input
Hidkon
Ourgus
Laput
Hidden
Output
Input
Hiddon
Outpur
[:1
[-1.5 -1.4
(-0.50 -0 45
[AR.
1-1115, [.50]
[1.1]
[1.
[1
0.18 0.22)
0.11
[1.1]
11
1.
1.5
(a) One perturbed feature-
20%
(b) Two perturhed features
p= 20%.
(c)
Two perturbed features 40%
Iaput
Hidden
Output
Input
Thidien
Outpus
Eaput
Hiblenn
Output
[0.0|
[-035
10.4|
pa
1.0.1.11
0.000 474
10.00 0.11)
0.85)
10.09 0.111
MRL1
10.18 0.23)
1uL1 m22
[
17 91
(d) Three perturbed features - p=40%.
(c) Three perturbed features - 1000
(f) Four perturbed features p=100%
Figure 7: An example of a full abstraction refinement procedure using the tighter Minkowski sum instead of the weighted sum.
Fig. 7 illustrates, similar to the running example in Sec. and Sec. 4, the specified bounds for each input feature and hidden ReLUU activation neuron. We consider a binary classification task where the output is interpreted class 1 if the output neuron has a positive value, and class 0 otherwise. For the initial input [1, 1, 1, 1]. the output is positive, resulting in a classification of 1. When neurons are merged at a rate of p = 40%, an explanation size 2 is sufficient; however, the same explanation size is inadequate when p = 20%. For the full network (p = 100%), the cardinality aeddiaaity-minimall minimal explanation has a size of 1.
17

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Table 3: Dimensions for the MNIST classifier.
Table 4: Dimensions for the CIFAR- 10 classifier.
Layer type
Paramater
Activation
Layer type
Paramater
Activation
Input
784 x 200
Sigmoid
Input
32 x 32 x
ReLU
Fully-connected
200 x 200
Sigmoid
Convolution
32 x x 4
ReLU
Fully-connected
200 x 200
Sigmoid
Convolution
64 x 32 x 4 x 4
ReLU
Fully-connected
200 x 200
Sigmoid
Fully-connected
32768 128
ReLU
Fully-connected
200 x 200
Sigmoid
Fully-connected
128 x 64
ReLUU
Fully-connected
200 x 200
Sigmoid
Fully-connected
64 X 10
Softmax
Fully-connected 200 x 200
Sigmoid
Fully-connected
200 x 10
Softmax
Table 5: Dimensions for the GTSRB classifier.
Layer type
Paramater
Activation
Input
32 32 3
Sigmoid Sigmoid
Convolution
16 3 x 3 x 3
Avg-ppoliing
2
Convolution
32 16 3 3
Sigmoid
Avg--pooling
2 x 2
Fully-connected
4608 x 128
Sigmoid softmax
Fully Fully-connected
128 x 43
B.2. Implementation details of Alg. 1 and Alg. 2
Both Alg. 1 and Alg. 2 iterate over the features in a specified order. This approach aligns with the methodologies used in (Wu et al., 2023; Izza et al., 2024; Bassan & Katz, 2023), where a sensitivity traversal over the features is employed. We prioritize iterating over features with the lowest sensitivity first, as they are most likely to be successfully freed, thus leading to a smaller explanation. As we refine the abstract network following Prop. 2, we define a series of reduction rates used during each refinement step. For simplicity, we start with coarsest abstraction at a reduction rate p 10% of the original network's neurons and increase p by 10% at each subsequent refinement, until p = 100% is reached, which restores the original network.
We also note that while MNIST utilizes grayscale images, both CIFAR-10 and GTSRB use RGB images. Following standard practices for colored images (Wu et al., 2023; Ribeiro et al., 2018; Carter et al., 2019; 2021), we provide explanations for CIFAR- 10 and GTSRB on a per-pixel basis, rather than at the neuron level; this means we either include/exclude all color channels of pixel within the explanation or none. Consequently, the maximum size of an explanation, |S], 32 32 instead of 32 32- 3. For MNIST, which has only one color channel, the maximum size is always |S| 28 288
B.3. Training and Model Implementation
For MNIST and CIFAR-IO, we utilized common models from the neural network verification competition (VNN-COMP) (Brix et al., 2023), which are frequently used in experiments related neural network verification tasks. Specifically, the MNIST model architecture sourced from the ERAN benchmark within VNN-COMP, and the CIFAR-I0 model is derived from the "marabou" benchmark. Since GTSRB is not directly utilized in VNN-COMP, we trained this model using batch size of 32 for 10 epochs with the ADAM optimizer, achieving an accuracy of 84.8%. The precise dimensions and configurations of the models used for both VNN-COMP (MNIST and CIFAR- 11) and GTSRB are provided: Tab. 3 for MNIST, Tab. 4, and Tab. for GTSRB. For MNIST and GTSRB, we use a perturbation radius 6oc = 0.01 as commonly used in VNN-COMP benchmarks, and for CIFAR- 10, we use a smaller perturbation radius 6 = 0.001 as we have found this network be not very robust.
18

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Abstracterefine (ours)
Original network
200
2,000
20,000
Cumulative time
100
1,000
10,000
0
0
200
400
600
200
400
600 800
1,000
200 400
600
800
1,000
Nr. of processed features
Nr. processed features
Nr. of processed features (c) GTSRB
(a) MNIST
(b) CIFAR-10
Figure 8: The percentage of features successfully processed coeissed-ieeniffeee as either included or excluded from the explana- tion tion-over cumulative time for MNIST, CIFARIO, and GTSRB, throughout the entire -erraction-refinemmett algorithm, or using the standard verification algorithm on the original network. The standard deviation shown as shaded region.
Original network
10%
20%
30%
40%
P 50%
80%
90%
1,000
1,000
Explomation size
600
800
800
400
1haal
1010
600
600
USB
4111
100
400
Tiil
200
200
100
200
1,000
2,000
10,000
20,000
Cumalative time [s] MNIST
Cumulative time
Cumulative time [x]
(b) CIFAR-10
(c) GTSRB
Figure 9: The explanation size cumulative time for MNIST, CIFARIO, and GTSRB, segmented by reduction rate, throughout the entire abstraction-refinene algorithm, or using the standard verification algorithm on the original network. The standard deviation is shown as a shaded region.
C. Additional experiments and ablation studies
C.1. Additional experiments on image classification
In this section, we present further experimental results to complement those discussed the main body the paper. We begin by expanding on Fig. 4, which illustrates the change in explanation size over time for the standard verification method versus the abstraaction-reiinmmen approach. In Fig. 8, we offer similar comparison, this time focusing on the number of processed features, i.e., features that have been selected to be included excluded from the explanation. It is evident that the abstraction-reffine refinement method processes features more efficiently than the standard approach, leading to enhanced scalability.
We continue to build on the findings presented in Fig. 6, which illustrates the number of features processed at various reduction rates. Fig. 9, we similarly demonstrate the change in explanation size over time across different reduction rates. As lower reduction rates o initially have a much steeper curve than larger ones, the explanation size reduced faster. However, these lower reduction rates converge larger explanation sizes than larger reduction rates. Our approach benefits from both worlds by initially using the steepest curve to reduce the explanation size, and automatically switching to the next steeper curve if no features can be freed anymore using the current rate.
Lastly, we provide some qualitative figures that depict the iterative abstraction-refinemeed process in the explanations across different reduction rates. Fig. 10 displays the initial images paired with a colored grid, where each color represents a specific reduction rate. These images are selected from the MNIST, CIFAR10, 10, and GTSRB datasets. the last row, we show some
19

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Network
10%
20%
30%
10%
50%
60%
70%
80%
90%
100%
2
S
9
30
100
Figure 10: Original images compared images featuring the complete abstraction grid at various abstraction rates for MNIST, CIFAR10, and GTSRB.
explanations of GTSRB images with unexpected explanations. For example, for the first image in the last row, the red circle surrounding the sign does not seem to be very important, as these pixels could be removed from the explanations using the coarsest abstraction (p 10%).
Additionally, to provide a more detailed visualization of the entire abstraction-refinmmen explanation process, which allows users to halt the verification any stage, we include visualizations of both abstract and refined explanations at various steps and reduction rates. These visualizations are shown for all three benchmarks MNIST, CIFAR-10, and GTSRB in Fig, 11.
Finally, we also want to give visual comparison of our approach and heuristic approaches in Fig. 12: First, images Fig. 12b-d highlight the importance of minimality. For example, the interior of the forward sign is not included in our explanation, and the edges alone are sufficient for classification. This shows the interior pixels are irrelevant and can be excluded without affecting the prediction. In contrast, non-minimal sufficient subsets include unnecessary features. To better grasp the significance of small or minimal explanations, one can consider the extreme case where the entire image is chosen the explanation: although it is clearly sufficient, it is neither minimal nor informative. Secondly, image Fig. 12f-h shows that fixing the provably sufficient subset ensures robustness: any change in the complement within the domain does not alter the classification. This contrasts with heuristic subsets, where changes in the complement can flip the prediction revealing their limitations. The explanation also matches human intuition, as the highlighted region alone justifies the predicted class, unlike the much less clear heuristic explanations.
C.2. Ablation Study
C.2.1. SUFFCIENCY--CMMPUATTII TIME TRADE-OFF
In this subsection, we will examine the impact of varying perturbation radii ep on our experimental results. Larger ep perturbations make each query more challenging but provide stronger sufficiency guarantees. However, as the sufficiency conditions become more stringent, the total number of queries decreases, leading to larger explanation sizes. We conducted an experiment on MNIST using different perturbation radii, with the results presented in Tab.
20

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Network size
10%
20%
30%
40%
50%
60%
70%
80%
90%
100%
2
30
30
30
30
30
0
Original image
10%
S 30%
o 60%
80%
(f) Original network
Explanation size increases
Network size and computation time increases
Figure 11: A step-by-step visualization of the different abstraction levels for both the network and explanation across MNIST, CIFAR-10, and GTSRB.
A
(a) Original Image
(b) Sufficient (minimal)
(c) Sufficient (non-minimal)
(d) Sufficient (non-minimal)
(c) Original Image
( Sufficient (minimal)
(g) Anchors
(h) SIS
Figure 12: Visual comparisons of sufficiency and minimality of explanations.
Table 6: Impact perturbation radius 6p on explanation size and computation time.
Method
Perturbation radius
Explanation size
Computation time [s]
0.012
219.450+:12..22
110.1114:33.7 712
0.011
186.970+1140443
101.881441.66
0.010
153.240+1335773
94.897+-46.22
Abstracttrefine (ours)
0.009
119.040+127.277
81.889
0.008
87.330+113.822
62.607+58, 0.884
0.007
59.420-+95.607
53.072--56.70 709
21

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Table 7: Impact of feature order on explanation size and computation time.
Method
Feature order
Explanation size
Computation time [s]
Sensitivity Shapley In-order
153.24-:135.73 175.70=150.09
90.26:1-44.54
Abstract+refine (ours)
93.10=145.39
231.46=160.73
98.10:+46.42
Table 8: Average time to solve the verification query for different reduction rates p.
Abstraction
MNIST
CIFAR
GTSRB
p 0.1
0.08
0.35
1.89
= 0.2
0.11
0.42
3.05
= 0.3
0.13
0.55
4.73
P = 0.4
0.16
0.75
7.05
P 0.5
0.18
0.90
9.27
P 0.6
0.20
0.92
11.28
P 0.7
0.22
0.93
12.97
0.8
0.23
0.92
14.38
0.9
0.25
0.93
15.68
C.2.2. FEATURE ORDERING
We illustrate the impact of different feature orderings on the explanations generated by our method. While we adopt the approach proposed by (Wu et al., 2023), which orders features by descending sensitivity values, we also present results for explanation sizes and computation times using alternative feature orderings in our MNIST configuration. These alternatives include ordering by descending Shapley value attributions (Lundberg Lee, 2017) and, for comparison, a straightforward in-order traversal that results larger subsets. The results are summarized in Tab. 7.
C.2.3. LOCALIZATION OF
FEATURES
In this experiment, we evaluate how effectively sufficient explanations identify class daas-discriminative features - that is, the proportion of features included in the explanation that actually correspond to meaningful class indicators (c.g.. an object within an image). Since GTSRB includes object detection annotations, we leveraged its ground truth to measure how many of the features highlighted by our method fall within the annotated object regions. We compared this to explanations generated by Anchors. Our method achieved 93.33% aligmment with the annotated regions, significantly outperforming Anchors, which reached only 60.36%. This suggests that our explanations are more tightly focused around the object of interest in the image.
C.2.4. AVERAGE VERIFICATION QUERY TIME
To provide further insights into the different components of our approach, we provide average time to solve the verification query for different reduction rates and over all benchmarks in Tab. 8.
C.3. Choice of Activation Function
In our main experiments, we used networks with either ReLU or sigmoid activation, respectively (Appendix B). While this networks are taken from VNN-COMP (Brix et al., 2023), we provide a full picture in this study including both activation functions for both networks in Tab.
C.4. Analyzing different network sizes
While the previous experiment already show the scalability of our approach on different network sizes (Appendix B), the networks are on different datasets. this study, we show results comparing three networks taken from the Marabou benchmark of VNN-COMP (Brix et al., 2023), which all have CIFAR-10 images as input (Tab. 10).
22

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Table 9: Computation time and explanation size for varying activation functions.
Explanation size
Dataset
Activation
Timeout [s]
Standard
Ours
ReLU
20
439.74
380.36
MNIST
Sigmoid
100
408.7
204.4
ReLU
1, 0,00
448.7
308.2 2
CIFAR-10
Sigmoid
1. 0.000
576.50
309.13
ReLU
000
849.4
701.0
GTSRB
Sigmoid
10, 000
502.4
101.7
Table 10: Computation time of explanation for networks taken from the Marabou benchmark.
Netowrk
Standard
Ours
Small
161.50=161.33 1045.13=95.05
335.07144733 780.95=18.01
Medium
Large 1953.34=509.34
1382.95-+161.49
D. Extension to Additional Domains
Although our method primarily targets classification tasks image domains, is model-type agnostic. Furthermore, can be easily adapted to regression tasks by defining the sufficiency conditions for subset for model f IR - R and some given xnput.x IR" as:
V$ E (x): (xx: 86, 8 8 E
(8)
Comparison to results over Taxinet (Wu et al., 2023): We aimed to compare results over regression tasks to those conducted by (Wu et al., 2023) which ran "traditional" computation of a provably sufficient explanation for neural networks over the Taxinet benchmark, which a real-world safety-critical airborne navigation system (Julian et al., 2020). The authors of (Wu et al., 2023) obtain minimal sufficient explanations over three different benchmarks of varying sizes, two of which are relatively small, one which is larger (the CNN architecture). We performed experiments using this architecture. Our abstraction refinement approach obtained explanations within 35.71 = 3.71 seconds and obtained explanations size 699.30 = 169.34, which provides substantial improvement the results reported by (Wu et al., 2023) (8814.85 seconds, and explanation size was not reported). We additionally provide visualizations for some of our obtained explanations (Fig, 13 and 14).
Extension to language tasks. We present results from experiments conducted on the safeNLP benchmark (Casadio et al., 2025), trained on the medical safety NLP dataset sourced from the annual neural network verification competition
autonomous aircraft taxiing scenario (Julian al., 2020, Fig. 1), where images captured by a camera mounted on the right wing cropped (red box) and downsampled
Figure 13:
23

---

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Figure 14: Varying results of explanations across different abstraction levels for the Taxinet benchmark.
Abstract+refine (ours)
Original Network
30
Time per feature [s]
0.8
Explanation size
20
0.6
10
0.2
10
20
0.2
0.4
0.6
0.8
Nr. of Processed features
Cumulative time [s] (b)
(a)
Figure 15: (a) The percentage of features successfully ceeesssd-identffiedd as either included or excluded from the oxplanation-over cumulative time and (b) the explanation size over cumulative time for safeNLP, throughout the entire abstraction-reffiemmen algorithm, or using the standard verification algorithm on the original network. The standard deviation shown as a shaded region.
(VNN-COMP) (Brix et al., 2023). Notably, this benchmark is the only language-domee domain dataset included the competition. The perturbations applied within latent space that represents embedding of the input, thereby ensuring that the perturbations preserve the meaning of the sentence. Our findings are follows: the traditional (non--abstracioo--refieeeeee approach executed in 0.71 + 0.24 seconds with an explanation size of 6.67 + 5.06, while the completed in 0.66 + 0.22 seconds, achieving the same explanation size of 6.67 + 5.06. The results are also visualized in Fig. 15. The performance improvement here relatively modest, as the benchmark contains few nonlinear activations. However, as emphasized our study and the experimental analysis, the benefits of the abstraction-refinemee method become significantly more pronounced in larger models with more nonlinear activations, and this benehmark should purely demonstrate that approach also be applied to non-image domains.
approach
24


Reviews:
[{"review_id": "Z1Yln65tWf", "reviewer": "Reviewer_ztpX", "summary": "The paper seeks to use an abstraction-refinement approach to generate \"provably sufficient\" explanations for neural networks.\n\n==\nThe rebuttal has satisfactorily addressed my major concerns.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their valuable and constructive feedback. \n\n**Improving the motivation behind the work**\n\nWe agree that the motivation for obtaining explanations with provable guarantees, as well as the importance of the specific guarantees we provide, can be better articulated. We will make sure to better clarify this in the final version. Please see our detailed response on this point below:\n\n**General motivation.** Explanations for black-box models are often sought to *enhance user trust* in the model. For instance, consider a scenario where a medical professional must trust a black-box model to diagnose a disease from MRI scans. An explanation can help them decide whether to rely on the prediction - especially if it highlights medically relevant image regions. However, if the explanation is untrustworthy and lacks guarantees - such as presenting a subset that isn’t truly sufficient - it can misrepresent the model’s reasoning, leading the medical professional to place misplaced trust in it, potentially resulting in harmful outcomes.\n\nSuch scenarios have sparked increasing interest in the literature in developing explanations that come with provable guarantees [see, e.g., 1–8]. In this context, *explanations that are both provably minimal and sufficient* have gained significant attention as a highly sought-after form of provable explanation [see, e.g., 1-8, among others]. The key idea is to identify small subsets of features that, even when all other features take arbitrary values, still preserve the model’s prediction. This ensures the subset’s certified sufficiency, helping users understand the reasoning behind the prediction and disregard irrelevant features.\n\n**Scope.** While we agree that the guarantees our method provides inherently face scalability challenges - due to their reliance on verification, as is with all approaches tackling this task - we emphasize the significant relative improvements our approach achieves over previous methods. As several reviewers have also positively noted, our contributions are particularly notable in terms of reduced computation time, the generation of smaller explanations, and the ability to handle larger models. As the field of neural network verification continues to progress rapidly [9-11], our method - offering a significant, orthogonal enhancement for generating explanations using these tools - will similarly evolve.\n\nMoreover, to further show the generality of our results, we present experiments on two additional benchmarks in Appendix D: (1) the only language task from the annual neural network verification competition (VNN-COMP, [11]), based on a medical safety NLP dataset, which uses meaning-preserving perturbations in an embedded input space; and (2) a regression task, where our guarantees ensure output stability, evaluated on the *real-world, safety-critical Taxi-Net benchmark*, evaluated in Wu et al. (Neurips 2023, [2]).\n\nFinally, in response to the reviewer’s comment and reviewer pUMo’s feedback, we will include additional qualitative examples in the final version to better motivate our work. As part of our response to reviewer pUMo, we have added a small illustrative visualization, which we also plan to incorporate - along with other visualizations - into the final version.\n\nWe thank the reviewer for highlighting this important point and will significantly enhance our discussion of these aspects in the final version.\n\n[1] Delivering Trustworthy AI Through Formal XAI (Marques Silva et al., AAAI 2022)\n\n[2] Verix: Towards Verified Explainability of Deep Neural Networks (Wu et al., Neurips 2023)\n\n[3] Abduction-Based Explanations for Machine Learning Models (Ignatiev et al., AAAI 2019)\n\n[4] On Guaranteed Optimal Robust Explanations for NLP Models (La Malfa et al., IJCAI 2021)\n\n[5] Model Interpretability Through the Lens of Computational Complexity (Barcelo et al., Neurips 2020)\n\n[6] Computing Abductive Explanations for Boosted Trees (Audemard et al., AISTATS 2023)\n\n[7] Explanations for Monotonic Classifiers (Marques Silva et al., ICML 2020)\n\n[8] Foundations of Symbolic Languages for Model Interpretability (Arenas et al., Neurips 2021)\n\n[9] Beta-Crown: Efficient Bound Propagation with Per-Neuron Split Constraints for Neural Network Robustness Verification (Wang et al., Neurips 2021)\n\n[10] Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes (Zhou et al., Neurips 2024)\n\n[11] First Three Years of the International Verification of Neural Networks Competition (VNN-COMP) (Brix et al., STTT 2023)", "claims_and_evidence": "1. The paper is motivated by the need for proofs in high-assurance systems. However, the investigations are on relatively simple benchmarks and simple models.\n\n2. The notion of a provably correct AI system is clear. However, provably sufficient explanations need not carry the same sense of high assurance. \n\n3. Explanations are often meant for human users. It is not clear that a provably sufficient explanation will be desired by a human end user or will enhance assurance arguments for complex systems.", "methods_and_evaluation_criteria": "1. The method is evaluated on relatively simple benchmarks using simple models.\n2. There is no evaluation to show these provably sufficient explanations lead to high assurance, which is the central motivation of the paper.", "theoretical_claims": "1. The theoretical claims primarily build upon earlier work on abstraction refinement and neural network verification. \n2. The connection between explainable AI for high-assurance applications and provably sufficient explanations is tenuous.", "experimental_designs_or_analyses": "1. The experiments are on really small models and low-resolution data sets.", "relation_to_broader_scientific_literature": "The paper introduces ideas from formal verification such as abstraction refinement to explainable AI.", "essential_references_not_discussed": "None", "other_strengths_and_weaknesses": "None", "other_comments_or_suggestions": "None", "questions_for_authors": "None", "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": "AyvDdxY6or", "reviewer": "Reviewer_pUMo", "summary": "This paper introduces a novel abstraction-refinement technique to efficiently compute provably sufficient explanations of neural network predictions, defined as a subset of input features that are sufficient to determine that the prediction remains the same. The method constructs an abstract neural network, which is significantly smaller than the original model, by merging similar neurons, showing that a sufficient explanation for the abstract model is also provably sufficient for the original. Since an explanation that is minimal for the abstract network may not be minimal for the original, authors introduce an approach that iteratively refines the abstract network by gradually increasing its size until a provably minimal sufficient explanation is found for the refined network that is also provably minimal for the original. This method substantially improves the efficiency of computing sufficient explanations compared to the existing verification-based baseline while also outperforming heuristic-based methods –in terms of explanation size and time-- which fail to provide sufficient explanations and lack formal guarantees. The results demonstrate that the approach enhances scalability, interpretability, and flexibility, offering a more fine-grained understanding of neural network decisions.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We appreciate the reviewer's constructive feedback and their acknowledgment of the significance of our work.\n\n**Extension to different $\\epsilon_p$ perturbations**\n\nWe thank the reviewer for raising this important point. As correctly noted, larger $ϵ_p$ perturbations yield stronger sufficiency guarantees but may result in larger explanations. We chose the perturbation levels in this paper based on those commonly used in the annual Neural Network Verification Competition (VNN-COMP [1]), but our method is general and can be applied to any perturbation. We already include an ablation study in *Appendix C*, which we’ll reference more clearly. Per the reviewer’s suggestion, we’ll expand it with additional benchmarks, perturbation levels, and visualizations.\n\n**Qualitative analysis and the importance of minimality**\n\nWe agree that this is an important point, and will include further qualitative assessments in the final version. As a preliminary example, we share one [illustrative case](https://postimg.cc/Mcg8tp1y).\n\nFirst, image (a) highlights the importance of minimality. For example, the interior of the forward sign (red frame in image (c)) is not included in our explanation, and the edges alone are sufficient for classification. This shows *the interior pixels are irrelevant* and can be excluded without affecting the prediction. In contrast, non-minimal sufficient subsets (e.g., the other examples) include unnecessary features. To better grasp the significance of small or minimal explanations, one can consider the extreme case where the entire image is chosen as the explanation: although it is clearly sufficient, it is neither minimal nor informative.\n\nSecond, image (b) shows that fixing the provably sufficient subset ensures robustness: any change in the complement $\\bar{S}$ within the domain doesn't alter the classification. This contrasts with heuristic subsets, where changes in the complement can flip the prediction - revealing their limitations. The explanation also matches human intuition, as the highlighted region (the triangular forward sign) alone justifies the predicted class, unlike the much less clear heuristic explanations.\n\n**Additional quantitative analysis and scope**\n\nSince our work focuses on *sufficient explanations* rather than the more widely studied *additive attributions*, certain commonly used evaluation metrics - such as infidelity [2], which are specifically designed for additive forms - are not directly applicable. Adapting such metrics for sufficiency-based explanations would require significant modifications and, on its own, constitutes an interesting direction for future work. Therefore, we followed established conventions in the literature [e.g., 3–5] for evaluating sufficiency-based explanations, relying on the three widely accepted metrics in this area: generation time, sufficiency, and conciseness.\n\nThat said, we appreciate the reviewer’s interesting idea of assessing how well sufficient explanations localize class-discriminative features. We tested this using object-detection ground truth from GTSRB and found that indeed 93.33% of our method’s explanation pixels aligned with annotated regions, outperforming Anchors (60.36%). We thank the reviewer for this idea and will include a detailed experiment on this point in the final version.\n\nLastly, while our main experiments focus on vision classification models, our approach is domain-agnostic and can extend to other domains. Appendix D includes examples of both language and regression tasks. For language, we use the only VNN-COMP [1] language benchmark based on a medical NLP dataset, certifying meaning-preserving perturbations via an embedded input space. For regression, we use the real-world safety-critical Taxi-Net benchmark used in Wu et al. (Neurips 2023, [3]), showing that fixing input features keeps predictions within a target range. We will expand on these extensions and additional applications in the final draft.\n\n[1] First Three Years of the International Verification of Neural Networks Competition (VNN-COMP) (Brix et al., STTT 2023)\n\n[2] On the (In) Fidelity and Sensitivity of Explanations (Yeh et al., Neurips 2019)\n\n[3] Verix: Towards Verified Explainability of Deep Neural Networks (Wu et al., Neurips 2023)\n\n[4] On Guaranteed Optimal Robust Explanations for NLP Models (La Malfa et al., IJCAI 2021)\n\n[5] Abduction-based Explanations for Machine Learning Models (Ignatiev et al., AAAI 2019)", "claims_and_evidence": "The main claim that the proposed method outperforms existing verification-based methods by producing smaller explanations more efficiently is supported by the evaluation setup. Also, the comparison against heuristic-based approaches shows that they do not provide sufficient explanations while lacking theoretical guarantees. \nHowever, I still find the following claims unsupported:\n1.\tClaim: “A smaller explanation provides a better interpretation, and for this reason, the minimality of the explanation is also a desired property” in L019-023.\nIssue: this claim is not well-supported by the authors throughout the paper. Since this is the basis behind finding provably minimal sufficient explanations (the main contribution in the paper), I think it would be more convincing to add how this improves interpretability (e.g., visually, quantitatively) and compare it to other non-minimal explanations.", "methods_and_evaluation_criteria": "The proposed method for providing provably sufficient explanations efficiently is well-motivated, especially for safety-critical domains, where having reliable explanations is crucial.\n\nHowever, there is quite a few limitations in the evaluation criteria:\n-\tLimited diversity in benchmark datasets and architecture: the evaluation focuses on MNIST, CIFAR-10 and GTSRB, but lacks a broader range of complex real-world datasets that are more relevant for downstream tasks. \n-\tLack of qualitative comparison of explanations: the paper only evaluates their method against heuristic-based methods quantitatively in Table 2. (e.g., size and efficiency), but does not provide a qualitative comparison. It is unclear whether the generated provably sufficient and minimal explanations are more meaningful semantically or more interpretable than heuristic-based explanations.\n-\tQuantitative evaluation metrics are not enough: The metrics used (e.g. explanation size and time) are not enough from an explainability point of view. Perhaps it would be useful to include quantitative interpretability metrics (e.g., Grid Pointing Game), or any other similar metric, to see how provably sufficient explanations can truly localize class-discriminative features compared to heuristic-based approaches.", "theoretical_claims": "Claim: Alg. 2 is claimed to produce a provably sufficient and minimal explanation as stated in Proposition 5.\n\nIssue:  Going through the proof, I did not find any detail on whether the final explanation is always the globally minimal one, or whether there are multiple minimal explanations (different subsets of input features of same minimal size). If so, this needs to be explicitly clarified.", "experimental_designs_or_analyses": "Yes. I checked the experimental design described in Section 5 (Experimental results) and Appendix B, C and D. \nOne issue is the choice of the perturbation radius $\\epsilon_p$. There is no justification as to why the values were chosen to be 0.01 and 0.001 (L734-L735).", "relation_to_broader_scientific_literature": "This paper contributes to the field of formal explainable artificial intelligence (formal XAI) by leveraging formal verification techniques (abstraction refinement) to provide provably sufficient explanations more efficiently. Unlike heuristic-based methods such as Anchors and SIS, which lack guarantees, and prior verification techniques that are computationally expensive, this method merges neurons to reduce verification complexity while ensuring explanation sufficiency. The paper extends work in neural network verification (e.g., Reluplex, SMT solvers) by refining the abstraction iteratively to find a minimal sufficient explanation. This improves over the verification baseline method (Alg. 1), making formal guarantees less computationally expensive with applications in trustworthy AI and safety-critical domains. By bridging verification, explainability, and scalability, this work contributes to making formal XAI more practical.", "essential_references_not_discussed": "Not that I am aware of.", "other_strengths_and_weaknesses": "Strengths\n-\tThis paper introduces a novel abstraction-refinement approach to efficiently generate provably sufficient explanations for neural networks. The idea is interesting and reasonable: to show that a certain property of a reduced size model (e.g., abstract sufficient explanation) provably holds for the original model, especially for the verification literature which is often limited by scalability\n-\tThe paper is well-organized, and the description of the algorithm and evaluation is clear.\n\nWeaknesses\n-\tCertified radius: there is no evaluation on the effect of changing the perturbation radius on the produced explanations. Clearly a larger radius would be more desired, but there is no elaboration on this part.\n-\tHalting condition: there are no clear evaluation criteria or recommendation of which halting condition (e.g., network size $\\rho$) a user should decide on to improve both the computation time and interpretability. (L090-092, right)", "other_comments_or_suggestions": "no further suggestions", "questions_for_authors": "1.\tHow does the proposed method perform w.r.t different perturbation radii $\\epsilon_p$? I think this is a crucial point to show, as to also justify the choice of the current radii.", "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": "ijivqbMj5W", "reviewer": "Reviewer_jftS", "summary": "This paper aims to improve the scalability of verification algorithms for computing minimal sufficient explanations of neural network predictions. \\\nThe traditional approach iteratively removes input features while preserving the invariance property that the retained set must remain a sufficient explanation. However, this strategy is computationally expensive due to the large number of evaluations required for the neural network. \\\nThe proposed approach introduces an abstraction-refinement technique that enables querying a surrogate, smaller network, thereby reducing the computational cost of verification. The approach progressively increases the network size to ensure convergence to the minimal sufficient explanation set. Notably, the ordering of network sizes corresponds to an ordering of the explanation sets (under the subset relation), allowing formal guarantees such as minimality and sufficiency. \\\nExperiments are conducted on three datasets, MNIST, CIFAR-10 and GTSRB, comparing the proposed method against the traditional formal approach and demonstrating improved efficiency. Additionally, comparisons with heuristic-based methods, including Anchors and SIS, highlight the ability to reduce the computational time gap between formal and heuristic-based approaches while ensuring formal guarantees.\n\n## update after rebuttal\n\nThe authors have addressed my concerns. I think the additional effort put into the rebuttal have enhanced the completeness of the work, in particular with respect to the additional computational analysis of querying surrogate oracles, the analysis of the scalability trend (scaling the size of the original backbone) and the additional experiments to make the analysis consistent across different network architectures (in terms of activation functions). All these experiments should be included in the paper or in the supplementary material. Additionally, the illustrative examples are an interesting addition to improve the clarity of the presentation and increase the accessibility and readability of the paper. These examples should be included in the main paper.\nOverall, I'm happy to increase my score. Congratulations to the authors !", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We appreciate the reviewer's constructive feedback and their acknowledgment of the significance of our work.\n\n**Expanding the scope**\n\nWe thank the reviewer for bringing up this point and will improve its discussion in the final version. We note that while our primary experiments focus on vision classification models, our approach is domain-agnostic and can be applied to other domains. In Appendix D, we provide example experiments in additional domains. For language tasks, we utilized the only language-specific benchmark from the annual neural network verification competition (VNN-COMP [1]), which is based on a medical safety NLP dataset. Certification was achieved over an embedded representation of the input space, ensuring meaning-preserving perturbations. Another example of an expansion can include regression tasks, not just classification. In this case, the provable guarantee would ensure that fixing a subset of features keeps the output prediction within a specified range. We demonstrate this in Appendix D using the real-world, safety-critical Taxi-Net benchmark from Wu et al. (Neurips 2023, [2]). We will enhance our discussion of these extensions, as well as other potential applications, in the body of the final draft.\n\n**Design choices for experimental analysis**\n\nWe selected these specific configurations because they are utilized in the annual neural network verification competition (VNN-COMP [1]). However, in response to the reviewer’s feedback, we will include the additional requested configurations in our final version, with the varying distinct activation functions used for each setting. Our method is also compatible with networks that include residual connections, and we will include an experiment in the final version to highlight this.\n\n**Performance trend and additional quantitative measures**\n\nWe thank the reviewer for these valuable suggestions. We will indeed incorporate additional quantitative measures in the final version, specifically detailing both time per query and time per iteration across our various settings. Due to space limitations in the rebuttal, we provide here only representative results - namely, the average query times in seconds for our different settings in Section E.5.\n\n| Abstraction| MNIST | CIFAR | GTSRB |\n|-------|-------|-------|-------|\n| $\\rho$=0.1 | 0.08 | 0.35 | 1.89  |\n| $\\rho$=0.2 | 0.11 | 0.42 | 3.05  |\n| $\\rho$=0.3 | 0.13 | 0.55 | 4.73  |\n| $\\rho$=0.4 | 0.16 | 0.75 | 7.05  |\n| $\\rho$=0.5 | 0.18 | 0.90 | 9.27  |\n| $\\rho$=0.6 | 0.20 | 0.92 | 11.28 |\n| $\\rho$=0.7 | 0.22 | 0.93 | 12.97 |\n| $\\rho$=0.8 | 0.23 | 0.92 | 14.38 |\n| $\\rho$=0.9 | 0.25 | 0.93 | 15.68 |\n\nWe appreciate the reviewer’s suggestion to examine the scalability trend in our results and will include dedicated experiments in the final version to explore this aspect more thoroughly. Our current findings indicate that increasing model size leads to an increase in overall generation time. At the same time, this also amplifies the relative benefits of the abstraction-refinement strategy, as larger models tend to produce more significant improvements when using coarser abstractions. To illustrate this effect more clearly, we performed an additional experiment based on the “Marabou” benchmark from VNN-COMP [1]. While our original setup focused solely on the “cifar10_large” model, we now include the “cifar10_medium” and “cifar10_small” variants as well. In this experiment, the abstraction-refinement approach showed relative improvements over the standard method, reducing computation time by 136.46 seconds for the small model, 264.18 seconds for the medium model, and 570.39 seconds for the large model. In the final version, we will include additional experiments that vary model sizes while keeping all other parameters constant, to more clearly illustrate this trend.\n\n**Paper clarity improvements**\n\nWe thank the reviewer for the helpful feedback on these points. In the final version, we will include a running example to help clarify our definitions. Due to space limitations, our current detailed explanation of the sufficiency proofs and abstraction appears primarily in Appendix A, with only a concise summary in the main text. As recommended, we will integrate portions of this discussion into the main body and improve the overall presentation of these topics.\n\n[1] First three years of the international verification of neural networks competition (VNN-COMP) (Brix et al., STTT 2023)\n\n[2] Verix: Towards Verified Explainability of Deep Neural Networks (Wu et al., Neurips 2023)", "claims_and_evidence": "Overall, the claims of the paper are clear and reasonable. The idea of leveraging a continuum of progressively larger models to reduce the computation time for verification and improve the scalability is novel and significant.", "methods_and_evaluation_criteria": "Experiments are in my opinion overall convincing, but should be strengthened in terms of their scope. Please refer to the Experimental Designs Or Analyses Section for further details.", "theoretical_claims": "I haven’t checked the proofs for the theory, but all results about sufficiency and minimality are reasonable. There is however a major issue with the clarity of the presentation. Please refer to the Other Strength and Weaknesses section for further details.", "experimental_designs_or_analyses": "Some of the design choices for the experimental analysis are questionable. For instance the backbone network for evaluation uses sigmoid activations for MNIST and GTSRB, and ReLU for CIFAR-10. In order to improve the completeness of the analysis, experiments with both sigmoid and ReLU should be provided in all datasets.\nAdditionally, it would be good to perform an analysis with networks using residual connections, otherwise the scope of validity of the results is quite limited.\n\nIn addition to Figure 4, it would be good to provide a more fine-grained analysis of the computation time, including the number of call evaluations to the neural network surrogates with the corresponding cost in terms of time per call (over iteration/feature).\n\nAdditionally, the analysis doesn’t provide any insight about the “trend” for the scalability, as the size of the original backbones is kept fixed. It would be good to repeat the analysis for smaller models (or larger backbones) and compare with the already provided results.", "relation_to_broader_scientific_literature": "In my opinion, there is good discussion about the related work.", "essential_references_not_discussed": "No", "other_strengths_and_weaknesses": "The paper can be improved in terms of Clarity. Specifically:\n1. It would be good to provide a running example (simple yet non-trivial) to highlight the notion of abstraction and refinement of a network and the corresponding consequence on the explanation set. A lot of definitions and propositions are provided without giving the reader the possibility to gain an intuition.\n2. No sufficient detail about the proving of sufficiency and the way in which networks are abstracted and refined is provided. This hinders the clarity and reproducibility of the work.\n\nOverall, the paper makes an interesting and original contribution. However, the scope of the experimental analysis is rather limited and the paper can improve in terms of clarity. Therefore, I make an initial and cautious judgement, but I'm willing to increase my score.", "other_comments_or_suggestions": "None", "questions_for_authors": "Please refer to the Sections:\n- Experimental Designs Or Analyses\n- Other Strengths And Weaknesses", "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": "LEHZMhz8sJ", "reviewer": "Reviewer_ZvCk", "summary": "The paper tackles the issue of computing verifiably sufficient input-level\nexplanations of neural network predictions.  The proposed algorithm speeds up\nthe computation, which involves several invokations to an exact solver, by\nconstructing a smaller-scale abstraction of the target neural network. The\nabstraction retains sufficiency but may break minimality.  An incremental\nversion of the algorithm thus constructs a sequence of smaller-to-larger\nabstractions until the corresponding explanation is both sufficient and\nminimal.  The experiments primarily focus on evaluating efficiency and size\ngains.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We appreciate the reviewer's constructive feedback and their acknowledgment of the significance of our work.\n\n**Enumeration of minimal sufficient explanations**\n\nWe thank the reviewer for the insightful comment and agree that this is a highly relevant direction, particularly in the context of formal explainable AI. We touch on a related aspect in Appendix C, where we explore how varying feature orderings can influence the explanations generated by our algorithm. Intuitively, running the algorithm over different orderings yields different explanations. A more advanced strategy could start with an initial explanation and iteratively perturb specific features - e.g., replacing features in the explanation with those from its complement - to produce alternative explanations. Another possible direction is to explicitly maximize the divergence between explanations to encourage diversity, for instance by using reverse orderings. While enumerating all possible explanations is computationally intensive, one could potentially leverage the duality with the minimum hitting set (MHS) problem [1] to generate many contrastive explanations and iterate over diverse MHSs. However, such an approach may not scale well to large input domains due to the sheer number of possible contrastive explanations. We appreciate the importance of this point and will incorporate a discussion of it into both the main text and appendix of the final version, and highlight it as an interesting direction for future research.\n\n**Additional weaknesses, comments and suggestions**\n\nWe first acknowledge the weakness pointed out by the reviewer regarding the scalability challenges in producing provably sufficient and minimal explanations for neural networks. However, as both the reviewer and other reviewers have noted, our method represents a significant improvement over prior approaches tackling the same task - offering better computation time, support for larger model sizes, and more concise explanations. We also refer the reviewer to Appendix D, where we demonstrate the generalizability of our method across additional settings. This includes evaluation on a language benchmark derived from a medical NLP dataset, where certification is conducted using meaning-preserving perturbations within an embedded input space, as well as in a regression setting. In the latter, we use the real-world, safety-critical Taxi-Net benchmark to show that fixing certain input features keeps predictions within a target range.\n\nMoreover, we highly appreciate the reviewer’s many thoughtful comments and suggestions, which we will incorporate into the final version and will help us improve the clarity of our work. Regarding Algorithm 2, the counterexample is obtained directly from the verifier but can also be extracted through an external adversarial attack, and we will clarify this accordingly. By a standard algorithm, we refer to a typical greedy approach, which does not incorporate abstraction-refinement, such as the one presented in Algorithm 1 and used in prior works (e.g., the method by Wu et al., NeurIPS 2023 [2]). Importantly, we emphasize that our abstraction-refinement approach is agnostic to the specific technique used to generate explanations and is applicable to any method that derives explanations through multiple certification queries. We agree that this point should be more clearly articulated in the final version.\n\nWe agree with the reviewer’s comment on the importance of improving the discussion of the abstraction methodology in the main text. To enhance clarity, we will relocate portions of the detailed expedition of the abstraction technique from Appendix A to Section 3 and refine the overall discussion accordingly. Additionally, the standard deviation is computed as the square root of the mean of the squared deviations from the average, normalized by dividing by the total number of data points used in each separate experiment. We will also address the notation issues raised and emphasize the non-uniqueness of the generated subsets. While this aspect is partially covered in Appendix C, which discusses different feature orderings, we will ensure it is explicitly highlighted and discussed in the main text as well. Thank you for bringing these valuable points to our attention!\n\nLastly, we appreciate the reviewer’s interesting point regarding the non-monotonicity that is observed in Table 1. This effect is due to the experiment's timeout: without it, the behavior remains monotonic (see Fig. 6). However, with the timeout, larger abstraction configurations can get stuck earlier in the algorithm, causing them to produce larger explanations within the time limit, which explains the observed slight non-monotonic behavior. We will clarify this interesting point in our final version. \n\n[1] From Contrastive to Abductive Explanations and Back Again (Ignatiev et al., KR 2021)\n\n[2] Verix: Towards Verified Explainability of Deep Neural Networks (Wu et al., Neurips 2023)", "claims_and_evidence": "Evidence is quite convincing.\n\nThe main claims are that the explanations output by the proposed algorithm are\nsufficient by construction and small, while the algorithm itself is claimed\nto be faster than the competition.\n\n- Sufficiency: this is supported both by the analysis of Algorithm 2 in page 6\n  and by the results in Table 2: the explanations always achieve 100%\n  sufficiency; the metric used for this assessment appears to be in line with\n  the general notion of sufficiency in the formal explainability literature.\n\n- Size: there appear to be sizeable (!) gains in terms of explanation size\n  in Table 1.\n\n- Speed: the results in Figure 2 indicate a reasonable speed-up on all data sets.\n\nMore generally, the algorithm is tested on three data sets and different neural\nnet architectures.  While the networks are quite small, this is due to\nscalability issues of current NN verification tools, not directly the proposed\nalgorithm.", "methods_and_evaluation_criteria": "Yes.  The setup is very much in line with what's expected from an NN\nverification paper (which slightly differs from what XAI researchers might\nexpect, but this difference is also expected).", "theoretical_claims": "I did not check the correctness of the claims.  They all seem to be intuitively\nreasonable.", "experimental_designs_or_analyses": "Yes, the design is clean.", "relation_to_broader_scientific_literature": "To the best of my knowledge, the contribution is positioned appropriately against existing literature.", "essential_references_not_discussed": "No to my knowledge.", "other_strengths_and_weaknesses": "#STRENGTHS\n\n- Clearly written and structured\n- The motivation is likewise clear\n- Presents a sensible and technically non-trivial solution\n- The experiments are well designed\n- The results provide evidence that the claims hold\n\n#WEAKNESSES\n\n- Even when tackled using nice strategies -- like the proposed algorithm -- finding provably sufficient explanations is still computationally challenging, limiting (at least at present) applicability and significance.", "other_comments_or_suggestions": "- Algorithm 2, line 8: \"obtain counterexample\" - how is this done?\n\n- Section 5: it is not immediately obvious what the \"standard algorithm\" is or\n  whether it is reflective of the SOTA.  Please be clearer about it.\n\n- Table 1: explanation size is not monotonic across $\\rho$'s - this is a bit\n  counterintuitive when compared with the discussion in Section 3.  Could\n  you please clarify what is happening here?\n\n- Figures and Tables: how is the std deviation computed?\n\n- Proofs: it's not necessary to mention that proofs are in Appendix A four times.\n\n- Prop 4: min-suff is technically undefined.\n\n- Prop 2: the notation f \\in f and f \\subset f is not defined.\n\n- It is really unfortunate that the construction by Ladner & Althoff is not\n  explained in more detailed in the main text.\n\n- Minimal sufficient explanations are not unique.  I strongly suggest the\n  authors to discuss uniqueness of the computed explanations in the Limitations\n  paragraph.", "questions_for_authors": "- Could your algorithm help *enumeration* of minimal sufficient explanations too?  If so, it may be worth to point this out, as a number of papers on formal explainability are concerned with this very problem.", "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:

Meta-review: In the context of post-hoc explainability, this paper addresses the challenge of computing minimal sufficient reasons for the classifications made by neural networks. Here, sufficiency is assessed based on the neighborhood of the queried instance. Since solving this problem is generally NP-hard, the authors propose an abstraction-based explanation approach that starts with a coarse approximation of the neural net and iteratively refines this abstraction until a minimal sufficient reason is identified. The authors demonstrate the correctness of their approach through various results and validate its practical performance, measured in terms of runtime and explanation sizes, across several benchmarks.

The average score for this paper exceeds the acceptance threshold, with reviewers providing scores that range from "weak accept" to "accept." All reviewers acknowledge the novelty of this abstraction approach, noting the intriguing connections it establishes between formal explainability and model abstraction. Furthermore, revised reviews indicate that the authors effectively addressed concerns regarding the scope of the study, the experimental design choices, and the need for additional statistical tests. For these reasons, I recommend accepting the paper.

In a revised version, I suggest incorporating constructive feedback from the rebuttal phase to further enhance the paper and address the concerns raised. Additionally, adding comments about the runtime complexity of the neuron-merging algorithm in Section 3 would provide valuable insights into the feasibility of this approach.
Decision: Accept (poster)