# Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Builds on 50 of its 73 references that are in the map.
- First posted on arXiv 10 Jun 2025.

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

- [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)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Towards Robust Interpretability with Self-Explaining Neural Networks](https://mlsanity.com/paper/1806.07538/) (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)
- [Explaining Deep Neural Networks with a Polynomial Time Algorithm for Shapley Values Approximation](https://mlsanity.com/paper/1903.10992/) (2019)
- [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)
- [Model Interpretability through the Lens of Computational Complexity](https://mlsanity.com/paper/2010.12265/) (2020)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Explaining Naive Bayes and Other Linear Classifiers with Polynomial Time and Delay](https://mlsanity.com/paper/2008.05803/) (2020)
- [On Explaining Random Forests with SAT](https://mlsanity.com/paper/2105.10278/) (2021)
- [On Guaranteed Optimal Robust Explanations for NLP Models](https://mlsanity.com/paper/2105.03640/) (2021)
- [Logic-Based Explainability in Machine Learning](https://mlsanity.com/paper/2211.00541/) (2022)
- [On Tackling Explanation Redundancy in Decision Trees](https://mlsanity.com/paper/2205.09971/) (2022)
- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [Explanations for Monotonic Classifiers](https://mlsanity.com/paper/2106.00154/) (2021)
- [On Efficiently Explaining Graph-Based Classifiers](https://mlsanity.com/paper/2106.01350/) (2021)
- [On Computing Probabilistic Explanations for Decision Trees](https://mlsanity.com/paper/2207.12213/) (2022)
- [Trading Complexity for Sparsity in Random Forest Explanations](https://mlsanity.com/paper/2108.05276/) (2021)
- [What made you do this? Understanding black-box decisions with sufficient input subsets](https://mlsanity.com/paper/1810.03805/) (2018)
- [Overinterpretation reveals image classification model pathologies](https://mlsanity.com/paper/2003.08907/) (2020)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [ASTERYX : A model-Agnostic SaT-basEd appRoach for sYmbolic and score-based eXplanations](https://mlsanity.com/paper/2206.11900/) (2022)
- [Probabilistic Sufficient Explanations](https://mlsanity.com/paper/2105.10118/) (2021)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Computing Abductive Explanations for Boosted Trees](https://mlsanity.com/paper/2209.07740/) (2022)
- [Feature Necessity & Relevancy in ML Classifier Explanations](https://mlsanity.com/paper/2210.15675/) (2022)

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

- [Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees](https://mlsanity.com/paper/2602.16823/) (2026)
- [SHAP Meets Tensor Networks: Provably Tractable Explanations with Parallelism](https://mlsanity.com/paper/2510.21599/) (2025)
- [GNN Explanations that do not Explain and How to find Them](https://mlsanity.com/paper/2601.20815/) (2026)
- [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)
- [Unifying Formal Explanations: A Complexity-Theoretic Perspective](https://mlsanity.com/paper/2602.18160/) (2026)
- [Provably Explaining Neural Additive Models](https://mlsanity.com/paper/2602.17530/) (2026)
- [Missingness Bias Calibration in Feature Attribution Explanations](https://mlsanity.com/paper/2603.04831/) (2026)
- [On Improving Deep Active Learning with Formal Verification](https://mlsanity.com/paper/2512.14170/) (2025)
- [Talking with Verifiers: Automatic Specification Generation for Neural Network Verification](https://mlsanity.com/paper/2603.02235/) (2026)
- [Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networks](https://mlsanity.com/paper/2605.24084/) (2026)
- [Neuron Activation-based Computation of Logical Explanations for Deep Neural Networks](https://mlsanity.com/paper/2609.14099/) (2026)
- [The Misery of Mechanistic Interpretability: A Formal Perspective](https://mlsanity.com/paper/2609.15533/) (2026)

## Abstract (arXiv)

Despite significant advancements in post-hoc explainability techniques for neural networks, many current methods rely on heuristics and do not provide formally provable guarantees over the explanations provided. Recent work has shown that it is possible to obtain explanations with formal guarantees by identifying subsets of input features that are sufficient to determine that predictions remain unchanged using neural network verification techniques. Despite the appeal of these explanations, their computation faces significant scalability challenges. In this work, we address this gap by proposing a novel abstraction-refinement technique for efficiently computing provably sufficient explanations of neural network predictions. Our method abstracts the original large neural network by constructing a substantially reduced network, where a sufficient explanation of the reduced network is also provably sufficient for the original network, hence significantly speeding up the verification process. If the explanation is in sufficient on the reduced network, we iteratively refine the network size by gradually increasing it until convergence. Our experiments demonstrate that our approach enhances the efficiency of obtaining provably sufficient explanations for neural network predictions while additionally providing a fine-grained interpretation of the network's predictions across different abstraction levels.
