Uncovering Bugs in Formal Explainers: A Case Study with PyXAI

TL;DR

This paper introduces a new methodology for validating formal XAI explainers and demonstrates its effectiveness by uncovering bugs in PyXAI, highlighting the need for rigorous validation of practical implementations.

Contribution

It presents a novel validation methodology for formal explainers and applies it to reveal bugs in the PyXAI tool, emphasizing implementation correctness.

Findings

PyXAI produces incorrect explanations on most datasets tested

The validation methodology effectively uncovers bugs in formal explainers

Highlights the importance of validation in formal XAI tools

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.