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

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.

Artificial intelligence systems can be used to make important decisions, like approving a bank loan. A popular method called SHAP explains these choices by scoring the importance of input features, such as an applicant's income. However, calculating these exact scores for complex models like neural networks requires impractical amounts of time and computing power. This is because the calculation must evaluate an overwhelmingly large number of feature combinations. We developed a new approach using a technique called bound propagation to speed up this computation. Our method establishes strict upper and lower limits for each feature's importance instead of calculating the exact scores directly. It then progressively tightens these limits until the precise answers are found. This new algorithm can handle significantly more input features than previous exact methods.