ExplainabilityAccountabilityTransparencycs.AI
Uncovering Bugs in Formal Explainers: A Case Study with PyXAI
Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, Joao Marques-Silva
November 5, 2025
arXiv.org
3 citations
Key Takeaways
-
Formal explainability tools may contain implementation bugs despite theoretical soundness: PyXAI, a publicly available formal explainer, produced incorrect explanations on most datasets tested, demonstrating that theoretical guarantees don't automatically translate to reliable real-world performance.
-
Validation of AI explanation tools is critically underdeveloped: The paper highlights that formal explainers—which promise rigorous, mathematically-guaranteed explanations—have received little scrutiny for practical correctness, creating a gap between what users assume these tools do and what they actually deliver.
-
A new testing methodology is needed for formal explainers: The authors developed a novel validation approach specifically designed to catch bugs in formal explanation systems, suggesting that standard software testing practices may be insufficient for this specialized domain.
-
Users cannot assume formal explainers are trustworthy without independent verification: The widespread bugs found in PyXAI suggest that organizations deploying formal explainers for high-stakes decisions (hiring, lending, healthcare) should independently validate these tools rather than relying on their theoretical guarantees alone.
Abstract
Formal explainable artificial intelligence (XAI) offers unique theoretical guarantees of rigor when compared to other non-formal methods of explainability. However, little attention has been given to the validation of practical implementations of formal explainers. This paper develops a novel methodology for validating formal explainers and reports on the assessment of the publicly available formal explainer PyXAI. The paper documents the existence of incorrect explanations computed by PyXAI on most of the datasets analyzed in the experiments, thereby confirming the importance of the proposed novel methodology for the validation of formal explainers.