# Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networks

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 62 of its 99 references that are in the map.
- First posted on arXiv 22 May 2026.

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

- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [A Unified Approach to Interpreting Model Predictions](https://mlsanity.com/paper/1705.07874/) (2017)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [Gaussian Error Linear Units (GELUs)](https://mlsanity.com/paper/1606.08415/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Fooling LIME and SHAP: Adversarial Attacks on Post hoc Explanation Methods](https://mlsanity.com/paper/1911.02508/) (2019)
- [The many Shapley values for model explanation](https://mlsanity.com/paper/1908.08474/) (2019)
- [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)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [Problems with Shapley-value-based explanations as feature importance measures](https://mlsanity.com/paper/2002.11097/) (2020)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Abduction-Based Explanations for Machine Learning Models](https://mlsanity.com/paper/1811.10656/) (2018)
- [Improving KernelSHAP: Practical Shapley Value Estimation via Linear Regression](https://mlsanity.com/paper/2012.01536/) (2020)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Explaining Deep Neural Networks with a Polynomial Time Algorithm for Shapley Values Approximation](https://mlsanity.com/paper/1903.10992/) (2019)
- [Sampling Permutations for Shapley Value Estimation](https://mlsanity.com/paper/2104.12199/) (2021)
- [On The Reasons Behind Decisions](https://mlsanity.com/paper/2002.09284/) (2020)
- [On the Tractability of SHAP Explanations](https://mlsanity.com/paper/2009.08634/) (2020)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [From Shapley Values to Generalized Additive Models and back](https://mlsanity.com/paper/2209.04012/) (2022)
- [Shapley values for feature selection: The good, the bad, and the axioms](https://mlsanity.com/paper/2102.10936/) (2021)
- [On Guaranteed Optimal Robust Explanations for NLP Models](https://mlsanity.com/paper/2105.03640/) (2021)
- [SHAP-IQ: Unified Approximation of any-order Shapley Interactions](https://mlsanity.com/paper/2303.01179/) (2023)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [Explaining Predictive Uncertainty with Information Theoretic Shapley Values](https://mlsanity.com/paper/2306.05724/) (2023)

## Abstract (arXiv)

Shapley additive explanations (SHAP) are widely recognised as computationally intractable for neural networks, since they induce an exponential search space over the input features. In this work, we take a first step towards scaling exact SHAP computation to larger search spaces by introducing an algorithm that leverages recent advances in neural network verification to compute arbitrarily tight exact lower and upper bounds on SHAP values for neural networks, ultimately recovering the exact SHAP values. We demonstrate that our approach scales to orders of magnitude larger search spaces than state-of-the-art exact methods. This provides an important first step towards exact SHAP computation and establishes a principled cornerstone for evaluating statistical approximation methods on larger search spaces.