VeriX: Towards Verified Explainability of Deep Neural Networks

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.

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. - 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. - 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? - 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?

Questions

As mentioned above, I would be interested in the authors thoughts about the following questions: 1. Can the approach be usefully scaled to large models with millions of parameters? 2. How can such explanations be useful to developers? How can developers deploy the algorithm in practice to aid in constructing more trustworthy models? 3. 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? -------------------- Edits after author response: Based on author responses to my questions, I have increased my score to 7

Rating

7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

4 excellent

Presentation

4 excellent

Contribution

3 good

Limitations

Yes, the authors clearly discuss the limitations of their approach in the paper.

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. One 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.

Strengths

- Computing formal local explanations achieved with applying robustness queries to the model is novel - The proposed solution offers formal guarantees of soundness and precision of the resulting explanations in contrast to popular post-hoc XAI approaches like LIME, SHAP, Anchor that are heuristic in their nature - Moreover, the paper propose a nice trick for the traversal order of the features which allows in practice to generate smaller explanations, and might be further exploited to speed up the extraction of the explanations with using other algorithms like quickplain to drop quickly group of irrelevant features (instead of a single feature at time with the linear algo 1) - 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: JOHN 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. (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.) - Section 3.2 ( Theorem 3.3, 3.4 and proposition 3.5) rediscovers what has been established for at least 30 years. The 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. - 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 are dual, and this has been shown in XAI: A. Ignatiev "On Relating Explanations and Adversarial Examples." NeurIPS 2019.

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. - 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? - 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? - can you propose an efficient algorithm to enumerate optimal explanations? - how can we compute efficiently a ( single) counterfactual based on robustness checking, and directly given input data without generating (optimal) explanations ?

Rating

5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.

Confidence

5: You are absolutely certain about your assessment. You are very familiar with the related work and checked the math/other details carefully.

Soundness

3 good

Presentation

3 good

Contribution

2 fair

Limitations

- The paper failed to show clearly and formally the duality between explanations and counterfactuals - The outlined algorithm reports the basic version of the linear search algorithm and does not implement possible optimization/refinement to reduce the total number of oracle calls, for example it does not discuss how can be AEx exploited to improve the procedure. Remarks: - 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. Besides, 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. - 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.

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.

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. 2. 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. 3. 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? 4. 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.

Questions

The questions correspond to the weaknesses. 1. What is the runtime of the experiments? Have the authors compare the runtimes of using different nn verification tools? 2. How strong do \epsilon and \delta influence the results? 3. 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?

Rating

5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

4 excellent

Presentation

2 fair

Contribution

2 fair

Limitations

The paper It is declared in this paper that the proposed algorithm only produces local optimal solutions. The limitation is not addressed.

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.

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.

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.

Questions

- Could you provide more details on the scalability of VERIX, especially for larger and more complex models? - How does VERIX perform on non-image data? Were any experiments conducted using such data? - Could you discuss the potential trade-offs in using VERIX, especially regarding computational cost and complexity?

Rating

7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.

Confidence

3: You are fairly confident in your assessment. It is possible that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.

Soundness

3 good

Presentation

3 good

Contribution

3 good

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.

Response to rebuttal

Thank you for the detailed response to my questions and for pointing me towards the material in the appendix. I am happy to keep my score but I have two follow-up comments. 1. My question about how does one trust the explanation referred to the fact that for a fixed model $f$ and fixed input $x$, the presented algorithm can generate various explanations depending on the traversal order (as demonstrated by Figures 5 and 10). Intuitively, it would seem that when $f$ predicts $y$ on $x$, there ought to be a unique explanation about the behavior of $f$. To put it differently, should we think of the explanation generated using a random traversal order as a "valid" explanation? If yes, then the explanation in the 4th column of Figure 5(a) is as valid as the explanation in 3rd column of Figure 5(a), and we can either conclude that the model is very badly behaved based on the random traversal explanation or well-behaved based on the sensitivity traversal explanation. Why is the explanation generated by sensitivity-based traversal order considered more trustworthy? I think the answer is that the size of an optimal robust explanation is inversely related to its trustworthiness. So, the cardinality-minimal explanation is the most trustworthy, and one can define an order on the trustworthiness of the explanations as the inverse order of their sizes. I think a discussion on the ordering of explanations would strengthen the paper. Related to this, I have a question -- is the intersection of various explanations generated by random traversal a "valid" explanation? If so, then the empty explanation would be the most trustworthy one (based on the previous argument). But my guess is that the intersection of explanations is not a valid explanation; in fact, I think it is not even an optimal robust explanation as per Definition 2.1 and my suggestion would be to remove Fig 10(c) from the paper because I am not sure what it conveys. 2. I think the results presented in Fig 11 are an important aspect of the empirical evaluation and it would be nice if, in addition to the figure, quantitative results about the size of the explanations when using sound but incomplete verifiers were provided (similar to the *size* column in Table 2).