We present our work [1, 2] on modal logics for binary-input classifiers and their explanations. They are able to represent classifiers that propositional logic cannot. In particular, black box classifier is understood as uncertainty among admissible classifiers which are coherent with an agent's partial knowledge, and represented in a product modal logic framework. We also briefly show the logics' application to XAI. The notions of explanation and explainability have been extensively investigated by philosophers [3, 4, 5] and are key aspects of AI-based systems. Classifier systems compute a given function in the context of a classification or prediction task. Explaining why the system has classified a given instance in a certain way is crucial for making the system intelligible and for finding biases in the classification process. Thus, a variety of notions of explanations have been discussed in the area of explainable AI (XAI) including abductive, contrastive and counterfactual explanations At the mathematical level, a Boolean classifier is nothing but a Boolean function , and traditionally is represented by a propositional formula . Using modal logic we can model binary-input classifiers which have finite-valued output and are possibly partial. Moreover, it enables us to represent black box classifiers which are key research objects in XAI. A classifier is a white box, if it is determined and given in the model, while black box is understood as uncertainty (indeterminacy) among admissible classifiers which are coherent with an agent's partial knowledge about the classifier. In this paper we present four modal logics for binary-input classifiers in a unified framework: PLC (Product logic for binary-input Classifier) and 1st Workshop on Bias, Ethical AI, Explainability and the role of Logic and Logic Programming, BEWARE-22, co-located ∗Corresponding author. †These authors contributed equally.
WPLC (Weak PLC), according to whether the set of atomic propositions is finite or countably infinite, and whether the represented classifiers are white box or black box, see Table 1.
Cardinality of language is Classifiers are finite white box infinite white box finite black box infinite black box
Furthermore, we exemplify how to apply them to XAI by a) expressing abductive explanation in our language; b) defining its counterpart in the case of black box classifiers; c) formalizing the explanation verification as a model checking problem.
Language Let Atm0 be a countable set of atomic propositions with elements noted , ′, … to denote input variables of classifiers. We introduce a finite set Val to denote the output values (classifications, decisions) of the classifier. Elements of Val are noted , ′, … for classes. For any ∈ Val, we call t() a decision atom, to be read as “the actual decision (or output) takes value ”, and have Dec = {t() ∶ ∈ Val}. Finally, let Atm = Atm0 ∪ Dec. The modal language ℒ (Atm) is hence defined by the following grammar: ∶∶= ∣ t() ∣ ¬ ∣ ∧ ∣ 2I ∣ 2F , where ranges over Atm0, ranges over Val, and is a finite subset of Atm0 which we note ⊆ fin Atm0. Connectives ∨, →, ↔, ◇I and ◇F are defined in the normal way. Let Atm(), Atm0(), Dec() denote the set of all atomic propositions, input variables, and decision atoms in the formula respectively. Finally, let ℒ −2F (Atm) denote the 2F -free fragment of ℒ (Atm).
Semantics The language is built to model (possibly partial) functions from 2Atm0 to Val, and their interactions. Let us begin with the language ℒ −2F (Atm), which is interpreted relative to classifier models whose class is defined as follows.
A classifier model (CM) is a tuple = (, ) where: • ⊆ 2 Atm0 is the set of states, and • ∶ ⟶ Val is a decision (or classification) function.
A pointed CM is a pair (, ) where is a CM and ∈ . We call = (, ) class of (finite) classifier models is noted CM (finite-CM ). ifnite if is finite. The
Hence, the classifier has more than 2 outputs if | ( )| > 2 ; has countably infinite variables if Atm0 is countably infinite; and is partial if ≠ 2 Atm0. Essentially, one can view a CM just as an S5 model on Atm0 with partition labelled by elements in Val, which is indicated by the satisfaction relation defined below, where 2I tentatively seems nothing but an S5 operator. Definition 2 (Satisfaction relation 1). Let ∈ ℒ −2F (Atm), = (, ) be a CM and ∈ : (, ) ⊧ ⟺ ∈ , (, ) ⊧ t() ⟺ () = , (, ) ⊧ ¬ ⟺ (, ) ⊧ ̸, (, ) ⊧ ∧ ⟺ (, ) ⊧ (, ) ⊧ 2I ⟺ ∀ ′ ∈ , (, and (, ) ⊧ , ′) ⊧ .
As mentioned, we think of black box classifier as uncertainty over a set of admissible classifiers coherent with the agent’s partial knowledge. This thought is formalized as the multi-classifier model defined below, which is nothing but a set of CMs with the same set of states. Definition 3 (Multi-classifier model). A multi-classifier model (MCM) is a pair Γ = (, Φ) where ⊆ 2 Atm0 and Φ ⊆ Val , where Val is the set of functions with domain and codomain Val. A pointed MCM is a triple (Γ, , ) where Γ = (, Φ) is an MCM, ∈ and ∈ Φ . We call Γ = (, Φ) ifnite if is finite. The class of all (finite) multi-classifier models is noted MCM (finite-MCM ). Definition 4 (Satisfaction relation 2). Let ∈ ℒ ( Atm), Γ = (, Φ) an MCM, ∈ and ∈ Φ : (Γ, , ) ⊧ (Γ, , ) ⊧ t() (Γ, , ) ⊧ ¬ (Γ, , ) ⊧ ∧ (Γ, , ) ⊧ 2I (Γ, , ) ⊧ ⟺
⟺ ⟺ ⟺ ⟺ ⟺ 2F ∈ ,
() = , (Γ, , ) ⊧ ̸, (Γ, , ) ⊧ and (Γ, , ) ⊧ , ∀ ′ ∈ ∶ (Γ, ′, ) ⊧ , ∀ ′ ∈ Φ ∶ (Γ, , ′) ⊧ .
Both 2I and 2F have standard modal reading but range over diferent sets. 2I has to be read “ necessarily holds for the actual function, regardless of the input instance”, while its dual ◇I = def ¬2I ¬ has to be read “ possibly holds for the actual function, regardless of the input instance”. Similarly, 2F has to be read “ necessarily holds for the actual input instance, regardless of the function” and its dual ◇F has to be read “ possibly holds for the actual input instance, regardless of the function”. Therefore, the agent knows that the actual classification for is , if (Γ, , ) ⊧ 2F t() , i.e. only classifiers outputting for are admissible; and (Γ, , ) ⊧ ◇F t() means that classifying as is coherent with agent’s partial knowledge. With these two modal dimensions, our framework subjects to the so-called product modal logic.
An important abbreviation is the following, where ⊆ fin Atm0: [ ] = def ⋀ ((⋀ ∧ ⊆ ∈
⋀ ¬) → ∈ ⧵ 2I ((⋀ ∧ ∈
⋀ ¬) → ) ).
∈ ⧵
Complex as it seems, [ ] means nothing but “ necessarily holds, if the values of the input
variables in are kept fixed”. It can be justified by checking that (Γ, , ) ⊧ [ ] , if and only if
∀ ′ ∈ , if ∩ = ′ ∩ then (Γ, ′, ) ⊧ . Its dual ⟨ ⟩ = def ¬[ ]¬ has to be read “ possibly
holds, if the values of the input variables in are kept fixed”. These modalities have a ceteris
paribus reading and were first introduced in [
We have to separate two cases, when Atm0 is finite or countably infinite. The reason lays on the axiom Funct in Table 2, which intends to express the “functionality” property cn, Atm0 is not a well-formed formula, and Funct has to be abandoned. syntactically. We define cn, Atm0 =def ⋀∈ ∧ ⋀ ∈ Atm0⧵ ¬ . But when Atm0 is infinite,
We define PLC as the extension of classical propositional logic with and inference rule in Table 2; and WBCL as BCL minus Funct. all axioms and inference rules in Table 2; WPLC as PLC minus Funct; BCL as all 2F -free axioms (■ ∧ ■ ( → ) ) → ■ ■ → ■ → ■ ¬■ → ■ ¬■ 2F 2I ↔ ⋁ t() ∈ Val
2I 2F t() → ¬ t( ′) if ≠ ′ (cn, Atm0 ∧ t() ) → 2I (cn, Atm0 → t() ) → ¬ → ■ 2F 2F ¬ (K■ ) (T■ ) (4■ ) (5■ ) (Comm) (AtLeastt() ) (AtMostt() )
(Funct) (Indep2F, ) (Indep2F,¬ ) (Nec■ ) Axioms and rules of inference, with ■ ∈ {2I , 2F }
We obtained the technical results in Theorem 1 and Table 3, whose proofs are in [
BCL and PLC are sound and complete with respect to CM
WBCL and WPLC are sound and complete with
Finite variables Infinite variables
Polynomial Polynomial NP-complete in NEXPTIME
its negation), which we denote by . We use ( ) to denote all terms whose atoms are in .
In the XAI literature recently people have focused on local explanation, namely to answer why
the given instance is classified as such and so. A central notion is called abductive explanation
[
A X p (, ) = def ∧ [ Atm()] t() ∧ ⟨Atm() ⧵ {}⟩¬
t().
⋁ ∈ Atm()
The three conjuncts mean that 1) is a “part” of the instance; 2) atoms in Atm() staying the same valuation as in , t() necessarily holds regardless of other atoms; 3) is the “minimal” such property, in the sense that any its proper part ′ ⊂ fails condition 2). Hence intuitively, it is suficient and necessary to answer why the actual classification is by saying “because the instance obtains property ”.
Let = (, ) be a CM. We say that is -definite for ⊆ fin Atm0, if ∀, ′ ∈ , ∩ = ′ ∩ then () = ′() . And it is easy to see that is -definite, if (, ) ⊧ D e f ( ) where D e f ( ) = def ⋀∈ Val 2I (⟨ ⟩ t() → [ ] t()) . When the classifier is -definiteness for some ⊆ fin Atm0 , AXp always exists for the actual classification. We may call it the “principle of suficient reason” (PSR) in term of Spinoza [Ethics, 1p11d2], and obtain the following validity. ⊧CM (t() ∧ D e f ( )) → ⋁ A X p (, ) ∈ Term( )
However, a suficient reason may not be known to the agent when the classifier is a black box. We define as a subjective abductive explanation of the actual classification , noted S u b A X p (, ) , if the agent knows that is an abductive explanation of the actual classification , that is:
S u b A X p (, ) = def 2F A X p (, ).
To see how S u b A X p fails PSR, consider the following example. Suppose a classifier trained for deciding whether a paper is acceptable for a conference which has four input features: significance, or iginality, clarity and anonymity. Let 1 and 0 denote acceptance and rejection respectively.
Example 1 (Fail of PSR in black box). Let Γ = (, Φ) be an MCM of this black box, where = 2{,,,} and 1 = {, , } ∈ . Consider 1, 2 ∈ Φ whose syntactic expressions are 2I (t(1) ↔ (( ∧ ) ∨ ( ∧ )) , and 2I (t(1) ↔ ( ∧ )) resp.. Then, (Γ, 1, 1) ⊧ A X p ( ∧ , 1) ∧ ⋀
¬S u b A X p (, 1).
∈ ({,,,})
Therefore, it is of particular interest to determine how much knowledge is needed to verify subjective AXps. This problem can be studied in form of model checking. Let ΓΣ,, 0 = (, Φ Σ,, 0) denote an MCM induced by Σ a finite subset of ℒ −2F (Atm), ⊆ 2 Atm0, 0 ∈ , where ΦΣ,, 0 =def { ∈ Val ∶ ∀ ∈ Σ, (, , 0) ⊧ } . We can formalize the following model checking problem.
Subjective AXp existence Given: finite Σ ⊂ ℒ −2F (Atm), ⊆ 2 Atm0, 0 ∈ .
Question: Does it exist a term s.t. (ΓΣ,, 0, 0, ) ⊧ A X p (, ( 0)) for all ∈ Φ Σ,, 0?
There are many other explanation notions, and logical extensions discussed in [