Uncovering Bugs in Formal Explainers: A Case Study with PyXAI

TL;DR

The paper tackles the problem of validating formal explainers in XAI by introducing a framework that compares an untrusted target explainer $T$ against untrusted reference $R$ and, when needed, a second explainer $S$, all while queried against the ML model $M$. It formalizes explanations as weak and strong abductive and contrastive explanations via predicates $\mathsf{WAXp}$, $\mathsf{AXp}$, $\mathsf{WCXp}$, and $\mathsf{CXp}$, and details their validation through logic-based checks and witness verification. Applying the framework to the public PyXAI tool with RFxpl and XReason on 27 binary datasets, the authors uncover numerous bugs in PyXAI’s AXp and CXp outputs, supported by case studies and extensive experimental statistics. The work demonstrates that even formal explainers with rigorous foundations can produce incorrect or non-minimal explanations in practice, highlighting the need for cross-validation and, potentially, certified explanations for reliability in real-world deployments.

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.

Figures (1)

• Figure 1: Random Forest trained with Scikit-learn on Boolean dataset xd6 using 4 trees and a max-depth of 4.