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.
| Comments: | 66 pages, 12 figures, 305 Lean 4 theorems. Code at this https URL |
| Subjects: | Machine Learning (cs.LG); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Machine Learning (stat.ML) |
| MSC classes: | 68T07, 62J02, 03B35, 91B14, 62C99 |
| ACM classes: | I.2.6; F.2.0; I.2.3; G.3 |
| Cite as: | arXiv:2605.21492 [cs.LG] |
| (or arXiv:2605.21492v1 [cs.LG] for this version) | |
| https://doi.org/10.48550/arXiv.2605.21492 arXiv-issued DOI via DataCite |
|
| Related DOI: | https://doi.org/10.5281/zenodo.19468379
DOI(s) linking to related resources |
From: Drake Caraker [view email]
[v1]
Wed, 8 Apr 2026 10:11:45 UTC (2,874 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。