Venue: NeurIPS 2021 Conference

Reviews:

final_score: rating: 7: Good paper, accept
review_content: 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.

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. 
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. 

Generally, this is a really nice paper that approaches XAI from the angle of declarative languages. 

The 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. 

The 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?

I 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. 
Generally, 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. 

limitations_and_societal_impact: Yes
review_title: null

final_score: rating: 8: Top 50% of accepted NeurIPS papers, clear accept
review_content: summary: 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.
main_review: There has been quite a lot of work on methods for interpreting/auditing/etc.
machine learning models. As the paper observes, indeed, it seems inevitable that
there will be a plethora of distinct tasks for different purposes. Actually,
the "no silver bullet" discussion in the opening paragraph really should cite
the influential report by Doshi-Velez and Kim

Doshi-Velez and Kim, Towards A Rigorous Science of Interpretable Machine Learning, arXiv:1702.08608, 2017.

I recognize it is an arXiv report, but it is very well known at this point and
lends credibility to these claims.

Generally speaking, what is needed are tools that permit a user (an auditor, 
customer, engineer, etc.) to ensure that the models are meeting the needs of an 
application. To my knowledge, most work in this area has focused on evaluating
one particular property, or surveying the kinds of properties these users want
evaluated (mostly work in CHI in that case). As far as I am aware, the tack 
taken in this work is original, developing a framework and tools to capture the
whole family of such tasks. I believe this paper could be influential. At a
technical level, the logic and fragments, and the criterion for polynomial-time 
evaluation of the fragment, are all interesting contributions in my view.

One may argue that it is a limitation of the framework that it isn't operating
on neural networks. I'm not so worried about this -- it's worthwhile to 
capture what can be checked against models that are "known to be interpretable",
before worrying about what can be extended to messy models like neural nets.
It is still helpful to present tools to a user that allow them to explore such
models and validate them against various requirements. 
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_title: null

final_score: rating: 3: Clear rejection
review_content: 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.
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.

Originality. 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).

Quality: The quality is reasonable; it just doesn't do vey much.

Clarity: That paper is reasonably clear.

Significance:  This is very low. I can't imagine anyone using this for anything useful.

Given 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.

For 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?

I don't think NeurIPS is the right venue for this paper. The style of theorems would be more suited to a conference like KR.

Overall, I am sceptical that  giving yes/no answers is useful for interpretability. You assume that it is true, but never justify it.

limitations_and_societal_impact: Yes
review_title: null

final_score: rating: 7: Good paper, accept
review_content: summary: 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.
main_review: This is a very well-written and detailed paper. The appendix is 
long and contains interesting material. The proof of Theorem 1 is particularly clever.

This field of research appears novel: defining a new language for 
interpretability queries, analysis of the complexity of queries when the models are restricted.

I am not very convinced that this is a definitive language which will be 
used in the field, since it is basically a low-level language. For example
the definition of the notion MATCH (line 210) is a roundabout way of 
saying something quite simple, i.e. that x and y agree on features in S.
However, the authors have implemented a translator from a higher-level 
language to their low-level language. So the interest of FOIL is its
simplicity since this helps for proving (in)tractability results.

The theoretical study is restricted to DTs and OBDDs, which leaves open 
similar questions for more complex models (such as random forests or d-DNNFs).

line 165: specify whether instances can be partial or not. If they are
necessarily total instances, then the claim that EVAL(phi,CNF) is NP-complete
doesn't make sense.

Minimal Sufficient Reason: perhaps note that this is known by other 
authors as PI-explanations or abductive explanations (see, for example, 
Shih et al. A symbolic approach to explaining bayesian network classifiers, 
IJCAI 18 and Marques-Silva et al. Explaining Naive Bayes and Other Linear
Classifiers with Polynomial Time and Delay, NeurIPS 20).

Line 367: 'a particular subclass of BDDs': specify (in the body of the paper)
exactly which subclass. 

Line 371: 'medium size decision trees': what size are we talking about here?

some problems with English:
- legend fig.1: does the requester has a stable job
- line 41: we explain along the paper
- line 196: The following query express this
- line 319: The whole package needs of
- line 330: controlling by three aspects

limitations_and_societal_impact: Yes.
review_title: null

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)