A Logic for Binary Classifiers and Their Explanation

Recent years have witnessed a renewed interest in Boolean functions in explaining binary classifiers in the field of explainable AI (XAI). The standard approach to Boolean functions is based on propositional logic. We present a modal language of a ceteris paribus nature which supports reasoning about binary classifiers and their properties. We study a family of classifier models, axiomatize it and show completeness of our axiomatics. Moreover, we prove that satisfiability checking for our modal language relative to such a class of models is NP-complete. 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.