The Attribution Impossibility: No Feature Ranking Is Faithful, Stable, and Complete Under Collinearity

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.

한 줄 요약

**[Feature Attribution / Impossibility]** Collinearity 하에서 어떤 feature ranking도 faithful·stable·complete 동시 만족 불가능 — 4 모델 클래스 정량화·DASH ensemble로 해소·305 Lean 4 theorem으로 형식 검증, 77 공개 데이터셋 중 68%에서 instability 관찰.

핵심 기여도

Feature가 collinear할 때 어떤 feature ranking도 동시에 faithful·stable·complete할 수 없음을 증명 — collinear pair에서 ranking은 coin flip으로 reduce된다는 impossibility 정리.
4 모델 클래스에 대해 impossibility 정량화, DASH ensemble averaging으로 해소·305 Lean 4 theorem으로 machine-verified.
Complete attribution design space 특성화 — 정확히 두 method family 존재(faithful-complete methods: unstable, ranking이 최대 50% flip / DASH 같은 ensemble methods: stable, symmetric feature에 tie 보고), dichotomy 외 method 없음.
정량적 impossibility — attribution ratio가 gradient boosting에서 1/(1-rho^2)로 diverge, Lasso에서 infinite, random forest에서 converge. DASH가 unbiased aggregation 중 Pareto-optimal, Cramer-Rao variance bound 달성·tight ensemble size formula. 77 공개 데이터셋 중 68%에서 attribution instability 관찰, conditional SHAP도 동일 인과 효과 시 impossibility 회피 불가. Z-test workflow·single-model screening tool·fairness audit 함의 포함, 모든 결과 Lean 4(305 theorem, 16 axiom, 0 sorry)로 mechanically verified — 설명 AI 분야 첫 formally verified impossibility.

핵심 아이디어

Feature attribution의 faithful·stable·complete trilemma는 collinearity 하에서 본질적 impossibility이며, DASH 같은 ensemble averaging이 Cramer-Rao bound에 도달하는 유일한 Pareto-optimal 해법이고, 이 모든 결과는 formal verification으로 보장 가능하다.

기술적 접근법

**방법론**: Impossibility theorem + DASH ensemble + Lean 4 formal verification.
**핵심 기법**: (1) Collinear pair에서 ranking의 coin flip reduce 증명, (2) 4 모델 클래스의 정량적 attribution ratio 분석(1/(1-rho^2), infinite, converge), (3) DASH(Diversified Aggregation of SHAP)로 Cramer-Rao bound 달성, (4) Tight ensemble size formula, (5) Lean 4 mechanical verification — 305 theorem, 16 axiom, 0 sorry.

주요 결과

4 모델 클래스의 attribution ratio 정량화: gradient boosting 1/(1-rho^2) diverge, Lasso infinite, random forest converge.
77 공개 데이터셋 중 68%에서 attribution instability 관찰.
DASH가 unbiased aggregation 중 Pareto-optimal, Cramer-Rao bound 달성.
305 Lean 4 theorem(16 axiom, 0 sorry)로 mechanically verified.
SHAP 기반 proxy discrimination audit이 collinearity 하 unreliable함을 증명.

의의 및 한계

**의의**: 설명 AI 분야 첫 formally verified impossibility, design space dichotomy의 명확화, fairness audit의 신뢰성에 대한 systematic 경고, DASH의 Pareto-optimality 보장. **한계**: Collinearity 가정 외 일반화는 추가 분석, 형식 검증의 axiom 의존, 실제 ML 배포에서 DASH의 ensemble cost 부담.

실용적 활용

SHAP 기반 설명·fairness audit 진단.
DASH ensemble로 안정적 attribution.
모델 해석 도구의 신뢰성 평가.