# A dive into formal explainable attributions for image classification

Dorin Doncenco, Julien Girard-Satabin, Romain Xu-Darme, Zakaria Chihani

<figure><img src="image_1.png" /></figure>

## To cite this version:

Dorin Doncenco, Julien Girard-Satabin, Romain Xu-Darme, Zakaria Chihani. A dive into formal explainable attributions for image classification. European Conference on Artificial Intelligence 2025, Oct 2025, Bologna, Italy. hal-05219606

HAL Id: hal-05219606

https://hal.science/hal-05219606v1

Submitted on 22 Aug 2025

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

<figure><img src="image_2.png" /></figure>
# A dive into formal explainable attributions for image classification

Dorin Doncenco<sup>a,b,*</sup>, Julien Girard-Satabin<sup>a</sup>, Romain Xu-Darme<sup>a</sup> and Zakaria Chihani<sup>a</sup>

ORCID (Dorin Doncenco): https://orcid.org/0009-0007-1203-6456, ORCID (Julien Girard-Satabin): https://orcid.org/0000-0001-6374-3694, ORCID (Romain Xu-Darme): https://orcid.org/0000-0002-8630-5635,

ORCID (Zakaria Chihani): https://orcid.org/0009-0004-8915-4774

**Abstract.** In the field of explainable Artificial Intelligence (xAI), attribution methods provide off-the-shelf tools to explain the decision of a machine-learning model. However, existing methods usually do not correctly reflect the actual model behaviour, and they are difficult to compare, due to a lack of ground truth and/or consensus on what a correct explanation should be. Meanwhile, existing work leveraging formal verification to attribution methods is promising but suffer from scalability issues.

In this study, we propose a Formally Grounded Correctness (FGC) metric to measure the correctness of existing attribution methods using formal verification. FGC can be used to rank popular explanation methods according to their correctness, ensuring that explanations are correct with regards to the model decision. To allow the application of FGC on more challenging datasets, we propose to use sound, incomplete algorithms, that trade accuracy for scalability, with existing work on input segmentation. We extensively benchmark FGC on MNIST, GTSRB and a scaled down version of ImageNet with several state-of-the-art provers and show its practical usefulness. FGC surprisingly shows that the baseline saliency heuristic is a strong baseline with regards to correctness, shedding light on some caveats of other popular explanation techniques.

## 1 Introduction

Introduced in recent years for neural networks (NN), *local attribution methods* [1] consist in identifying which subset of an input is relevant *w.r.t.* a particular decision of a network. Example of local attribution methods include perturbation-based approaches like LIME [47] and Anchors [48], gradient-based methods [51, 53] or computing Shapley values [39]. Full reviews on the field are available [1, 14]. Local attribution methods can be used to highlight a model's failure modes, to correct bugs [6], identify and correct unwanted biases in the model's prediction, or help humans build a mental model on the behaviour of a complex model [18].

Attribution methods are unfortunately not a panacea for generating informative explanations. As shown by multiple studies [3, 16, 27], different methods can generate widely different explanations for a given decision, raising the question: *which explanation is "better"?* More generally, several properties can be used as potential criterion for assessing the quality of an explanation [45]. In this work,

we explore two of these properties: *correctness*, and *compactness*. Applied to attribution methods, correctness evaluates the ability of the explanation method to sort the input features based on their importance *w.r.t.* the decision of the model, while compactness favors smaller explanations over larger ones (see Miller [41]). Therefore, *a correct and compact explanation would identify the most important input features, and only those features*. However, when attempting to generate such explanations, one faces two major obstacles: 1) exploring all possible “coalitions” of input features without a heuristic quickly becomes computationally intractable (e.g., Lundberg and Lee [39]); 2) as shown in Xu-Darme et al. [64], there usually does not exist a consensus on how to measure the adequacy of an explanation *w.r.t.* a given property. This lack of consensus can stem from different interpretations of the property, and/or the reliance on empirical evidence (e.g., random sampling) rather than hard proofs that the property holds. Hence, the need for attribution methods that generate explanations which can be *provably* evaluated against desirable properties.

To address this lack of consensus, we propose considering Formal Abductive Explanations (FAE) [40, 29, 13] for NNs. FAEs are a class of attribution methods grounded on formal methods. Contrary to the sampling-based and gradient-based methods, such techniques query the model to build the set of *all* possible outputs based on a specification of the inputs. Hence, they provide a higher degree of fidelity to the NN prediction that mitigates the well-known brittleness of other approaches [3, 27].

Formally, given an arbitrary input vector *x* with feature *i* denoted as *x*<sub>*i*</sub>, Θ(*x*) the set of indices of *x*, a NN *f* and a classification result *f*(*v*) = *c* (where *v* is a particular value of *x*), the problem of finding an *abductive explanation* requires building a subset-minimal *E* such that ⋀<sub>x<sub>i</sub>∈E</sub> (*x*<sub>i</sub> = *v*<sub>i</sub>) → *f*(*x*) = *c*. An *optimal abductive explanation* is the smallest set *E<sub>optimal</sub>* among all abductive explanations. Intuitively, *E* is the set of *relevant features* whose value is sufficient to guarantee a particular outcome, and conversely, Θ(*x*) \ *E* is the set of *irrelevant features*. The size of an explanation is therefore measured as the number of relevant features. As opposed to the more empirical attribution methods described above, it is also worth mentioning that such explanations are binary: a feature is either relevant or irrelevant.

An interesting question is whether FAE can be used to address the lack of consensus described earlier. Therefore, as FAE approaches

<footnote><sup>a</sup>Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France</footnote>

<footnote><sup>b</sup>CentraleSupélec - MICS</footnote>

<footnote>* Corresponding Author. Email: first.last@cea.fr.</footnote>
are only influenced by the model decision w.r.t. the features, they can be used as a referee of some sort against other attribution metrics. Implementations of FAEs — VeriX [62] and Bassan and Katz [7] — build *E* by iteratively perturbing each *x*ᵢ (e.g., within a bounded ε ball), and checking whether the prediction changes. Both methods use: 1) a greedy algorithm that heavily relies on the traversal order of Θ(*x*); 2) the Marabou [32, 61] algorithm — heavily used in the field of formal adversarial robustness [60, 61, 38, 52] — to produce the formal queries to the NN. This reliance on the traversal order of Θ(*x*) is crucial. Indeed, choosing which features to consider first is already an algorithmic choice on which feature is relevant (or irrelevant). It is then sensible to use existing attribution metrics as a traversal order. An optimal traversal order would then select features in order to obtain the smallest possible *E*. Thus, we believe that the resulting size of *E* can be considered a good quality metric for the underlying attribution method.

However, Marabou’s exhaustive search algorithm is costly, making it difficult to scale to the larger networks [52, 44] and high-dimensional inputs typically associated with tasks such as computer vision. This, in turn, questions the applicability of formal explanations in real-world datasets.

Therefore, developing techniques that are both provably sound and applicable to real-world settings has become a crucial endeavour. To that end, the international competition on NN verification (VNN-Comp) [10, 11] fosters the development of more scalable algorithms. The best contenders in VNN-Comp are said *incomplete*: they trade optimality (in terms of explanation size) for scalability to higher-dimensional inputs. Because of this, incomplete algorithms may be a way forward to real-world application of formal explanations.

A second approach to mitigating the scalability issue — proposed in Bassan and Katz [7] — consists of segmenting the input into *bundles* of features (*superpixels* in computer vision) and building explanations from these bundles rather than individual features. Not only are the effects on scalability visible, but this approach also provides an interesting prospect on the notion of compactness presented above. Although they result in bigger explanations (w.r.t. number of features), bundle-based explanations can also be closer to human perception (in terms of *concepts*, as the field of concept-based explanations [33]). An explanation with big chunks of image instead of pixels as its main constituent is more palatable for an end-user.

**Contributions** Our contributions can be summarised as follows:

* We show how algorithms for generating formal abductive explanations can exhibit a partial order on existing attribution methods, through the relationship between the correctness of the method used as prior for the traversal order and the size of the resulting explanation. In particular, we prove that for linear models, the VeriX algorithm generates an optimal explanation when using a correct attribution method. We introduce the Formally-Grounded Correctness (FGC) metric for attribution methods that exhibit such a partial order, and demonstrate its consistency across various modalities;

* We show how using state-of-the-art verification algorithms (winners of the competition VNN-Comp) and input segmentation algorithms allows the scaling of formal explanations to bigger problems, specifically Tiny ImageNet, allowing the computation of FGC on a wide range of problems.

This paper is structured as follows: Section 2 describes our experimental setting; in Section 3, we explore the correlation between the correctness of attribution methods and the size of formal

explanations, in Section 4, we study improvements to the scalability of formal explanations. Finally, Section 5 concludes our paper and outlines our future work.

## 2 Experimental settings

**Datasets** We used the MNIST [36] and GTSRB [55] datasets to compare with existing VeriX approaches. We used Tiny ImageNet [43], a version of ImageNet [15] with 200 labels scaled down to a resolution of 64 × 64, as representative for a more challenging, realistic computer vision task. Unless stated otherwise, experiments were computed on 50 images drawn evenly from the test set of the dataset; results were averaged on that number of instances. The same 50 images (dataset-wise) were used for each experiment.

**Solvers** To verify the queries on neural networks, we used 3 solvers: PyRAT [37] with the zonotopes domain, α, β-CROWN [60] with the CROWN Interval Bound Propagation method [66] for bound computation, and Marabou [61]. Marabou has a sound and complete mode with Gurobi [24] enabled, however, due to architectural issues in our available computing cluster, we were not able to secure a suitable Gurobi license for Marabou. Thus we used the default SMT solver, assumed to be complete.

**Model architectures** For MNIST and GTSRB experiments with PyRAT, α, β-CROWN, we used a small convolutional neural network, with one convolution layer of kernel size 3, 4 filters, a maxpool (stride 2), followed by a fully connected layer of size 20, a ReLU and a final fully connected layer. Accuracy on MNIST is 0.96, GTSRB is 0.92. For Tiny ImageNet experiments, we retrained a Resnet18 [25] network ourselves<fnref n="1" /> up to 0.56 accuracy<fnref n="2" />.

**Computing resources** The experiments are run using the Slurm workload manager [30], with 12 GB RAM and a Intel(R) Xeon(R) Gold 6154 CPU @ 3.00GHz Processor. For Tiny ImageNet, we used 48 GB RAM. We note that 72 GB RAM were not enough for computing a formal explanation with ImageNet. We did not use GPUs for our computations.

**External libraries** We used: 1) the Captum library [35] to compute feature attributions; <fnref n="2" /> 2) the Quantus library [26] for the implementation and default parameters of the Faithfulness Correlation/Estimate correctness metrics<fnref n="4" />; <fnref n="3" />) our own implementation for Local Relative Correctness, with an evaluation radius of 10⁻<fnref n="3" />; <fnref n="4" />) scikit-learn [46] for the implementation of the input segmentation methods; 5) the original VeriX implementation, integrating different solvers, traversal orders, and superpixel explanations (unless stated otherwise, we used the default ϵ = 5 × 10⁻<fnref n="2" /> for our experiments as the perturbation level argument in the VeriX algorithm); 6) the auto_LiRPA library [63] for training certified robust networks.

<footnote n="1">¹ Based on: https://github.com/tjmoon0104/Tiny-ImageNet-Classifier</footnote>

<footnote n="2">² While we acknowledge that the accuracy of this model is subpar, we believe that subpar predictive performance does not impede the validity of our results regarding the scalability of formal explanations. Training more accurate networks would require operations and network sizes not amenable to current provers. We also highlight that the VNN-COMP integrates a benchmark for verifying lower accuracy (0.35) networks: https://github.com/huanzhang12/vnncomp2024_tinyimagenet_benchmark?tab=readme-ov-file</footnote>

<footnote n="3">³ In the case of Shapley Values Sampling, we used the parameter *n*<sub>sampling</sub> = 100. Setting *n*<sub>sampling</sub> = 10000 significantly increased the computational costs without increasing performance.</footnote>

<footnote n="4">⁴ In practice, the Quantus library implements many correctness metrics. However, due to limited computing resources, we restricted our study to FE/FC.</footnote>
# 3 Formal methods as a proxy to evaluate attribution methods

## 3.1 On the importance of the traversal order

Algorithms for generating abductive explanations are greedy. Thus, as noted by the authors of VeriX, “the traversal order can significantly affect the size and shape of the explanation”. In particular, they show that a heuristic based on feature-level sensitivity — computed using occlusion [65] and where features are explored from least to most important — leads to more “sensible” and smaller explanations, compared to a random traversal order.

In this work, we further explore the impact of the traversal order, using heuristics based on multiple feature attribution methods: random and occlusion [65] (VeriX baseline), integrated gradients [56], input × gradient [50], saliency [51] and SHAP [39]. These particular methods were chosen as representatives of the different groups described in the taxonomy of Koenen and Wright [34]. In all cases, we averaged the absolute value of each pixel’s importance across color channels, and pixels were explored from least to most important. As a sanity check, we also considered a “reverse saliency” heuristic, where pixels were explored in reverse order w.r.t. their importance as given by the saliency method.

As shown in Table 1, traversal orders based on saliency consistently lead to smaller explanations than all other methods (including the baseline established by Wu et al. [62]). Our experiments also reveal that there exists such a thing as a “bad” traversal order, with explanations generated using “reverse saliency” being even larger than those generated using a random order. This result shows that local attribution methods can be used as prior knowledge to improve more formal approaches. Moreover, given their relatively low computational overhead (especially compared to formal verification tools), we argue that attribution methods should always be used in this context.

A seemingly unexpected behaviour in this is the Shapley Sampling attribution method. We have found that SHAP scores perfom similarly to the random attribution approach on color datasets (eg. GTSRB), which supports previous work [28] that SHAP scores can be sensitive to irrelevant features, and do not necessarily preserve the order of relative importance of features.

## 3.2 Using VeriX as a correctness metric

As indicated in Section 1, the ability to sort pixels based on their importance to the model’s decision relates to the property of correctness of attribution methods. Hence, the results presented above point towards a strong correlation between the correctness of an attribution method used as a prior for the traversal order, and the size of the resulting abductive explanation. More precisely, we postulate that the more correct the heuristic attribution method, the smaller the abductive explanation.

The proof that this postulate holds when the model is linear can be found in Appendix A [17]. The proof can be extended to NN with ReLU activation functions, as they are piece-wise linear. More formally, if $f: \mathbb{R}^d \to \mathbb{R}$ is a ReLU-NN, then for any input $\mathbf{x}$, there exists a threshold $\mu(\mathbf{x}) \ge 0$ and a set of parameters $\{w_i(\mathbf{x})\}_{i \in \{0, \dots, d\}} \in \mathbb{R}^d$ such that the model remains linear around $\mathbf{x}$:

$$ \forall \hat{\mathbf{x}} = \langle \hat{\chi}_1, \dots, \hat{\chi}_d \rangle, \\ \|\mathbf{x} - \hat{\mathbf{x}}\|_{\infty} < \mu(\mathbf{x}) \Rightarrow f(\hat{\mathbf{x}}) = w_0(\mathbf{x}) + \sum_{i=1}^{d} w_i(\mathbf{x}) \hat{\chi}_i $$

**Theorem.** If $f: \mathbb{R}^d \to \mathbb{R}$ is a ReLU-NN, $\mathbf{x}$ is an input, $\mu(\mathbf{x}) > \epsilon$, and $\eta$ is a permutation of $\{1, \dots, d\}$ such that $|w_{\eta(i)}(\mathbf{x})| < |w_{\eta(i+1)}(\mathbf{x})|$, then VeriX($f, \mathbf{x}, \epsilon, \infty, \delta, \pi$) returns an optimal abductive explanation of the smallest size using $\pi = (\eta(1), \eta(2), \dots, \eta(d))$.

In other words, given a small-enough perturbation around $\mathbf{x}$ for each feature, a ReLU model behaves as a linear function (ie. piecewise linear). As such, the optimal abductive explanation can be found using the vanilla saliency attribution method. This theorem is a direct consequence of the linear case in Appendix A [17], with the assumption that $\mu(\mathbf{x}) > \epsilon$ which guarantees that the model remains linear around $\mathbf{x}$.

One crucial corollary to this hypothesis is that the size of the abductive explanations generated by algorithms such as VeriX can serve as a proxy for the correctness of the attribution methods that are used to derive the traversal order, i.e., VeriX can serve as a benchmark for correctness, ranking attribution methods from most to least correct. In the rest of this paper, we call this metric Formally-Grounded Correctness (FGC in short).

**Is FGC stable?** To evaluate the consistency of FGC, we first studied the stability of its ranking of each attribution method across multiple test images. We found that this ranking is stable across all the experiments presented in Table 1, with a p-value lower than 0.01 on the Friedman test [20] for each attribution method. We provide exact p-values in each table of our experimental results.

We also check the consistency of FGC across various experimental settings, by computing the Spearman’s rank correlation coefficient [54] between the FGC rankings in all of our experiments. We find in Appendix C [17] that the FGC is strongly correlated across all experimental settings, except for the difference between the MNIST and color datasets: this hints that the faithfulness of attribution methods changes when there is a significant shift in the dataset studied (binary data vs color, continuous images), but it is otherwise stable.

**Does FGC display similar behaviour on models trained with different objectives?** In practice, models can be trained with other objectives than minimising prediction loss. In particular, models can be trained to be certifiably robust against small perturbations on the inputs [66, 49]. Given that local robustness is at the core of VeriX, robust models might impair our approach. To test this hypothesis, we evaluated FGC on several networks that we trained on GTSRB at various robustness levels. The results in Table 1 of Appendix B show that while these networks are less sensitive to perturbations (as expected), the ordering of attribution methods remains similar.

As a sanity check and inspired by previous work [3, 27], we also consider randomly-initialized neural networks - which can also be useful for feature extraction [58, 5].

Randomly-initialized networks showcase a similar pattern where the saliency and its reverse attribution method perform at the extreme. The correlation between the experiments on randomly initialized networks and the other experiments highlights that lower accuracies of a network does not impede the quality of FGC. See Table 2 of Appendix B for more details.

**Is FGC consistent with other correctness metrics?** Several metrics have been introduced to measure the correctness of attribution methods: Faithfulness Correlation (FC) [9] swaps subsets of features with a fixed baseline and examines the correlation between the sum of attribution values of each subset and changes in the model output; similarly, Faithfulness Estimate (FE) [4] examines the correlation between attribution scores and changes in the model output on various points; Local Relative Correctness (LRC) [64] first builds a surrogate
<table><caption>**Table 1.** Average size (in pixels) and computation time (in seconds) per heuristic, for the explanations of the 50 evenly-drawn test images in the **MNIST** and **GTSRB** datasets. Explanations computed using the **Marabou**, **PyRAT** and **α, β-CROWN** solvers. Rounded down.</caption><thead><tr><th rowspan="2">Heuristic</th><th rowspan="2">Size</th><th colspan="2">Marabou</th><th colspan="2">PyRAT</th><th colspan="2">α, β-CROWN</th></tr><tr><th>Time</th><th>Time</th><th>Time</th><th>Time</th><th>Time</th><th>Time</th></tr></thead><tbody><tr><th colspan="8" style="text-align: left;">MNIST</th></tr><tr><td>Random</td><td>648 ± 51</td><td>710 ± 467</td><td>669 ± 39</td><td>215 ± 48</td><td>622 ± 52</td><td>42 ± 0</td><td>42 ± 0</td></tr><tr><td>Occlusion</td><td>646 ± 53</td><td>637 ± 412</td><td>652 ± 46</td><td>157 ± 25</td><td>621 ± 53</td><td>40 ± 1</td><td>40 ± 1</td></tr><tr><td>Integrated Gradients</td><td>634 ± 68</td><td>411 ± 264</td><td>689 ± 35</td><td>131 ± 16</td><td>632 ± 56</td><td>41 ± 1</td><td>41 ± 1</td></tr><tr><td>Input X Gradient</td><td>633 ± 69</td><td>413 ± 266</td><td>688 ± 37</td><td>161 ± 28</td><td>631 ± 58</td><td>41 ± 1</td><td>41 ± 1</td></tr><tr><td>Saliency</td><td><b>602 ± 73</b></td><td>818 ± 553</td><td><b>635 ± 52</b></td><td>219 ± 45</td><td><b>578 ± 72</b></td><td>42 ± 0</td><td>42 ± 0</td></tr><tr><td>Reverse Saliency</td><td>701 ± 40</td><td>242 ± 180</td><td>722 ± 24</td><td>125 ± 19</td><td>682 ± 38</td><td>40 ± 1</td><td>40 ± 1</td></tr><tr><td>Shapley Values</td><td>623 ± 59</td><td>675 ± 429</td><td>662 ± 41</td><td>218 ± 37</td><td>600 ± 61</td><td>72 ± 3</td><td>72 ± 3</td></tr><tr><td>Friedman p-value</td><td>7.70e-40</td><td></td><td>9.44e-55</td><td></td><td>2.36e-40</td><td></td><td></td></tr><tr><th colspan="8" style="text-align: left;">GTSRB</th></tr><tr><td>Random</td><td>930 ± 78</td><td>1446 ± 1981</td><td>934 ± 76</td><td>520 ± 224</td><td>918 ± 80</td><td>138 ± 4</td><td>138 ± 4</td></tr><tr><td>Occlusion</td><td>877 ± 112</td><td>2104 ± 2521</td><td>897 ± 98</td><td>562 ± 201</td><td>870 ± 113</td><td>139 ± 4</td><td>139 ± 4</td></tr><tr><td>Integrated Gradients</td><td>859 ± 120</td><td>2211 ± 2453</td><td>888 ± 103</td><td>575 ± 208</td><td>854 ± 121</td><td>140 ± 5</td><td>140 ± 5</td></tr><tr><td>Input X Gradient</td><td>858 ± 120</td><td>2220 ± 2472</td><td>888 ± 104</td><td>573 ± 210</td><td>853 ± 121</td><td>139 ± 4</td><td>139 ± 4</td></tr><tr><td>Saliency</td><td><b>852 ± 123</b></td><td>2407 ± 2570</td><td><b>877 ± 110</b></td><td>597 ± 222</td><td><b>846 ± 124</b></td><td>140 ± 4</td><td>140 ± 4</td></tr><tr><td>Reverse Saliency</td><td>989 ± 41</td><td>427 ± 756</td><td>993 ± 35</td><td>303 ± 84</td><td>985 ± 40</td><td>136 ± 3</td><td>136 ± 3</td></tr><tr><td>Shapley Values</td><td>966 ± 68</td><td>922 ± 1479</td><td>976 ± 61</td><td>490 ± 136</td><td>961 ± 69</td><td>279 ± 20</td><td>279 ± 20</td></tr><tr><td>Friedman p-value</td><td>3.09e-55</td><td></td><td>6.86e-56</td><td></td><td>9.90e-55</td><td></td><td></td></tr></tbody></table>

<table><caption>**Table 2.** Average correctness score of attribution methods for multiple metrics on the GTSRB dataset. For LRC/FGC, less is better.</caption><thead><tr><th>Metric</th><th>FC↑</th><th>FE↑</th><th>LRC↓</th><th>FGC↓ (ours)</th></tr></thead><tbody><tr><td>Saliency</td><td>0.83</td><td>0.95</td><td>0.07</td><td>877.00</td></tr><tr><td>Reverse Saliency</td><td>-0.83</td><td>-0.95</td><td>2.02</td><td>993.00</td></tr><tr><td>Shapley Values Sampling</td><td>0.92</td><td>0.98</td><td>1.55</td><td>976.00</td></tr><tr><td>Integrated Gradients</td><td>0.93</td><td>0.98</td><td>1.72</td><td>888.00</td></tr><tr><td>Input X Gradient</td><td>0.95</td><td>0.98</td><td>1.15</td><td>888.00</td></tr><tr><td>Occlusion</td><td>0.75</td><td>0.99</td><td>3.49</td><td>897.00</td></tr><tr><td>Random</td><td>-0.00</td><td>-0.00</td><td>9.59</td><td>934.00</td></tr></tbody></table>

<table><caption>**Table 3.** Spearman's rank correlation score between various correctness metrics evaluating our selected attribution methods on the GTSRB dataset. The *p*-value is given in parentheses.</caption><thead><tr><th>Metrics</th><th>FE</th><th>LRC</th><th>FGC (ours)</th></tr></thead><tbody><tr><td>FC</td><td>0.61 (0.15)</td><td>0.64 (0.12)</td><td>0.59 (0.16)</td></tr><tr><td>FE</td><td>—</td><td>0.18 (0.7)</td><td>0.32 (0.48)</td></tr><tr><td>LRC</td><td>—</td><td>—</td><td>0.58 (0.18)</td></tr></tbody></table>

# 4 Scalability of formal explanation methods on neural networks

model from the feature attribution, then measures the average local error between the model and the surrogate, relative to the model's own local stability. The results of these experiments, shown in Table 2, reveal a consensus regarding the relative correctness of gradient-based methods, compared to other attribution methods. As in Xu-Darme et al. [64], this consensus was refined by computing the pairwise Spearman rank correlation score [54] between all correctness metrics (including ours) over the GTSRB dataset, i.e., a Spearman score of 1 between two correctness metrics indicates that they systematically rank the attribution methods under test in the same order. As shown in Table 3, there does not seem to exist any global consensus between the different correctness metrics. As stated earlier, this lack of consensus may stem from the fact that most metrics rely on empirical evidence (random sampling<fnref n="5" />), and — as pointed out by Xu-Darme et al. [64] — it is difficult to compare correctness metrics in general without any ground truth of what a correct explanation should be.

In summary, our FGC metric: 1) relies on verified properties of explanations rather than empirical evidence; 2) computes a stable ranking of attribution methods; 3) has a proven relation to correctness in the linear case (see Appendix A). These three observations constitute strong indications that formal methods can also be an effective tool to evaluate the correctness of existing attribution methods.

To ensure the practical usefulness of explanation techniques in critical settings, two factors are important (on top of preserving correctness w.r.t. the model's prediction). First, the time to compute an explanation: short generation time maximises the number of possible queries for the human requiring the explanation. Second, the size of addressable inputs: while previous work [62, 7] focused on small images, few output classes and small networks, realistic computer vision tasks may involve high-dimensional inputs, deep neural network architectures and a huge number of classes. Our study aims to assert whether formal explanations can be applied to those use cases; that is to say, can such approaches provide meaningful explanations within a reasonable time limit on deeper networks and bigger inputs?

Hence, this section describes our experiments related to the two main approaches for increasing the scalability of formal attribution methods: 1) using state-of-the-art incomplete algorithms as part of the verification procedure; and 2) segmenting the input into disjoint sets.

## 4.1 Exploring incomplete algorithms for scalability

We considered the top 3 winners of the VNN-Comp 2024 edition: α, β-CROWN [60], PyRAT [38] and Marabou [32, 61]. The first two rely on domain propagation, i.e., instead of computing the concrete values of inputs, they propagate bounds on possible values. The theoretical foundations of such algorithms are well-explored [12, 42]. But more importantly, and contrary to Marabou, these algorithms are incomplete.

<footnote n="5">⁵ Although [64] proposed to use adversarial sampling to identify corner cases in LRC. Interestingly, FGC reaches a marginally better consensus with LRC than with FC/FE.</footnote>
Informally, *complete* algorithms — such as Marabou — use exhaustive search algorithms. In the context of formal abductive explanations, using a complete algorithm means that a given feature will always be *decidedly* inside or outside the explanation. But even backed with clever heuristics, exhaustive search space remains costly, and possibly prone to approximation errors when handling real numbers. In practice, this means that a complete algorithm may still fail to return an answer when the computation time exceeds a given threshold (timeout), or return an incorrect answer due to approximations. On the contrary, *incomplete* algorithms — as provided by tools such as *α*, *β*-CROWN and PyRAT — compute an over-approximation of the output set from a specification on input set. Then, they check the intersection of this abstracted output set with another set describing the property to check (in VeriX case, robustness against a perturbation of a given set of features). However, imprecision may arise when the abstracted output set is too lax, leading the solver to answer *unknown* (i.e., it is unknown if altering these features will result in a decision change). In that case, the offending features are added to the explanation, following a conservative approach. Incidentally, this over-approximation also means that such algorithms are less prone to approximation errors when handling real numbers. The main consequence is that incomplete algorithms have no guarantees to provide *correct and compact explanations*, but only *correct explanations* (meaning that all relevant features are included in the explanation), i.e., the explanations will theoretically be larger than with complete algorithms.

While this sounds like a drawback, we argue that it is worth exploring the gap between complete and incomplete algorithms in practice. We show that it may not be as wide as initially expected. Thus, we applied VeriX with PyRAT, *α*, *β*-CROWN and Marabou as verifiers on MNIST, and GTSRB. For Tiny ImageNet, we used PyRAT; the RAM requirements for verifying with Marabou exceeds 128 GB RAM, whereas the *α*, *β*-CROWN verifier returns all pixels as relevant, which makes a comparison between the traversal orders impossible. For each verifier and dataset, we used the traversal orders detailed in Section 3.

The results in Table 1 had already shown that the simple choice of a different verifier can reduce the computation time of formal explanations by several orders of magnitude w.r.t. results from the state of the art, while maintaining the rankings relative to traversal orders. The computation time can be further reduced, using the upcoming approach.

## 4.2 Partition of the input set

Abductive explanation methods applied to computer vision tasks suffer from a major drawback: they reason at the *feature level*. Hence, their computing time is entirely dependent on the size of the *search space*. Indeed, each feature must be checked one after the other, which may prove intractable on large input spaces. To mitigate this issue, Bassan and Katz [7] proposed to build a segmentation of the input space into *bundles* of features. In practice, they used the Quickshift algorithm [59] to partition images into a disjoint set of superpixels, and showed that the union of formal explanations on bundles is a valid formal explanation on the whole image. In addition, this explanation computed using superpixels provides a more human-readable explanation compared to the pixel-level approach (Figure 1).

We also expand the study of FGC to superpixels (Figure 2). More precisely, we use existing attribution methods as heuristics to determine the traversal order of superpixels, computing the

<figure><img src="image_3.png" /><figcaption>**Figure 1.** Example comparison between pixel-level and superpixel-level formal explanations. Pixel-level explanations are coarse, whereas superpixel-level explanations take advantage of segmentation methods such as quickshift to point towards a specific area, that is more human readable. Best viewed in color.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>**Figure 2.** Original image (left), with a saliency traversal order aggregated into superpixels using the mean of the gradient (middle). Brighter superpixels in the traversal order means the superpixel will be traversed later in VeriX. The resulting explanation (right) is more contiguous than pixel-level explanations. Green highlights relevant pixels. Best viewed in color.</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>**Figure 3.** Trade-off between average superpixel size and explanation size and computation time. The bigger the superpixels, the quicker the explanation is computed, but the final explanation size is bigger and less accurate. Note that the explanation size axis does not start from 0, and the y-scale for time is logarithmic.</figcaption></figure>

importance of each superpixel as the average importance of its associated pixels. We extended the list of possible segmentation methods to also include the Felzenszwalb [19], Watershed [8], and SLIC [2] approaches.

We first tried several parameters for Quickshift to vary the size of superpixels. As illustrated in Figure 3, we observed a clear trade-off between the computing time and the size of the resulting explanation, depending on the average superpixel size. Following this, we selected the parameters leading to an average superpixel size of 85 pixels (resulting in an average of 12 superpixels per GTSRB image), to ensure an average verification time below 100s. Having too few superpixels would lead to no variance between the attribution methods used as heuristics, and too many superpixels would make this approach computationally similar to the pixel-level approach. Then, we selected the parameters leading to similar superpixel sizes for the other segmentation approaches.
The results of our experiments, presented in Table 4 indicate that the Felzenszwalb partition method tends to produce smaller explanations, compared to Quickshift (bar the pathological reverse saliency traversal order), Watershed or SLIC. From the point of view of our FGC metric, we noticed an instability of the ranking for Watershed and SLIC — using the Friedman test — mainly due to the similar results obtained in terms of explanation size across all attribution methods considered. This instability was caused by Watershed and SLIC segmenting images into superpixels that are very small, with few superpixels covering the entirety of the image. Nevertheless, FGC remained stable when using Quickshift or Felzenszwalb (p-value lower than 0.05), confirming its relevance as a ranking metric.

Finally, as shown in Table 5, the benefit of using the saliency attribution method w.r.t. the size of the resulting explanation is maintained when using superpixels, across all solvers. This further confirms the relevance of using abductive explanations as a way to evaluate the correctness of attribution methods. To demonstrate the scalability of this approach, we also applied the Felzenszwalb segmentation method to the Tiny ImageNet dataset with a ResNet18 model, and observed the same trends, particularly that the saliency attribution method results in the smallest explanations, even when using larger models on larger datasets.

## 4.3 Discussion

We encountered several limitations during our experiments. First, as stated in our experimental settings (Section 2), we postulate that the inconsistent results (w.r.t. explanation size)<fnref n="6" /> obtained in Table 1, where the supposedly complete Marabou solver has larger explanations than other solvers, are due to the fact that using Marabou without Gurobi leads to longer solving times, thus more timeouts and therefore bigger explanations. A GitHub issue on the VeriX code mention this phenomenon<fnref n="7" />. We reproduced that issue on a separate laptop, where it was possible to install Gurobi and to run small-scale experiments: on that setting, Marabou produced smaller explanations.

A second limitation relates to the (lack of) support of various common machine-learning operations by verification tools. As a result, our choice of possible NN architectures was limited.

Nevertheless, our experiments show that, with the combination of:
1) a good segmentation algorithm (Felzenszwalb),
2) a good traversal order based on reasonable prior knowledge of the importance of certain regions in the image, provided by heuristics such as saliency,
3) a fast and accurate verifier (e.g., PyRAT or α, β-CROWN), it is possible to reduce the computing time of an abductive explanation by two or three orders of magnitude, with a moderate increase in explanation size. For example, using superpixels, α, β-CROWN is able to generate explanations in less than one second on GTSRB, further strengthening our claim that formal attributions methods can scale up to computer vision tasks. The computation of formal explanations beyond the GTSRB dataset to Tiny ImageNet validates that approaches grounded on formal methods are not limited to toy datasets. This clearly shows that it is possible to apply formal attribution methods on critical settings, with a controlled trade-off on the size of explanation.

<figure><img src="image_6.png" /><figcaption>**Figure 4.** Size and time required to compute a formal explanation depending on the perturbation $\epsilon$ on the GTSRB dataset.</figcaption></figure>

On this subject, it is worth mentioning that the scalability of VeriX largely depends on the choice of the maximum perturbation $\epsilon$. As illustrated in Figure 4, high $\epsilon$ values cause most pixels to be relevant, while small $\epsilon$ perturbations will never change the prediction (e.g., the choice of $\epsilon$ during our experiments with superpixels on GTSRB or TinyImagenet led to explanations covering around 80% of the image). Crucially, the optimal value of $\epsilon$ depends solely on the stability of the model itself. This is related to robustness - more robust models will require larger perturbations to provide a meaningful explanation, thus mechanically decreasing the size of the explanation. Unfortunately, this (predictable) behaviour leads to the observation that not only does there exist a trade-off between the compactness — and therefore usefulness — of a formal explanation and the time it takes to compute it, but also that finding the balance between these two properties (usefulness v. scalability) depends entirely on the NN under test. In other words, formal explanations generated from unstable NNs are more likely to remain uninformative and/or computing intensive, strengthening our belief that there exists an intimate correlation between the stability (robustness) of a NN and its explainability.

# 5 Conclusion and Future Direction

As is often the case in machine-learning developments, two of the main obstacles are scalability and trustworthiness, i.e., how can one get a result faster or for larger instances, and how confident can one be in the results. In this paper, we focused on the xAI field and offered a way to alleviate both these obstacles, specifically through formal methods. In particular, we showed how generating formal explanations can be scaled up using input segmentation, and how formal methods can be used as a *principled* means to evaluate attribution methods. We justified our claim with multiple arguments indicating the validity of this assertion from the point of view of two desired attributes of an explanation: its compactness and its correctness.

Principled approaches for xAI could be explored further. Indeed, the divide between NN and human perceptions is more and more obvious, as exemplified by adversarial attacks [57, 22] or shortcuts [21]. Such divide may produce vastly different world perceptions that result in *disalignment* [23]. It is thus crucial to ensure that decisions are taken accordingly to human values. Scalability of formal xAI could be explored further, exploring distributed verification approaches. As we proved that formal xAI can scale up to larger networks, we believe that their correctness will prove to be an important source of trust when explaining increasingly complex models. In this regard, we plan to pursue the study of our FGC metric, applying it in a more systematic manner to additional attribution methods.

<footnote n="6">⁶ Marabou without enabling Gurobi is sound and complete. Gurobi is a MILP solver used in Marabou to accelerate the tightening of ReLUs bounds in a split-and-conquer approach, hence exhibiting more accurate and faster results. We emphasize that enabling Gurobi is an optional step that does not invalidate the soundness of the underlying procedure (Reluplex [31], the predecessor of Marabou, used GLPK as a LP solver, but support was dropped when switching to Marabou).</footnote>

<footnote n="7">⁷ https://github.com/NeuralNetworkVerification/VeriX/issues/1</footnote>
<table><caption>**Table 4.** Partitioning methods, on GTSRB / PyRAT.</caption><thead><tr><th rowspan="2">Heuristic</th><th colspan="2">Felzenszwalb</th><th colspan="2">Quickshift</th><th colspan="2">SLIC</th><th colspan="2">Watershed</th></tr><tr><th>Size (px)</th><th>Time (s)</th><th>Size (px)</th><th>Time (s)</th><th>Size (px)</th><th>Time (s)</th><th>Size (px)</th><th>Time (s)</th></tr></thead><tbody><tr><td>Random</td><td>914 ± 88</td><td>6 ± 2</td><td>909 ± 112</td><td>6 ± 4</td><td><b>889 ± 114</b></td><td>6 ± 2</td><td><b>915 ± 84</b></td><td>6 ± 1</td></tr><tr><td>Occlusion</td><td>886 ± 118</td><td>7 ± 3</td><td>900 ± 123</td><td>6 ± 4</td><td>897 ± 100</td><td>6 ± 1</td><td>917 ± 86</td><td>6 ± 1</td></tr><tr><td>Integrated Gradients</td><td>886 ± 117</td><td>7 ± 3</td><td>897 ± 126</td><td>7 ± 4</td><td>890 ± 101</td><td>5 ± 1</td><td><b>915 ± 85</b></td><td>6 ± 1</td></tr><tr><td>Input X Gradient</td><td>888 ± 116</td><td>7 ± 3</td><td>898 ± 125</td><td>6 ± 4</td><td>894 ± 100</td><td>6 ± 1</td><td>917 ± 82</td><td>6 ± 1</td></tr><tr><td>Saliency</td><td><b>873 ± 126</b></td><td>7 ± 3</td><td><b>892 ± 133</b></td><td>7 ± 4</td><td>899 ± 104</td><td>6 ± 1</td><td>919 ± 84</td><td>6 ± 2</td></tr><tr><td>Reverse Saliency</td><td>945 ± 67</td><td>5 ± 1</td><td>942 ± 72</td><td>5 ± 2</td><td>895 ± 102</td><td>5 ± 1</td><td>920 ± 76</td><td>5 ± 1</td></tr><tr><td>Shapley Values</td><td>904 ± 108</td><td>149 ± 6</td><td>907 ± 118</td><td>148 ± 8</td><td>894 ± 108</td><td>135 ± 7</td><td>921 ± 80</td><td>147 ± 4</td></tr><tr><td>Friedman p-value</td><td>1.52e-18</td><td></td><td>1.06e-10</td><td></td><td>4.10e-01</td><td></td><td>9.49e-01</td><td></td></tr></tbody></table>

<table><caption>**Table 5.** Average size (in pixels) and computation time (in seconds) per heuristic, for the explanations of 50 evenly-drawn test images in the **GTSRB** dataset, for **Marabou**, **PyRAT** solvers, and of 1000 evenly-drawn test images for the **α, β-CROWN** solver with a perturbation level of $\epsilon = 5 \times 10^{-2}$, and on the **Tiny ImageNet** dataset with **PyRAT** with a perturbation level of $\epsilon = 10^{-4}$. **Superpixel-level** computation, using Felzenszwalb segmentation. Rounded down.</caption><thead><tr><th rowspan="2">Dataset<br>Solver<br>Heuristic</th><th colspan="4">GTSRB</th><th colspan="4">Tiny ImageNet</th></tr><tr><th colspan="2">Marabou</th><th colspan="2">PyRAT</th><th colspan="2">α, β-CROWN</th><th colspan="2">PyRAT</th></tr><tr><th></th><th>Size</th><th>Time</th><th>Size</th><th>Time</th><th>Size</th><th>Time</th><th>Size</th><th>Time</th></tr></thead><tbody><tr><td>Random</td><td>970 ± 78</td><td>23 ± 26</td><td>948 ± 92</td><td>7 ± 4</td><td>893 ± 145</td><td>1 ± 0</td><td>1577 ± 974</td><td>3709 ± 1614</td></tr><tr><td>Occlusion</td><td>932 ± 121</td><td>25 ± 29</td><td>943 ± 103</td><td>8 ± 6</td><td>872 ± 167</td><td>1 ± 0</td><td>1530 ± 960</td><td>3894 ± 1573</td></tr><tr><td>Integrated Gradients</td><td>934 ± 123</td><td>24 ± 30</td><td>943 ± 102</td><td>8 ± 6</td><td>872 ± 167</td><td>1 ± 0</td><td>1552 ± 982</td><td>4111 ± 1599</td></tr><tr><td>Input X Gradient</td><td>929 ± 121</td><td>25 ± 32</td><td>942 ± 103</td><td>8 ± 6</td><td>871 ± 168</td><td>1 ± 0</td><td>1543 ± 971</td><td>4060 ± 1580</td></tr><tr><td>Saliency</td><td><b>916 ± 123</b></td><td>32 ± 36</td><td><b>936 ± 108</b></td><td>8 ± 6</td><td><b>864 ± 175</b></td><td>1 ± 0</td><td><b>1471 ± 958</b></td><td>4049 ± 1597</td></tr><tr><td>Reverse Saliency</td><td>1009 ± 36</td><td>8 ± 8</td><td>970 ± 60</td><td>6 ± 3</td><td>930 ± 102</td><td>1 ± 0</td><td>1886 ± 1010</td><td>3597 ± 1642</td></tr><tr><td>Shapley Values</td><td>965 ± 88</td><td>158 ± 29</td><td>956 ± 82</td><td>177 ± 11</td><td>896 ± 147</td><td>147 ± 7</td><td>1578 ± 1009</td><td>16647 ± 1647</td></tr><tr><td>Friedman p-value</td><td>2.53e-15</td><td></td><td>4.23e-06</td><td></td><td>7.01e-311</td><td></td><td>2.34e-17</td><td></td></tr></tbody></table>

## Acknowledgements

This publication was made possible by the use of the FactoryIA supercomputer, financially supported by the Ile-De-France Regional Council.

This work was supported by the French Agence Nationale de la Recherche (ANR) through SAIF (ANR-23-PEIA-0006).

We thank Augustin Lemesle and Julien Lehmann, for their thorough help and support with PyRAT.

## References

[1] K. Abhishek and D. Kamath. Attribution-based xai methods in computer vision: A review. ArXiv, abs/2211.14736, 2022.

[2] R. Achanta, A. Shaji, K. Smith, A. Lucchi, P. V. Fua, and S. Süsstrunk. Slic superpixels compared to state-of-the-art superpixel methods. IEEE Transactions on Pattern Analysis and Machine Intelligence, 2012.

[3] J. Adebayo, J. Gilmer, M. Muelly, I. Goodfellow, M. Hardt, and B. Kim. Sanity Checks for Saliency Maps. In Advances in Neural Information Processing Systems 32, 2018.

[4] D. Alvarez Melis and T. Jaakkola. Towards robust interpretability with self-explaining neural networks. Advances in neural information processing systems, 31, 2018.

[5] E. Amid, R. Anil, W. Kotłowski, and M. K. Warmuth. Learning from randomly initialized neural network features, 2022.

[6] A. Balayn, N. Rikalo, C. Lofi, J. Yang, and A. Bozzon. How can explainability methods be used to support bug identification in computer vision models? In CHI Conference on Human Factors in Computing Systems, CHI '22. ACM, Apr. 2022. doi: 10.1145/3491102.3517474.

[7] S. Bassan and G. Katz. Towards formal xai: formally approximate minimal explanations of neural networks. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 187–207. Springer, 2023.

[8] S. Beucher. Use of watersheds in contour detection. In Proc. Int. Workshop on Image Processing, Sept. 1979, 1979.

[9] U. Bhatt, A. Weller, and J. M. F. Moura. Evaluating and aggregating feature-based model explanations. In International Joint Conference on Artificial Intelligence, 2020.

[10] C. Brix, M. N. Müller, S. Bak, T. T. Johnson, and C. Liu. First three years of the international verification of neural networks competition (vnn-comp), 2023.

[11] C. Brix, S. Bak, T. T. Johnson, and H. Wu. The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results, 2024. URL https://arxiv.org/abs/2412.19985.

[12] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977. doi: 10.1145/512950.512973.

[13] A. Darwiche and A. Hirth. On the reasons behind decisions. In ECAI 2020, pages 712–720. IOS Press, 2020.

[14] A. Das and P. Rad. Opportunities and challenges in explainable artificial intelligence (xai): A survey. ArXiv, abs/2006.11371, 2020.

[15] J. Deng, W. Dong, R. Socher, L.-J. Li, K. Li, and L. Fei-Fei. Imagenet: A large-scale hierarchical image database. 2009 IEEE Conference on Computer Vision and Pattern Recognition, pages 248–255, 2009.

[16] A.-K. Dombrowski, M. Alber, C. Anders, M. Ackermann, K.-R. Müller, and P. Kessel. Explanations can be manipulated and geometry is to blame. Advances in neural information processing systems, 32, 2019.

[17] D. Doncenco, J. Girard-Satabin, R. Xu-Darme, and Z. Chihani. Supplementary Material for "A dive into formal explainable attributions for image classification", 2025. URL https://doi.org/10.5281/zenodo.16683943.

[18] T. Fel, J. Colin, R. Cadène, and T. Serre. What i cannot predict, i do not understand: A human-centered evaluation framework for explainability methods. Advances in neural information processing systems, 2021.

[19] P. F. Felzenszwalb and D. P. Huttenlocher. Efficient graph-based image segmentation. International Journal of Computer Vision, 2004.

[20] M. Friedman. The use of ranks to avoid the assumption of normality implicit in the analysis of variance. Journal of the American Statistical Association, 32:675–701, 1937.

[21] R. Geirhos, J.-H. Jacobsen, C. Michaelis, R. Zemel, W. Brendel, M. Bethge, and F. A. Wichmann. Shortcut learning in deep neural networks. Nature Machine Intelligence, 2020.

[22] J. Gilmer, N. Ford, N. Carlini, and E. Cubuk. Adversarial examples are a natural consequence of test error in noise. In K. Chaudhuri and R. Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning. PMLR, 2019.

[23] R. Greenblatt, C. Denison, B. Wright, F. Roger, M. MacDiarmid, S. Marks, J. Treutlein, T. Belonax, J. Chen, D. Duvenaud, A. Khan, J. Michael, S. Mindermann, E. Perez, L. Petrini, J. Uesato, J. Kaplan, B. Shlegeris, S. R. Bowman, and E. Hubinger. Alignment faking in large language models, 2024. URL https://arxiv.org/abs/2412.14093.

[24] Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2024. URL https://www.gurobi.com.

[25] K. He, X. Zhang, S. Ren, and J. Sun. Deep residual learning for image
recognition. In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 770–778, 2016.

[26] A. Hedström, L. Weber, D. Krakowczyk, D. Bareeva, F. Motzkus, W. Samek, S. Lapuschkin, and M. M. M. Höhne. Quantus: An explainable ai toolkit for responsible evaluation of neural network explanations and beyond. Journal of Machine Learning Research, 2023.

[27] A. Hedström, L. Weber, S. Lapuschkin, and M. Höhne. A fresh look at sanity checks for saliency maps. In L. Longo, S. Lapuschkin, and C. Seifert, editors, Explainable Artificial Intelligence, pages 403–420, Cham, 2024. Springer Nature Switzerland.

[28] X. Huang and J. Marques-Silva. On the failings of shapley values for explainability. International Journal of Approximate Reasoning, 2024.

[29] A. Ignatiev, N. Narodytska, and J. Marques-Silva. Abduction-based explanations for machine learning models. In AAAI Conference on Artificial Intelligence, 2018.

[30] M. A. Jette and T. Wickberg. Architecture of the slurm workload manager. In D. Klusaček, J. Corbalán, and G. P. Rodrigo, editors, Job Scheduling Strategies for Parallel Processing, pages 3–23, Cham, 2023. Springer Nature Switzerland.

[31] G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International conference on computer aided verification, pages 97–117. Springer, 2017.

[32] G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljić, D. L. Dill, M. J. Kochenderfer, and C. Barrett. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In I. Dillig and S. Tasiran, editors, Computer Aided Verification. Springer International Publishing, Cham, 2019.

[33] B. Kim, M. Wattenberg, J. Gilmer, C. J. Cai, J. Wexler, F. B. Viégas, and R. Sayres. Interpretability beyond feature attribution: Quantitative testing with concept activation vectors (tcav). In International Conference on Machine Learning, 2017.

[34] N. Koenen and M. N. Wright. Toward understanding the disagreement problem in neural network feature attribution. In L. Longo, S. Lapuschkin, and C. Seifert, editors, Explainable Artificial Intelligence, pages 247–269, Cham, 2024. Springer Nature Switzerland.

[35] N. Kokhlikyan, V. Miglani, M. Martin, E. Wang, B. Alsallakh, J. Reynolds, A. Melnikov, N. Kliushkina, C. Araya, S. Yan, and O. Reblitz-Richardson. Captum: A unified and generic model interpretability library for pytorch. ArXiv, abs/2009.07896, 2020.

[36] Y. Lecun, L. Bottou, Y. Bengio, and P. Haffner. Gradient-based learning applied to document recognition. Proceedings of the IEEE, 1998.

[37] A. Lemesle and Z. Chihani. PyRAT — pyrat-analyzer.com. https://pyrat-analyzer.com/, 2024. [Accessed 29-07-2024].

[38] A. Lemesle, J. Lehmann, and T. L. Gall. Neural network verification with pyrat. The Static Analysis Symposia, 2025.

[39] S. M. Lundberg and S.-I. Lee. A unified approach to interpreting model predictions. Advances in neural information processing systems, 2017.

[40] J. Marques-Silva and A. Ignatiev. Delivering trustworthy ai through formal xai. In AAAI Conference on Artificial Intelligence, 2022.

[41] T. Miller. Explanation in artificial intelligence: Insights from the social sciences. Artificial intelligence, 267:1–38, 2019.

[42] A. Miné. Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation. Foundations and Trends® in Programming Languages, 2017.

[43] mnmoustafa and M. Ali. Tiny imagenet. https://kaggle.com/competitions/tiny-imagenet, 2017. Kaggle.

[44] C. Müller, F. Serre, G. Singh, M. Püschel, and M. Vechev. Scaling polyhedral neural network verification on gpus. Proceedings of Machine Learning and Systems, 3, 2021.

[45] M. Nauta, J. Trienes, S. Pathak, E. Nguyen, M. Peters, Y. Schmitt, J. Schlötterer, M. van Keulen, and C. Seifert. From anecdotal evidence to quantitative evaluation methods: A systematic review on evaluating explainable ai. ACM Computing Surveys, 55:1–42, 2022.

[46] F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 2011.

[47] M. T. Ribeiro, S. Singh, and C. Guestrin. “why should i trust you?”: Explaining the predictions of any classifier. Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2016.

[48] M. T. Ribeiro, S. Singh, and C. Guestrin. Anchors: High-precision model-agnostic explanations. In Proceedings of the AAAI conference on artificial intelligence, volume 32, 2018.

[49] Z. Shi, Y. Wang, H. Zhang, J. Yi, and C.-J. Hsieh. Fast certified robust training with short warmup. Advances in Neural Information Processing Systems, 2021.

[50] A. Shrikumar, P. Greenside, and A. Kundaje. Learning important features through propagating activation differences. In D. Precup and Y. W. Teh, editors, Proceedings of the 34th International Conference on Machine Learning, volume 70 of Proceedings of Machine Learning Research, pages 3145–3153. PMLR, 06–11 Aug 2017. URL https://proceedings.mlr.press/v70/shrikumar17a.html.

[51] K. Simonyan, A. Vedaldi, and A. Zisserman. Deep inside convolutional networks: Visualising image classification models and saliency maps. 2014. URL http://arxiv.org/abs/1312.6034.

[52] G. Singh, T. Gehr, M. Püschel, and M. Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POLP):1–30, 2019.

[53] D. Smilkov, N. Thorat, B. Kim, F. B. Viégas, and M. Wattenberg. Smoothgrad: removing noise by adding noise. ArXiv, abs/1706.03825, 2017.

[54] C. Spearman. The proof and measurement of association between two things. The American Journal of Psychology, 1904.

[55] J. Stallkamp, M. Schlipsing, J. Salmen, and C. Igel. The german traffic sign recognition benchmark: a multi-class classification competition. In The 2011 international joint conference on neural networks. IEEE, 2011.

[56] M. Sundararajan, A. Taly, and Q. Yan. Axiomatic attribution for deep networks. In International conference on machine learning. PMLR, 2017.

[57] C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus. Intriguing properties of neural networks. In 2nd International Conference on Learning Representations, 2014.

[58] D. Ulyanov, A. Vedaldi, and V. Lempitsky. Deep image prior. In Proceedings of the IEEE conference on computer vision and pattern recognition, 2018.

[59] A. Vedaldi and S. Soatto. Quick shift and kernel methods for mode seeking. In Computer Vision–ECCV 2008: 10th European Conference on Computer Vision. Springer, 2008.

[60] S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In M. Ranzato, A. Beygelzimer, Y. Dauphin, P. Liang, and J. W. Vaughan, editors, Advances in Neural Information Processing Systems, volume 34, pages 29909–29921. Curran Associates, Inc., 2021.

[61] H. Wu, O. Isac, A. Zeljić, T. Tagomori, M. Daggitt, W. Kokke, I. Refaeli, G. Amir, K. Julian, S. Bassan, et al. Marabou 2.0: a versatile formal analyzer of neural networks. In International Conference on Computer Aided Verification. Springer, 2024.

[62] M. Wu, H. Wu, and C. Barrett. Verix: Towards verified explainability of deep neural networks. Advances in neural information processing systems, 2024.

[63] K. Xu, Z. Shi, H. Zhang, Y. Wang, K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33, 2020.

[64] R. Xu-Darme, J. Benois-Pineau, R. Giot, G. Quénot, Z. Chihani, M.-C. Rousset, and A. Zhukov. On the stability, correctness and plausibility of visual explanation methods based on feature importance. In Proceedings of the 20th International Conference on Content-based Multimedia Indexing, pages 119–125, 2023.

[65] M. D. Zeiler and R. Fergus. Visualizing and understanding convolutional networks. In Computer Vision–ECCV 2014: 13th European Conference, Zurich, Switzerland. Springer, 2014.

[66] H. Zhang, H. Chen, C. Xiao, S. Gowal, R. Stanforth, B. Li, D. Boning, and C.-J. Hsieh. Towards stable and efficient training of verifiably robust neural networks. 2019.