If you have ever trained a gradient-boosted model, computed SHAP values, retrained with a different random seed, and found that the top-ranked feature changed, you may have assumed this was a data quality issue or a hyperparameter problem. This paper proves it is neither. It is a mathematical impossibility, and the authors go considerably further than simply naming the problem: they quantify it across four model classes, resolve it constructively, and machine-verify the entire framework in Lean 4.
The core claim is striking in its simplicity. For a pair of collinear features, ranking them by attribution is equivalent to a coin flip. Across a survey of 77 public datasets, 68% exhibit attribution instability, and the authors note this is a conservative lower bound given the statistical power of their survey design. The problem is not incidental to SHAP; it is structural, and it persists under conditional SHAP when features share equal causal effects.
The Impossibility and Its Structure
The paper formalises three desiderata for any feature ranking method: faithfulness (the ranking reflects the actual model), stability (retraining with a different seed produces the same ranking), and completeness (every pair of features is ranked). The central result, Theorem 5, proves these three properties are mutually incompatible when any two features are collinear. The proof proceeds via the Rashomon property: under collinearity, there exist multiple models with equal predictive performance that assign different importance orderings to the correlated pair. A faithful method must track each model's ordering; a stable method must ignore it; no method can do both while also committing to a strict ranking.
What distinguishes this from earlier attribution impossibility results (Bilodeau et al. 2024, Huang and Marques-Silva 2024, Srinivas and Fleuret 2019) is the combination of cross-model stability as the central axis, quantitative architecture-specific bounds, a constructive resolution with proved optimality, and full formal verification. The comparison table in the paper is blunt: prior results address stability empirically at best, none provide quantitative bounds, and none offer a resolution.
The design space theorem (Theorem 28) is particularly clean. Exactly two families of attribution methods exist. The first family is faithful and complete but unstable, with rankings that flip up to 50% of the time for symmetric collinear pairs. The second family, of which DASH is the canonical member, is stable but reports ties for symmetric features. There is no third option. This is not a practical limitation of current methods; it is a partition of the entire space of possible methods.
Quantitative Bounds and Architecture Discrimination
The qualitative impossibility is complemented by architecture-specific bounds on the attribution ratio, defined as the factor by which the dominant feature is overweighted in a single model draw. The results are meaningfully different across architectures:
- Gradient boosting: the attribution ratio diverges as 1/(1 - rho^2), growing without bound as correlation approaches 1
- Lasso: the ratio is infinite, since the regulariser forces exactly one feature in a collinear pair to zero
- Random forests: the ratio converges to 1 + O(1/sqrt(T)) with the number of trees, explaining their comparative stability
- Neural networks: empirically validated with 87% of feature pairs showing instability under model variation, versus 11% under KernelSHAP sampling noise alone
The gradient boosting bound is derived from a split-gap lemma (Lemma 14) that characterises how a tree's first split breaks the symmetry between collinear features. The proportionality constant alpha, theoretically 2/pi for Gaussian data, is empirically fitted at 0.60 with a well-understood gap attributable to non-Gaussian residuals in later boosting rounds. Importantly, the impossibility theorem itself does not depend on alpha; the quantitative ratio uses it only to predict severity.
DASH and the Constructive Resolution
The paper proposes DASH (Diversified Aggregation of SHAP) as the resolution. DASH averages SHAP values across M independently trained models with equal weights. It is the unique symmetric unbiased linear aggregation method, and Theorem 22 proves it is Pareto-optimal among all unbiased aggregations on the stable branch, achieving the Cramer-Rao variance bound. The ensemble size required to reduce the flip rate below a target epsilon is given by a tight lower bound (Proposition 26): M = 25 models brings the flip rate below 1%, while M = 5 provides substantial improvement at modest cost.
The practical implications are concrete. In a simulated loan application pipeline with five correlated income features, 43.2% of denied applicants received a different top reason for denial depending on which of 25 models was queried. DASH consensus resolved this entirely, with 100% stable top-1 reasons. The fairness audit impossibility (Theorem 48) formalises what this implies: SHAP-based proxy discrimination audits are provably unreliable under collinearity, not merely noisy.
Formal Verification and Methodology
The Lean 4 formalization comprises 305 theorems across 54 files, derived from 16 axioms with zero uses of sorry. The core impossibility depends on zero axioms beyond the Rashomon property as hypothesis. This is, to the authors' knowledge, the first formally verified impossibility result in explainable AI, and the formalization served a practical purpose beyond certification: it caught two logical inconsistencies and one type mismatch that survived informal review. The recommendation to formalise impossibility theorems as standard practice is well-supported by this experience.
The paper also generalises the impossibility framework to model selection and causal orientation as instances of the same abstract symmetric decision problem, showing that cross-validation instability and CPDAG orientation ambiguity are structurally identical phenomena. This unification is conceptually valuable, though the causal orientation section relies on the interventional SHAP implementation in the shap package, which the authors acknowledge does not exactly implement the theoretical conditional SHAP of Janzing et al. (2020).
Limitations and Open Questions
Several limitations are worth noting. The split-count axioms assume full signal capture (alpha = 1); for finite-depth trees the empirical alpha is approximately 0.60, though the impossibility holds for any alpha greater than zero. The equicorrelation assumption within feature groups simplifies the axioms considerably; the Rashomon property holds pairwise but the group structure is an idealisation. The prevalence survey uses 20 models per dataset, giving only 32% power to detect a 10% flip rate, making 68% a conservative lower bound with the authors estimating true prevalence at 75-85%.
DASH requires M times the training cost of a single model, which is non-trivial for large architectures. The attention-based instability results for transformers are presented as suggestive evidence rather than a formal extension, since attention weights do not satisfy the proportionality axiom. The Bayes-optimality half of the design space theorem is proved but not yet formalised in Lean, requiring measure-theoretic decision theory not yet available in Mathlib.
The relationship to feature removal via VIF thresholding is handled honestly: decorrelating features eliminates the impossibility but changes the model and may discard genuinely useful information. DASH is the explanation-side fix for models that retain all features by design. These are complementary approaches rather than competing ones.
The paper is technically dense but carefully structured, with a named-results index that makes navigation practical. For anyone working on model auditing, fairness certification, or explainability tooling, the central message is unambiguous: attribution instability under retraining is not an engineering problem to be solved with better software. It is a theorem. The question is only how to report it honestly.
Code, Lean proofs, and reproduction scripts are available at github.com/DrakeCaraker/dash-impossibility-lean. Full paper: arXiv:2605.21492.