Abstracting and Refining Provably Sufficient Explanations of Neural Network Predictions

We thank the reviewer for the valuable comments. See our response below.

Corollary 1 is not entirely self-contained

We thank the reviewer for highlighting this point. Given the significance of Corollary 1, we agree that making the proof more self-contained, building on the work of Ladner et al., would enhance the paper's overall clarity and accessibility. We will incorporate this change in the final version.

Paper title implies that the contribution focuses on subset sufficiency, but proving minimality appears more challenging

The core idea behind proving that our abstraction-refinement strategy achieves a provably sufficient and minimal explanation is divided into two key challenges. The first challenge lies in recognizing that a neuron-merging abstraction technique, such as the one discussed by Ladner et al., can be used to abstract a neural network while ensuring that a provably sufficient explanation for the abstract model remains provably sufficient for the original model. As the reviewer rightly pointed out, the second significant challenge is applying such an abstraction method to derive explanations that are not only provably sufficient but also provably minimal with respect to the original model. While a sufficient explanation of the abstract model remains sufficient for the original model, it does not necessarily ensure provable minimality. To address this, we introduce the concept of a “provably refined network” component, enabling the gradual refinement of both the neural network and its explanation. This process is highlighted in Algorithm 2 of the paper. We agree with the reviewer that emphasizing the “minimality” aspect of our provable explanations in the paper title could enhance clarity and better reflect the contributions of the work. Thank you for bringing this to our attention.

Extending the results to arbitrary modifications of the complement

Extending the results to arbitrarily large modifications of the complement can be obtained by expanding the bounds over the input features during the certification process. Since our method is agnostic to these bounds, this extension is naturally feasible. Regarding scalability, on the one hand, each verification query becomes more computationally demanding as it involves certifying a much larger domain. On the other hand, this broader setting generates larger explanations, due to the increased likelihood of subsets failing to maintain sufficiency, and since fewer verification queries are required, the overall runtime may not increase significantly. However, it is worth mentioning that since the obtained subsets may be significantly large, the generated explanations may be less meaningful. To illustrate this, we conducted an initial experiment on MNIST, comparing perturbations within a small domain of 0.01 to those in the entire [0,1] domain. The results are as follows:

Building on this remark and the questions raised by reviewer t2CN, we will include an additional analysis in our paper. This analysis will evaluate our method's performance under varying $\epsilon$ perturbations across all benchmarks, offering insights into the trade-offs between sufficiency and runtime. An initial experiment on MNIST yielded the following results:

In the final version, we will include the complete experiment across all benchmarks. Thank you for highlighting this point.

Thank you for your answer. I appreciated your new experiments on the increasing radius. I have one final doubt regarding your second answer. I would appreciate it if you could clarify the following point.

[...] The first challenge lies in recognizing that a neuron-merging abstraction technique, such as the one discussed by Ladner et al., can be used to abstract a neural network while ensuring that a provably sufficient explanation for the abstract model remains provably sufficient for the original model [...]

What do you mean, practically, by "recognizing"? It seems more of a motivation behind the paper's idea rather than a key contribution to the paper. My concern is further supported by the fact that Corollary 1 appeared more like a straightforward application of the result of [1], without highlighting the contribution provided by the authors. Maybe, uploading your revised version of Corollary 1, where you mentioned that you clarified this, would help.

Thank you again for your answer.

We thank the reviewer for the insightful comments. Our responses are provided below.

Extension to other non-image model types such as language models, and tabular data

Our method is data-type agnostic and can be applied to other model types, such as those handling text or tabular data. We chose to focus on vision tasks due to their suitability for visualizing results and the computational challenges they present, given the relatively large input space. A key consideration in language tasks is that an $\epsilon$ perturbation may significantly alter the semantic meaning of the input, making it less meaningful compared to vision tasks. An alternative approach is to apply $\epsilon$ perturbations within a latent space.

We conducted an initial experiment using our method on the SafeNLP language task from the annual Neural Network Verification Competition [5]. This task, the only language-focused challenge in the competition, is based on the medical safety NLP dataset. Certification with respect to $\epsilon$ was achieved over an embedded representation of the input space, allowing for meaning-preserving perturbations. The experiment produced provably minimal and sufficient explanations, achieving a computation time of 0.66 ± 0.22 seconds and an explanation size of 6.67 ± 5.06. We appreciate the reviewer's suggestion to explore this direction and will include a comprehensive experiment in the final version of our paper to demonstrate our method's applicability to this benchmark.

Another possible extension of our method is to regression tasks and not just classification. The provable guarantee here would be to satisfy that fixing the subset $S$ determines that the prediction remains within some $\delta$ range. Following a suggestion by reviewer eaKy, we demonstrated this on the real-world, safety-critical Taxi-Net benchmark employed by the work of Wu et al. [5]. The results demonstrate that our method produces explanations for this setting with an average computation time of 35.71 ± 3.71 seconds and an average explanation size of 699.30 ± 169.34, marking a significant improvement over the outcomes reported by Wu et al.

We appreciate the reviewer for bringing up this point and will incorporate both of these experiments, demonstrating potential extensions of our method, into the final version.

Scaling the framework to larger architectures

Obtaining provable sufficient explanations indeed depends on neural network verification queries, which currently constrain the scalability of this approach for SOTA architectures. However, with rapid advancements in verification techniques [1 - 4, and as explained below], ongoing improvements in scalability will directly enhance the applicability of our method. Compared to other methods addressing the same task of providing provably sufficient explanations for neural network predictions [5 - 7], our abstraction-refinement approach is significantly more scalable. This is demonstrated not only by the substantial efficiency improvements highlighted in the experiments section but also by the generation of explanations over much larger models. For instance, our approach handles notably larger models compared to recent work providing provably sufficient explanations (Wu et al., NeurIPS 2023) [5], which follows a "traditional" methodology (i.e., it does not leverage our abstraction-refinement technique).

Providing background on neural network verification

Neural network verification is an active research area (e.g., [1–4]), with recent advancements in scaling methods like branch-and-bound [1,2,4] and abstract interpretation [3,4]. Our neuron-merging abstraction method is verification-agnostic, enhancing scalability in a complementary way. In the final version, we will include a detailed overview of recent advancements to improve accessibility. Thank you for highlighting this.

We appreciate the reviewer’s valuable comments. See our responses below.

Reliance on neural network verification and extension to additional benchmarks and domains, such as Taxinet

We agree and acknowledge that any approach seeking to deliver provably sufficient explanations is naturally limited by the scalability challenges of neural network verifiers [1,2,3]. Nonetheless, progress in this field is advancing rapidly [4,5], and as the reviewer noted, our abstraction-refinement methodology provides a substantial improvement in the capability of using such methods to obtain provable explanations for neural networks. Additionally, we note that the benchmarks used in our experiments are more than one order of magnitude larger than those utilized in the notable work by Wu et al. (NeurIPS 2023, [1]), highlighting the improvements of our method in this regard as well.

Additionally, similar to Wu et al., our framework can be adapted to regression tasks by verifying whether fixing a subset $S$ keeps the prediction within a specified $\delta$ range. Based on the reviewer's suggestions, we conducted an experiment using our approach on the TaxiNet benchmark. The results show that our method generates explanations for this setting with an average computation time of 35.71 ± 3.71 seconds and an average explanation size of 699.30 ± 169.34, representing a significant improvement compared to the results reported by Wu et al. We appreciate the reviewer’s suggestion to extend our results for this benchmark and will include a detailed analysis in the final version.

Following another suggestion from the reviewer, we evaluated our method on the SafeNLP language task from the annual Neural Network Verification Competition [5]. This task, the only language task in the contest, is trained on the medical safety NLP dataset. The $\epsilon$ certification is achieved over an embedding of the input space, enabling meaning-preserving perturbations. Our experiments yielded the following results: an average computation time of 0.66 ± 0.22 seconds and an average explanation size of 6.67 ± 5.06. We appreciate the reviewers' suggestions and will incorporate an extended experiment on this benchmark in the final version to demonstrate the applicability of our method across additional domains.

Abstraction risks oversimplifying models to a degree where explanations are uninformative

We agree that this might partially occur at very low reduction rates, where the explanations remain provably sufficient at each abstraction level for the original model but are not necessarily provably minimal. However, our evaluations demonstrate that even at slightly higher reduction rates - still considerably smaller than the original network (such as around 20%-30% of the non-linear activations) - the provided explanations closely match those generated for the original model. This highlights minimal information loss in this context even at moderately higher reduction rates. This characteristic is, in fact, the core insight enabling our method to greatly enhance explanation generation efficiency, as most features are validated within coarser abstractions.

Comparison to additional XAI benchmarks

To ensure a fair comparison, our generated explanations should be evaluated against methods that also aim to identify subsets intended to be sufficient. This stands in contrast to most existing XAI techniques, such as classic additive feature attribution methods or many gradient-based methods, which do not focus on obtaining sufficient subsets and are therefore not directly comparable. Within this context, we believe that the comparisons in our work are thorough, as they include evaluations against the two most prominent heuristic approaches as well as traditional provable methods.

However, in response to the reviewer’s comment, as well as the suggestions from reviewers t2CN and ovvZ, we will incorporate additional experiments to evaluate our approach across additional configurations. These experiments will include brute-force occlusion, provable explanations with varying feature orderings (based on descending importance in different additive attributions), and feature selection within an additive feature attribution framework. Preliminary results comparing our approach to brute-force occlusion revealed that the average subset sufficiency of the latter is 19%, comparable to heuristic methods like Anchors and SIS, with an explanation size of 14.92 ± 8.64. In contrast, our method naturally ensures 100% sufficiency.

Dear Authors,

Thank you for your thoughtful response. Similar to my works, I find this research demonstrates significant potential in utilizing formal methods for explainable AI. And I found it inspiring. I thoroughly enjoyed reading your paper and appreciate the effort you have put into expanding the dataset beyond my earlier suggestions, as my biggest concerns regarding scalability to other datasets and models are somewhat addressed.

I do not have any further questions and would like to maintain my score as it is if the paper revision is reflected accordingly.

We appreciate the reviewer’s valuable and thoughtful comments. Please find our responses below.

The practicality of the approach and exploring potential trade-offs between sufficiency and runtime.

Certifying the provable sufficiency of an explanation depends on the use of a neural network verifier, which currently poses scalability challenges. However, advancements in this area are rapid [1,2], and our approach significantly outperforms competing methods for the same task [e.g., 3 - Wu et al., Neurips 2023], including substantial improvements in runtime (as highlighted in the experiments section) and in handling significantly larger models. While methods such as SIS and Anchors are generally more scalable since they do not rely on verifiers, they cannot guarantee provable sufficiency. As shown in the experiments section, fewer than 20% of the subsets generated by these methods were sufficient, whereas our method consistently produces provably sufficient subsets by design.

However, we do agree with the reviewer that discussing certain trade-offs is worthwhile, and we will include a thorough discussion of this in our final draft. Here is a brief overview:

Sufficiency-runtime tradeoff: A potential sufficiency-scalability trade-off lies in the size of the $\epsilon$ ball for explanation verification. Smaller $\epsilon$ balls improve scalability but limit sufficiency verification to narrower domains. We performed an initial MNIST experiment with small $\epsilon$ perturbations, which showed how this reduction impacts computation time.

In the final draft, we will provide a thorough analysis of this tradeoff, determined by the $\epsilon$ perturbation, across all our benchmarks.

Minimality-runtime tradeoff: Another possible trade-off concerns minimality. Our approach shows that provably sufficient explanations can be achieved at varying levels of abstraction. Even with low reduction rates (e.g., reducing 90% of non-linear activations), many input dimensions can be verified, yielding a concise subset. Users can halt the abstraction-refinement process early, generating a provably sufficient (though non-minimal) explanation with significantly higher efficiency - requiring only ~10% of the computation time compared to the full algorithm. We thank the reviewer for raising this and will highlight it in the final version.

Methods for abstraction in additive attributions and occlusion-based approaches should be referenced

We acknowledge the reviewer's emphasis on the importance of addressing methods, such as the notable work by Ancona et al., which employ probabilistic or uncertainty-based abstractions of neural networks to constrain additive attribution fidelity. However, we note that while these works focus on probabilistic guarantees, our method provides a much stronger, strict formal guarantee over entire continuous domains. To our knowledge, this is the first abstraction algorithm over neural networks to offer explanations with such guarantees. Our method introduces additional novelty through the refinement component, which progressively relaxes the abstraction constraints, and hence also ensures provable minimality guarantees.

Similarly, we acknowledge that occlusion-based methods, such as those by Zeiler et al., are also relevant for their focus on feature subsets, and we will discuss them as related work. However, we do note a fundamental difference between occlusion-based methods and the formal guarantees provided by our approach. Specifically, occlusion methods typically rely on a fixed auxiliary baseline for the occluded complement, whereas our method ensures the strict sufficiency of the derived subset across an entire continuous domain, offering significantly stronger formal guarantees.