Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Faster Verified Explanations for Neural Networks

Alessandro De Palma, Greta Dolcetti, Caterina Urban

TL;DR

The paper tackles the scalability challenge of verified explanations for neural networks by introducing FaVeX, a batch-sequential algorithm that accelerates robustness queries and incorporates verifier incompleteness through verifier-optimal robust explanations. By partitioning features into invariants, counterfactuals, and unknowns, it provides a practical, hierarchical explanation that adapts to incomplete verification. FaVeX combines batch processing, incremental branch-and-bound reuse, and restricted-space counterfactual search to achieve large-scale explanations on networks with hundreds of thousands of activations, while also delivering improved counterfactual discovery on larger CNNs. The work demonstrates substantial speedups over prior methods and shows that verifier-optimal explanations offer meaningful, scalable insights for safety-critical models. Overall, it advances formal explainability toward real-world applicability in vision tasks and beyond.

Abstract

Verified explanations are a theoretically-principled way to explain the decisions taken by neural networks, which are otherwise black-box in nature. However, these techniques face significant scalability challenges, as they require multiple calls to neural network verifiers, each of them with an exponential worst-case complexity. We present FaVeX, a novel algorithm to compute verified explanations. FaVeX accelerates the computation by dynamically combining batch and sequential processing of input features, and by reusing information from previous queries, both when proving invariances with respect to certain input features, and when searching for feature assignments altering the prediction. Furthermore, we present a novel and hierarchical definition of verified explanations, termed verifier-optimal robust explanations, that explicitly factors the incompleteness of network verifiers within the explanation. Our comprehensive experimental evaluation demonstrates the superior scalability of both FaVeX, and of verifier-optimal robust explanations, which together can produce meaningful formal explanation on networks with hundreds of thousands of non-linear activations.

Faster Verified Explanations for Neural Networks

TL;DR

The paper tackles the scalability challenge of verified explanations for neural networks by introducing FaVeX, a batch-sequential algorithm that accelerates robustness queries and incorporates verifier incompleteness through verifier-optimal robust explanations. By partitioning features into invariants, counterfactuals, and unknowns, it provides a practical, hierarchical explanation that adapts to incomplete verification. FaVeX combines batch processing, incremental branch-and-bound reuse, and restricted-space counterfactual search to achieve large-scale explanations on networks with hundreds of thousands of activations, while also delivering improved counterfactual discovery on larger CNNs. The work demonstrates substantial speedups over prior methods and shows that verifier-optimal explanations offer meaningful, scalable insights for safety-critical models. Overall, it advances formal explainability toward real-world applicability in vision tasks and beyond.

Abstract

Verified explanations are a theoretically-principled way to explain the decisions taken by neural networks, which are otherwise black-box in nature. However, these techniques face significant scalability challenges, as they require multiple calls to neural network verifiers, each of them with an exponential worst-case complexity. We present FaVeX, a novel algorithm to compute verified explanations. FaVeX accelerates the computation by dynamically combining batch and sequential processing of input features, and by reusing information from previous queries, both when proving invariances with respect to certain input features, and when searching for feature assignments altering the prediction. Furthermore, we present a novel and hierarchical definition of verified explanations, termed verifier-optimal robust explanations, that explicitly factors the incompleteness of network verifiers within the explanation. Our comprehensive experimental evaluation demonstrates the superior scalability of both FaVeX, and of verifier-optimal robust explanations, which together can produce meaningful formal explanation on networks with hundreds of thousands of non-linear activations.

Paper Structure

This paper contains 20 sections, 1 theorem, 3 equations, 6 figures, 11 tables, 5 algorithms.

Table of Contents

  1. Introduction
  2. Optimal vs. Verifier-Optimal Robust Explanations
  3. Background
  4. Neural Network Verification
  5. Verified Explanations
  6. Verifier-Optimal Robust Explanations
  7. FaVeX: Faster Verified Explanations
  8. Computing (Verifier-Optimal) Robust Explanations
  9. Incremental Branch-and-Bound Verification
  10. Restricted-Space Counterfactual Search
  11. Implementation
  12. Verifier
  13. FaVeX
  14. Experimental Evaluation
  15. Experimental Setting
  16. ...and 5 more sections

Key Result

Lemma 4

Given a classifier $f : \mathbb{R}^{d} \rightarrow \mathbb{R}^{k}$, an input vector $\mathbf{x} \in \mathbb{R}^d$, a perturbation radius $\epsilon > 0$, and a complete verifier $\overline{v} : \mathcal{Q} \rightarrow \{-1, 1\}$, a $v$-optimal robust explanation (Definition def:v-optimal-x) is an opt

Figures (6)

  • Figure 1: Comparison of standard (a) and verifier-optimal (b) robust explanations ($\epsilon = 0.25$) of the first image in the MNIST testing dataset, where counterfactuals are highlighted in yellow, unknowns in blue, and invariants are not highlighted.
  • Figure 2: Example of computing a standard (optimal) robust explanation on 9 features. The verification steps proceed from left to right; the dotted box indicates the feature under analysis, dark grey shows the invariants, yellow shows the explanations for which a counterexample has been found, and question marks denote features for which a timeout has been encountered. The final results of the analysis can be seen in the rightmost column.
  • Figure 3: Example of computing a verifier-optimal robust explanation on 9 features. The verification steps proceed from left to right; the dotted box indicates the feature under analysis, dark grey shows the invariants, blue shows the unknowns, yellow shows the explanations for which a counterexample has been found, and question marks denote features for which a timeout has been encountered. The final results of the analysis can be seen in the rightmost column.
  • Figure 4: Example of $v$-optimal robust explanation.
  • Figure 5: Example of search tree explored by branch-and-bound.
  • ...and 1 more figures

Theorems & Definitions (4)

  • Definition 1: Robust Explanation
  • Definition 2: Optimal Explanation
  • Definition 3: Verifier-Optimal Robust Explanation
  • Lemma 4