ExplAIner: A Declarative Query Language for Explaining Classification Models MARCELO ARENAS, Pontificia Universidad Católica de Chile, Chile PABLO BARCELÓ, Pontificia Universidad Católica de Chile, Chile DIEGO BUSTAMANTE, Pontificia Universidad Católica de Chile, Chile JOSE CARABALL, Pontificia Universidad Católica de Chile, Chile MARÍA ALEJANDRA SCHILD, Pontificia Universidad Católica de Chile, Chile BERNARDO SUBERCASEAUX, Carnegie Mellon University, USA The XAI community has studied a wide range of queries and scores for explaining predictions of ML models. From a data management perspective, this proliferation of explanation notions calls for declarative query languages in which such notions can be specified, combined, and analyzed uniformly. In this paper, we develop such a framework for Boolean models. We first revisit FOIL, an interpretability query language for black-box models, and show that it has two fundamental limitations: it cannot express central optimality-based explanation queries, and its evaluation problem over decision trees is hard for every level of the polynomial hierarchy.
arXiv:2607.06407v1 [cs.AI] 7 Jul 2026
We then introduce ExplAIner, a query language based on FOIL with an extended vocabulary and a layered structure. We show that ExplAIner can express a broad family of explanation notions, including abductive, contrastive, feature-based, and distance-based queries. We also prove that the evaluation problem for each query in ExplAIner belongs to the Boolean hierarchy over every class of Boolean models for which some basic predicates can be evaluated in polynomial time. In particular, that property holds for deterministic and decomposable Boolean circuits. Finally, we introduce Opt-FOIL, an optimization-oriented fragment of ExplAIner for computing explanations that are minimal with respect to strict partial orders, and prove that its evaluation problem is in FPNP under the same tractability assumptions. These complexity results have a direct algorithmic consequence: a fixed ExplAIner query can be evaluated with a fixed number of calls to a SAT solver, while a notion of explanation specified in Opt-FOIL can be computed with a polynomial number of such calls. This is particularly relevant in formal XAI, where SAT solvers have been successfully used to compute explanations for several classes of ML models.
1
Introduction Explainability as a query-language problem. The increasing use of machine learning (ML) models in decision-making
systems has created a pressing need for principled methods to understand the predictions produced by such models. This need has led to a large body of work in explainable AI (XAI) [8, 21, 22, 37], and in particular to a variety of queries, scores, and explanation notions aimed at identifying why a model classifies a given input in a particular way [15, 33, 34]. Examples include abductive explanations, contrastive explanations, counterfactual-style queries, and feature-necessity or feature-relevance notions [16, 23, 25, 40]. From a data management perspective, this proliferation of explanation notions suggests a natural question: rather than designing a separate algorithm or formalism for each explanation task, can we develop a declarative language in which users specify what explanation they are looking for? This is in line with a long tradition in databases: complex computational tasks are exposed through query languages with well-defined syntax and semantics, while the study of their expressive power and evaluation complexity provides a principled understanding of what can be asked and Authors’ Contact Information: Marcelo Arenas, Pontificia Universidad Católica de Chile, Santiago, Chile; Pablo Barceló, Pontificia Universidad Católica de Chile, Santiago, Chile; Diego Bustamante, Pontificia Universidad Católica de Chile, Santiago, Chile; Jose Caraball, Pontificia Universidad Católica de Chile, Santiago, Chile; María Alejandra Schild, Pontificia Universidad Católica de Chile, Santiago, Chile; Bernardo Subercaseaux, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA.
1
2
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
how hard it is to answer [1, 30, 38, 42]. In this view, a model becomes an object over which one poses queries, and explanation notions become fixed queries evaluated over that object [3, 4]. This perspective has several advantages. First, it provides a uniform framework for comparing and combining explanation notions. This is important because there is no single explanation concept that is best suited for all users, models, or applications; in many cases, the most informative explanation is obtained by combining several criteria [18, 35]. Second, it makes it possible to study explainability through standard database-theoretic lenses, such as expressiveness and evaluation complexity [1, 31, 42]. Third, it opens the door to the development of general optimization techniques for the operators of a query language for explainability. Such techniques can reduce the evaluation time of several explainability queries simultaneously, rather than treating each query in isolation. A central issue in such a framework is how to measure the complexity of query evaluation. Since an explanation notion is intended to be specified by a fixed formula of the language, the appropriate measure is data complexity: the query is fixed, while the input consists of the model representation and the instance to be explained [42]. From this perspective, polynomial-time data complexity is desirable, but it is not the only meaningful tractability target. Many explanation tasks are inherently computationally demanding [11, 43], and therefore a useful explainability language should also allow controlled forms of non-polynomial complexity. In particular, data complexity in PNP remains a reasonable and useful target: it corresponds to computation with a polynomial number of calls to an NP oracle, and it is compatible with the use of SAT solvers as evaluation engines. This complexity level is especially appropriate in our setting because the inputs are model representations, not database instances in the traditional sense. In contrast with large relational databases, the tree-based models commonly considered in formal explainability are often of moderate size, and SAT-based methods have been successfully used to compute explanations for such models [26, 29, 45]. Thus, in this paper we regard polynomial time and PNP as desirable data-complexity bounds for an explainability query language. Toward declarative languages for model interpretability. A first step in this direction was taken by Arenas et al. [4], who introduced FOIL, a first-order interpretability logic for querying ML models. FOIL is model-agnostic: it treats a model as a black box and provides access to its positive instances together with the natural subsumption relation over partial instances. This simple design makes FOIL an appealing foundational language, and it is expressive enough to capture several basic explanation notions. However, model-agnosticism also has limitations. If the language is too weak, it cannot express explanation concepts that are central in practice. If it is too unconstrained, its evaluation problem may become too complex to support query evaluation in the sense expected from a database-oriented framework. Thus, the challenge is to design a language that balances two requirements. On the one hand, it should be expressive enough to capture a broad family of explanation queries, including optimality-based notions such as minimum or maximum explanations. On the other hand, it should have well-behaved evaluation and computation problems over relevant classes of Boolean models. In this paper, we address this challenge by developing a declarative framework for explaining Boolean models. Our setting is not tied to decision trees. Instead, we consider models abstractly as Boolean functions, while also studying concrete representation classes such as deterministic and decomposable Boolean circuits and decision trees. This allows us to separate the logical specification of explanation queries from the representation-dependent complexity of evaluating them. Such a separation is particularly natural from a database perspective, where query specification and query evaluation over different representation classes are treated as distinct but connected problems. The limitations of FOIL. We begin by revisiting FOIL from the perspective of query-language design. We show that, despite its foundational role, FOIL does not satisfy the requirements above. First, FOIL lacks the expressive power
ExplAIner: A Declarative Query Language for Explaining Classification Models
3
needed to capture some natural optimality-based explanation notions. In particular, we prove that minimum abductive explanations cannot be expressed in FOIL, even when the underlying model is restricted to be a decision tree. This shows that the limitation is not caused by the use of complex model classes, but by the expressive resources of the language itself. Second, FOIL has high evaluation complexity. We prove that, for every level of the polynomial hierarchy, there is a fixed FOIL formula whose evaluation problem over decision trees is hard for that level. Thus, even on a class of models traditionally regarded as interpretable, unrestricted FOIL does not provide the kind of controlled data complexity that one would expect from a practical declarative language for explanations. This complements earlier complexity-theoretic approaches to model interpretability, which study the difficulty of answering explanation queries over different model classes [11, 43]. ExplAIner: a tractable logic for explanation queries. Motivated by these limitations, we introduce ExplAIner, a first-order logic designed to express explanation queries over Boolean models while retaining controlled evaluation complexity. The language extends the basic FOIL vocabulary with a relation that compares partial instances according to the number of defined features. This addition is essential for expressing optimality conditions based on cardinality, such as minimum abductive explanations [11, 16] and maximum contrastive explanations [23, 25]. ExplAIner is organized in layers. Its atomic layer captures structural properties of partial instances; its quantified layer allows formulas to refer to the behavior of the model by combining formulas from the atomic layer with the predicates AllPos and AllNeg, which express whether all completions of a partial instance are classified positively or negatively; and its topmost layer permits Boolean combinations of explanation properties. This organization is designed to provide enough expressive power for explanation tasks while keeping evaluation under control. We show that ExplAIner can express the explanation notions studied in this paper, including weak abductive explanations, abductive explanations, and minimum abductive explanations [9, 11, 16, 25]; weak contrastive explanations, contrastive explanations, and maximum contrastive explanations [11, 15, 25]; minimum change required and maximum change allowed [11]; and necessary features and relevant features [23, 28]. At the same time, we prove that the evaluation problem for ExplAIner belongs to the Boolean hierarchy over every class of models for which the basic AllPos and AllNeg checks are tractable. This includes decision trees and also richer representation classes with suitable tractability properties, such as deterministic and decomposable Boolean circuits [5, 17]. Opt-FOIL: computing explanations. Evaluation is only one part of the problem. A language for explainability should also support the computation of explanations. For this reason, we introduce Opt-FOIL, an optimization-oriented fragment built from the quantified layer of ExplAIner together with a minimization operator over definable strict partial orders. Opt-FOIL captures explanation tasks in which one seeks an object satisfying a logical specification and minimal with respect to a user-defined preference order. This includes standard subset-minimal explanations, cardinality-minimum explanations, and distance-based notions such as minimum change required. By changing the order, the same formalism can also express maximality-based notions, such as maximum contrastive explanations and maximum change allowed. Our main computational result for Opt-FOIL is that its computation problem belongs to FPNP over every class of models for which AllPos and AllNeg can be evaluated in polynomial time, where FP is the class of functions that can be computed in polynomial time. In the terminology above, this means that computing explanations specified in Opt-FOIL has controlled data complexity: the formula is fixed, and the cost is measured as a function of the model representation and the input instance. This places Opt-FOIL within the complexity regime identified above as suitable for declarative
4
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
explainability languages, while allowing the language to capture optimization-based explanation tasks that are unlikely to admit polynomial-time algorithms in full generality.
Technical contributions. The following are the technical contributions of the paper. • We prove two limitations of FOIL over decision trees. On the expressiveness side, we show that no FOIL formula can define the minimum abductive explanation query. On the complexity side, we prove that for every level Σ𝑘𝑃 of the polynomial hierarchy, there is a fixed FOIL formula whose evaluation problem is Σ𝑘𝑃 -hard. • We introduce ExplAIner, a logic based on FOIL with an extended vocabulary and a layered structure: the atomic layer, the quantified layer, and the full ExplAIner layer. The vocabulary of ExplAIner consists of the predicates ⊆, ⪯, AllPos, and AllNeg, where ⊆ is the subsumption relation on partial instances and ⪯ compares partial instances by their number of defined features. We show that both ⊆ and ⪯ are necessary by proving that neither relation is first-order definable from the other over decision trees. • We show that ExplAIner is expressive enough to encode the explanation queries considered in the paper, including weak abductive explanations, subset-minimal abductive explanations, cardinality-minimum abductive explanations, weak and maximal contrastive explanations, minimum change required, maximum change allowed, necessary features, and relevant features. Each of these notions is expressed by a fixed query in ExplAIner. • We establish complexity bounds for the three layers of ExplAIner. First, we show that the evaluation problem for queries in the atomic layer can be solved in polynomial time over every class of Boolean models. Second, for every class of Boolean models over which the predicates AllPos and AllNeg can be decided in polynomial time, we show that the evaluation problem for queries in the quantified layer is in NP. Moreover, we show that there exists a query in the quantified layer whose evaluation problem is NP-complete over the class of decision trees. Third, for every class of Boolean models over which AllPos and AllNeg can be decided in polynomial time, we show that the evaluation problem for ExplAIner queries is in the Boolean hierarchy; equivalently, such queries can be evaluated with a fixed number of calls to an NP oracle. Furthermore, we show that for every level BH𝑘 of the Boolean hierarchy, there exists an ExplAIner query whose evaluation problem is BH𝑘 -hard over the class of decision trees. Importantly, the assumption that the predicates AllPos and AllNeg can be decided in polynomial time is not specific to decision trees. This condition also holds for more general classes of Boolean models, including deterministic and decomposable Boolean circuits. Thus, the upper bounds above apply beyond tree-based representations and cover circuit classes that are central in knowledge compilation [17]. • We define Opt-FOIL as an optimization-oriented fragment of ExplAIner, based on the quantified layer together with a minimization operator over strict partial orders. For every class of Boolean models over which the predicates AllPos and AllNeg can be decided in polynomial time, we show that the computation problem for Opt-FOIL queries is in FPNP . Hence, explanations specified in Opt-FOIL can be computed with a polynomial number of calls to an NP oracle. • As a result of independent interest, we use Presburger arithmetic to show that the problem of verifying whether a sentence over the atomic layer of ExplAIner is valid is decidable. This result is needed to provide an effective syntax for Opt-FOIL, since Opt-FOIL requires verifying that a sentence in the atomic layer defines a strict partial order.
ExplAIner: A Declarative Query Language for Explaining Classification Models
5
• Finally, we show that, under standard complexity-theoretic assumptions, Opt-FOIL is strictly contained in ExplAIner, and ExplAIner is strictly contained in FOIL over the extended vocabulary consisting of the predicates ⊆, ⪯, AllPos, and AllNeg. Organization of the paper. The remainder of the paper is organized as follows. Section 2 introduces the basic notions used throughout the paper, including Boolean models, partial instances, model representations, and the explanation queries studied in our framework. Section 3 revisits FOIL and establishes its limitations in terms of expressiveness and evaluation complexity. Section 4 introduces ExplAIner and proves its main expressiveness and evaluation results. Section 5 presents Opt-FOIL, our optimization-oriented language for computing explanations, together with its computational guarantees. Section 6 presents concluding remarks and directions for future work. Finally, the appendix contains supplementary material, including technical proofs that are deferred for readability. 2
Background
We begin by introducing the main components of our framework, followed by a review of various explainability queries that will be addressed in the subsequent sections. 2.1
Models and instances
We use an abstract notion of a model of dimension 𝑛, and define it as a Boolean function M : {0, 1}𝑛 → {0, 1}.1 We write d𝑖𝑚(M) for the dimension of a model M. A partial instance of dimension 𝑛 is a tuple e ∈ {0, 1, ⊥}𝑛 , where ⊥ is used to represent undefined features. We define e⊥ = {𝑖 ∈ {1, . . . , 𝑛} | e[𝑖] = ⊥}. An instance of dimension 𝑛 is a tuple e ∈ {0, 1}𝑛 , that is, a partial instance without undefined features. For every instance e of dimension d𝑖𝑚(M), we write M (e) for the value assigned by M to e. Given two partial instances e, e′ of dimension 𝑛, we write e ⊆ e′ and say that e is subsumed by e′ if and only if, for every 𝑖 ∈ {1, . . . , 𝑛}, whenever e[𝑖] ≠ ⊥, we have e[𝑖] = e′ [𝑖]. In other words, e′ can be obtained from e by replacing some occurrences of ⊥ by Boolean values. For example, (1, ⊥) is subsumed by (1, 0), but it is not subsumed by (0, 0). A partial instance e can be seen as a compact representation of the set of instances e′ such that e is subsumed by e′ . Such instances e′ are called the completions of e and the set of all of them is denoted by comp(e). For each 𝑛, partial instances of dimension 𝑛 are partitioned into 𝑛 + 1 levels: for each 𝑖 ∈ {0, . . . , 𝑛}, level 𝑖 consists of all partial instances with exactly 𝑖 defined features. Given partial instances e, e′ , we write e ⪯ e′ and say that e is on a ′ |. In other words, e′ has at least as many defined features as e. less or equal level than e′ if and only if |e⊥ | ≥ |e⊥
We will also use the symbols ⊂ and ≺ for the corresponding strict relations. In several proofs, we write e · e′ for the concatenation of both instances. Moreover, for a value 𝑠 ∈ {0, 1, ⊥}, we denote by {𝑠}𝑛 the partial instance of dimension 𝑛 whose entries are all equal to 𝑠. We next introduce several classes of Boolean functions that will be used throughout the paper. Boolean Circuits. A Boolean circuit of dimension 𝑛 is a directed acyclic graph over a set of variables {𝑥 1, ..., 𝑥𝑛 } such that: (i) Every node without incoming edges is either a variable gate or a constant gate. A variable gate is labeled with a variable, and a constant gate is labeled with either 0 or 1; 1We focus on Boolean models, as is common in formal XAI research [10, 13, 43].
6
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux (ii) Every node with incoming edges is a logic gate, and is labeled with a symbol ∧, ∨ or ¬. If it is labeled with the symbol ¬, then it has exactly one incoming edge; (iii) Exactly one node does not have any outgoing edges, and this node is called the output gate. Given a Boolean circuit 𝐶 and an instance e of dimension 𝑛, the value 𝐶 (e) is defined as the value of the output gate
of 𝐶 when we evaluate 𝐶 on input e. Note that we are identifying inputs of the circuit as instances of the Boolean model. Several restrictions of Boolean circuits with good computational properties have been studied. Negation Normal Form. A negation normal form (NNF) circuit of dimension 𝑛 is a Boolean circuit of dimension 𝑛 such that the incoming edge of every negation gate comes from a variable gate. Determinism and decomposability. Let 𝑋 be a set of variables, let 𝐶 be a circuit over 𝑋 , and let 𝑔 be a gate of 𝐶. We define 𝐶𝑔 to be the Boolean circuit over 𝑋 induced by the set of gates 𝑔′ of 𝐶 for which there exists a directed path from 𝑔′ to 𝑔 in 𝐶. Note that 𝑔 is the output gate of 𝐶𝑔 . An ∨-gate 𝑔 of 𝐶 is said to be deterministic if, for every pair 𝑔1 , 𝑔2 of distinct input gates of 𝑔, there is no instance e such that 𝐶𝑔1 (e) = 𝐶𝑔2 (e) = 1. The circuit 𝐶 is called deterministic if every ∨-gate of 𝐶 is deterministic. For every gate 𝑔 of 𝐶, define var(𝑔) as the set of variables 𝑥 ∈ 𝑋 such that there exists a variable gate labeled by 𝑥 in 𝐶𝑔 . An ∧-gate 𝑔 of 𝐶 is said to be decomposable if for every pair 𝑔1 , 𝑔2 of distinct input gates of 𝑔, we have var(𝑔1 ) ∩ var(𝑔2 ) = ∅. The circuit 𝐶 is called decomposable if every ∧-gate of 𝐶 is decomposable.
∧ ∨
𝑥1
∧ ¬ 𝑥2
𝑥3
𝑥4
Fig. 1. A d-DNNF circuit of dimension 4.
Deterministic Decomposable Negation Normal Form. A deterministic decomposable negation normal form (d-DNNF) circuit of dimension 𝑛 is an NNF circuit of dimension 𝑛 that is both deterministic and decomposable. An example is shown in Figure 1. Binary Decision Diagram. A binary decision diagram (BDD) of dimension 𝑛 is a directed acyclic graph with a unique root, and whose nodes and edges are labeled as follows: (i) every leaf is labeled by true or false and (ii) every non-leaf node is labeled by a feature in {1, ..., 𝑛} and has exactly two outgoing edges, one labeled by 0 and the other by 1. Let 𝐵 be a binary decision diagram and let e be an instance of dimension 𝑛. The value 𝐵(e) is defined as the Boolean value of the leaf obtained by starting at the root and following the path such that, at each non-leaf node labeled by 𝑖, the outgoing edge labeled by e[𝑖] is chosen.
ExplAIner: A Declarative Query Language for Explaining Classification Models
7
Decision Trees. A decision tree (DTree) over instances of dimension 𝑛 is a binary decision diagram of dimension 𝑛 such that (i) its underlying graph is a tree and (ii) no feature appears more than once on any root-to-leaf path. An example is shown in Figure 2.
𝑥2 0
1 𝑥3
𝑥1 0
1
false
true
0
1
𝑥4
𝑥4
0
1
0
1
true
false
true
false
Fig. 2. A decision tree of dimension 4. For the sake of readability, we label nodes by 𝑥𝑖 rather than by indices.
2.2
Explainability queries
We now define the explainability queries studied in this work. Weak Abductive Explanation. Given an instance e and a model M, a partial instance e1 is a weak abductive explanation (wAXp) for e on M if e1 ⊆ e and, for every e2 ∈ comp(e1 ), the condition M (e) = M (e2 ) holds [23]. This notion is also known as sufficient reason in the literature [6]. For example, in Figure 1, (1, 1, 1, ⊥) is a weak abductive explanation for the instance (1, 1, 1, 1). Abductive Explanation. Given a pair (e, M), a partial instance e1 is an abductive explanation (AXp) for e on M if it is a weak abductive explanation for e on M and there is no weak abductive explanation e2 such that e2 ⊂ e1 [25]. This notion of explanation has been extensively studied and it can be found in the literature under names such as sufficient reason [16, 32], prime implicant [41], and minimal sufficient reason [6]. Modeling abduction using propositional logic or first-order logic, and the complexity of computing such an explanation has been studied for many decades [36]. In Figure 1, (1, 1, 1, ⊥) is a weak abductive explanation for (1, 1, 1, 1), but not an abductive explanation. By contrast, one can check that (1, 1, ⊥, ⊥) is indeed an abductive explanation. Minimum Abductive Explanation. Given a pair (e, M), a partial instance e1 is a minimum abductive explanation (mAXp) for e on M if it is a weak abductive explanation for e on M and there is no weak abductive explanation e2 such that e2 ≺ e1 . Our definition is based on the minimum sufficient reason explainability query by [11] and [6]. In Figure 1, (1, 1, ⊥, ⊥) is also a minimum abductive explanation for (1, 1, 1, 1). Weak Contrastive Explanation. Given a pair (e, M), the partial instance e1 is a weak contrastive explanation (wCXp) for e on M if e1 ⊆ e and there is an instance e2 ∈ comp(e1 ) such that the condition M (e) ≠ M (e2 ) holds [34].
8
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux Contrastive Explanation. Given a pair (e, M), the partial instance e1 is a contrastive explanation (CXp) for e on M if
it is a weak contrastive explanation for e on M such that there is no weak contrastive explanation e2 satisfying e1 ⊂ e2 . It can be shown that this definition is equivalent to the one by [34]. Maximum Contrastive Explanation. Given a pair (e, M), the partial instance e1 is a maximum contrastive explanation (mCXp) for e on M if it is a weak contrastive explanation for e on M such that there is no weak contrastive explanation e2 satisfying e1 ≺ e2 . In Figure 1, the partial instance (⊥, 1, 1, 1) is a maximum contrastive explanation for (1, 1, 1, 1), thus also a CXp and a wCXp. Minimum Change Required. Given a pair (e, M), an instance e1 is a solution to the minimum change required query (MCR) for e on M if M (e) ≠ M (e1 ) and M (e) = M (e2 ), for every instance e2 at smaller Hamming distance (meaning the number of flipped features between two instances) from e than e1 . The instance e1 represents the minimum distance required to change the value on the model. This notion is based on the query introduced by [11]. Considering the instance (1, 1, 1, 1) in Figure 1, one possible explanation for the query is (0, 1, 1, 1). Maximum Change Allowed. Given a pair (e, M), an instance e1 is a solution to the maximum change allowed query (MCA) for e on M if M (e) = M (e1 ) and M (e) ≠ M (e2 ), for every instance e2 at greater Hamming distance from e than e1 . This notion is based on the query introduced by [2]. As the authors argue, only studying counterfactual queries like minimum change required may not capture the whole picture for explaining certain situations. That is why we include their semifactual version of the problem. In Figure 1, the maximum change allowed for the negative input (0, 1, 1, 1) is the instance (0, 0, 0, 0). The original versions of MCR and MCA [2, 11] are defined similarly with respect to each other, but have very different interpretations. Given a distance 𝑘 for MCR it is not trivially easier to decide any distance 𝑘 ′ for MCA; and vice versa. We only know that the inequality 𝑘 ≤ 𝑘 ′ + 1 holds. Thus, presenting both queries has additional value and lets us present another useful case of maximization. Necessary Feature. Given a pair (e, M), a partial instance e1 with exactly one defined feature is a necessary feature (NF) for e on M if, for every weak abductive explanation e2 for e on M, e1 ⊆ e2 holds. An equivalent formulation appears in [23], where the authors define the property feature necessity on their own framework using abductive explanations instead of weak abductive explanations. It is easy to see that both definitions are equivalent. Considering (1, 1, 1, 1) in Figure 1, the instance has two abductive explanations: (1, 1, ⊥, ⊥) and (1, ⊥, 1, 1). Therefore, the feature 𝑥 1 = 1, represented by the partial instance (1, ⊥, ⊥, ⊥), is a necessary feature. Relevant Feature. Given a pair (e, M), a partial instance e1 with exactly one defined feature is a relevant feature (RF) for e on M if there exists an abductive explanation e2 for e on M such that e1 ⊆ e2 . This notion appears in the literature as the AXp membership problem [24] and as feature relevancy [23]. Considering (1, 1, 1, 1) and its abductive explanations (1, 1, ⊥, ⊥) and (1, ⊥, 1, 1) in Figure 1, 𝑥 2 = 1 is one of the relevant features, and can be represented by the partial instance (⊥, 1, ⊥, ⊥). 3
First Order Interpretability Logic
In this section, we introduce an initial interpretability logic designed for expressing queries. We demonstrate that it faces limitations in expressive power and exhibits high computational complexity for its evaluation problem.
ExplAIner: A Declarative Query Language for Explaining Classification Models
9
Our work is inspired by the first-order interpretability logic (FOIL) [4], which is a simple explainability language rooted in first-order logic. FOIL is simply first-order logic over two relations on the set of partial instances of a given dimension: a unary relation Pos whose interpretation is the set of instances that are positively classified by the model, and a binary relation ⊆ that represents the subsumption relation among partial instances. Given a vocabulary 𝜎 consisting of relations 𝑅1 , . . ., 𝑅ℓ , recall that a structure 𝔄 over 𝜎 consists of a domain over which quantifiers range, and an interpretation for each relation 𝑅𝑖 . Moreover, given a first-order formula 𝜑 defined over the vocabulary 𝜎, we write 𝜑 (𝑥 1, . . . , 𝑥𝑘 ) to indicate that the free variables of 𝜑 are among {𝑥 1, . . . , 𝑥𝑘 }. Finally, given a structure 𝔄 over the vocabulary 𝜎 and elements 𝑎 1 , . . ., 𝑎𝑘 in the domain of 𝔄, we use 𝔄 |= 𝜑 (𝑎 1, . . . , 𝑎𝑘 ) to indicate that the formula 𝜑 is satisfied by 𝔄 when each variable 𝑥𝑖 is replaced by element 𝑎𝑖 (1 ≤ 𝑖 ≤ 𝑘). Consider a model M with d𝑖𝑚(M) = 𝑛. The structure 𝔄 M representing M over the vocabulary formed by Pos and ⊆ is defined as follows. The domain of 𝔄 M is the set {0, 1, ⊥}𝑛 of all partial instances of dimension 𝑛. A partial instance e ∈ {0, 1, ⊥}𝑛 belongs to the interpretation of Pos in 𝔄 M if and only if e ∈ {0, 1}𝑛 and M (e) = 1. Moreover, a pair (e1, e2 ) is in the interpretation of relation ⊆ in 𝔄 M if and only if e1 is subsumed by e2 . Finally, given a formula 𝜑 (𝑥 1, . . . , 𝑥𝑘 ) in FOIL and partial instances e1 , . . ., e𝑘 of dimension 𝑛, the model M is said to satisfy 𝜑 (e1, . . . , e𝑘 ), denoted by M |= 𝜑 (e1, . . . , e𝑘 ), if 𝔄 M |= 𝜑 (e1, . . . , e𝑘 ). Notice that for a succinctly-represented model M, the structure 𝔄 M can be exponentially larger than the representation of M. Hence, 𝔄 M is a theoretical construction needed to formally define the semantics of FOIL, but it should not be constructed explicitly when checking in practice if a formula 𝜑 is satisfied by M.
3.1
Expressing interpretability queries in FOIL
It will be instructive for the rest of our presentation to see a few examples of how FOIL can be used to express some natural explainability queries on models. In these examples, we make use of the following FOIL formula: Full(𝑥) := ∀𝑦 (𝑥 ⊆ 𝑦 → 𝑦 ⊆ 𝑥). Notice that if M is a model and e is a partial instance, then M |= Full(e) if and only if e is also an instance (i.e., it has no undefined features). We also use the formula AllPos(𝑥) := ∀𝑦 (𝑥 ⊆ 𝑦 ∧ Full(𝑦)) → Pos(𝑦) , such that M |= AllPos(e) if and only if every instance in comp(e) is classified as positive by M. Analogously, we define a formula AllNeg(𝑥). The definitions of both predicates are inspired by important knowledge compilation queries such as a conditioning transformation of the input and a consistency or validity check on the conditioned model [17]. AllPos(𝑥) and AllNeg(𝑥) will be important components of a new logic for explainability defined in Section 4 since they enable the expression of a wide range of explainability queries. For example, we can now define weak abductive explanations (refer to Section 2.2) in FOIL as follows: wAXp(𝑥, 𝑦) := Full(𝑥) ∧ 𝑦 ⊆ 𝑥 ∧ (Pos(𝑥) → AllPos(𝑦)) ∧ (¬Pos(𝑥) → AllNeg(𝑦)). In fact, it is easy to see that M |= wAXp(e, e′ ) if and only if e′ is a weak abductive explanation for e over M. Notice that e is always a weak abductive explanation for itself. However, we are typically interested in explanations that satisfy some optimality criterion. A common such criterion is that of being minimal [11, 27, 41]. Let us write 𝑥 ⊂ 𝑦 for
10
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
𝑥 ⊆ 𝑦 ∧ ¬(𝑦 ⊆ 𝑥). Then, for AXp(𝑥, 𝑦) := wAXp(𝑥, 𝑦) ∧ ∀𝑧 (𝑧 ⊂ 𝑦 → ¬wAXp(𝑥, 𝑧)), we have that M |= AXp(e, e′ ) if and only if e′ is an abductive explanation for e over M. We could similarly express local explainability queries like contrastive explanations through the same approach using FOIL. As we show below, FOIL fails to meet either of the two criteria we are looking for in a practical language that provides explanations. The first issue is its limited expressiveness: there are important notions of explanations that cannot be expressed in this language, even when restricted to decision trees, which are traditionally deemed to be easily interpretable. The second issue is its high computational complexity: there are queries in FOIL that cannot be evaluated with a polynomial number of calls to an NP oracle. Both facts firmly establish the inadequacy of FOIL as a practical language. 3.2
FOIL presents limited expressiveness
In some scenarios we want to express a stronger condition for abductive and contrastive explanations: not only that they are minimal, but also that they are minimum (see Section 2.2). In the case of abductive explanations, they can be minimal without being minimum. The following theorem shows that FOIL cannot express the query that asks whether a partial instance e′ is a minimum abductive explanation for a given instance e over decision trees. Theorem 3.1. There is no formula mAXp(𝑥, 𝑦) in FOIL such that, for every decision tree T , instance e and partial instance e′ , we have that T |= mAXp(e, e′ ) ⇔ e′ is a minimum abductive explanation for e over T . Proof. The proof extends techniques from [31] such as the games for FO distinguishability. We now present notions that will be used in this and the following arguments throughout this paper. The quantifier rank of an FO formula 𝜑, denoted by qr(𝜑), is the maximum depth of quantifier nesting in it. For a structure 𝔄, we write dom(𝔄) to denote its domain. An Ehrenfeucht-Fraïssé (EF) game is played in two structures, 𝔄1 and 𝔄2 , of the same schema, by two players, the spoiler and the duplicator. In round 𝑖 the spoiler selects a structure, say 𝔄1 , and an element 𝑐𝑖 in dom(𝔄1 ); the duplicator responds by selecting an element 𝑒𝑖 in dom(𝔄2 ). The duplicator wins in 𝑘 rounds, for 𝑘 ≥ 0, if {(𝑐𝑖 , 𝑒𝑖 ) | 𝑖 ≤ 𝑘 } defines a partial isomorphism between 𝔄1 and 𝔄2 . If the duplicator wins no matter how the spoiler plays, we write 𝔄1 ≡𝑘 𝔄2 . A classical result states that 𝔄1 ≡𝑘 𝔄2 iff 𝔄1 and 𝔄2 agree on all FO sentences of quantifier rank ≤ 𝑘 (cf. [31]). ¯ ¯ ≡𝑘 (𝔄2, 𝑏) Also, if 𝑎¯ is an 𝑚-tuple in dom(𝔄1 ) and 𝑏¯ is an 𝑚-tuple in dom(𝔄2 ), where 𝑚 ≥ 0, we write (𝔄1, 𝑎) ¯ ¯ 𝑏). In the same whenever the duplicator wins in 𝑘 rounds no matter how the spoiler plays, but starting from position (𝑎, ¯ iff for every FO formula 𝜑 (𝑥) ¯ ¯ ≡𝑘 (𝔄2, 𝑏) ¯ of quantifier rank ≤ 𝑘, it holds that 𝔄1 |= 𝜑 (𝑎) ¯ ⇔ 𝔄2 |= 𝜑 (𝑏). way, (𝔄1, 𝑎) It is well-known (cf. [31]) that there are only finitely many FO formulae of quantifier rank 𝑘, up to logical equivalence. ¯ of quantifier rank ≤ 𝑘 such that 𝔄 |= 𝜑 (𝑎). ¯ The rank-𝑘 type of an 𝑚-tuple 𝑎¯ in a structure 𝔄 is the set of all formulae 𝜑 (𝑥) ¯ Given the above, there are only finitely many rank-𝑘 types, and each one of them is definable by an FO formula 𝜏𝑘(𝔄,𝑎) (𝑥) ¯
of quantifier rank 𝑘. We now introduce some terminology necessary for the proof. Let M, M ′ be models of dimension 𝑛 and 𝑝, respectively, and consider the structures 𝔄 M = ⟨{0, 1, ⊥}𝑛 , ⊆𝔄M , Pos𝔄M ⟩ and 𝔄 M ′ = ⟨{0, 1, ⊥}𝑝 , ⊆𝔄M ′ , Pos𝔄M ′ ⟩. We write 𝔄 M ⊕ 𝔄 M ′ for the structure over the same vocabulary that satisfies the following: • The domain of 𝔄 M ⊕ 𝔄 M ′ is {0, 1, ⊥}𝑛+𝑝 .
ExplAIner: A Declarative Query Language for Explaining Classification Models
11
• The interpretation of ⊆ on 𝔄 M ⊕ 𝔄 M ′ is the usual subsumption relation on {0, 1, ⊥}𝑛+𝑝 . • The interpretation of Pos on 𝔄 M ⊕ 𝔄 M ′ is the set of instances e ∈ {0, 1}𝑛+𝑝 such that (e[1], · · · , e[𝑛]) ∈ Pos𝔄M or (e[𝑛 + 1], · · · , e[𝑛 + 𝑝]) ∈ Pos𝔄M ′ . We will also consider structures of the form 𝔄𝑛 = ⟨{0, 1, ⊥}𝑛 , ⊆𝔄 ⟩, where ⊆ is interpreted as the subsumption relation over {0, 1, ⊥}𝑛 . For any such structure, we write 𝔄𝑛+ for the structure over the vocabulary {⊆, Pos} that extends 𝔄 by adding only the tuple {1}𝑛 to the interpretation of Pos. We now state two crucial lemmas, whose proofs can be found in the appendix of this work (refer to Sections A.1 and A.2). Lemma 3.2. If 𝑛, 𝑝 ≥ 3𝑘 , then (𝔄𝑛 , {1}𝑛 ) ≡𝑘 (𝔄𝑝 , {1}𝑝 ). In particular, 𝔄𝑛+ ≡𝑘 𝔄𝑝+ . Lemma 3.3. Consider models M, M1 , and M2 of dimension 𝑛, 𝑝, and 𝑞, respectively, and assume that (𝔄 M1 , {1}𝑝 ) ≡𝑘 (𝔄 M2 , {1}𝑞 ). Then it is the case that 𝔄 M ⊕ 𝔄 M1 , {1}𝑛+𝑝 , {⊥}𝑛 · {1}𝑝
≡𝑘
𝔄 M ⊕ 𝔄 M2 , {1}𝑛+𝑞 , {⊥}𝑛 · {1}𝑞 .
We now proceed with the proof of Theorem 3.1. Assume, for the sake of contradiction, that there is in fact a formula mAXp(𝑥, 𝑦) in FOIL such that, for every decision tree M, instance e, and partial instance e′ , we have that 𝔄 M |= mAXp(e, e′ ) iff e′ is a minimum abductive explanation for e over M. Let 𝑘 ≥ 0 be the quantifier rank of this formula. We show that there exist decision trees M1 and M2 , instances e1 and e2 over M1 and M2 , respectively, and partial instances e1′ and e2′ over M1 and M2 , respectively, for which the following holds: • (M1, e1, e1′ ) ≡𝑘 (M2, e2, e2′ ), and hence M1 |= mAXp(e1, e1′ ) ⇔ M2 |= mAXp(e2, e2′ ). • It is the case that e1′ is a minimum abductive explanation for e1 under M1 , but e2′ is not a minimum abductive explanation for e2 under M2 . This is our desired contradiction. Let M𝑛,𝑝 be a decision tree of dimension 𝑛 + 𝑝 such that, for every instance e ∈ {0, 1}𝑛+𝑝 , we have that M𝑛,𝑝 (e) = 1 iff e is of the form {1}𝑛 · {0, 1}𝑝 , i.e., the first 𝑛 features of e are set to 1, or e is of the form {0, 1}𝑛 · {1}𝑝 , i.e., the last 𝑝 features of e are set to 1. Take the instance e = {1}𝑛+𝑝 . It is easy to see that e only has two abductive explanations in M𝑛,𝑝 ; namely, e1 = {1}𝑛 · {⊥}𝑝 and e2 = {⊥}𝑛 · {1}𝑝 . We define the following: • M1 := M2𝑘 ,2𝑘 and M2 := M2𝑘 ,2𝑘 +1 . 𝑘
𝑘
𝑘
𝑘
• e1 := {1}2 +2 and e2 := {1}2 +2 +1 . • e1′ := {⊥}
2𝑘
· {1}
2𝑘
𝑘
𝑘
and e2′ := {⊥}2 · {1}2 +1 .
From our previous observation, e1′ is an abductive explanation for e1 over M1 and e2′ is an abductive explanation for e2 over M2 . We show first that (𝔄 M1 , e1, e1′ ) ≡𝑘 (𝔄 M2 , e2, e2′ ). It can be observed that 𝔄 M1 is of the form 𝔄𝑁 ⊕ 𝔄𝑁1 , where 𝑁 is 𝑘
a model of dimension 2𝑘 that only accepts the tuple {1}2 and the same holds for 𝑁 1 . Analogously, 𝔄 M2 is of the form 𝑘
𝔄𝑁 ⊕ 𝔄𝑁2 , where 𝑁 2 is a model of dimension 2𝑘 + 1 that only accepts the tuple {1}2 +1 . From Lemma 3.2, we have that 𝑘
𝑘
(𝔄𝑁1 , {1}2 ) ≡𝑘 (𝔄𝑁2 , {1}2 +1 ).
12
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux 𝑘
𝑘
Notice that indeed any winning strategy for the Duplicator on this game must map the tuples {1}2 in 𝔄𝑁1 and {1}2 +1 into each other. Now, from Lemma 3.3, we obtain that 𝑘
𝑘
𝑘
𝑘
𝔄𝑁 ⊕ 𝔄𝑁1 , {1}2 +2 , {⊥}2 · {1}2
≡𝑘
𝑘 𝑘 𝑘 𝑘 𝔄𝑁 ⊕ 𝔄𝑁2 , {1}2 +2 +1, {⊥}2 · {1}2 +1 .
We can then conclude that (𝔄 M1 , e1, e1′ ) ≡𝑘 (𝔄 M2 , e2, e2′ ), as desired. Notice now that e1′ is a minimum abductive explanation for e1 over M1 . In fact, by our previous observations, the 𝑘
𝑘
only other abductive explanation for e1 over M1 is e1′′ = {1}2 · {⊥}2 , which has the same number of undefined 𝑘
𝑘
features as e1′ . In turn, e2′ is not a minimum abductive explanation for e2 over M2 . This is because e2′′ = {1}2 · {⊥}2 +1 is also an abductive explanation for e2 over M2 , and e2′′ has more undefined features than e2′ . 3.3
□
Evaluating FOIL is intractable
For each query 𝜑 (𝑥 1, . . . , 𝑥𝑘 ) in FOIL and C a class of models, we define its associated problem Eval(𝜑, C) as follows (we assume models and instances have the same dimension): Problem:
Eval(𝜑, C)
Input:
A model M ∈ C and partial instances e1, . . . , e𝑘
Output:
Yes, if M |= 𝜑 (e1, . . . , e𝑘 ), and No otherwise
It is known that there exists a formula 𝜑 (𝑥) in FOIL for which its evaluation problem over the class of decision trees is NP-hard [4]. We want to determine whether the language FOIL is appropriate for implementation using SAT encodings. Thus, it is natural to ask whether the evaluation problem for formulas in this logic can always be decided in polynomial time by using a NP oracle. However, we prove that this is not always the case. Although the evaluation of FOIL formulas is always in the polynomial hierarchy (PH), there exist formulas in FOIL for which their corresponding evaluation problems are hard for every level of PH. Based on widely held complexity assumptions, we can conclude that FOIL contains formulas whose evaluations cannot be decided in polynomial time by using a NP oracle even on decision trees (DTree). Theorem 3.4. The following statements hold: (1) Let 𝜑 be a FOIL formula. Then, there exists 𝑘 ≥ 0 such that Eval(𝜑, NNF) is in the Σ𝑘P complexity class. (2) For every 𝑘 ≥ 0, there is an FOIL-formula 𝜑𝑘 such that Eval(𝜑𝑘 , DTree) is Σ𝑘P -hard. Proof. For the first item, consider a fixed FOIL formula 𝜑 (𝑥 1, . . . , 𝑥𝑚 ). We assume without loss of generality that 𝜑 is in prenex normal form, i.e., it is of the form ∃𝑦¯1 ∀¯ 𝑦2 · · · 𝑄𝑘 𝑦¯𝑘 𝜓 (𝑥 1, . . . , 𝑥𝑚 , 𝑦¯1, . . . , 𝑦¯𝑘 ),
(𝑘 ≥ 0)
where 𝑄𝑘 = ∃ if 𝑘 is odd and 𝑄𝑘 = ∀ otherwise, and 𝜓 is a quantifier-free formula. A FOIL formula of this form is called a Σ𝑘 -FOIL formula. Consider that M is a negation normal form of dimension 𝑛, and assume that we want to check whether M |= 𝜑 (e1, . . . , e𝑚 ), for e1, . . . , e𝑚 given partial instances of dimension 𝑛. We know that the predicates Pos and ⊆ can be decided in polynomial time on M. Additionally, the formula 𝜑 is fixed, and thus the length of each tuple 𝑦¯𝑖 , for 𝑖 ≤ 𝑘, is constant. Therefore, we can decide this problem in polynomial time by using a Σ𝑘 -alternating Turing machine (as the fixed size quantifier-free formula 𝜓 can be evaluated in polynomial time over M).
ExplAIner: A Declarative Query Language for Explaining Classification Models
13
We now deal with the second item. We start by studying the complexity of the well-known quantified Boolean formula (QBF) problem for the case when the underlying formula (or, more precisely, the underlying Boolean function) is defined by a decision tree. More precisely, suppose that M is a decision tree over instances of dimension 𝑛. A Σ𝑘 -QBF over M, for 𝑘 > 1, is an expression ∃𝑃1 ∀𝑃2 · · · 𝑄𝑘 𝑃𝑘 M, where 𝑄𝑘 = ∃ if 𝑘 is odd and 𝑄𝑘 = ∀ otherwise, and 𝑃1, . . . , 𝑃𝑘 is a partition of {1, . . . , 𝑛} into 𝑘 equivalence classes. As an example, if M is of dimension 3 then ∃{2, 1}∀{3} M is a Σ2 -QBF over M. The semantics of these expressions is standard. For instance, ∃{1, 2}∀{3} M holds if there exists a partial instance (𝑏 1, 𝑏 2, ⊥) ∈ {0, 1} × {0, 1} × {⊥} such that both M (𝑏 1, 𝑏 2, 0) = 1 and M (𝑏 1, 𝑏 2, 1) = 1. For a fixed 𝑘 > 1, we introduce then the problem Σ𝑘 -QBF(DTree). It takes as input a Σ𝑘 -QBF 𝛼 over M, for M a decision tree, and asks whether 𝛼 holds. We establish the following result, which we believe of independent interest, as (to the best of our knowledge) the complexity of the QBF problem over decision trees has not been studied in the literature (refer to Section A.3 for the proof). Lemma 3.5. For every odd 𝑘 ≥ 1, the problem Σ𝑘+1 -QBF(DTree) is Σ𝑘P -complete. For the second item, we can now finish the proof of the theorem with the help of Lemma 3.5 and a reduction from Σ𝑘+1 -QBF(DTree). We can assume that 𝑘 is odd because for proving that there are FOIL-formulas 𝜑𝑘 ′ such that Eval(𝜑𝑘 ′ , DTree) is Σ𝑘P′ -hard it is enough to show that there are FOIL-formulas 𝜑𝑘 such that Eval(𝜑𝑘 , DTree) is Σ𝑘P′ -hard for some 𝑘 ≥ 𝑘 ′ . The input to Σ𝑘+1 -QBF(DTree) is given by an expression 𝛼 of the form ∃𝑃1 ∀𝑃2 · · · ∃𝑃𝑘 ∀𝑃𝑘+1 M, for M a decision tree of dimension 𝑛 and 𝑃1, . . . , 𝑃𝑘+1 a partition of {1, . . . , 𝑛}. We explain next how the formula 𝜑𝑘 (𝑥 1, . . . , 𝑥𝑘+1 ) is defined. We start by defining some auxiliary terminology. We use 𝑥 [𝑖] to denote the 𝑖-th feature of the partial instance that is assigned to variable 𝑥. We define the following formulas. • Undef (𝑥) := ¬∃𝑦(𝑦 ⊂ 𝑥). That is, Undef defines the set that only consists of the partial instance {⊥}𝑛 in which all components are undefined. • Single(𝑥) := ∃𝑦(𝑦 ⊂ 𝑥) ∧ ∀𝑦 (𝑦 ⊂ 𝑥 → Undef(𝑦)). That is, Single defines the set that consists precisely of those partial instances in {0, 1, ⊥}𝑛 which have exactly one defined component. • (𝑥 ⊔ 𝑦 = 𝑧) := (𝑥 ⊆ 𝑧) ∧ (𝑦 ⊆ 𝑧) ∧ ¬∃𝑤 (𝑥 ⊆ 𝑤) ∧ (𝑦 ⊆ 𝑤) ∧ (𝑤 ⊂ 𝑧) . That is, 𝑧, if it exists, is the join of 𝑥 and 𝑦. In other words, 𝑧 is defined if every feature that is defined over 𝑥 and 𝑦 takes the same value in both partial instances, and, in such case, for each 1 ≤ 𝑖 ≤ 𝑛 we have that 𝑧 [𝑖] = 𝑥 [𝑖] ⊔ 𝑦 [𝑖], where ⊔ is the commutative and idempotent binary operation that satisfies ⊥ ⊔ 0 = 0 and ⊥ ⊔ 1 = 1. As an example, (1, 0, ⊥, ⊥) ⊔ (1, ⊥, ⊥, 1) = (1, 0, ⊥, 1), while (1, ⊥) ⊔ (0, 0) is undefined. • (𝑥 ⊓ 𝑦 = 𝑧) := (𝑧 ⊆ 𝑥) ∧ (𝑧 ⊆ 𝑦) ∧ ¬∃𝑤 (𝑤 ⊆ 𝑥) ∧ (𝑤 ⊆ 𝑦) ∧ (𝑧 ⊂ 𝑤) . That is, 𝑧 is the meet of 𝑥 and 𝑦 (which always exists). In other words, for each 1 ≤ 𝑖 ≤ 𝑛 we have that 𝑧 [𝑖] = 𝑥 [𝑖] ⊓ 𝑦 [𝑖], where ⊓ is the commutative and idempotent binary operation that satisfies ⊥ ⊓ 0 = ⊥ ⊓ 1 = 0 ⊓ 1 = ⊥. As an example, (1, 0, ⊥, ⊥) ⊓ (1, ⊥, ⊥, 1) = (1, ⊥, ⊥, ⊥), while (1, ⊥) ⊓ (0, 0) = (⊥, ⊥). • Comp(𝑥, 𝑦) := ∃𝑤∃𝑧 (Undef(𝑧) ∧ 𝑥 ⊔ 𝑦 = 𝑤 ∧ 𝑥 ⊓ 𝑦 = 𝑧). That is, Comp defines the pairs (e1, e2 ) of partial instances in {0, 1, ⊥}𝑛 × {0, 1, ⊥}𝑛 such that no feature that is defined in e1 is also defined in e2 , and vice versa.
14
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux In fact, assume for the sake of contradiction that this is not the case. By symmetry, we only have to consider the following two cases. – There is an 𝑖 ≤ 𝑛 with e1 [𝑖] = 1 and e2 [𝑖] = 0. Then the join of e1 and e2 does not exist. – There is an 𝑖 ≤ 𝑛 with e1 [𝑖] = e2 [𝑖] = 1. Then the 𝑖-th component of the meet of e1 and e2 takes value 1, and hence e1 ⊓ e2 ≠ {⊥}𝑛 . • MaxComp(𝑥, 𝑦) := Comp(𝑥, 𝑦) ∧ ¬∃𝑧 (𝑦 ⊂ 𝑧) ∧ Comp(𝑥, 𝑧) . That is, MaxComp defines the pairs (e1, e2 ) such that the components that are defined in e1 are precisely the ones that are undefined in e2 , and vice versa. • Rel(𝑥, 𝑦) := ¬∃𝑧 (𝑧 ⊆ 𝑦) ∧ Single(𝑧) ∧ Comp(𝑥, 𝑧) . That is, Rel defines the pairs (e1, e2 ) of partial instances in {0, 1, ⊥}𝑛 × {0, 1, ⊥}𝑛 such that every feature that is defined in e1 is also defined in e2 . • MaxRel(𝑥, 𝑦) := Rel(𝑥, 𝑦) ∧ ¬∃𝑧 (𝑧 ⊂ 𝑦) ∧ Rel(𝑥, 𝑧) . That is, MaxRel defines the pairs (e1, e2 ) such that the features defined in e1 and in e2 are the same. For defining the formula 𝜑𝑘 (𝑥 1, . . . , 𝑥𝑘+1 ) we will use guarded quantifiers. For each 𝑖 with 1 ≤ 𝑖 ≤ 𝑘 + 1 consider ∃ G (𝑥𝑖 ) 𝑦𝑖 𝜓 = ∃𝑦𝑖 MaxRel(𝑥𝑖 , 𝑦𝑖 ) ∧ 𝜓 ∀ G (𝑥𝑖 ) 𝑦𝑖 𝜓 = ∀𝑦𝑖 MaxRel(𝑥𝑖 , 𝑦𝑖 ) → 𝜓 We now define the formula 𝜑𝑘 (𝑥 1, . . . , 𝑥𝑘+1 ) as ∃ G (𝑥 1 ) 𝑦1 ∀ G (𝑥 2 ) 𝑦2 · · · ∃ G (𝑥𝑘 ) 𝑦𝑘 ∀ G (𝑥𝑘+1 ) 𝑦𝑘+1 ∀𝑧 𝑧 = 𝑦1 ⊔ 𝑦2 ⊔ · · · ⊔ 𝑦𝑘+1 → Pos(𝑧)
For each 𝑖 with 1 ≤ 𝑖 ≤ 𝑘 + 1, let e𝑖 be the partial instance of dimension 𝑛 such that 1 e𝑖 [ 𝑗] = ⊥
if 𝑗 ∈ 𝑃𝑖 , otherwise.
That is, e𝑖 takes value 1 over the features in 𝑃𝑖 and it is undefined over all other features. We claim that 𝛼 holds if, and only if, M |= 𝜑𝑘 (e1, . . . , e𝑘+1 ). The result then follows since M is a decision tree. For the sake of presentation we only prove the aforementioned equivalence for the case when 𝑘 = 1, since the extension to 𝑘 > 1 is standard (but cumbersome). That is, we consider the case when 𝛼 = ∃𝑃1 ∀𝑃2 M and, therefore, 𝜑 2 (𝑥 1, 𝑥 2 ) = ∃ G (𝑥 1 ) 𝑦1 ∀ G (𝑥 2 ) 𝑦2 ∀𝑧 𝑧 = 𝑦1 ⊔ 𝑦2 → Pos(𝑧) . (⇐) Assume first that M |= 𝜑 2 (e1, e2 ). Hence, there exists a partial instance e1′ such that M |= MaxRel(e1, e1′ ) ∧ ∀ G (e2 ) 𝑦2 ∀𝑧 𝑧 = e1′ ⊔ 𝑦2 → Pos(𝑧) .
(1)
This means that the features defined in e1 and e1′ are exactly the same, and hence e1′ is a partial instance that is defined precisely over the features in 𝑃1 . We claim that every instance e that is a completion of e1′ satisfies M (e) = 1, thus showing that 𝛼 holds. In fact, take e to be an arbitrary completion. By definition, e can be written as e1′ ⊔ e2′ , where e2′ is a partial instance that is defined precisely over those features not in 𝑃1 , i.e., over the features in 𝑃2 . Thus in the formula (1) we can assign the partial instance e2′ to the variable 𝑦2 and the instance e to the variable 𝑧, which allows us to conclude that M |= Pos(e). This tells us that M (e) = 1. (⇒) Assume in turn that 𝛼 holds, and hence that there is a partial instance e1′ that is defined precisely over the features in 𝑃1 such that every instance e that is a completion of e1′ satisfies M (e) = 1. We claim that M |= MaxRel(e1, e1′ ) ∧ ∀ G (e2 ) 𝑦2 ∀𝑧 𝑧 = e1′ ⊔ 𝑦2 → Pos(𝑧) ,
ExplAIner: A Declarative Query Language for Explaining Classification Models
15
which implies that M |= 𝜑 2 (e1, e2 ). In fact, let e2′ be an arbitrary instance such that MaxRel(e2, e2′ ) holds. By definition, e2′ is defined precisely over the features in 𝑃2 . Let e = e1′ ⊔ e2′ . Notice that e is well-defined since the sets of features defined in e1′ and e2′ , respectively, are disjoint. Moreover, e is a completion of e1′ as 𝑃1 ∪ 𝑃2 = {1, . . . , 𝑛}. We then have that M (e) = 1 as 𝛼 holds. This allows us to conclude that M |= Pos(e), and hence that M |= 𝜑 2 (e1, e2 ). This concludes the proof of the theorem. 4
□
ExplAIner: a tractable logic for explainability
In the previous section we identified two limitations of FOIL that must be addressed in order to build a practical logic for explanations. On one hand, we must extend FOIL to increase its expressive power, and on the other hand, we must constrain the resulting logic to ensure that its evaluation complexity is appropriate. In this section we define ExplAIner, a logic that takes both criteria into account and in which explainability notions can be expressed naturally. 4.1
The atomic layer of ExplAIner
FOIL cannot express properties such as minimum abductive explanations that involve comparing cardinalities of sets of features. As a first step, we solve this issue by extending the vocabulary of FOIL with a simple binary relation ⪯ defined as: ′ M |= e ⪯ e′ ⇐⇒ |e⊥ | ≥ |e⊥ |.
As we will show later, the use of this predicate indeed allows us to express many notions of explanations. Note that we could not simply keep only one of ⊆ and ⪯ when defining the new logic, as we show that they cannot be defined in terms of each other. First, we show that predicate ⪯ cannot be defined in terms of predicate ⊆. Proposition 4.1. There is no formula 𝜑 (𝑥, 𝑦) in FOIL defined over the vocabulary {⊆} such that, for every decision tree T and pair of partial instances e, e′ , we have that ′ T |= 𝜑 (e, e′ ) ⇐⇒ |e⊥ | ≥ |e⊥ |.
Proof. For the sake of contradiction, assume that 𝜑 (𝑥, 𝑦) is definable in FOIL over the vocabulary {⊆}. Then the following are formulas in FOIL: wAXp(𝑥, 𝑦)
:=
mAXp(𝑥, 𝑦)
:=
Full(𝑥) ∧ 𝑦 ⊆ 𝑥 ∧ ∀𝑧 𝑦 ⊆ 𝑧 ∧ Full(𝑧) → (Pos(𝑧) ↔ Pos( 𝑥)) , wAXp(𝑥, 𝑦) ∧ ∀𝑧 wAXp(𝑥, 𝑧) → (𝜑 (𝑧, 𝑦) → 𝜑 (𝑦, 𝑧)) .
But the second formula verifies if a partial instance 𝑦 is a minimum abductive explanation for a given instance 𝑥, which contradicts the inexpressibility result of Theorem 3.1, and hence concludes the proof of the proposition.
□
Second, we show that predicate ⊆ cannot be defined in terms of predicate ⪯. Proposition 4.2. There is no formula 𝜓 (𝑥, 𝑦) in FOIL defined over the vocabulary {⪯} such that, for every decision tree T 2 and pair of partial instances e, e′ , we have that T |= 𝜓 (e, e′ ) ⇐⇒ e is subsumed by e′ . 2 Naturally, this statement does not rely on decision trees at all since it concerns only ⊆ and ⪯ ; we only state it in these terms for consistency.
16
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux Proof. Intuitively, ⪯ is invariant under any bijection of partial instances that preserves the number of ⊥’s, whereas
subsumption is not. We formalize this as follows. For the sake of contradiction, assume that 𝜓 (𝑥, 𝑦) is definable in FOIL over the vocabulary {⪯}, and let 𝑛 ≥ 3. Moreover, for every 𝑘 ∈ {0, . . . , 𝑛}, define 𝐿𝑘 as the following set of partial instances: {e ∈ {0, 1, ⊥}𝑛 | |e⊥ | = 𝑘},
=
𝐿𝑘
and let 𝑓𝑘 : 𝐿𝑘 → 𝐿𝑘 be an arbitrary bijection from 𝐿𝑘 to itself. Finally, let 𝑓 : {0, 1, ⊥}𝑛 → {0, 1, ⊥}𝑛 be defined as 𝑓 (e) = 𝑓𝑖 (e) if e ∈ 𝐿𝑖 . Clearly, 𝑓 is a bijection from {0, 1, ⊥}𝑛 to {0, 1, ⊥}𝑛 . For a decision tree T of dimension 𝑛, define 𝔄 ′T as the restriction of 𝔄 T to the vocabulary {⪯}. Then function 𝑓 is an automorphism of 𝔄 ′T since 𝑓 is a bijection from {0, 1, ⊥}𝑛 to {0, 1, ⊥}𝑛 , and for every pair of partial instances e1, e2 : 𝔄 ′T |= e1 ⪯ e2
if and only if
𝔄 ′T |= 𝑓 (e1 ) ⪯ 𝑓 (e2 ).
Then given that 𝜓 (𝑥, 𝑦) is definable in first-order logic over the vocabulary {⪯}, we have that for every pair of partial instances e1, e2 : 𝔄 ′T |= 𝜓 (e1, e2 )
if and only if
𝔄 ′T |= 𝜓 (𝑓 (e1 ), 𝑓 (e2 )).
(2)
But now assume that 𝑔𝑘 : 𝐿𝑘 → 𝐿𝑘 is defined as the identity function for every 𝑘 ∈ {0, . . . , 𝑛} \ {1}, and assume that 𝑔1 is defined as follows for every partial instance e:
𝑔1 (e)
=
(⊥, 0, . . . , 0) (0, . . . , 0, ⊥) e
if e = (0, . . . , 0, ⊥) if e = (⊥, 0, . . . , 0) otherwise
Clearly, each function 𝑔𝑖 is a bijection. Moreover, let 𝑔 : {0, 1, ⊥}𝑛 → {0, 1, ⊥}𝑛 be defined as 𝑔(e) = 𝑔𝑖 (e) if e ∈ 𝐿𝑖 . Then we have by (2) that for every pair of partial instances e1 , e2 : 𝔄 ′T |= 𝜓 (e1, e2 )
if and only if
𝔄 ′T |= 𝜓 (𝑔(e1 ), 𝑔(e2 )).
Hence, taking e1 = (⊥, ⊥, 0, . . . , 0) and e2 = (⊥, 0, . . . , 0), given that 𝑔(e1 ) = (⊥, ⊥, 0, . . . , 0) and 𝑔(e2 ) = (0, . . . , 0, ⊥), we conclude that: 𝔄 ′T |= 𝜓 ((⊥, ⊥, 0, . . . , 0), (⊥, 0, . . . , 0)) if and only if 𝔄 ′T |= 𝜓 ((⊥, ⊥, 0, . . . , 0), (0, . . . , 0, ⊥)). But this leads to a contradiction, since (⊥, ⊥, 0, . . . , 0) is subsumed by (⊥, 0, . . . , 0), but (⊥, ⊥, 0, . . . , 0) is not subsumed by (0, . . . , 0, ⊥). This concludes the proof of the proposition.
□
However, adding ⪯ to FOIL can only add extra complexity. Therefore, our second step is to define the logic ExplAIner expressive enough to capture important notions, but keeping the evaluation tractable using SAT solvers. Our logic ExplAIner consists of three hierarchical layers, where the first layer does not depend on the structure of the model. Predicates ⊆ and ⪯, as well as predicate Full used in Section 3.1, can be regarded as syntactic in the sense that they refer to the values of the features of partial instances, and they do not make reference to classification models. It turns out that all the syntactic predicates needed in our logical formalism can be expressed as first-order formulas over the
ExplAIner: A Declarative Query Language for Explaining Classification Models
17
predicates ⊆ and ⪯. The atomic formulas of ExplAIner are defined as first-order formulas over the vocabulary {⊆, ⪯}. We now prove that such formulas can be evaluated in polynomial time. We also prove that in the case of sentences, that is, formulas without free variables, it is decidable whether a sentence is true in every structure 𝔅𝑛 . Given 𝑛 ≥ 0 and a model M of dimension 𝑛, define 𝔅M as a structure over the vocabulary {⊆, ⪯} generated from 𝔄 M by removing the interpretation of predicate Pos, and adding the interpretation of predicate ⪯. Notice that, given two models M1 and M2 of dimension 𝑛, we have that 𝔅M1 = 𝔅M2 , so we define simply 𝔅𝑛 as 𝔅M for an arbitrary model of dimension 𝑛. Therefore, when measuring the complexity of evaluating formulas in the atomic layer, we take 𝑛 in unary as part of the input, since 𝑛 is the size of the partial instances. Hence, for each formula 𝜑 (𝑥 1, . . . , 𝑥𝑘 ) in the atomic layer of ExplAIner, we define its associated problem Eval(𝜑) as follows: Problem: Input: Output:
Eval(𝜑) An integer 𝑛 ∈ N given in unary and partial instances e1, . . . , e𝑘 Yes, if 𝔅𝑛 |= 𝜑 (e1, . . . , e𝑘 ), and No otherwise
Recall also that the width of a first-order formula 𝜑, denoted wd(𝜑), is defined as the maximum number of free variables among all subformulas of 𝜑 (see [20] for a reference). Theorem 4.3. The following statements hold: (1) Let 𝜑 be a first-order formula defined over the vocabulary {⊆, ⪯}. Then Eval(𝜑) ∈ P. (2) It is decidable whether a given first-order sentence 𝜑 defined over the vocabulary {⊆, ⪯}is true in every structure wd(𝜑 ) poly |𝜑 |·3wd(𝜑 )
𝔅𝑛 . In particular, it can be solved in 22
space, and, hence, in 22
2
poly |𝜑 |·3
time.
Proof. We will prove both claims by a reduction to Presburger arithmetic. One standard presentation of Presburger arithmetic consists of two constants, 0 and 1, a binary relation < and a binary function +. We consider the model N of the non-negative integers with the usual interpretations. We will use the following two well-known facts about Presburger arithmetic: I. Presburger arithmetic admits quantifier elimination, that is, for every Presburger formula 𝜑 (𝑦1, . . . , 𝑦𝑚 ) there exists a quantifier-free formula 𝜓 (𝑦1, . . . , 𝑦𝑚 ) such that 𝜑 and 𝜓 are logically equivalent [39]. II. The problem of determining the truth of sentences in Presburger Arithmetic with respect to the model N can be solved in double exponential space with respect to the size of the sentence [12]. First, we introduce some terminology. Let 𝑛 ∈ N be the dimension. Then, for a tuple Γ = (𝑥 1, . . . , 𝑥𝑘 ) of (distinct) variables, an assignment 𝑠 : Γ → {0, 1, ⊥}𝑛 , and a coordinate 𝑖 ∈ {1, . . . , 𝑛}, we define the “pattern” pat𝑖Γ,𝑠 as the tuple 𝑠 (𝑥 1 )𝑖 , . . . , 𝑠 (𝑥𝑘 )𝑖 ∈ {0, 1, ⊥}𝑘 . Given a pattern 𝜌 ∈ {0, 1, ⊥}𝑘 , we define its pattern count in (Γ, 𝑠) by 𝑐 𝜌Γ,𝑠 := { 𝑖 ∈ {1, . . . , 𝑛} : pat𝑖Γ,𝑠 = 𝜌 } . Clearly,
∑︁
𝑐 𝜌Γ,𝑠 = 𝑛. For example, let Γ = (𝑥 1, 𝑥 2 ) and let 𝑛 = 4. Suppose that 𝑠 (𝑥 1 ) = (1, ⊥, 0, 0) and 𝑠 (𝑥 2 ) =
𝜌 ∈ {0,1,⊥}𝑘
(1, 1, ⊥, ⊥). Then the four coordinates have patterns pat1Γ,𝑠 = (1, 1),
pat2Γ,𝑠 = (⊥, 1),
pat3Γ,𝑠 = (0, ⊥),
Hence 𝑐 Γ,𝑠 = 𝑐 Γ,𝑠 = 1, (1,1) (⊥,1) and every other pattern in {0, 1, ⊥}2 has count 0.
𝑐 Γ,𝑠 = 2, (0,⊥)
pat4Γ,𝑠 = (0, ⊥).
18
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux We are now ready to state the reduction lemma (refer to Section A.4 for the proof): Lemma 4.4. Let 𝜑 (𝑥 1, . . . , 𝑥 ℓ ) be a first-order formula defined over the vocabulary {⊆, ⪯}, and let Γ ≔ (𝑥 1, . . . , 𝑥𝑘 ) be a
tuple of distinct variables that contains all free variables of 𝜑. Then there exists a Presburger formula TΓ (𝜑) (𝑧 𝜌 )𝜌 ∈ {0,1,⊥}𝑘 such that for every 𝑛 ∈ N and every assignment 𝑠 : Γ → {0, 1, ⊥}𝑛 , 𝔅𝑛 |= 𝜑 (𝑠 (𝑥 1 ), . . . , 𝑠 (𝑥 ℓ ))
⇐⇒
N |= TΓ (𝜑) (𝑐 𝜌Γ,𝑠 )𝜌 .
Moreover, if 𝑘 = ℓ (that is, if Γ contains exactly the free variables of 𝜑), then we have that TΓ (𝜑) (𝑧 𝜌 )𝜌 ∈ {0,1,⊥}𝑘 = 𝑂 |𝜑 | · 3wd(𝜑 ) · poly(wd(𝜑)) , and the reduction can be computed using the same space. We now show how Lemma 4.4 implies both statements of the theorem. For the first part, let 𝜑 (𝑥 1, . . . , 𝑥𝑘 ) be a first-order formula defined over the vocabulary {⊆, ⪯}, and let Γ = (𝑥 1, . . . , 𝑥𝑘 ). Because Presburger arithmetic admits quantifier elimination, we know that there exists a quantifier-free Presburger formula 𝜓 (𝑧 𝜌 )𝜌 ∈ {0,1,⊥}𝑘 that is logically equivalent to TΓ (𝜑) (𝑧 𝜌 )𝜌 ∈ {0,1,⊥}𝑘 . From Lemma 4.4 we know that, for every 𝑛 ∈ N and every assignment 𝑠 : Γ → {0, 1, ⊥}𝑛 , 𝔅𝑛 |= 𝜑 (𝑠 (𝑥 1 ), . . . , 𝑠 (𝑥 ℓ ))
⇐⇒
N |= 𝜓 (𝑐 𝜌Γ,𝑠 )𝜌 .
Now suppose we are given an integer 𝑛 ∈ N in unary and partial instances e1, . . . , e𝑘 . Let 𝑠 : Γ → {0, 1, ⊥}𝑛 be the assignment such that 𝑠 (𝑥𝑖 ) = e𝑖 for every 𝑖 ∈ {1, . . . , 𝑘 }. Notice that we can compute in linear time all the values {𝑐 𝜌Γ,𝑠 } 𝜌 ∈ {0,1,⊥}𝑘 , as 3𝑘 is constant with respect to the input size of Eval(𝜑). Notice that each variable 𝑐 𝜌Γ,𝑠 has a value
less than or equal to 𝑛. Because 𝜓 is a fixed, quantifier-free formula, we can evaluate it onto the values {𝑐 𝜌Γ,𝑠 } 𝜌 ∈ {0,1,⊥}𝑘 in polynomial time. This shows that Eval(𝜑) ∈ P.
For the second part, let 𝜑 be a first-order sentence defined over the vocabulary {⊆, ⪯}. Because we can take Γ as an empty context, there is only one possible pattern. Therefore, the formula TΓ (𝜑) (𝑧) has exactly one free variable. Recall that, in general, given an assignment for Γ in 𝔅𝑛 , the sum over all pattern counts must equal 𝑛. Hence, in this case, 𝜑 is true in every structure 𝔅𝑛 if and only if ∀𝑚 TΓ (𝜑) (𝑚) is a true Presburger sentence. We know from Lemma 4.4 that the sentence ∀𝑚 TΓ (𝜑) (𝑚) has size 𝑂 |𝜑 | · 3wd(𝜑 ) · poly(wd(𝜑)) and it can be constructed in at most the same space. Because the problem of determining the truth value of a Presburger sentence can be solved in double exponential space, we conclude that we can determine if 𝜑 is true in every structure 𝔅𝑛 in 22
poly |𝜑 |·3wd(𝜑 )
space. This concludes the proof
of the theorem. □ 4.2
The quantified layer of ExplAIner
In this layer we introduce predicates whose interpretation does depend on the model. The vocabulary of this layer is {⊆, ⪯, AllPos, AllNeg}, where M |= AllPos(e) if and only if all instances in comp(e) are classified positively by M, and AllNeg is defined analogously. As we will show, at this point we will already be able to express properties over polynomial-size sets of instances and minimality/minimum conditions.
ExplAIner: A Declarative Query Language for Explaining Classification Models
19
We will need two auxiliary formulas from the atomic layer that we already defined during the proof of Theorem 3.4. The first is Undef(𝑥) := ¬∃𝑦 (𝑦 ⊂ 𝑥), which defines the set that only contains the partial instance {⊥}𝑛 . The second is Single(𝑥) := ∃𝑦 (𝑦 ⊂ 𝑥) ∧ ∀𝑦(𝑦 ⊂ 𝑥 → Undef(𝑦)), which defines the set of partial instances with exactly one defined feature. The quantified layer is recursively defined as follows: (1) Boolean combinations of formulas from the atomic layer, together with AllPos(𝑥) and AllNeg(𝑥), are formulas from the quantified layer. (2) If 𝜑 is a formula from the quantified layer, then ∃𝑥 𝜑 is a formula from the quantified layer. (3) If 𝜑 is a formula from the quantified layer, then ∀𝑥 (Single(𝑥) → 𝜑) is a formula from the quantified layer. Using only the first rule we can already express some basic explainability properties. For example, we can express the query for weak abductive explanations as follows: wAXp(𝑥, 𝑦) := Full(𝑥) ∧ 𝑦 ⊆ 𝑥 ∧ (AllPos(𝑥) → AllPos(𝑦)) ∧ (AllNeg(𝑥) → AllNeg(𝑦)). The third rule involves the concept of guarded quantification. In that case we only quantify over partial instances with exactly one defined feature, which naturally correspond to assignments of a value to a single feature. On any class of models C, the number of partial instances with one defined feature is at most twice the dimension of the model, so we cannot express universal properties over superpolynomial-size sets of partial instances. Notice that our rules do not allow us to define unguarded universal quantifiers because the first rule only allows us to take Boolean combinations of unquantified formulas. In particular, in this layer we are not allowed to negate formulas that were produced using the second (or third) rule. Theorem 4.5. The following statements hold: (1) Let C be a class of models such that Eval(AllPos(𝑥), C) ∈ P and Eval(AllNeg(𝑥), C) ∈ P. Then Eval(𝜑, C) ∈ NP for every formula 𝜑 from the quantified layer of ExplAIner. (2) There exists a formula 𝜑 from the quantified layer of ExplAIner such that Eval(𝜑, DTree) is NP-hard. Proof. For the first item, let C be a class of models such that Eval(AllPos(𝑥), C) ∈ P and Eval(AllNeg(𝑥), C) ∈ P, and let 𝜑 be a fixed formula from the quantified layer of ExplAIner. The algorithm is the following. For each existential quantifier we nondeterministically guess a partial instance as a polynomial-size witness. Each guarded universal quantifier ranges only over the set of partial instances with exactly one defined feature, whose size is linear in the dimension 𝑛. Since the formula is fixed, unfolding all guarded universal quantifiers yields only polynomially many cases (to be more precise, at most 𝑛𝑐 cases, where 𝑐 is the quantifier rank of 𝜑). At every computation path of this process, we are left with a Boolean combination of formulas from the atomic layer, together with AllPos(𝑥) and AllNeg(𝑥). Thanks to Theorem 4.3 and to the hypothesis that Eval(AllPos(𝑥), C) ∈ P and Eval(AllNeg(𝑥), C) ∈ P, and considering that the formula 𝜑 is fixed, we can do that evaluation in polynomial time. For the second item, we consider the following formula from the quantified layer of ExplAIner: nmAXp(𝑥, 𝑦) := ∃𝑧 ¬wAXp(𝑥, 𝑦) ∨ [𝑧 ≺ 𝑦 ∧ wAXp(𝑥, 𝑧)] .
20
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
nmAXp defines the pairs (e1, e2 ) such that the partial instance e2 is not a minimum abductive explanation for the instance e1 , that is, it is logically equivalent to ¬mAXp(𝑥, 𝑦). We conclude the proof using the following intermediate result, whose proof can be found in the appendix of this work (refer to Section A.5). Lemma 4.6. Eval(mAXp(𝑥, 𝑦), DTree) is coNP-hard. □ 4.3
The ExplAIner logic
We define ExplAIner as the logic obtained by taking Boolean combinations of formulas from the quantified layer. In particular, since we can negate quantified formulas, in this third layer we are allowed to use unguarded universal quantifiers. Nevertheless, notice that a necessary condition for a formula to have a valid syntax according to the ExplAIner logic is that alternations between unguarded quantifiers cannot occur. We now provide a precise characterization of the complexity of the evaluation problem for ExplAIner. More specifically, we establish that this problem can always be solved in the Boolean Hierarchy over NP [14, 44], i.e., in the class consisting of Boolean combinations of NP languages. In fact, we will show that the ExplAIner logic captures the entire Boolean Hierarchy. For the following theorem, we denote the levels of the Boolean Hierarchy by BH𝑘 , and we denote by BH the Boolean Hierarchy consisting of all these levels. Theorem 4.7. The following statements hold: (1) Let 𝜑 be an ExplAIner formula. Then there exists a 𝑘 ≥ 1 such that, for every class of models C such that Eval(AllPos(𝑥), C) ∈ P and Eval(AllNeg(𝑥), C) ∈ P, it holds that Eval(𝜑, C) ∈ BH𝑘 . (2) For every 𝑘 ≥ 1, there exists an ExplAIner formula 𝜑 such that Eval(𝜑, DTree) is BH𝑘 -hard. This result tells us that ExplAIner meets one of the fundamental criteria for an interpretability logic, namely that we can evaluate an ExplAIner formula over a tuple of partial instances in polynomial time with a polynomial number of calls to an NP oracle. In fact, by definition of the Boolean hierarchy, the evaluation of a fixed ExplAIner formula can be done with a constant number of calls to an NP oracle. Thus, we argue that the technology of SAT solvers will allow us to tractably evaluate ExplAIner over classes that support consistency and validity checks in polynomial time. More precisely, Theorem 4.7 requires the class of models C to satisfy that Eval(AllPos(𝑥), C) ∈ P and Eval(AllNeg(𝑥), C) ∈ P in order for ExplAIner to be able to tractably solve its evaluation problem over that class. This includes decision trees, but also richer representation classes like d-DNNF circuits. Moreover, this includes fragments of the class of circuits corresponding to propositional formulas in conjunctive normal form (CNF) whose satisfiability can be decided in polynomial time, such as the class of circuits corresponding to CNF formulas in which each clause contains at most two literals (2CNF), and the class of circuits corresponding to Horn CNF formulas (HORN). We formally state these results in the following corollary. Corollary 4.8. Let 𝜑 be an ExplAIner formula. Then Eval(𝜑, d-DNNF) ∈ BH, Eval(𝜑, 2CNF) ∈ BH, and Eval(𝜑, HORN) ∈ BH. In what follows, we provide a proof of Theorem 4.7. Proof of Theorem 4.7. We consider languages over a finite alphabet Σ. First, we introduce Boolean operations between complexity classes as follows [44]:
ExplAIner: A Declarative Query Language for Explaining Classification Models
21
(1) 𝐴 ∨ 𝐵 = {𝐿𝐴 ∪ 𝐿𝐵 | 𝐿𝐴 ∈ 𝐴 and 𝐿𝐵 ∈ 𝐵}; (2) 𝐴 ∧ 𝐵 = {𝐿𝐴 ∩ 𝐿𝐵 | 𝐿𝐴 ∈ 𝐴 and 𝐿𝐵 ∈ 𝐵}; (3) coA = {L | L ∈ A}. Then, the Boolean Hierarchy BH is defined as the union ∪𝑘 ≥1 BH𝑘 [14], where: (1) BH1 = NP; (2) BH2𝑖 = BH2𝑖 −1 ∧ coNP; (3) BH2𝑖+1 = BH2𝑖 ∨ NP. Note that coNP ⊆ BH2 . In fact, let 𝐿 ∈ coNP and note that 𝐿 = Σ∗ ∩ 𝐿, where Σ∗ ∈ BH1 . With this definition, every Boolean combination of NP and coNP languages is contained in BH𝑘 for some positive integer 𝑘. For the first item of the theorem, let 𝜑 be an ExplAIner formula. We know that 𝜑 is a fixed Boolean combination of formulas from the quantified layer of ExplAIner. Now let C be a class of models such that Eval(AllPos(𝑥), C) ∈ P and Eval(AllNeg(𝑥), C) ∈ P. Thanks to the first part of Theorem 4.5 we know that Eval(𝜓, C) ∈ NP for every formula 𝜓 from the quantified layer of ExplAIner that appears as a subformula of 𝜑. This means that the evaluation problem Eval(𝜑, C) corresponds to a fixed Boolean combination of languages in NP, and so it must be contained in BH𝑘 for some 𝑘 ≥ 1. Notice that such a 𝑘 does depend on 𝜑 but not on C. We now turn our attention to the second item of the theorem. We will first describe a family of decision problems known to be complete for every level of the Boolean hierarchy. As usual, let us denote by SAT the language of propositional formulas that are satisfiable, and by UNSAT the language of propositional formulas that are not satisfiable. For each 𝑘 ≥ 1 we define the language SAT(𝑘) recursively as follows: (1) SAT(1) := {(𝜑 1 ) | 𝜑 1 ∈ SAT}; (2) SAT(2𝑖) := {(𝜑 1, . . . 𝜑 2𝑖 ) | (𝜑 1, . . . 𝜑 2𝑖 −1 ) ∈ SAT(2𝑖 − 1) ∧ 𝜑 2𝑖 ∈ UNSAT}; (3) SAT(2𝑖 + 1) := {(𝜑 1, . . . 𝜑 2𝑖+1 ) | (𝜑 1, . . . 𝜑 2𝑖 ) ∈ SAT(2𝑖) ∨ 𝜑 2𝑖+1 ∈ SAT}. It is known that, for every 𝑘 ≥ 1, SAT(𝑘) is BH𝑘 -complete [14]. We will now fix a 𝑘 ≥ 1 and prove that there exists an ExplAIner formula 𝜑𝑘 such that SAT(𝑘) can be reduced in polynomial time to Eval(𝜑𝑘 , DTree), thus concluding the hardness item of the theorem. We know from Lemma 4.6 that the following language is NP-hard: 𝐿 = {(T , e, e′ ) | T is a decision tree, e and e′ are partial instances and T |= ¬mAXp(e, e′ )}. Also, because the class of decision trees satisfies the hypothesis of the first item of Theorem 4.5, we actually know that 𝐿 is NP-complete. Hence, we have a polynomial-time algorithm that, given a propositional formula 𝜓 , constructs a decision tree T𝜓 and partial instances e𝜓 , e𝜓′ such that: 𝜓 ∈ SAT
⇐⇒
T𝜓 |= ¬mAXp(e𝜓 , e𝜓′ ).
(3)
Let (𝜓 1, . . . ,𝜓𝑘 ) be a tuple of 𝑘 propositional formulas, and assume that, for each 𝑖 ∈ {1, . . . , 𝑘 }, the decision tree T𝜓𝑖 Í has dimension 𝑛𝑖 . Then a decision tree T of dimension 𝑑 = 𝑘 + 𝑘ℓ=1 𝑛 ℓ is defined as follows:
22
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
1
1
T𝜓1
0 1
2
T𝜓2
0 3
1
0 ···
T𝜓3
0 𝑘 1
0
T𝜓𝑘
true
where, for each 𝑖 ∈ {1, . . . , 𝑘 }, T𝜓𝑖 mentions the features: 𝐵𝑖 := {𝑠𝑖 + 1, 𝑠𝑖 + 2, . . . 𝑠𝑖 + 𝑛𝑖 }
where 𝑠𝑖 = 𝑘 +
𝑖 −1 ∑︁
𝑛ℓ .
ℓ=1
This way, we ensure that, for every 𝑖 ≠ 𝑗, T𝜓𝑖 and T𝜓 𝑗 are defined over disjoint sets of features. Moreover, define the following partial instances of dimension 𝑑: • For each 𝑖 ∈ {1, . . . , 𝑘}, the partial instance e𝑖 is defined as {0}𝑖 −1 · {1} · {0}𝑘 −𝑖 · {⊥}𝑑 −𝑘 . • For each 𝑖 ∈ {1, . . . , 𝑘}, the partial instances e𝑖,1 and e𝑖,2 are defined as follows: – e𝑖,1 [𝑖] = e𝑖,2 [𝑖] = 1; – e𝑖,1 [ 𝑗] = e𝑖,2 [ 𝑗] = 0 for every 𝑗 ∈ {1, . . . , 𝑘 } \ {𝑖}; – e𝑖,1 [ 𝑗] = e𝜓𝑖 [ 𝑗 − 𝑠𝑖 ] for every 𝑗 ∈ 𝐵𝑖 ; – e𝑖,2 [ 𝑗] = e𝜓′ 𝑖 [ 𝑗 − 𝑠𝑖 ] for every 𝑗 ∈ 𝐵𝑖 ; – e𝑖,1 [ 𝑗] = 0 for every 𝑗 ∈ {𝑘 + 1, . . . , 𝑑 } \ 𝐵𝑖 ; – e𝑖,2 [ 𝑗] = ⊥ for every 𝑗 ∈ {𝑘 + 1, . . . , 𝑑 } \ 𝐵𝑖 . Moreover, consider the following ExplAIner formulas: rwAXp(𝑥, 𝑦, 𝑤)
:=
rmAXp(𝑥, 𝑦, 𝑤)
:=
𝑤 ⊆ 𝑥 ∧ 𝑤 ⊆ 𝑦 ∧ Full(𝑥) ∧ 𝑦 ⊆ 𝑥 ∧ (AllPos(𝑥) → AllPos(𝑦)) ∧ (AllNeg(𝑥) → AllNeg(𝑦)); rwAXp(𝑥, 𝑦, 𝑤) ∧ ¬∃𝑧 𝑤 ⊆ 𝑧 ∧ rwAXp(𝑥, 𝑧, 𝑤) ∧ 𝑧 ≺ 𝑦 .
These formulas should be interpreted as the usual predicates, but relativized to one branch of T . More concretely, the partial instance 𝑤 will serve to select in which of the branches T𝜓1 , T𝜓2 , . . . , T𝜓𝑘 we will look at. Notice that the decision tree T and the partial instances e1 , . . ., e𝑘 , e1,1 , e1,2 , . . ., e𝑘,1 , e𝑘,2 can be constructed in polynomial time in the size of (𝜓 1, . . . ,𝜓𝑘 ). Besides, from the definition of these elements, for every 𝑖 ∈ {1, . . . , 𝑘 } it holds that T𝜓𝑖 |= mAXp(e𝜓𝑖 , e𝜓′ 𝑖 )
⇐⇒
T |= rmAXp(e𝑖,1, e𝑖,2, e𝑖 ).
(4)
ExplAIner: A Declarative Query Language for Explaining Classification Models
23
Finally, let 𝜑𝑘 be the ExplAIner formula obtained by constructing the following sequences of formulas 𝛼 1, . . . , 𝛼𝑘 , and then defining 𝜑𝑘 (𝑥 1,1, 𝑥 1,2, 𝑥 1, . . . , 𝑥𝑘,1, 𝑥𝑘,2, 𝑥𝑘 ) := 𝛼𝑘 (𝑥 1,1, 𝑥 1,2, 𝑥 1, . . . , 𝑥𝑘,1, 𝑥𝑘,2, 𝑥𝑘 ): 𝛼1
:=
¬rmAXp(𝑥 1,1, 𝑥 1,2, 𝑥 1 );
𝛼 2ℓ
:=
(𝛼 2ℓ −1 ∧ rmAXp(𝑥 2ℓ,1, 𝑥 2ℓ,2, 𝑥 2ℓ ));
𝛼 2ℓ+1
:=
(𝛼 2ℓ ∨ ¬rmAXp(𝑥 2ℓ+1,1, 𝑥 2ℓ+1,2, 𝑥 2ℓ+1 )).
For example, we have that: 𝛼2
=
(¬rmAXp(𝑥 1,1, 𝑥 1,2, 𝑥 1 ) ∧ rmAXp(𝑥 2,1, 𝑥 2,2, 𝑥 2 ))
𝛼3
=
(¬rmAXp(𝑥 1,1, 𝑥 1,2, 𝑥 1 ) ∧ rmAXp(𝑥 2,1, 𝑥 2,2, 𝑥 2 )) ∨ ¬rmAXp(𝑥 3,1, 𝑥 3,2, 𝑥 3 )
Combining conditions (3) and (4) with the definition 𝜑𝑘 (𝑥 1,1, 𝑥 1,2, 𝑥 1, . . . , 𝑥𝑘,1, 𝑥𝑘,2, 𝑥𝑘 ), we conclude that (𝜓 1, . . . ,𝜓𝑘 ) ∈ SAT(𝑘) if and only if T |= 𝜑𝑘 (e1,1, e1,2, e1, . . . , e𝑘,1, e𝑘,2, e𝑘 ). Given that SAT(𝑘) is BH𝑘 -complete and that the decision tree T and the partial instances e1,1 , e1,2 , e1 , . . ., e𝑘,1 , e𝑘,2 , e𝑘 can be constructed in polynomial time in the size of (𝜓 1, . . . ,𝜓𝑘 ), we conclude that Eval(𝜑𝑘 , DTree) is BH𝑘 -hard. This completes the proof of the theorem. 4.4
□
On the expressiveness of ExplAIner
ExplAIner allows us to express in a simple way the basic notions of explainability studied in this paper. Moreover, its evaluation problem is tractable given access to SAT solvers. Figure 3 shows how all the queries defined in Section 2.2 can be expressed in the ExplAIner logic. Just for clarity we use unguarded universal quantifiers, which are not allowed according to the ExplAIner syntax, because in these cases they can be rewritten as negations of unguarded existential quantifiers, as we discussed in Section 4.3. We also make use of some auxiliary predicates defined in the appendix (refer to Section A.7). Probably the most complicated formula of this section is the one used to express the query of relevant feature RF(𝑥, 𝑦). The idea there is to guess a weak abductive explanation 𝑤 containing the assigned feature under consideration and verify that undefining the feature makes 𝑤 lose the property of weak abductiveness. In fact, suppose first that 𝑦 is indeed a relevant feature for 𝑥. Then some abductive explanation 𝑤 contains 𝑦. Because 𝑤 is minimal, undefining 𝑦 from 𝑤 cannot produce another weak abductive explanation, so the witness pair 𝑤, 𝑧 exists. Conversely, if 𝑦 is not a relevant feature for 𝑥, then it cannot be contained in any minimal abductive explanation for 𝑥. Assume toward a contradiction that there exist witnesses 𝑤 and 𝑧 for the formula, where 𝑤 is a weak abductive explanation containing 𝑦, 𝑧 is obtained from 𝑤 by undefining 𝑦, and 𝑧 is not a weak abductive explanation. Now let 𝑢 ⊆ 𝑤 be an abductive explanation. As 𝑦 is not relevant, 𝑢 cannot contain 𝑦, and therefore 𝑢 ⊆ 𝑧. Since every completion of 𝑧 is also a completion of 𝑢, it would follow that 𝑧 is a weak abductive explanation, a contradiction. Hence no such witness pair 𝑤, 𝑧 can exist. It should be noted that if C is a class of models such that Eval(AllPos(𝑥), C) ∈ P but Eval(AllNeg(𝑥), C) ∉ P (under standard complexity-theoretic assumptions), then we still have that the problem Eval(𝜓, C) is in the Boolean hierarchy for the ExplAIner formulas 𝜓 that do not mention the predicate AllNeg(𝑥). Hence, the evaluation problem for this restricted fragment is still in the Boolean hierarchy, thus satisfying our criteria for an interpretability logic. This is the case, for example, for CNF formulas, for which validity checks can be done in polynomial time but checking unsatisfiability is coNP-complete. In this case, we can still express queries such as minimum change required and maximum change allowed, since they can be expressed in ExplAIner without mentioning the predicate AllNeg(𝑥). Similarly, if C is a class of models such that Eval(AllNeg(𝑥), C) ∈ P but Eval(AllPos(𝑥), C) ∉ P (for example, DNF
24
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
wAXp(𝑥, 𝑦) = Full(𝑥) ∧ 𝑦 ⊆ 𝑥 ∧ (AllPos(𝑥) → AllPos(𝑦)) ∧ (AllNeg(𝑥) → AllNeg(𝑦)) AXp(𝑥, 𝑦) = wAXp(𝑥, 𝑦) ∧ ∀𝑧 [𝑧 ⊂ 𝑦 → ¬wAXp(𝑥, 𝑧)] mAXp(𝑥, 𝑦) = wAXp(𝑥, 𝑦) ∧ ∀𝑧 [𝑧 ≺ 𝑦 → ¬wAXp(𝑥, 𝑧)] wCXp(𝑥, 𝑦) = Full(𝑥) ∧ 𝑦 ⊆ 𝑥 ∧ (AllPos(𝑥) → ¬AllPos(𝑦)) ∧ (AllNeg(𝑥) → ¬AllNeg(𝑦)) CXp(𝑥, 𝑦) = wCXp(𝑥, 𝑦) ∧ ∀𝑧 [𝑦 ⊂ 𝑧 → ¬wCXp(𝑥, 𝑧)] mCXp(𝑥, 𝑦) = wCXp(𝑥, 𝑦) ∧ ∀𝑧 [𝑦 ≺ 𝑧 → ¬wCXp(𝑥, 𝑧)] MCR(𝑥, 𝑦) = Full(𝑥) ∧ Full(𝑦) ∧ ¬(AllPos(𝑥) ↔ AllPos(𝑦)) ∧ ∀𝑧 [Full(𝑧) ∧ ¬(AllPos(𝑥) ↔ AllPos(𝑧))] → LEH(𝑥, 𝑦, 𝑧)
MCA(𝑥, 𝑦) = Full(𝑥) ∧ Full(𝑦) ∧ (AllPos(𝑥) ↔ AllPos(𝑦)) ∧ ∀𝑧 [Full(𝑧) ∧ (AllPos(𝑥) ↔ AllPos(𝑧))] → LEH(𝑥, 𝑧, 𝑦)
NF(𝑥, 𝑦) = Single(𝑦) ∧ Full(𝑥) ∧ 𝑦 ⊆ 𝑥 ∧ ¬∃𝑧 [wAXp(𝑥, 𝑧) ∧ ¬(𝑦 ⊆ 𝑧)] RF(𝑥, 𝑦) = Single(𝑦) ∧ Full(𝑥) ∧ 𝑦 ⊆ 𝑥 ∧ ∃𝑤, 𝑧 [wAXp(𝑥, 𝑤) ∧ Add(𝑧, 𝑦, 𝑤) ∧ ¬wAXp(𝑥, 𝑧)] Fig. 3. Formulas that express all queries in Section 2.2 using ExplAIner.
formulas), then we still have that the evaluation problem is in the Boolean hierarchy for ExplAIner formulas 𝜓 that do not mention the predicate AllPos(𝑥). Despite all the virtues of ExplAIner, unfortunately it is in general not able to solve computation problems efficiently. In fact, note that the ability to tractably evaluate queries over concrete partial instances does not directly imply that positive answers to the query can be constructed efficiently. We devote the rest of the paper to addressing this problem and propose a third logic that resolves it. 5
Opt-FOIL: computing explanations efficiently
Given an ExplAIner formula 𝜑 (𝑥, 𝑢 1, . . . , 𝑢𝑘 ), we use the notation 𝜑 [𝑢 1, . . . , 𝑢𝑘 ] (𝑥) to indicate that 𝑥 is a distinguished variable and 𝑢 1, . . . , 𝑢𝑘 are parameters that define the possible values for 𝑥. In general, we use this syntax when 𝑥 stores an explanation given an assignment for the variables 𝑢 1 , . . ., 𝑢 ℓ . For example, we write 𝜑 [𝑢] (𝑥) = AXp(𝑢, 𝑥) to indicate that 𝑥 is an abductive explanation given an assignment for the variable 𝑢 (that is, 𝑥 is an abductive explanation for 𝑢). For each query 𝜑 [𝑥 1, . . . , 𝑥𝑘 ] (𝑥) in ExplAIner and C a class of models, we define the computation problem Comp(𝜑, C) as follows: Problem:
Comp(𝜑 [𝑥 1, . . . , 𝑥𝑘 ] (𝑥), C)
Input:
A model M ∈ C and partial instances e1, . . . , e𝑘
Output:
Partial instance e such that M |= 𝜑 [e1, . . . , e𝑘 ] (e), and No if no such partial instance exists
5.1
The computational drawback of ExplAIner
We proved in Section 4.3 that the ExplAIner logic admits tractable evaluations over adequate classes of models, which allows us to check if a partial instance is an answer for some explainability query. The next step in the study of
ExplAIner: A Declarative Query Language for Explaining Classification Models
25
ExplAIner is to establish the complexity of actually computing such answers. Unfortunately, the following result tells us that this problem cannot be solved with a polynomial number of calls to an NP oracle, showing an important limitation of ExplAIner. Theorem 5.1. There exists an ExplAIner formula 𝜑 [𝑦, 𝑧] (𝑥) such that Comp(𝜑 [𝑦, 𝑧] (𝑥), DTree) ∉ FPNP unless PH collapses to PNP . Proof. Consider the following ExplAIner formula: 𝜑 (𝑥, 𝑦, 𝑧) := MaxRel(𝑥, 𝑦) ∧ ¬∃𝑤 [MaxRel(𝑤, 𝑧) ∧ 𝑥 ⊆ 𝑤 ∧ AllNeg(𝑤)], where MaxRel(𝑥, 𝑦), defined during the proof of Theorem 3.4, is a formula from the atomic layer of ExplAIner such ′ , i.e., the sets of undefined features in e and e′ are the same. Now consider that M |= MaxRel(e, e′ ) if and only if e⊥ = e⊥
the formula 𝜑 (𝑦, 𝑧) := ∃𝑥 𝜑 (𝑥, 𝑦, 𝑧), which is a FOIL formula with predicates {⊆, ⪯, AllPos, AllNeg}. We will show that Eval(𝜑, DTree) is NPNP -hard by a Karp reduction from the following well-known NPNP -complete problem (see [7] for a reference): given a propositional formula 𝛼 (p, q) in DNF, where p and q are sets of variables, decide if the quantified propositional formula ∃p∀q 𝛼 (p, q) is true. We will describe a polynomial-time reduction that constructs a decision tree T𝛼 and partial instances e𝛼 , e𝛼′ such that ∃p∀q 𝛼 (p, q) is true if and only if T𝛼 |= 𝜑 (e𝛼 , e𝛼′ ). Let 𝑛 be the number of terms in 𝛼. We construct a decision tree T𝛼 of dimension 𝑛 + |p| + |q|. We partition the features of T𝛼 into three consecutive blocks 𝐻 , 𝐸 and 𝑈 , where |𝐻 | = 𝑛, |𝐸| = |p|, and |𝑈 | = |q|. The block 𝐻 will be used to select a term from 𝛼, while 𝐸 and 𝑈 will encode truth assignments to the existential p and to the universal variables q, respectively.
Fig. 4. Construction used in the proof of Theorem 5.1. On the left, the decision tree T𝛼 . On the right, the gadget for the term o ∧ p ∧ ¬q.
For every term ℎ𝑟 (1 ≤ 𝑟 ≤ 𝑛) we construct a decision tree 𝐶𝑟 over 𝐸 and 𝑈 features in such a way that an input to that tree encoding a truth assignment reaches a true leaf if and only if the term ℎ𝑟 evaluated over that assignment is true. We now explain how to construct T𝛼 . We use the feature corresponding to term ℎ 1 as the root. For every 𝑖 < 𝑛, the outgoing edge of ℎ𝑖 labeled by 1 is connected to ℎ𝑖+1 , and the outgoing edge of ℎ𝑛 labeled by 1 is connected to a
26
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
false leaf. Also, for every 𝑖, we connect the outgoing edge labeled by 0 of ℎ𝑖 to a copy of the tree 𝐶𝑖 . An example is shown in Figure 4. Set e𝛼 = {⊥}𝑛 · {0} |p| · {⊥} |q| and e𝛼′ = {⊥}𝑛 · {0} |p|+|q| . We now show that the reduction is correct. First suppose that ∃p∀q 𝛼 (p, q) is true. Let 𝜈 be a truth assignment for the variables p such that for every truth assignment 𝜎 for the variables q it holds that 𝛼 (𝜈 (p), 𝜎 (q)) is true. Let e𝛼′′ be a partial instance with just its 𝐸 features defined according to 𝜈. Notice that e𝛼′′ and e𝛼 have the same defined features. We claim that 𝜑 (e𝛼′′, e𝛼 , e𝛼′ ). In fact, let e𝛼′′′ be a partial instance with the same defined features as e𝛼′ and such that e𝛼′′ ⊆ e𝛼′′′ . Notice that e𝛼′′′ naturally encodes a truth assignment 𝜎 for the variables q together with 𝜈. By taking a completion of e𝛼′′′ that has a 0 in the feature corresponding to a true term under the truth assignment (𝜈, 𝜎) and a 1 in the features corresponding to all previous terms, we can see that ¬AllNeg(e𝛼′′′ ). This shows that 𝜑 (e𝛼′′, e𝛼 , e𝛼′ ), and therefore T𝛼 |= 𝜑 (e𝛼 , e𝛼′ ). Now suppose that T𝛼 |= 𝜑 (e𝛼 , e𝛼′ ), so that there exists a partial instance e𝛼′′ such that 𝜑 (e𝛼′′, e𝛼 , e𝛼′ ). Because e𝛼′′ has the same defined features as e𝛼 , we can define a truth assignment 𝜈 for the variables p according to e𝛼′′ . Now let 𝜎 be any truth assignment for the variables q. We claim that 𝛼 (𝜈 (p), 𝜎 (q)) is true. In fact, let e𝛼′′′ be the partial instance with the same defined features as e𝛼′ and which corresponds to the pair (𝜈, 𝜎). Because we have that 𝜑 (e𝛼′′, e𝛼 , e𝛼′ ), it must be the case that ¬AllNeg(e𝛼′′′ ). That means that there exists a completion of e𝛼′′′ that is evaluated as true by T𝛼 . That necessarily means that there is a term in 𝛼 (𝜈 (p), 𝜎 (q)) that is being satisfied. Hence ∃p∀q 𝛼 (p, q) is true. This reduction shows that Eval(𝜑, DTree) is NPNP -hard. To conclude the proof of the theorem, assume for the sake of contradiction that Comp(𝜑 [𝑦, 𝑧] (𝑥), DTree) ∈ FPNP . Then, it is clear that we would have Eval(𝜑, DTree) ∈ PNP . Finally, PNP = NPNP implies that PH = PNP . □
To solve the problem that Theorem 5.1 signifies, we now propose Opt-FOIL, a logic that is defined by introducing a minimality operator over a subset of ExplAIner. As we will show in the next section, Opt-FOIL meets all the criteria for an appropriate interpretability logic. 5.2
The Opt-FOIL logic
Our aim is to capture the right subset of ExplAIner that meets all the criteria for an interpretability logic. For this, we will define a third logic called Opt-FOIL. We will show that the computation problem for this logic can be solved in polynomial time with a polynomial number of calls to an NP oracle. We will say that a formula 𝜌 (𝑥, 𝑦, 𝑣 1, . . . , 𝑣 ℓ ) from the atomic layer of ExplAIner represents a strict partial order if, for every natural number 𝑛 and assignment of partial instances of dimension 𝑛 to the variables 𝑣 1 , . . ., 𝑣 ℓ , the resulting binary relation over the variables 𝑥 and 𝑦 is a strict partial order over the partial instances of dimension 𝑛. Formally, 𝜌 (𝑥, 𝑦, 𝑣 1, . . . , 𝑣 ℓ ) represents a strict partial order if, for every 𝑛 ∈ N, 𝔅𝑛 |= ∀𝑣 1 · · · ∀𝑣 ℓ ∀𝑥 ¬𝜌 (𝑥, 𝑥, 𝑣 1, . . . , 𝑣 ℓ ) ∧ ∀𝑥∀𝑦∀𝑧 (𝜌 (𝑥, 𝑦, 𝑣 1, . . . , 𝑣 ℓ ) ∧ 𝜌 (𝑦, 𝑧, 𝑣 1, . . . , 𝑣 ℓ )) → 𝜌 (𝑥, 𝑧, 𝑣 1, . . . , 𝑣 ℓ ) . The variables 𝑣 1 , . . ., 𝑣 ℓ in the formula 𝜌 (𝑥, 𝑦, 𝑣 1, . . . , 𝑣 ℓ ) are considered as parameters that define a strict partial order. In fact, different assignments for these variables can give rise to different orders. Hence, we use the notation 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦) to make explicit the distinction between the parameters 𝑣 1 , . . ., 𝑣 ℓ and the variables 𝑥, 𝑦 that are instantiated with partial instances. For example, the strict partial order determined by the subsumption relation is defined by the formula 𝜌 1 (𝑥, 𝑦) = 𝑥 ⊂ 𝑦.
ExplAIner: A Declarative Query Language for Explaining Classification Models
27
As a second example, consider the case where a certain feature must be disregarded when defining an order on partial instances (for instance, it is often undesirable to use the feature gender for comparisons). Such an order can be defined as follows. Notice that, with the appropriate values for the variables 𝑣 1 and 𝑣 2 , the following formula checks whether the 𝑖-th feature of 𝑥 is undefined: UF(𝑥, 𝑣 1, 𝑣 2 ) := ¬(𝑣 1 ⊆ 𝑥) ∧ ¬(𝑣 2 ⊆ 𝑥). For example, if we are considering partial instances of dimension 5 and we need to check whether instance 𝑥 has value ⊥ in the first feature, then we can use the values 𝑐 1 = (0, ⊥, ⊥, ⊥, ⊥) and 𝑐 2 = (1, ⊥, ⊥, ⊥, ⊥) for the variables 𝑣 1 and 𝑣 2 , respectively. Moreover, let Pr(𝑥, 𝑦) := 𝑥 ⊂ 𝑦 ∧ ¬∃𝑧 (𝑥 ⊂ 𝑧 ∧ 𝑧 ⊂ 𝑦) be a formula that checks whether 𝑥 is a predecessor of 𝑦 under the order ⊂. Now define Strip[𝑣 1, 𝑣 2 ] (𝑥, 𝑦) := (UF(𝑥, 𝑣 1, 𝑣 2 ) ∧ 𝑥 = 𝑦) ∨ (¬UF(𝑥, 𝑣 1, 𝑣 2 ) ∧ Pr(𝑦, 𝑥) ∧ UF(𝑦, 𝑣 1, 𝑣 2 )). Notice that, with the appropriate values for 𝑣 1 and 𝑣 2 , Strip[𝑣 1, 𝑣 2 ] (𝑥, 𝑦) holds if and only if 𝑦 is obtained from 𝑥 by undefining the distinguished feature when necessary. Then, the following formula defines a strict partial order based on ⊂ but that disregards the 𝑖-th feature when comparing partial instances: 𝜌 2 [𝑣 1, 𝑣 2 ] (𝑥, 𝑦) := ∃𝑥 ′ ∃𝑦 ′ Strip[𝑣 1, 𝑣 2 ] (𝑥, 𝑥 ′ ) ∧ Strip[𝑣 1, 𝑣 2 ] (𝑦, 𝑦 ′ ) ∧ 𝑥 ′ ⊂ 𝑦 ′ . For example, 𝜌 2 [𝑐 1, 𝑐 2 ] (𝑥, 𝑦) with constants 𝑐 1 and 𝑐 2 mentioned above defines a strict partial order that disregards the first feature when comparing partial instances of dimension 5. Formulas from the atomic layer of ExplAIner representing strict partial orders will be used in the definition of Opt-FOIL. Hence, it is necessary to have an algorithm that verifies whether this condition is satisfied in order to have a decidable syntax for Opt-FOIL. We will now prove that such an algorithm exists. Proposition 5.2. The problem of verifying, given a formula 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦) from the atomic layer of ExplAIner, wd(𝜌 ) poly |𝜌 |·3wd(𝜌 )
whether it represents a strict partial order can be solved in 22
space, and, hence, in 22
2
poly |𝜌 |·3
time.
Proof. Let 𝜌 (𝑥, 𝑦, 𝑣 1, . . . , 𝑣 ℓ ) be an arbitrary formula from the atomic layer of ExplAIner, that is, a formula over the vocabulary {⊆, ⪯}. Then, we consider the following sentence: 𝜑 := ∀𝑣 1 · · · ∀𝑣 ℓ ∀𝑥 ¬𝜌 (𝑥, 𝑥, 𝑣 1, . . . , 𝑣 ℓ ) ∧ ∀𝑥∀𝑦∀𝑧 (𝜌 (𝑥, 𝑦, 𝑣 1, . . . , 𝑣 ℓ ) ∧ 𝜌 (𝑦, 𝑧, 𝑣 1, . . . , 𝑣 ℓ )) → 𝜌 (𝑥, 𝑧, 𝑣 1, . . . , 𝑣 ℓ ) . Notice that 𝜑 has width wd(𝜑) ≤ wd(𝜌) + 1. By definition, determining if 𝜌 corresponds to a strict partial order is equivalent to checking if for every structure 𝔅𝑛 it holds that 𝔅𝑛 |= 𝜑. Thanks to the second part of Theorem 4.3, we know that this can be done in the stated space. □ Proposition 5.2 serves as a theoretical upper bound to prove that Opt-FOIL has a decidable syntax. Observe that if we restrict ourselves to formulas of bounded width, then the space complexity falls from triple exponential to double exponential in |𝜌 | (which implies that the time complexity is triple exponential in |𝜌 |). In practice, we expect formulas representing strict partial orders to be small and to have a simple structure, so we do not expect this theoretical high computational complexity to pose an actual implementation obstacle. We now explain how strict partial orders will be used in the logic Opt-FOIL.
28
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux Given a formula 𝜑 [𝑢 1, . . . , 𝑢𝑘 ] (𝑥) from the quantified layer of ExplAIner and another formula 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑦, 𝑧)
from the atomic layer of ExplAIner that represents a strict partial order, an Opt-FOIL formula is an expression of the following form: Ψ[𝑢 1, . . . , 𝑢𝑘 , 𝑣 1, . . . , 𝑣 ℓ ] (𝑥) = min[𝜑 [𝑢 1, . . . , 𝑢𝑘 ] (𝑥), 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑦, 𝑧)]. Notice that 𝑥, 𝑢 1, . . . , 𝑢𝑘 , 𝑣 1, . . . , 𝑣 ℓ are the free variables of this expression, while the variables 𝑦, 𝑧 will be quantified. In particular, 𝑢 1, . . . , 𝑢𝑘 are the parameters that define the notion of explanation, 𝑣 1, . . . , 𝑣 ℓ are the parameters that define the strict partial order, and 𝑥 is a variable used to store an explanation that is minimal in the sense given by the strict partial order. The semantics of Ψ[𝑢 1, . . . , 𝑢𝑘 , 𝑣 1, . . . , 𝑣 ℓ ] (𝑥) is defined by considering the following ExplAIner formula: 𝜃 min (𝑥, 𝑢 1, . . . , 𝑢𝑘 , 𝑣 1, . . . , 𝑣 ℓ ) := 𝜑 (𝑥, 𝑢 1, . . . , 𝑢𝑘 ) ∧ ¬∃𝑦 𝜑 (𝑦, 𝑢 1, . . . , 𝑢𝑘 ) ∧ 𝜌 (𝑦, 𝑥, 𝑣 1, . . . , 𝑣 ℓ ) . More precisely, given a model M of dimension 𝑛 and partial instances e, e1′ , . . . , e𝑘′ , e1′′, . . . , eℓ′′ of dimension 𝑛, we define that M |= Ψ[e1′ , . . . , e𝑘′ , e1′′, . . . , eℓ′′ ] (e) if and only if M |= 𝜃 min (e, e1′ , . . . , e𝑘′ , e1′′, . . . , eℓ′′ ). The computation problem for Opt-FOIL has to be defined considering the different roles of the variables in the formula Ψ[𝑢 1, . . . , 𝑢𝑘 , 𝑣 1, . . . , 𝑣 ℓ ] (𝑥). In particular, the parameters 𝑢 1, . . . , 𝑢𝑘 , 𝑣 1, . . . , 𝑣 ℓ should be given as input, while the value of 𝑥 is the explanation to be computed. The following definition takes these considerations into account. As usual, we write C to denote some class of models. Problem:
Comp(Ψ[𝑢 1, . . . , 𝑢𝑘 , 𝑣 1, . . . , 𝑣 ℓ ] (𝑥), C)
Input:
A model M ∈ C and partial instances e1′ , . . ., e𝑘′ , e1′′ , . . ., eℓ′′
Output:
Partial instance e such that M |= Ψ[e1′ , . . . , e𝑘′ , e1′′, . . . , eℓ′′ ] (e), and No if no such partial instance exists
We now show that Opt-FOIL fulfills our criteria by establishing that the computation problem for Opt-FOIL can be solved in polynomial time with a polynomial number of calls to an NP oracle: Theorem 5.3. Let C be a class of models such that Eval(AllPos(𝑥), C) ∈ P and Eval(AllNeg(𝑥), C) ∈ P. Then Comp(Ψ, C) ∈ FPNP for every formula Ψ in Opt-FOIL. As a corollary of this result, we obtain that Opt-FOIL can be used to compute explanations in polynomial time using a polynomial number of calls to an NP oracle for the class of decision trees. Moreover, the same holds for more expressive representation classes, including d-DNNF circuits and fragments of the class of circuits corresponding to propositional formulas in conjunctive normal form (CNF) whose satisfiability is decidable in polynomial time, such as 2-CNF formulas (2CNF) and Horn CNF formulas (HORN). We formally state these results in the following corollary. Corollary 5.4. Let 𝜑 be an Opt-FOIL formula. Then Comp(𝜑, d-DNNF) ∈ FPNP , Comp(𝜑, 2CNF) ∈ FPNP , and Comp(𝜑, HORN) ∈ FPNP . Proof of Theorem 5.3. Let 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦) be a formula from the atomic layer of ExplAIner that represents a strict partial order. We say that a sequence (e1, . . . , e𝑘 ) of partial instances of dimension 𝑛 is a path of dimension 𝑛 in 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦) if there exist partial instances e1′ , . . ., eℓ′ of dimension 𝑛 such that, for every 𝑖 ∈ {1, . . . , 𝑘 − 1}, it holds that 𝔅𝑛 |= 𝜌 [e1′ , . . . , eℓ′ ] (e𝑖 , e𝑖+1 ). The following lemma shows that, for a fixed formula 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦), the lengths of such paths are polynomially bounded with respect to 𝑛 (refer to Section A.6 for the proof).
ExplAIner: A Declarative Query Language for Explaining Classification Models
29
Lemma 5.5. Let 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦) be a formula from the atomic layer of ExplAIner that represents a strict partial order. Then there exists a fixed polynomial 𝑝 such that for every path (e1, . . . , e𝑘 ) of dimension 𝑛 in 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦), it holds that 𝑘 ≤ 𝑝 (𝑛). Lemma 5.5 gives us a simple algorithm to compute a solution for an Opt-FOIL formula min[𝜑 [𝑢 1, . . . , 𝑢𝑘 ] (𝑥), 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑦, 𝑧)], given as input a model M ∈ C of dimension 𝑛 and partial instances e1′ , . . ., e𝑘′ , e1′′ , . . ., eℓ′′ of dimension 𝑛. We first use an NP oracle to verify whether M |= ∃𝑥 𝜑 [e1′ , . . . , e𝑘′ ] (𝑥), which is a formula from the quantified layer of ExplAIner. If M ̸ |= ∃𝑥 𝜑 [e1′ , . . . , e𝑘′ ] (𝑥), then the answer is No. Otherwise, the NP oracle can be used to construct an initial partial instance e0 such that M |= 𝜑 [e1′ , . . . , e𝑘′ ] (e0 ). The idea is to maintain a current partial assignment e′′ (originally set to {⊥}𝑛 ) of the features that is known to extend to some witness. For each feature, we query whether there exists a witness extending e′′ but with that feature fixed to 0. If the answer is positive, we keep that feature as 0 in e′′ , otherwise we query whether there exists one extending e′′ but with that feature fixed to 1. If that answer is positive, we keep that feature as 1, and if both answers are negative, then we leave the feature undefined. This way, the invariant is preserved at every step, and after at most 2𝑛 oracle queries we obtain the partial instance e0 . We then use the NP oracle to verify whether M |= ∃𝑥 𝜑 [e1′ , . . . , e𝑘′ ] (𝑥) ∧ 𝜌 [e1′′, . . . , eℓ′′ ] (𝑥, e0 ) ; which can be written as a formula from the quantified layer of ExplAIner by appending ‘∧ 𝜌 [e1′′, . . . , eℓ′′ ] (𝑥, e0 )’ within all the quantifiers of 𝜑 [e1′ , . . . , e𝑘′ ] (𝑥). If the answer is positive, then again we use the NP oracle as described before to construct a partial instance e1 such that M |= 𝜑 [e1′ , . . . , e𝑘′ ] (e1 ) ∧ 𝜌 [e1′′, . . . , eℓ′′ ] (e1, e0 ). The algorithm continues in this way, constructing a sequence of partial instances (e𝑖 , e𝑖 −1, . . . , e0 ) that constitutes a path of dimension 𝑛 in 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑦, 𝑧). The algorithm stops when the condition M |= ∃𝑥 𝜑 [e1′ , . . . , e𝑘′ ] (𝑥) ∧ 𝜌 [e1′′, . . . , eℓ′′ ] (𝑥, e𝑖 )
does not hold, which by construction guarantees that e𝑖 is a minimal instance. Lemma 5.5 guarantees that e𝑖 will be found in a polynomial number of steps. Since in each step we call the NP oracle a polynomial number of times, this concludes the proof of the theorem.
□
We now begin the study of the expressiveness of Opt-FOIL. As is customary, we say that a logic L1 is contained in a logic L2 if for every formula in L1 there exists an equivalent formula in L2 . Moreover, L1 is properly contained in L2 if L1 is contained in L2 and L2 is not contained in L1 . The following proposition shows that the expressive power of Opt-FOIL is less than that of ExplAIner, which in turn has less expressive power than FOIL with predicates {⊆, ⪯, AllPos, AllNeg}. Proposition 5.6. Assuming that the polynomial hierarchy does not collapse, Opt-FOIL is strictly contained in ExplAIner, and ExplAIner is strictly contained in FOIL with extended predicates. Proof. For the first containment, let Ψ[𝑢 1, . . . , 𝑢𝑘 , 𝑣 1, . . . , 𝑣 ℓ ] (𝑥) = min[𝜑 [𝑢 1, . . . , 𝑢𝑘 ] (𝑥), 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑦, 𝑧)]
30
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
be an Opt-FOIL formula. As we discussed before, we can consider the equivalent ExplAIner formula 𝜃 min (𝑥, 𝑢 1, . . . , 𝑢𝑘 , 𝑣 1, . . . , 𝑣 ℓ ). Now, for the sake of contradiction, suppose that the containment is not strict. Let 𝜑 [𝑦, 𝑧] (𝑥) be an ExplAIner formula such that Comp(𝜑 [𝑦, 𝑧] (𝑥), DTree) ∉ FPNP unless PH collapses to PNP (whose existence is guaranteed by Theorem 5.1). Let Ψ[𝑦, 𝑧] (𝑥) be its equivalent expression in Opt-FOIL. By Theorem 5.3, the problem Comp(Ψ[𝑦, 𝑧] (𝑥), DTree) is in FPNP . Thus, Comp(𝜑 [𝑦, 𝑧] (𝑥), DTree) can be solved in FPNP . This would imply the collapse of the polynomial hierarchy to PNP . We conclude that the containment is strict. For the second containment, each formula in ExplAIner is a FOIL formula with extended predicates by definition. It is strict because we can express ΣP2 -hard problems in FOIL over decision trees (Theorem 3.4), but no ExplAIner formula can express a ΣP2 -hard evaluation problem over decision trees unless ΣP2 ⊆ BH (Theorem 4.7).
□
The logic Opt-FOIL allows us to express in a simple way all notions of explainability that we study in this paper. For example, recall from Section 4.2 that wAXp(𝑢, 𝑥) can be expressed as a formula from the quantified layer of ExplAIner. Therefore, taking 𝜑 [𝑢] (𝑥) = wAXp(𝑢, 𝑥), the following Opt-FOIL formulas encode the notions of minimal and minimum abductive explanations: AXp[𝑢] (𝑥)
=
min[𝜑 [𝑢] (𝑥), 𝑦 ⊂ 𝑧],
mAXp[𝑢] (𝑥)
=
min[𝜑 [𝑢] (𝑥), 𝑦 ≺ 𝑧].
Likewise, min[𝜑 [𝑢] (𝑥), 𝜌 2 [𝑣 1, 𝑣 2 ] (𝑦, 𝑧)] encodes the notion of abductive explanations for the order 𝜌 2 [𝑣 1, 𝑣 2 ] (𝑦, 𝑧) that disregards a feature. The different variants of contrastive explanations can be expressed similarly. As a second example, consider the notion of minimum change required and the predicate LEH defined in Section A.7. Then, taking 𝜑 [𝑢] (𝑥) = Full(𝑢) ∧ Full(𝑥) ∧ ¬(AllPos(𝑢) ↔ AllPos(𝑥)) and 𝜌 3 [𝑢] (𝑦, 𝑧) = LEH(𝑢, 𝑦, 𝑧) ∧ ¬LEH(𝑢, 𝑧, 𝑦), we can express the notion of minimum change required in Opt-FOIL as follows: MCR[𝑢] (𝑥) = min[𝜑 [𝑢] (𝑥), 𝜌 3 [𝑢] (𝑦, 𝑧)]. By reversing the order, the logic Opt-FOIL can also be used to express notions of explainability that involve maximality conditions. For example, consider the query of maximum change allowed that asks for the maximum number of changes that can be made to an instance without changing the output of the classification model. Taking 𝜑 [𝑢] (𝑥) = Full(𝑢) ∧ Full(𝑥) ∧ (AllPos(𝑢) ↔ AllPos(𝑥)) and defining the reverse order 𝜌 4 [𝑢] (𝑦, 𝑧) = 𝜌 3 [𝑢] (𝑧, 𝑦), we can express the notion of maximum change allowed in Opt-FOIL as follows: MCA[𝑢] (𝑥) = min[𝜑 [𝑢] (𝑥), 𝜌 4 [𝑢] (𝑦, 𝑧)]. An important advantage of Opt-FOIL is that it allows for the combination of explainability notions. For example, given two instances 𝑢 1 and 𝑢 2 of the same dimension, consider the query CAXp[𝑢 1, 𝑢 2 ] (𝑥) = wAXp(𝑢 1, 𝑥) ∧ wAXp(𝑢 2, 𝑥) that checks whether 𝑥 is a common weak abductive explanation for 𝑢 1 and 𝑢 2 . Then the following Opt-FOIL formula
ExplAIner: A Declarative Query Language for Explaining Classification Models
31
computes a common weak abductive explanation for two instances (if such an explanation exists): Ψ1 [𝑢 1, 𝑢 2 ] (𝑥) = min[CAXp[𝑢 1, 𝑢 2 ] (𝑥), 𝑦 ⊂ 𝑧]. Note that an answer to this query is not necessarily minimal with respect to all weak abductive explanations for either 𝑢 1 or 𝑢 2 . Finally, another advantage of Opt-FOIL is that it allows for the exploration of the space of explanations for a given classification. For example, assume that we already have an abductive explanation 𝑢 1 for an instance 𝑢, which can be computed using the Opt-FOIL formula AXp[𝑢] (𝑥). Our aim is to compute a second abductive explanation 𝑢 2 for 𝑢. Consider the formula: SAXp[𝑢, 𝑢 1 ] (𝑥) = wAXp(𝑢, 𝑥) ∧ wAXp(𝑢, 𝑢 1 ) ∧ ¬(𝑢 1 ⊆ 𝑥). This formula checks whether 𝑥 is a weak abductive explanation for 𝑢 that does not subsume the abductive explanation 𝑢 1 . Thus, an abductive explanation for the instance 𝑢 that is different from 𝑢 1 can be computed using the following Opt-FOIL formula: Ψ2 [𝑢, 𝑢 1 ] (𝑥) = min[SAXp[𝑢, 𝑢 1 ] (𝑥), 𝑦 ⊂ 𝑧]. We can apply the same idea to other notions of explanation, such as the MCR explainability query, in order to compute multiple explanations for the output of a classification model. 6
Concluding remarks and future work
We have proposed a declarative approach to model interpretability based on query languages for explaining Boolean classification models. The starting point of our work is the observation that the growing number of explanation notions studied in formal XAI calls for a uniform language in which such notions can be specified, combined, and analyzed. This view is natural from a data management perspective: explanation notions become queries, models become the structures over which these queries are evaluated, and the main questions are those of expressiveness, evaluation complexity, and computation of answers. Our first contribution was to revisit FOIL from this perspective. We showed that, despite its foundational role, FOIL is not well suited as a practical query language for explanations. On the one hand, it cannot express some central optimality-based notions, such as minimum abductive explanations, even over decision trees. On the other hand, its evaluation problem over decision trees is hard for every level of the polynomial hierarchy. These results show that a useful explainability language must carefully balance expressive power with controlled evaluation complexity. To address this challenge, we introduced ExplAIner, a layered query language with an extended vocabulary for reasoning about partial instances and the behavior of Boolean models. We showed that ExplAIner can express a broad family of explanation notions, including abductive, contrastive, feature-based, and distance-based queries. At the same time, we proved that the evaluation problem for each fixed ExplAIner query belongs to the Boolean hierarchy over every class of Boolean models for which the predicates AllPos and AllNeg can be evaluated in polynomial time. This condition holds not only for decision trees, but also for more general representation classes such as deterministic and decomposable Boolean circuits. We also introduced Opt-FOIL, an optimization-oriented fragment of ExplAIner for computing explanations that are minimal with respect to strict partial orders. This fragment captures a wide range of optimality-based explanation tasks while retaining controlled computational behavior: under the same assumptions on AllPos and AllNeg, explanations
32
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
specified in Opt-FOIL can be computed in FPNP . Together, the results for ExplAIner and Opt-FOIL show that declarative specification and complexity-theoretic analysis can provide a principled foundation for model interpretability. Several directions remain open. A first direction is to extend the framework beyond Boolean classification models. Although Boolean models are standard in formal XAI and already capture many explanation tasks, many applications involve multi-class outputs, non-Boolean features, or structured feature domains. It would be interesting to understand which parts of the present framework extend directly to these richer settings, and which additional predicates or language constructs are needed. A second direction is to study further model representations. Our upper bounds are stated for every class of Boolean models over which AllPos and AllNeg can be evaluated in polynomial time, and this already includes decision trees and deterministic decomposable Boolean circuits. A natural next step is to identify additional representation classes that satisfy this condition. This would help clarify the connection between explainability languages and knowledge compilation more broadly. A third direction concerns query optimization. One of the motivations for a declarative language is that different explanation notions can share common subqueries and operators. This suggests the possibility of developing optimization techniques for explainability queries, in the same spirit as query optimization in databases. Such techniques could exploit common subformulas, reuse calls to procedures for AllPos and AllNeg, or identify fragments with better evaluation strategies. Finally, it would be valuable to study richer answer mechanisms for explainability queries. In this paper, explanations are treated as partial instances satisfying a logical specification, possibly optimized with respect to a strict partial order. However, users may require different levels of detail, multiple alternative explanations, or rankings of explanations according to several criteria. Extending the language with principled mechanisms for enumeration, ranking, and comparison of explanations is an important step toward a more complete declarative framework for model interpretability. 7
Acknowledgements
Part of this work has been funded by ANID - Millennium Science Initiative Program - Code ICN17002. Diego Bustamante was partially funded by ANID - Subdirección de Capital Humano (Magíster Nacional, 2023, folio 22231282). María Alejandra Schild was financially supported by ANID (Doctorado Nacional, 2025, folio 21251617). Bernardo Subercaseaux is (partially) supported by the DARPA expMath program through the DARPA CMO contract number HR0011262E028. References [1] Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of Databases. Addison-Wesley. [2] Gianvincenzo Alfano, Sergio Greco, Domenico Mandaglio, Francesco Parisi, Reza Shahbazian, and Irina Trubitsyna. 2024. Even-if Explanations: Formal Foundations, Priorities and Complexity. arXiv:2401.10938 [cs.AI] [3] Marcelo Arenas. 2024. A Data Management Approach to Explainable AI. In Companion of the 43rd Symposium on Principles of Database Systems (PODS Companion ’24). ACM, 1–3. doi:10.1145/3635138.3654762 [4] Marcelo Arenas, Daniel Baez, Pablo Barceló, Jorge Pérez, and Bernardo Subercaseaux. 2021. Foundations of Symbolic Languages for Model Interpretability. In NeurIPS 2021. 11690–11701. [5] Marcelo Arenas, Pablo Barceló, Leopoldo E. Bertossi, and Mikaël Monet. 2021. The Tractability of SHAP-Score-Based Explanations for Classification over Deterministic and Decomposable Boolean Circuits. In AAAI. 6670–6678. [6] Marcelo Arenas, Pablo Barceló, Diego Bustamante, Jose Caraball, and Bernardo Subercaseaux. 2024. A Uniform Language to Explain Decision Trees. In Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning. 60–70. doi:10.24963/kr.2024/6 [7] S. Arora and B. Barak. 2006. Computational Complexity: A Modern Approach. Cambridge University Press. https://theory.cs.princeton.edu/ complexity/book.pdf
ExplAIner: A Declarative Query Language for Explaining Classification Models
33
[8] Alejandro Barredo Arrieta, Natalia Díaz Rodríguez, Javier Del Ser, Adrien Bennetot, Siham Tabik, Alberto Barbado, Salvador García, Sergio Gil-Lopez, Daniel Molina, Richard Benjamins, Raja Chatila, and Francisco Herrera. 2020. Explainable Artificial Intelligence (XAI): Concepts, taxonomies, opportunities and challenges toward responsible AI. Inf. Fusion 58 (2020), 82–115. [9] Gilles Audemard, Steve Bellart, Louenas Bounia, Frederic Koriche, Jean-Marie Lagniez, and Pierre Marquis. 2022. On Preferred Abductive Explanations for Decision Trees and Random Forests. In IJCAI, Lud De Raedt (Ed.). 643–650. doi:10.24963/ijcai.2022/91 [10] Gilles Audemard, Steve Bellart, Louenas Bounia, Frédéric Koriche, Jean-Marie Lagniez, and Pierre Marquis. 2022. On the Explanatory Power of Boolean Decision Trees. Data Knowl. Eng. 142, C (nov 2022), 17 pages. doi:10.1016/j.datak.2022.102088 [11] Pablo Barceló, Mikaël Monet, Jorge Pérez, and Bernardo Subercaseaux. 2020. Model Interpretability through the lens of Computational Complexity. In Advances in Neural Information Processing Systems, Vol. 33. 15487–15498. https://proceedings.neurips.cc/paper/2020/hash/ b1adda14824f50ef24ff1c05bb66faf3-Abstract.html [12] Leonard Berman. 1980. The complexity of logical theories. Theoret. Comput. Sci. 11, 1 (1980), 57, 71–77. doi:10.1016/0304-3975(80)90037-7 With an introduction “On space, time and alternation”. [13] Gianpiero Cabodi, Paolo E. Camurati, Joao Marques-Silva, Marco Palena, and Paolo Pasini. 2024. Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2024), 1–1. doi:10.1109/TCAD.2024.3387876 [14] Jin-yi Cai, Thomas Gundermann, Juris Hartmanis, Lane A. Hemachandra, Vivian Sewelson, Klaus W. Wagner, and Gerd Wechsung. 1988. The Boolean Hierarchy I: Structural Properties. SIAM J. Comput. 17, 6 (1988), 1232–1252. [15] Adnan Darwiche. 2023. Logic for Explainable AI. arXiv:2305.05172 [cs.AI] [16] Adnan Darwiche and Auguste Hirth. 2020. On the Reasons Behind Decisions.. In ECAI. 712–720. doi:10.3233/FAIA200158 [17] Adnan Darwiche and Pierre Marquis. 2011. A Knowledge Compilation Map. CoRR abs/1106.1819 (2011). arXiv:1106.1819 http://arxiv.org/abs/1106. 1819 [18] Finale Doshi-Velez and Been Kim. 2017. Towards A Rigorous Science of Interpretable Machine Learning. arXiv:1702.08608 [stat.ML] [19] Ding-Zhu Du and Ker-I Ko. 2014. Theory of computational complexity (second ed.). John Wiley & Sons, Inc., Hoboken, NJ. xvi+494 pages. doi:10.1002/9781118595091 [20] Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, and Scott Weinstein. 2007. Finite model theory and its applications. Springer, Berlin. xiv+437 pages. [21] Riccardo Guidotti, Anna Monreale, Salvatore Ruggieri, Franco Turini, Fosca Giannotti, and Dino Pedreschi. 2019. A Survey of Methods for Explaining Black Box Models. ACM Comput. Surv. 51, 5 (2019), 93:1–93:42. [22] David Gunning and David Aha. 2019. DARPA’s Explainable Artificial Intelligence (XAI) Program. AI Magazine 40, 2 (June 2019), 44–58. doi:10.1609/ aimag.v40i2.2850 [23] Xuanxiang Huang, Martin C. Cooper, António Morgado, Jordi Planes, and João Marques-Silva. 2023. Feature Necessity & Relevancy in ML Classifier Explanations.. In ETAPS. 167–186. doi:10.1007/978-3-031-30823-9_9 [24] Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, and João Marques-Silva. 2021. On Efficiently Explaining Graph-Based Classifiers. In KR, Meghyn Bienvenu, Gerhard Lakemeyer, and Esra Erdem (Eds.). 356–367. [25] Alexey Ignatiev, Nina Narodytska, and João Marques-Silva. 2019. Abduction-Based Explanations for Machine Learning Models. In AAAI. AAAI Press, 1511–1519. [26] Alexey Ignatiev and João P. Marques Silva. 2021. SAT-Based Rigorous Explanations for Decision Lists. In SAT (LNCS, Vol. 12831), Chu-Min Li and Felip Manyà (Eds.). Springer, 251–269. [27] Yacine Izza, Alexey Ignatiev, and João Marques-Silva. 2020. On Explaining Decision Trees. CoRR abs/2010.11034 (2020). [28] Yacine Izza, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, and J. Marques-Silva. 2021. Efficient Explanations With Relevant Sets. ArXiv abs/2106.00546 (2021). [29] Yacine Izza and João Marques-Silva. 2021. On Explaining Random Forests with SAT. In IJCAI, Zhi-Hua Zhou (Ed.). ijcai.org, 2584–2591. [30] Paris C. Kanellakis. 1990. Elements of Relational Database Theory. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B). 1073–1156. [31] Leonid Libkin. 2004. Elements of Finite Model Theory. Springer. [32] Felix Lindner and Katrin Möllney. 2019. Extracting Reasons for Moral Judgments Under Various Ethical Principles. 216–229. doi:10.1007/978-3-03030179-8_18 [33] Joao Marques-Silva. 2023. Logic-Based Explainability in Machine Learning. 24–104 pages. doi:10.1007/978-3-031-31414-8_2 [34] Joao Marques-Silva. 2024. Logic-Based Explainability: Past, Present and Future. In Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies: 12th International Symposium, ISoLA 2024, Crete, Greece, October 27–31, 2024, Proceedings, Part IV (Crete, Greece). Springer-Verlag, Berlin, Heidelberg, 181–204. doi:10.1007/978-3-031-75387-9_12 [35] Joao Marques-Silva and Alexey Ignatiev. 2023. No silver bullet: interpretable ML models must be explained. Frontiers in Artificial Intelligence 6 (Apr 2023), 1128212. doi:10.3389/frai.2023.1128212 [36] Pierre Marquis. 1991. Extending abduction from propositional to first-order logic. In Fundamentals of Artificial Intelligence Research, International Workshop FAIR ’91, Smolenice, Czechoslovakia, September 8-13, 1991, Proceedings (Lecture Notes in Computer Science, Vol. 535), Philippe Jorrand and Jozef Kelemen (Eds.). Springer, 141–155. doi:10.1007/3-540-54507-7_12
34
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
[37] Christoph Molnar. 2022. Interpretable Machine Learning (2 ed.). https://christophm.github.io/interpretable-ml-book [38] Christos H. Papadimitriou and Mihalis Yannakakis. 1999. On the Complexity of Database Queries. J. Comput. Syst. Sci. 58, 3 (1999), 407–427. [39] Mojżesz Presburger. 1991. On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation. Hist. Philos. Logic 12, 2 (1991), 225–233. doi:10.1080/014453409108837187 Translated from the German and with commentaries by Dale Jacquette. [40] Marco Túlio Ribeiro, Sameer Singh, and Carlos Guestrin. 2018. Anchors: High-Precision Model-Agnostic Explanations. In AAAI. 1527–1535. [41] Andy Shih, Arthur Choi, and Adnan Darwiche. 2018. A symbolic approach to explaining Bayesian network classifiers. arXiv preprint arXiv:1805.03364 (2018). [42] Moshe Y. Vardi. 1982. The Complexity of Relational Query Languages. In STOC. 137–146. [43] Stephan Wäldchen, Jan MacDonald, Sascha Hauch, and Gitta Kutyniok. 2021. The Computational Complexity of Understanding Binary Classifier Decisions. J. Artif. Intell. Res. 70 (2021), 351–387. [44] Gerd Wechsung. 1985. On the Boolean closure of NP. In Fundamentals of Computation Theory, FCT ’85 (Lecture Notes in Computer Science, Vol. 199). 485–493. [45] Jinqiang Yu, Alexey Ignatiev, Peter J. Stuckey, and Pierre Le Bodic. 2020. Computing Optimal Decision Sets with SAT. In CP (LNCS, Vol. 12333), Helmut Simonis (Ed.). Springer, 952–970.
ExplAIner: A Declarative Query Language for Explaining Classification Models A
Supplementary Material
A.1
Proof of Lemma 3.2
35
We will first prove an auxiliary result. We start by introducing some terminology. Let 𝑈 = {𝑎𝑖 | 𝑖 > 0} be a countably infinite set. We take a disjoint copy 𝑈 = {𝑎𝑖 | 𝑖 > 0} of 𝑈 . For an 𝑋 ⊆ 𝑈 ∪ 𝑈 , we define 𝑋𝑈 \𝑈 := {𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑋 and 𝑎 ∉ 𝑋 } 𝑋𝑈 ∩𝑈 := {𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑋 and 𝑎 ∈ 𝑋 } 𝑋𝑈 \𝑈 := {𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑋 and 𝑎 ∉ 𝑋 } The ℓ-type of 𝑋 , for ℓ ≥ 0, is the tuple min {ℓ, |𝑋𝑈 \𝑈 |}, min {ℓ, |𝑋𝑈 ∩𝑈 |}, min {ℓ, |𝑋𝑈 \𝑈 |} . We write 𝑋 ⇆ℓ 𝑋 ′ , for 𝑋, 𝑋 ′ ⊆ 𝑈 ∪ 𝑈 , if 𝑋 and 𝑋 ′ have the same ℓ-type. If 𝑋 ⊆ 𝑈 ∪ 𝑈 , then 𝑋 is well formed (wf) if for each 𝑖 > 0 at most one element from {𝑎𝑖 , 𝑎𝑖 } is in 𝑋 . Lemma A.1. Assume that 𝑋 ⇆3𝑘+1 𝑌 , for 𝑋, 𝑌 ⊆ 𝑈 ∪ 𝑈 and 𝑘 ≥ 0. Then: • For every wf 𝑋 1 ⊆ 𝑋 , there exists a wf 𝑌1 ⊆ 𝑌 such that 𝑋 1 ⇆3𝑘 𝑌1 and 𝑋 \ 𝑋 1 ⇆3𝑘 𝑌 \ 𝑌1 . • For every wf 𝑌1 ⊆ 𝑌 , there exists a wf 𝑋 1 ⊆ 𝑋 such that 𝑋 1 ⇆3𝑘 𝑌1 and 𝑋 \ 𝑋 1 ⇆3𝑘 𝑌 \ 𝑌1 . Proof. Given 𝑍 ⊆ 𝑈 , we use 𝑍 to denote the set {𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑍 }, and given 𝑊 ⊆ 𝑈 , we use 𝑊 to denote the set {𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑊 }. Let 𝑋 1 be a wf subset of 𝑋 . Then we have that 𝑋 1 = 𝑋 1,1 ∪ 𝑋 1,2 ∪ 𝑋 1,3 ∪ 𝑋 1,4 , where 𝑋 1,1
⊆
𝑋𝑈 \𝑈 ,
𝑋 1,2
⊆
{𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑋𝑈 ∩𝑈 },
𝑋 1,3
⊆
{𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑋𝑈 ∩𝑈 },
𝑋 1,4
⊆
𝑋𝑈 \𝑈 ,
and 𝑋 1,2 ∩ 𝑋 1,3 = ∅ (since 𝑋 1 is wf). We construct a set 𝑌1 = 𝑌1,1 ∪ 𝑌1,2 ∪ 𝑌1,3 ∪ 𝑌1,4 by considering the following rules. (1) If |𝑋𝑈 \𝑈 | < 3𝑘+1 , then |𝑌𝑈 \𝑈 | = |𝑋𝑈 \𝑈 | since 𝑋 ⇆3𝑘+1 𝑌 . In this case, we choose 𝑌1,1 ⊆ 𝑌𝑈 \𝑈 in such a way that |𝑌1,1 | = |𝑋 1,1 | and |𝑌𝑈 \𝑈 \ 𝑌1,1 | = |𝑋𝑈 \𝑈 \ 𝑋 1,1 |. If |𝑋𝑈 \𝑈 | ≥ 3𝑘+1 , then |𝑌𝑈 \𝑈 | ≥ 3𝑘+1 since 𝑋 ⇆3𝑘+1 𝑌 . In this case, we choose 𝑌1,1 ⊆ 𝑌𝑈 \𝑈 in the following way. If |𝑋 1,1 | < 3𝑘 , then |𝑌1,1 | = |𝑋 1,1 |, and if |𝑋𝑈 \𝑈 \ 𝑋 1,1 | < 3𝑘 , then |𝑌𝑈 \𝑈 \ 𝑌1,1 | = |𝑋𝑈 \𝑈 \ 𝑋 1,1 |. Finally, if |𝑋 1,1 | ≥ 3𝑘 and |𝑋𝑈 \𝑈 \ 𝑋 1,1 | ≥ 3𝑘 , then |𝑌1,1 | ≥ 3𝑘 and |𝑌𝑈 \𝑈 \ 𝑌1,1 | ≥ 3𝑘 . Notice that we can choose such a set 𝑌1,1 since |𝑌𝑈 \𝑈 | ≥ 3𝑘+1 . (2) If |𝑋𝑈 ∩𝑈 | < 3𝑘+1 , then |𝑌𝑈 ∩𝑈 | = |𝑋𝑈 ∩𝑈 | since 𝑋 ⇆3𝑘+1 𝑌 . In this case, we choose 𝑌1,2 ⊆ {𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑌𝑈 ∩𝑈 } and 𝑌1,3 ⊆ {𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑌𝑈 ∩𝑈 } in such a way that 𝑌1,2 ∩ 𝑌1,3 = ∅, |𝑌1,2 | = |𝑋 1,2 |, |𝑌1,3 | = |𝑋 1,3 | and |𝑌𝑈 ∩𝑈 \ (𝑌1,2 ∪ 𝑌1,3 )| = |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪ 𝑋 1,3 )|.
36
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux If |𝑋𝑈 ∩𝑈 | ≥ 3𝑘+1 , then |𝑌𝑈 ∩𝑈 | ≥ 3𝑘+1 since 𝑋 ⇆3𝑘+1 𝑌 . In this case, we choose 𝑌1,2 ⊆ {𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑌𝑈 ∩𝑈 } and 𝑌1,3 ⊆ {𝑎 ∈ 𝑈 | 𝑎 ∈ 𝑌𝑈 ∩𝑈 } in the following way. (a) If |𝑋 1,2 | < 3𝑘 , |𝑋 1,3 | < 3𝑘 and |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪𝑋 1,3 )| ≥ 3𝑘 , then |𝑌1,2 | = |𝑋 1,2 |, |𝑌1,3 | = |𝑋 1,3 | and 𝑌1,2 ∩𝑌1,3 = ∅. Notice that we can choose such sets 𝑌1,2 and 𝑌1,3 since |𝑌𝑈 ∩𝑈 | ≥ 3𝑘+1 . (b) If |𝑋 1,2 | < 3𝑘 , |𝑋 1,3 | ≥ 3𝑘 and |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪ 𝑋 1,3 )| < 3𝑘 , then |𝑌1,2 | = |𝑋 1,2 |, |𝑌𝑈 ∩𝑈 \ (𝑌1,2 ∪ 𝑌1,3 )| = |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪𝑋 1,3 )| and 𝑌1,2 ∩𝑌1,3 = ∅. Notice that we can choose such sets 𝑌1,2 and 𝑌1,3 since |𝑌𝑈 ∩𝑈 | ≥ 3𝑘+1 . (c) If |𝑋 1,2 | ≥ 3𝑘 , |𝑋 1,3 | < 3𝑘 and |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪ 𝑋 1,3 )| < 3𝑘 , then |𝑌1,3 | = |𝑋 1,3 |, |𝑌𝑈 ∩𝑈 \ (𝑌1,2 ∪ 𝑌1,3 )| = |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪𝑋 1,3 )| and 𝑌1,2 ∩𝑌1,3 = ∅. Notice that we can choose such sets 𝑌1,2 and 𝑌1,3 since |𝑌𝑈 ∩𝑈 | ≥ 3𝑘+1 . (d) If |𝑋 1,2 | < 3𝑘 , |𝑋 1,3 | ≥ 3𝑘 and |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪𝑋 1,3 )| ≥ 3𝑘 , then |𝑌1,2 | = |𝑋 1,2 |, |𝑌1,3 | ≥ 3𝑘 , |𝑌𝑈 ∩𝑈 \ (𝑌1,2 ∪𝑌1,3 )| ≥ 3𝑘 and 𝑌1,2 ∩ 𝑌1,3 = ∅. Notice that we can choose such sets 𝑌1,2 and 𝑌1,3 since |𝑌𝑈 ∩𝑈 | ≥ 3𝑘+1 . (e) If |𝑋 1,2 | ≥ 3𝑘 , |𝑋 1,3 | < 3𝑘 and |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪𝑋 1,3 )| ≥ 3𝑘 , then |𝑌1,3 | = |𝑋 1,3 |, |𝑌1,2 | ≥ 3𝑘 , |𝑌𝑈 ∩𝑈 \ (𝑌1,2 ∪𝑌1,3 )| ≥ 3𝑘 and 𝑌1,2 ∩ 𝑌1,3 = ∅. Notice that we can choose such sets 𝑌1,2 and 𝑌1,3 since |𝑌𝑈 ∩𝑈 | ≥ 3𝑘+1 . (f) If |𝑋 1,2 | ≥ 3𝑘 , |𝑋 1,3 | ≥ 3𝑘 and |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪ 𝑋 1,3 )| < 3𝑘 , then |𝑌𝑈 ∩𝑈 \ (𝑌1,2 ∪ 𝑌1,3 )| = |𝑋𝑈 ∩𝑈 \ (𝑋 1,2 ∪ 𝑋 1,3 )|, |𝑌1,2 | ≥ 3𝑘 , |𝑌1,3 | ≥ 3𝑘 and 𝑌1,2 ∩ 𝑌1,3 = ∅. Notice that we can choose such sets 𝑌1,2 and 𝑌1,3 since |𝑌𝑈 ∩𝑈 | ≥ 3𝑘+1 . (g) If |𝑋 1,2 | ≥ 3𝑘 , |𝑋 1,3 | ≥ 3𝑘 and |𝑋𝑈 ∩𝑈 \(𝑋 1,2 ∪𝑋 1,3 )| ≥ 3𝑘 , then |𝑌1,2 | ≥ 3𝑘 , |𝑌1,3 | ≥ 3𝑘 , |𝑌𝑈 ∩𝑈 \(𝑌1,2 ∪𝑌1,3 )| ≥ 3𝑘 and 𝑌1,2 ∩ 𝑌1,3 = ∅. Notice that we can choose such sets 𝑌1,2 and 𝑌1,3 since |𝑌𝑈 ∩𝑈 | ≥ 3𝑘+1 . (3) If |𝑋𝑈 \𝑈 | < 3𝑘+1 , then |𝑌𝑈 \𝑈 | = |𝑋𝑈 \𝑈 | since 𝑋 ⇆3𝑘+1 𝑌 . In this case, we choose 𝑌1,4 ⊆ 𝑌𝑈 \𝑈 in such a way that |𝑌1,4 | = |𝑋 1,4 | and |𝑌𝑈 \𝑈 \ 𝑌1,4 | = |𝑋𝑈 \𝑈 \ 𝑋 1,4 |. If |𝑋𝑈 \𝑈 | ≥ 3𝑘+1 , then |𝑌𝑈 \𝑈 | ≥ 3𝑘+1 since 𝑋 ⇆3𝑘+1 𝑌 . In this case, we choose 𝑌1,4 ⊆ 𝑌𝑈 \𝑈 in the following way. If |𝑋 1,4 | < 3𝑘 , then |𝑌1,4 | = |𝑋 1,4 |, and if |𝑋𝑈 \𝑈 \ 𝑋 1,4 | < 3𝑘 , then |𝑌𝑈 \𝑈 \ 𝑌1,4 | = |𝑋𝑈 \𝑈 \ 𝑋 1,4 |. Finally, if |𝑋 1,4 | ≥ 3𝑘 and |𝑋𝑈 \𝑈 \ 𝑋 1,4 | ≥ 3𝑘 , then |𝑌1,4 | ≥ 3𝑘 and |𝑌𝑈 \𝑈 \ 𝑌1,4 | ≥ 3𝑘 . Notice that we can choose such a set 𝑌1,4 since |𝑌𝑈 \𝑈 | ≥ 3𝑘+1 .
By definition of 𝑌1,1 , 𝑌1,2 , 𝑌1,3 and 𝑌1,4 , it is straightforward to conclude that 𝑌1 is wf, 𝑋 1 ⇆3𝑘 𝑌1 and (𝑋 \𝑋 1 ) ⇆3𝑘 (𝑌 \𝑌1 ). We have just proved that for every wf 𝑋 1 ⊆ 𝑋 , there exists a wf 𝑌1 ⊆ 𝑌 such that 𝑋 1 ⇆3𝑘 𝑌1 and 𝑋 \ 𝑋 1 ⇆3𝑘 𝑌 \ 𝑌1 . In the same way, it can be shown that for every wf 𝑌1 ⊆ 𝑌 , there exists a wf 𝑋 1 ⊆ 𝑋 such that 𝑋 1 ⇆3𝑘 𝑌1 and 𝑋 \ 𝑋 1 ⇆3𝑘 𝑌 \ 𝑌1 . This concludes the proof of the lemma. □ ∗
∗
We now consider structures of the form 𝔄 ∗ = ⟨2𝑋 , ⊆𝔄 ⟩, where 𝑋 ⊆ 𝑈 ∪ 𝑈 and ⊆ 𝔄 is the relation that contains all pairs (𝑌, 𝑍 ), for 𝑌, 𝑍 ⊆ 𝑋 , such that 𝑌 ⊆ 𝑍 . Given two structures 𝔄1∗ and 𝔄2∗ of this form, perhaps with constants, we write 𝔄1∗ ≡𝑘wf 𝔄2∗ to denote that the Duplicator has a winning strategy in the 𝑘-round Ehrenfeucht-Fraïssé game played on structures 𝔄1∗ and 𝔄2∗ , but where Spoiler and Duplicator are forced to play wf subsets of 𝑈 ∪ 𝑈 only. ∗
∗
Consider structures 𝔄1∗ = ⟨2𝑋1 , ⊆𝔄1 ⟩ and 𝔄2∗ = ⟨2𝑋2 , ⊆𝔄2 ⟩ of the form described above. We claim that, for every 𝑘 ≥ 0, 𝑋 1 ⇆3𝑘 𝑋 2
=⇒
𝔄1∗, (𝑋 1 ∩ 𝑈 ) ≡𝑘wf
𝔄2∗, (𝑋 2 ∩ 𝑈 ) .
Before proving the claim (5), we explain how it implies Lemma 3.2. Take a structure of the form 𝔄𝑛
(5) = ⟨{0, 1, ⊥}𝑛 , ⊆𝔄𝑛 ⟩, ∗
where ⊆𝔄𝑛 is the subsumption relation over {0, 1, ⊥}𝑛 . Take, on the other hand, the structure 𝔄𝑛∗ = ⟨2𝑋 , ⊆𝔄𝑛 ⟩, where 𝑋 = {𝑎 1, . . . , 𝑎𝑛 , 𝑎¯1, . . . , 𝑎¯𝑛 }. It can be seen that there is an isomorphism 𝑓 between 𝔄𝑛 and the substructure of 𝔄𝑛∗ induced by the wf subsets of 𝑋 . The isomorphism 𝑓 takes an instance e ∈ {0, 1, ⊥}𝑛 and maps it to 𝑌 ⊆ 𝑋 such that for
ExplAIner: A Declarative Query Language for Explaining Classification Models
37
every 𝑖 ∈ {1, . . . , 𝑛}, (a) if e[𝑖] = 1 then 𝑎𝑖 ∈ 𝑌 , (b) if e[𝑖] = 0 then 𝑎¯𝑖 ∈ 𝑌 , and (c) if e[𝑖] = ⊥ then neither 𝑎𝑖 nor 𝑎¯𝑖 is in 𝑌 . By definition, the isomorphism 𝑓 maps the tuple {1}𝑛 in 𝔄𝑛 to the set 𝑋 ∩ 𝑈 = {𝑎 1, . . . , 𝑎𝑛 } in 𝔄𝑛∗ . From claim (5), it follows then that if 𝑛, 𝑝 ≥ 3𝑘 it is the case that (𝔄𝑛∗ , {𝑎 1, . . . , 𝑎𝑛 }) ≡𝑘wf (𝔄𝑝∗ , {𝑎 1, . . . , 𝑎𝑝 }). From our previous observations, this implies that (𝔄𝑛 , {1}𝑛 ) ≡𝑘 (𝔄𝑝 , {1}𝑝 ). We conclude, in particular, that 𝔄𝑛+ ≡𝑘 𝔄𝑝+ , as desired. We now prove the claim in (5). We do it by induction on 𝑘 ≥ 0. The base cases 𝑘 = 0 and 𝑘 = 1 are immediate. We ∗
∗
now move to the induction case for 𝑘 + 1. Take structures 𝔄1∗ = ⟨2𝑋1 , ⊆𝔄1 ⟩ and 𝔄2∗ = ⟨2𝑋2 , ⊆𝔄2 ⟩ of the form described above, such that 𝑋 1 ⇆3𝑘+1 𝑋 2 . Assume, without loss of generality, that for the first round the Spoiler picks the well formed element 𝑋 1′ ⊆ 𝑋 1 in the structure 𝔄1∗ . From Lemma A.1, there exists 𝑋 2′ ⊆ 𝑋 2 such that 𝑋 1′ ⇆3𝑘 𝑋 2′ and 𝑋 1 \ 𝑋 1′ ⇆3𝑘 𝑋 2 \ 𝑋 2′ . By induction hypothesis, the following holds: ′
⟨2𝑋1 , ⊆⟩, (𝑋 1′ ∩ 𝑈 )
′
≡𝑘wf
⟨2𝑋2 , ⊆⟩, (𝑋 2′ ∩ 𝑈 )
⟨2𝑋1 \𝑋1 , ⊆⟩, ((𝑋 1 \ 𝑋 1′ ) ∩ 𝑈 )
≡𝑘wf
′ ⟨2𝑋2 \𝑋2 , ⊆⟩, ((𝑋 2 \ 𝑋 2′ ) ∩ 𝑈 ) .
′
A simple composition argument allows to obtain the following from these two expressions: ⟨2𝑋1 , ⊆⟩, (𝑋 1 ∩ 𝑈 ), 𝑋 1′ ≡𝑘wf ⟨2𝑋2 , ⊆⟩, (𝑋 2 ∩ 𝑈 ), 𝑋 2′ .
(6)
This holds because 𝑋 1′ = (𝑋 1 ∩ 𝑈 ) iff 𝑋 2′ = (𝑋 2 ∩ 𝑈 ). In fact, assume that 𝑋 1′ = (𝑋 1 ∩ 𝑈 ), so that 𝑋 1′ ∩ 𝑈 = ∅. Since 𝑋 1′ ⇆3𝑘 𝑋 2′ , it follows that 𝑋 2′ ⊆ 𝑋 2 ∩ 𝑈 . On the other hand, 𝑋 1 \ 𝑋 1′ = 𝑋 1 ∩ 𝑈 . As 𝑋 1 \ 𝑋 1′ ⇆3𝑘 𝑋 2 \ 𝑋 2′ , we conclude that 𝑋 2 \ 𝑋 2′ ⊆ 𝑈 , and hence 𝑋 2 ∩ 𝑈 ⊆ 𝑋 2′ . Combining both inclusions, we obtain that 𝑋 2′ = (𝑋 2 ∩ 𝑈 ). The other direction is completely analogous. But Equation (6) is equivalent with the following fact: wf ⟨2𝑋1 , ⊆⟩, (𝑋 1 ∩ 𝑈 ) ≡𝑘+1
⟨2𝑋2 , ⊆⟩, (𝑋 2 ∩ 𝑈 ) .
This finishes the proof of Lemma 3.2. A.2
Proof of Lemma 3.3
Let e𝑖 and e𝑖′ be the moves played by Spoiler and Duplicator in 𝔄 M ⊕ 𝔄 M1 and 𝔄 M ⊕ 𝔄 M2 , respectively, for the first 𝑖 ≤ 𝑘 rounds of the Ehrenfeucht-Fraïssé game 𝔄 M ⊕ 𝔄 M1 , {1}𝑛+𝑝 , {⊥}𝑛 · {1}𝑝
≡𝑘
𝔄 M ⊕ 𝔄 M2 , {1}𝑛+𝑞 , {⊥}𝑛 · {1}𝑞 .
We write e𝑖 = (e𝑖1, e𝑖2 ) to denote that e𝑖1 is the tuple formed by the first 𝑛 features of e𝑖 and e𝑖2 is the one formed by the ′ , e′ ) to denote that e′ is the tuple formed by the first 𝑛 features of e′ last 𝑝 features of e𝑖 . Similarly, we write e𝑖′ = (e𝑖1 𝑖 𝑖2 𝑖1 ′ is the one formed by the last 𝑞 features of e′ . and e𝑖2 𝑖
The winning strategy for Duplicator is as follows. Suppose 𝑖 − 1 rounds have been played, and for round 𝑖 the Spoiler picks element e𝑖 ∈ 𝔄 M ⊕ 𝔄 M1 (the case when he picks an element in 𝔄 M ⊕ 𝔄 M2 is symmetric). Assume also that
38
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
e𝑖 = (e𝑖1, e𝑖2 ). The duplicator then considers the position ′ (e12, . . . , e (𝑖 −1)2 ), (e12 , . . . , e′(𝑖 −1)2 )
′ to e in 𝔄 on the game (𝔄 M1 , {1}𝑝 ) ≡𝑘 (𝔄 M2 , {1}𝑞 ), and finds his response e𝑖2 𝑖2 M2 . The Duplicator then responds to ′ ) ∈ 𝔄 the Spoiler’s move e𝑖 ∈ 𝔄 M ⊕ 𝔄 M1 by choosing the element e𝑖′ = (e𝑖1, e𝑖2 M ⊕ 𝔄 M2 .
Notice, by definition, that e𝑖 = {1}𝑛+𝑝 iff e𝑖′ = {1}𝑛+𝑞 . Similarly, e𝑖 = {⊥}𝑛 · {1}𝑝 iff e𝑖′ = {⊥}𝑛 · {1}𝑞 . Moreover, it is easy to see that playing in this way the Duplicator preserves the subsumption relation. Analogously, the strategy preserves the Pos relation. In fact, e𝑖 is a positive instance of 𝔄 M ⊕ 𝔄 M1 iff e𝑖1 is a positive instance of 𝔄 M or e𝑖2 is ′ is a a positive instance of 𝔄 M1 . By definition, the latter follows if and only if e𝑖1 is a positive instance of 𝔄 M or e𝑖2
positive instance of 𝔄 M2 , which in turn is equivalent to e𝑖′ being a positive instance of 𝔄 M ⊕ 𝔄 M2 . We conclude that this is a winning strategy for the Duplicator, and hence that 𝔄 M ⊕ 𝔄 M1 , {1}𝑛+𝑝 , {⊥}𝑛 · {1}𝑝 ≡𝑘 𝔄 M ⊕ 𝔄 M2 , {1}𝑛+𝑞 , {⊥}𝑛 · {1}𝑞 . This finishes the proof of Lemma 3.3.
A.3
Proof of Lemma 3.5
To prove that Σ𝑘+1 -QBF(DTree) is in Σ𝑘P , note that we can decide in polynomial time if a given decision tree encodes a tautology. Therefore, we can use a Σ𝑘 -alternating Turing machine for guessing the values for the first 𝑘 quantifiers, we prune the decision tree according to those guesses, and then we solve the remaining universal quantifier directly. For the hardness, we use a reduction from the following standard Σ𝑘P -hard problem (see [19] for a reference): Given a 3CNF formula 𝜑 over the set 𝑋 = {𝑥 1, . . . , 𝑥𝑚 } of propositional variables, is it the case that the expression 𝜓 = ∃𝑋 1 ∀𝑋 2 · · · ∃𝑋𝑘 𝜑 holds, where 𝑋 1, . . . , 𝑋𝑘 is a partition of 𝑋 in 𝑘 equivalence classes? Note that the hypothesis of 𝑘 being odd is important here because if the last quantifier were universal, we could solve it directly as in the case of decision trees. From 𝜓 we build in polynomial time a Σ𝑘+1 -QBF 𝛼 over M𝜑 , where M𝜑 is a decision tree that can be built in polynomial time from 𝜑, such that 𝜓 holds
⇐⇒
𝛼 holds.
(7)
We now explain how to define M𝜑 from the CNF formula 𝜑. Let 𝜑 = 𝐶 1 ∧ · · · ∧ 𝐶𝑛 be a propositional formula, where each 𝐶𝑖 is a disjunction of three literals and does not contain repeated or complementary literals. Moreover, assume that {𝑥 1, . . . , 𝑥𝑚 } is the set of variables occurring in 𝜑, and the proof will use partial instances of dimension 𝑛 + 𝑚. Notice that the last 𝑚 features of such a partial instance e naturally define a truth assignment for the propositional formula 𝜑. More precisely, for every 𝑖 ∈ {1, . . . , 𝑛}, we use notation e(𝐶𝑖 ) = 1 to indicate that there is a disjunct ℓ of 𝐶𝑖 such that ℓ = 𝑥 𝑗 and e[𝑛 + 𝑗] = 1, or ℓ = ¬𝑥 𝑗 and e[𝑛 + 𝑗] = 0, for some 𝑗 ∈ {1, . . . , 𝑚}. Furthermore, we write e(𝜑) = 1 if e(𝐶𝑖 ) = 1 for every 𝑖 ∈ {1, . . . , 𝑛}. For each clause 𝐶𝑖 (𝑖 ∈ {1, . . . , 𝑛}), let M𝐶𝑖 be a decision tree of dimension 𝑛 + 𝑚 (but that will only use features 𝑛 + 1, . . . , 𝑛 + 𝑚) such that for every instance e: M𝐶𝑖 (e) = 1 if and only if e(𝐶𝑖 ) = 1. Notice that M𝐶𝑖 can be constructed in constant time as it only needs to contain at most eight paths of depth 3. For example, assuming that 𝐶 = (𝑥 1 ∨ 𝑥 2 ∨ 𝑥 3 ), a possible decision tree M𝐶 is depicted in the following figure:
ExplAIner: A Declarative Query Language for Explaining Classification Models
39
𝑛+1 0
1
𝑛+2 0
𝑛+2 0
1
𝑛+3 0 false
𝑛+3 0
1 true
1
𝑛+3
𝑛+3
0
1
true
true
0
1
true
true
1
true
true
Moreover, define M𝜑 as the following decision tree. 0
1
M𝐶1
1 0
2
M𝐶2
1 0
3
M𝐶3
1 ··· 1 𝑛 0
1
M𝐶𝑛
true
Recall that the set of features of M𝜑 is [1, 𝑛 + 𝑚]. The formula 𝛼 is defined as ∃𝑃1 ∀𝑃 2 · · · ∃𝑃𝑘 ∀𝑃 M𝜑 , assuming that 𝑃𝑖 , for 1 ≤ 𝑖 ≤ 𝑘, is the set {𝑛 + ℓ | 𝑥 ℓ ∈ 𝑋𝑖 }, and 𝑃 = {1, . . . , 𝑛}. That is, 𝑃𝑖 is the set of features from M𝜑 that represent the variables in 𝑋𝑖 and 𝑃 is the set of features that are used to encode the clauses of 𝜑. We show next that the equivalence stated in (7) holds. For simplicity, we only do it for the case 𝑘 = 1. The proof for 𝑘 > 1 uses exactly the same ideas, only that it is slightly more cumbersome. Assume, on the one hand, that 𝜓 = ∃𝑋 1𝜑 holds. That is, there exists an assignment 𝜎1 : 𝑋 1 → {0, 1} such that 𝜑 holds when variables in 𝑋 1 are interpreted according to 𝜎1 . We show next that 𝛼 = ∃𝑃 1 ∀𝑃M𝜑 holds, where 𝑃1 and 𝑃 are defined as above. Take the partial instance e𝜎1 of dimension 𝑛 + 𝑚 that naturally “represents” the assignment 𝜎1 ; that is: • e𝜎1 [𝑖] = ⊥, for each 𝑖 ∈ {1, . . . , 𝑛}, • e𝜎1 [𝑛 + 𝑖] = 𝜎1 (𝑥𝑖 ), for each 𝑖 ∈ {1, . . . , 𝑚} with 𝑥𝑖 ∈ 𝑋 1 , and • e𝜎1 [𝑛 + 𝑖] = ⊥, for each 𝑖 ∈ {1, . . . , 𝑚} with 𝑥𝑖 ∉ 𝑋 1 . To show that 𝛼 holds, it suffices to show that M𝜑 (e) = 1 for every instance e of dimension 𝑛 + 𝑚 that subsumes e𝜎1 . Take an arbitrary such an instance e ∈ {0, 1}𝑛+𝑚 . Notice that if e[𝑖] = 1, for every 𝑖 ∈ {1, . . . , 𝑛}, then M𝜑 (e) = 1 by definition of M𝜑 . Suppose then that there exists a minimum value 𝑖 ∈ {1, . . . , 𝑛} such that e[𝑖] = 0. Hence, to show that M𝜑 (e) = 1 we need to show that M𝐶𝑖 (e) = 1. But this follows easily from the fact that e naturally represents an assignment 𝜎 for 𝜑 such that the restriction of 𝜎 to 𝑋 1 is precisely 𝜎1 . We know that any such an assignment 𝜎 satisfies 𝜑, and therefore it satisfies 𝐶𝑖 . It follows that M𝐶𝑖 (e) = 1.
40
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux Assume, on the other hand, that 𝛼 = ∃𝑃 1 ∀𝑃M𝜑 holds. Then there exists a partial instance e of dimension 𝑛 + 𝑚 such
that the following statements hold: • e[𝑖] ≠ ⊥ iff for some 𝑗 ∈ {1, . . . , 𝑚} it is the case that 𝑖 = 𝑛 + 𝑗 and 𝑗 ∈ 𝑃1 , and • for every e′ ∈ comp(e) we have that M𝜑 (e′ ) = 1. We show next that 𝜓 = ∃𝑋 1𝜑 holds. Let 𝜎1 : 𝑋 1 → {0, 1} be the assignment for the variables in 𝑋 1 that is naturally defined by e. It suffices to show that each clause 𝐶𝑖 of 𝜑, for 𝑖 ∈ {1, . . . , 𝑛}, is satisfied by the assignment that interprets the variables in 𝑋 1 according to 𝜎1 . Let us define a completion e′ of e that satisfies the following: • e′ [𝑖] = 0, • e′ [ 𝑗] = 1, for each 𝑗 ∈ {1, . . . , 𝑛} with 𝑖 ≠ 𝑗, and • e′ [𝑛 + 𝑗] = 𝜎1 (𝑥 𝑗 ), if 𝑗 ∈ {1, . . . , 𝑚} and 𝑗 ∈ 𝑃 1 . We know that M𝜑 (e′ ) = 1, which implies that M𝐶𝑖 (e′ ) = 1 (since e′ takes value 0 for feature 𝑖). We conclude that 𝐶𝑖 is satisfied by the assignment which is naturally defined by e′ , which is precisely the one that interprets the variables in 𝑋 1 according to 𝜎1 . A.4
Proof of Lemma 4.4
We induct on the depth of 𝜑. First we will see the atomic cases: • For atomic formulas of the form 𝑥𝑖 = 𝑥 𝑗 , we take ∑︁
𝑧 𝜌 = 0.
𝜌 ∈ {0,1,⊥}𝑘 𝜌𝑖 ≠𝜌 𝑗
• For atomic formulas of the form 𝑥𝑖 ⊆ 𝑥 𝑗 , we take ∑︁
𝑧 𝜌 = 0.
𝜌 ∈ {0,1,⊥}𝑘 𝜌𝑖 ≠𝜌 𝑗 ∧ 𝜌𝑖 ≠⊥
• For atomic formulas of the form 𝑥𝑖 ⪯ 𝑥 𝑗 , we take ∑︁ 𝑧𝜌 ≤ 𝜌 ∈ {0,1,⊥}𝑘 𝜌 𝑗 =⊥
∑︁
𝑧𝜌 .
𝜌 ∈ {0,1,⊥}𝑘 𝜌𝑖 =⊥
Now we describe the structural induction. For the negation, it is enough to take TΓ (¬𝜓 ) (𝑧 𝜌 )𝜌 as ¬ TΓ (𝜓 ) (𝑧 𝜌 )𝜌 . If 𝜑 is of the form 𝜓 1 ◦ 𝜓 2 , where ◦ is a binary logical connective, then we take TΓ (𝜑) (𝑧 𝜌 )𝜌 as TΓ (𝜓 1 ) (𝑧 𝜌 ) ◦ TΓ (𝜓 2 ) (𝑧 𝜌 ) . Note that here it is important to use the inductive hypothesis with Γ that contains both the free variables of 𝜓 1 and of 𝜓 2 . We need to be more careful if 𝜑 is of the form ∃𝑢 𝜓 (𝑦1, . . . , 𝑦ℓ , 𝑢). By changing the name of the variable if necessary, we can assume that 𝑢 ∉ Γ. Consider Λ = (𝑥 1, . . . , 𝑥𝑘 , 𝑢) and take the formula TΛ (𝜓 ) (𝑤𝜏 )𝜏 ∈ {0,1,⊥}𝑘+1 given by the inductive hypothesis. We take TΓ (𝜑) (𝑧 𝜌 )𝜌 ∈ {0,1,⊥}𝑘 to be ∃(𝑤𝜏 )𝜏 ∈ {0,1,⊥}𝑘+1
ProjΛ→Γ ((𝑤𝜏 )𝜏 , (𝑧 𝜌 )𝜌 ) ∧ TΛ (𝜓 ) (𝑤𝜏 )𝜏 ∈ {0,1,⊥}𝑘+1 ,
ExplAIner: A Declarative Query Language for Explaining Classification Models where ProjΛ→Γ ((𝑤𝜏 )𝜏 , (𝑧 𝜌 )𝜌 ) is defined to be Û
41
𝑧 𝜌 = 𝑤 (𝜌,0) + 𝑤 (𝜌,1) + 𝑤 (𝜌,⊥) .
𝜌 ∈ {0,1,⊥}𝑘
Finally, if 𝜑 is of the form ∀𝑢 𝜓 (𝑦1, . . . , 𝑦ℓ , 𝑢), we define Λ as before and take TΓ (𝜑) (𝑧 𝜌 )𝜌 ∈ {0,1,⊥}𝑘 to be ∀(𝑤𝜏 )𝜏 ∈ {0,1,⊥}𝑘+1 ProjΛ→Γ ((𝑤𝜏 )𝜏 , (𝑧 𝜌 )𝜌 ) → TΛ (𝜓 ) (𝑤𝜏 )𝜏 ∈ {0,1,⊥}𝑘+1 . For the second part of the lemma, note that for a subformula translated in a context Γ of size 𝑘, the corresponding Presburger formula has 3𝑘 variables. In the atomic cases we just need to manage sums without repetitions over those variables. Boolean connectives also do not cause any problems. In the case of quantifiers, we need to increase the size of the context from 𝑘 to 𝑘 + 1 and we also add 3𝑘 projection formulas plus the recursive call. But because 𝑘 + 1 ≤ wd(𝜑) and there are 𝑂 (|𝜑 |) subformulas, the total output size is 𝑂 (|𝜑 | · 3wd(𝜑 ) ) up to polynomial factors of wd(𝜑). Notice that the same argument applies for proving that the computation itself can be done using at most that same space. A.5
Proof of Lemma 4.6
Consider the following similar problem. The input is a model M ′ , an instance e′ and a 𝑘 ∈ N, and the question is whether there exists a partial instance e that is a weak abductive explanation for e′ on M ′ and whose number of defined features is at most 𝑘. This problem was studied in [11], where it was shown to be NP-hard on decision trees. We show a reduction from this problem. First assume that M ′ (e′ ) = 1. We create new variables 𝑋𝑖 for 𝑖 ∈ {0, 1, ..., 𝑘 }. Let M be a new decision tree such that dim(M) = 𝑘 + 1 + dim(M ′ ), depicted in the following figure:
We use 𝑋 0 as the root of M. For every 𝑖 < 𝑘, the outgoing edge of 𝑋𝑖 labeled by 1 is connected to 𝑋𝑖+1 , and the outgoing edge of 𝑋𝑘 labeled by 1 is connected to a true leaf. Connect all outgoing edges labeled by 0 to a copy of ′
M ′ . Let e1 = {1}𝑘+1 · e′ and e2 = {1}𝑘+1 · {⊥}dim( M ) be partial instances of size d𝑖𝑚(M). We claim that e2 is a minimum abductive explanation for e1 on M if and only if the answer to the original problem was negative. For the case M ′ (e′ ) = 0 we can just set the value of the new leaf to false and the same construction will work. We now discuss why the reduction works. Suppose first that (M ′, e′, 𝑘) outputs Yes. It follows that there exists a partial instance e on M ′ that is a weak abductive explanation for e′ with at most 𝑘 defined features. Now notice that
42
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
the partial instance {⊥}𝑘+1 · e is a weak abductive explanation for e1 on M and has at most 𝑘 defined features. Because e2 has 𝑘 + 1 defined features, it follows that e2 is not a minimum abductive explanation for e1 on M. Now suppose that (M ′, e′, 𝑘) outputs No. Then there is no weak abductive explanation for e′ on M ′ with at most 𝑘 defined features. This implies that there is also no partial instance e on M that is a weak abductive explanation for e1 with at most 𝑘 defined features. This is because any candidate weak abductive explanation for e1 with at most 𝑘 defined features leaves at least one of the new variables undefined, and therefore some completion of it reaches a copy of M ′ . Once it enters that copy of M ′ , its restrictions on the old coordinates would induce a weak abductive explanation for e′ on M ′ with at most 𝑘 defined features, contradicting the assumption. But we know that e2 is a weak abductive explanation for e1 with 𝑘 + 1 defined features, so it is a minimum abductive explanation for e1 on M, as we needed.
A.6
Proof of Lemma 5.5
We first treat the parameter-free case 𝜌 (𝑥, 𝑦), and then we extend the idea to the general case. Fix a dimension 𝑛. Given a partial instance of dimension 𝑛, define #0 (e) as the number of occurrences of the symbol 0 in e, and likewise for #1 (e) and #⊥ (e). Moreover, for every (𝑝, 𝑞, 𝑟 ) ∈ N3 such that 𝑝 + 𝑞 + 𝑟 = 𝑛, define 𝐿 (𝑝,𝑞,𝑟 ) := {e | e is a partial instance of dimension 𝑛 such that #0 (e) = 𝑝, #1 (e) = 𝑞 and #⊥ (e) = 𝑟 }. Notice that there are at most 𝑛+2 ≤ (𝑛 + 1) 2 different sets 𝐿 (𝑝,𝑞,𝑟 ) . We claim that if e1 and e2 are partial instances of 2 dimension 𝑛 such that e1, e2 ∈ 𝐿 (𝑝,𝑞,𝑟 ) for the same triple (𝑝, 𝑞, 𝑟 ), then 𝔅𝑛 ̸ |= 𝜌 (e1, e2 ). From that we can conclude that the statement of the lemma holds for 𝑝 (𝑛) = (𝑛 + 1) 2 , since if (e1, . . . , e𝑘 ) is a path of dimension 𝑛 in 𝜌 (𝑥, 𝑦), then each e𝑖 must belong to a different set 𝐿 (𝑝,𝑞,𝑟 ) . For the sake of contradiction, suppose that e1, e2 are two different partial instances of dimension 𝑛 that belong to the same set 𝐿 (𝑝,𝑞,𝑟 ) and such that 𝔅𝑛 |= 𝜌 (e1, e2 ). Then there exists a permutation 𝜋 : {1, . . . , 𝑛} → {1, . . . , 𝑛} such that 𝜋 (e1 ) = e2 . Notice that for every pair e, e′ of partial instances of dimension 𝑛 it holds that: e ⊆ e′
⇔
𝜋 (e) ⊆ 𝜋 (e′ )
e ⪯ e′
⇔
𝜋 (e) ⪯ 𝜋 (e′ ).
Thus, 𝜋 is an automorphism for the structure 𝔅𝑛 . Because we have that 𝔅𝑛 |= 𝜌 (e1, e2 ), and 𝜌 is defined over the vocabulary {⊆, ⪯}, it follows 𝔅𝑛 |= 𝜌 (𝜋 (e1 ), 𝜋 (e2 )). But since e2 = 𝜋 (e1 ), we also have that 𝔅𝑛 |= 𝜌 (e2, 𝜋 (𝜋 (e1 ))). Because 𝜌 (𝑥, 𝑦) is transitive, it follows that 𝔅𝑛 |= 𝜌 (e1, 𝜋 2 (e1 )). In the same way, we can conclude that 𝔅𝑛 |= 𝜌 (e1, 𝜋 𝑘 (e1 )) for every 𝑘 ≥ 1. Given that the set of permutations of 𝑛 elements with the composition operator forms a group of order 𝑛!, we know that 𝜋 𝑛! is the identity permutation, so that 𝜋 𝑛! (e1 ) = e1 . Therefore, we conclude that 𝔅𝑛 |= 𝜌 (e1, e1 ), which leads to a contradiction since 𝜌 (𝑥, 𝑦) represents a strict partial order. Consider now a formula 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦) with parameters. As in the previous case, we fix a dimension 𝑛. Moreover, we also fix a sequence e1′ , . . ., eℓ′ of partial instances of dimension 𝑛 (notice that the bound 𝑝 (𝑛) should not depend on those partial instances). Then, for every (𝑎 1, . . . , 𝑎 ℓ ) ∈ {0, 1, ⊥}ℓ , consider the set 𝑃 (𝑎1 ,...,𝑎ℓ ) = {𝑖 ∈ {1, . . . , 𝑛} | e′𝑗 [𝑖] = 𝑎 𝑗 for all 𝑗 ∈ {1, . . . , ℓ }}, that is, all positions for which the sequence e1′ , . . ., eℓ′ realizes the pattern (𝑎 1, . . . , 𝑎 ℓ ). Given 𝑠 ∈ {0, 1, ⊥}, a pattern 𝑡 ∈ {0, 1, ⊥}ℓ and a partial instance e of dimension 𝑛, define #𝑠,𝑡 (e) as the number of indices 𝑖 ∈ 𝑃𝑡 such that e[𝑖] = 𝑠. Notice that the numbers #𝑠,𝑡 (e) are invariant under permutations of the features that map each pattern block onto itself.
ExplAIner: A Declarative Query Language for Explaining Classification Models
43
We define an equivalence relation as follows. For two partial instances e1 and e2 of dimension 𝑛, we write e1 ∼ e2 if #𝑠,𝑡 (e1 ) = #𝑠,𝑡 (e2 ) for every 𝑠 ∈ {0, 1, ⊥} and every 𝑡 ∈ {0, 1, ⊥}ℓ . Notice that there are at most 3ℓ +1 −1 𝑛 + 3ℓ+1 − 1 𝑛 + 3ℓ+1 − 1 ≤ 3ℓ+1 − 1 3ℓ+1 − 1 ! different equivalence classes. Because ℓ is fixed, we can consider that number as our polynomial 𝑝 (𝑛). We claim that if e1 ∼ e2 , then 𝔅𝑛 ̸ |= 𝜌 [e1′ , . . . , eℓ′ ] (e1, e2 ). From that we can conclude, as in the parameter-free case, that the statement of the lemma holds. In fact, if (e1, . . . , e𝑘 ) is a path of dimension 𝑛 in 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦), then each e𝑖 must belong to a different equivalence class. For the sake of contradiction, suppose that e1, e2 are two different partial instances of dimension 𝑛 such that e1 ∼ e2 and 𝔅𝑛 |= 𝜌 [e1′ , . . . , eℓ′ ] (e1, e2 ). For each pattern block 𝑃𝑡 , consider a permutation 𝜋𝑡 of 𝑃𝑡 sending the restriction of e1 on 𝑃𝑡 to the restriction of e2 on 𝑃𝑡 . Combining these permutations yields a permutation 𝜋 : {1, . . . , 𝑛} → {1, . . . , 𝑛} such that 𝜋 (e1 ) = e2 . Notice that by the way we constructed the permutations 𝜋𝑡 and the pattern blocks 𝑃𝑡 , we have that 𝜋 (e′𝑗 ) = e′𝑗 for every 𝑗 ∈ {1, . . . , ℓ }. As in the parameter-free case, we have that 𝜋 is an automorphism for the structure 𝔅𝑛 . Since 𝜌 is a formula defined over the vocabulary {⊆, ⪯}, and 𝔅𝑛 |= 𝜌 [e1′ , . . . , eℓ′ ] (e1, e2 ), it follows that 𝔅𝑛 |= 𝜌 [𝜋 (e1′ ), . . . , 𝜋 (eℓ′ )] (𝜋 (e1 ), 𝜋 (e2 )). Because 𝜋 (e′𝑗 ) = e′𝑗 for every 𝑗 ∈ {1, . . . , ℓ } and e2 = 𝜋 (e1 ), we obtain that 𝔅𝑛 |= 𝜌 [e1′ , . . . , eℓ′ ] (e2, 𝜋 (𝜋 (e1 ))), and using that 𝜌 [e1′ , . . . , eℓ′ ] (𝑥, 𝑦) is transitive, we also have that 𝔅𝑛 |= 𝜌 [e1′ , . . . , eℓ′ ] (e1, 𝜋 2 (e1 )). In the same way, it is possible to conclude that 𝔅𝑛 |= 𝜌 [e1′ , . . . , eℓ′ ] (e1, 𝜋 𝑘 (e1 )) for every 𝑘 ≥ 1. Given that the set of permutations of 𝑛 elements with the composition operator forms a group of order 𝑛!, we know that 𝜋 𝑛! is the identity permutation, so that 𝜋 𝑛! (e1 ) = e1 . Therefore, we conclude that 𝔅𝑛 |= 𝜌 [e1′ , . . . , eℓ′ ] (e1, e1 ), which leads to a contradiction since 𝜌 [𝑣 1, . . . , 𝑣 ℓ ] (𝑥, 𝑦) represents a strict partial order. A.7
Auxiliary predicates
Definition of the formula LEH(𝑥, 𝑦, 𝑧). Let GLB (Greatest Lower Bound) be the following formula: GLB(𝑥, 𝑦, 𝑧) := 𝑧 ⊆ 𝑥 ∧ 𝑧 ⊆ 𝑦 ∧ ∀𝑤 ((𝑤 ⊆ 𝑥 ∧ 𝑤 ⊆ 𝑦) → 𝑤 ⊆ 𝑧). The interpretation of this predicate is such that for every model M of dimension 𝑛 and every sequence of instances e1, e2, e3 it holds that M |= GLB(e1, e2, e3 ) if and only if e3 is the greatest partial instance subsumed by e1 and e2 , i.e., the partial instance with most defined features subsumed by both. This property allows us to measure the number of defined features on which the two instances agree. By using this predicate, let LEH be a ternary predicate such that M |= LEH(e1, e2, e3 ) if and only if the Hamming distance between e1 and e2 is less than or equal to the Hamming distance between e1 and e3 . The relation LEH can be expressed as a formula from the atomic layer of ExplAIner as follows: LEH(𝑥, 𝑦, 𝑧) := Full(𝑥) ∧ Full(𝑦) ∧ Full(𝑧) ∧ ∃𝑤 1 ∃𝑤 2 (GLB(𝑥, 𝑦, 𝑤 1 ) ∧ GLB(𝑥, 𝑧, 𝑤 2 ) ∧ 𝑤 2 ⪯ 𝑤 1 ). Definition of the formula Add(𝑥, 𝑦, 𝑧). Let LU (Level Up) be the following formula: LU(𝑥, 𝑦) := 𝑥 ≺ 𝑦 ∧ ¬∃𝑧 (𝑥 ≺ 𝑧 ∧ 𝑧 ≺ 𝑦), such that M ⊨ LU(e1, e2 ) if and only if e1 has exactly one less defined feature than e2 . By using this predicate, let Add be a ternary predicate such that M ⊨ Add(e1, e2, e3 ) if and only if e2 is a feature subsumed by e3 and e1 is obtained
44
Arenas, Barceló, Bustamante, Caraball, Schild and Subercaseaux
from e3 by undefining the feature e2 . The relation Add can be expressed as formula from the atomic layer of ExplAIner as follows: Add(𝑥, 𝑦, 𝑧) := Single(𝑦) ∧ 𝑥 ⊆ 𝑧 ∧ LU(𝑥, 𝑧) ∧ 𝑦 ⊆ 𝑧 ∧ ¬(𝑦 ⊆ 𝑥). Recall that Single(𝑥) defines the set of partial instances with exactly one defined feature, and can be expressed as follows: Single(𝑥) := ∃𝑦 (𝑦 ⊂ 𝑥) ∧ ∀𝑦(𝑦 ⊂ 𝑥 → ¬∃𝑧 (𝑧 ⊂ 𝑦)).