Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations

We appreciate the reviewer's constructive feedback and their acknowledgment of the significance of our work.

Expanding the scope

We thank the reviewer for bringing up this point and will improve its discussion in the final version. We note that while our primary experiments focus on vision classification models, our approach is domain-agnostic and can be applied to other domains. In Appendix D, we provide example experiments in additional domains. For language tasks, we utilized the only language-specific benchmark from the annual neural network verification competition (VNN-COMP [1]), which is based on a medical safety NLP dataset. Certification was achieved over an embedded representation of the input space, ensuring meaning-preserving perturbations. Another example of an expansion can include regression tasks, not just classification. In this case, the provable guarantee would ensure that fixing a subset of features keeps the output prediction within a specified range. We demonstrate this in Appendix D using the real-world, safety-critical Taxi-Net benchmark from Wu et al. (Neurips 2023, [2]). We will enhance our discussion of these extensions, as well as other potential applications, in the body of the final draft.

Design choices for experimental analysis

We selected these specific configurations because they are utilized in the annual neural network verification competition (VNN-COMP [1]). However, in response to the reviewer’s feedback, we will include the additional requested configurations in our final version, with the varying distinct activation functions used for each setting. Our method is also compatible with networks that include residual connections, and we will include an experiment in the final version to highlight this.

Performance trend and additional quantitative measures

We thank the reviewer for these valuable suggestions. We will indeed incorporate additional quantitative measures in the final version, specifically detailing both time per query and time per iteration across our various settings. Due to space limitations in the rebuttal, we provide here only representative results - namely, the average query times in seconds for our different settings in Section E.5.

We appreciate the reviewer’s suggestion to examine the scalability trend in our results and will include dedicated experiments in the final version to explore this aspect more thoroughly. Our current findings indicate that increasing model size leads to an increase in overall generation time. At the same time, this also amplifies the relative benefits of the abstraction-refinement strategy, as larger models tend to produce more significant improvements when using coarser abstractions. To illustrate this effect more clearly, we performed an additional experiment based on the “Marabou” benchmark from VNN-COMP [1]. While our original setup focused solely on the “cifar10_large” model, we now include the “cifar10_medium” and “cifar10_small” variants as well. In this experiment, the abstraction-refinement approach showed relative improvements over the standard method, reducing computation time by 136.46 seconds for the small model, 264.18 seconds for the medium model, and 570.39 seconds for the large model. In the final version, we will include additional experiments that vary model sizes while keeping all other parameters constant, to more clearly illustrate this trend.

Paper clarity improvements

We thank the reviewer for the helpful feedback on these points. In the final version, we will include a running example to help clarify our definitions. Due to space limitations, our current detailed explanation of the sufficiency proofs and abstraction appears primarily in Appendix A, with only a concise summary in the main text. As recommended, we will integrate portions of this discussion into the main body and improve the overall presentation of these topics.

[1] First three years of the international verification of neural networks competition (VNN-COMP) (Brix et al., STTT 2023)

[2] Verix: Towards Verified Explainability of Deep Neural Networks (Wu et al., Neurips 2023)

We appreciate the reviewer's constructive feedback and their acknowledgment of the significance of our work.

Enumeration of minimal sufficient explanations

We thank the reviewer for the insightful comment and agree that this is a highly relevant direction, particularly in the context of formal explainable AI. We touch on a related aspect in Appendix C, where we explore how varying feature orderings can influence the explanations generated by our algorithm. Intuitively, running the algorithm over different orderings yields different explanations. A more advanced strategy could start with an initial explanation and iteratively perturb specific features - e.g., replacing features in the explanation with those from its complement - to produce alternative explanations. Another possible direction is to explicitly maximize the divergence between explanations to encourage diversity, for instance by using reverse orderings. While enumerating all possible explanations is computationally intensive, one could potentially leverage the duality with the minimum hitting set (MHS) problem [1] to generate many contrastive explanations and iterate over diverse MHSs. However, such an approach may not scale well to large input domains due to the sheer number of possible contrastive explanations. We appreciate the importance of this point and will incorporate a discussion of it into both the main text and appendix of the final version, and highlight it as an interesting direction for future research.

Additional weaknesses, comments and suggestions

We first acknowledge the weakness pointed out by the reviewer regarding the scalability challenges in producing provably sufficient and minimal explanations for neural networks. However, as both the reviewer and other reviewers have noted, our method represents a significant improvement over prior approaches tackling the same task - offering better computation time, support for larger model sizes, and more concise explanations. We also refer the reviewer to Appendix D, where we demonstrate the generalizability of our method across additional settings. This includes evaluation on a language benchmark derived from a medical NLP dataset, where certification is conducted using meaning-preserving perturbations within an embedded input space, as well as in a regression setting. In the latter, we use the real-world, safety-critical Taxi-Net benchmark to show that fixing certain input features keeps predictions within a target range.

Moreover, we highly appreciate the reviewer’s many thoughtful comments and suggestions, which we will incorporate into the final version and will help us improve the clarity of our work. Regarding Algorithm 2, the counterexample is obtained directly from the verifier but can also be extracted through an external adversarial attack, and we will clarify this accordingly. By a standard algorithm, we refer to a typical greedy approach, which does not incorporate abstraction-refinement, such as the one presented in Algorithm 1 and used in prior works (e.g., the method by Wu et al., NeurIPS 2023 [2]). Importantly, we emphasize that our abstraction-refinement approach is agnostic to the specific technique used to generate explanations and is applicable to any method that derives explanations through multiple certification queries. We agree that this point should be more clearly articulated in the final version.

We agree with the reviewer’s comment on the importance of improving the discussion of the abstraction methodology in the main text. To enhance clarity, we will relocate portions of the detailed expedition of the abstraction technique from Appendix A to Section 3 and refine the overall discussion accordingly. Additionally, the standard deviation is computed as the square root of the mean of the squared deviations from the average, normalized by dividing by the total number of data points used in each separate experiment. We will also address the notation issues raised and emphasize the non-uniqueness of the generated subsets. While this aspect is partially covered in Appendix C, which discusses different feature orderings, we will ensure it is explicitly highlighted and discussed in the main text as well. Thank you for bringing these valuable points to our attention!

Lastly, we appreciate the reviewer’s interesting point regarding the non-monotonicity that is observed in Table 1. This effect is due to the experiment's timeout: without it, the behavior remains monotonic (see Fig. 6). However, with the timeout, larger abstraction configurations can get stuck earlier in the algorithm, causing them to produce larger explanations within the time limit, which explains the observed slight non-monotonic behavior. We will clarify this interesting point in our final version.

[1] From Contrastive to Abductive Explanations and Back Again (Ignatiev et al., KR 2021)

[2] Verix: Towards Verified Explainability of Deep Neural Networks (Wu et al., Neurips 2023)

We appreciate the reviewer's constructive feedback and their acknowledgment of the significance of our work.

Extension to different $\epsilon_p$ perturbations

We thank the reviewer for raising this important point. As correctly noted, larger $ϵ_p$ perturbations yield stronger sufficiency guarantees but may result in larger explanations. We chose the perturbation levels in this paper based on those commonly used in the annual Neural Network Verification Competition (VNN-COMP [1]), but our method is general and can be applied to any perturbation. We already include an ablation study in Appendix C, which we’ll reference more clearly. Per the reviewer’s suggestion, we’ll expand it with additional benchmarks, perturbation levels, and visualizations.

Qualitative analysis and the importance of minimality

We agree that this is an important point, and will include further qualitative assessments in the final version. As a preliminary example, we share one illustrative case.

First, image (a) highlights the importance of minimality. For example, the interior of the forward sign (red frame in image (c)) is not included in our explanation, and the edges alone are sufficient for classification. This shows the interior pixels are irrelevant and can be excluded without affecting the prediction. In contrast, non-minimal sufficient subsets (e.g., the other examples) include unnecessary features. To better grasp the significance of small or minimal explanations, one can consider the extreme case where the entire image is chosen as the explanation: although it is clearly sufficient, it is neither minimal nor informative.

Second, image (b) shows that fixing the provably sufficient subset ensures robustness: any change in the complement $\bar{S}$ within the domain doesn't alter the classification. This contrasts with heuristic subsets, where changes in the complement can flip the prediction - revealing their limitations. The explanation also matches human intuition, as the highlighted region (the triangular forward sign) alone justifies the predicted class, unlike the much less clear heuristic explanations.

Additional quantitative analysis and scope

Since our work focuses on sufficient explanations rather than the more widely studied additive attributions, certain commonly used evaluation metrics - such as infidelity [2], which are specifically designed for additive forms - are not directly applicable. Adapting such metrics for sufficiency-based explanations would require significant modifications and, on its own, constitutes an interesting direction for future work. Therefore, we followed established conventions in the literature [e.g., 3–5] for evaluating sufficiency-based explanations, relying on the three widely accepted metrics in this area: generation time, sufficiency, and conciseness.

That said, we appreciate the reviewer’s interesting idea of assessing how well sufficient explanations localize class-discriminative features. We tested this using object-detection ground truth from GTSRB and found that indeed 93.33% of our method’s explanation pixels aligned with annotated regions, outperforming Anchors (60.36%). We thank the reviewer for this idea and will include a detailed experiment on this point in the final version.

Lastly, while our main experiments focus on vision classification models, our approach is domain-agnostic and can extend to other domains. Appendix D includes examples of both language and regression tasks. For language, we use the only VNN-COMP [1] language benchmark based on a medical NLP dataset, certifying meaning-preserving perturbations via an embedded input space. For regression, we use the real-world safety-critical Taxi-Net benchmark used in Wu et al. (Neurips 2023, [3]), showing that fixing input features keeps predictions within a target range. We will expand on these extensions and additional applications in the final draft.

[1] First Three Years of the International Verification of Neural Networks Competition (VNN-COMP) (Brix et al., STTT 2023)

[2] On the (In) Fidelity and Sensitivity of Explanations (Yeh et al., Neurips 2019)

[3] Verix: Towards Verified Explainability of Deep Neural Networks (Wu et al., Neurips 2023)

[4] On Guaranteed Optimal Robust Explanations for NLP Models (La Malfa et al., IJCAI 2021)

[5] Abduction-based Explanations for Machine Learning Models (Ignatiev et al., AAAI 2019)

We thank the reviewer for their valuable and constructive feedback.

Improving the motivation behind the work

We agree that the motivation for obtaining explanations with provable guarantees, as well as the importance of the specific guarantees we provide, can be better articulated. We will make sure to better clarify this in the final version. Please see our detailed response on this point below:

General motivation. Explanations for black-box models are often sought to enhance user trust in the model. For instance, consider a scenario where a medical professional must trust a black-box model to diagnose a disease from MRI scans. An explanation can help them decide whether to rely on the prediction - especially if it highlights medically relevant image regions. However, if the explanation is untrustworthy and lacks guarantees - such as presenting a subset that isn’t truly sufficient - it can misrepresent the model’s reasoning, leading the medical professional to place misplaced trust in it, potentially resulting in harmful outcomes.

Such scenarios have sparked increasing interest in the literature in developing explanations that come with provable guarantees [see, e.g., 1–8]. In this context, explanations that are both provably minimal and sufficient have gained significant attention as a highly sought-after form of provable explanation [see, e.g., 1-8, among others]. The key idea is to identify small subsets of features that, even when all other features take arbitrary values, still preserve the model’s prediction. This ensures the subset’s certified sufficiency, helping users understand the reasoning behind the prediction and disregard irrelevant features.

Scope. While we agree that the guarantees our method provides inherently face scalability challenges - due to their reliance on verification, as is with all approaches tackling this task - we emphasize the significant relative improvements our approach achieves over previous methods. As several reviewers have also positively noted, our contributions are particularly notable in terms of reduced computation time, the generation of smaller explanations, and the ability to handle larger models. As the field of neural network verification continues to progress rapidly [9-11], our method - offering a significant, orthogonal enhancement for generating explanations using these tools - will similarly evolve.

Moreover, to further show the generality of our results, we present experiments on two additional benchmarks in Appendix D: (1) the only language task from the annual neural network verification competition (VNN-COMP, [11]), based on a medical safety NLP dataset, which uses meaning-preserving perturbations in an embedded input space; and (2) a regression task, where our guarantees ensure output stability, evaluated on the real-world, safety-critical Taxi-Net benchmark, evaluated in Wu et al. (Neurips 2023, [2]).

Finally, in response to the reviewer’s comment and reviewer pUMo’s feedback, we will include additional qualitative examples in the final version to better motivate our work. As part of our response to reviewer pUMo, we have added a small illustrative visualization, which we also plan to incorporate - along with other visualizations - into the final version.

We thank the reviewer for highlighting this important point and will significantly enhance our discussion of these aspects in the final version.

[1] Delivering Trustworthy AI Through Formal XAI (Marques Silva et al., AAAI 2022)

[2] Verix: Towards Verified Explainability of Deep Neural Networks (Wu et al., Neurips 2023)

[3] Abduction-Based Explanations for Machine Learning Models (Ignatiev et al., AAAI 2019)

[4] On Guaranteed Optimal Robust Explanations for NLP Models (La Malfa et al., IJCAI 2021)

[5] Model Interpretability Through the Lens of Computational Complexity (Barcelo et al., Neurips 2020)

[6] Computing Abductive Explanations for Boosted Trees (Audemard et al., AISTATS 2023)

[7] Explanations for Monotonic Classifiers (Marques Silva et al., ICML 2020)

[8] Foundations of Symbolic Languages for Model Interpretability (Arenas et al., Neurips 2021)

[9] Beta-Crown: Efficient Bound Propagation with Per-Neuron Split Constraints for Neural Network Robustness Verification (Wang et al., Neurips 2021)

[10] Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes (Zhou et al., Neurips 2024)

[11] First Three Years of the International Verification of Neural Networks Competition (VNN-COMP) (Brix et al., STTT 2023)