The Attribution Impossibility Triangle: 305 Lean Theorems Prove SHAP Is Unreliable Under Collinearity

Forum topic · 小凯 · 2026-05-22

Summary

A 2026 paper by Drake Caraker, Bryan Arnold, and David Rhoads (arXiv:2605.21492) uses 305 machine-verified Lean 4 theorems, derived from 16 axioms with zero 'sorry' statements, to prove an impossibility result for explainable AI: when features are collinear, no feature attribution ranking can simultaneously be faithful, stable, and complete. The authors quantify attribution variance divergence as 1/(1-ρ²) for gradient boosting models, show Lasso attributions become indeterminate for perfectly collinear features, and survey 77 public datasets finding 68% exhibit significant attribution instability. They further prove a dichotomy: all methods are either faithful-complete but unstable (like classic SHAP, whose rankings flip with up to 50% probability for collinear features) or ensemble methods that trade completeness for stability. The paper proposes DASH (Diversified Aggregation of SHAP), a Pareto-optimal unbiased ensemble approach, while honestly acknowledging it tames rather than resolves the impossibility. The authors caution that SHAP-based fairness audits are systematically unreliable under collinearity, since models can shift blame to scapegoat features. Practical takeaway: attribution rankings from models with highly correlated features should not feed serious decisions.

| Item | Detail | |------|--------| | Paper | The Attribution Impossibility: No Feature Ranking Is Faithful, Stable, and Complete Under Collinearity | | Authors | Drake Caraker, Bryan Arnold, David Rhoads | | arXiv ID | 2605.21492 | | Dates | Submitted April 8, 2026; latest revision May 21, 2026 | | Categories | cs.LG / cs.AI / cs.LO / stat.ML | | Core finding | 305 Lean 4 theorems formally prove that no feature attribution ranking can simultaneously satisfy faithfulness, stability, and completeness under collinearity. 68% of surveyed public datasets are affected. SHAP-based fairness auditing is systematically unreliable under collinearity. |

1. The Value of Proving "Impossible"

The most elegant theorems in mathematical history are impossibility proofs: angles cannot be trisected with compass and straightedge, quintic equations have no radical solutions, the halting problem is undecidable. Their shared value is telling you to stop trying — the direction itself is wrong.

This paper does exactly that for explainable AI (XAI). Using 305 Lean 4 theorems derived from 16 axioms with zero sorry statements, it mechanically verifies a harsh conclusion:

When features are collinear, no feature attribution ranking can simultaneously satisfy three basic properties: faithfulness, stability, and completeness.

This is not "nobody has found one yet." It is a proven "never possible."

2. The Three Properties

Faithfulness: the attribution must tell the truth. If the model relies on feature A more than B, the ranking must place A above B, always.
Stability: running on the same data twice should yield the same attribution. You cannot say A is most important today and B tomorrow.
Completeness: attribution values must sum to the total prediction — nothing may be missing.

The core proof shows that when two features are highly correlated, you can have at most two of the three. In collinear settings, a "feature importance ranking" is no more reliable than a coin flip.

3. Why Collinearity Kills Attribution

Imagine a house-price model with features A = number of bedrooms and B = floor area — highly correlated in most listings. Asked how much A versus B contributed to a prediction, the model internally does not separate them: it can assign A's effect to B and vice versa, leaving the total prediction unchanged.

The paper quantifies this precisely:

For gradient boosting models, attribution variance diverges as 1/(1-ρ²), where ρ is the correlation coefficient. As ρ → 1, variance → ∞.
For Lasso, the divergence is infinite — attributions for perfectly collinear features are theoretically indeterminate.
Random forests are relatively most robust: attribution variance converges under collinearity, at the cost of losing completeness.

4. 68% of Datasets Are Affected

A survey of 77 public datasets found 68% exhibit significant attribution instability. This means whenever SHAP is run on data with more than two features and someone says "these are the top three features," there is more than a two-in-three chance the ranking itself is unreliable.

Real-world consequences:

A loan model claims "credit score is the top rejection factor" — but income and credit score are highly correlated, so the ranking is arbitrary.
A medical model names "blood pressure" the top risk factor — but blood pressure correlates with age and weight.
A hiring algorithm ranks "education" first — but education correlates with parental education.

The paper further shows that using SHAP directly in fairness audits to select "which feature groups cause discrimination" is systematically unreliable — the model can shift blame onto a scapegoat feature correlated with the true source of discrimination.

5. A Dichotomy of the Design Space

The paper fully characterizes the design space of feature attribution. Only two method classes exist:

1. Faithful-complete methods: correct and complete attributions, but extremely unstable — rankings for collinear features flip with up to 50% probability. Classic SHAP belongs here. 2. Ensemble methods: sacrifice completeness for stability by aggregating attributions across models/samples. The paper's DASH belongs here.

There is no third class. Any attribution method must choose A or B. This is a mathematical proof, not a philosophical discussion.

6. DASH: A Pragmatic Answer to Impossibility

DASH (Diversified Aggregation of SHAP) trains N slightly different models (different seeds, training subsets) and averages their SHAP values. It is proven Pareto-optimal among unbiased aggregation methods and operates at the Cramér–Rao variance lower bound, with an exact formula for the ensemble size N needed to reach an acceptable variance.

Honest caveat: DASH does not resolve the impossibility — it tames its impact. For fully collinear features, DASH honestly reports a tie rather than randomly picking one. That is closer to the truth than SHAP's point estimate, but still gives no answer to "which one matters more."

7. Honest Boundaries

Pairwise linearity focus: "collinearity" is defined mainly via pairwise linear correlation; higher-order and nonlinear collinearity patterns are not covered and may require extending the Lean 4 framework.
Cost of ensembling: DASH requires retraining multiple models, impractical for expensive models like large language models; cheaper alternatives are not discussed.
Unquantified consequences: the gap between "instability" and "decision errors with real consequences" is not measured — small fluctuations and full rank flips differ greatly in severity.
Conditional SHAP: the paper proves conditional SHAP cannot escape the impossibility when features have identical causal effects — a condition rarely verifiable in real data.

Takeaway

Like the uncertainty principle in physics, this impossibility is not a limitation of tools but a structural property of the problem itself. Not poorly written SHAP, not insufficient sampling — the geometry of the question forbids faithfulness, stability, and completeness simultaneously.

For practitioners: if you use SHAP to explain a model with highly correlated features, be honest. Part of your ranking is randomly drawn from overlapping information, and that part should not enter any serious decision.

Source: arXiv:2605.21492