Table of Contents
Fetching ...

Mathematically rigorous proofs for Shapley explanations

David van Batenburg

TL;DR

This work provides a rigorous treatment of SHAP explanations by reformulating the original axioms and proving that the Shapley-based explanations are unique under Local Accuracy, Missingness, Restricted Symmetry, and Restricted Consistency. It also shows how SHAP can be computed as the solution to a weighted regression problem (KernelSHAP), with a detailed linear-algebra foundation and a discussion of the conditions under which the regression formulation is valid. By presenting a counterexample to the claim that Consistency implies Symmetry and by establishing a precise game-theoretic correspondence, the paper strengthens the theoretical underpinnings of SHAP while offering a practical, scalable computation route. The results have significant implications for the reliability and interpretability of model decisions in high-stakes domains, providing both clarity and methods for robust explanations.

Abstract

Machine Learning is becoming increasingly more important in today's world. It is therefore very important to provide understanding of the decision-making process of machine-learning models. A popular way to do this is by looking at the Shapley-Values of these models as introduced by Lundberg and Lee. In this thesis, we discuss the two main results by Lundberg and Lee from a mathematically rigorous standpoint and provide full proofs, which are not available from the original material. The first result of this thesis is an axiomatic characterization of the Shapley values in machine learning based on axioms by Young. We show that the Shapley values are the unique explanation to satisfy local accuracy, missingness, symmetry and consistency. Lundberg and Lee claim that the symmetry axiom is redundant for explanations. However, we provide a counterexample that shows the symmetry axiom is in fact essential. The second result shows that we can write the Shapley values as the unique solution to a weighted linear regression problem. This result is proven with the use of dimensionality reduction.

Mathematically rigorous proofs for Shapley explanations

TL;DR

This work provides a rigorous treatment of SHAP explanations by reformulating the original axioms and proving that the Shapley-based explanations are unique under Local Accuracy, Missingness, Restricted Symmetry, and Restricted Consistency. It also shows how SHAP can be computed as the solution to a weighted regression problem (KernelSHAP), with a detailed linear-algebra foundation and a discussion of the conditions under which the regression formulation is valid. By presenting a counterexample to the claim that Consistency implies Symmetry and by establishing a precise game-theoretic correspondence, the paper strengthens the theoretical underpinnings of SHAP while offering a practical, scalable computation route. The results have significant implications for the reliability and interpretability of model decisions in high-stakes domains, providing both clarity and methods for robust explanations.

Abstract

Machine Learning is becoming increasingly more important in today's world. It is therefore very important to provide understanding of the decision-making process of machine-learning models. A popular way to do this is by looking at the Shapley-Values of these models as introduced by Lundberg and Lee. In this thesis, we discuss the two main results by Lundberg and Lee from a mathematically rigorous standpoint and provide full proofs, which are not available from the original material. The first result of this thesis is an axiomatic characterization of the Shapley values in machine learning based on axioms by Young. We show that the Shapley values are the unique explanation to satisfy local accuracy, missingness, symmetry and consistency. Lundberg and Lee claim that the symmetry axiom is redundant for explanations. However, we provide a counterexample that shows the symmetry axiom is in fact essential. The second result shows that we can write the Shapley values as the unique solution to a weighted linear regression problem. This result is proven with the use of dimensionality reduction.

Paper Structure

This paper contains 27 sections, 36 theorems, 154 equations, 2 figures.

Key Result

Theorem 15

The Shapley value is the unique allocation procedure that is symmetric, strongly monotonic and efficient.

Figures (2)

  • Figure 1: Visualisation of superpixels. The left image is the original image $x$ with the superpixels highlighted. This image will be the output of $h_x(1111)$. The right image is the output $h_x(0110$).
  • Figure 2: Visualisation of an explanation on an acoustic guitar. The model used to create this explanation is AlexNet NIPS2012_c399862d.

Theorems & Definitions (79)

  • Definition 1: Simplification function
  • Definition 2: Simplified model
  • Definition 3: Shapley values for machine learning
  • Claim 8
  • Definition 9: Cooperative Game
  • Definition 10: Allocation Procedure
  • Definition 11: Shapley values for cooperative games
  • Theorem 15
  • proof
  • Lemma 16
  • ...and 69 more