特征共线时，任何归因排名都无法同时忠实、稳定、完整，这是数学上的不可能。
The Attribution Impossibility: No Feature Ranking Is Faithful, Stable, and Complete Under Collinearity
- 证明共线特征无法同时满足忠实、稳定、完整，排名本质如抛硬币
- 提出DASH方法，通过集成平均实现稳定归因，避免排名翻转
- 首次用形式化证明验证可解释AI的不可能性，适合公平性审计研究者
当特征共线时，任何特征归因排名都无法同时满足忠实性、稳定性与完整性。对于共线特征对，排名等价于抛硬币。本文证明此不可能性，量化了四种模型类别的表现：梯度提升中归因比发散为1/(1-ρ²)，Lasso中为无穷大，随机森林中收敛。提出DASH（Diversified Aggregation of SHAP）方法，通过集成平均实现稳定归因，报告对称特征的并列结果。归因设计空间被完全刻画：仅存在两类方法——忠实完整的（不稳定，排名翻转率高达50%）和类似DASH的集成方法（稳定）。在77个公开数据集的调查中，68%显示归因不稳定性。即使使用条件SHAP也无法规避该不可能性。框架包含可量化的诊断工具（Z检验流程与单模型筛查），对公平性审计具有直接影响：基于SHAP的代理歧视审计在共线性下必然不可靠。设计空间定理、诊断方法与不可能性均在Lean 4中机械验证（305个定理，源自16条公理，无未证明项），据我们所知，这是首个在可解释人工智能领域被形式化验证的不可能性结果。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。