A unified logical framework for explanations in classifier systems
This work provides a formal foundation for explanations in classifier systems, addressing the need for rigorous reasoning in XAI, though it is incremental as it builds on existing Boolean function approaches.
The authors tackled the problem of explaining binary classifiers in explainable AI by developing a unified modal logical framework that supports reasoning about classifier properties and various explanation types, resulting in a language with NEXPTIME-complete satisfiability checking in infinite-variable cases and polynomial complexity in finite-variable cases.
Recent years have witnessed a renewed interest in Boolean function in explaining binary classifiers in the field of explainable AI (XAI). The standard approach of Boolean function is propositional logic. We present a modal language of a ceteris paribus nature which supports reasoning about binary input classifiers and their properties. We study a family of classifier models, axiomatize it as two proof systems regarding the cardinality of the language and show completeness of our axiomatics. Moreover, we prove that satisfiability checking problem for our modal language is NEXPTIME-complete in the infinite-variable case, while it becomes polynomial in the finite-variable case. We furthermore identify an interesting NP fragment of our language in the infinite-variable case. We leverage the language to formalize counterfactual conditional as well as a variety of notions of explanation including abductive, contrastive and counterfactual explanations, and biases. Finally, we present two extensions of our language: a dynamic extension by the notion of assignment enabling classifier change and an epistemic extension in which the classifier's uncertainty about the actual input can be represented.