The Attribution Impossibility: No Feature Ranking Is Faithful, Stable, and Complete Under Collinearity
Organizations: Independent Researchers
Abstract
No feature ranking can be simultaneously faithful, stable, and complete when features are collinear. For collinear pairs, ranking reduces to a coin flip. We prove this impossibility, quantify it for four model classes, resolve it via ensemble averaging (DASH), and machine-verify it with 305 Lean 4 theorems. We characterize the complete attribution design space: exactly two families of methods exist -- faithful-complete methods (unstable, with rankings that flip up to 50% of the time) and ensemble methods like DASH (stable, reporting ties for symmetric features) -- and no method lies outside this dichotomy. The impossibility is quantitative: the attribution ratio diverges as 1/(1-rho^2) for gradient boosting, is infinite for Lasso, and converges for random forests. DASH (Diversified Aggregation of SHAP) is provably Pareto-optimal among unbiased aggregations, achieving the Cramer-Rao variance bound with a tight ensemble size formula. In a survey of 77 public datasets, 68% exhibit attribution instability. Switching to conditional SHAP does not escape the impossibility when features have equal causal effects. The framework includes practical diagnostics -- a Z-test workflow and single-model screening tool -- and has direct consequences for fairness auditing: SHAP-based proxy discrimination audits are provably unreliable under collinearity. The design space theorem, diagnostics, and impossibility are mechanically verified in Lean 4 (305 theorems from 16 axioms, 0 sorry) -- to our knowledge, the first formally verified impossibility in explainable AI.
Figures & tables
| Axiom | Lean 4 name | Justification |
| First-mover surjectivity | firstMover_surjective | DGP symmetry: each feature can be first-mover |
| Split count (first-mover) | splitCount_firstMover | Gaussian conditioning (Lemma 14 ) |
| Split count (non-first-mover) | splitCount_nonFirstMover | Residual signal after first-mover absorbs -component |
| Global proportionality | proportionality_global | Uniform contribution model with constant across models |
| Cross-group symmetry | splitCount_crossGroup_symmetric | DGP symmetry: equal split counts when first-mover elsewhere |
| Cross-group stability | splitCount_crossGroup_stable | Changing first-mover within a group does not affect other groups |
| Fitted | ||||||
|---|---|---|---|---|---|---|
| Depth 1 (stumps) | 1.28 | 1.32 | 1.42 | 1.99 | 2.16 | |
| Depth 3 | 1.19 | 1.26 | 1.24 | 1.30 | 1.32 | |
| Depth 6 | 1.65 | 1.67 | 1.74 | 1.90 | 2.03 | |
| Depth 10 | 2.23 | 2.25 | 2.28 | 2.49 | 2.62 | — |
| Theory ( ) | 1.10 | 1.33 | 1.96 | 5.26 | 10.26 |
| Model class | Ratio | Scaling with | Mechanism |
|---|---|---|---|
| Gradient boosting | Increases with | Sequential residuals | |
| Lasso | Constant | Hard selection | |
| Neural network | Model-dependent | Architecture-dependent | Init. symmetry breaking |
| Random forest 3 3 3 The RF bound is informal. The GBDT and Lasso bounds are Lean-verified; the NN bound is conditional on the dominance hypothesis. | as | Independent trees |
| Method | Pairs resolved | |||
|---|---|---|---|---|
| Single model | 16.0% [13.8, 18.1] | 16.4% [14.3, 18.5] | 18.7% [16.4, 21.1] | 40/40 |
| Bootstrap SHAP | 16.2% [13.8, 18.2] | 16.1% [14.2, 18.0] | 18.8% [16.4, 21.4] | 40/40 |
| Subsampled SHAP | 16.3% [13.8, 18.5] | 16.1% [14.2, 17.9] | 18.8% [16.5, 21.3] | 40/40 |
| Dash ( ) | 3.8% [2.8, 4.9] | 3.1% [2.4, 3.9] | 3.7% [2.7, 4.7] | 40/40 |
| CI SHAP | 0.2% [0.1, 0.4] | 0.8% [0.6, 1.1] | 3.1% [2.1, 4.6] | 22/40 |
| 0.0 | 0.1 | 0.2 | 0.3 | 0.5 | 0.7 | 1.0 | |
|---|---|---|---|---|---|---|---|
| 0.50 | 50 | 19 | 0 | 0 | 0 | 0 | 0 |
| 0.70 | 53 | 19 | 0 | 0 | 0 | 0 | 0 |
| 0.80 | 52 | 44 | 19 | 10 | 0 | 0 | 0 |
| 0.90 | 50 | 50 | 48 | 40 | 40 | 19 | 0 |
| 0.95 | 50 | 50 | 50 | 48 | 44 | 40 | 27 |
| 0.99 | 50 | 50 | 50 | 50 | 50 | 48 | 48 |
| Experiment | Configuration |
|---|---|
| Synthetic (main text) | , groups of , , , , 50 seeds, |
| Validation (depth ) | , groups of , , , , 30 seeds, depths , |
| Breast Cancer | 30 features, 569 samples, , depth , , 50 seeds, TreeSHAP on 200 test samples |
| Hardware | Apple Silicon (M-series), single core |
| Software | Python 3.9.6, XGBoost 2.1.4, SHAP 0.49.1, NumPy 2.0.2 |
| Compute | Synthetic: min; Validation: min; Breast Cancer: min |
| Metric | XGBoost | LightGBM | CatBoost |
|---|---|---|---|
| Unstable pairs (flip ) | 162 | 183 | 160 |
| Max flip rate | 0.500 | 0.500 | 0.500 |
| Z-test correlation |
| Dataset | Pairs | Unstable | Screen prec. | ||
|---|---|---|---|---|---|
| Breast Cancer | 30 | 435 | 168 | 0.94 | |
| California Housing | 8 | 28 | 1 | — | |
| Diabetes | 10 | 45 | 15 | 0.50 | |
| Wine | 13 | 78 | 24 | 1.00 | |
| Heart Disease | 13 | 78 | 27 | 1.00 | |
| Credit-g | 20 | 190 | 47 | 0.67 |
| File | Section | Key Result |
| Defs.lean | § 2 | 14 axioms + derived theorems |
| Trilemma.lean | Thm. 5 | attribution_impossibility |
| Iterative.lean | § 3.3 | iterative_impossibility |
| General.lean | § 4.1 | gbdt_impossibility |
| SplitGap.lean | Lem. 14 | split_gap_exact |
| Ratio.lean | Thm. 15 | ratio_tendsto_atTop |
| Result | Stability? | Quantitative? | Resolution? | Formal? |
|---|---|---|---|---|
| Bilodeau et al. (2024) | No | No | No | No |
| Huang et al. (2024) | No | No | No | No |
| Srinivas et al. (2019) | No | No | No | No |
| Rao (2025) | No | No | No | No |
| Laberge et al. (2023) | Empirical | No | No | No |
| Herren & Hahn (2023) | Inference | No | No | No |
Appendix figures & tables2 assets
Supplementary material from the paper’s appendix.
Appendix
| Metric | XGBoost | LightGBM | CatBoost |
|---|---|---|---|
| Unstable pairs (flip ) | 162 | 183 | 160 |
| Max flip rate | 0.500 | 0.500 | 0.500 |
| Z-test correlation | |||
| Screen precision | 0.26 | 0.20 | — |
| Dash max flip ( ) | 0.48 | 0.48 | 0.48 |
| Experiment | Key finding | Script |
|---|---|---|
| Monte Carlo flip rate | validated to 1.3% error | monte_carlo_flip_rate.py |
| Hyperparameter sweep | Min flip 38.7% at ; never 0% | hyperparameter_sensitivity.py |
| Class imbalance | 1:5+ imbalance 100% pairs unstable | class_imbalance_instability.py |
| Missing data | MCAR/MAR/MNAR all compound instability | missing_data_instability.py |
| Longitudinal drift | Spearman degrades 1.0 0.18 over 31 rounds | longitudinal_retraining.py |
| Adversarial configs | All 108 configs hit 0.500 ceiling at | adversarial_max_instability.py |
Feature Attribution
Feature attribution estimates which input features or internal components contribute to a model’s predictions.
See all 231 papers