Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.
review_content: summary: In the setting of explainable artificial intelligence, this paper investigates probabilistic explanations for decision tree predictions. Namely, given a decision tree $T$, a data instance $e$ and a confidence parameter $\delta \in (0,1]$, a $\delta$-sufficient reason for $e$ given $T$ is a monomial that covers $e$ and for which the proportion of satisfying assignments $e'$ such that $T(e') = T(e)$ is at least $\delta$. A minimal $\delta$-sufficient reason is a  $\delta$-sufficient reason that is subset minimal, and a minimum $\delta$-sufficient reason is $\delta$-sufficient reason of minimum size. Based on these definitions, the authors prove that the problems of finding minimal/minimum $\delta$-sufficient reasons are NP-hard. They also consider tractable cases by considering restrictions on the structure (bounded split number) and the semantics (monotonicity) of decision trees. Finally, they propose a propositional SAT encoding for computing minimum $\delta$-sufficient reasons.

strengths_and_weaknesses: Overall, I would say that the paper includes some good ideas, but it requires more polishing. For the moment, the paper is not self-contained and should be re-organized.

Let us start with the positive aspects.  Based on the recent work by Izza et al. (2022), the problem of finding a $\delta$-sufficient reason of size at most $k$ belongs to NP, and the optimization version of this problem belongs to $\Theta_2^P$. So, a key question is to determine whether such a problem is NP-hard, or not. This is arguably the main result of this paper (Section 4): the authors have proven that the problems of computing minimal/minimum $\delta$-sufficient reasons are NP-hard. The work spent on finding tractable subclasses (Section 5) is interesting but would deserve further investigation (see comments in the section "Limitations").

Unfortunately, the paper is not self-contained. In particular, the main result of this study (Theorem 3) includes a sketch of proof that could be improved. To this point, I was merely confused by the sentence “Finally, the reduction from k-Minimal-Expected-Clauses to Check-Sub-SR builds an instance $(T, e)$ from $(\phi, \sigma)$ in a way that there is a direct correspondence between partial assignments $\mu \subseteq \sigma$ and partial instances $e’ \subseteq e$, satisfying that [...]”. As we know, unless P = \#P, we cannot find a polynomial translation from a $k$-CNF formula $\phi$ to an equivalent decision tree $T$ (even for $k = 2$). In fact, the construction of $T$ is more sophisticated (notably, it is not equivalent to $\phi$), and the overall proof is clarified in the Supplementary Material. 

My last major comment is about the SAT encoding of the (decision version of the) minimum $\delta$-sufficient reason problem (Section 6.2). While this encoding looks elegant, the experiments reported in the Supplementary Material are at a preliminary stage. Read again my comment below, but if the authors really want to provide a propositional SAT encoding, it should be tested on various datasets, and it should be compared with the SMT encoding proposed by Izza et al.


questions: Yes, I have a few questions about tractable cases:
* A natural class of shallow (and interpretable) models is the family of decision trees of bounded depth, say $d$. Are the problems of finding minimal/minimum $\delta$-sufficient reasons still intractable for fixed $d$? Are they fixed-parameter tractable with respect to $d$?
* Theorem 5 is interesting but leaves open a natural case: the well-studied class of monotone DNF. As we know, counting the number of satisfying assignments of a DNF admits an FPRAS. So, do we still have an FPRAS result for computing minimal/minimum $\delta$-sufficient reasons when the predictor is representable by a monotone DNF formula?  
limitations: Overall, I think that the key results of this paper are of theoretical nature, and hence, this paper should stick to the theoretical side. Indeed, as mentioned above, the experimental study is still at an early stage. So, focusing on theoretical results (Section 4 and 5) should leave some room for presenting the proof of the main result (Theorem 2) in more detail, and for examining more tractable cases - or showing that natural subclasses remain intractable.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: After rebuttal: The authors clarified my misunderstanding and I acknowledge that the problem seems to be practically harder than I thought. Some reservations about the relevance of decision trees for NeurIPS, the choice of the dataset and the speed of the SAT encodings remain, but I will change my overall evaluation to weak accept and lower my confidence.

---

The paper studies computing delta-sufficient reasons for decision trees. It shows that finding subset and cardinality minimal delta-sufficient reasons is not possible in polynomial time assuming P!=NP. A SAT-encoding is presented and the appendix shows some runtime results for trees with up to 200 leaves. 
strengths_and_weaknesses: While this is a solid technical paper, I do not think that it is a good contribution for NeurIPS. It seems to me that the contribution is mainly interesting from a theoretical perspective. Please correct me if am wrong, but it seems to me that the complexity arises only from considering all possible extensions of the minimal sufficient reasons. However, considering all these candidates seems unnecessary in a decision tree because decision trees are typically not exponentially large. Indeed, all trees in the experiments have at most 200 leaves. This means that there are at most 200 decision paths that have to be analyzed. The SAT encodings need more than 4 seconds even if the trees have only 20 leaves, which seems rather slow. The runtime remains the same as the number of leaves increases, but this is probably because the encoding (exponentially) depends on the number of features (that presumably did not change in the experiments) and not on the number of decision paths (which is exponentially bounded by the number of features, but typically significantly smaller than the worst-case bound). It seems that the problem could be solved more efficiently by considering the decision nodes and their possible extensions in the tree. From an explanation perspective, it would also be nice to see some examples of explanations generated with this approach. Overall, I think that the current state of the paper could be a nice contribution for a smaller conference on theoretical aspects. However, for a major conference like NeurIPS, the significance is not sufficiently clear.
questions: Please correct me if I am wrong about the difficulty of the problem. Are the decision trees available for inspection in the code repository? I would be interested in looking at the decision trees of depth 20 in order to understand why the problem could be more complicated. It would also be interesting to know what the theoretical upper bound for the number of leaves compared to their actual number is. What is actually the background of the generated trees? Have they been generated randomly or do they achieve better performance with increasing number of leaves? Why has MNIST actually been chosen for the experiments? It does not really seem a natural choice for decision trees. Can we actually learn anything from the decision tree/ the explanations for MNIST? Why not consider a tabular dataset? 
limitations: Yes.
review_title: null

final_score: rating: 8: Strong Accept: Technically strong paper, with novel ideas, excellent impact on at least one area, or high-to-excellent impact on multiple areas, with excellent evaluation, resources, and reproducibility, and no unaddressed ethical considerations.
review_content: summary: A sufficient reason (SR) for a decision taken by a classifier on input x
is a subset e of the assignment x (when viewed as a set of literals)
which is sufficient to account for the decision. For obvious reasons 
the user may be interested in minimum-cardinality or (more modestly)
subset-minimal SR's. SR's are a basic notion in the formal approach to 
explaining decisions of classifiers, however it is a very strict notion,
leading to SR's which contain too many features for the user to grasp.
Thus, from a practical point of view, a more useful notion is a delta-SR 
e which allows a certain degree of error, in that only a fraction delta<1 of 
the completions of the partial assignment e need to be classified the same as x.

This paper settles the computational complexity of certain problems concerned with
finding delta-SR's over decision trees, showing notably that even finding a subset-minimal 
delta-SR is intractable (assuming P not equal to NP). 

They show that this intractability can be avoided if extra restrictions are applied
(such as a structural property of the decision tree or monotonicity of the classifier).
They also give a SAT encoding for finding smallest delta-SR's.
strengths_and_weaknesses: The main complexity results are negative but nonetheless very interesting since they
show intractability even for decision trees, which is one of the simplest possible
ML models. It is not too difficult to show that the simple greedy-deletion algorithm
which can be used to find SR's of decision trees in polynomial time no longer
works for delta-SR's due to the non-hereditary nature of delta-SR's (e.g. we can
have A \subset B \subset C with A,C both delta-SR's but not B). But, NP-hardness
is not at all obvious. The constructions required to prove this in the supplementary 
material are far from straightforward.

There are also some positive results, concerning DT's with bounded split number or
monotone free BDD's (Corollary 1). The authors also give a SAT encoding which provides a
way of calculating delta-SR's, but as is shown in the supplementary material this is
only practical for decision trees of very modest size (20 leaves, 36 features).
This simply confirms, in practice, the theoretical intractability proved in the paper.

Minor points:
- perhaps reword 1st sentence of abstract since formal XAI is not just
concerned with explaining decisions of ML models.
- line 286: a citation is required so the reader can easily find out what free BDDs are 
and find a proof that counting is polytime.
- line 308: in the output, don't you mean n-|..| \leq k instead of |..| \leq k?
- line 325: "its labeled" should be "it is labeled"
- line 342: "can be take safely" should be "can be taken safely"
- line 346: missing "be" before "a series"
- line 365: missing "and" before "clauses"?
- I am confused by Question 2 in Future Work which seems to have been answered by Corollary 1.
- line 376: delete "a" in "every fixed such a"
- use {} in latex to impose capitals in bibliography entries (e.g. {XAI})
- the arXiv paper by Izza et al occurs twice in the bibliography
- line 636: Do you mean \neg y_i instead of y_i ? Below you seem to be assuming that
these variables are negated.
- line 682: Let us say
- line 687: do you mean 4e instead of M?
- line 719: delete "that"

questions: (1) Can the notion of split number be generalised to DAGs (such as d-DNNFs)? 

(2) Is bounded split number not the same as bounded treewidth? It is well known that
bounded treewidth allows polynomial-time counting for many combinatorial problems
(see, for example, Michael Jakl, Reinhard Pichler, Stefan Rümmele & Stefan Woltran,
Fast Counting with Bounded Treewidth, LPAR 2008, pp 436–450 or articles cited therein)

(3) Have you tested the loss in accuracy if you restrict yourself to learning
DT's with bounded split number? 
limitations: N/A
review_title: null

Meta-review: metareview: The paper studies the complexity of discovering probabilistic explanations for decision trees. They show that computing minimum/minimal probabilistic explanations is an NP-hard problem. On the other hand, they also identify structural conditions that make the problem efficiently solvable.

The reviewers appreciated the challenges in proving the complexity results. Although the experimental results are not so convincing, we evaluated the paper mainly on its theoretical aspects and find it suitable for acceptance.
confidence: Certain
Decision: Accept