On Quantifying Literals in Boolean Logic and its Applications to Explainable AI (Extended Abstract)

1 Introduction

To quantify a variable from a Boolean formula is to eliminate that variable from the formula. This quantification process can be performed either existentially or universally, each leading to a different semantics and a different set of applications. The use of quantification in Boolean logic dates back at least to George Boole's work [1854] where he used universal quantification to perform some forms of logical deduction. Existential quantification has a particularly intuitive interpretation as it can be viewed as a process of removing from a formula all and only the information which pertains to the quantified variable. Due to this semantics, which is referred to as forgetting [Lin and Reiter, 1994], existential quantification has received much attention in AI and database theory, particularly in the management of inconsistent information. This use dates back at least to [Weber, 1986] who employed existential quantification to combine pieces of information that may contradict each other. Variable quantification plays a prominent role in complexity theory too since deciding the validity of quantified Boolean formulas (QBFs)

∗This is an extended abstract of [Darwiche and Marquis, 2021].

is the canonical PSPACE-complete problem; see, for example, [Papadimitriou, 1994]. The validity of QBFs has also been used to characterize the polynomial hierarchy [Stockmeyer, 1977]. In contrast to AI where existential quantification has had a more dominant role than universal quantification, the role of these two forms of quantification has been more symmetrical in other areas of computer science particularly in complexity theory.

The interpretation of existential variable quantification as a process of forgetting information prompted a refinement in which literals (states of variables) are also existentially quantified [Lang et al., 2003], allowing one to remove information that pertains to a literal from a formula. Existential literal quantification is more fine-grained than existential variable quantification as the latter can be formulated in terms of the former. This has led to further applications which are reviewed in [Darwiche and Marquis, 2021].

The dominance of existential quantification within AI is worth noting. We attribute this to the lack of an intuitive enough interpretation of universal quantification, which is a gap that we address in this work. We started our study by an observation that some recent work on explainable AI [Darwiche and Hirth, 2020] can be formulated in terms of universal quantification, particularly universal literal quantification which has not been discussed in the literature before this work. This prompted us to formalize this notion and to elaborately investigate its connections to explainable AI. Our investigation led us to interpret universal quantification as a selection process (in contrast to a forgetting process), which gave rise to many implications. It also led us to some results on the efficient computation of universal literal quantification (e.g., being tractable on CNFs) which has further implications on the efficient computation of explainable AI queries.

In explainable AI, one is typically interested in reasoning about the behavior of classifiers which make decisions on instances. For example, one may wish to understand why a classifier made a particular decision. One may also wish to determine whether a decision is biased (i.e., would be different if we were to only change some protected features of the instance). Such classifiers can be represented using Boolean formulas, even in some cases where they have a numeric form that is learned from data. 1 Amajor insight underlying our results is that many explainable AI queries correspond to a process of selecting instances with particular properties, where the Boolean formula characterizing such instances constitutes the answer to the explainable AI query. Moreover, the universal quantification of literals can be used to select such instances. We use this insight to formulate and generalize some of the recently introduced notions in explainable AI.

1 One can capture the input-output behavior of machine learn-

We limit the scope of this extended abstract to the definition of universal literal quantification, some of its properties and to only one of its applications to explainable AI. We will also discuss the selection semantics of universal literal quantification. For a more comprehensive and in-depth treatment, including proofs of results, we defer the reader to the corresponding journal article [Darwiche and Marquis, 2021].

2 Classifiers as Boolean Formulas

We assume a finite set of Boolean variables Σ where x and ¯x denote the positive and negative literals of Boolean variable X, respectively. A world is a set of literals which contains exactly one literal for each variable in Σ. If Σ = {X, Y, Z}, then {x, ¯ y, z} and {¯x, ¯ y, ¯ z} would be examples of worlds. We will sometimes simply use x¯ yz and ¯x¯ y¯ z to denote such worlds. We use ⊤ and ⊥ to denote the Boolean constants true and false, and φ |= ϕ to mean that Boolean formula φ implies the Boolean formula ϕ. Finally, ϕ|x denotes the formula obtained by replacing every occurrence of variable X in ϕ with ⊤. Similarly, ϕ|¯x is the formula obtained by replacing every occurrence of variable X in ϕ with ⊥.

We will restrict our discussion to classifiers over binary features and two classes (positive and negative). A classifier is then represented by a Boolean formula ∆, where variable assignments that satisfy ∆ correspond to positive instances and those that satisfy ¬∆ correspond to negative instances.

Definition 1. Let ∆ be a Boolean formula over variables X1, . . . ,Xn. We call ∆ a classifier, variable Xi a feature, literal ℓi a characteristic, and δ = {ℓ1, . . . , ℓn} an instance. The decision of classifier ∆ on instance δ is denoted ∆(δ). It is defined as ∆(δ) = 1 if δ |= ∆ (positive decision) and ∆(δ) = 0 if δ |= ¬∆ (negative decision). We further define ∆δ = ∆ when the instance δ is positive and ∆δ = ¬∆ when the instance δ is negative.

Since ∆ captures positive instances and ¬∆ captures negative instances, we work with ∆ when reasoning about positive decisions and with ¬∆ when reasoning about negative decisions. This explains the significance of the notation ∆δ.

Consider the following classifier for admitting students into an academic program [Darwiche and Hirth, 2020]. This classifier makes its decision based on five features: whether an applicant passed the entrance exam (E), is a first time applicant (F), has good grades (G), has work experience (W)

ing classifiers with discrete features using Boolean formulas, either through an encoding or a compilation process. This has been shown for Bayesian network classifiers, random forests and some types of neural networks. For some example works along these lines, see [Chan and Darwiche, 2003; Narodytska et al., 2018; Shih et al., 2019; Ignatiev et al., 2019a; Ignatiev et al., 2019b; Shi et al., 2020; Audemard et al., 2020; Choi et al., 2020].

and comes from a rich hometown (R). The classifier is specified by the following Conjunctive Normal Forms (CNFs):

Consider now an applicant who does not come from a rich hometown but satisfies all other requirements. This applicant will be admitted, ∆(e, f, g,w, ¯ r) = 1. The applicant will not be admitted if they did not pass the entrance exam, ∆(¯ e, f, g, w, ¯ r) = 0. Instance δ1 = {e, f, g,w, ¯ r} is positive and instance δ2 = {¯ e, f, g, w, ¯ r} is negative. Using our notation, ∆δ1 = ∆ since δ1 |= ∆ and ∆δ2 = ¬∆ since δ2 |= ¬∆.

3 Universal Literal Quantification

We next define the universal quantification of literal ℓ from a Boolean formula ϕ and show how it can be used to reason about the decisions of classifiers (explain them in particular).

We first note that ϕ can be expanded as ϕ = (ℓ ∨ (ϕ|¯ ℓ)) ∧ (¯ ℓ ∨ (ϕ|ℓ)), which is equivalent to what is known as Boole's or Shannon's expansion, ϕ = (ℓ ∧ (ϕ|ℓ)) ∨ (¯ ℓ ∧ (ϕ|¯ ℓ)).

Definition 2. Universally quantifying literal ℓ from formula ϕ is defined as follows: ∀ℓ · ϕ = (ℓ ∨ (ϕ|¯ ℓ)) ∧ (ϕ|ℓ).

That is, the operator ∀ℓ drops literal ¯ ℓ from the expansion ϕ = (ℓ ∨ (ϕ|¯ ℓ)) ∧ (¯ ℓ ∨ (ϕ|ℓ)). Universal quantification is classically applied to variables: ∀X · ϕ = (ϕ|x) ∧ (ϕ|¯x). 2 Consider the formula ϕ = (x⇒y) ∧ (y⇒x) which says that variables X and Y are equivalent. We have ∀x · ϕ = x ∧ y and ∀¯x · ϕ = ¯x ∧ ¯ y. Note, however, that ∀X · ϕ = ⊥. Moreover, ∀x · (∀¯x · ϕ) = ∀¯x · (∀x · ϕ) = ⊥. For the formula φ = (x⇒y), we have ∀x · φ = y, ∀¯x · φ = (x⇒y) and ∀X·φ = y. Moreover, we have ∀x·(∀¯x·φ) = ∀¯x·(∀x·φ) = y. [Darwiche and Marquis, 2021] studied various properties of universal literal quantification, including the following ones.

• Universal literal quantification is commutative: For literals ℓ1, ℓ2 and formula ϕ, ∀ℓ1 ·(∀ℓ2 ·ϕ) = ∀ℓ2 ·(∀ℓ1 ·ϕ). Thus, the order of quantifying literals does not matter so we can write ∀{ℓ1, . . . , ℓn} · ϕ or ∀ℓ1, . . . , ℓn · ϕ.
• Universal literal quantification strengthens a formula: For literal ℓ and formula ϕ, we have ∀ℓ · ϕ |= ϕ.
• Universal literal quantification is more fine-grained than universal variable quantification: For variable X and formula ϕ, we have ∀X · ϕ = ∀x, ¯x · ϕ (= ∀{x, ¯x} · ϕ).
• Universal literal quantification preserves logical implication: For literal ℓ, formulas ϕ and φ, we have ϕ |= φ only if ∀ℓ · ϕ |= ∀ℓ · φ.
• Universal literal quantification is the dual of existential literal quantification: For literal ℓ and formula ϕ, we have ∀ℓ · ϕ = ¬(∃ℓ · (¬ϕ)).

4 An Application to Explainable AI

We next consider an application of universal literal quantification to explaining the decisions of classifiers. Consider a decision ∆(δ) made by classifier ∆ on instance δ. One way to explain this decision is to identify a minimal set of characteristics γ ⊆ δ that is sufficient to trigger the decision, γ |= ∆δ. This notion of explanation was introduced in [Shih et al., 2018] under the name of a PI-explanation and later called a sufficient reason for the decision [Darwiche and Hirth, 2020] and an abductive explanation [Ignatiev et al., 2019a].

2 We also note the classical, dual definition ∃X · ϕ = (ϕ|x) ∨ (ϕ|¯x), and ∃ℓ · ϕ = (ϕ|ℓ) ∨ (¯ ℓ ∧ (ϕ|¯ ℓ)) [Lang et al., 2003].

Consider the admission classifier above and an applicant who does not come from a rich hometown but satisfies all other requirements. This applicant will be admitted, ∆(e, f, g, w, ¯ r) = 1, and the decision has two sufficient reasons: {e, f, g} and {e, f, w}. Passing the entrance exam (e), being a first time applicant (f) and having good grades (g) guarantee admission yet no strict subset of these characteristics will. Having work experience instead of good grades will also guarantee admission but again no strict subset of characteristics {e, f,w} guarantees this. If this applicant were to come from a rich hometown, then there would be more sufficient reasons for the admission decision, ∆(e, f, g, w, r) = 1: {e, f, g}, {e, f, w}, {e, g, r}, {e, r, w} and {g, r, w}.

A decision may have an exponential number of sufficient reasons. Moreover, some explainable AI queries, such as ones relating to decision bias, are based on checking whether the sufficient reasons for a decision satisfy some properties. These sufficient reasons can sometimes be represented compactly using the notion of a complete reason introduced in [Darwiche and Hirth, 2020], which showed a number of results relating to this notion. For example, the sufficient reasons for a decision correspond to the prime implicants of its complete reason. Moreover, some properties of sufficient reasons can be checked in time linear in the size of a complete reason when it is represented in an appropriate form. However, the process for computing complete reasons in [Darwiche and Hirth, 2020] was procedural and restricted to a specific type of classifiers. Universal literal quantification can be used to provide a semantical definition of complete reasons which decouples them from the type of underlying classifier.

Theorem 1. For classifier ∆ and instance δ = {ℓ1, . . . , ℓn}, ∀δ·∆δ is equivalent to the complete reason for decision ∆(δ).

As shown in [Darwiche and Marquis, 2021], a number of logical forms allow a linear-time computation of universal literal quantification, including Conjunctive Normal Form (CNF). In particular, if ∆ is a CNF, then ∀ℓ·∆ can be obtained by dropping every occurrence of literal ¯ ℓ from the CNF.

Consider the admission classifier above and an applicant who passed the entrance exam, has good grades and work experience, comes from a rich hometown but is not a first time applicant. The classifier will admit this applicant, ∆(e, ¯ f , g, r, w) = 1. The complete reason for this decision is ∀e, ¯ f , g, r, w ·∆ = (e∨g)∧(e∨w)∧(r)∧( ¯ f ∨g ∨w), which has four prime implicants representing the sufficient reasons for the decision: {e, g, r}, {e, r, w}, {e, ¯ f , r}, {g, r, w}.

[Darwiche and Marquis, 2021] discussed further applications of universal literal quantification, which include determining decision bias and identifying characteristics that are irrelevant to a decision. It also showed how this notion can be used to reason about populations, which are groups of instances that are decided similarly.

5 Selection Semantics

As mentioned earlier, the popularity of existential quantification in AI is due to its forgetting semantics. In particular, to existentially quantify a variable X from a formula ϕ is to remove any information, and only information, that the formula ϕ contains about variable X. Similarly, to existentially quantify a literal from a formula is to remove any, and only, information that the formula contains about the literal. We will next provide a selection semantics for universal literal quantification; see [Darwiche and Marquis, 2021] for the corresponding semantics of universal variable quantification.

Our semantics is based on the notion of α-independent models for a formula ϕ, where α is a set of literals. These are models of formula ϕ that do not depend on literals α; that is, they continue to be models of ϕ if we flip any of the literals they may have in α (a model of ϕ is a world that satisfies it).

Definition 3. Let α be a set of literals for distinct variables. A world ω is said to be an α-independent model of formula ϕ iff α ⊆ ω and ω \ α |= ϕ.

Consider a world ω and literals α such that α ⊆ ω. If world ω is an α-independent model of formula ϕ, we can flip any literals of α in world ω while maintaining the world as a model of ϕ. Consider formula ϕ = (x ∨ y) ∧ z and its model ω = {x, y, z}. This model is not an {x, y}-independent model of ϕ since {¯x, ¯ y, z} is not a model of ϕ. On the other hand, world {x, y, ¯ z} is an {x, y}-independent model of ¬ϕ as we can flip literals x and y in any manner while maintaining the world as a model for ¬ϕ.

We are now ready to present our selection semantics for universally quantifying a set of (possibly conflicting) literals ℓ1, . . . , ℓn from a formula ϕ. According to this semantics, universally quantifying these literals is a process of selecting models of ϕ that do not depend on literals ¯ ℓ1, . . . , ¯ ℓn.

Theorem 2. Let ϕ be a formula, ℓ1, . . . , ℓn be literals, ω be a world and α = ω ∩ {¯ ℓ1, . . . , ¯ ℓn}. Then ω |= ∀ℓ1, . . . , ℓn · ϕ iff ω is an α-independent model of ϕ.

Consider ϕ = (x ∨ y ∨ z) ∧ (¯x ∨ y ∨ t), literals x, y, z and world ω = ¯x¯ yzt, leading to α = ω ∩ {¯x, ¯ y, ¯ z} = ¯x¯ y. Then ω is an α-independent model of ϕ since zt |= ϕ. Hence, ω |= ∀x, y, z · ϕ which can be verified since ∀x, y, z · ϕ = (x ∨ y ∨ z) ∧ (y ∨ t). For literals x, ¯ y, ¯ z, we get α = ω ∩ {¯x, y, z} = ¯xz so ω is not an α-independent model of ϕ since ¯ yt ̸|= ϕ (indeed, ¯x¯ y¯ zt |= ¬ϕ). Hence, ω ̸|= ∀x, ¯ y, ¯ z · ϕ which can be verified since ∀x, ¯ y, ¯ z · ϕ = x ∧ t.

According to Theorem 2, when universally quantifying literals ℓ1, . . . , ℓn from formula ϕ, we are selecting all (and only) models of ϕ that do not depend on literals ¯ ℓ1, . . . , ¯ ℓn. That is, the models of ∀ℓ1, . . . , ℓn · ϕ are precisely the models of ϕ which continue to be models of ϕ if we were to flip any literals they may have in ¯ ℓ1, . . . , ¯ ℓn. We next discuss this selection semantics in the context of classification.

Consider a classifier whose positive instances are specified by formula ∆ and suppose we universally quantify a set of characteristics ℓ1, . . . , ℓn from ∆ to yield ∀ℓ1, . . . , ℓn · ∆. In this case, ∀ℓ1, . . . , ℓn · ∆ characterizes all positive instances δ whose positiveness does not depend on characteristics ¯ ℓ1, . . . , ¯ ℓn. That is, flipping any characteristics in

δ ∩ {¯ ℓ1, . . . , ¯ ℓn} will yield a positive instance. A symmetric situation arises when universally quantifying characteristics ℓ1, . . . , ℓn from ¬∆: We select negative instances whose negativeness does not depend on characteristics ¯ ℓ1, . . . , ¯ ℓn.

For a concrete example, consider the following classifier which decides whether an applicant should be granted a loan based on four features: whether they defaulted on a previous loan (D), have a guarantor (G), own a home (H) or have a high income (I). This classifier is specified by the following formula ∆ and its negation ¬∆, both in CNF:

This classifier will grant a loan to an applicant who never defaulted on a loan, owns a home, has a high income but does not have a guarantor, ∆( ¯ d, ¯ g, h, i) = 1. This positive instance is not a model of ∀d·∆ = i∧g. Thus, characteristic ¯ d is essential for the positiveness of this instance (instance {d, ¯ g, h, i} is negative). However, the positive instance { ¯ d, g, ¯h, i} is a model of ∀d · ∆ so characteristic ¯ d is not essential for its positiveness (instance {d, g, ¯h, i} is also positive).

If the characteristics ℓ1, . . . , ℓn correspond to a positive instance δ, then δ = {ℓ1, . . . , ℓn} |= ∆. In this case, ∀ℓ1, . . . , ℓn · ∆ characterizes all positive instances δ′ whose positiveness is due only to the characteristics they have in common with δ; that is, independently of their characteristics δ′ ∩{¯ ℓ1, . . . , ¯ ℓn}. Hence, ∀ℓ1, . . . , ℓn ·∆will characterize all subsets of instance δ which are sufficient to trigger a positive decision (these subsets correspond to the sufficient reasons for the decision). This explains why universal literal quantification can be used to compute the complete reason behind a decision as shown earlier. Due to this selection semantics of universal literal quantification, [Darwiche and Marquis, 2021] showed that it can be used to answer further queries of interest to explainable AI. This includes queries relating to decision bias and to the irrelevance of certain characteristics and features to decisions.

Acknowledgments

This work has benefited from the support of the International Research Project MAKC ("Modern Approaches to Knowledge Compilation") shared between the Automated Reasoning Group of the University of California at Los Angeles (UCLA) and the Centre de Recherche en Informatique de Lens (CRIL UMR 8188 CNRS - Artois University). The work has been partially supported by NSF grant IIS-1910317, DARPA grant N66001-17-2-4032, AI Chair EXPEKCTATION (ANR-19-CHIA-0005-01) of the French National Research Agency (ANR) and by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA No 952215.