Logic for Explainable AI
^††thanks: This work has been partially supported by NSF grant #ISS-1910317.

We assume a finite set of discrete variables $\Sigma$. Each variable $X\in\Sigma$ has a finite number of states $x_{1},\ldots,x_{n},$ $n>1$. A literal $\ell$ for variable $X$, called an $X$-literal, is a set of states such that $\emptyset\subset\ell\subset\{x_{1},\ldots,x_{n}\}$. We often denote a literal such as $\{x_{1},x_{3},x_{4}\}$ by $x_{134}$ which reads: the state of variable $X$ is either $x_{1}$ or $x_{3}$ or $x_{4}$. A literal is simple iff it contains a single state. Hence, $x_{3}$ is a simple literal but $x_{134}$ is not. Since a simple literal corresponds to a state, we use these two notions interchangeably. If a variable $X$ has two states, it is said to be Boolean or binary and its states are denoted by $x$ and $\overline{x}$. Such a variable can only have two simple literals, $\{x\}$ and $\{\overline{x}\}$, denoted $x$ and $\overline{x}$ for convenience. A formula is either a constant $\top$, $\bot$, literal $\ell$, negation $\overline{\alpha}$, conjunction $\alpha\cdot\beta$ or disjunction $\alpha+\beta$ where $\alpha$, $\beta$ are formulas. The set of variables appearing in a formula $\Delta$ are denoted by $\texttt{vars}(\Delta)$.

The semantics of discrete logic directly generalize those of Boolean logic. A world, denoted $\omega$, maps each variable in $\Sigma$ to one of its states. A world $\omega$ is called a model of formula $\alpha$, written $\omega\models\alpha$, iff $\alpha$ is satisfied by $\omega$ (that is, $\alpha$ is true at $\omega$). The constant $\top$ denotes a valid formula (satisfied by every world) and the constant $\bot$ denotes an unsatisfiable formula (has no models). Formula $\alpha$ implies/entails formula $\beta$, written $\alpha\models\beta$, iff every model of $\alpha$ is also a model of $\beta$. In this case, we say $\alpha$ is stronger than $\beta$ and also say $\beta$ is weaker than $\alpha$.

A discrete variable $X\in\Sigma$ is called a feature and a state $x_{i}$ (or simple literal $\{x_{i}\}$) is called a characteristic. An instance is a conjunction of characteristics, one for each feature in $\Sigma$ (instances are in one-to-one correspondence with worlds).

The decision graph below is a classifier with three ternary features $X,Y,Z$ and three classes $c_{1},c_{2},c_{3}$. Its class formulas are $\Delta_{1}=x_{12}+x_{3}\cdot y_{1}\cdot z_{13}$, $\Delta_{2}=x_{3}\cdot z_{2}$ and $\Delta_{3}=x_{3}\cdot y_{23}\cdot z_{13}$.

This classifier has $27$ instances: $20$ in class $c_{1}$, $3$ in class $c_{2}$ and $4$ in class $c_{3}$. For example, instance ${\cal I}=x_{3}\cdot y_{2}\cdot z_{2}$ is in class $c_{2}$ since ${\cal I}\models\Delta_{2}$. Again, even though a classifier may take different forms, the presented theory of explainability views it as a set of class formulas since this is all we need to explain decisions.

The answers to questions Q1, Q2 and Q3 will be expressed using logical formulas that have normal forms, discussed next. A term is a conjunction of literals for distinct variables. A clause is a disjunction of literals for distinct variables. A Disjunctive Normal Form (DNF) is a disjunction of terms. A Conjunctive Normal Form (CNF) is a conjunction of clauses. A Negation Normal Form (NNF) is a formula with no negations. These definitions imply that terms cannot be inconsistent, clauses cannot be valid, DNFs and CNFs are NNFs, and none of these normal forms can include negations. We say a formula (term/clause) is simple if it contains only simple literals. Simple and non-simple formulas will delineate two approaches for answering questions Q1, Q2 and Q3 based on the amount of information they convey about decisions.

When constructing abstractions of instances to explain decisions, the notion of conditioning plays a central role. Observe first that a simple term like $x_{1}\cdot y_{3}\cdot z_{2}$ represents a set of states. The conditioning of formula $\Delta$ on a simple term $\tau$ is denoted by $\Delta|\tau$ and obtained as follows. For each state $x_{i}$ that appears in the simple term $\tau$, replace each $X$-literal $\ell$ in $\Delta$ with $\top$ if $x_{i}\in\ell$; otherwise, replace $\ell$ with $\bot$. Consider the formula $\Delta=x_{12}+x_{3}\cdot y_{1}\cdot z_{13}$ and the simple term $\tau=x_{3}\cdot z_{1}$. Then $\Delta|\tau=\bot+\top\cdot y_{1}\cdot\top=y_{1}$. In general, the conditioned formula $\Delta|\tau$ does not mention any variable that appears in term $\tau$.

Questions Q2 and Q3 involve a notion of minimality that will be captured using the classical notions of prime implicants and implicates. A term $\tau$ is called an implicant of formula $\Delta$ iff it implies $\Delta$ ($\tau\models\Delta$). It is called a prime implicant if no other implicant of $\Delta$ is weaker than $\tau$ (i.e., $\tau\models\tau^{\prime}\models\Delta$ does not hold for any term $\tau^{\prime}\neq\tau$). A clause $\sigma$ is an implicate of formula $\Delta$ iff it is implied by $\Delta$ ($\Delta\models\sigma$). It is called a prime implicate if no other implicate of $\Delta$ is stronger than $\sigma$ (i.e., $\Delta\models\sigma^{\prime}\models\sigma$ does not hold for any clause $\sigma^{\prime}\neq\sigma$). A prime implicant $\tau$ is variable-minimal iff no other prime implicant $\tau^{\prime}$ satisfies $\texttt{vars}(\tau^{\prime})\subset\texttt{vars}(\tau)$. Variable-minimal prime implicates are defined similarly.

The prime implicants and implicates of discrete formulas behave in ways that may surprise someone who is accustomed to these notions in a Boolean setting. Moreover, these behaviors have interesting implications on questions Q2 and Q3. Consider the Boolean formula $\Delta_{b}=(x+\overline{z})\cdot(x\cdot z+y)$. The term $x\cdot y\cdot\overline{z}$ is an implicant but not prime. The only way to weaken this term so it becomes prime is by dropping some of its variables ($y\cdot\overline{z}$ is a prime implicant). In discrete logic, we can possibly weaken a term without dropping any of its variables, by adding states to some of its literals. Consider the discrete formula $\Delta_{d}=(x\cdot z_{1}+z_{2})\cdot(x\cdot z_{3}+y)$, where variable $Z$ is ternary and variables $X,Y$ are binary. The term $x\cdot y\cdot z_{1}$ is an implicant of this formula but is not prime. We can weaken this term by adding the state $z_{2}$ to literal $z_{1}$, leading to the prime implicant $x\cdot y\cdot z_{12}$. A symmetrical situation arises for prime implicates: the only way to strengthen a Boolean clause is by dropping some of its variables but we can strengthen a discrete clause by removing states from its literals.

The first proposal requires the sought condition—that is, the reason for the decision—to be constructed from states that appear in the instance which can be combined in any fashion but using only conjunctions and disjunctions. Technically speaking, it requires the condition to be a simple NNF formula whose literals all appear in the instance being explained. This leads to the notion of complete reason introduced in [5].²²2Ref. [5] gave a different but equivalent definition and for binary variables. See [4] for a more general treatment.

We stress here that the complete reason is a simple NNF formula, that is, every literal it contains corresponds to a state.

Consider a classifier with three ternary features $X,Y,Z$. Instance ${\cal I}=x_{2}\cdot y_{2}\cdot z_{1}$ is decided as belonging to class $c_{2}$ which has formula $\Delta_{2}=x_{23}\cdot(x_{2}+y_{23})\cdot(y_{23}+z_{1})$. The complete reason for this decision is $x_{2}\cdot(y_{2}+z_{1})$. It says that instance ${\cal I}$ belongs to class $c_{1}$ because it has characteristic $x_{2}$ and one of the two characteristics $y_{2},z_{1}$. This is indeed the most general condition on the instance which implies the class formula and that is constructed by applying conjunctions and disjunctions to the instance characteristics $x_{2}$, $y_{2}$ and $z_{1}$.

Two questions become relevant now. First, how do we compute the complete reason? Second, how can we use complete reasons when they are too complex to be interpretable by humans? We will address the first question next while leaving the second question until later in the tutorial.

Ref. [5] showed that if the class formula is appropriately represented (e.g., as an OBDD [6]), the complete reason can be computed in linear time. A major development then came in [7] which introduced the following quantification operator and showed that it can be used to express the complete reason.

This operator is commutative so it is meaningful to quantify an instance ${\cal I}$ from its class formula $\Delta_{i},$ written $\forall{\cal I}\cdot\Delta_{i}$, by quantifying the states of ${\cal I}$ in any order. Moreover, $\forall{\cal I}\cdot\Delta_{i}$ corresponds to the complete reason as shown in [7] for Boolean variables and in [4] for discrete variables. One significance of this result is that this quantification operator is well behaved computationally on a number of logical forms. For example, one can quantify any set of states from a CNF in linear time. More generally, the operator distributes over conjunctions, and distributes over disjunctions when the disjuncts do not share variables as also shown in [7] (see weaker conditions in [4]). This brought into focus the following form of class formulas as it allows one to compute complete reasons in linear time (and general reasons too that are discussed in Section III-B).

Due to this form and some of its weakenings, [4] provided closed-form complete reasons for certain classes of classifiers that are based on decision graphs.

We now turn to a recent development [2] that identified a weaker requirement on abstractions of instances which can produce more information when explaining decisions.⁴⁴4Def. 5 is actually a proposition in [2]. We reversed the formulation here to serve the storyline in this tutorial.

The only difference between the complete reason and the general reason is that the former requires literals to appear in the instance, while the latter only requires that they are implied by the instance. Hence, general reasons are no longer simple formulas like complete reasons as they may contain non-simple literals. If all features are binary, then every literal is simple and the complete and general reasons are equal. However, in the presence of non-binary features, general reasons provide more information about why a decision was made. Let us see this through an example.

Consider the classifier in Fig. 3 and a patient Rob,

decided as yes. The complete reason for the decision is

and the general reason is

The complete reason justifies the decision by Rob having Diabetes and a Btype of A. But the general reason provides weaker justifications. One of them is that Rob has Diabetes and his Btype is not AB or O. Another justification is that he has Diabetes, his Weight is not norm and his Btype is not O.

The additional information provided by general reasons is particularly critical in the context of discretized classifiers. Consider again the decision tree in Fig. 2 which has two numeric features Age, BMI. The feature Age is discretized into three intervals $[0,18),[18,40)$ and $[40,\infty)$ with corresponding labels $a_{1},a_{2},a_{3}$. The feature BMI is discretized into four intervals $[0,25),[25,27),[27,30),[30,\infty)$ with corresponding labels $b_{1},b_{2},b_{3},b_{4}$. Hence, Age can be treated as a discrete variable with states $a_{1},a_{2},a_{3}$ and BMI can be treated as a discrete variable with states $b_{1},b_{2},b_{3},b_{4}$. Consider now the instance ${{\footnotesize\textsc{Age}}}\mathord{=}\mathord{42}\cdot{{\footnotesize\textsc{BMI}}}\mathord{=}\mathord{28}$ which is discretized into $a_{3}\cdot b_{3}$ (${\footnotesize\textsc{Age}}\geq 40$ and $27\leq{\footnotesize\textsc{BMI}}<30$). The decision on this instance is yes and its class formula $\Delta_{{\footnotesize\textsc{yes}}}$ is $a_{1}\cdot b_{4}+a_{2}\cdot b_{34}+a_{3}\cdot b_{234}$ (obtained by tracing the paths leading into class yes). The complete reason for this decision is $a_{3}\cdot b_{3}$ which is the instance itself so no abstraction took place. The general reason is $a_{23}\cdot b_{34}+a_{3}\cdot b_{234}$ which reads

This is a weaker property of the instance that still implies the decision. For example, the first part says the decision is justified by Age being no less than $18$ and BMI being no less than $27$. These kind of justifications are impossible to obtain using complete reasons as such reasons can only reference instance characteristics, that is, ${\footnotesize\textsc{Age}}\geq 40$ and $27\leq{\footnotesize\textsc{BMI}}<30$.

General reasons can also be expressed using a quantification operator introduced in [2].

This operator is also commutative so we can quantify an instance ${\cal I}$ from its class formula $\Delta_{i},$ written $\overline{\forall}\,{\cal I}\cdot\Delta_{i}$, by quantifying the states of ${\cal I}$ in any order. Moreover, $\overline{\forall}\,{\cal I}\cdot\Delta_{i}$ corresponds to the general reason for the decision on instance ${\cal I}$ as shown in [2]. The operators $\forall$ and $\overline{\forall}\,$ have similar computational properties as far as distributivity and tractability on forms such as CNFs and or-decomposable NNFs. This is why, similar to complete reasons, we also have closed-form general reasons for certain classes of classifiers [2].

Complete and general reasons satisfy a property called fixation, which has key implications including on computation as we discuss later. This property was also identified in [2].

The formula $x_{12}\cdot y_{13}+z_{23}$ is locally fixated on the instance ${\cal I}=x_{1}\cdot y_{1}\cdot z_{2}$, but this is not true for the formula $x_{12}\cdot y_{23}+z_{23}$ since the literal $y_{23}$ is not consistent with the instance ${\cal I}$. The fixation of complete reasons follows directly from Def. 2 and the fixation of general reasons follows directly from Def. 5.

If a simple formula is fixated then it is also monotone.

For example, the formula $(x_{1}+y_{2})\cdot(x_{1}+z_{3})\cdot(y_{2}+z_{3})$ is monotone, but the formulas $(x_{1}+y_{2})\cdot(x_{12}+z_{3})\cdot(y_{2}+z_{3})$ is not monotone since it contains a non-simple literal $x_{12}$. The formula $(x_{1}+y_{2})\cdot(x_{1}+z_{3})\cdot(y_{3}+z_{3})$ is not monotone either since it contains distinct literals $y_{2}$ and $y_{3}$ for variable $Y$. Complete reasons are known to be monotone and this property was exploited computationally in [5, 4] when computing the prime implicants and implicates of complete reasons.

For an instance ${\cal I}$ and its class formula $\Delta_{i}$, we have [2]:

so the general reason is always weaker than the complete reason. The above relations also show that reasons, whether complete or general, are stronger than class formulas. Hence, the operators $\forall$ and $\overline{\forall}\,$ can be viewed as selection operators since they select subsets of the instances in class $c_{i}$ [7, 2]. In particular, $\forall{\cal I}\cdot\Delta_{i}$ selects all instances in class $c_{i}$ whose membership in the class does not depend on characteristics that are inconsistent with instance ${\cal I}$. For example, suppose that instance ${\cal I}^{\prime}$ is in class $c_{i}$ and disagrees with instance ${\cal I}$ only on the states of features $X,Y,Z$. Then ${\cal I}^{\prime}$ will be selected by $\forall{\cal I}\cdot\Delta_{i}$ iff changing the states of any subset of its features $X,Y,Z$ yields an instance that is also in class $c_{i}$. In contrast, $\overline{\forall}\,{\cal I}\cdot\Delta_{i}$ selects all instances that remain in class $c_{i}$ if any of their characteristics are changed to agree with instance ${\cal I}$ (these include the ones selected by $\forall{\cal I}\cdot\Delta_{i}$). In the previous example, instance ${\cal I}^{\prime}$ will be selected by $\overline{\forall}\,{\cal I}\cdot\Delta_{i}$ iff setting the states of any subset of its features $X,Y,Z$ to the states they have in ${\cal I}$ yields an instance that is also in class $c_{i}$.

We assume in this section that our goal is to undermine the current decision, without targeting a particular alternate decision. This aim can be achieved using the following notion.

Each necessary reason is a clause $\ell_{1}+\ldots+\ell_{n}$ where each literal $\ell_{i}$ is simple (a state) and appears in instance ${\cal I}$.⁸⁸8Since the complete reason is simple and fixated on the instance. Hence, each necessary reason is satisfied by the instance. However, if we change the instance in a way that violates a necessary reason, the decision is no longer guaranteed to be sustained. Suppose state $\ell_{i}$ is for feature $X_{i}$. To violate the necessary reason $\ell_{1}+\ldots+\ell_{n}$ we must change the state of each feature $X_{i}$ in the instance. The guarantee that comes with a necessary reason is that at least one such change will flip the decision, and no strict subset of this change will flip the decision.

The notion of a necessary reason was first formalized in [12] using a different but equivalent definition, under the name of a contrastive explanation [13]. Necessary reasons are sometimes also called counterfactual explanations [14].⁹⁹9There is an extensive body of work in philosophy, social science and AI that discusses contrastive explanations and counterfactual explanations; see, e.g., [15, 16, 17, 18, 19, 20, 21, 22, 23, 24]. While the definitions of these notions are sometimes variations or refinements on one another, they are not always compatible. The term “necessary reason” was first used in [4] which showed that contrastive explanations are the prime implicates of the complete reason and provided the semantics of necessity discussed earlier (a property that must be preserved if the decision is to be preserved). Let us now illustrate necessary reasons using a concrete example.

We are back to patient Lara given in (1) who was decided as yes by the classifier in Fig. 3. The class formula is given in (2) and the complete reason for the decision is given in (3). This complete reason has two prime implicates, $({{\footnotesize\textsc{Diabetes}}}\mathord{=}\mathord{{\footnotesize\textsc{y}}})$ and $({{\footnotesize\textsc{Weight}}}\mathord{=}\mathord{{\footnotesize\textsc{over}}})+({{\footnotesize\textsc{Btype}}}\mathord{=}\mathord{{\footnotesize\textsc{A}}})$. There is only one way to violate the first reason by setting Diabetes to n, which will indeed flip the decision to no as can be verified in Fig. 3. The second necessary reason can be violated in six different ways, by setting Weight to a state in $\{{\footnotesize\textsc{under}},{\footnotesize\textsc{norm}}\}$ and setting Btype to a state in $\{{\footnotesize\textsc{B}},{\footnotesize\textsc{AB}},{\footnotesize\textsc{O}}\}$. Not all of these changes/violations will flip the decision but at least one will. The change to $({{\footnotesize\textsc{Weight}}}\mathord{=}\mathord{{\footnotesize\textsc{under}}})\cdot({{\footnotesize\textsc{Btype}}}\mathord{=}\mathord{{\footnotesize\textsc{O}}})$ does flip the decision but the change to $({{\footnotesize\textsc{Weight}}}\mathord{=}\mathord{{\footnotesize\textsc{under}}})\cdot({{\footnotesize\textsc{Btype}}}\mathord{=}\mathord{{\footnotesize\textsc{AB}}})$ does not (always assuming that Diabetes is left unchanged). We stress again that no strict subset of the first change will flip the decision since the changes suggested by necessary reasons are minimal.

We will now see that we can do better than this if we employ the general reasons of decisions as suggested recently in [2].

Like necessary reasons, violating a general necessary reason will undermine the decision. However, we now have an additional guarantee: every violation of a general necessary reason will flip the decision. This guarantee will not hold if we do not insist on variable-minimal prime implicates, and if some prime implicate that is not variable minimal satisfies this guarantee, then some changes it suggests cannot be minimal (i.e., we can flip the decision with fewer changes to the instance). Moreover, any change that flips the decision and is suggested by some necessary reason will also be suggested by some general necessary reason. That is, the latter reasons subsume the former and convey more information about decisions and the underlying classifiers.¹¹¹¹11The general necessary reasons are fixated (Def. 7) on instance ${\cal I}$. Let us look at a concrete example.

The general reason for the decision on Lara is given in (6) and has three prime implicates

All are variable-minimal so they are all general necessary reasons. The first can be violated in only one way by setting Diabetes to n which will flip the decision. The second can be violated in two ways by setting Weight to a state in $\{{\footnotesize\textsc{under}},{\footnotesize\textsc{norm}}\}$ and setting Btype to state O. Both violations will flip the decision as can be verified using the classifier in Fig. 3. The third general necessary reason can be violated in two ways by setting Weight to state norm and setting Btype to a state in $\{{\footnotesize\textsc{AB}},{\footnotesize\textsc{O}}\}$. Again, both violations will flip the decision. Hence, every violation of these general necessary reasons is guaranteed to flip the decision. Moreover, every change suggested by a necessary reason and which flips the decision is also suggested by some general necessary reason.

We conclude this section by the following remarks. Boolean resolution derives the clause $\alpha+\beta$ from clauses $x+\alpha$ and $\overline{x}+\beta$. Moreover, a classical method for computing prime implicates of Boolean CNFs is to close the CNF under resolution and remove subsumed clauses after each resolution step; see, e.g., [25, 26]. As recently shown in [2], this can also be done for discrete CNFs but using a generalized resolution rule that derives clause $\ell\cdot\ell^{\prime}+\alpha+\beta$ from clauses $\ell+\alpha$ and $\ell^{\prime}+\beta$ where $\ell$ and $\ell^{\prime}$ are literals for the same variable. What is particularly striking is this. If the CNF is locally fixated (Def. 7), as is the case for general reasons, then one can compute the general necessary reasons by simply discarding clauses that are not variable-minimal after each resolution step [2].

The previous discussion showed how (general) necessary reasons can be used to flip a decision but without a guarantee on what the new decision is. This becomes an issue when the classifier has more than two classes and hence can make more than two decisions. Consider a classifier that decides whether an applicant should be approved for large loan ($c_{1}$), approved for a small loan ($c_{2}$) or declined ($c_{3}$). Let $\Delta_{1},\Delta_{2},\Delta_{3}$ be the corresponding class formulas and suppose we have an applicant ${\cal I}$ who was approved for a small loan, that is, ${\cal I}\models\Delta_{2}$. The (general) necessary reasons for this decision do suggest minimal changes to the application that will flip the decision but they do not guarantee whether the new decision will approve a larger loan or decline the application. Suppose that we wish to flip the decision so the applicant is approved for a larger loan ($c_{1}$). What we can do is merge classes $c_{2}$ and $c_{3}$ leading to a classifier with two decisions $c_{1},c_{23}$ and corresponding class formulas $\Delta_{1}$ and $\Delta_{23}=\Delta_{2}+\Delta_{3}$. The decision to approve a small loan $(c_{2})$ in the original classifier, ${\cal I}\models\Delta_{2}$, is now a decision to approve a small loan or decline the application ($c_{23}$) in the new classifier, ${\cal I}\models\Delta_{23}$. Flipping this decision is then guaranteed to approve a large loan ($c_{1}$).

More generally, suppose we have a classifier with classes $c_{1},\ldots,c_{n}$, class formulas $\Delta_{1},\ldots,\Delta_{n}$, and an instance ${\cal I}$ in class $c_{i}$, ${\cal I}\models\Delta_{i}$. If we wish to minimally change this instance so it moves to some other class $c_{j}$, we need to compute the complete reason $\forall{\cal I}\cdot\sum_{k\neq j}\Delta_{k}$ or the general reason $\overline{\forall}\,{\cal I}\cdot\sum_{k\neq j}\Delta_{k}$. This can then be followed by computing the (variable-minimal) prime implicates of these reasons as discussed earlier. This technique of merging class formulas was proposed in [4] and the resulting necessary reasons have been known as targeted contrastive explanations [12].

Compiling the class formulas of Bayesian network classifiers is perhaps the most subtle conceptually since deciding what instance belongs to what class requires probabilistic reasoning. There are two fundamental insights behind this compilation process. The first is the notion of equivalence intervals introduced in [29]. Consider the Naïve Bayes classifier in Fig. 1(a) which has the class distribution $\Pr({P}\mathord{=}\mathord{{\footnotesize\textsc{yes}}}),\Pr({P}\mathord{=}\mathord{{\footnotesize\textsc{no}}})=(0.87,0.13)$. We can change this distribution quite significantly without changing any decision made by this classifier as long as $\Pr({P}\mathord{=}\mathord{{\footnotesize\textsc{yes}}})\in[0.684,0970]$, which is called an equivalence interval. The second fundamental insight is the notion of equivalent sub-classifiers also introduced in [29]. Continuing with the same classifier, suppose we set the features $U,B$ to values ${\footnotesize\textsc{+ve}},{\footnotesize\textsc{--ve}}$. This leads to a sub-classifier over one features $S$ with a new class distribution $(0.948,0.052)$ since $\Pr({P}\mathord{=}\mathord{{\footnotesize\textsc{yes}}}|{U}\mathord{=}\mathord{{\footnotesize\textsc{+ve}}},{B}\mathord{=}\mathord{{\footnotesize\textsc{--ve}}})=0.948$. Similarly, if these two features are set to ${\footnotesize\textsc{--ve}},{\footnotesize\textsc{+ve}}$, we get another sub-classifier over the same features $U$ but with a different class distribution $(0.924,0.076)$ since $\Pr({P}\mathord{=}\mathord{{\footnotesize\textsc{yes}}}|{U}\mathord{=}\mathord{{\footnotesize\textsc{--ve}}},{B}\mathord{=}\mathord{{\footnotesize\textsc{+ve}}})=0.924$. By utilizing the concept of equivalence intervals, we can conclude that these two sub-classifiers are equivalent, that is, they make the same decisions on sub-instances ${S}\mathord{=}\mathord{{\footnotesize\textsc{+ve}}}$ and ${S}\mathord{=}\mathord{{\footnotesize\textsc{--ve}}}$. Putting these two insights together, we can compile a Bayesian network classifier into a (symbolic) decision graph by conducting a depth-first search on the space of feature instantiations while pruning the search whenever we encounter a sub-classifier that is equivalent to another sub-classifier that we already encountered (compiled); see Fig. 5. This was used to compile Naïve Bayes classifiers in [29], tree-structured classifiers in [9] and graph-structured classifiers in [30]. The techniques for computing equivalence intervals and for identifying equivalent sub-classifiers depend on the classifier’s structure which explains this progression. Fig. 1(b) depicts the compiled decision graph using this method for the Naïve Bayes classifier in Fig. 1(a). Extracting class formulas from decision graphs is discussed next.

Our next discussion on decision graphs applies to decision trees since they are a special case. It is well known that the class formulas of decision graphs can be directly obtained as DNFs. To construct the DNF for a class $c_{i}$, we simply construct a term for each path from the root to a leaf labeled with $c_{i}$ and then disjoin these terms. For example, in the decision graph below, there are two paths from the root to class $c_{1}$ which generate the DNF $\Delta_{1}=x_{12}+x_{3}\cdot y_{1}\cdot z_{13}$.

For decision graphs (that are not trees), this may yield a DNF that is exponentially larger than the graph. We can alleviate this by constructing an NNF circuit whose size is guaranteed to be linear in the decision graph size. The next construction from [4] produces circuits that satisfy even stronger properties as such circuits will allow one, under weak conditions, to compute complete and general reasons in time linear in the circuit size.

Let $c_{1},\ldots,c_{n}$ be the classes of the decision graph (i.e., labels of leaf nodes) and suppose we wish to construct an NNF circuit for the formula of some class $c_{k}$. We first define the function $\texttt{nnf}(N)$ which maps a node $N$ in the decision graph into an NNF fragment as follows. If node $N$ has outgoing edges $\xrightarrow{\ell_{1}}C_{1},\ldots,\xrightarrow{\ell_{m}}C_{m}$, then $\texttt{nnf}(N)=\sum_{i=1}^{m}(\ell_{i}\cdot\texttt{nnf}(C_{i}))$. For leaf nodes, $\texttt{nnf}(c_{i})=\top$ if $c_{i}=c_{k}$ and $\texttt{nnf}(c_{i})=\bot$ if $c_{i}\neq c_{k}$. We can now convert the decision graph into an NNF circuit by calling $\texttt{nnf}(R)$ where $R$ is the graph’s root node. This is the standard method but [4] defined the function $\texttt{nnf}(.)$ differently so the NNF circuits satisfy desirable properties. In particular, for an internal node $N$, it instead used $\texttt{nnf}(N)=\prod_{i=1}^{m}(\ell^{\prime}_{i}+\texttt{nnf}(C_{i}))$ where literal $\ell^{\prime}_{i}$ is the complement of literal $\ell_{i}$. Leaf nodes are kept the same, $\texttt{nnf}(c_{i})=\top$ if $c_{i}=c_{k}$ and $\texttt{nnf}(c_{i})=\bot$ if $c_{i}\neq c_{k}$. The new method is equivalent to using the first method to construct an NNF circuit for the union of classes $c_{1},\ldots,c_{k-1},c_{k+1},\ldots,c_{n}$ and then negating the resulting circuit using deMorgan’s law.

The NNF circuits constructed by this new method are guaranteed to be or-decomposable (Def. 4) if the decision graph satisfies the test-once property (a feature is tested at most once on any path). Recall that complete and general reasons can be computed in linear time if the class formulas are or-decomposable NNFs since the operators $\forall$ (Def. 3) and $\overline{\forall}\,$ (Def. 6) will distribute over disjunctions and conjunctions in such NNFs. One can also obtain NNF circuits that allow linear-time computation of complete and general reasons if the decision graph satisfies the weak test-once property discussed in [4]. Discretized decision graphs satisfy this property (e.g., the decision tree in Fig. 2(b)). The above construction and its variants are the basis for the closed-form complete reasons proposed in [4] and the closed-form general reasons in [2].

For random forests with majority voting, one can easily construct NNF circuits for class formulas by combining the NNF circuits for trees in the forest using a majority circuit. But the resulting circuit is not guaranteed to be or-decomposable even when the circuits for trees are or-decomposable.

The compilation of neural network classifiers into class formulas is more involved due to the multiplicity of techniques and assumptions such as the type of activation functions and whether the network is binary, binarized or quantized. We will therefore restrict the discussion to one approach for binary neural networks while giving pointers to other approaches.

The work we shall sample is [11] which assumed neural networks with binary inputs and step-activation functions. The compilation technique is based on a few observations. First, a neuron with step activation has a binary output so if its inputs are also binary then the neuron represents a Boolean function. Hence, a neural network with binary inputs and step-activation functions must represent a Boolean function (i.e., the signals on its inputs, internal wires and output must all be in $\{0,1\}$). One can therefore convert the neural network into a Boolean circuit (from which class formulas can be easily extracted) if one can compile a neuron into a Boolean circuit (i.e., one with binary inputs and a step-activation function). The next observation is that a neuron with step activation is a linear classifier similar to Naïve Bayes classifiers. Hence, the technique we discussed earlier for compiling Naïve Bayes classifiers into decision graphs, from [29], can be adopted for compiling this class of neurons into decision graphs and then NNF circuits. Once such neurons are successfully compiled, the neural network can be immediately represented as a Boolean circuit from which class formulas can be easily obtained. This work went a bit further by employing a variant on the compilation method in [29] which assumes that the neuron weights $w_{1},\ldots,w_{n}$ and threshold $T$ are integers. This allows one to conduct the compilation in $O(nW)$ time where $W=|T|+\sum_{i=1}^{n}|w_{i}|$ is a sum of absolute values. This pseudo-polynomial time compilation algorithm can be applied to real-valued weights by multiplying the weights by a constant and then truncating (i.e., the weights have fixed precision). This technique permitted the compilation of neural networks with hundreds of inputs (features). The example in Fig. 4 and many other examples in [11] were produced by this approach.

For further techniques that encode input-output behavior symbolically, see [31, 32, 33, 34, 35, 36, 37] for binarized neural networks and [38, 39, 40, 41] for quantized ones. Most of these works target verification tasks though instead of explaining behavior.