1 Introduction↩︎

Reasoning about the behavior of AI systems has been receiving significant attention recently, particularly the decisions made by machine learning classifiers. Some methods operate directly on classifiers, e.g., [1], [2] while others operator on symbolic encodings of their input-output behavior, e.g., [3], [4] which may be compiled into tractable circuits [5]–[10]. When explaining decisions, the notion of a sufficient reason has been well investigated. This is a minimal subset of an instance that is sufficient to trigger the decision and can therefore be used to explain why it was made. Sufficient reasons were introduced in [6] under the name of PI explanations and later referred to as abductive explanations [4].¹ Two related notions we discuss later are contrastive explanations as formalized in [14] and counterfactual explanations as formalized in [9].²

[26] introduced the complete reason for a decision as a Boolean formula that characterizes why a decision was made, and showed how it can be used to gather insights about the decision. This includes generating explanations, determining decision bias and evaluating counterfactual queries. For example, it was shown that sufficient reasons correspond to the prime implicants of the complete reason. Hence, if one has access to the complete reason behind a decision, then one can abstract the computation of sufficient reasons away from the classifier and its encoding or compilation. Consider a classifier for admitting applicants to an academic program based five Boolean features [26]: passing the entrance exam (\(E\)), being a first time applicant (\(F\)), having good grades (\(G\)), having work experience (\(W\)) and coming from a rich hometown (\(R\)). The positive instances of this classifier are specified by the following Boolean formula: \(\Delta = (e \vee g)\wedge(e \vee r)\wedge(e \vee w)\wedge(f \vee r)\wedge({\bar{f}} \vee g \vee w).\) Luna (\(\delta\)) passed the entrance exam, has good grades and work experience, comes from a rich hometown but is not a first time applicant (\(\delta = e,{\bar{f}},g,r,w\)). The classifier will admit Luna. The complete reason for this decision is: \(\Gamma = (e\vee g)\wedge(e \vee w)\wedge(r)\wedge({\bar{f}}\vee g \vee w).\) There are four prime implicants of \(\Gamma\): \(\{e,g,r\}, \{e,r,w\}, \{e,{\bar{f}},r\}\) and \(\{g,r,w\}\). Each is a minimal subset of instance \(\delta\) which is sufficient to trigger the admit decision. Even though the number of sufficient reasons may be exponential, the complete reason can be compact and computed in linear time if the classifier is represented using a suitable form [26]. Further insights can be obtained about a decision by analyzing its complete reason. For example, the decision on Luna is biased as it would be different if she did not come from a rich hometown. In that case, she would be denied admission because she does not come from a rich hometown and is not a first time applicant as this would be the only sufficient reason for rejection. These conclusions can be derived by operating directly, and efficiently, on the complete reason as shown in [26].

More recently, [27] introduced the notion of universal literal quantification to Boolean logic and used it to formulate complete reasons. According to this formulation, we can obtain the above complete reason \(\Gamma\) by computing \(\forall e,{\bar{f}},g,r,w \cdot \Delta\), to be explained later. We will base our treatment on this formulation while operating in a discrete instead of a Boolean setting. The conclusion section in [27] proposed a generalization of universal literal quantification to discrete variables but without further discussion. We will adopt this definition, study it further and exploit it to derive efficient, closed-form complete reasons for multi-class decision trees and graphs with nominal (discrete) and numeric (continuous) features. We will show that the obtained complete reasons belong to a particular logical form that arise when explaining the decisions of a broader class of classifiers. We will further show that the prime implicates of complete reasons correspond to contrastive explanations, which will provide further insights into the semantics and utility of these explanations. We will refer to these prime implicates as necessary reasons for the decision and semantically justify this terminology. We will then propose an output polynomial algorithm for computing the shortest necessary reasons of the identified class of complete reasons. We will finally show that computing shortest sufficient reasons is hard for this class of complete reasons and propose an algorithm for computing them which appears to be quite efficient based on an empirical evaluation. Proofs of all results can be found in the appendix.

2 Syntax and Semantics of Discrete Formulas↩︎

We start by defining the syntax and semantics of discrete formulas which we use to capture classifiers with discrete features. The treatment in this section is largely classical and provides obvious generalizations of what is known on Boolean logic. But we spell it out so we can provide a formal treatment of our upcoming results, especially that we sometimes depart from what may be customary.

For a discrete variable \(X\) with values \(x_1, \ldots, x_n\), we will call \({X}\!=\!{x}_i\) a state for variable \(X\). A discrete formula is defined over a set of discrete variables as follows. Every state or constant (\(\top\), \(\bot\)) is a discrete formula. If \(\alpha\) and \(\beta\) are discrete formulas, then \(\neg \alpha\), \(\alpha \vee \beta\) and \(\alpha \wedge \beta\) are discrete formulas. A positive literal is a state \({X}\!=\!{x}_i\) typically denoted by \(x_i\). A negative literal is a negated state \(\neg ({X}\!=\!{x}_i),\) typically denoted by \({\bar{x}}_i\). A negative literal will also be called a state if the variable has only two values. A clause is a disjunction of literals with at most one literal per variable. A term is a conjunction of literals with at most one literal per variable.

A CNF is a conjunction of clauses. A DNF is a disjunction of terms. An NNF is defined as follows. Constants and literals are NNFs. If \(\alpha\) and \(\beta\) are NNFs, then \(\alpha \vee \beta\) and \(\alpha \wedge \beta\) are NNFs (hence, conjunctions and disjunctions cannot be negated). An NNF is \(\vee\)-decomposable iff for each disjunction \(\bigvee_i \alpha_i\) in the NNF, the disjuncts \(\alpha_i\) do not share variables. An NNF is \(\wedge\)-decomposable iff for each conjunction \(\bigwedge_i \alpha_i\) in the NNF, the conjuncts \(\alpha_i\) do not share variables. An NNF is positive iff it contains only positive literals. Any NNF can be made positive by replacing negative literals \({\bar{x}}_i\) with \(\bigvee_{j \neq i} x_j\). An NNF is monotone iff it is positive and does not contain distinct states \(x_i\) and \(x_j\) for any variable \(X\).

A positive term contains only positive literals (i.e., states). The conditioning of discrete formula \(\Delta\) on positive term \(\gamma\) is denoted \(\Delta {|}\gamma\) and obtained as follows. For each state \(x_i \in \gamma\), replace the occurrences of \(x_i\) with \(\top\) and the occurrences of \(x_j\), \(j \neq i\), with \(\bot\). The formula \(\Delta {|}x_i\) does not mention variable \(X\). An instance is a positive term which contains precisely one state for each variable. If we condition a discrete formula on an instance, we get a Boolean formula that does not mention any variables (evaluates to true or false).

The semantics of discrete formulas is symmetric to the semantics of Boolean formulas, except that the notion of a world (truth assignment) is now defined as a function that maps each discrete variable to one of its states (a world corresponds to an instance). A world \({\omega}\) satisfies a discrete formula \(\alpha\), written \({\omega}\models \alpha\), precisely when \(\alpha {|}{\omega}\) evaluates to true. In this case, we say that world \({\omega}\) is a model of formula \(\alpha\). Notions such as satisfiability, validity, implication and equivalence can now be defined for discrete formulas as in Boolean logic. For example, formula \(\alpha\) implies formula \(\beta\), written \(\alpha \models \beta\), iff every model of \(\alpha\) is a model of \(\beta\). We next define the notions of implicants and implicates. An implicant of a discrete formula \(\Delta\) is a term \(\delta\) such that \(\delta \models \Delta\). The implicant is prime iff no other implicant \(\delta^\star\) is such that \(\delta^\star \subset \delta\). An implicate is a clause \(\delta\) such that \(\Delta \models \delta\). The implicate is prime iff no other implicate \(\delta^\star\) is such that \(\delta^\star \subset \delta\).

Our treatment will represent a classifier with discrete features and multiple classes \(c_1, \ldots, c_n\) by a set of mutually exclusive and exhaustive discrete formulas \(\Delta^1, \ldots, \Delta^n\), where the models of formula \(\Delta^i\) capture the instances in class \(c_i\). That is, instance \(\delta\) is in class \(c_i\) iff \(\delta \models \Delta^i\). We refer to each \(\Delta^i\) as a class formula. When \(\delta \models \Delta^i\), we say that instance \(\delta\) is decided positively by \(\Delta^i\). The complete reason for this decision will then be the formula \(\forall \delta \cdot \Delta^i\). The next section will explain what \(\forall \delta\) is and how to compute it efficiently. In the upcoming discussion, we may use the engineering notation for Boolean operators when convenient, writing \(x_1y_2 + x_2 z_3\), for example, instead of \((x_1 \wedge y_2) \vee (x_2 \wedge z_3)\).

3 Quantifying States of Discrete Variables↩︎

[27] introduced universal literal quantification for Boolean logic and suggested the following generalization to discrete variables without further study.

Quantification is commutative so we can equivalently write \(\forall x \cdot (\forall y \cdot \Delta)\), \(\forall y \cdot (\forall x \cdot \Delta)\) or \(\forall \{x,y\} \cdot \Delta\). We will study Definition 1 and exploit it for computing complete reasons.

The next three results parallel Boolean ones in [27]. They are followed by two novel results.

The next result shows when \(\forall x_i\) can be distributed.

Given Propositions 1 and 2, we can universally quantify states out of \(\vee\)-decomposable NNFs in linear time while preserving \(\vee\)-decomposability in the resulting NNF.

Consider the class formula \(\Delta = {\bar{x}}_1(x_2+{\bar{y}}_1)({\bar{y}}_1+z_1)\) over ternary variables \(X\), \(Y\), \(Z\) and instance \(\delta = x_2, y_2, z_1\) which is decided positively by \(\Delta\). The complete reason for this decision is \(\forall \delta \cdot \Delta\). Since \(\Delta\) is \(\vee\)-decomposable, Proposition 3 gives \(\forall x_2, y_2, z_1 \cdot \Delta = (x_2)(x_2+y_2)(y_2+z_1) = x_2(y_2+z_1).\) Hence, this instance was decided positively because it has characteristic \(x_2\) and one of the characteristics \(y_2\) and \(z_1\).

We next identify conditions that allow the distribution of \(\forall x_i\) over disjuncts that share variables.

For a Boolean variable \(X\) with states \(x\) and \({\bar{x}}\), Proposition 4 says that we can distribute \(\forall x\) over disjuncts \(\alpha\) and \(\beta\) even if they mention literal \({\bar{x}}\) (but do not mention \(x\)). This is a novel result compared to [27].

Next is another novel condition that licenses the distribution of \(\forall x_i\) over disjuncts, which we use to derive closed forms for the complete reasons of decision trees and graphs.

Consider variables \(X\) (\(x_1, \ldots, x_4\)) and \(Y\) (\(y_1, y_2\)) and the formulas \(\alpha = y_1 (x_1 + x_2 + x_4)\) and \(\beta = x_1 + x_2\). We can invoke Proposition [prop:wtop] to distribute \(\forall x_1\) using \(S = \{x_1,x_2\}\) and \(S' = \{x_1,x_2,x_4\}\). Hence, \(\forall x_1 \cdot (\alpha \vee \beta) = \forall x_1 \cdot (y_1 (x_1 + x_2 + x_4)) \vee \forall x_1 \cdot (x_1 + x_2) = y_1 x_1 + x_1 = x_1\). Propositions 2 and 4 do not license this distribution of \(\forall x_i\) though.

4 The Complete Reasons for Decision Graphs↩︎

We next provide closed forms for the complete reasons of decision graphs, which subsume decision trees, in the form of monotone, \(\vee\)-decomposable NNFs. This will later facilitate the computation of their prime implicants and implicates (sufficient and necessary reasons). We first treat multi-class decision graphs with nominal features and then treat decision graphs with numeric features; see Figures [fig:admissions-dg] and 3.

Each leaf node in a decision graph is labeled with some class \(c\). Moreover, each internal node \(T\) in the graph has outgoing edges \(\xrightarrow[]{ X,\:S_1}\!T_1, \ldots, \xrightarrow[]{ X,\:S_n}\!T_n\), \(n \geq 2\). We say in this case that node \(T\) tests variable \(X\). The children of node \(T\) are \(T_1, \ldots, T_n\) and \(S_1, \ldots, S_n\) is a partition of some states of variable \(X\). A decision graph will be represented by its root node. Hence, each node in the graph represents a smaller decision graph. We allow variables to be tested more than once on a path from the root to a leaf but under the following condition, which we call the weak test-once property. Consider path \(\ldots, T\xrightarrow[]{ X,\:S_j}\!T_j, \ldots, T'\xrightarrow[]{ X,\:R_k}\!T_k, \ldots\) from the root to leaf and suppose that nodes \(T\) and \(T'\) test variable \(X\). If no nodes between \(T\) and \(T'\) on the path test variable \(X\), then \(\{R_k\}_k\) must be a partition of states \(S_j\). Moreover, if \(T\) is the first node that tests \(X\) on the path, then \(\{S_j\}_j\) must be a partition of all states for \(X\). For binary variables, the weak test-once property reduces to the standard test-once property: A variable can be tested at most once on any path from the root to a leaf. The weak test-once property is critical for treating numeric features. As we show later, one can easily discretize continuous variables based on the thresholds used at decision nodes, which leads to decision graphs that satisfy the weaker test-once property but not the standard one.

A decision graph classifies an instance \(\delta\) as follows. Suppose \(\delta[X]\) is the state of variable \(X\) in instance \(\delta\). We start at the graph root and repeat the following. When we are at node \(T\) that has outgoing edges \(\xrightarrow[]{ X,\:S_1}\!T_1, \ldots, \xrightarrow[]{ X,\:S_n}\!T_n\), we follow the (unique) edge \(\xrightarrow[]{ X,\:S_i}\!T_i\) which satisfies \(\delta[X] \in S_i\). This process leads us to a unique leaf node. The label \(c\) of this leaf node is then the class assigned to instance \(\delta\) by the decision graph (that is, instance \(\delta\) belongs to class \(c\)).

We next provide a closed-form NNF that captures the instances belonging to some class \(c\) in a decision graph.

This NNF is positive and can be constructed in linear time but is not \(\vee\)-decomposable: The disjuncts in \(\bigvee_{x_j \not \in S_i} x_j\) share variables and variable \(X\) will appear in \(\Delta^c[T_j]\) if tested again in graph \(T_j\). Yet, this NNF is tractable for universal quantification as revealed in the proof of the next result, which provides closed-form complete reasons for decision graphs.

Consider the decision graph in Figure [fig:admissions-dg] and an applicant who scored \(< 1450\) on the SAT, had a medium GPA and did not pass their essay or interview. This applicant is rejected by the classifier and the complete reason for the decision, as constructed by Proposition 7, is shown in Figure [fig:admissions-cr].

Even though we are working with decision graphs that include discrete variables and multiple classes, we get complete reasons in the form of monotone NNFs, which are effectively Boolean NNFs. This will simplify the computation of necessary and sufficient reasons in later sections, as it allows us to avoid certain complications that can arise when binarizing discrete variables; see, e.g., [28].

4.1 Numeric Features↩︎

Suppose we have a continuous variable \(X\) that is being tested at node \(T\) in a decision graph. The test will have the form \(X \leq t_i\), where \(t_i\) is a threshold in \((-\infty,\infty)\). Node \(T\) will then have two outgoing edges, one is followed when \(X \leq t_i\) (high edge) and the other is followed when \(X > t_i\) (low edge); see Figure 3. Suppose now that \(t_1, \ldots, t_n\) is the set of all thresholds for variable \(X\) in the decision graph and assume that these thresholds are in increasing order. We can then treat variable \(X\) as a discrete variable with the following \(n+1\) states: \((-\infty,t_1], (t_1,t_2], \ldots, (t_{n-1},t_n], (t_n,\infty)\). If variable \(X\) is being tested first at node \(T\), we label the high edge of node \(T\) with states \((-\infty,t_1], (t_1,t_2], \ldots, (t_{i-1},t_i]\) and its low edge with states \((t_i,t_{i+1}], \ldots, (t_{n-1},t_n], (t_n,\infty)\). Consider Figure 3 (left). Variable “petalwidth" (\(W\)) has three thresholds \(0.6, 1.5, 1.7\), leading to four discrete states \(S_W = (-\infty, 0.6]\), \((0.6, 1.5]\), \((1.5, 1.7]\), \((1.7,\infty)\). Variable”petallength” (\(L\)) has one threshold \(4.9\), leading to two discrete states \(S_L = (-\infty, 4.9]\), \((4.9, \infty)\). Variable \(W\) is tested three times in the decision tree. The first test (\(W \leq 0.6\)) splits states \(S_W\) into \(S_1 = (-\infty, 0.6]\) for the high edge and \(S_2 = (0.6, 1.5], (1.5, 1.7], (1.7,\infty)\) for the low edge. The second test (\(W \leq 1.7\)) splits \(S_2\) into \(S_{21} = (0.6, 1.5], (1.5, 1.7]\) for the high edge and \(S_{22} = (1.7,\infty)\) for the low edge. The third and final test (\(W \leq 1.5\)) splits states \(S_{21}\) into \((0.6, 1.5]\) and \((1.5, 1.7]\). The resulting decision tree with discrete variables does not satisfy the test-once property but does satisfy the weak test-once property as shown in Figure 3 (right).

Consider now instance \(\delta_1: W = 0.8, L = 5.3\) which is classified as “Iris-virginica” by the decision tree with continuous variables (\(T_1\)). We can view this instance as the discrete instance \(\delta_2: W = (0.6,1.5], L = (4.9,\infty)\) since \(0.8 \in (0.6,1.5]\) and \(5.3 \in (4.9,\infty)\). The decision tree with discrete variables (\(T_2\)) will also classify instance \(\delta_2\) as “Iris-virginica.” A continuous instance and its corresponding discrete instance will be classified identically by decision trees \(T_1\) and \(T_2\) because \(T_1\) cannot discriminate continuous values that belong to the same interval. Finally, to generate the complete reason for instance \(\delta_1\), we compute \(\forall \delta_2 \cdot \Delta^c[T_2]\) using Proposition 7 where \(c\) is class “Iris-virginica.”

4.2 Further Extensions↩︎

The closed-form complete reason in Proposition 7 applies directly to Free Binary Decision Diagrams (FBDDs) [29] and Ordered Binary Decision Diagrams (OBDDs) [30] as they are special cases of decision graphs. FBDDs use binary variables and binary classes (\(\top\) and \(\bot\)). OBDDs are a subset of FBDDs which test variables in the same order along any path from the root to a leaf. We can similarly obtain closed forms for the complete reasons of Sentential Decision Diagrams (SDDs) [31], which test on formulas (sentences) instead of variables. This is possible since given an SDD for \(\Delta\) we can obtain an SDD for \(\neg \Delta\) in linear time. An SDD \(\Delta\) is an \(\wedge\)-decomposable NNF that represents instances for class \(\top\). The SDD for \(\neg \Delta\) is also an \(\wedge\)-decomposable NNF but represents instances for class \(\bot\). If we negate \(\Delta\) and \(\neg \Delta\) using deMorgan’s law, we obtain \(\vee\)-decomposable NNFs for classes \(\bot\) and \(\top\), respectively. This allows us to obtain a closed-form, monotone, \(\vee\)-decomposable complete reason for any instance using universal quantification. [27] showed that an SDD can be universally quantified in linear time. Earlier, [26] showed that Decision-DNNFs [32] can be universally quantified in linear time as well.³ Decision-DNNFs cannot be negated efficiently so they do not permit closed-form complete reasons unless we have Decision-DNNFs for classes \(\top\) and \(\bot\). While decision tree classifiers are normally learned from data, classifiers such as OBDDs and SDDs are compiled from other classifiers like Bayesian/neural networks and random forests; see, e.g., [7], [8], [28]. The relative succinctness of these representations of classifiers has been well studied. FBDDs are a subset of Decision-DNNFs and there is a quasipolynomial simulation of Decision-DNNFs by equivalent FBDDs [33]. SDDs and FBDDs are not comparable [34], [35] so SDDs and Decision-DNNFs are not comparable either. SDDs are exponentially more succinct than OBDDs [36].

5 Necessary and Sufficient Reasons↩︎

As mentioned earlier, the prime implicants of a complete reason can be interpreted as sufficient reasons for the decision.

We next show that the prime implicates of a complete reason can be interpreted as necessary reasons for the decision and correspond to contrastive explanations [14]. We first provide further insights into complete reasons which will help in justifying this interpretation.

If instances \(\delta_1\) and \(\delta_2\) are congruent, they must belong to the same class since \(\delta_1 \models \Delta\) and \(\delta_2 \models \Delta\) so they are decided similarly. Moreover, their common characteristics \(\delta_1\cap\delta_2\) are sufficient to justify the decision. That is, the decisions on them are equal and have a common justification.

Hence, the complete reason \(\forall \delta \cdot \Delta\) captures all, and only, instances that are congruent to instance \(\delta\). The complete reason does not capture all instances that are decided similarly to \(\delta\) since some of these instances may be decided that way for a different reason (the decisions are not congruent).

Consider the class formula \(\Delta = {\bar{x}}_1(x_2+{\bar{y}}_1)({\bar{y}}_1+z_1)\) over ternary variables \(X\), \(Y\) and \(Z\). The instance \(\delta = x_2 y_2 z_1\) is decided positively by this formula (\(\delta \models \Delta\)) and the complete reason for this decision is \(\forall x_2, y_2, z_1 \cdot \Delta = x_2(y_2+z_1)\). There are four other instances that satisfy this complete reason, \(x_2 y_2 z_2\), \(x_2 y_2 z_3\), \(x_2 y_1 z_1\) and \(x_2 y_3 z_1\). All are decided positively by \(\Delta\) and the states each share with instance \(\delta\) justify the decision. Instance \(x_3 y_2 z_1\) is also decided positively by \(\Delta\) but for a different reason: the states \(y_2 z_1\) it shares with instance \(\delta\) do not justify the decision, \(y_2 z_1 \not \models \Delta\). Hence, this instance is not captured by the complete reason for \(\delta\).

5.1 Implicants and Implicates as Reasons↩︎

We next review the interpretation of prime implicants as sufficient reasons and discuss the interpretation of prime implicates as necessary reasons for a decision. We will represent these notions by sets of literals, which are interpreted as conjunctions for prime implicants (terms) and as disjunctions for prime implicates (clauses).

A prime implicant \(\sigma\) of the complete reason \(\forall \delta \cdot \Delta\) can be viewed as a sufficient reason for the underlying decision as it is a minimal subset of instance \(\delta\) that is guaranteed to sustain the decision, congruently. If we change any part of the instance but for \(\sigma\), the decision will stick and for a common reason since the new and old instances are congruent. Consider the complete reason in Figure [fig:admissions-cr] which corresponds to a reject decision on the instance SAT \(<1450\), GPA=medium, Essay=fail, Interview=fail. There are two prime implicants for this complete reason: \(\{\text{SAT~<1450, GPA=medium, Interview=fail}\}\) and \(\{\text{Essay=fail, Interview=fail}\}\). Each of these prime implicants is a minimal subset of the instance that is sufficient to trigger the reject decision.

A prime implicate \(\sigma\) of the complete reason \(\forall \delta \cdot \Delta\) can be viewed as a necessary reason for the underlying decision as it is a minimal subset of the instance that is essential for sustaining a congruent decision. If we change all states in \(\sigma\), the decision on the new instance will be different or will be made for a different reason since the new and old instances will not be congruent (we provide a stronger semantics later). Consider again the complete reason in Figure [fig:admissions-cr] and the corresponding instance and reject decision. There are three prime implicates for this complete reason: \(\{\text{Interview=fail}\}\), \(\{\text{SAT~<1450, Essay=fail}\}\) and \(\{\text{GPA=medium, Essay=fail}\}\). Changing Interview to pass will change the decision. Changing SAT to \(\geq 1450\) and Essay to pass will also change the decision. Since GPA is a ternary variable, there are two ways to change its value. If we change GPA and Essay to high and pass, respectively, the decision will change. But if we change these features to low and pass, respectively, the decision will not change but the new instance (SAT \(<1450\), GPA=low, Essay=pass, Interview=fail) will not be congruent with the original instance (SAT \(<1450\), GPA=medium, Essay=fail, Interview=fail). That is, the common characteristics of these instances \(\{\text{SAT~<1450, Interview=fail}\}\) cannot on their own justify the reject decision.

For yet another example, consider again class formula \(\Delta = {\bar{x}}_1(x_2+{\bar{y}}_1)({\bar{y}}_1+z_1)\) over ternary variables \(X\), \(Y\) and \(Z\). The complete reason for positive instance \(\delta = x_2 y_2 z_1\) is \(\Gamma = \forall \delta \cdot \Delta = x_2(y_2+z_1)\). The prime implicants of \(\Gamma\) are \(x_2 y_2\) and \(x_2 z_1\), which are the sufficient reasons for the decision. If we change instance \(\delta\) while keeping one of these reasons intact, the decision sticks. The prime implicates of \(\Gamma\) are \(x_2\) and \(y_2+z_1\), which are the necessary reasons for the decision. If we violate one of these reasons, the decision will be different or made for a different reason. Changing instance \(\delta\) to \(x_2 y_1 z_3\) violates the necessary reason \(y_2+z_1\), which leads to a negative decision. Changing the instance to \(\delta^\star = x_3 y_2 z_1\) violates the necessary reason \(x_2\). The decision remains positive though but for a different reason than why \(\delta\) is positive. That is, the common characteristics \(\delta \cap \delta^\star = y_2 z_1\) do not justify the decision on these instances, \(y_2 z_1 \not \models \Delta\).

5.2 More on Necessity↩︎

We next show that necessary reasons correspond to basic contrastive explanations as formalized in [14] using the following definition (modulo notation).

That is, it is possible to change the decision on instance \(\delta\) by only changing the states in \(\gamma\). Moreover, we must change all states in \(\gamma\) for the decision to change.

This correspondence is perhaps not too surprising given the duality between abductive and contrastive explanations [14] and the classical duality between prime implicants and prime implicates. However, it does provide further insights into contrastive explanations: changing the states of a contrastive explanation leads to a non-congruent decision. It also provides further insights on the necessity of prime implicates: while violating a necessary reason will only lead to an instance that is not congruent (decided differently or for a different reason), there must exist at least one violation of each necessary reason which is guaranteed to change the decision. This follows directly from Definition 5. If the variables of a necessary reason are all binary, there is only one way to violate the reason (by negating each variable in the reason). In this case, violating the necessary reason is guaranteed to change the decision.

For an example, let us revisit the complete reason in Figure [fig:admissions-cr] and the corresponding instance and reject decision. This decision has three necessary reasons: \(\{\text{Interview=fail}\}\), \(\{\text{SAT~<1450, Essay=fail}\}\) and \(\{\text{GPA=medium, Essay=fail}\}\). There is only one way to violate each of the first two reasons, and each violation leads to reversing the decision as we saw earlier. There are two ways to violate the third necessary reason. One of these violations (GPA=high, Essay=pass) reverses the decision but the other violation (GPA=low, Essay=pass) keeps the reject decision intact (but for a different reason).

In summary, a necessary reason (contrastive explanation) identifies a minimal subset of the instance which is guaranteed to change the decision if that subset is altered properly. The minimality condition ensures that we must alter every variable in a necessary reason to change the decision, but it does not specify how to alter it (except for binary variables). We will revisit this distinction when we discuss counterfactual explanations [9].

5.3 Targeting a Particular Class↩︎

Beyond basic contrastive explanations, [14] discussed targeted contrastive explanations which aim to change the instance class from \(c\) to some class \(c^\star\); see [18], [21]. This notion is particularly relevant to multi-class classifiers as it reduces to basic contrastive explanations when the classifier has only two classes. Targeted contrastive explanations can be obtained using the complete reason for why the instance was classified as not \(c^\star\) (that is, a class other than \(c^\star\)). This complete reason can be obtained using a slight modification of Equation ?? where we modify the first two conditions as follows: \[\Gamma^c[T] = \left\{ \begin{array}{ll} \top & if \(T\) has class \(c' \neq c^\star\) \\ \bot & if \(T\) has class \(c^\star\) \\ \bigwedge_{j} (\Gamma^c[T_j] \vee {\ell}_j) & if \(T\) has edges \(\xrightarrow[]{ X,\:S_j}\!T_j\) \end{array} \right. \label{eq:cr-cf-target}\tag{1}\] The prime implicates for this complete reason (i.e., necessary reasons) will then identify minimal subsets of the instance that lead to the targeted class \(c^\star,\) if altered properly.

Consider the decision tree in Figure [fig:target](a) which has two binary features \(X\) and \(Y\) and three classes \(c_1, c_2, c_3.\) The instance \(x_2 y_1\) is classified as \(c_2\). The complete reason for this decision, as computed by Equation ?? , is shown in Figure [fig:target](b) and has two necessary reasons \(x_2\) and \(y_1\). If we violate the first necessary reason (\(x_2 \rightarrow x_1\)), the class changes to \(c_1\). If we violate the second necessary reason (\(y_1 \rightarrow y_2\)), the class changes to \(c_3\). Suppose now we wish to change the class \(c_2\) of this instance particularly to \(c_3\). The complete reason for “why not \(c_3\),” as computed by Equation 1 , is shown in Figure [fig:target](c) and has only one necessary reason, \(y_1\). Violating this necessary reason is guaranteed to change the class to \(c_3\).

[9] discussed the complexity of computing the related notion of counterfactual explanations which are defined as follows. Given an instance \(\delta\) in class \(c\), find an instance \(\delta^\star\) in a different class \(c^\star\) that is as close as possible to instance \(\delta\) with respect to the hamming distance. In other words, instance \(\delta^\star\) must maximize the number of characteristics it shares with instance \(\delta\). Consider now the characteristics \(\gamma\) of instance \(\delta\) that do not appear in instance \(\delta^\star\) (\(\gamma=\delta\setminus\delta^\star\)). Changing these characteristics to \(\gamma^\star = \delta^\star\setminus\delta\) will change the class from \(c\) to \(c^\star\). Hence, characteristics \(\gamma\) are a length-minimal subset of instance \(\delta\) which, if changed properly, will guarantee a change from class \(c\) to class \(c^\star\). Every characteristic of \(\gamma\) must be changed to ensure this class change, otherwise \(\delta^\star\) would not be a counterfactual explanation. Moreover, when the features are binary, there is only one way to change the characteristics \(\gamma\) so the class will change from \(c\) to \(c^\star\); that is, by flipping every characteristic in \(\gamma\) to yield \(\gamma^\star\). In this case, counterfactual explanations are in one-to-one correspondence with the shortest necessary reasons which we discuss next.

6 Computing Shortest Explanations↩︎

A complete reason may have too many prime implicants and implicates. We will therefore provide algorithms for computing the shortest implicants and implicates (which must be prime) for monotone, \(\vee\)-decomposable NNFs. As discussed earlier, we can in linear time obtain complete reasons in this form for decision graphs and SDDs, which include FBDDs, OBDDs and decision trees as special cases.

Shortest Necessary Reasons. This will be an output polynomial algorithm that is based on three (conceptual) passes on the complete reason which we describe next.

The first pass computes the implicate minimum length.

The second pass prunes the NNF using the imlof nodes.

The third pass computes the prime implicates of NNF \(\mathrm{\small prune}(\Delta)\) in output polynomial time. Algorithm [alg:snr] implements the second and third passes assuming the first, linear-time pass has been performed. It represents an implicate by a set of literals and uses the Cartesian product operation on sets of implicates: \(S_1 \times S_2 = \{\sigma_1 \cup \sigma_2 \mid \sigma_1 \in S_1, \sigma_2 \in S_2\}\). Algorithm [alg:snr] applies the second pass implicitly by excluding conjuncts on Line [snr:ln:and]. This is the standard procedure for computing the prime implicates of a monotone NNF, but with no subsumption checking which is critical for its complexity. In the standard procedure, one must ensure that the implicates computed on Lines 5 and [snr:ln:and] are reduced: no implicate \(\sigma_1\) subsumes another \(\sigma_2\) (\(\sigma_1 \subseteq \sigma_2\)).⁴

Since NNF \(\mathrm{\small prune}(\Delta)\) is \(\vee\)-decomposable, the disjuncts \(\alpha_1, \ldots, \alpha_n\) on Line 5 do not share variables. Hence, if every \(\Call{snr}{\alpha_i}\) is reduced, their Cartesian product is reduced. Moreover, due to pruning in the second pass, the implicates \(\Call{snr}{\alpha_i}\) computed on Line [snr:ln:and] all have the same length so no subsumption is possible.

We obtain a tighter complexity if we apply Algorithm [alg:snr] to the closed-form complete reasons of decision trees given by Proposition 7, due to the following bound on the number of prime implicates (a superset of shortest implicates).

The complete reason for a decision tree \(T\) has \(O(|T|)\) nodes and edges, where \(|T|\) is the decision tree size (see Proposition 7). The time and space complexity of Algorithm [alg:snr] is then \(O(|T| \cdot L)\) for decision trees.

[38] showed that the number of contrastive explanations is linear in the decision tree size. Proposition 15 tightens this result by providing a more specific bound. For a decision \(T\) with binary variables and binary classes, [39] showed that the set of all contrastive explanations can be computed in time polynomial in \(|T|+n\), where \(n\) is the number of variables. Algorithm [alg:snr] comes with a tighter complexity for the computation of shortest contrastive explanations for decision trees and applies to multi-class decision trees with discrete features. Another related complexity result is that counterfactual explanations, as discussed earlier, can be enumerated with polynomial delay if the classifier satisfies some conditions as stated in [9].

We finally observe that if an NNF is monotone and \(\wedge\)-decomposable, then one can develop a dual of Algorithm [alg:snr] for computing the shortest prime implicants of the NNF.

Shortest Sufficient Reasons We next present Algorithm [alg:ssr] for computing the shortest implicants of monotone, \(\vee\)-decomposable NNFs which is a hard task. For decision trees, the problem of deciding whether there exists a sufficient reason of length \(\leq k\) is NP-complete [40]. Since decision trees have closed-form complete reasons that are monotone and \(\vee\)-decomposable, computing the shortest implicants for this class of NNFs is hard. [39] showed that the number of shortest sufficient reasons for decision trees can be exponential and provided an incremental algorithm for computing the shortest sufficient reasons for decision trees with binary variables and binary classes, based on a reduction to the Partial MaxSat problem. Algorithm [alg:ssr] has a broader scope, does not require a reduction and is based on two key techniques.

The first technique is to compute all unsubsumed implicants of length \(\leq k\), called \(k\)-implicants, starting with \(k=0\). If no implicants are found, \(k\) is incremented and the process is repeated. The second technique relates to computing the \(k\)-implicants of a conjunction \(\alpha \wedge \beta\). If we have the \(k\)-implicants \(S\) for \(\alpha\) and the \(k\)-implicants \(R\) for \(\beta\), we can compute the Cartesian product \(S \times R\) and keep unsubsumed implicants of length \(\leq k\). Algorithm [alg:ssr] does something more refined. It first computes the \(k\)-implicants \(S\) for \(\alpha\). For each implicant \(\sigma \in S\), it then computes and accumulates the \(k'\)-implicants for \(\beta | \sigma\) where \(k' = k - |\sigma|\). These techniques control the number of generated \(k\)-implicants at each NNF node (smaller \(k\) leads to fewer \(k\)-implicants). Our implemented caching scheme on Lines 6 & [ssr:ln:i-cache] exploits the following properties. If the \(k\)-implicants for \(\Delta | \sigma\) are \(\{\{\}\}\), then these are also its \(j\)-implicants for all \(j\). Further, if we cached the \(k\)-implicants for \(\Delta | \sigma\), then we can use them to retrieve its \(j\)-implicants for any \(j \leq k\) by selecting implicants of length \(\leq j\). We empirically evaluate Algorithms [alg:snr] & [alg:ssr] next.

Empirical Evaluation. Table 1 depicts an empirical evaluation on decision trees learned from OpenML datasets [41] and binary decision graphs compiled from Bayesian network classifiers [7], [42]. The decision trees were learned by weka [43] using python-weka-wrapper3 available at pypi.org. We used weka’s J48 classifier with default settings, which learns pruned C4.5 decision trees with numeric and nominal features [44]. Each dataset was split using weka into training (\(85\%\)) and testing (\(15\%\)) data. We aimed for OpenML datasets with more than \(100\) features since many smaller datasets we tried were very easy, but we kept a few smaller ones since they are commonly reported on (adult, compas, spambase). Some of the learned decision trees had significantly fewer variables than the corresponding datasets (e.g., gisette has \(5000\) features but the learned decision tree has \(111\)). The decision graphs we used are the reportedly largest ones compiled by [7], [42]. For each decision tree, we computed reasons for decisions on \(1000\) instances sampled from testing data (or all testing data if smaller than \(1000\)). We tried random instances but they were much easier. For each decision graph, we computed complete reasons for \(1000\) random instances (there is no corresponding data). The total number of instances for the fifteen benchmarks was \(13963\). We did not report the time for computing a complete reason as this is a closed form with linear size (Equation ?? ).

We compared four algorithms: snr(Algorithm [alg:snr]), nr(standard algorithm for computing prime implicates of a monotone NNF but with no subsumption checking at \(\vee\)-nodes since the input NNF is \(\vee\)-decomposable),⁵ ssr(Algorithm [alg:ssr]) and sr(dual of nr). Each instance had a timeout of \(60\) seconds. In Table 1, nodes, num, nom, classes; card and acc stand for number of nodes, numeric features, nominal features, classes; maximum cardinality of variables and accuracy. Count and time are averages over instances that both sr/ssr(nr/snr) finished. The bolded exponent of time is the number of instances that timed out (not reported if zero). The supplementary material contains further statistics such as stdev, mean and max. We used a Python implementation on a dual Intel(R) Xeon E5-2670 CPUs running at 2.60GHz and 256GB RAM. As revealed by Table 1, ssris quite effective. Its average running time is normally in milliseconds, it timed out on only \(37\) instances and can be two orders of magnitude faster than srwhich timed out on \(2222\) instances. snris also much faster than nrbut the latter is also very effective on decision trees (see Proposition 15) but timed out on \(19\) decision graph instances. All algorithms are quite effective on the easier benchmarks.

7 Conclusion↩︎

We studied the computation of complete reasons for multi-class classifiers with nominal and numeric features. We derived closed forms for the complete reasons of decision trees and graphs in the form of monotone, \(\vee\)-decomposable NNFs and showed how similar forms can be derived for SDDs. We further established a correspondence between the prime implicates of complete reasons and contrastive explanations. We then presented an output polynomial algorithm for enumerating the shortest implicates (shortest necessary reasons) for complete reasons in the above form. We also presented a simple algorithm for enumerating the shortest implicants (shortest sufficient reasons) which appears to be effective based on an empirical evaluation over fifteen datasets.

8 Acknowledgements↩︎

This work has been partially supported by NSF grant #ISS-1910317 and ONR grant #N00014-18-1-2561.

9 Proofs↩︎

References↩︎