Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks

Formal explanations can be verified for correctness: Unlike most existing explainable AI methods that rely on heuristics without guarantees, this paper demonstrates that formal methods can generate "provably correct explanations" of why neural networks make specific decisions—an important advancement for safety-critical applications like healthcare or autonomous vehicles.

Minimal explanations are more practical than perfect ones: The researchers propose finding "minimal explanations" that approximate the absolute best explanation, rather than pursuing computationally impossible perfect solutions. This pragmatic approach makes formal XAI scalable enough to work with real neural networks while still maintaining mathematical guarantees.

Verification techniques can measure explanation quality: The paper shows how formal verification methods can calculate "lower and upper bounds on the optimal explanation," providing a way to quantify how good an explanation is—helping users understand the reliability of the explanations they receive.

Bundled explanations improve interpretability: The authors introduce "bundles" that group related features together, producing "more succinct and interpretable explanations." This addresses a key challenge in XAI: even when explanations are correct, they can be too complex for humans to understand and act upon.

Scalability improvements make formal XAI practical: By proposing "heuristics that significantly improve the scalability of the verification process," this work moves formal XAI from a theoretical concept toward practical deployment in real-world systems where computational resources are limited.