A unified logical framework for explanations in classifier systems

要約

近年、説明可能なAI（XAI）の分野において、二値分類器を説明するためのブール関数に再び注目が集まっている。ブール関数の標準的なアプローチは命題論理である。我々は、二値入力分類器とその性質に関する推論をサポートする、セテリス・パリブスの性質を持つ様相言語を提示する。分類器モデルのファミリーを研究し、言語のカーディナリティに関する2つの証明体系として公理化し、公理論の完全性を示す。さらに、モーダル言語の充足可能性検査問題は、無限変数の場合にはNEXPTIME完全であるが、有限変数の場合には多項式になることを証明する。さらに、無限変数の場合には、我々の言語の興味深いNPフラグメントを特定する。我々は、この言語を活用して、帰納的説明、対比的説明、反事実的説明、バイアスを含む説明の様々な概念と同様に、反事実的条件式を形式化する。最後に、分類器の変更を可能にする代入の概念による動的拡張と、実際の入力に対する分類器の不確実性を表現できる認識論的拡張である。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL