Towards Tractable, Provably Exact Shapley Interactions and Beyond in Neural Networks

Shapley interactions and the broader family of game-theoretic explanations are widely used to characterise how features contribute to neural network predictions. Yet exact computation requires reasoning over exponentially many feature subsets, and these quantities are therefore typically estimated, without provable guarantees. We introduce a verification-based algorithm for discovering additive structures within neural networks, enabling the computation of *provable upper and lower bounds on the exact values* of a broad family of game-theoretic explanations, including Shapley interactions of any order and sparse Fourier explanations. We then analyse the computational limits of this problem, proving that computing Shapley interactions remains #P-hard even for networks with as few as two ReLU neurons or a single attention layer. To address this, we introduce a robustness-based training scheme that encourages additive structure in the learned model, substantially improving the scalability of our algorithm. Experimentally, our approach handles substantially larger models and search spaces and brings exact certified game-theoretic interactions to transformer architectures for the first time. Overall, our results provide game-theoretic attributions and interactions with provable guarantees where estimation would otherwise be required, while also providing a principled basis for evaluating such estimators.