Foundations of Symbolic Languages for Model Interpretability
Year: 2021

Abstract:
Several queries and scores have been proposed to explain individual predictions made by ML models. Examples include queries based on “anchors”, which are parts of an instance that are sufficient to justify its classification, and “featureperturbation” scores such as SHAP. Given the need for flexible, reliable, and easy-toapply interpretability methods for ML models, we foresee the need for developing declarative languages to naturally specify different explainability queries. We do this in a principled way by rooting such a language in a logic called FOIL, that allows for expressing many simple but important explainability queries, and might serve as a core for more expressive interpretability languages. We study the computational complexity of FOIL queries over classes of ML models often deemed to be easily interpretable: decision trees and more general decision diagrams. Since the number of possible inputs for an ML model is exponential in its dimension, tractability of the FOIL evaluation problem is delicate, but can be achieved by either restricting the structure of the models, or the fragment of FOIL being evaluated. We also present a prototype implementation of FOIL wrapped in a high-level declarative language, and perform experiments showing that such a language can be used in practice.

heading: 1 Introduction
text: Context. The degree of interpretability of a machine learning (ML) model seems to be intimately related with the ability to “answer questions” about it. Those questions can either be global (behavior of the model as a whole) or local (behavior regarding certain instances/features). Concrete examples of such questions can be found in the recent literature, including, e.g., queries based on “anchors”, which are parts of an instance that are sufficient to justify its classification [4, 13, 16, 32], and numerical scores that measure the impact of the different features of an instance on its result [24, 31, 36].
It is by now clear that ML interpretability admits no silver-bullet [18], and that in many cases a combination of different queries may be the most effective way to understand a model’s behavior. Also, model interpretability takes different flavors depending on the application domain one deals with. This naturally brings to the picture the need for general-purpose specification languages that can provide flexibility and expressiveness to practitioners specifying interpretability queries. An even more advanced requirement for these languages is to be relatively easy to use in practice. This tackles the growing need for bringing interpretability methods closer to users with different levels of expertise.
35th Conference on Neural Information Processing Systems (NeurIPS 2021).
One way in which these requirements can be approached in a principled way is by developing a declarative interpretability language, i.e., one in which users directly express the queries they want to apply in the interpretability process (and not how these queries will be evaluated). This is of course reminiscent of the path many other areas in computer science have followed, in particular by using languages rooted in formal logic; so has been the case, e.g., in data management [1], knowledge representation [3], and model checking [15]. One of the advantages of this approach is that logics have a well-defined syntax and clear semantics. On the one hand, this ensures that the obtained explanations are provably sound and faithful to the model, which avoids a significant drawback of several techniques for explaining models in which the explanations can be inaccurate, or require themselves to be further explained [33]. On the other hand, a logical root facilitates the theoretical study of the computational cost of evaluation and optimization for the queries in the language.
Our proposal. Our first contribution is the proposal of a logical language, called FOIL, in which many simple yet relevant interpretability queries can be expressed. We believe that FOIL can further serve as a basis over which more expressive interpretability languages can be built, and we propose concrete directions of research towards its expansion. In a nutshell, given a decision modelM that performs classification over instances e of dimension n, FOIL can express properties over the set of all partial and full instances of dimension n. A partial instance e is a vector of dimension n in which some features are undefined. Such undefined features take a distinguished value ⊥. An instance is full if none of its features is undefined. The logic FOIL is simply first-order logic with access to two predicates on the set of all instances (partial or full) of dimension n: A unary predicate POS(e), stating that e is a full instance thatM classifies as positive, and a binary predicate e ⊆ e′, stating that instance e′ potentially fills some of the undefined features of instance e; e.g., (1, 0, ⊥) ⊆ (1, 0, 1), but (1, 0, ⊥) 6⊆ (1, 1, 1). As an overview of our proposal, consider the case of a bank using a binary model to judge applications for loans. Figure 1a illustrates the problem with concrete features, and Figure 1b presents an example of a concrete interactive syntax. In Figure 1b, after loading and exploring the model, the interaction asks whether the model could give a loan to a person who is married and does not have kids. Assuming that the “Accepted” class is the positive one, this interaction can easily be formalized in FOIL by means of the query ∃x ( POS(x) ∧ (⊥,⊥,⊥,⊥, 0, 1,⊥) ⊆ x ) .
Theoretical contributions. The evaluation problem for a fixed FOIL query ϕ is as follows. Given a decision modelM, is it true that ϕ is satisfied under the interpretation of predicates ⊆ and POS defined above? An important caveat about this problem is that, in order to evaluate ϕ, we need to potentially look for an exponential number of instances, even if the features are Boolean, thus rendering the complexity of the problem infeasible in some cases. Think, for instance, of the query ∃x POS(x), which asks ifM has at least one positive instance. Then this query is intractable for every class of models for which this problem is intractable; e.g., for the class of propositional formulas in CNF (notice that this is nothing but the satisfiability problem for the class at hand).
The main theoretical contribution of our paper is an in-depth study of the computational cost of FOIL on two classes of Boolean models that are often deemed to be “easy to interpret”: decision trees and ordered binary decision diagrams (OBDDs) [10, 14, 19, 28, 33]. An immediate advantage of
these models over, say, CNF formulas, is that the satisfiability problem for them can be solved in polynomial time; i.e., the problem of evaluating the query ∃xPOS(x) is tractable. Our study aims to (a) “measure” the degree of interpretability of said models in terms of the formal yardstick defined by the language FOIL; and (b) shed light on when and how some simple interpretability queries can be evaluated efficiently on these decision models.
We start by showing that, in spite of the aforementioned claims on the good level of interpretability for the models considered, there is a simple query in FOIL that is intractable over them. In fact, such an intractable query has a natural “interpretability” flavor, and thus we believe this proof to be of independent interest.
However, these intractability results should not immediately rule out the use of FOIL in practice. In fact, it is well known that a logic can be intractable in general, but become tractable in practically relevant cases. Such cases can be obtained by either restricting the syntactic fragment of the logic considered, or the structure of the models in which the logic is evaluated. We obtain positive results in both directions for the models we mentioned above. We explain them next.
Syntactic fragments. We show that queries in ∃FOIL, the existential fragment of FOIL, admit tractable evaluation over the models we study. However, this language lacks expressive power for capturing some interpretability queries of practical interest. We then introduce ∃FOIL+, an extension of ∃FOIL with a finite set of unary universal queries from FOIL that is enough for expressing some relevant interpretability queries. We provide a characterization theorem for the tractability of ∃FOIL+ over any class of Boolean decision models that reduces the tractability of this fragment to the tractability of two fixed and specific FOIL queries. Then we prove that said queries are tractable over perceptrons, which implies the tractability of ∃FOIL+ for this model. Unfortunately, the evaluation of said queries is NP-hard for decision trees and OBDDs. Both the proof of tractability for perceptrons and intractability for decision trees and OBDDs are relatively simple, thus showing that the characterization theorem provides a useful technique for understanding which models are tractable for the evaluation of ∃FOIL+. Structural restrictions. We restrict the models allowed in order to obtain tractability of evaluation for arbitrary FOIL queries. In particular, we show that evaluation of ϕ, for ϕ a fixed FOIL query, can be solved in polynomial time over the class of OBDDs as long as they are complete, i.e., any path from the root to a leaf of the OBDD tests every feature from the input, and have bounded width, i.e., there is a constant bound on the number of nodes of the OBDD in which a feature can appear.
Practical implementation. We designed FOIL with a minimal set of logical constructs and tailored for models with binary input features. These decisions are reasonable for a detailed theoretical analysis but may hamper FOIL usage in more general scenarios, in particular when models have (many) categorical or numerical input features, and queries are manually written by non-expert users. To tackle this we introduce a more user-friendly language with a high-level syntax (à la SQL in the spirit of the query in Figure 1b) that can be compiled into FOIL queries. Moreover, we present a prototype implementation that can be used to query decision trees trained in standard ML libraries by binarizing them into models (a subclass of binary decision diagrams) over which FOIL queries can be efficiently evaluated. We also test the performance of our implementation over synthetic and real data giving evidence of the usability of FOIL as a base for practical interpretabilty languages.

heading: 2 A Logic for Interpretability Queries
text: Background. An instance of dimension n, with n ≥ 1, is a tuple e ∈ {0, 1}n. We use notation e[i] to refer to the i-th component of this tuple, or equivalently, its i-th feature. Moreover, we consider an abstract notion of a model of dimension n, and we define it as a Boolean function M : {0, 1}n → {0, 1}. That is,M assigns a Boolean value to each instance of dimension n, so that we focus on binary classifiers with Boolean input features. Restricting inputs and outputs to be Boolean makes our setting cleaner while still covering several relevant practical scenarios. We use notation dim(M) for the dimension of a modelM. A partial instance of dimension n is a tuple e ∈ {0, 1,⊥}n. Intuitively, if e[i] = ⊥, then the value of the i-th feature is undefined. Notice that an instance is a particular case of a partial instance where all features are assigned value either 0 or 1. Given two partial instances e1, e2 of dimension n, we say that e1 is subsumed by e2 if for every i ∈ {1, . . . , n} such that e1[i] 6= ⊥, it holds that e1[i] = e2[i].
That is, e1 is subsumed by e2 if it is possible to obtain e2 from e1 by replacing some unknown values. Notice that a partial instance e can be thought of as a compact representation of the set of instances e′ such that e is subsumed by e′, where such instances e′ are called the completions of e.
Models. A binary decision diagram (BDD [38]) over instances of dimension n is a rooted directed acyclic graphM with labels on edges and nodes such that: (i) each leaf is labeled with true or false; (ii) each internal node (a node that is not a leaf) is labeled with a feature i ∈ {1, . . . , n}; and (iii) each internal node has two outgoing edges, one labeled 1 and the another one labeled 0. Every instance e ∈ {0, 1}n defines a unique path πe = u1 · · ·uk from the root u1 to a leaf uk ofM such that: if the label of ui is j ∈ {1, . . . , n}, where i ∈ {1, . . . , k − 1}, then the edge from ui to ui+1 is labeled with e[j]. Moreover, the instance e is positive, denoted byM(e) = 1, if the label of uk is true; otherwise the instance e is negative, which is denoted byM(e) = 0. A binary decision diagramM is free (FBDD) if for every path from the root to a leaf, no two nodes on that path have the same label. Besides,M is ordered (OBDD) if there exists a linear order < on the set {1, . . . , n} of features such that, if a node u appears before a node v in some path inM from the root to a leaf, then u is labeled with i and v is labeled with j for features i, j such that i < j. A decision tree is simply an FBDD whose underlying DAG is a tree. Finally, a perceptronM of dimension n is a pair (w, t) where w ∈ Rn and t ∈ R, and the classification of an instance e ∈ {0, 1}n is defined as M(e) = 1 if and only if w · e ≥ t. In this paper, we focus on the following classes of models: OBDD, the class of ordered BDDs, DTree, the class of decision trees, and Ptron, the class of perceptrons. None of these classes directly subsume the other: decision trees are not necessarily ordered, while the underlying DAG of an OBDD is not necessarily a tree. In fact, it is known that neither OBDDs can be compiled into polynomial-size decision trees nor decision trees into polynomial-size OBDDs [6, 17]. Perceptrons on the other hand can only model linear decision boundaries and thus are inherently less expressive than decision trees or OBDDs. It is also known that perceptrons cannot be compiled in polynomial time to decision trees or OBDDs unless P = NP [4].
The logic FOIL. We consider first-order logic over a vocabulary consisting of a unary predicate POS and a binary predicate ⊆. This logic is called first-order interpretability logic (FOIL), and it is our reference language for defining conditions on models that we would like to reason about. In particular, predicate POS is used to indicate the value of an instance in a model, while predicate ⊆ is used to represent the subsumption relation among partial instances. In what follows, we show that many natural properties can be expressed in a simple way in FOIL, demonstrating the suitability of this language for the purpose of expressing explainability queries.
We assume familiarity with the syntax and semantics of first-order logic (see the appendix for a review of these concepts). In particular, given a vocabulary σ consisting of relations R1, . . ., R`, recall that a structure A over σ consists of a domain, where quantifiers are instantiated, and an interpretation for each relation Ri. Moreover, given a first-order formula ϕ defined over the vocabulary σ, we write ϕ(x1, . . . , xk) to indicate that {x1, . . . , xk} is the set of free variables of ϕ. Finally, given a structure A over the vocabulary σ and elements a1, . . ., ak in the domain of A, we use A |= ϕ(a1, . . . , ak) to indicate that formula ϕ is satisfied by A when each variable xi is replaced by element ai (1 ≤ i ≤ k). Our goal when introducing FOIL is to have a logic that allows to specify natural properties of models in a simple way. In this sense, we still need to define when a modelM satisfies a formula in FOIL, as M is not a structure over the vocabulary {POS, ⊆} (so we cannot directly use the notion of satisfaction of a formula by a structure). More precisely, assuming that dim(M) = n, the structure AM associated toM is defined as follows. The domain of AM is the set {0, 1,⊥}n of all partial instances of dimension n. An instance e ∈ {0, 1}n is in the interpretation of predicate POS in AM if and only ifM(e) = 1. Finally, a pair (e1, e2) is in the interpretation of predicate ⊆ in AM if and only if e1 is subsumed by e2. Then, given a formula ϕ(x1, . . . , xk) in FOIL and partial instances e1, . . ., ek of dimension n, modelM is said to satisfy ϕ(e1, . . . , ek), denoted byM |= ϕ(e1, . . . , ek), if and only if AM |= ϕ(e1, . . . , ek). Evaluation problem. FOIL is our main tool in trying to understand how interpretable is a class of models. In particular, the following is the main problem studied in this paper, given a class C of models and a formula ϕ(x1, . . . , xk) in FOIL.
Problem: EVAL(ϕ, C) Input: A modelM∈ C of dimension n, and partial instances e1, . . . , ek of dimension n
Output: YES, ifM |= ϕ(e1, . . . , ek), and NO otherwise
For example, assume that CNF, DNF are the classes of models given as propositional formulae in CNF and DNF, respectively. If ϕ = ∃x POS(x), then EVAL(ϕ,CNF) is NP-complete and EVAL(ϕ,DNF) can be solved in polynomial time, as such problems correspond to the satisfiability problems for the propositional formulae in CNF and DNF, respectively.
Given a modelM, it is important to notice that the size of the structure AM can be exponential in the size ofM. Hence, AM is a theoretical construction needed to formally define the semantics of FOIL, but that should not be built when verifying in practice if a formula ϕ is satisfied byM. In fact, if we are aiming at finding tractable algorithms for FOIL-evaluation, then we need to design an algorithm that uses directly the encoding ofM as a model (for example, as a binary decision tree) rather than as a logical structure. In other words, in order to evaluate a query ϕ = ∃x POS(x) over a modelM of dimension n, one could certainly iterate over all 2n instances e ∈ {0, 1}n and evaluate M(e). This of course impractical for even small-dimensional data. Therefore, evaluating formulas without iterating over the entire space of (partial) instances is the main technical challenge behind the results presented in this paper.

heading: 3 Expressing Properties in the Logic
text: Basic queries. We provide some formulas in FOIL to gain more insight into this logic. Fix a model M of dimension n. We can ask whetherM assigns value 1 to some instance by using FOIL-formula ∃x POS(x). Similarly, formula ∃y (FULL(y) ∧ ¬POS(y)) can be used to check whetherM assigns value 0 to some instance, where
FULL(x) = ∀y (x ⊆ y → x = y) (1) is used to verify whether all values in x are known (that is, M |= FULL(e) if and only if e is an instance). Notice that formula FULL(y) has to be included in ∃y (FULL(y) ∧ ¬POS(y)) since M |= ¬POS(e) for each partial instance e with unknown values. Given an instance e such thatM(e) = 1, we can ask if the values assigned to the first two features are necessary to obtain a positive classification. Formally, define e{1,2} as a partial instance such that e{1,2}[1] = e{1,2}[2] = ⊥ and e{1,2}[i] = e[i] for every i ∈ {3, . . . , n}, and assume that
ϕ(x) = ∀y ((x ⊆ y ∧ FULL(y))→ POS(y)). IfM |= ϕ(e{1,2}), then the values assigned in e to the first two features are not necessary to obtain a positive classification. Notice that the use of unknown values in e{1,2} is fundamental to reason about all possible assignments for the first two features, while keeping the remaining values of features unchanged. Besides, observe that a similar question can be expressed in FOIL for any set of features.
As before, we can ask if there is a completion of a partial instance e that is assigned value 1, by using FOIL-formula ψ(x) = ∃y (x ⊆ y ∧ FULL(y) ∧ POS(y)); that is,M |= ψ(e) if and only if there is an assignment for the unknown values of e that results in an instance classified positively.
Minimal sufficient reasons. Given an instance e and a partial instance e′ that is subsumed by e, consider the problem of verifying whether e′ is a sufficient reason for e in the sense that every completion of e′ is classified in the same way as e [4, 21, 34]. The following query expresses this:
SR(x, y) = FULL(x) ∧ y ⊆ x ∧ ∀z [(y ⊆ z ∧ FULL(z))→ (POS(x)↔ POS(z))], (2) given thatM |= (e, e′) if and only if e′ is a sufficient reason for e. Finally, it can also be expressed in FOIL the condition that y is a minimal sufficient reason for x:
MSR(x, y) = SR(x, y) ∧ ∀z ((z ⊆ y ∧ SR(x, z))→ z = y). That is,M |= (e, e′) if and only if e′ is a sufficient reason for e, and there is no partial instance e′′ such that e′′ is a sufficient reason for e and e′′ is properly subsumed by e′. Minimal sufficient reasons have also been called PI-explanations or abductive explanations in the literature [20, 21, 26, 35].
Bias detection queries. Let us consider an elementary approach to fairness based on protected features, i.e., features from a set P that should not be used for decision taking (e.g., gender, age,
marital status, etc). We use a formalization of this notion proposed in [16], while noting it does not capture many other forms of biases and unfairness [27], and is thus to be taken only as an example. Given a modelM of dimension n, and a set of protected features P ⊆ {1, . . . , n}, an instance e is said to be a biased decision ofM if there exists an instance e′ such that e and e′ differ only on features from P andM(e) 6=M(e′). A modelM is biased if and only if there is an instance e that is a biased decision ofM. In what follows, we show how to encode queries relating to biased decisions in FOIL.
Let S = {1, . . . , n}, and assume that 0S is an instance of dimension n such that 0S [i] = 0 for every i ∈ S, and 0S [j] = ⊥ for every j ∈ {1, . . . , n} \ S. Moreover, define 1S in the same way but considering value 1 instead of 0, and define
MATCH(x, y, u, v) = ∀z [(z ⊆ u ∨ z ⊆ v)→ (z ⊆ x↔ z ⊆ y)]. When this formula is evaluated replacing u by 0S and v by 1S , it verifies whether x and y have the same value in each feature in S. More precisely, given a modelM and instances e1, e2 of dimension n, we have thatM |= MATCH(e1, e2,0S ,1S) if and only if e1[i] = e2[i] for every i ∈ S. Notice that the use of free variables u and v as parameters allows us to represent the matching of two instances in the set of features S, as, in fact, such matching is encoded by the formula MATCH(x, y,0S ,1S). The use of free variables as parameters is thus a useful feature of FOIL.
With the previous terminology, we can define a query
BIASEDDECISION(x, u, v) = FULL(x) ∧ ∃y [FULL(y) ∧MATCH(x, y, u, v) ∧ (POS(x)↔ ¬POS(y))].
To understand the meaning of this formula, assume that N = {1, . . . , n} \ P is the set of nonprotected features. When BIASEDDECISION(x, u, v) is evaluated replacing u by 0N and v by 1N , it verifies whether there exists an instance y such that x and y have the same values in the non-protected features but opposite classification, so that x is a biased decision. Hence, the formula
BIASEDMODEL(u, v) = ∃xBIASEDDECISION(x, u, v) can be used to check whether a modelM is biased with respect to the set P of protected features, as M satisfies this property if and only ifM |= BIASEDMODEL(0N ,1N ).
A query of the form ∃x ( POS(x) ∧ (⊥,⊥,⊥,⊥, 0, 1,⊥) ⊆ x ) was included as an initial example in Section 1. According to the formal definition of FOIL, such a query corresponds to ϕ(u) = ∃x ( POS(x) ∧ u ⊆ x ) , and the desired answer is obtained when verifying whether ϕ(e) is satisfied by a model, where e[1] = e[2] = e[3] = e[4] = ⊥, e[5] = 0, e[6] = 1 and e[7] = ⊥. Again, notice that the use of free variables as parameters is an important feature of FOIL.

heading: 4 Limits to Efficient Evaluation
text: Several important interpretability tasks have been shown to be tractable for the decision models we study in the paper [4], which has justified the informal claim that they are “interpretable”. But this does not mean that all interpretability tasks are in fact tractable for these models. We try to formalize this idea by studying the complexity of evaluation for queries in FOIL over them. We show next that the evaluation problem over the models studied in the paper can become intractable, even for some simple queries in the logic with a natural interpretability flavor. This intractability result is of importance, in our view, as it sheds light on the limits of efficiency for interpretability tasks over the models studied, and hence on the robustness of the folklore claims about them being “interpretable”. Theorem 1. There exists a formula ψ(x) in FOIL for which EVAL(ψ(x),DTree) and EVAL(ψ(x),OBDD) are NP-hard.
This result tell us that there exists a concrete property expressible in FOIL that cannot be solved in polynomial time for decision trees and OBDDs (unless P = NP). In what follows, we describe this property, and how it is represented as a formula ψ(x) in FOIL (the complete proof of Theorem 1 is provided in the appendix).
Assume that x ⊂ y is the formula x ⊆ y ∧ x 6= y that verifies whether x is properly subsumed by y. We first define the following auxiliary predicates:
ADJ(x, y) = x ⊂ y ∧ ¬∃z (x ⊂ z ∧ z ⊂ y), DIFF(x, y) = FULL(x) ∧ FULL(y) ∧ x 6= y ∧ ∃z (ADJ(z, x) ∧ ADJ(z, y)).
More precisely, ADJ(x, y) is used to check whether a partial instance x is adjacent to a partial instance y, in the sense that x is properly subsumed by y and there is no partial instance z such that x is properly subsumed by z and z is properly subsumed by y. Moreover, DIFF(x, y) is used to verify whether two instances x and y differ exactly in the value of one feature. By using these predicates, we define the following notion of stability for an instance:
STABLE(x) = ∀y [DIFF(x, y)→ (POS(x)↔ POS(y))]. That is, an instance x is said to be stable if and only if any change in exactly one feature of x leads to the same classification. Then the formula ψ(x) in Theorem 1 is defined as follows:
ψ(x) = ∃y (x ⊆ y ∧ POS(y) ∧ STABLE(y)). Hence, given a partial instance x, formula ψ(x) is used to check if there is a completion of x that is stable and positive. Theorem 1 states that checking this for decision trees and OBDDs is an intractable problem. Observe that the notion of stability used in ψ(x) has a natural interpretability flavor: it identifies positive instances whose classification is not affected by the perturbation of a single feature. Note as well that the supposed interpretability of decision trees has already been questioned and nuanced in the literature [4, 23], to which this result contributes.

heading: 5 Tractable Restrictions
text: Theorem 1 tells us that evaluation of FOIL queries can be an intractable problem, but of course this does not completely rule out the applicability of the logic. In fact, as we show in this section one can obtain tractability by either restricting the analysis to a useful syntactic fragment of FOIL, or by considering a structural restriction on the class of models over which FOIL queries are evaluated.

heading: 5.1 A tractable fragment of FOIL
text: We present a fragment of FOIL that is simple enough to yield tractability, but which is at the same time expressive enough to encode natural interpretability problems. This is not a trivial challenge, though, as the proof of Theorem 1 shows intractability of queries in a syntactically simple fragment of FOIL (in fact, only two quantifier alternations suffice for the result to hold).
Our starting point in this search is ∃FOIL, which is the fragment of FOIL consisting of all formulas where no universal quantifier occurs and no existential quantifier appears under a negation (each such a formula can be rewritten into a formula of the form ∃x1 · · · ∃xk α, where α does not mention any quantifiers). Moreover, we consider the fragment ∀FOIL of FOIL, which is defined in the same way as ∃FOIL but exchanging the roles of universal and existential quantifiers. Then we show the following: Proposition 1. Let ϕ be a query in ∃FOIL or ∀FOIL. Then EVAL(ϕ,DTree) and EVAL(ϕ,OBDD) can be solved in polynomial time.
However, the fragment ∃FOIL has a limited expressive power since, for example, the predicate FULL(x) defined in (1) cannot be expressed in it (see Appendix B for a formal proof of this claim). To remedy this, we extend ∃FOIL by including predicate FULL(x) and two other unary predicates that are common in interpretability queries. More precisely, let ALLPOS(x) and ALLNEG(x) be unary predicates defined as follows:
ALLPOS(x) = ∀y ( (x ⊆ y ∧ FULL(y) ) → POS(y)),
ALLNEG(x) = ∀y ( x ⊆ y → ¬POS(y) ) .
Then ∃FOIL+ is defined as the fragment of FOIL consisting of all formulae where no universal quantifier occurs and no existential quantifier appears under a negation, and which are defined over the extended vocabulary {POS, ⊆, FULL, ALLPOS, ALLNEG}. In the same way, we define ∀FOIL+ by exchanging the roles of universal and existential quantifiers. Notice that the formula defining the notion of sufficient reason in (2) is in ∀FOIL+. Similarly, the notion of minimal sufficient reason introduced in Section 3 can be expressed in ∀FOIL+:
MSR(x, y) = SR(x, y) ∧ ∀u [(u ⊆ y ∧ u 6= y ∧ POS(x))→ ¬ALLPOS(u)] ∧ ∀v [(v ⊆ y ∧ v 6= y ∧ ¬POS(x))→ ¬ALLNEG(v)].
In what follows, we investigate the tractability of the fragments ∃FOIL+ and ∀FOIL+. In particular, in the case of ∃FOIL+, we show that the tractability for a class of models C can be characterized in terms of the tractability in C of two specific queries in ∃FOIL+:
PARTIALALLPOS(x, y, z) = ∃u [x ⊆ u ∧ ALLPOS(u) ∧ ∃v (y ⊆ v ∧ u ⊆ v) ∧ ∃w (z ⊆ w ∧ u ⊆ w)],
and PARTIALALLNEG(x, y, z) that is defined exactly as PARTIALALLPOS(x, y, z) but replacing ALLPOS(u) by ALLNEG(u). More precisely, we have the following: Theorem 2. For every class C of models, the following conditions are equivalent: (a) EVAL(ϕ, C) can be solved in polynomial time for each query ϕ in ∃FOIL+; (b) EVAL(PARTIALALLPOS, C) and EVAL(PARTIALALLNEG, C) can be solved in polynomial time.
This theorem gives us a concrete way to study the tractability of ∃FOIL+ over a class of models. Besides, as the negation of a query in ∀FOIL+ is a query in ∃FOIL+, Theorem 2 also provides us with a tool to study the tractability of ∀FOIL+. In fact, it is possible to prove the following for the class Ptron of perceptrons. Proposition 2. The problems EVAL(PARTIALALLPOS,Ptron) and EVAL(PARTIALALLNEG,Ptron) can be solved in polynomial time.
From this proposition and Theorem 2, it is possible to establish the following tractability results for ∃FOIL+ and ∀FOIL+. Corollary 1. Let ϕ be a query in ∃FOIL+ or ∀FOIL+. Then EVAL(ϕ,Ptron) can be solved in polynomial time.
In fact, a more general corollary holds: EVAL(ϕ,Ptron) is tractable as long as ϕ is a Boolean combination of queries in ∃FOIL+ (which covers the case of ∀FOIL+). Unfortunately, these queries turn out to be intractable over decision trees and OBDDs. Proposition 3. Let C be OBDD or DTree. The problems EVAL(PARTIALALLPOS, C) and EVAL(PARTIALALLNEG, C) are NP-hard.

heading: 5.2 A structural restriction ensuring tractability
text: We now look into the other direction suggested before, and identify a structural restriction on OBDDs that ensures tractability of evaluation for each query in FOIL. This restriction is based on the usual notion of width of an OBDD [5, 9]. An OBDDM over a set {1, . . . , n} of features is complete if each path from the root ofM to one of its leaves includes every feature in {1, . . . , n}. The width of M, denoted by width(M), is defined as the maximum value ni for i ∈ {1, . . . , n}, where ni is the number of nodes ofM labeled by feature i. Then, given k ≥ 1, k-COBDD is defined as the class of complete OBDDsM such that width(M) ≤ k. By building on techniques from [9], we prove that: Theorem 3. Let k ≥ 1 and query ϕ in FOIL. Then EVAL(ϕ, k-COBDD) can be solved in polynomial time.

heading: 6 Practical Implementation
text: The FOIL language has at least two downsides from a usability point of view. First, in FOIL every query is constructed using a minimal set of basic logical constructs. Moreover, the variables in queries are instantiated by feature vectors that may have hundreds of components. This implies that some simple queries may need fairly long and complicated FOIL expressions. Second, FOIL is designed to only work over models with binary input features. These downsides are a consequence of our design decisions that were reasonable for a detailed theoretical analysis but may hamper FOIL usage in more general scenarios, in particular when models have (many) categorical or numerical input features.
In this section, we describe a simple high-level syntax and implementation of a more user-friendly language (à la SQL) to query general decision trees, and we show how to compile it into FOIL queries to be evaluated over a suitable binarization of the queried model. As a whole, the pipeline requires several pieces that we explain in this section: (i) a working and efficient query-evaluation implementation of a fragment of FOIL over a suitable sub-class of Binary Decision Diagrams (BDDs),
100 200 300 Input feature dimension
0.1
0.2
0.3
0.4
0.5
0.6
Ti m
e in
se co
nd s
100 leaves 500 leaves 1000 leaves
(a) Average time for 60 random FOIL queries over Decision Trees trained with random data.
100 200 300 Input feature dimension
0.0
0.5
1.0
1.5
2.0
2.5
Ti m
e in
se co
nd s
100 leaves 500 leaves 1000 leaves
(b) Maximum time for 60 random FOIL queries over Decision Trees trained with random data.
> exists student, student.age <= 18 and (student.internetAtHome or student.male) and
goodGrades(student)
(c) Example of a query in our system executed over a model trained in the dataset in [29].
Figure 2: Execution time for FOIL queries and a high-level practical syntax.
(ii) a transformation from the high-level syntax to FOIL queries, and (iii) a transformation from a general decision tree to a BDD over which the FOIL query can be efficiently evaluated. We only present here the main ideas and intuitions of the implemented methods. A detailed exposition along with our implementation and a set of real examples can be found in the supplementary material.
6.1 Implementing and testing core FOIL
We implemented a version of the algorithm derived from Section 5.1 for evaluating existential and universal FOIL queries that is proven to work over a suitable sub-class of BDDs. The method receives a query as a plain text file and a BDD in JSON format. We tested the efficiency of our implementation varying three different parameters: the number of input features, the number of leaves of the decision tree, and the size of the input queries. We created a set of trees trained with random input data with input feature dimensions in the range [10, 350], and of 100, 500 and 1000 leaves (24 different decision trees). We note that the best performing decision trees over standard datasets [37] rarely contain more than 1000 total nodes [25], thus the trees that we tested can be considered of standard size. We created a set of random queries with 1 to 4 quantified variables, and a varying number of operators (60 different queries). We run every query 5 times over each tree, and averaged the execution time to obtain the running time of one case. From all our tests no case required more than 2.5 seconds for its complete evaluation with a total average execution time of 0.213 seconds and standard deviation of 0.169 in the whole dataset. Figure 2a shows the average time (average over different queries) for all settings. We observed that some queries where specially more time consuming than others. Figure 2b shows the maximum execution time over all queries for each setting. The most important factor when evaluating queries is the number of input features, which is consistent with a theoretical worst case analysis. All experiments where run on a personal computer with a 2.48GHz Intel N3060 processor and 2GB RAM. The exact details of the machine are presented in the supplementary material.

heading: 6.2 Interpretability symbolic queries in practice
text: High-level features. We designed and implemented a prototype system for user-friendly interpretability queries. Figure 2c shows a real example query that can be posed in our system for a model trained over the Student Performance Data Set [29]. Notice that our syntax allow named features, names for the target class (goodGrades in the example) and the comparison with numerical thresholds which goes beyond the FOIL formalization. Our current implementation allows for numerical and logical comparisons, as well as handy logical shortcuts such as implies and iff. Moreover we implemented a wrapper to directly import Decision Trees trained in the Scikit-learn [30] library.
Binarizing models and queries. One of the main issues when compiling these new queries into FOIL is how to binarize numerical features. Choi et al. [12] describe in extensive detail an approach to encode general decision trees into binary ones. The key observation is that one can separate numerical values into equivalence classes depending on the thresholds used by a decision tree. For example, assume a tree with an age feature that learns nodes with thresholds age ≤ 16 and age ≤ 24. It is clear that such a tree cannot distinguish an age = 17 from an age = 19. In general, every tree induces a finite number of equivalence classes for each numerical feature and one can take advantage of that to produce a binary version of the tree [12]. In our case, we also need to take the query into account. For instance, when evaluating a query with a condition student.age <= 18, ages 17 and
19 become distinguishable. Considering all these thresholds we have intervals (−∞, 16], (16, 18], (18, 24], (24,∞) and we can use four binary features to encode in which interval an age value lies. It is worth noting that this process creates extra artificial features, and thus, the decision tree that learned real thresholds needs to be binarized in the new feature space accordingly. One can show that a naive implementation would imply an exponential blow up in the size of the new tree. To avoid this our binarization process transforms the real-valued decision tree into a binary FBDD, over which we prove that our polynomial algorithms from Section 5.1 are still applicable.
Performance tests. We tested a set of 20 handcrafted queries over decision trees with up to 400 leaves trained for the Student Performance Data Set [29], which combines Boolean and numerical features. Our results show that natural queries can be evaluated over decision trees of standard size [25] in less than a second on a standard personal machine, thus validating the practical usability of our prototype.

heading: 7 Final Remarks and Future Work
text: In several aspects the logic FOIL is limited in expressive power for interpretability purposes. This was a design decision for this paper, in order to start with a “minimal” logic that would allow highlighting the benefits of having a declarative language for interpretability tasks, and at the same time allowing to carry out a clean theoretical analysis of its evaluation complexity. However, a genuinely practical declarative language should include other functionalities that allow more sophisticated queries to be expressed. As an example, consider the notion of SHAP-score [24] that has a predominant place in the literature on interpretability issues today. In a nutshell, for a decision modelM with dim(M) = n and instance e ∈ {0, 1}n, this score corresponds to a weighted sum of expressions of the form #POSS(e), for S ⊆ {1, . . . , n}, where #POSS(e) is the number of instances e′ for which M(e′) = 1 and e′ coincides with e over all features in S. Expressing this query, hence, requires extending FOIL with a recursive mechanism that permits to iterate over the subsets S of {1, . . . , n}, and a feature for counting the number of positive completions of a partial instance; e.g., in the form of a “numerical” query φ(x) := #y.(x ⊆ y ∧ POS(y)). Logics of this kind abound in computer science logic (c.f., [2, 22]), and one could use all this knowledge in order to build a suitable extension of FOIL for dealing with this kind of interpretability tasks. One can also envision a language facilitating the comparison of different models by providing separate POS predicates for each of them. Then, for example, one can ask whether two models are equivalent, or if they differ for a particular kind of instances. Such an extension can affect the complexity of evaluation in nontrivial ways.
Arguably, interpretability measures the degree in which humans can understand decisions made by machines. One of our main calls in this paper is to build more symbolic interpretability tools, and thus, make them closer to how humans reason about facts and situations. Having a symbolic high-level interpretability language to inspect ML models and their decisions is thus a natural and challenging way of pursuing this goal. We took a step further in this paper presenting theoretical and practical results, but several problems remain open. A particularly interesting one is whether a logical language can effectively interact with intrinsically non-symbolic models, and if so, what mechanisms could allow for practical tractability without sacrificing provable correctness.
Acknowledgments and Disclosure of Funding
This work was partially funded by ANID - Millennium Science Initiative Program - Code ICN17_002. Arenas is funded by Fondecyt grant 1191337, while Barceló and Pérez are funded by Fondecyt grant 1200967.

Review summaries:
The authors propose a declarative, logic-based language to query machine learning models. The language is tailored to a syntax and semantics that supports queries that explore the behaviour of the machine learning model. For instance, using Pos(e) as an atom that expresses that input e (which might contain undefined arguments) is a positive example, that is, an example classified as positive by the ML model, and using predicates for individual features such as “married” and “has kids”, one could query whether the model under consideration would give a loan to a person who is married and does not have kids.  Given such a logical language, it is natural to ask what the complexity of answering queries in the languages are and to restrict the language in ways that make queries tractable. This is what the authors set out to do in the submitted paper. 

This paper introduces a simple logic for examining classifiers. It shows 1) The logic allows defining, in particular, a predicate capturing (minimal) sufficient reason explanations (i.e., a set of feature values that ensure the classifier gives a certain classification) and a predicate indicating whether the classifier makes a decision using a protected set of features. 2) The most natural version of the logic allows defining a predicate that is NP-hard to evaluate for both decision tree and OBDD classifiers 3) A simple fragment of the logic is adequate to capture the formulas indicated in (1), and there are two formulas such that if these can be evaluated in polynomial time for a model class, then the entire fragment is polynomial time 4) The fragment in (3) is polynomial-time decidable for decision trees and OBDDs (on account of the indicated criterion) 5) A restricted kind of OBDD allows the more general logic to be decided in polynomial time.

The authors present a logical language, called FOIL, in which many simple yet relevant interpretability queries can be expressed. They go on to study the computational complexity  of FOIL queries over two classes of ML models often deemed to be easily interpretable: decision trees and OBDDs.   The authors show that despite claims of the good level of interpretability for models such as DTs and OBDDs, there is a simple query in FOIL that is  intractable over them. The authors go on to to define two tractable fragments of FOIL.