# Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks

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

## Key facts

- Cited by 42 papers in the map (data through 14 Oct 2026).
- Builds on 42 of its 72 references that are in the map.
- First posted on arXiv 25 Oct 2022.

## Builds on (most cited first, 30 of 42)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Grad-CAM: Visual Explanations from Deep Networks via Gradient-based Localization](https://mlsanity.com/paper/1610.02391/) (2016)
- [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)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [SmoothGrad: removing noise by adding noise](https://mlsanity.com/paper/1706.03825/) (2017)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [One pixel attack for fooling deep neural networks](https://mlsanity.com/paper/1710.08864/) (2017)
- [Adversarial Attacks on Neural Network Policies](https://mlsanity.com/paper/1702.02284/) (2017)
- [BAE: BERT-based Adversarial Examples for Text Classification](https://mlsanity.com/paper/2004.01970/) (2020)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [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)
- ["How do I fool you?": Manipulating User Trust via Misleading Black Box Explanations](https://mlsanity.com/paper/1911.06473/) (2019)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [On Guaranteed Optimal Robust Explanations for NLP Models](https://mlsanity.com/paper/2105.03640/) (2021)
- [Superpixels: An Evaluation of the State-of-the-Art](https://mlsanity.com/paper/1612.01601/) (2016)
- [On Explaining Decision Trees](https://mlsanity.com/paper/2010.11034/) (2020)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [SAT-Based Rigorous Explanations for Decision Lists](https://mlsanity.com/paper/2105.06782/) (2021)
- [Can I Trust the Explainer? Verifying Post-hoc Explanatory Methods](https://mlsanity.com/paper/1910.02065/) (2019)
- [Don't Lie to Me! Robust and Efficient Explainability with Verified Perturbation Analysis](https://mlsanity.com/paper/2202.07728/) (2022)
- [Parallelization Techniques for Verifying Neural Networks](https://mlsanity.com/paper/2004.08440/) (2020)
- [On Tractable Representations of Binary Neural Networks](https://mlsanity.com/paper/2004.02082/) (2020)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)

## Built on by (most cited first, 30 of 42)

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Local vs. Global Interpretability: A Computational Complexity Perspective](https://mlsanity.com/paper/2406.02981/) (2024)
- [Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation](https://mlsanity.com/paper/2405.08297/) (2024)
- [Delivering Inflated Explanations](https://mlsanity.com/paper/2306.15272/) (2023)
- [From Robustness to Explainability and Back Again](https://mlsanity.com/paper/2306.03048/) (2023)
- [Stability Guarantees for Feature Attributions with Multiplicative Smoothing](https://mlsanity.com/paper/2307.05902/) (2023)
- [Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations](https://mlsanity.com/paper/2506.08505/) (2025)
- [Explain Yourself, Briefly! Self-Explaining Neural Networks with Concise Sufficient Reasons](https://mlsanity.com/paper/2502.03391/) (2025)
- [Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees](https://mlsanity.com/paper/2602.16823/) (2026)
- [Probabilistic Stability Guarantees for Feature Attributions](https://mlsanity.com/paper/2504.13787/) (2025)
- [Auditing Local Explanations is Hard](https://mlsanity.com/paper/2407.13281/) (2024)
- [SHAP Meets Tensor Networks: Provably Tractable Explanations with Parallelism](https://mlsanity.com/paper/2510.21599/) (2025)
- [Analyzing Adversarial Inputs in Deep Reinforcement Learning](https://mlsanity.com/paper/2402.05284/) (2024)
- [Most General Explanations of Tree Ensembles (Extended Version)](https://mlsanity.com/paper/2505.10991/) (2025)
- [Interpretability Can Be Actionable](https://mlsanity.com/paper/2605.11161/) (2026)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [Sum-of-Parts: Self-Attributing Neural Networks with End-to-End Learning of Feature Groups](https://mlsanity.com/paper/2310.16316/) (2023)
- [Bridging Dimensions: Confident Reachability for High-Dimensional Controllers](https://mlsanity.com/paper/2311.04843/) (2023)
- [Self-Explaining Neural Networks for Business Process Monitoring](https://mlsanity.com/paper/2503.18067/) (2025)
- [Formal Abductive Latent Explanations for Prototype-Based Networks](https://mlsanity.com/paper/2511.16588/) (2025)
- [Towards Formal Verification of Deep Neural Networks for Object Detection](https://mlsanity.com/paper/2407.01295/) (2024)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Additive Models Explained: A Computational Complexity Approach](https://mlsanity.com/paper/2510.21292/) (2025)
- [FAME: Formal Abstract Minimal Explanation for Neural Networks](https://mlsanity.com/paper/2603.10661/) (2026)
- [Interactive Explanations for Reinforcement-Learning Agents](https://mlsanity.com/paper/2504.05393/) (2025)
- [Unifying Formal Explanations: A Complexity-Theoretic Perspective](https://mlsanity.com/paper/2602.18160/) (2026)
- [Incremental Neural Network Verification via Learned Conflicts](https://mlsanity.com/paper/2603.12232/) (2026)
- [Finding Minimum-Cost Explanations for Predictions made by Tree Ensembles](https://mlsanity.com/paper/2303.09271/) (2023)
- [Uncovering Bugs in Formal Explainers: A Case Study with PyXAI](https://mlsanity.com/paper/2511.03169/) (2025)
- [Provably Explaining Neural Additive Models](https://mlsanity.com/paper/2602.17530/) (2026)

## Abstract (arXiv)

With the rapid growth of machine learning, deep neural networks (DNNs) are now being used in numerous domains. Unfortunately, DNNs are "black-boxes", and cannot be interpreted by humans, which is a substantial concern in safety-critical systems. To mitigate this issue, researchers have begun working on explainable AI (XAI) methods, which can identify a subset of input features that are the cause of a DNN's decision for a given input. Most existing techniques are heuristic, and cannot guarantee the correctness of the explanation provided. In contrast, recent and exciting attempts have shown that formal methods can be used to generate provably correct explanations. Although these methods are sound, the computational complexity of the underlying verification problem limits their scalability; and the explanations they produce might sometimes be overly complex. Here, we propose a novel approach to tackle these limitations. We (1) suggest an efficient, verification-based method for finding minimal explanations, which constitute a provable approximation of the global, minimum explanation; (2) show how DNN verification can assist in calculating lower and upper bounds on the optimal explanation; (3) propose heuristics that significantly improve the scalability of the verification process; and (4) suggest the use of bundles, which allows us to arrive at more succinct and interpretable explanations. Our evaluation shows that our approach significantly outperforms state-of-the-art techniques, and produces explanations that are more useful to humans. We thus regard this work as a step toward leveraging verification technology in producing DNNs that are more reliable and comprehensible.