# Efficiently Computing Compact Formal Explanations

arXiv: https://arxiv.org/abs/2409.03060 · HTML: https://mlsanity.com/paper/2409.03060/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 33 references that are in the map.
- First posted on arXiv 4 Sep 2024.

## Builds on (most cited first, 18 of 18)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [A Unified Approach to Interpreting Model Predictions](https://mlsanity.com/paper/1705.07874/) (2017)
- ["Why Should I Trust You?": Explaining the Predictions of Any Classifier](https://mlsanity.com/paper/1602.04938/) (2016)
- [On Calibration of Modern Neural Networks](https://mlsanity.com/paper/1706.04599/) (2017)
- [A Baseline for Detecting Misclassified and Out-of-Distribution Examples in Neural Networks](https://mlsanity.com/paper/1610.02136/) (2016)
- [Interpretability Beyond Feature Attribution: Quantitative Testing with Concept Activation Vectors (TCAV)](https://mlsanity.com/paper/1711.11279/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Why ReLU networks yield high-confidence predictions far away from the training data and how to mitigate the problem](https://mlsanity.com/paper/1812.05720/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Abduction-Based Explanations for Machine Learning Models](https://mlsanity.com/paper/1811.10656/) (2018)
- [A Symbolic Approach to Explaining Bayesian Network Classifiers](https://mlsanity.com/paper/1805.03364/) (2018)
- [On The Reasons Behind Decisions](https://mlsanity.com/paper/2002.09284/) (2020)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [On Guaranteed Optimal Robust Explanations for NLP Models](https://mlsanity.com/paper/2105.03640/) (2021)
- [Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation](https://mlsanity.com/paper/2405.08297/) (2024)
- [Validation of Image-Based Neural Network Controllers through Adaptive Stress Testing](https://mlsanity.com/paper/2003.02381/) (2020)

## Built on by (most cited first, 4 of 4)

- [Efficient Contrastive Explanations on Demand](https://mlsanity.com/paper/2412.18262/) (2024)
- [Fixed Point Explainability](https://mlsanity.com/paper/2505.12421/) (2025)
- [Beyond L2: Generalizing Abductive Latent Explanations to Diverse Prototype-Based Architectures](https://mlsanity.com/paper/2608.16773/) (2026)
- [Neuron Activation-based Computation of Logical Explanations for Deep Neural Networks](https://mlsanity.com/paper/2609.14099/) (2026)

## Abstract (arXiv)

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.