Foundations of Symbolic Languages for Model Interpretability
Authors: Marcelo Arenas
Daniel Báez
Pablo Barcelo
Jorge Pérez
Bernardo Subercaseaux
Venue: NeurIPS 2021 Spotlight (2021)
Keywords: language
interpretability
logic
complexity
decision trees
explainability

Abstract: Several queries and scores have recently been proposed to explain individual predictions over ML models. Examples include queries based on “anchors”, which are parts of an instance that are sufficient to justify its classification, and “feature-perturbation” scores such as SHAP. Given the need for flexible, reliable, and easy-to-apply 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, which 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 two 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.

Foundations of Symbolic Languages for Model Interpretability
Marcelo Arenas Daniel Baez², Pablo Barcel6 ,oorge Pérez Bernardo Subercaseaux
Department of Computer Science, PUC-Chile Institute for Mathematical and Computational Engineering, PUC-Chile
3 Department of Computer Science, Universidad de Chile
Millennium Institute for Foundational Research on Data, Chile Carnegie Mellon University, USA
[marenas, pbarcelo] Bing. puc. cl, jperezedce uchile. cl,, bsuberca@andress cmm, edu
Abstract
Several queries and scores have been proposed to explain individual predictions made by ML models. Examples include queries based "anchors", which are parts of an instance that are sufficient to justify its classification, and "feature- perturbation" scores such as SHAP. Given the need for flexible, reliable, and easy-to apply interpretability methods for ML models, we foresee the need for developing declarative languages to naturally specify different explainability queries. We do this in principled way by rooting such 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 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 prototype implementation of FOIL wrapped in hevel declarative language, and perform experiments showing that such a language can be used in practice.
its dimension,
Introduction
Context. The degree of interpretability of machine learning (ML.) model seems to be intimately related with the ability to "answer questions" about it. Those questions 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 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).
by now clear that ML interpretability admits no silver- [18], and that in many cases a combination of different queries may be the most effective way to understand model's behavior. Also, model interpretability takes different flavors depending on the application domain one deals with. This naturally brings the picture the need for ceneral-purpost specification languages that can provide flexibility and expressiveness to practitioners specifying interpretability queries. An advanced requirement for these languages is to be relatively easy to 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 (NcurIPS 2021).

---

(oad."ml..np" as MyModel; show features; (stableJob, , >40yo, prevLoan, ownsHouse, hasKids, isMarried, crimRecord); Boolean show classes;
Stahle joh 40yo
Previous loans
Black Box Model
Application Rejected
Rejected (0), Accepted (1)
Owns house
Has kids
Married
exists person, person.isMarries isMarried and not person hasKids and MyModel (person) = Accepted;
Criminal Record
(a) Diagram a particular loan decision.
YES
(b) Example of possible concrete syntax for language tailored for interpretability queries.
Figure 1: Example of a bank that uses model to decide whether to accept loan applications considering binary features like "does the requester have stable job" and "are they older than 40"?
One way 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 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, c.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 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 logical language, called FOIL. in which many simple yet relevant interpretability queries can be expressed. We believe that FOIL can further serve basis over which more expressive interpretability languages can be built, and propose concrete directions of research towards its expansion. In a nutshell, given a decision model M that performs classification over instances 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 undefined. Such undefined features take a distinguished value 1. An instance is full if none of its features is undefined. The logic FOIL is simply first-order logic with access to the of all instances (partial full) of dimension n: unary predicate Pos(e), stating that e is a full instance that M classifies as positive, and a binary predicate e C e', stating that instance e' potentially fills some of the undefined features of instance e e.g. (1, 0, 1) (1, 0, 1), but (1, 0, 1) & (1, 1, 1).
two predicates
As an overview of our proposal, consider the case of a bank using binary model judge applications for loans. Figure la illustrates the problem with concrete features, and Figure 1b presents an example of 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 l (Pos(x) A I,, 1, C r).
Theoretical contributions. The evaluation problem for fixed FOIL. query yp is as follows. Given a decision model M, is it true that yp is satisfied under the interpretation of predicates S and Pos defined above? An important caveat about this problem is that, in order to evaluate ip, 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 Er (z)( which asks if M 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 {zPos(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 (h) 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 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 FFIIL, 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 3FOIL with 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 FFOIL+ 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 F 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 I
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 (p, for yo 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 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 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 introduce 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 subelass 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.
A Logic for Interpretability Queries
Background. An instance of dimension n, with 2 1, is tuple E 10, We use notation eji] to refer to the i-th component of this tuple. or cquivalently, its i-th feature. Morcover, we consider abstract notion of model of dimension n, and we define it as Boolean function M: : {0, 13" + {0, 1). That is, MM 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 dM) for the dimension of model M.
A partial instance of dimension n is a tuple e E {0, 1, 1, Intuitively, if e|i] = L, then the value of the i-th feature is undefined. Notice that an instance is particular case of partial instance where all features are assigned value either 0 or 1. Given two partial instances e,, e2 of dimension n, we say
that e; is subsumed by e2 if for every i E {1, (I.....7.) such that ej * L. it holds that e [i] = ez[i].
3

---

That is. e₁ is subsumed by e2 if it is possible to obtain ea from e, 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 rooted directed acyclic graph M 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) labeled with a feature i E [I,...,, n):: and (iii) each internal node has two outgoing edges, one labeled 1 and the another one labeled 0. Every instance e E {0, 1)"h defines a unique path me = U1 ... Uy from the root i1 to a leaf ug of M such that: if the label of u; is E {l.....II n), ..), where i E fl..... k 1), then the edge from u, to 24+1 labeled with elj]. Moreover, the instance e is positive, denoted by M(()) = if the label of us is true; otherwise the instance is negative, which is denoted by MMe) = O. A binary decision diagram M 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.....,) ] of features such that, if a node u appears before a node v in some path in MM from the root to leaf, then u is labeled with and is labeled with j for features i, such that i < j. A decision tree is simply an FBDD whose underlying DAG is a tree. Finally, a perceptron M of dimension n is a pair (w, E) where w E IR" and & E IR, and the classification of an instance e E 10, is defined as M(e) = if and only if w e 2 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 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 binary predicate S. This logic is called first-order interpretability logic (FÓIL), and is our reference language for defining conditions on models that we would like to reason about. In partieular, predicate POS is used to indicate the value of an instance in model, while predicate C is used to represent the subsumption relation among partial instances. In what follows, we show that many natural properties can be expressed in 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 review of these concepts). In particular, given a vocabulary consisting of relations Rq...., Rr recall that a structure 2 over a consists of domain, where quantifiers are instantiated, and an interpretation for each relation R,, Moreover, given first-order formula defined over the vocabulary a,, we write p( xx) to indicate that (x1,... 3 is the set of free variables of p.. Finally, given a structure Al over the vocabulary and elements a1. ... ag in the domain of 21, we use 2 F sp(a).... ax) to indicate that formula &p satisfied by when each variable 2; is replaced by element a; (1 S S k)).
Our goal when introducing FOIL is to have a logic that allows to specify natural properties of models in simple way. In this sense, we still need define when a model M satisfies a formula in FOIL, as M is not a structure over the vocabulary {Pos. C} (so we cannot directly use the notion of satisfaction of formula by structure). More precisely, assuming that dim(M) n,, the structure 21 associated to M is defined as follows. The domain of 2[ is the set {0, 1. of all partial instances of dimension n. An instance e 10.1)" " is in the interpretation of predicate Pos in 2| if and only if M(e)= = 1. Finally, a pair (e1, e2) is in the interpretation of predicate C in AM if and only if e subsumed by 02. Then, given a formula (p( .rx) in FOIL. and partial instances 0j, ex),
..... of dimension n, model M is said to satisfy plc1..... ek), denoted by M F if and only if A F pp(c,....,
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 pf
Fx) ) in FOIL.

---

Problem:
EVAI,(p,, C) Input: A model M E C of dimension n, and partial instances e1, YES, if M - plee..... 0x), and No otherwise
of dimension y!
Output:
For example, assume that CNF, DNF are the classes of models given as propositional formulae in CNF and DNF, respectively. If o = Er (os(z), then (y, CNF) NP-complete and (v, 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 model M, it is important to notice that the size of the structure MM can be exponential in the size of M. Hence, MM is theoretical construction needed formally define the semantics of FOIL. but that should not be built when verifying in practice if a formula y is satisfied by M. In fact, if are aiming finding tractable algorithms for FOlL-evaluation, then need to design an algorithm that uses directly the encoding of M as a model (for example, as a binary decision tree) rather than as a logical structure. In other words, in order evaluate a query o Er (os( over a model M of dimension n. one could certainly iterate over all 2" instances E {0, 3r and evaluate M(e). This of course impractical for even mmall-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.
3 Expressing Properties in the Logic
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 whether M assigns value to some instance by using FOIL-formula Er (as( Similarly, formula By (FULLI(V) A -Pos(y)) can be used to check whether M assigns value 0 to some instance, where
FULL(x) = vy(=ay-z=E)
is used to verify whether all values in 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 By (FUll(y) -Pos(y)) since M -Po((e) for each partial instance with unknown values.
Given instance such that M(e) 1, we ask if the values assigned to the first two features are necessary to obtain a positive classification. Formally, define e(1.2) as partial instance such that ((1.2) C1, [2] = and (1.2)) [0] = cli] for every i E (3....,n n.). and assume that Vy ((x C y A FULL(y))
(la)
Pos()))
M F ()((),))) 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 similar question can be expressed in FOIL for any set of features.
As before, we can ask if there is completion of a partial instance that is assigned value by using FOIL-formula (xx) By (x C y A FULL(y) A Pos(y)); ); that is, M }= (e) if and only if there is an assignment for the unknown values of e that results 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 sufficient reason for in the sense that every completion of e' is classified in the same way as e [4, 21, 34j. The following query expresses this:
SR(r, v) = (ULL(E) A C A ((v C = FU)L(())) > (Pos(x) ++ Pos(=))], (2)
given that M F (e, if and only if e' is sufficient reason for e. Finally, it can also be expressed in FOIL the condition that y is a minimal sufficient reason for x::
ASR(r.8) = SR(2,8) v) A V2 ((2 S SR(2, 2)) + 2 2= =)
That is, M MF (c, c') if and only if e' is 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 Pl-explanations or abductive explanations in the literature [20, 21, 26, 35].
Bias detection queries. Let us consider an elementary approach to faimness based on protected features, i.c., features from a set P that should not be used for decision taking (c.g., gender, age,
5

---

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 be taken only as an example. Given a model .M of dimension n, and a set of protected features P C (I,...,7 ) ", an instance said to be a biased decision of M if there exists an instance e' such that e and e' differ only on features from P and (())) * MMee). A model M is biased if and only if there is an instance
that is a biased decision of M. In what follows, we show how to encode queries relating to biased decisions in FOIL.
Let S fI...... n.. and assume that 0g is an instance of dimension n such that Os for every i E S. and Os = 1 for every E {1....,,) n) S. Moreover, define 1g in the same way but considering value instead of 0, and define
MATCH((E, y, u, v) = Vz C u - - ( Ev)].
When this formula is evaluated replacing by Oş and by 1s, it verifies whether x and y have the same value each feature in S. More precisely, given a model M and instances e1, 02 of dimension n, we have that M - MATCH(e), e2 Os, 1s) if and only if e [i] = e2li] for every E S. Notice that the use of free variables u and v as parameters allows us to represent the matching of two instances in the of features S, as, in fact, such matching encoded by the formula MATCH(2, y, Os, 1s). The use of free variables as parameters is thus a useful feature of FOIL.
With the previous terminology, we can define query
BIASEDDECCISION(;; u, = FUILL(a))
By (FULL()) A MATCH( y, v) A (PoS(x) +> -PoS()))]
To understand the meaning of this formula, assume that N (1..... n) \ P is the set of non- protected features. When BIASEDDECISIONS (x. v) is evaluated replacing u by Oy and v by 1x. it verifies whether there exists an instance y such that and y have the same values in the non-protected features but opposite classification, so that is a biased decision. Hence, the formula
BIASEDMODEL(11, v) =
3x BIASEDDECISION((: u,
can be used to check whether model M is biased with respect to the set P of protected features, as M satisfies this property if and only if M = BIASEDMODEL 1x).
A query of the form 3z (PoS(æ) A (L, 1,, in Section 1. According to the formal definition of FOIL, such a query corresponds to ppu)) = Ar (P)s(x) A u S x),, and the desired answer is obtained when verifying whether (p(e) is satisfied by a model, where e[1] = e[2] e(33 = e[4] = L. e(5] = 0, e(6] = 1 and e(7] = L. Again, notice that the use of free variables as parameters is important feature of FOIL.
2) was included an initial example
4 Limits to Efficient Evaluation
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 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 (VAL()( DTree) and (vAL()(z), 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 NP). In what follows, we describe this property, and how it is represented as a formula ((()) in FOIL (the complete proof of Theorem is provided in the appendix).
Assume that x C y is the formula x S y A + y that verifies whether x is properly subsumed by y. We first define the following auxiliary predicates:
v) = x C y A3x (x C 22 C y): DIFF(Z,)) = FULL(z) A FULL A I # AV (ADI(2,2) A ADJ(Z,))).

---

More precisely, ADJ(z, y) is used to check whether partial instance is adjacent to a partial instance y, in the sense that properly subsumed by y and there is no partial instance such that x properly subsumed by and is properly subsumed by Moreover, DIFF(I, y) is used to verify whether two instances a 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(T)
Vy DiFF(I, y) (Pos(x) Pos(y))]
That is, an instance 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 (xx) in Theorem is defined follows:
(x) = By (æ S y A Pos(y) A STABLE(y)).
Hence, given a partial instance æ, formula (xr is used to check if there is completion of x that is stable and positive. Theorem states that checking this for decision trees and OBDDs an intractable problem. Observe that the notion of stability used in vb(x) has natural interpretability flavor: it identifies positive instances whose classification is not affected by the perturbation of 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.
Tractable Restrictions
Theorem tells us that evaluation of FOIL queries can be an intractable problem, but of course this does not completely rule out the applicability the logic. fact, as we show this section one can obtain tractability by either restricting the analysis to useful syntactic fragment of FOIL, or by considering a structural restriction on the class models over which FOIL queries are evaluated.
5.1 A tractable fragment of FOIL
We present 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 not trivial challenge, though, as the proof of Theorem shows intractability of queries in a syntactically simple fragment of FOIL (in fact, only two quantifier alternations suffice for the result hold).
Our starting point in this search is FFOIL, which is the fragment of FOIL consisting of all formulas where no universal quantifier occurs and existential quantifier appears under negation (each such a formula can be rewritten into a formula of the form 3z, ... Foy o, where a does not mention any quantifiers). Moreover, we consider the fragment YFOIL of FOIL, which defined in the same way as =FOIL but exchanging the roles of universal and existential quantifiers. Then we show the following:
Let yp be query in FFOII. or AFOIL. Then EVAL( DTree) and EvAL OBDD) OBDDD) can be solved in polynomial time.
Proposition 1.
However, the fragment 3FOIL has limited expressive power since, for example, the predicate FULL,(x) defined in (1) cannot be expressed (see Appendix B for a formal proof of this claim). To remedy this, we extend 3FOIL by including predicate FULL(x) and two other unary predicates that are common in interpretability queries. More precisely, let ALLPOS(z) and ALLNEG(x)) be unary predicates defined as follows:
ALLPOs(x) Vy ((x S A A (U) Pos(y)),
ALLNEG(x) Vy (1 Cy -Pos(y))
Then 3FOIL+ + defined as the fragment of FOIL consisting quantifier occurs and no existential quantifier appears under negation, and which are defined over the extended vocabulary (Pos, S. FULL, ALLPOS, ALLNEG). In the same way, we define YFOIL* by exchanging the roles of universal and existential quantifiers. Notice that the formula defining the notion of sufficient reason in (2) is in VFOIL* Similarly, the notion of minimal sufficient reason introduced in Section can be expressed in VFOII+:
formulae where no universal
MSR (2r v) = SR(a, v) A Vu [(u Cy Au # y A POS(s)) + ALLPOS(u)) A
Vel(v C -Pos(2) + -ALLNEG())].
7

---

In what follows. we investigate the tractability of the fragments EFOIL" + and AFOIL". In particular, in the case of =FOIL* we show that the tractability for class of models C can characterized in terms of the tractability in C of two specific queries in FFOIL*:
PARTIALALL.PO((4: y, Bu [a S a ALL (u)) A
EF (u S U EVAuç A Bu S A S [w], and PARTIALALL.NEO(, 2, that is defined exactly as PARTIAL.ALLPOS(r,, 2) but replacing AL.) by ALI.NEG(U). More precisely, we have the following:
Theorem 2. For every class C of models, the following conditions are equivalent: (a) EVAL(p, C) can be solved in polynomial time for each query in 3FOIL* : (b) EYAL(PARTIALALLPOS, C)) and BVAL(PARTTALLLLNEGG C) can be solved in polynomial time.
This theorem gives us concrete way study the tractability of 3FOIL* over class of models. Besides, as the negation of a query in VFOIL* a query in JFOIL Theorem also provides us with tool to study the tractability of VFOIL". In fact, it is possible to prove the following for the class Ptron of perceptrons.
Proposition
2. The problems
EVAL(PARTIALALLPOS, Ptron)
and
EVAL(PARTIALALLNEGG Ptron) can be solved in polynomial time.
From this proposition and Theorem 2, is possible establish the following tractability results for EFOIL* and VFOIL*
Corollary 1. Let be a query in 3FOIL* + or VFOIL* Then EVAL(yP, Ptron) can be solved in polynomial time.
In fact, a more general corollary holds: EV,L( Ptron) is tractable as long as yp Boolean combination of queries 3FOIL* (which covers the case of VFOIL Unfortunately, these queries turn out to be intractable over decision trees and OBDDs.
Proposition 3. Lei C be OBDD or DTree. The problems BVAL(PARTIALALLPOS, and EAA.PPARTALLLLLNE,, C) are NP-hard.
5.2 A structural restriction ensuring tractability
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 the usual notion of width of an OBDD [5. 9]. An OBDD M over a set {1....,,) n of features is complete each path from the root of M one of its leaves includes every feature in {1,.... ........ n). The width of M, denoted by width(M] is defined as the maximum value n; for i E {1..... n). where n, is the number of nodes of M labeled by feature i. Then, given & 2 1, k-COBDD is defined as the class of complete OBDDs M such that width(MM & k. By building on techniques from [9], we prove that:
Theorem 3. Let 2 and query ip FOIL. Then (vAL(p,k-COBDE can be solved in polyno- mial time.
6 Practical Implementation
The FOIL. language has at least two downsides from a usability point of view. First, in FOIL every query is constructed using 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 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 simple high-level syntax and implementation of more user-frient buer-friendly language (ă SQL) to query general decision trees, and we show how to compile into FOIL queries to be evaluated over 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 suitable sub-class of Binary Decision Diagrams (BDDs),
8

---

1.5
Sid baten
lores HB0 lanis
Time in sec2nds
secrends
exists student, student, age <= 18 and (student internetAtHome student.mal male)) and (studdent))))
414
0.5
03
6.0
303
Input feature dimension
200 301
Input feuture dimension
331 300
(c) Example of query in sys- executed over model trained in dataset in [29].
(a) Average time for 60 random FOIL queries over Decision Trees trained with random data.
Maximum time for 60 random FOIL queries over Decision Trees
trained with random data.
Figure 2: Execution time for FOIL queries and a high-level practical syntax.
(ii) a transformation from the high-level syntax FOIL queries, and (iii) a transformation from 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 query plain text file and 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 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 more than 1000 total nodes [25], thus the trees that we tested can be considered of standard size. We created 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 case required more than 2.5 seconds for its complete evaluation with 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 theoretical worst case analysis. All experiments where run on personal computer with a 2.48GHz Intel N3060 processor and 2GB RAM. The exact details of the machine are presented in the supplementary material.
over standard datasets [37] rarely contain
6.2 Interpretability symbolic queries in practice
High-level features. We designed and implemented a prototype system for user-friendly interpretabil- ity queries. Figure 2c shows real example query that can be posed in our system for model trained over the Student Performance Data Ser [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 impl ies 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 how to binarize numerical features. Choi 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 tree with age feature that learns nodes with thresholds age S 16 and age < 24. clear that such a tree cannot distinguish an age 17 from an age 19. In general, every tree induces 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]. our case, we also need to take the query into account. For instance, when evaluating query with condition student. age <= 18, ages 17 and

---

19 become distinguishable. Considering all these thresholds we have intervals (- 16], (16, 18). (18, 24), (24, oo) and we can use four binary features 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 binarized 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 second on a standard personal machine, thus validating the practical usability of our prototype.
7 Final Remarks and Future Work
In several aspects the logic FOIL is limited in expressive power for interpretability purposes. This was design decision for this paper, in order to start with "minimal" logic that would allow highlighting the benefits of having declarative language for interpretability tasks, and at the same time allowing to carry out clean theoretical analysis of its evaluation complexity. However, 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 model M with (MM and instance e É {0, 13"h this score corresponds the form # #PoSs(c)) for S S {1...., m), where #Poss (e) is the number of instances e' for which M(c') 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 feature for counting the number of positive completions of a partial instance; e.g., in the form of a "numerical" query <(x)) == #y.(x C A (os( Logics of this kind abound in computer science logic (c.f., [2, 22 and one could use all this knowledge in order to build 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.
weighted sum of expressions of
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 MI. models and their decisions is thus 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. particularly interesting one is whether 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 - Millenniin Science Initiative Program Code ICN17_(M) 000.. Arenas is funded by Fondecyt grant 1191337, while Barceló and Pérez are funded by Fondecyt grant 1200967.
References
[1] S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995.
[2] M. Arenas, M. Muñoz, and C. Riveros. Descriptive complexity for counting complexity classes. Logical Methods in Computer Science; ; Volume 16, pages Issue 1 1860-5974 2020.
[3] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003,
10

---

[4] P. Barceló, M. Monet, J. Pérez, and B. Subercaseaux. Model interpretability through the lens of computational complexity. In NeurIPS, 2020.
[5] B. Bollig. On the width of ordered binary decision diagrams, In COCOA, pages 444-458, 2014.
[6] Y. Breitbart, H. Hunt, and D. Rosenkrantz. On the size of binary decision diagrams representing boolean functions. Theoretical Computer Science, 145(1-2):45 69, July 1995.
[7] R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677-691, Aug. 1986.
[8] F. Capelli and S. Mengel. Knowledge compilation, width and quantification. CoRR. abs/1801 hts/1807.0k 0.26604463, 2018.
[9] Capelli and S. Mengel. Tractable QBF by Knowledge Compilation. In STACS, pages 18:1-18: 16, 2019.
[10] H. Chan and A. Darwiche. Reasoning about bayesian network classifiers. In UAI, pages 107-115, 2003.
[11] C. C. Chang and H. J. Keisler. Model theory. Elsevier, 1990.
[12] A. Choi, A. Shih, A. Goyanka, and A. Darwiche. On symbolically encoding the behavior of random forests. CoRR, Abs/2007.01499. 2020.
[13] A. Choi, R. Wang, and A. Darwiche. On the relative expressiveness of bayesian and neural networks. Int. J. Approx. Reason., 113:303-323, 2019.
[14] K. Chubarian and G. Turán. Interpretability of bayesian network classifiers: OBDD approxima- tion and polynomial threshold functions. In ISAIM, 2020.
[15] E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press, 2001.
[16] A. Darwiche and A. Hirth. On the reasons behind decisions. In ECAL, pages 712-720, 2020.
[17] A. Darwiche and P. Marquis. A knowledge compilation map. Journal of Artificial Intelligence Research, 17:229-2666 264, Sept. 2002.
[18] F. Velhi-Velez and B. Kim. Towards rigorous science of interpretable machine learning. 2017.
[19] L. H. Gilpin, D. Bau, B. Z. Yuan, A. Bajwa, M. Specter, and L. Kagal. Explaining explanations: An overview of interpretability of machine learning. In DSAA, pages 80-89, 2018.
[20] A. Ignatiev, N. Narodytska, and J. Marques-Silva. Abduction-based explanations for machine learning models. CoRR, abs/1811 1811116656 2018.
[21] Y. Izza, A. Ignatiey, and J. Marques-Silva. On explaining decision trees. CoRR, abs/2010.11034,, 2020.
[22] L. Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.
[23] Z. C. Lipton. The mythos of model interpretability: In machine learning, the concept of interpretability is both important and slippery. Queue, 16(3):31-57, June 2018.
[24] S. M. Lundberg and S. Lee. A unified approach to interpreting model predictions. In NIPS, pages 4765 4774, 2017.
[25] R. G. Mantovani, T. Horváth, R. Cerri, S. B. Junior, J. Vanschoren, and A. C. P. de Leon Ferreira de Carvalho. An empirical study on hyperparameter tuning of decision trees. CoRR, abs/1812.02201 2018
[26] J. Marques- T. Gerspacher, M. C. Cooper, A. Ignatiev and N. Narodytska. Explaining naive bayes and other linear classifiers with polynomial time and delay. In H. Larochelle, M. Ranzato, R. Hadsell, M. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information P Processing Systems 2020, NeurIPS 2020, December 6- 6-1 2020, virtual, 2020.

---

[27] N. Mehrabi, F. Morstatter, N. Saxena, K. Lerman, and A. Galstyan. A survey on bias and fairness in machine learning, ACM Comput. Surv., 54(6), July 2021.
[28] C. Molnar.
Interpretable Machine Learning.
2019.
nttps://christophe github. wttp///tteerretaaeeell--ooooeooo
[29] F. Pagnotta and H. M. Amran. Using data mining predict secondary school student alcohol consumption, 2016.
[30] Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, Prettenhofer, R. Weiss, V. Dubourg. J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12:2825-2830, 2011.
[31] M. T. Ribeiro, Singh, and Guestrin. "why should trust you?": Explaining the predictions of any classifier. In SIGKDD, pages 1135-1144, 2016.
[32] M. T. Ribeiro, S. Singh, and C. Guestrin. Anchors: figh-precision model aadel-agnostic explanations.
In AAAI, pages 1527-1535, 2018.
[33] C. Rudin. Please stop explaining black box models for high stakes decisions. CoRR, abs/1811.10154 2018.
[34] A. Shih, A. Choi, and A. Darwiche. symbolic approach to explaining bayesian network classifiers. In J. Lang, editor, Proceedings of the Twenty-Sevent International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 5103-5111, 2018.
[35] A. Shih, A. Choi, and A. Darwiche. A symbolic approach to explaining bayesian network classifiers, 2018.
[36] E. Strumbelj and Kononenko. An efficient explanation individual classifications using game theory. J. Mach. Learn. Res., 11:1-18, 2010.
[37] Vanschoren, N. Van Rijn, B. Bischl, and L. Torgo. Openml: networked science in machine learning. ACM SIGKDD Explorations Newsletter, 15(2):49-60, 2014.
[38] I. Wegener. Bdds: design, analysis, complexity, and applications. Discrete Applied Mathematics, 138(1-2):229 251, 2004.
12


Reviews:
[{"review_id": "pho2_JcXbZb", "reviewer": "Reviewer_tR2Z", "summary": "This paper proposed a query language that can be used to ask yes/no questions of a model. The language was investigated for OBDDs and decision trees.", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "The main problem with this paper is that it claims to be about interpretability, but I can't see how the proposed query language is more interpretable than say the original decision tree or OBDD.  Why is asking Boolean questions helpful for interpretability? It might be obvious to you, but isn't to me. Please give some concrete use cases. (As an example, one use case might be to able to explain why some examples in a test set are given the classification thay were given.) For any complete case, it gives the same answer as the model.\n\nOriginality. The paper is moderately original; there is not a lot of novel content. I was surprised that you did not have two sorts of queries: \"could\" an instance of this query be positive and \"must\" an instance of this partial query be positive. (I realize the logic can hadle this, but you then don't go and propose what would be a usable language for someone else to use to query a model).\n\nQuality: The quality is reasonable; it just doesn't do vey much.\n\nClarity: That paper is reasonably clear.\n\nSignificance:  This is very low. I can't imagine anyone using this for anything useful.\n\nGiven theorem 1, I would think that you would redesign FOIL.  Give a formalism such as a decision tree that is already very interpretable (OBDDs no so much), it seems strange to want to ask complicated queries over them and then claim it is about interpretability.\n\nFor a top conference like NeurIPS, there needs to be a concrete result. Average time for simple queries as a function of input dimensions is not a very interesting result. (Why is it so slow?)  If the claims are about interpretability, then the results should be about interpretability. Have other users tried to interpret the results?\n\nI don't think NeurIPS is the right venue for this paper. The style of theorems would be more suited to a conference like KR.\n\nOverall, I am sceptical that  giving yes/no answers is useful for interpretability. You assume that it is true, but never justify it.\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Yes", "review_text": "", "extra_scores": {"ethical_concerns": "No issues I saw.", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "2"}, "extra_text": {}}, {"review_id": "Yfv2wkcPpSO", "reviewer": "Reviewer_WuQH", "summary": "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.\n\nGiven 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. ", "questions": "", "limitations": "", "rating": 7, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "The motivation for the problem under consideration and the general writing style is fantastic. Despite its somewhat “exotic” topic for a machine learning conference, the paper is accessible and I enjoyed reading it a lot. \n\nGenerally, this is a really nice paper that approaches XAI from the angle of declarative languages. \n\nThe major shortcoming (in my opinion) of the paper is the somewhat hidden link between the logical semantics and the operation one has to run using the machine learning model. It would be good to explain early in the paper how a statement like “Pos(e)” would be evaluated given a (real-world) machine learning model. Is it that one would query the ML models with “e” and, based on the classification result, return true/false? Given a query such as “exists x P(x)”, is the idea to query the ML model (in the worst case) an exponential number of times? Is the assumption, in other words, that an ML model can be seen as a function which we can query in constant time? Is it true that the idea is limited to binary covariates (features)? (I assume the answer to the above questions is “yes” but I am not 100% sure). Making these types of connections more explicit, early on in the paper, would build a better bridge between the typical ML readership and the proposed logical formalism. \n\nThe authors specify two classes of “models” for which they analyse the query language: decision trees and OBDDs. It would be good to motivate OBDDs a bit more as I have not seen an OBDD used as a machine learning model. I understand that it is a nice formalism that renders certain queries tractable. But what is the relevance to ML here?\n\nI was intrigued by the bias example starting with line 201. This is one definition of bias (a very strong form as far as I can tell) but does not fully cover all situations one might want to call biased. In the end, what one wants is that the protected covariate is independent of the response variable (the model output). Is that satisfied by the definition of “Bias” here? Again, as you can see, I find the connection between the logical approach of the authors and the typical concepts in machine learning sometimes difficult to establish. \nGenerally, I think this is a strong paper. My worry is that most ML researchers would skip the paper because the link between their “reality”, that is, concepts and terminology, and what is used in the paper is missing or not made clear enough. \n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Yes", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "2 hours"}, "extra_text": {}}, {"review_id": "K3LFzSWraL", "reviewer": "Reviewer_deaJ", "summary": "The authors present a logical language, called FOIL, in which\nmany simple yet relevant interpretability queries can be expressed.\nThey go on to study the computational complexity \nof FOIL queries over two classes of ML models often\ndeemed to be easily interpretable: decision trees and OBDDs. \n\nThe authors show that despite claims of the good level of interpretability\nfor models such as DTs and OBDDs, there is a simple query in FOIL that is \nintractable over them. The authors go on to to define two tractable\nfragments of FOIL.", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "This is a very well-written and detailed paper. The appendix is \nlong and contains interesting material. The proof of Theorem 1 is particularly clever.\n\nThis field of research appears novel: defining a new language for \ninterpretability queries, analysis of the complexity of queries when the models are restricted.\n\nI am not very convinced that this is a definitive language which will be \nused in the field, since it is basically a low-level language. For example\nthe definition of the notion MATCH (line 210) is a roundabout way of \nsaying something quite simple, i.e. that x and y agree on features in S.\nHowever, the authors have implemented a translator from a higher-level \nlanguage to their low-level language. So the interest of FOIL is its\nsimplicity since this helps for proving (in)tractability results.\n\nThe theoretical study is restricted to DTs and OBDDs, which leaves open \nsimilar questions for more complex models (such as random forests or d-DNNFs).\n\nline 165: specify whether instances can be partial or not. If they are\nnecessarily total instances, then the claim that EVAL(phi,CNF) is NP-complete\ndoesn't make sense.\n\nMinimal Sufficient Reason: perhaps note that this is known by other \nauthors as PI-explanations or abductive explanations (see, for example, \nShih et al. A symbolic approach to explaining bayesian network classifiers, \nIJCAI 18 and Marques-Silva et al. Explaining Naive Bayes and Other Linear\nClassifiers with Polynomial Time and Delay, NeurIPS 20).\n\nLine 367: 'a particular subclass of BDDs': specify (in the body of the paper)\nexactly which subclass. \n\nLine 371: 'medium size decision trees': what size are we talking about here?\n\nsome problems with English:\n- legend fig.1: does the requester has a stable job\n- line 41: we explain along the paper\n- line 196: The following query express this\n- line 319: The whole package needs of\n- line 330: controlling by three aspects\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Yes.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "5"}, "extra_text": {}}, {"review_id": "9Rf61lsgGZ1", "reviewer": "Reviewer_oTbW", "summary": "This paper introduces a simple logic for examining classifiers. It shows\n1) The logic allows defining, in particular, a predicate capturing (minimal)\nsufficient reason explanations (i.e., a set of feature values that ensure the\nclassifier gives a certain classification) and a predicate indicating whether\nthe classifier makes a decision using a protected set of features.\n2) The most natural version of the logic allows defining a predicate that is\nNP-hard to evaluate for both decision tree and OBDD classifiers\n3) A simple fragment of the logic is adequate to capture the formulas indicated\nin (1), and there are two formulas such that if these can be evaluated in\npolynomial time for a model class, then the entire fragment is polynomial time\n4) The fragment in (3) is polynomial-time decidable for decision trees and OBDDs\n(on account of the indicated criterion)\n5) A restricted kind of OBDD allows the more general logic to be decided in\npolynomial time.", "questions": "", "limitations": "", "rating": 8, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "There has been quite a lot of work on methods for interpreting/auditing/etc.\nmachine learning models. As the paper observes, indeed, it seems inevitable that\nthere will be a plethora of distinct tasks for different purposes. Actually,\nthe \"no silver bullet\" discussion in the opening paragraph really should cite\nthe influential report by Doshi-Velez and Kim\n\nDoshi-Velez and Kim, Towards A Rigorous Science of Interpretable Machine Learning, arXiv:1702.08608, 2017.\n\nI recognize it is an arXiv report, but it is very well known at this point and\nlends credibility to these claims.\n\nGenerally speaking, what is needed are tools that permit a user (an auditor, \ncustomer, engineer, etc.) to ensure that the models are meeting the needs of an \napplication. To my knowledge, most work in this area has focused on evaluating\none particular property, or surveying the kinds of properties these users want\nevaluated (mostly work in CHI in that case). As far as I am aware, the tack \ntaken in this work is original, developing a framework and tools to capture the\nwhole family of such tasks. I believe this paper could be influential. At a\ntechnical level, the logic and fragments, and the criterion for polynomial-time \nevaluation of the fragment, are all interesting contributions in my view.\n\nOne may argue that it is a limitation of the framework that it isn't operating\non neural networks. I'm not so worried about this -- it's worthwhile to \ncapture what can be checked against models that are \"known to be interpretable\",\nbefore worrying about what can be extended to messy models like neural nets.\nIt is still helpful to present tools to a user that allow them to explore such\nmodels and validate them against various requirements. ", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "One class of properties that are missing from the logic that is orthogonal to the kind of counting queries supporting SHAP-like attribution that are mentioned in the future work are queries that concern the performance in practice -- e.g., what kind of errors is the model likely to make? These probably would require some kind of probabilistic extension, where queries are evaluated wrt the actual data distribution. This is relatively minor, in that the paper at least indicates that there are *some* natural queries that are not captured.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "4"}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper attracted significant discussion among reviewers. The reviewers identified the potential of a declarative unifying framework and rigorous theoretical analysis.  The reviewers also highlighted the novelty as a core strength. On the other hand, one reviewer did point out the lack of convincing empirical study. 

The consensus among reviewers was that the fact paper drew diverse and strong opinions makes it a great candidate for acceptance since it has the potential to spur such discussions in the community. Given that all the reviewers came to a consensus that the paper be accepted (even though not every reviewer agreed with the objectives of the paper), the job of AC was an easy one. 

We hope that the authors will take the comments of all the reviewers very seriously and incorporate them into the final version. 

Decision: Accept (Spotlight)