Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficiently Computing Compact Formal Explanations

Min Wu, Xiaofu Li, Haoze Wu, Clark Barrett

TL;DR

VeriX+ tackles the challenge of producing minimal, formally guaranteed explanations for neural networks under bounded perturbations. It fuses bound-propagation-based sensitivity for compact explanations with batch-oriented traversals (binary search and QuickXplain adaptations) and a confidence-ranking heuristic to accelerate generation, achieving sizable gains on standard benchmarks and real-world tasks. The approach also demonstrates applicability to transformers and practical scenarios such as autonomous aircraft taxiing and sentiment analysis, with additional insights into adversarial training and OOD detection. Overall, VeriX+ advances scalable, verifiable explanations and highlights their practical value in safety-critical AI contexts.

Abstract

Building on VeriX (Verified eXplainability, arXiv:2212.01051), a system for producing optimal verified explanations for machine learning models, we present VeriX+, which significantly improves both the size and the generation time of formal explanations. We introduce a bound propagation-based sensitivity technique to improve the size, and a binary search-based traversal with confidence ranking for improving time -- the two techniques are orthogonal and can be used independently or together. We also show how to adapt the QuickXplain algorithm to our setting to provide a trade-off between size and time. Experimental evaluations on standard benchmarks demonstrate significant improvements on both metrics, e.g., a size reduction of $38\%$ on the GTSRB dataset and a time reduction of $90\%$ on MNIST. We demonstrate that our approach is scalable to transformers and real-world scenarios such as autonomous aircraft taxiing and sentiment analysis. We conclude by showcasing several novel applications of formal explanations.

Efficiently Computing Compact Formal Explanations

TL;DR

VeriX+ tackles the challenge of producing minimal, formally guaranteed explanations for neural networks under bounded perturbations. It fuses bound-propagation-based sensitivity for compact explanations with batch-oriented traversals (binary search and QuickXplain adaptations) and a confidence-ranking heuristic to accelerate generation, achieving sizable gains on standard benchmarks and real-world tasks. The approach also demonstrates applicability to transformers and practical scenarios such as autonomous aircraft taxiing and sentiment analysis, with additional insights into adversarial training and OOD detection. Overall, VeriX+ advances scalable, verifiable explanations and highlights their practical value in safety-critical AI contexts.

Abstract

Building on VeriX (Verified eXplainability, arXiv:2212.01051), a system for producing optimal verified explanations for machine learning models, we present VeriX+, which significantly improves both the size and the generation time of formal explanations. We introduce a bound propagation-based sensitivity technique to improve the size, and a binary search-based traversal with confidence ranking for improving time -- the two techniques are orthogonal and can be used independently or together. We also show how to adapt the QuickXplain algorithm to our setting to provide a trade-off between size and time. Experimental evaluations on standard benchmarks demonstrate significant improvements on both metrics, e.g., a size reduction of on the GTSRB dataset and a time reduction of on MNIST. We demonstrate that our approach is scalable to transformers and real-world scenarios such as autonomous aircraft taxiing and sentiment analysis. We conclude by showcasing several novel applications of formal explanations.
Paper Structure (32 sections, 2 theorems, 2 equations, 17 figures, 14 tables, 4 algorithms)

This paper contains 32 sections, 2 theorems, 2 equations, 17 figures, 14 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. $\textsc{VeriX+}$: Verified eXplainability plus
  3. Optimal Verified Explanations
  4. Workflow of $\textsc{VeriX+}$ in A Nutshell
  5. Methodological Advances for Explanation Size and Generation Time
  6. Improving size: A Bound Propagation-based Traversal Order
  7. Improving Time: A Binary Search-based Traversal
  8. Improving Time: A Confidence Ranking
  9. A Size-Time Trade-off: QuickXplain
  10. Experimental Results
  11. Improvements for Explanation Size and Generation Time
  12. Explanations for Transformers in Real-world Applications
  13. Comparison to Existing Formal and Non-formal Explanation Approaches
  14. Explanations from Adversarial Training
  15. Using Explanation Size to Detect OOD and Misclassified Examples
  16. ...and 17 more sections

Key Result

Theorem 3.1

Given a neural network $f$ and an input $\mathbf{x} = \langle x_1, \ldots, x_m \rangle$ where $m \geq 2$, the time complexity of $\textsc{binarySequential}(f, \mathbf{x})$ is $2$ calls of $\textsc{check}$ for the best case (all features are irrelevant) and $k_{2m} = 2 \cdot k_m + 1$ or $k_{2m+1} = k

Figures (17)

  • Figure 1: The $\textsc{VeriX+}$ framework.
  • Figure 2: $\textsc{traversalOrder}$
  • Figure 3: $\textsc{binarySequential}$
  • Figure 4: $\textsc{check}$ with confidence ranking
  • Figure 5: $\textsc{QuickXplain}$
  • ...and 12 more figures

Theorems & Definitions (5)

  • Definition 2.1: Optimal Verified Explanation verix
  • Theorem 3.1: Time Complexity
  • Theorem 3.2: Time Complexity
  • proof
  • proof