VeriX: Towards Verified Explainability of Deep Neural Networks
Authors: Min Wu
Haoze Wu
Clark Barrett
Venue: NeurIPS 2023 poster (2023)
Keywords: trustworthy machine learning
deep neural networks
explainability
interpretability
formal methods
automated verification
TL;DR: We present VeriX (Verified Explainability), a system for producing optimal robust explanations and generating counterfactuals along decision boundaries of machine learning models.

Abstract: We present **VeriX** (**Veri**fied e**X**plainability), a system for producing *optimal robust explanations* and generating *counterfactuals* along decision boundaries of machine learning models. We build such explanations and counterfactuals iteratively using constraint solving techniques and a heuristic based on feature-level sensitivity ranking. We evaluate our method on image recognition benchmarks and a real-world scenario of autonomous aircraft taxiing.

VERIX: Towards Verified Explainability of Deep Neural Networks
Min Wu
Haoze Wu
Department of Computer Science Stanford University
Department of Computer Science
Stanford University
minwuêcs. wtwp://wssssttaooooooooooooooome lanford.edu edu
haozewuêcs. srnrzeem@@sssstffoddddoo stanford.ed
Clark Barrett
Department of Computer Science
Stanford University
barrettêcs .eareeessssstttttt stw.ford......om edu
Abstract
We present VERIX (VERIfied explainability), a system for producing optimal robust explanations and generating counterfactuals along decision boundaries of machine learning models. We build such explanations and counterfactuals iteratively using constraint solving techniques and heuristic based feature- level sensitivity ranking. We evaluate our method on image recognition benchmarks and real-world scenario of autonomous aircraft taxiing.
Introduction
Broad deployment of artificial intelligence (AD) systems in safety-critical domains, such tonomous driving [18] and healthcare [63], necessitates the development of approaches for trust- worthy AL. One key ingredient for trustworthiness is explainability: the ability for AI system to communicate the reasons for its behavior terms that humans can understand.
Early work on explainable Al includes well-known model-agnostic explainers which produce expla- nations that remain valid for nearby inputs in feature space. In particular, LIME (42 and SHAP (38] learn simple, and thus interpretable, models locally around given input. Following LIME, work on Anchors 43] attempts to identify a subset of such input explanations that are (almost) sufficient to ensure the corresponding output value. Such approaches can produce explanations efficiently, however, they do not provide any formal guarantces and are thus inappropriate for use high-risk scenarios. For instance, in healthcare. if diagnosis model used by dermatologist has explanation claiming that depends only on a patient's 's skin lesions (such as "plaque". "pustule", and "ulcer" in (10), yet in actuality, patients with similar such lesions but different skin tones ("Fitzpatrick I-11, IIIIV, V-VI" [9) receive dissimilar diagnoses, then the explanation is not only wrong, but may actually mask bias in the model. Another drawback of model-agnostic approaches is that they often depend on access to training data, which may not always be available (perhaps due to privacy concerns). And even if available, distribution shift can compromise the results.
Recent efforts towards formal explainable [40] aim to compute rigorously defined explanations that can guarantee soundness, in the sense that fixing certain input features is sufficient ensure the invariance of a model's prediction. However, their work only considers unbounded perturbations, which may be too course-grained to be useful (for other limitations, see Section 5). To mitigate those brawbacks, (33 bring in two types of bounded perturbations, c-ball and k--N box closure, and show how to compute optimal robust explanations with respect to these perturbations for natural
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

2
2
(a) Original "2" (b) Segmentation
(c) VERIX
(d) "2" into "7" (c) "2" into "0"
(f) "2" into "3"
Figure 1: Intuition for our VERIX approach: (a) An MNIST handwritten "2"; (b) Segmentation of "2" into 3 partitions; (c) Our VERIX explanation (green pixels) of "2"; (d)(e)() Masking white pixels or whitening black pixels may turn "2" into possible counterfactuals.
language processing (NLP) models. K-NN box closure essentially chooses a finite set of the k closest tokens for each word in a text sample, so the perturbation space is intrinsically discrete; on the other hand, c-ball perturbations provide a way to handle a continuous word embedding (though the authors of 333 suggest that these may be more cumbersome in NLP applications and focus k--N box perturbations in their experimental results).
In this paper, we present VERIX (VERIfied explainability), tool for producing optimul robust explanations and generating counterfactuals along decision boundaries of deep neural networks. Our contributions can be summarized as follows.
We utilize constraint solving techniques to compute robust and optimal explanations with provable guarantees against infimite and continuous perturbations in the input space.
We bring a feature-level sensitivity traversal into the framework to efficiently approximate global optima, which improves scalability for high-diment high-dimensional inputs and large models.
We note for the first time the relationship between our explanations and counterfuctuals, and show how to compute such counterfactuals automatically at no additional cost.
We provide an extensive evaluation on a variety of perception models, including safety- critical real-world autonomous aircraft taxiing application.
We start by providing intuition for our VERIX approach by analyzing an example explanation in Figure This explanation is generated for fully colnecco model trained on the MNIST dataset. Model-agnostic explainers such as Anchors
rely on partitioning an image into a disjoint set of segments and then selecting the most prominent segment(s). Figure Tb shows "2" divided into parts using k-means clustering (37]. Based on this segmentation, the purple and yellow parts would be chosen for the explanation, suggesting that the model largely relies on these segments to make its decision. This also matches our intuition, as a human would immediately identify these pixels as containing information and disregard the background. However, does this mean it is enough to focus on the salient features when explaining a classifier's prediction? Not necessarily. VERIX'S explanation is highlighted in green in Figure Ic It demonstrates that whatever prominent is important but what is absent in the backgroumd also matters. We observe that VERIX not only marks those white pixels forming the silhouette of "2" but also includes some background pixels that might affect the prediction if changed. For instance, neglecting the bottom white pixels may lead to misclassification as "7"; meanwhile, the classifier also needs to check if the pixels along the left and in the middle are not white to make sure it is not "O" or "3". While Figures [d]] [e] and TT are simply illustrative to provide intuition about why different parts of the explanation may be present, we remark that explanations from VERIX are produced automatically and deterministically.
4
VERIX: Verified eXplainability
Let f be a neural network and x a d-dimensional input vector of features (x) .x.)).)))) We use O(x), or simply Ô, when the context is clear, denote its set of feature indices {I....,d} .d. We write X where A C ((x) to denote only those features indexed by indices in A. We denote model prediction as f(x = c, where is a single quantity in regression or a label among others (c E C) in classification. For the latter, we use fx( to denote the confidence value (pre- or post- softmax) of classifying as c, i.e., [x) arg max fc Depending on different application domains, x can be an image consisting of dl pixels as in our case or text comprising d words as in NLP [3 In this paper, we focus on perception models. This has the additional benefit that explanations this context are oeffiillsstratiee and thus casier to understand.

---

2.1 Optimal robust explanations
Existing work such as abductive explanations (26. prime implicants [45] and sufficient reasons define a formal explanation as a minimal subset of input features that are responsible for model's decision, in the sense that any possible perturbations on the rest features will never change prediction. Building this, [3 introduces bounded perturbations and computes cdistance-restricted such explanations for NLP models. Our definition closely follows [33] except: (1) rather than minimizing an arbitrary cost function, consider the uniform case (i.e., the same cost is assigned to each feature) so as to compute the smallest number of features; (2) we focus on continuous e-ball perturbations not discrete k-NN box closure; (3) we allow for bounded variation (parameterized by 6) in the output to accommodate both classification (set to 0) and regression (6 could be some pre-defined hyper--arameee quantifying the allowable output change) whilst [33] focuses sentiment analysis (i.e., binary classification).
Definition 2.1 (Optimal Robust Explanation). Given a neural network S. an input x, a manipulation magnitude and discrepancy 8, robust explanation with respect to norm p E 21, oo) is a set of input features x such that = O(x) A, then
x B'
|
x
SE (f()) f(x') 6,
(1)
where xB' is some perturbation on features xB and x' is the input variant combining x and xB' In particular, we say that the robust explanation x is optimal if
X 3x xx.
| @ x)
+ x3)
SEA - [(xx) -(x))
(2)
where X' is some perturbation of and @ denotes concatenation of two features.
We refer to xB as the irrelevant features. Intuitively, perturbations bounded by imposed upon the irrelevant features xB will never change prediction, as shown by the small blue "+" variants in Figure 2 Moreover, each feature x (and their combinations) in the optimal expla- nation x be perturbed. together with the irrelevant features, to go beyond the decision boundary, i.c., the orange "+" variants. We mention two special cases: is c-robust, then all features are irrelevant, i.e., any
decision boundary
B'
A'
counterfactral
B
if (f)
counterfictual
A = 0. meaning there is valid explanation e-perturbation does not affect the prediction at all (in other words, larger is required to get a meaningful explanation); (2) if perturbing any feature in input x can change the prediction, then A O(x), meaning the entire input is an explanation.
X
nobust
optimal
A'
original
Figure 2: Graphical illustration of VERIX. Each gray square denotes the original input (big blue "+") or a variant (smaller "+"). Variants (blue "+") that do not change the explanation
We remark that definition of optimality is local in that computes a minimal subset of features. An in- teresting problem would be to find a globally optimal explanation, i.e., the smallest (fewest features) among all possible local optima, also known the cardinality- minimal explanation [26]. Approaches (such as those based minimum hitting sets [33 4 for computing such global optima are often too computationally diffi-
(green circle) are guaran- teed to lie the same side of the decision boundary. Counterfactuals (orange "+") with perturbed explanations A' are classi- fied differently.
cult converge for large models and high-dimensiona inputs as in our case. Therefore, we propose a tractable heuristic (Section 3.3) that approximates the ideal and works fairly well in practice.
2.2 Counterfactuals along decision boundary
While there are infinitely many variants the input space, we are particularly interested in those that lie along the decision boundary of model. Figure 2 shows several pairs of variants (blue and orange "+") connected by red dotted lines. Fach pair has the property that the blue variant has the same prediction as the original input whereas the orange variant, obtained by further perturbing one
3

---

Table 1: Evolving index set A for explanation x and index B for irrelevant features x
along
reasoning result (True / False) of the CHECK sub- cul-procedure when processing Example 3.1
feature
A
B
B
reasoner
irrelevant features x
explanation x
BU
True
x
[1}
BU (2)
True
x x
x²
[1,2]
BU [3)
True
x x2xxx
X
[1,2,3]
BU [U]
xx x(2)
(x
X
[4]
[1,2,3]
BU
False
(x', (e.x",xx xx)
X
(4,5)
[1,2,3]
BU [6)
True
(x" (1.x2-xx,,00
Cx (x
X²
(4.5)
[1,2,3.6]
BU [7]
True
(x xx9)
X
(4,5)
(1,2,3,6,7)
BU (8)
False
(x x2 18
X²
(4,5,8)
6,,2,36677
BU (9)
single feature x in the optimal explanation x (together with the irrelevant features, i.e., x x' Equation ( produces different prediction. We note that these orange variants are essentially counterfactual explanations [5]]: each is a concrete example of a nearby point in the input space illustrating one way to change the model prediction. We emphasize that our focus this paper is to compute explanations of the form in Definition 2.1] but it is noteworthy that these counterfactuals generated automatically and at no additional cost during the computation. In fact, we end up with distinct counterfactual for each feature in explanation, comprehensive review counterfactual explanations and their uses).
will see below (see (20 [0 for
Computing VERIX explanations by constraint solving
Before presenting the VERIX algorithm (Algorithm detail, we first illustrate it via simple example.
Example 3.1 (VERIX Computation). Suppose is input as in Figure 3 and we have
x
x²
x
x²
2
with 9 features (x' .x'....."" x²)) classification network f. perturbation magnitude e, and are using = co. The outer loop of the algorithm traverses the input features. For simplicity, assume the order of the traversal is from x to x Both the explanation index set A and the irrelevant set B are initialized D. At each iteration, VERIX decides whether to add the index i to A or B. The evolution of the index sets is shown Table Concretely, when i 1, VERIX formulates pre-condition which spec- ifies that x" can be perturbed by e while the other features remain unchanged. An automated reasoner is then invoked to check whether the pre-condition logically implics the post- condition (in this case, fxx) f(x), meaning the prediction the same after perturbation). Suppose the reasoner returns True; then, c-perturbation on x can alter the prediction. Following Equation of Definition 2.1 we thus add x' to the irrelevant features B Figure top left, shows visu- alization of this. VERIX next moves on to x². This time the precondition allows e-perturbations
x
x
x
x
x
x
X
x-
x7
x
x7
x
2
x²
x
x²
x²
x3
x²
x2
x
x
x
x
x3
x
x
2
x
x²
x
x2
x
x
x
x
x
x²
x²
x
x
x
x
x²
x
x²
x
x
x
Figure 3: Computing VERIX expla- nation by constraint solving for a sim- ple input x (x'...,,X) ......))). Green is the optimal robust explanation xA, gray denotes irrelevant features B
both x and x² while keeping the other features unchanged. The post-condition remains the same. Suppose the reasoner returns True again we then add x to xB (Figure top middle). Following similar steps, we add x" xB (Figure top right). When comes to we allow e-perturbations for (x) x² 2x'",x² while the other features are fixed. Suppose this time the reasoner returns False there exists counterexample (this counterexample is the counterfactual for feature x*) that violates fxx f(x), i.e., the prediction can be different. Then, according Equation 2 of Definition 2.1 we add x² the optimal explanation x (shown as green in Figure 3 middle left). The computation continues until all the input features are visited. Eventually, we have x = (x1 x,,,xxxx x) (Figure 3 bottom right), which means that, the features in the explanation are fixed, the model's prediction invariant to any possible p-prturrattion on the other features. Additionally, for each of the features x we have a counterfactual that demonstrates
how that feature can be altered (together with irrelevant features) to change the prediction.

---

3.1 Building optimal robust explanations and counterfactuals iteratively
We now formally describe our VERIX methodology. which exploits an automated reasoning engine for neural network verification as a black-box sub-procedure. We assume the reasoner takes as inputs a network f and a specification
Din (x) 7 Dout (c)
where X are variables representing the network inputs and è are expressions representing the network outputs. Pin (x) and (c) are formulas. We use X denote the variable corresponding to the 7th feature. The reasoner checks whether a specification holds on a network.
Inspired by the deletion-based method [8] we propose Algorithm I in which the VERIX procedure takes input net- work I and an input x = (x-,.. x²). It outputs optimal explanation x² with respect to perturbation magnitude e, dis- tance metric p. and discrepancy 6. also outputs a set of counterfactuals, one for each feature in xA The procedure main- tains three sets, A, B, and C, throughout: A comprises feature indices forming the explanation; B includes feature indices that can excluded from the explanation;
Algorithm VERIX (VERIfied explainability)
Input: neural network f and input x = (x',...., Parameter: e-perturbation, norm p. and discrepancy 8 Output: optimal robust explanation xA, counterfactuals C for each X x^
1: function VERIX(J, x)
2:
A, C + 0, 0
3:
c c f(x)
4:
e f(x)
5:
π + TRAVERSALORDER(2)
and C is the set of counterfactuals. Re-
for in x do
call that xB denotes the irrelevant features
7:
B + BU
(i.e., perturbing xB while leaving x un- changed never changes the prediction). To start with, these sets are initialized to 0 (Line D. and the prediction for input x recorded as c, for which we remark that c may or may not be an accurate prediction 12:
Ø B - -X B (c)
8:
H Φ A (2 ( = x81B*)
9:
10:
(HOLD, m) CHECK (1,
c2-cl
5)
11:
HOLD then B + B
else A + A AU return (x C)
according to the ground truth VERIX 13:
generates an explanation regardless. Over-
all, the procedure examines every feature
x" in x according to TRAVERSAL.RDEE (Line 5) to determine whether i can be added to B or must belong A. The traversal order can significantly affect the size and shape of the explanation. We propose a heuristic for computing traversal order that aims to produce small explanations in Section 3.3 (in Example 33. sequential order is used for ease of explanation). For each we compute Ø, formula that encodes two conditions: (i) the current x" and xB are allowed to be perturbed by at most (Line 8 and (ii) the rest of the features are fixed (Line 9). The property that we check is that ó implies |é - c| < 8 (Line 10). denoting prediction invariance.
An automated reasoning sub-procedure CHECK is deployed examine whether network f the specification & > Jé f2-e cl S ō holds (Line 10 i.e., whether perturbing the current x and irrelevant features while fixing the rest ensures consistent prediction. It returns (True, m) if this is the case (where m is arbitrary) and (False, m)) if not, where m is a concrete input falsifying the formula. In practice, this CHICKK can be instantiated with an off-the-shelf neural network verification tool [46 41 31 (6 21 If HOLD is True, i is added to the irrelevant set B (Line IT]. Otherwise, i is added to the explanation index set A (Line 12). which conceptually indicates that x contributes to the explanation of the prediction (since feature indices in B have already been proven to not affect prediction). In other words, an e-perturbation that includes the irrelevant features current x" can breach the decision boundary of f. This fact is represented by the counterexample m, which represents the counterfactua| for x" and is added to the set C' of counterfactuals. The procedure continues until all feature indices in x are traversed and placed into one of the two disjoint sets A and B. At the end, x is returned as the optimal explanation and C returned as the set of counterfactuals.
well as the
Properties of counterfactuals such as actionability 20 can be addressed by using appropriate to ensure that the counterexamples returned by verifiers will always be from the input data distribution.
5

---

3.2 Soundness and optimality of explanations
To ensure the VERIX procedure returns robust explanation, we require that CHECK is sound, i.e. the solver returns True only if the specification actually holds. For the robust explanation to be optimal, CHECK also needs to be complete, i.e., the solver always returns True if the specification holds. We can incorporate various existing reasoners as the CHECK sub-routine. We note that an incomplete reasoner (the solver may return Unknown) does not undermine the soundness of our approach, though it does affect optimality (the produced explanations may be larger than necessary).
Lemma 3.2. If the CHECK sub-procedure is sound, then, at the end of each for-loop ileration (Lines 7 12 in Algorithm 7 the irrelevant set of indices B satisfies
(|
B
x
11, S 5e) A (x B x B) = jē cl S 6.
(4)
Intuitively, any e-perturbation imposed upon all irrelevant features when fixing the others will always keep the prediction consistent, i.e., the infinite number of input variants (indicated with small blue "4" Figure 2) will always remain within the decision boundary. We include rigorous proofs for Lemma 3.2 and Theorems an in Appendix A Soundness directly follows from Lemma 3.2
Theorem 3.3 (Soundness). If the CHECK sub-procedure is sound, then the value x returned by Algorithm 7 is a robust explanation - this satisfies Equation 7 of Definition 22.
Theorem 3.4 (Optimality). If the CHECK sub-procedure is sound and complete, then the robust explanation A returned by Algorithm 7 is optimal - this satisfies Equation (2 of Definition 2.1
Intuitively, optimality holds because if it is not possible for an e-perturbation on some feature x" in explanation x to change the prediction, then it will be added to the irrelevant features xB3 when feature x" is considered during the execution of Algorithm
Proposition 3.5 (Complexity). Given d-dimensional input x and a network S. the complexity of computing an optimal robust explanation using the VERIX algorithm O(d P(f)), where P(f) is the cost of checking specification (of the form in Equation 3 over f.
An optimal explanation can be achieved from one traversal of input features as we are computing the local optima. f is piecewise- hiccewise-linear, checking a specification over f is NP-complete [30.. We remark that such complexity analysis is closely related to that of the deletion- -bsedd method [ here we particularly focus on how network / and d-dimensional input would affect the complexity of computing an optimal robust explanation.
3.3 Feature-level sensitivity traversal
While Example 3.1 used simple sequential order for illustration purpose, we introduce heuristic based on feature-level sensitivity, inspired by the occlusion method (64), to produce actual traversals. Definition 3.6 (Feature-Level Sensitivity). Given an input x = (x)...., xd) and a network f. the feature-level sensitivity (in classification for a label e or in regression for a single quantity) for feature x" with respect to transformation T is
sensitivity( [(o())) - f(o(('),
(5)
where x' is with x replaced by T(x').
Typical transformations include deletion (T(x) 0) and reversal (T(x) = X X. where X is the upper bound for feature x). Intuitively, we measure how sensitive (in terms of an increase or decrease) model's confidence is to each individual feature. Given sensitivity values with respect some transformation, we rank the feature indices into a traversal order from least to most sensitive.
Experimental results
We have implemented the VERIX algorithm in Python, using the Marabou neural network verification
tool BI implement the CHECK proceduree of Algorithm [] (Line TOP. The VERIX code is available at /tttp:://iithu
com MewuraaNeeooorerr11 wwt.:riiiiaaaiiiiiiiiaaoaooiciet /eeeiin////iiii We trained fully- connected and convolutional networks on the MNIST [34], GTSRB [47], and TaxiNet [9] datasets for classification and regression tasks. Model specifications are in Appendix D Experiments were performed on a workstation equipped with AMD Ryzen? 7 5700G CPUs running Fedora 37. We set time limit of 300 seconds for each CHECK call.

---

50
(a) "keep right, 50 mph, road work, passing"
(b) Handwritten digit "1", not "8", not "5", not "2"
Figure 4: Optimal robust explanations (green) from VERIX on GTSRB (left) and MNIST (right)
images. (b) Pixels in yellow are those in the explanation to rule out different counterfactuals.
4.1 Example explanations for image recognition benchmarks
Figure 4 shows examples of VERIX explanations for GTSRB and MNIST images. The convolutional model trained GTSRB and fully-connected model on MNIST are in Appendix [ Tables and Aligning with our intuition, VERIX can distinguish the traffic signs (no matter a circle, a triangle, or square Figure 6aa) from their surroundings well; the explanations focus on the actual contents within the signs, e.g., the right arrow denoting "keep right" and the numher 50 as in "50 mph". Interestingly, for traffic signs consisting of irregular dark shapes on a white background such as "road work" and "no passing", VERIX discovers that the white background contains the essential features. We observe that MNIST explanations for the fully-connected model are in general more scattered around the background because the network relies on the non-existence of white pixels to rule out different counterfactuals (Figure/4b)st) shows which pixels the explanation have associated counterfactuals with predictions of "8", "5", and "2", respectively), whereas GTSRB explanations for the convolutional model can safely disregard the surrounding pixels outside the traffic signs.
4.2 Visualization of the effect of varying perturbation magnitude
key parameter of VERIX is the perturbation mag- nitude When e varied, the irrelevant features change accordingly. Figure visualizes this, show- ing how the irrelevant features change when is tightened from 100% to 10% and further to 5%. As c decreases, more pixels become irrelevant. Intu- itively, the VERIX explanation helps reveal how the network classifies this image as "0". The deep blue pixels are those that are irrelevant with 100%. Light blue pixels are more sensitive, allowing per- turbations of only 10%. The light yellow pixels represent 5%, and bright yellow are pixels that can- not even be perturbed 5% without changing the prediction. The resulting pattern is roughly consis- tent with our intuition, as the shape of the "0" can be seen embedded in the explanation.
O Diciit
(a) MNIST "O" (b) 0.1 (c) 0.05
Figure 5: Expansion of the irrelevant pixels when perturbation magnitude decreases from 100% to 10% and further to 5% (from deep blue light yellow). Each brighter color denotes the pixels added when moving to the next smaller c, e.g., 100%, 90%, 80% and
We remark that determining a suitable magnitude is non-trivial because if is too loose, explanations may too conservative, allowing very few pixels to change. On the other hand, if e is too small, nearly the whole set of pixels could become irrelevant. For instance, in Figure if we set to 1% then all pixels become irrelevant the classifier's prediction robust to 1 The "color map" we propose makes it possible to visualize not only the explanation but also how it varies with e. The user then has the freedom to pick specific depending on their application.
4.3 Sensitivity random traversal to generate explanations
To show the advantage of the feature-level sensitivity traversal, Figure | compares VERIX expla- nations using sensitivity-but based and random traversals. Sensitivity, as shown in the heatmaps of Figures 6a and (6) prioritizes pixels that have more influence on the network's 's decision, whereas a random ranking is simply shuffling of the pixels. We mention that, to compute the sensitivity, we used pixel deletion T(x) = 0 for GTSRB and reversal T(x) background pixels of MNIST images may have little effect as they often have zero values). We observe that the sensitivity traversal generates much more sensible explanations. In Figure 6c
for MNIST (deleting

---

(a) GTSRB "priority road", sensitivity, explanations.
(b) MNIST "O", sensitivity, explanations.
index MNIST images
random
random
random
random
random
senstivity
random
random
100
200
300
400
500
(c) Sensitivity vs. random traversals explanation size (number pixels).
Figure 6: Comparing VERIX explanations from sensitivity and random traversals. (a)(b) 1st column: original image: 2nd column: sensitivity heatmap; 3rd and 4th columns: explanations from sensitivity (green) and random (red) traversals. (c) Each blue triangle is unique explanation size from sensitivity ranking, and each set of circles shows explanation sizes from 100 random rankings.
Original, VERIX, Anchors, misclassified "yield" Figure 7: Comparing VERIX (green) to Anchors (red) on two different versions of "keep right" traffic sign from the GTSRB dataset, with strong light in the background and one without.
(a) Original, VERIX, Anchors, segmentation
compare explanation sizes for the first 10 images avoid potential selection bias) of the MNIST test set. For each image, we show 100 explanations from random traversal compared to the deterministic explanation from sensitivity traversal. We observe that the latter is almost always smaller, often significantly so, suggesting that sensitivity-baser traversals are a reasonable heuristic for attempting approach globally optimal explanations.
4.4 VERIX vs. existing approaches
We compare VERIX with Anchors 43 Figure 7 both approaches applied to two different "keep right" traffic signs. Anchors performs image segmentation and selects set of the segments as the explanation, making its explanations heavily dependent on the quality of the segmentation. For instance, distractions such as strong light in the background may compromise the segments (Figure 7 last column) thus resulting in less fess-than-ideal explanations, c.g., the top right region of the anchor (red) is outside the actual traffic sign. Instead, VERIX utilizes the model compute the sensitivity traversal, often leading to more reasonable explanations. Anchors is also not designed to provide formal guarantees. In fact, replacing the background of an anchor explanation used by the original paper [43 to justify "almost" guarantee can change the classification. For example, the last column Figure 7b is classified as "yield" with confidence 99.92%. We conducted quantitative shown in Table under "robust wrt # perturbations" When quantifying the robustness of Anchors, we generate 100 explanations for 100 MNIST and 100 GTSRB images separately, and impose 10, 100, 500, 1000 perturbations overlapping with other images the same dataset. If the prediction remains unchanged, then the explanation is robust against these perturbations. We notice that the robustness of Anchors decreases quickly when the number of perturbations increases, and when imposing 1000 perturbations per image, only 37 MNIST and 15 GTSRB explanations out of 100 robust. This not done for LIME, since it would be unfair to LIME as it does not have robustness as a primary goal. In contrast, VERIX provides provable robustness guarantees against any e-perturbations in the input space.
evaluation on the robustness of explanations,
each explanation by
Two key metrics for evaluating the quality of explanation are the size and the generation time. Table 2 shows that overall, VERIX produces much smaller explanations than Anchors and LIME but

---

Table 2: VERIX vs. existing approaches, showing average explanation size (number of pixels), generation time (seconds), and an empirical evaluation of the robustness of the produced explanations against perturbations. VERIX, is set to 5% for MNIST and 0.5% for GTSRB.
MNIST
GTSRB robust wrt perturbations
size
time
robust wrt # perturbations
size
time
sensitivity
180.6
174.77
100%
357.0
853.91
100%
VERIX
random
294.2
157.47
100%
383.5
814.18
100%
10
100
500
1000
10
100
500
1000
Anchors
494.9
13.46
557.7
26.15
85%
52%
40%
37%
72%
23%
16%
15%
LIME
432.8
9.03
452.9
7.85
(a) 3.94 (3.91) m (b) 5.09 (4.97) m (c) 3.32 (3.38) m (d) 1.75 (1.55) m (e) 1.58 (1.60) m (1) 3.88 (4.07) m
Figure 8: VERIX applied the TaxiNet dataset each column includes sampled camera view (top), its VERIX explanation (bottom), and the cross-track estimate of the form "actual (estimate) meters".
takes much longer (our limitation) to perform the computation necessary to ensure formal guarantees this thus provides trade-off between time and quality. Table Table_aasoo shows that sensitivity traversal produces significantly smaller sizes than its random counterpart with only a modest overhead in time.
4.5 Deployment in vision-based autonomous aireraft taxiing
We also applied VERIX to the real-world safety-critical aircraft taxiing scenario [29] shown in Figure [ The vision-basee autonomous taxing system needs to make sure the aircraft stays on the taxiway utilizing only pictures taken from the camera on the right wing. The task is to evaluate the cross- track position of the aircraft that controller can adjust its position accordingly. To achieve this, a regression model is used that takes a picture input and produces an estimate of the current position. preprocessing step crops out the sky and aireraft nose, keeping the crucial taxiway region (in the red box). This is then downsampled into a gray-scale image of size 27 x 54 pixels. We label each image with its corresponding lateral distance to the runway centerline together with the taxiway heading angle. We trained fully-connecter regression network on this dataset, referred to as the TaxiNet model (Appendix D.3 Table [T], to predict the aircraft's ''s cross-track distance.
Figure 9: An autonomous aircraft taxi- ing scenario (2). Pictures taken from the camera fixed on the right wing are cropped (red box) and downsampled.
Figure Sequre@exhie exhibits VERIX applied to the TaxiNet dataset, including a variety of taxiway images with different heading angles and number of lanes. For each taxiway, we show its VERIX explanation accompanied by the cross-track estimate. We observe that the model is capable of detecting the more remote line- its contour clearly marked in green. Mcanwhile, the model is mainly focused on the centerline (especially in Figures (b) [d Se and 8f. which makes sense as it needs to measure how far the aircraft has deviated from the center. Interestingly, while we intuitively might assume that the model would focus on the white lanes and discard the rest, VERIX shows that the bottom middle region is also crucial to the explanation (e.g., as shown in Figures [a and S&c.. This is because the model must take into account the presence and absence of the centerline. This is in fact in consistent with our observations about the black background in MNIST images (Figure D). We used e = 5% for these explanations, which suggests that for modest perturbations (e.g., brightness change due to different weather conditions) the predicted cross-track estimate will remain within an acceptable discrepancy, and taxiing will not be compromised.

---

Table Complete vs. incomplete verification, showing average explanation size (number of pixels) is set to 5% for MNIST and 0.5% for GTSRB.
and generation time (seconds). As in Table 2
MNIST
GTSRB
complete
incomplete
complete
incomplete
size
time
size
time
size
size
time
VERIX
sensitivity
180.6
174.77
330.8
106. 11
357.0
853.91
385.2
858.39
random
294.2
157.47
467.4
100.19
383.5
814.18
400.2
816.38
4.6
Using sound but incomplete analysis as the CHECK sub-procedure
We also evaluate using sound but incomplete analysis, such as DeepPoly [46). as the CHECK sub- procedure of Algorithm T
In Table we report the quantitative comparison.
We observe that, in general, explanations are larger when using incomplete analysis, but have shorter generation times. other words, there a trade-off between complete and incomplete analyses with respect to explanation size and generation time. This makes sense as the DeepPoly analysis deploys bound propagation without complete search. so when the verifier returns Unknown on a certain feature (Line 10 of Algorithm] I. it is unknown whether perturbing this feature (together with the current irrelevant set B) can or cannot change the model's prediction. Therefore, such features are put into the explanation set A, as only e-robust features are put into the irrelevant set B. This results in larger explanations. We re-emphasize that such explanations are no longer locally minimal, but they are still sound E-perturbations on the irrelevant features will definitely not alter the prediction. Another observation is that on MNIST, the discrepancy between explanations (size and time) from complete and incomplete verifiers is more pronounced than the discrepancy on GTSRB, This is because here we set e to 5% for MNIST and to 0.5% for GTSRB. So when generating explanations on MNIST, complete search is often required for a precise answer due to the larger value, whereas GTSRB, bound propagation is often enough due to the small c, and thus complete search is not always needed.
Due to space limitations, additional analyses of runtime performance and scalability for both complete and incomplete verifiers are included in Appendix B
Related work
Farlier work on formal explanations 40 has the following limitations. First, in terms of scala- bility, they can only handle simple machine learning models such as naive Bayes classifiers [39], random forests [28 6), decision trees (27), and boosted trees (24 25). In particular, [26) addresses networks but with very simple structure (e.g., one hidden layer of 15 or 20 neurons to distinguish two MNIST digits). In contrast, VERIX works with models applicable to real-world safety safety-critical criitial scenarios. Second, the size of explanations can be unnecessarily large. As workaround, approximate explanations [52 [53] are proposed
generalization provide probabilistic (thus compromised) guarantees of prediction invariance. VERIX, by using feature- sensitivity ranking, produces reasonably-sized explanations with rigorous guarantees. Third, these formal explanations allow any possible inpus in feature space, which is not necessary or realistic. For this, [3 brings in bounded perturbations for NLP models but their k-NN box closure essentially chooses finite set of the k closest tokens for each word so the perturbation space is intrinsically discrete. In other words, their method will scale our high-dimensional image inputs with infinite perturbations. One the other hand, those model-agnostic feature selection methods such as Anchors [3) and LIME [22 can work with large networks, however, they cannot provide strong guarantees like our approach can. brief survey of work in the general area of neural network verification appears in Appendix C
6 Conclusions and future work
We have presented the VERIX framework for computing optimal robust explanations and counterfac- tuals along the decision boundary. Our approach provides provable guarantees against infinite and continuous perturbations. A possible future direction is generalizing to other crucial properties such as fairness. Recall the diagnosis model in Section [] our approach can discover potential bias (if exists) by including skin tones ("Fitzpatrick I-I1, M-IV, V-VI" [19] in the produced explanation; then, a dermatologist could better interpret whether the model is producing a fair and unbiased result.
10

---

Acknowledgments
This work was supported in part by NSF grant 2211505, the Stanford Center for AI Safety, and the Stanford Center for Automated Reasoning.
References
[1] Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, lan Goodfellow, Andrew Harp. Geoffrey Irving, Michael Isard. Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dandelion Mané, Rajat Monga, Sherry Moore, Derek Murray, Chris Olah, Mike Schuster, Jonathon Shlens, Benoit Steiner, Ilya Sutskever, Kunal Talwar, Paul Tucker, Vincent Vanhoucke, Vijay Vasudevan, Fernanda Viégas, Oriol Vinyals, Pete Warden, Martin Wattenberg, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. TensorFlow: Large- scale machine learning heterogeneous systems, 2015. Software available from tensorflow.org.
[2] Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat Chaudhuri. Optimization and abstrac- tion: a synergistic approach for analyzing neural network robustness. Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 731-744, 2019.
[3] Stanley Bak, Changliu Liu, Taylor T. Johnson, Christopher Brix, and Mark Müller. The 3rd international verification of neural networks competition (ynn-comp), 2022. httpp::/ssiit //sites
google com honn/ieewvvnnn222
[4] Shahaf Bassan and Guy Katz. Towards formal approximated minimal explanations of neural networks. arXiv preprint arXiv:2210.13915, 2022.
[5] Elena Botoeva, Panagiotis Kouvaros, Jan Krongvist, Alessio Lomuscio, and Ruth Misener. Efficient verification of relu-based neural networks via dependency analysis. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 3291-3299, 2020.
[6] Ryma Boumazouza, Fahima Cheikh-Alili, Bertrand Mazure, and Karim Tabia. Asteryx: A agnes-ag sat-based approach for symbolic and score-based explanations. In Proceedings of the 30th ACM International Conference on Information & Knowledge Management, pages 129, 2021.
[7] Rudy Bunel, Ilker Turkaslan. Philip HS Torr, M Pawan Kumar, Jingyue Lu, and Pushmeet Kohli. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21:1-39, 2020.
[8] John W Chinneck and Erik W Dravnieks. Locating minimal infeasible constraint sets in linear programs. ORSA Journal on Computing, 3(2):157-168, 1991.
[9] François Chollet et al. Keras. https://keras:: 2015.
[10] Roxana Daneshjou, Mert Yuksekgonul, Zhuo Ran Cai, Roberto Novoa, and James Y Zou. Skincon: A skin disease dataset densely annotated by domain experts for fine-grained debugging and analysis. Advances in Neural Information Processing Systems, 35:18157-181677 2022.
[11] Adnan Darwiche and Auguste Hirth. On the reasons behind decisions. In Proceedings of the 24th European Conference on Artificial Intelligence, 2020.
[12] Sumanth Dathathri, Sieun Gao, and Richard M Murray. Inverse abstraction of neural networks using symbolic interpolation. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 3437-3444, 2019.
[13] Alessandro De Palma, Harkirat S Behl, Rudy Bunel, Philip Torr, and M Pawan Kumar. Scaling the convex barrier with active sets. In International Conference on Learning Representations, 2021.

---

[14] Dimitar Iliev Dimitrov. Gagandeep Singh, Timon Gehr, and Martin Vechev. Provably robust adversarial examples. In International Conference on Learning Representations (ICLR 2022). OpenReview, 2022.
[15] Ruediger Ehlers. Formal verification of piece-wise linear ferd-forward neural networks. In International Symposium Automated Technology for Verification and Analysis, pages 269- 286. Springer, 2017.
[16] Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanović, and Martin Vechev. Complete verification via multi-neuron relaxation guided cannchhnnd-boudee In International Conference on Learning Representations, 2022.
[17] Timon Gehr, Matthew Mirman, Dana Drachsler- Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. A12: safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE symposium on security and privacy (SP). pages 3-18. IEEE, 2018.
[18] Sorin Grigorescu, Bogdan Trasnea, Tiberiu Cocias, and Gigel Macesanu. A survey of deep learning techniques for autonomous driving. Journal of Field Robotics, 37(3):362-366 -266 2020.
[19] Matthew Groh, Caleb Harris, Luis Soenksen, Felix Lau, Rachel Han, Aerin Kim, Arash Koochek, and Omar Badri. Evaluating deep neural networks trained on clinical images in dermatology with the fitzpatrick 17k dataset. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pages 1820-1828, 2021.
[20] Riccardo Guidotti. Counterfactual explanations and how to find them: literature review and benchmarking. Data Mining and Knowledge Discovery, pages 1-55, 2022.
[21] Patrick Henriksen and Alessio Lomuscio. Efficient neural network verification via adaptive refinement and adversarial search. In ECA/ 2020, pages 2513-2520. IOS Press, 2020.
[22] Xiaowei Huang. Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu, and Xinping Yi. A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability. Computer Science Review, 370100 2020.
[23] Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In International conference on computer aided verification, pages 3-29. Springer, 2017.
[24] Alexey Ignatiev. Towards trustable explainable ai. In Proceedings of the Twenty-Ninth In- ternational Conference on International Joint Conferences on Artificial Intelligence, pages 5154-5158, 2020.
[25] Alexey Ignatiev, Yacine Izza, Peter J Stuckey, and Joao Marques-Sin Silva. Using maxsat for efficient explanations tree ensembles. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 3776-3785, 2022.
[26] Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva Abduction basedd explanations for machine learning models. In Proceedings of the AAAI Conference Artificial Intelligence, pages 1511-,, 2019.
[27] Yacine Izza, Alexey Ignatiev, and João Marques-Silva. On tackling explanation redundancy in decision trees. J. Artif. Intell. Res., 75:261-321, 2022.
[28] Yacine Izza and Joao Marques-Sine Silva. On explaining random forests with sat. In Zhi-Hua Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Artificial Intelli- gence, IJCAI-21, pages 2584-2591. International Joint Conferences on Artificial Intelligence Organization, 2021. Main Track.
[29] Kyle D Julian, Ritchie Lee, and Mykel J Kochenderfer. Validation of image-based neural network controllers through adaptive stress testing. In 2020 IEEE r3d international conference on intelligent transportation systems (ITSC), pages 1-7. IEEE, 2020.
12

---

[30] Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smm solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pages 97-117. Springer, 2017.
[31] Guy Katz, Derek A Huang. Duligur lbeling. Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor. Haoze Wu, Aleksandar Zeljić, et al. The marabou framework for verification and analysis of deep neural networks, In International Conference on Computer Aided Verification, pages 443 452, 2019.
[32] Haitham Khedr, James Ferlez, and Yasser Shoukry. Peregrinn: neural network verifier. In International Conference on Computer Aided Verification, pages 287-300. Springer, 2021.
greedy
[33] Emanuele La Malfa, Rhiannon Michelmore, Agnieszka M. Zbrzezny, Nicola Paoletti, and Marta Kwiatkowska. On guaranteed optimal robust explanations for nlp models. In Zhi-Hua Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Artificial Intelli- gence, IJCAI-21, pages 2658-2665. International Joint Conferences on Artificial Intelligence Organization, 8 2021.
[34] Yann LeCun, Corinna Cortes, and CJ Burges. Mnist handwritten digit database. ATT Labs [Online]. Available: http://yann. wec.m.com/exll//miiiii 2, 2010.
[35] Mark H Liffiton and Karem A Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40:1-33, 2008.
[36] Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, Mykel J Kochenderfer, et al. Algorithms for verifying deep neural networks. Foundations and Trends@ in Optimization, 4(3-4):244-404,2 2021.
[37] Stuart Lloyd. Least squares quantization in pem. IEEE transactions on information theory, 28(2):129-133 1982.
[38] Scott M Lundberg and Su-In Lee. A unified approach to interpreting model predictions. In Proceedings of the 31st International Conference on Neural Information Processing Systems, pages 4768 2017.
[39] Joao Marques-Silva Thomas Gerspacher, Martin C Cooper, Alexey Ignatiev, and Nina Naro- dytska. Explaining naive bayes and other linear classifiers with polynomial time and delay. In Proceedings of the 34th International Conference on Neural Information Processing Systems, pages 100900200000 2020.
[40] Joao Marques-Silva and Alexey Ignatiev. Delivering trustworthy ai through formal xai. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 3806-3814, 2022.
[41] Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Prima: general and precise neural network certification via scalable convex hull approximations. Proceedings of the ACM on Programming Languages, 6(POPL):1-33, 2022.
[42] Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. "why should trust you?" explaining the predictions of any classifier. In Proceedings of the 22nd ACM SIGKDD international conference on knowledge discovery and data mining, pages 1135-1144, 2016.
[43] Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. Anchors:
model- agnostic explanations. In Proceedings of the Thirty-Secant Second AAAI Conference on Artificial Intelligence and Thirtieth Innovative Applications of Artificial Intelligence Conference and Eighth AAAI Symposium on Educational Advances Artificial Intelligence, pages 1527-1535, 2018.
[44] Wenjie Ruan, Min Wu, Youcheng Sun, Xiaowei Huang, Daniel Kroening, and Marta K Kwiatkowska. Global robustness evaluation of deep neural networks with provable guar- antees for the Hamming distance. In Proceedings of the Eventy-Fightte International Joint Conference Artificial Intelligence, IJCAI-19, pages 5944-5952, 7 2019.
13

---

[45] Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. In Proceedings of the 27th International Joint Conference on Artificial Intelligence, pages 5103-5111, 2018.
[46] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):1- 30, 2019.
[47] Johannes Stallkamp, Mare Schlipsing, Jan Salmen, and Christian Igel. Man vs. computer: Benchmarking machine learning algorithms for traffic sign recognition. Neural networks, 32:323 332, 2012.
[48] Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations, 2019.
[49] Hoang-Dung Tran, Stanley Bak, Weiming Xiang, and Taylor T Johnson. Verification of deep convolutional neural networks using imagestars. In International Conference on Computer Aided Verification, pages 18-42. Springer, 2020.
[50] Sahil Verma, Varich Boonsanong. Minh Hoang, Keegan E. Hines, John P. Dickerson, and Chirag Shah. Counterfactual explanations and algorithmic recourses for machine learning: review. arXiv preprini arXiv:2010. 10596, 2020.
[51] Sandra Wachter, Brent Mittelstadt, and Chris Russell. Counterfactual explanations without open- ing the black box: Automated decisions and the gdpr. Harvard Journal of Law & Technology, 3 (2)):20018 2017.
[52] Stephan Waeldchen, Jan Macdonald, Sascha Hauch, and Gitta Kutyniok. The computational complexity of understanding binary classifier decisions. Journal of Artificial Intelligence Research, 70:351 -387, 2021.
[53] Eric Wang, Pasha Khosravi, and Guy Van den Broeck. Probabilistic sufficient explanations. In Zhi-Hua Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Arti- ficial Intelligence, IJCAI-21, pages
International Joint Conferences on Artificial Intelligence Organization, 2021. Main Track.
[54] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In Proceedings of the 32nd International Conference on Neural Information Processing Systems, pages 6369-63777 6379, 2018
[55] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In Proceedings of the 27th USENIX Conference Security Symposium, pages 1599-1614, 2018.
[56] Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In Proceedings of the 35th Conference on Neural Information Processing Systems (NeurIPS), volume 34, pages 29909-29921, 2021.
[57] Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska, and Gagandeep Singh. Scalable verification of GNN-based job schedulers. Proc. ACM Program. Lang., 6(0OPSLA2), oct 2022.
[58] Haoze WI, Alex Ozdemir, Aleksandar Zeljić, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, and Clark Barrett. Parallelization techniques for verifying neural networks. In 2020 Formal Methods in Computer Aided Design (FMCAD), pages 128-137. IEEE, 2020.
[59] Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George Pappas, Hamed Hassani, Corina Pasareanu, and Clark Barrett. Toward certified robustness against real- world distribution shifts. In IEEE Conference on Secure and Trustworthy Machine Learning, 2023.
14

---

[60] Haoze Wu, Aleksandar Zeljić. Guy Katz, and Clark Barrett. Efficient neural network analysis with sum-of- -fm--offfeusibilities In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 143-163. Springer, 2022.
[61] Min Wu and Marta Kwiatkowska. Robustness guarantees for deep neural networks on videos. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition. pages 311-320, 2020.
[62] Min Wu, Matthew Wicker, Wenjie Ruan, Xiaowei Huang, and Marta Kwiatkowska. A game- based approximate verification of deep neural networks with provable guarantees. Theoretical Computer Science, 807:298-329, 2020.
[63] Kun-Hsing Yu, Andrew L Beam, and Isaac S Kohane. Artificial intelligence in healtheare. Nature biomedical engineering. 2(10):719-731, 2018.
[64] Matthew D) Zeiler and Rob Fergus. Visualizing and understanding convolutional networks. In European conference on computer vision, pages 818-833. Springer, 2014.
[65] Tom Zelazny, Haoze Wu, Clark Barrett, and Guy Katz. On optimizing for neural network verification. In Formal Methods in Computer Aided Design (FMCAD), pages 17-26. IEEE, 2022.
methods
[66] Huan Zhang, Tsui-Wer Weng, Pin-Yu Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Proceedings of the 32nd International Conference on Neural Information Processing Systems, pages 1944-4953. 2018.
[67] Xin Zhang, Armando Lezama, and Rishabh Singh. Interpreting neural network judgments via minimal, stable, and symbolic corrections. In Proceedings of the 32nd International Conference Neural Information Processing Systems, pages 4879-4899 4890, 2018.
15

---

A Proofs for Section 3.2
We present rigorous proofs for Lemma 3.2 Theorems 3.3 and 3.4 in Section 3.2 justifying the soundness and optimality of our VERIX approach. For better readability, we repeat each lemma and theorem before their corresponding proofs.
A.1 Proof for Lemma 3.2
Lemma 3.2 If the CHECK sub-procedure is sound, then, at the end of each for-loop iteration (Lines in Algorithm|] [ the irrelevant set of indices B satisfies
- A = 0.B
B
(6)
Proof. Recall that the sub-procedure CHECK is sound means the deployed automated reasoner returns True only the specification actually holds. That is, from Line 10 we have
+ è cl
holds on network f. Simultaneously, from Lines 8 and we know that, check the current feature x" of the traversing order ग,, the pre-condition & contains
- B - 1 (
-
Specifically, we prove this through induction on the number of iteration i. When i is 0, pre-condition is initialized T and the specification holds trivially. In the inductive case, suppose CHECK returns False, then the set B is unchanged as in Line [2 Otherwise, if CHECK returns True, which makes HOLD become True, then the current feature index i is added into the irrelevant set of feature indices B as in Line I1 with such satisfying specification
<|x2" - B" BB,, Se) X O - 1 22- cl <
As the iteration proceeds, each time CHECK returns True, the irrelevant set B is augmented with the current feature index i, and the specification always holds it explicitly checked by the CHICK reasoner.
A.2 Proof for Theorem 3.3
Theorem
Soundness). If the CHECK sub-procedure is sound, then the value x returned by Algorithm is a robust explanation this satisfies Equation (T) of Definition 2.1
3.3
Proof. The for-loop from Line indicates that Algorithm goes through every each feature xf in input x by traversing the set indices (xx). Line means that æ is one such instance of ordered traversal. When the iteration ends, all the indices in (xx) are either put into the irrelevant set of indices by + B as in Line [1 or the explanation index set by A + A U {i} as in Line 12 That is. A and B are two disjoint index sets forming O(x); in other words, B = +(x) A. Therefore, combined with Lemma 3.2, when the reasoner CHECK sound, once iteration finishes we have the following specification
X1I, (C) = 01B) = |2 - cl s 8.
(7)
holds on network f. where X is the variable representing all the possible assignments of irrelevant features xB i.e., V BB' and the pre-condition B SB fixes the values of the explanation cl < where c +> f((x as in
features of an instantiated input x. Meanwhile, the post-condition Line ensures prediction invariance such that 5 is 0 for classification and otherwise a pre-defined allowable amount of perturbation for regression. To this end, for some specific input x we have the following property
B' 1
||
[(x) 5.
holds. Here we prove by construction. According to Equation of Definition 2.1 if the irrelevant features B satisfy the above property, then we call the rest features x a robust explanation with respect to network ff and input x.
D
16

---

A.3 Proof for Theorem 3.4
Theorem 3.4 Optiiallity). the CHECK sub cub-procedure is sound and complete, then the robust explanation x returned by Algorithm is optimal this satisfies Equation of Definition 2.1
Proof. We prove this by contradiction. From Equation 2 Definition 2.1 we know that explanation xA is optimal if, for any feature x in the explanation, there always exists an c-perturbation on x and the irrelevant features xBB such that the prediction alters. Let us suppose x A is not optimal, then there exists a feature x in x such that matter how to manipulate this feature into x' and the irrelevant features xB into xB the prediction always remains the same. That is,
E Vx
(x
x)
(x B' + x S 1f(x) - f(x') s 6,
(9)
where + denotes concatenation two features. When we pass this input x and network / into the VERIX framework, suppose Algorithm [ examines this feature the i-th iteration, then in Line the current irrelevant set of indices is B (i), and accordingly the pre-conditions are
Φ - [|x
Bu || S < x =xxx(((()))))))
(10)
Because X [B the variable representing all the possible assignments of irrelevant features x and the i-th feature x. i.e., V x x', and meanwhile
(BB(())) (BU((()
(11)
indicates that the other features are fixed with specific values of this x. Thus, with e + f(x) in Line 3 we have the specification é reasoner CHECK is sound and complete,
S holds on input and network f. Therefore, if the
CHECK( Φ = - 6)
(12)
will always return True. Line 10 assigns True to HOLD, and index i then put into the irrelevant set B thus i-th feature x in the irrelevant features xB, However, based on the assumption, feature X explanation xA, so X in x and xB simultaneously contradiction occurs. Therefore, Theorem holds.
17

---

B Runtime performance and scalability
B.1 Runtime performance when using sound and complete verifiers
Table 4: Average execution time (seconds) of CHECK and VERIX for complete verification. In particular, magnitude is set to 3% across the Dense, Dense (large), CNN models and the MNIST, TaxiNet, GTSRB datasets for sensible comparison.
Dense
Dense (large)
CNN
CHECK
VERIX
CHECK
VERIX
CHECK
VERIX
MNIST (28 28)
0.013
160.59
0.055
615.85
0.484
4956.91
TaxiNet (27 x 54)
0.020
114.69
0.085
386.62
2.609
8814.85
GTSRB (32 x 32 x 3)
0.091
675.04
0.257
1829.91
1.574
12935.27
We analyze the empirical time complexity of our VERIX approach in Table The model structures described in Appendix D.4 Typically, the individual pixel checks (CHECK) return definitive answer (True or False) within second on dense models and in a few seconds on convolutional networks. For image benchmarks such as MNIST and GTSRB, larger inputs more complicated models result in longer (pixel- and image-level) execution times for generating explanations. As for TaxiNet regression task, while its pixel-level check takes longer than that of MNIST, it is actually faster in total time on dense models because TaxiNet does not need to check against other labels.
B.2 Scalability on more complex models using sound but incomplete analysis
Table 5: Average execution time (seconds) of CHECK and VERIX for incomplete verification. Magni- tude is 3% for both MNIST-sota and GTSRB-sota models.
# ReLU
MaxPool
CHECK
VERIX
MNIST-sota GTSRB-sota
50960
5632
2.31
1841.25
106416
5632
8.54
8770.15
/
7
2
2
9
9
Figure 10: Sound but incomplete CHECK procedure DeepPoly contributes to robust but not optimal (larger than necessary) VERIX explanations for the convolutional network MNIST-sota.
The scalability of VERIX can be improved if we perform incomplete verification, for which we re-emphasize that the soundness of the resulting explanations is not undermined though optimality is no longer guaranteed, i.e., they may be larger than necessary. To illustrate, we deploy the incomplete DeepPoly [46] analysis (implemented in Marabou) perform the CHECK sub-procedure. Table reports the runtime performance of VERIX when using incomplete verification on state-of-the-ar network architectures with hundreds of thousands of neurons. See model structures in Appendix [ Experiments were performed on a cluster equipped with Intel Xeon F5-2637 v4
Tables 7 and 9
CPUs running Ubuntu 16.04. We set a time limit of 300 seconds for each CHECK call. Moreover, in Figure IO) we include some example explanations for the convolutional model MNIST-sota when using the sound but incomplete CHECK procedure DeepPoly. We can see that they indeed appear larger than the optimal explanations when the complete Marabou reasoner is used. We remark that, as soundness of the explanations is not undermined, they still provide guarantees against perturbations on the irrelevant pixels. Interestingly, MNIST explanations on convolutional models tend to be less scattered than these on fully-connected models, as shown in Figures 4b and 6bb due to the effect of convolutions. In general, the scalability of VERIX will grow with that of verification tools, which has improved significantly the past several years as demonstrated by the results from the Verification of Neural Networks Competitions (VNN-COMP) 3
18

---

Supplementary related work and discussion
C.1 Related work (cont.)
Continued from Section our work expands on [33 in four important ways: (i) we focus on e-ball perturbations and perception models, whose characteristies and challenges are different from those of NLP models; (ii) whereas [3 simply points to existing work on hitting sets and minimum satisfying assignments for computing optimal robust explanations, we provide a detailed algorithm with several illustrative examples, and include a concrete traversal heuristic that performs well in practice; we believe these details are useful for anyone wanting to produce a working implementation: (iii) we note for the first time the relationship between optimal robust explanations and counterfactuals; and (iv) we provide an extensive evaluation on a variety of perception models. We also note that in some aspects, our work is more limited: in particular, we use a simpler definition of optimal robust explanation (without a cost function) as our algorithm is specialized for the case of finding explanations with the fewest features.
We discuss some further related work in the formal verification community that are somewhat centered around interpretability or computing minimal explanations. [14] uses formal techniques to identify input regions around an adversarial example such that all points in those regions are also guaranteed to be adversarial. Their work improves upon previous work on identifying empirically robust adversarial regions, where points in the regions are empirically likely to be adversarial. Analogously, our work improves upon informal explanation techniques like Anchors. [12 is similar to [4] in that it also computes pre-images of neural networks that lead to bad outputs. In contrast, we compute subset of input features that preserves the neural network output. [67] is more akin to our work, with subtle yet important differences. Their goal is to identify a minimal subset of input features that when corrected, changes network's prediction. In contrast, that when fixed. preserves a network's s prediction. These two goals are related but not equivalent: given a correction set found by [67]. sound but minimil VERIX explanation can be obtained by fixing all features not in the correction set along with one of the features in the correction set. Symmetrically, given VERIX explanation, sound but non minmiil correction can be obtained by perturbing all the features not in the explanation along with one of the features in the explanation. This relation is analogous to that between minimal correction sets and minimal unsatisfiable cores in constraint satisfaction (e.g.. 35) Both are considered standard explanation strategies in that field.
goal is to find minimal subset of input features
C.2 Verification of neural networks
Researchers have investigated how automated reasoning can aid verification of neural networks with respect to formally specified properties [36 22], by utilizing reasoners based on abstraction [66
46
17
41 54
555
2 65
[5 59 and search [1 30
31
23
56
48 21
B 44 62 61
32
T6 58 60)
Those approaches mainly focus on verifying whether a network satisfies a certain pre-defined property (e.g., robustness), i.e., either prove the property holds or disprove it with counterexample. However, this does not shed light on why a network makes a specific prediction. In this paper, we take a step further, repurposing those verification engines as sub-routines inspect the decision-making process of model, thereby explaining its behavior (through the presence or absence of certain input features). The hope is that these explanations can help humans better interpret machine learning models and thus facilitate appropriate deployment.
C33 Trustworthiness of the explanations
For fixed model f and fixed input x, unique traversal order passed into Algorithm I contributes to a unique explanation. That said, different traversals can produce different explanations with various sizes. A natural question then is how evaluate which of these explanations are more trustworthy than others? Following a suggestion by an anonymous reviewer, we propose that the size of an explanation can be used as a rough proxy for its trustworthiness, since our experiments show that explanations from sensitivity traversals are much smaller and more sensible than those explanations from random traversals. This also suggests that the global cardinality miinmmal explanation might be more trustworthy than its locally minimal counterparts. However, as mentioned above, computing a globally minimal explanation is extremely expensive computationally. We view the exploration of better ways to approach globally minimum explanations as a promising direction for future research.
19

---

D
Model specifications
Apart from those experimental settings in Section we include detailed model specifications for reproducibility and reference purposes. Although evaluated on the MNIST [4 GTSRB [47], and TaxiNet [29] image datasets MNIST and GTSRB in classification and TaxiNet in regression, our VERIX framework can be generalized to other machine learning applications such as natural language processing. As for the sub-procedure CHECK of Algorithm I while VERIX can potentially incor- porate existing automated reasoners, we deploy the neural network verification tool Marabou [31. While supports various model formats such as .p from TensorFlow [ and .h5 from Keras (9), we employ the cross platform .nnx format for better Python API support. When importing model with softmax as the final activation function, we remark that, for the problem to be decidable, one needs to specify the Name parameter of the read_ onnx function as the pre-softmax logits. As workaround for this, one can also train the model without softmax in the last layer and instead use the SoftmaxLoss loss function from the tensorflow tensorflow_ranking package. Either way, VERIX produces consistent results.
D.1 MNIST For MNIST, we train fully-connected feed-forward neural network with 3 dense layers activated with ReLU (first 2 layers) and softmax (last classification layer) functions as in Table achieving 92. 92.26% accuracy. While the MNIST dataset can easily be trained with accuracy as high as 99.99%. we are more interested in whether a very simple model as such can extract sensible explanations - the answer is yes. Meanwhile, we also train several more complicated MNIST models, and observe that their optimal explanations share a common phenomenon such that they are relatively more scattered around the background compared to the other datasets. This cross model observation indicates that MNIST models need to check both the presence and absence of white pixels to recognize the handwritten digits correctly. Besides, to show the scalability of VERIX, we also deploy incomplete verification on sate-of-theear model structure as in Table 7
D.2 GTSRB
As for the GTSRB dataset, since it is not identically distributed as MNIST, to avoid potential distribution shift, instead of training a model out of the original 43 categories, we focus on the top first 10 categories with highest occurrence in the training set. This allows us to obtain appropriate model with high accuracy - the convolutional model we train as in Table acchiees a test accuracy of 93.83%. It is worth mentioning that, convolutional model is much more complicated than the simple dense model in (26), which only contains one hidden layer of 15 or 20 neurons trained to distinguish two MNIST digits. Also, as shown in Table 5 of Appendix B report results the state-of-the-art GTSRB classifier in Table 9
D.3 TaxiNet
Apart from the classification tasks performed on those standard image recognition benchmarks, VERIX approach can also tackle regression models, applicable to real-world safety-critical domains. In this vision-based autonomous aircraft taxiing scenario [29] of Figure 9 train the regression model in Table to produce an estimate of the cross-track distance (in meters) from the ownship to the taxiway centerline. The TaxiNet model has mean absolute error of 0.824 the test set, with no activation function in the last output layer.
D.4 Dense, Dense (large), and CNN
In Appendix B analyze execution time of VERIX three models with increasing complexity:
Dense, Dense (large), and CNN as in Tables II I2 and 13, respectively. To enable a fair and sensible comparison, those three models are used across the MNIST, TexiNet, and GTSRB datasets with only necessary adjustments to accommodate each task. For example, in all three models h x R x denotes different input size height width x channel for each dataset. For the activation function of the last layer, softmax is used for MNIST and GTSRB while TaxiNet as a regression task needs no such activation. Finally, TaxiNet deploys he re_uniform as the kernel_ime ini tialiiiieeeeee parameter in the intermediate dense and convolutional layers for task specific reason.
20

---

Table Structure for the MNIST classifier.
Table 8: Structure for the GTSRB classifier.
Layer Type
Parameter
Activation
Type Input
Parameter
Activation
Input
28
28 x
32 32 3
Flatten
Convolution
3 x (1)
Fully Connected
10
ReLU ReLU
Convolution
2 2 x (2)
Fully Connected
10
Fully Connected
20
ReLU
Fully Connected
10
softmax
Fully Connected
10
softmax
Table 7: Structure for the MNIST-sota classifier.
Table 9: Structure for the GTSRB-sota classifier.
Type
Parameter
Activation
Type
Parameter
Activation
Input
28 x 28 x
Input
28 28 x 1
Convolution
3 x 3 32
ReLU ReLU
Convolution
3 x x 32
ReLU
Convolution
3 32
Convolution
3 32
ReLU
MaxPooling
2 2
Convolution
x x 64
ReLU
Convolution
3 x 3 x 64
ReLU ReLU
MaxPooling
2 x 2
Convolution
3 x 3 64
Convolution
3 x 64
ReLU
MaxPooling
2
Convolution
3 64
ReLU
Flatten
MaxPooling
x 2
Fully Connected
200
ReLU
Flatten
Dropout
0.5
Fully Connected
200
ReLU
Fully Connected
200
ReLU
Dropout
0.5
Fully Connected
10
softmax
Fully Connected
200
ReLU
Fully Connected
10
softmax
21

---

Table 10: Structure for the TaxiNet model.
Table 11: Structure for the Dense model.
Type
Parameter
Activation
Layer Type
Parameter
Activation
Input
27
54 x
Input
h
Flatten
Flatten
Fully Connected
20
ReLU ReLU
Fully Connected
10
ReLU
Fully Connected
10
Fully Connected
10
ReLU
Fully Connected
Fully Connected
10/
softmax /
Table 12: Structure for Dense (large).
Layer Type
Parameter
Activation
Input
h Xxwxe
Flatten
Fully Connected
30
ReLU
Fully Connected
30
ReLU
Fully Connected
10/1
softmax
Table 13: Structure for the CNN model.
Layer Type
Parameter
Activation
Input
h
Convolution
3 x x 4
Convolution
x 3 x
Fully Connected
20 10/1
ReLU softmax
Fully Connected
22


Reviews:
[{"review_id": "j5CsWRHh3s", "reviewer": "Reviewer_Yjtz", "summary": "The paper presents a system called VERIX for producing robust explanations and generating counterfactuals for deep neural network decisions. VERIX addresses the problem of explainability in AI by applying constraint solving techniques and a sensitivity-based heuristic to iteratively create explanations and counterfactuals with formal guarantees. This is particularly valuable in high-risk domains like autonomous driving and healthcare. The paper provides a formal definition of an optimal robust explanation and discusses how the system deals with two types of bounded perturbations. A key novelty is the system's ability to compute counterfactuals automatically at no additional cost. The efficacy of the system is demonstrated through several experiments and comparisons with existing methodologies, including an application in an autonomous aircraft taxiing scenario.\n", "questions": "- Could you provide more details on the scalability of VERIX, especially for larger and more complex models?\n- How does VERIX perform on non-image data? Were any experiments conducted using such data?\n- Could you discuss the potential trade-offs in using VERIX, especially regarding computational cost and complexity?", "limitations": "The authors discuss potential limitations of VERIX, including scalability and the computational cost of computing optimal robust explanations. These limitations are adequately addressed. The authors also consider future work, such as extending VERIX to other properties like fairness. However, the potential negative societal impact of the work, if any, is not explicitly addressed.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The paper presents an original and well-motivated approach to producing robust explanations for machine learning models. It integrates constraint solving and sensitivity-based heuristic to generate explanations and counterfactuals that have formal guarantees. A significant strength lies in its applicability to safety-critical domains, where the understanding of model behavior is paramount. Moreover, the ability to generate counterfactuals at no additional computational cost provides a practical advantage. Finally, the detailed comparisons with other explainability methods provide compelling evidence of the superiority of VERIX in terms of its precision and the quality of explanations it provides.\n", "weaknesses": "While the paper provides a thorough evaluation of VERIX, the generalizability of the results could be questioned, as the experimental validation is primarily performed on image datasets. Exploring the performance of VERIX on diverse types of data, including structured and time-series data, could provide a more comprehensive view of the system's applicability. Additionally, the complexity and computational cost of the VERIX algorithm might limit its use for large-scale, high-dimensional data.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We would like to thank the reviewer for their recognition of our work.\n\nAnswers to Questions:\n\n## 1. Scalability of VeriX for more complex models\n\nDue to space limitation, we address this question with all the details in the **“global” response** to all reviewers at the top of this page. Specifically, in 1.1 of the “global” response we reported the *runtime performance* of our approach, and in 1.2 we scaled up to more state-of-the-art models using the *sound* but *incomplete* verifier CROWN as the CHECK sub-procedure then reported results and exhibited example explanations. \n\n## 2. Performance of VeriX on non-image data\n\nYes, our approach can be generalized to non-image data such as tabular data or texts in natural language processing.\n\n### 2.1 How our method can work on NLP datasets\n\nHere we show how it works on the SST (Stanford Sentiment Treebank) dataset for ***sentiment analysis***. Specifically, we train a neural network on the SST dataset to predict whether the sentiment of a text is *positive* or *negative*. We attach two figures in the PDF of the \"global\" response to demonstrate our experimental results.\n\nWe first perform tokenization and post-padding on the text and convert all the words into integer values. Then we train a model with an embedding layer to transform the integers into floats, i.e., word embeddings. The structure of the model is similar to the MNIST model we trained in the paper, only this time the activation function of the last layer is *sigmoid* rather than ReLU due to sentiment analysis. That is, if the model output is greater than 0.5, the text is positive; otherwise it's negative.\t \n\n### 2.2 Get feature-level sensitivity traversal\n\nWe take the following example text from the dataset, whose sentiment is *positive*.\n\n$\\mathtt{one \\ of \\  the \\ more \\ intelligent \\ children's \\ movies \\ to \\ hit \\ theaters \\ this \\ year}$\n\nBy using the feature-level *sensitivity* traversal (proposed in section 3.3), we plot the sensitivity as the heatmap in Figure 1 of the \"global\" response. We can see that the zero paddings (\"#\") have flat sensitivity, which makes sense. The actual words have various sensitivity values, represented by the lighter and deeper colors. Intuitively, this shows how sensitive each word is to the final prediction of the sentiment. For instance, here the word $\\mathtt{intelligent}$ is the most sensitive compared to others.\n\n### 2.3 Obtain our explanations\n\nOnce we have the sensitivity traversal, we pass it to Algorithm 1 to compute the explanations.\n\nIn Figure 2, we show our VeriX explanations - $\\mathtt{intelligent}$ and $\\mathtt{movies}$ - highlighted in red. The perturbation magnitude $\\epsilon$ is set to 0.015 at the embedding space. Our results show that *any possible* perturbations within 0.015 on the irrelevant tokens (in green) will never flip the model's decision from positive to negative.   \n\n## 3. Trade-offs of VeriX regarding computational cost and complexity\n\n### 3.1 Complexity of VeriX\n\nAs shown in *Proposition 3.5 (Complexity)* in lines 235-237,  the complexity of VeriX depends on (1) the dimension $d$ of input, and (2) $P(f)$, which is the cost of checking a specification over the model $f$.\n\n### 3.2 Input dimensions $d$\n\nFor dimension $d$, we performed computational cost analysis on different image benchmarks (MNIST, TaxiNet, and GTSRB) with various dimensions, as shown in Tables 3 and 4. Take MNIST and GTSRB as an example, when $d$ increases from 28x28 to 32x32x3, we observe that both $\\mathtt{CHECK}$ and VeriX times increase for all the models in Tables 3 and 4. That is, when the input dimension increases, the computational cost increases.\n\n### 3.3 Cost of checking a specification on model $f$\n\nAs for $P(f)$, when a model is more complex, it takes longer to check a specification on it. From Table 3, we see that for the same MNIST dataset, when model complexity increases from Dense to Dense (large) and to CNN, the $\\mathtt{CHECK}$ time increases from 0.013 to 0.055 and to 0.484. Similarly for TaxiNet and GTSRB.\n\n### 3.4 Trade-off\n\nTherefore, the ***trade-off*** between computational cost and complexity is that, in order to generate formal explanations for more complex inputs and models, i.e., greater $d$ and $P(f)$, we will need to take into account higher computational cost, e.g., longer execution time, which can be alleviated by allocating more computational resources, i.e., to reduce $P(f)$.  For even more scalability, we can use incomplete methods at the cost of larger explanations.\n\n---\n\nResponses to Limitations:\n\n## Potential societal impact\n\nWhile we explicitly discussed the limitations of our work, we didn’t address the societal impact. Formal methods are designed to *mitigate* negative social impact from incorrect or non-robust models.  Thus, our work aims to bring *positive* societal impact. For instance, by analyzing our formal explanations, users can choose those trustworthy models with sensible explanations better aligned with human perception, thereby facilitating their safe deployment in safety-critical applications such as the autonomous aircraft taxiing scenario in our section 4.5. Moreover, a possible future direction is to extend our method to discover potential bias in medical diagnosis models, and thus to promote fairness in healthcare.\n"}, {"review_id": "14UbYGf3Kv", "reviewer": "Reviewer_zc3P", "summary": "This paper proposes a feature sensitivity evaluation approach to enhance neural network explainability. The proposed approach aims to provide an optimal robust explanation, which is translated as a minimal combination of features that preserves invariance in the network's prediction. Neural network verification tools are leveraged to search for such combination of features.", "questions": "The questions correspond to the weaknesses.\n1. What is the runtime of the experiments? Have the authors compare the runtimes of using different nn verification tools?\n2. How strong do \\epsilon and \\delta influence the results?\n3. How different can the global and a local optimal feature set be? Under which conditions, the size difference between those two sets is large and under which conditions the difference is small?", "limitations": "The paper It is declared in this paper that the proposed algorithm only produces local optimal solutions. The limitation is not addressed. ", "rating": 5, "confidence": 4, "soundness": 4, "presentation": 2, "contribution": 2, "strengths": "The definition of optimal robust explaination is novel and rigorous. The usage of neural network verification tools not only formally guarantees the soundness of the results but also expands the applicability of those tools. ", "weaknesses": "1. The approach is apparently computational expensive. Many neural network verifiers are usually slow. Running those verifiers for all pixels in an image will be costly. \n2. Many neural network verifiers are sound but barely complete. That means, it is quite possible that HOLD in line 10 of Algorithm 1 is easily False if the parameter \\epsilon and \\delta are too strict for the verifier.\n3. The analysis on the experimental results are not persvasive enough. In line 263, why is it good to include the surrounding pixels as explaining pixels? For instance, in Fig4(a), if a traffic sign has a number '50' in a circle, it must be speed limit sign instead of stopping sign. Then why should we consider the white background important? \n4. Question 3 begs a questions on the definition of optimal robust explaination. Since in section 2.1, it is claimed that Definition 2.1 only describes a local optimal explaination. Basically, there is no guarantee on how large and how small the induced sets A can be. ", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We would like to thank the reviewer for their recognition of our work.\n\nAnswers to Questions:\n\n## 1. Runtime performance & Comparison to other NN verification tools\n\nDue to space limitation, we address this question with all the details in the **“global” response** to all reviewers at the top of this page. Specifically, in 1.1 of the “global” response we reported the *runtime performance*of our approach, and in 1.2 we used the *sound* but *incomplete* verifier CROWN as the CHECK sub-procedure to scale up to more state-of-the-art models then reported results and exhibited example explanations. \n\n## 2. Influence of parameters $\\epsilon$ and $\\delta$\n### 2.1 Influence of $\\epsilon$ \n\nThe effect of *perturbation magnitude* $\\epsilon$ is twofold:\n- if $\\epsilon$ is too small, more pixels tend to be robust to such small level of perturbations, therefore $\\mathtt{HOLD}$ in line 10 of Algorithm 1 is more likely to be $\\mathtt{False}$, and thus more pixels will be in the irrelevant set, resulting in smaller explanations. A special case mentioned in lines 98-103 is that when the input is $\\epsilon$-robust, then all the pixels become irrelevant, and thus no valid explanation is produced.\n- if $\\epsilon$ is too large,  then more perturbations are allowed in each pixel, and thus fewer pixels are needed to alter the model prediction, i.e., smaller irrelevant sets are produced and therefore larger explanations. The corresponding special case is that if perturbing any feature in an input can change the prediction, then the entire input is an explanation (lines 103-105).\n\nIn reality, how strong $\\epsilon$ influences the explanations really depends on how **robust** the actual model is on the dataset. Intuitively, if a model is more robust, it requires perturbations in more pixels to change prediction, i.e., larger irrelevant sets and smaller explanation sets. Therefore, to prevent the explanation from being way too small, it makes sense to choose a relatively loose $\\epsilon$ to allow more perturbations in each pixel. \n\nWhen doing the experiments, we trained various models on MNIST and GTSRB, and noticed that MNIST models tend to be *more robust* than GTSRB models since MNIST images are more independent and identically distributed. Therefore, to obtain sensible explanations, it makes more sense to set a *relatively loose* $\\epsilon$ for MNIST and a *relatively tight* $\\epsilon$ for GTSRB. For instance, in Table 2’s caption, we mentioned that $\\epsilon$ is set to $5$% for MNIST and $0.5$% for GTSRB, as these MNIST models are *already robust* to $1$%-perturbations (line 292).\n\nTo pick a suitable $\\epsilon$ for MNIST, in section 4.2 (Figure 8), we visualized the effect of varying $\\epsilon$ on explanations. The users then can use the same method to pick a suitable $\\epsilon$ depending on their applications.\n\n### 2.2 Influence of $\\delta$ \n\nThe output *discrepancy* $\\delta$ is used to accommodate both classification (set $\\delta = 0$, and thus $f(\\mathbf{x}) = f(\\mathbf{x}’)$, meaning the class is not changed) and regression ($\\delta$ could be some predefined hyper-parameter quantifying the allowable output change), as in lines 82-84.\n\nFor classification, recall $f(\\mathbf{x}) = \\arg \\max f_c(\\mathbf{x})$, where $f_c(\\mathbf{x})$ denotes the confidence value (pre- or post softmax) of classifying as class $c$. As $\\delta$ is $0$, it is the **confidence value** $f_c(\\mathbf{x})$ that plays a key role. Intuitively, when a prediction has higher confidence, its confidence needs to drop more in order to alter the prediction, which potentially requires perturbations in more pixels, therefore more pixels in the irrelevant set and consequently smaller explanations. For instance, MNIST models tend to have relatively high confidence of classifying an input as a certain digit - higher than that of GTSRB models classifying a traffic sign, so MNIST models often have smaller explanations than GTSRB models, as observed in Table 2. \n\nFor regression tasks, recall that $f(\\mathbf{x}) = c$, where $c$ is a single quantity, e.g., the cross-track estimate of the autonomous aircraft taxiing scenario in section 4.5. If $\\delta$ is small, i.e., $c$ is allowed to change little. Then, given the same perturbation magnitude $\\epsilon$, fewer pixels are allowed with such perturbations, therefore resulting in smaller irrelevant sets and thus larger explanations. \n\n## 3. Clarifying why those surrounding pixels are in the explanation for Fig 4(a) $\\mathtt{50 \\ mph}$\n\nWe would like to remark that it is not “us” who consider the white background in $\\mathtt{50 \\  mph}$ important; rather, it is “the model” that considers the white background important. \n\nWe can speculate as to why this is.  One thing to keep in mind is that the trained GTSRB model is ***not perfect***. A perfect model would be able to correctly recognize all traffic signs in the dataset (accuracy 100%), and, more importantly, we would hope that there are no unnecessary artifacts in its explanations.\n\nReal models are not perfect.  So in this case, we speculate that this GTSRB model checks a few surrounding pixels to “know” that they are the background and are therefore not important for decision-making. And simultaneously, it also checks key pixels in the central region of the image to “know” there is a number $\\mathtt{50}$, and therefore be able to predict it as a $\\mathtt{50 \\ mph}$ road sign.\n\n## 4. Regarding local and global optimal explanations\n\nIn Definition 2.1, an explanation is *locally optimal* in the sense that no proper subset of the explanation is itself an explanation.  We believe that this definition is a good compromise between *computational difficulty* and *usability*.  While a globally optimal explanation might be a bit smaller, it would be much more difficult to compute.  In practice, we don’t expect the globally optimal explanation to be much smaller than the one computed using the sensitivity traversal, which already shows promising results experimentally.\n"}, {"review_id": "EgxD01zWbe", "reviewer": "Reviewer_VvcV", "summary": "The paper contributes with proposing a robustness-based method to  compute formal explanations that irreducible (minimal subset of input data, often referred as sufficient explantions) for feedforward neural networks (NNs). Formal robustness checker is used in the experiments but the method allows to use any formal robustness solver to verify existence or not of adversarial examples (AEx) when perturbing a feature input $X^i$ to prove its importance or not for the prediction made by the NN model.  \n   \nOne of the drawback of formal methods in XAI is scalability, and NNs is a good example that shows the limits of automated reasoners. A compromise that might be acceptable for users is to restrict the explanation search to the vicinity of the data input and consider explanations that are sound locally (with some distance/perturbation $\\epsilon$) but not in the entire domain. And this paper proposes to compute distance-restricted sufficient explanations using robustness solver as alternative to automated reasoners, so that the input intervals to explore in the model is restricted, which is likely to scale for large NNs.", "questions": "- Explanations delivered by Algo 1 might be empty sets? similarly for the counterfactuals.  This is problematic for a user, which will always be interested in computing (understand the reason behind a prediction) a counterfactual/explanation for any point of the distribution data.\n\n- can you conclude about the duality between explanations and counterfactuals defined under $\\epsilon$-ball ($l_\\infty$-norm for robustness)? and how to compute (optimal) counterfactuals from explanations in the same why as algo1 that exploits counterfactuals  or in a efficient way? \n\n- Are counterfactuals  returned by algo 1 optimal/minimal (or smallest)? It seems not to be the case!  Then, an important question raises here: how to compute optimal counterfactuals? and in general case do you think that algo1 can be exploited to devise an algorim for computing optimal/smallest counterfactual?\n\n- can you propose an efficient algorithm to enumerate optimal explanations? \n\n- how can we  compute efficiently a ( single) counterfactual based on robustness checking, and directly given input data without generating  (optimal) explanations ?", "limitations": "- The paper failed to show clearly and formally the duality between explanations and counterfactuals \n- The outlined algorithm reports the basic version of the linear search algorithm and does not implement possible \noptimization/refinement to reduce the total number of oracle calls, for example it does not discuss how can be AEx exploited \nto improve the procedure.\n\n\nRemarks:\n- Notion of robust does not really make sense in my opinion, given the definition of an explanation.  In fact, by definition, it is set of feature that are important/relevant for the model prediction, and what remain is not. So no matter the value that other features take the predictions will remain the same, (there is no AEx). Indeed robustness and explanations are tightly related, since that AEx and explanations are related (recent work have pointed out the existing connection between both concepts)  but there’s no sense to caracterize robust explanations following def 2.1 and non-robust explanations. A given subset features  A is either an explanation if perturbing $j\\in A$ yield to an AEx, or not one if there still exists an AEx although all features of A are maintained to the values of the input vector.      \n\nBesides, recently another form of (robust) counterfactual explanations is introduced in J. Jiang et al \"Formalising the Robustness of Counterfactual Explanations for Neural Networks\" AAAI23, which is relates faithfulness of the explanation after retraining the same DNN. In this case, the notion of robustness is justified.\n\n- Optimality in algo1 should be precised  that it refers to subset minimality. A confusion might be introduced when using in the text optimal and smallest explanations.   Basically, algo1 returns an irreducible subset and not a minimum (or smallest) set.", "rating": 5, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- Computing formal local explanations achieved with applying robustness queries to the model is novel\n- The proposed solution offers formal guarantees of soundness and precision of the resulting explanations \nin contrast to popular post-hoc XAI approaches like LIME, SHAP, Anchor that are heuristic in their nature\n- Moreover, the paper propose a nice trick  for the traversal order of the features which allows in practice to generate smaller \nexplanations, and might be further exploited to speed up the extraction of the explanations with using other \nalgorithms  like quickplain to drop quickly group of irrelevant features (instead of a single feature at time with the linear algo 1) \n\n- Experimental results show that explanations computed by VeriX are more succinct than explanations returned by Anchor and LIME for two well-known image benchmarks.", "weaknesses": "- The paper rediscovers the so-called deletion-based algorithm, outlined in Algorithm 1, that can be traced at least to: \nJOHN W. CHINNECK  \"Locating Minimal Infeasible Constraint Sets in Linear Programs\" ORSA Journal on Computing1991,  initially used to compute min infeasible set (in over constrained formula) and also used by [24] to computing abductive explanations for NNs. \n(In the context of XAI, the insight of the algorithm is to delete features and check if there exists AEx, whilst for minimal infeasible/unsatisfiable sets it relaxes a constraint from the formula and if there is an unsatisfiable core.)\n\n- Section 3.2 ( Theorem 3.3, 3.4 and proposition 3.5) rediscovers what has been established for at least 30 years. \nThe complexity of algo1/deletion-based algorithm is well known in the literature, it’s a linear search procedure that performs $m$ oracle calls ($m$: number of iterations) and other variants of the algorithm allow to reduce $m$  by doing some pre-processing to refine the initial set x to traverse or exploiting unsatisfiable cores (here AEx) to drop some features and thus save  calls to the NP oracle.\n\n- The paper claims that it establishes for the first time the relationship between explanations and counterfactuals. Unfortunately, it overlooked what already exists in the literature and did not demonstrate clearly this relationship. In fact, explanations and counterfactuals \nare dual, and this has been shown in XAI: A. Ignatiev \"On Relating Explanations and Adversarial Examples.\" NeurIPS 2019.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Responses to Weaknesses:\n\n## 1&2. Algorithm 1, Theorems 3.3 & 3.4, and Proposition 3.5\n\nWe didn’t claim to be the first to discover the so-called deletion-based algorithm. Rather, we explore its use in Algorithm 1 to compute *optimal robust explanations* in the context of formal explainable AI.  We appreciate that the reviewer points out the existence of such an algorithm for computing *minimal infeasible sets* which can be traced back to [1]. We will cite [1] and clarify the correlation in our paper. Meanwhile, we cited [24] multiple times (lines 75, 111, 364, 759) in the paper and, particularly, discussed [24] in section 5 Related work.\n\nOur Theorems 3.3 (Soundness) and 3.4 (Optimality) do rely on the general properties of such deletion-based algorithms, but are also specialized for our specific definitions, so they are not identical.\n\nProposition 3.5 (Complexity) analyzes the complexity of Algorithm 1 with a particular focus on how *a network $f$* and *a $d$-dimensional input $\\mathbf{x}$* would affect the complexity. We felt this would be convenient for the reader.  Certainly the analysis is related to similar algorithms.  We would be happy to clarify that in the final version.\n\n[1] J. Chinneck, E. Dravnieks. “Locating minimal infeasible constraint sets in linear programs”. ORSA Journal on Computing, 1991.\n\n## 3. Relation of our formal explanations and counterfactuals\n\nThe reviewer says [2] relates explanations with counterfactuals, however we emphasize that [2] relates explanations with *adversarial examples* **not** counterfactuals, whereas our work relates *formal* explanations with counterfactuals.\n\n***While adversarial examples are related to counterfactuals, they are not the same.***  Below we quote from [3] the key difference between these two terms:\n> While the strategies used to find the adversarial examples can be the same adopted to retrieve counterfactuals, the objectives are different. For example, adversarial learning applied to images aims at finding a humanly imperceptible change in the input image that changes the prediction outcome with the idea of fooling the classifier. On the contrary, counterfactual explainers applied to images aim at highlighting significant parts of the image that change the prediction outcome with the idea of explaining the classifier.\n\nIn our Figure 4(b), we highlighted those significant parts (yellow) in the explanation (green) for the MNIST digit $\\mathtt{1}$ to demonstrate that, if these pixels are allowed to change, they can change the classification into $\\mathtt{8}$, $\\mathtt{5}$, and $\\mathtt{2}$, respectively.\n\n[2] A. Ignatiev. \"On relating explanations and adversarial examples\". NeurIPS 2019.\n\n[3] R. Guidotti. “Counterfactual explanations and how to find them: literature review and benchmarking”. Data Mining and Knowledge Discovery, 2022.\n\n---\nAnswers to Questions:\n\n## 1. Already clarified two special cases when computing explanations\n\nIn lines 98-105, we specifically clarified *two special cases*. The first case says if the model is **$\\epsilon$-robust**, then in order to obtain a valid explanation, a larger $\\epsilon$ is required. That’s why, in section 4.2 and Figure 8, we visualized the effect of varying $\\epsilon$ on explanations to help users choose an appropriate $\\epsilon$ to produce meaningful explanations and counterfactuals depending on their applications.\n\n## 2&3. Both asked how to compute optimal counterfactuals\n\nFrom the above text quoted from [3], we know adversarial examples and counterfactuals are not identical. In particular, [3] formalizes a list of desirable properties for counterfactuals: *validity, minimality, similarity, plausibility, discriminative power, actionability, causality, and diversity*, some of which are not typically taken into account by adversarial examples. Therefore, while [2] reveals the duality between explanations and adversarial examples, we must remark that such a straightforward duality between explanations and counterfactuals is not explicit, as it must simultaneously consider these desirable properties.\n\nMeanwhile, as emphasized in lines 124-125, our focus in this paper is to compute *optimal robust explanations* **not** optimal counterfactuals. We do not claim optimality for our counterfactuals. Rather, we observe that these counterfactuals can be computed with no extra cost and can be used to better understand the explanations we generate, as shown in Figure 4(b). If the reviewer is particularly interested in computing optimal counterfactuals, we refer to work [4] in which *actionability* and *plausibility* are considered.\n\n[4] A. Parmentier, T. Vidal. “Optimal counterfactual explanations in tree ensembles.” ICML 2021.\n\n## 4. Enumerate optimal robust explanations\n\nThe point of our novel *feature-level sensitivity traversal* (proposed in section 3.3) is to obtain a good optimal robust explanation without having to enumerate all such explanations, as that is computationally prohibitive. If the reviewer is interested in enumeration, we provide references to [5][6] in which the authors enumerated abductive and contrastive explanations.\n\n[5] A. Ignatiev. “From contrastive to abductive explanations and back again”. AIxIA, 2020.\n\n[6] J. Marques-Silva et al. “Explanations for monotonic classifiers”. ICML 2021.\n\n## 5. Counterfactuals computed without generating (optimal) explanations\n\nIn Algorithm 1, $\\mathbf{C}$ denotes a set of counterfactuals and $m$ is a single counterfactual.\n\nTherefore, in the  CHECK sub-procedure (line 10 of Algorithm1), we know that we do obtain a single counterfactual $m$ the *very first time* $\\mathtt{HOLD}$ is false, and we efficiently obtain such counterfactuals *every time* when $\\mathtt{HOLD}$ is false. In other words, we do not need to wait for the algorithm to finish in order to get counterfactuals.\n\nDue to space limitation, we address the rest of the comments in the **“global” response** (starting from point 2) to all reviewers at the top of the page.\n"}, {"review_id": "yZeB3MmvKZ", "reviewer": "Reviewer_oNV3", "summary": "This paper presents an elegant approach for calculating the optimal robust explanation for a DNN prediction. Intuitively, an explanation is robust if small perturbations of the the features not included in the explanation do not modify the model output. A robust explanation is optimal if small perturbations to any of the features included in the explanation changes the model output. The paper adapts this notion of optimal robust explanation from prior work [31]. The main contribution is the VERIX algorithm for calculating such explanations. This algorithm iterates over each input feature in sequence and uses neural network verification tools as a sub-procedure. Although the algorithm calculates an optimal robust explanation, the explanation is not necessarily the smallest since the model can have multiple optimal robust explanations for a prediction. The size of the calculated explanation crucially depends on the order in which the input features are traversed. The paper presents a heuristic based on input feature sensitivity that seems to work well in practice. For every feature included in the explanation, the algorithm also returns a counterfactual, i.e., an input with a different value for the feature under consideration that would change the model output. The approach is evaluated on models trained for MNIST, GTSRB, and TaxiNet datasets.", "questions": "As mentioned above, I would be interested in the authors thoughts about the following questions:\n\n1. Can the approach be usefully scaled to large models with millions of parameters?\n\n2. How can such explanations be useful to developers? How can developers deploy the algorithm in practice to aid in constructing more trustworthy models?\n\n3. Given the sensitivity of the algorithm to the feature traversal order, how does one trust the explanations? Relatedly, can saliency map be a good heuristic for picking the traversal order?\n\n--------------------\nEdits after author response:\nBased on author responses to my questions, I have increased my score to 7", "limitations": "Yes, the authors clearly discuss the limitations of their approach in the paper.", "rating": 7, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "The paper is very well-written and presents a simple, easy to understand algorithm for computing optimal robust explanations. The authors are upfront about the limitations of the approach which is much appreciated. The empirical evaluations do a good job of addressing different questions of interest such as the effect of $\\epsilon$ on the explanations and the effect of feature traversal order.", "weaknesses": "My primary concerns about the approach are about its scalability and the usefulness of the calculated explanations.\n\n- The algorithm repeatedly invokes neural network verification tools. Such tools are notoriously hard to scale, limiting the applicability of the approach to large, state-of-the-art networks. It would have been very interesting if the paper included an evaluation using sound but incomplete tools based on techniques like abstract interpretation. Such tools typically demonstrate greater scalability. It would be instructive to see the degradation in the quality of the explanation due to the use of these scalable tools. In the other direction, it would also be instructive to demonstrate the lack of scalability of tools like [4] that calculate the minimum sized explanations.\n\n- My concern about the usefulness of the calculated explanations is a more general concern about this line of work. Although I do not expect the authors to fully resolve this question, it would be useful to have a discussion about this in the paper. For instance, how can developers use these explanations? What specific data points should be picked for computing the explanations? Are there existing studies that show that such explanations are useful in practice?\n\n- Finally, I am also a little concerned by the sensitivity of the algorithm to the order in which the features are traversed. It would be helpful to evaluate a few different strategies for the same. Moreover, if the traversal order can lead to vastly different explanations, how does one trust the generated explanation?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We would like to thank the reviewer for their recognition of our work.\n\nAnswers to Questions:\n\n## 1. Scalability of the approach & Evaluation using other verification tools\n\nDue to space limitation, we address this question with all the details in the **“global” response** to all reviewers at the top of this page. Specifically, in 1.1 of the “global” response we reported the *runtime performance* of our approach, and in 1.2 we used the *sound* but *incomplete* verifier CROWN as the CHECK sub-procedure to scale up to more state-of-the-art models then reported results and exhibited example explanations. \n\nApart from this, we didn’t compare to these approaches [31,4] that compute the cardinality-minimal explanations because they are too computationally difficult to converge for *large* models, *high-dimensional* inputs, as well as *infinite and continuous* perturbations as in our case. For instance, [31] focuses on the $k$-NN box perturbations in their experimental results, which is essentially discrete as it chooses a finite set of the $k$ closest tokens for each word in a text example.\n\n## 2. Usefulness of such explanations\n\nWe discussed the potential usefulness of our explanations via the two practical applications in the paper, namely the *autonomous aircraft taxiing* scenario in section 4.5 and the *dermatology diagnosis model in healthcare* in section 1 Introduction and section 6 Conclusion.  \n\n### 2.1 Compare trustworthiness of models in aircraft taxiing \n\nFor the *autonomous aircraft taxiing* application, while users can train various regression models to obtain the cross-track estimates, our explanations can help users decide which of these models are more **trustworthy**. For instance, if a model produces not-so-bad estimates but its explanations do not make sense, e.g., it does not “look at” the $\\mathtt{remote \\ line}$ at all or it completely discards the central region - whether there is a $\\mathtt{centerline}$ or not, then users should at least take extra precautions to decide whether to trust this model.\n\n### 2.2 Identify potential bias in medical care \n\nFor the *dermatology diagnosis* model, our explanations could help identify potential **bias** if it exists. For instance, if the diagnosis model has an explanation based solely on the patient’s skin tones (“$\\mathtt{Fitzpatrick}$ I-II, III-IV, V-VI”), then the model is faulty and possibly biased as it should consider the diseased tissue not the skin type to make a diagnosis. \n\n## 3. Sensitivity based traversal order & how about saliency map\n\n### 3.1 How does one trust the explanations?\n\nUltimately, whether we should trust the explanations depends on how they are aligned with our **human perception**. Ideally, the model should be focusing on the pixels that we would focus on. However, such experiments involving real humans are challenging and require an entirely different experimental setup. As an alternative, we use *explanation size* and *generation time* as the two metrics when evaluating the explanations. As shown in Table 2, our explanations are much smaller than those from Anchors and LIME, but at the cost of taking more time.\n\n### 3.2 Sensitivity traversal relates robustness\n\nIntuitively, our sensitivity traversal measures how each individual pixel is sensitive to the confidence value of the prediction, and then ranks all pixels from the *least* to the *most* sensitive. We know that those least sensitive pixels tend to be ***more robust*** to perturbations therefore they are more likely to be in the irrelevant set. In other words, Algorithm 1 starts with those least sensitive pixels and puts them into the irrelevant set, and eventually leaves the most sensitive pixels in the explanation set.\n\nTo show that our deterministic *feature-level sensitivity* is a good heuristic to generate traversal orders, in section 4.3 and **Appendix B.1** we compare it to *random* traversals. From Figure 5, we can see that explanations from sensitivity traversals make much more sense than those from random traversals. Also, Figure 10(d) shows that the size of explanations from sensitivity traversals is much smaller than that from random traversals.\n\n### 3.3 How about saliency maps?\n\nThat said, *saliency maps* can be a good heuristic for picking the traversal order also, as long as they reflect the above-mentioned correlation with the model's prediction confidence. After all, our sensitivity (Figure 5(a) 2nd column) can be regarded as an example of a saliency map. A possible different strategy is to use the *gradient* of the model with respect to each pixel, and then rank the gradient accordingly from small to large.\n"}]

Author rebuttal:
We would like to thank all reviewers for their comments and suggestions. 

Due to space limitations, below in **1** we address the common questions from more than one reviewer about the *runtime performance and scalability* of our approach, in **2** we respond to a crucial misunderstanding from Reviewer VvcV regarding the *size* of our formal explanations, and in **3**, we address the “Remarks” section of Reviewer VvcV’s review.

## 1. Runtime performance and scalability of our approach

### 1.1 Runtime performance of the experiments

We already included the analysis of *runtime performance* in **Appendix B.2 (page 18)**.  It is referred to in line 360 of the main paper.

In Table 3, we reported the average execution time of the CHECK sub-procedure and the VeriX algorithm on image benchmarks (MNIST, TaxiNet, GTSRB) for models with increasing complexity - $\mathtt{Dense / Dense (large) / CNN}$. Typically, the CHECK sub-procedure returns a definitive answer (True/False) within a second on these dense models and in a few seconds on these CNN models. The total time to obtain a VeriX explanation varies from hundreds of seconds (for dense models) to thousands of seconds (for CNN models).

As analyzed in Proposition 3.5 (Complexity), the complexity of VeriX depends on (1) the input dimension $d$ and (2) the cost of checking a specification for model $f$, i.e., $P(f)$. Therefore, when the input dimension increases, e.g., from MNIST 28x28 to GTSRB 32x32x3, the CHECK and VeriX times increase accordingly. Meanwhile, for each dataset, when the model complexity increases, e.g., from $\mathtt{Dense}$ to $\mathtt{Dense (large)}$, the cost of checking a specification $P(f)$ increases, and thus the CHECK and VeriX times increase too. 

### 1.2  Scalable to more complex models using sound and incomplete verifier

Apart from the sound and complete tool Marabou, we also deployed the sound but *incomplete* **CROWN** analysis to perform the CHECK sub-procedure in order to scale up to more complex models. We should emphasize that, when the deployed verifier is sound but incomplete, the resulting explanations are still *sound* (i.e., provide guarantees against perturbations on the irrelevant pixels) though no longer *optimal* (i.e., no longer subset-minimal so may be larger than necessary).

In Table 4, we reported runtime performance of CHECK and VeriX on MNIST and GTSRB models with hundreds of thousands of neurons (e.g., 106416 ReLUs in $\mathtt{GTSRB}$-$\mathtt{sota}$) using the sound but *incomplete* CROWN analysis as the CHECK sub-procedure. We observe that CHECK returns in seconds and VeriX finishes in thousands of seconds. Moreover, for such *incomplete* verification, in Figure 11 we provided some example explanations for the CNN model $\mathtt{MNIST}$-$\mathtt{sota}$ (model structure in Table 6, page 21). We can see that they tend to be larger than the optimal explanations when using Marabou.

Finally, we would like to remark that the *scalability* of VeriX will grow with that of verification tools, which has improved significantly in the past several years as demonstrated by the results from the Verification of Neural Networks Competitions (VNN-COMP) [1].

[1] S. Bak et al. “The 4th International Verification of Neural Networks Competition (VNN-COMP).” 2023.


## 2. Our explanations are *smaller not larger* than Anchors!

**Reviewer VvcV *mistakenly* claims that our “formal explanations are generally quite large (compared for example to Anchor).”** 

We quote what the reviewer said below:
> Formal explanations are generally quite large (compared for example to Anchor), which is likely the case for NNs trained on image data. For example, explanations that represent 40% or 50% of features (~400 pixels in MNIST) might be hard for practitioners to be interpreted/understood. Is there any perspectives in this line to overcome the issue of size for formal explanations?

We are unsure what gave the reviewer this impression, but it is not correct.  On the contrary, our explanations are in fact ***significantly smaller*** than those produced by either LIME or Anchors, as shown in Table 2 (page 8) under the *size* column: our size `180.6` vs Anchor size `494.9` vs LIME size `432.8` for MNIST, and our size `357.0` vs Anchor size `557.7` vs LIME size `452.9` for GTSRB. We are guessing that when Reviewer VvcV specifically mentions “(~400 pixels in MNIST)”, they thought that was our result, but in fact that’s the Anchor result.

So, a key contribution is that our explanations are both *smaller* and provide *formal guarantees*. 

- - -
## 3. Responses to Reviewer VvcV’s Remarks

### 3.1 Notion of optimal robust explanations

Reviewer VvcV complains about the use of “*robust*” when talking about explanations.  They say, 
> In fact, by definition, it is set of feature that are important/relevant for the model prediction, and what remain is not. So no matter the value that other features take the predictions will remain the same, (there is no AEx).

If, in fact, this were the definition used in the literature, the reviewer would be correct.  But it is not.  Indeed, prominent techniques for producing “*explanations*” (such as LIME and Anchors) do not have the property that there is no adversarial example.  Thus, the introduction of the word “*robust*” seems appropriate to distinguish our definition from theirs.  We would also like to point out that the name “*optimal robust explanation*” is not something we invented, but comes from [31].  We use the same name to emphasize the link to that work and to avoid creating confusion by introducing many names for the same thing.

### 3.2 Optimality already clarified in the paper

In lines 106-115, we do in fact clarify that our definition of optimality is *local* in the sense that it computes a *minimal* subset of features rather than a “minimum (global smallest)” set of features.


Meta-review: The authors develop a framework for computing explanations for ML predictions in terms of feature attributions with formal robustness guarantees. The authors introduce several novel ideas and compelling experiments demonstrating the power of their approach on image classification and tabular domains. While the reviewers identified and raised some issues with the paper initially, these were successfully addressed in my opinion during the rebuttal phase. Hence I recommend acceptance.
Decision: Accept (poster)