Anytime Approximate Formal Feature Attribution

Formal feature attribution provides stronger guarantees than popular heuristic methods: Unlike common XAI approaches that lack quality guarantees or approximate Shapley values, formal feature attribution (FFA) grounds feature importance in formal reasoning about how a model actually behaves, offering a more rigorous foundation for understanding AI decisions.

Computing exact explanations is mathematically intractable: The paper proves that calculating formal feature attribution is #P-hard, meaning even with perfect information, computing exact feature importance scores is computationally infeasible—a fundamental limitation that any practical explanation system must work around.

Approximation methods are necessary but feasible: Because exact computation is intractable, the researchers developed efficient heuristic approaches that can approximate formal feature attribution "on-the-fly," making it practical to explain AI decisions in real-world applications despite the underlying computational challenges.

The gap between different explanation methods matters: The paper highlights that popular approaches attempting to approximate Shapley values are "not the same as explaining which features contribute to a decision," suggesting that organizations using standard XAI tools may be getting explanations that don't actually measure what they think they're measuring.

Formal methods offer a path toward more trustworthy AI explanations: By grounding feature attribution in formal logic rather than heuristics alone, this work provides a foundation for developing AI explanations with verifiable properties—important for high-stakes applications where understanding why an AI made a decision is critical.