Sensitivity Verification for Additive Decision Tree Ensembles

Authors: Arhaan Ahmad, Tanay Vineet Tayal, Ashutosh Gupta, S. Akshay
Primary area: alignment, fairness, safety, privacy, and societal considerations
Keywords: Robustness verification, Sensitivity analysis, SAT solvers, efficient encodings, NP-hardness, fairness, confidence

Abstract:
Tree ensemble models, such as Gradient Boosted Decision Trees (GBDTs) and random forests, are widely popular models for a variety of machine learning tasks. The power of these models comes from the ensemble of decision trees, which makes analysis of such models significantly harder than for single trees. As a result, recent work has focused on developing exact and approximate techniques for questions such as robustness verification, fairness and explainability for such models of tree ensembles.

In this paper, we focus on a specific problem of feature sensitivity for additive decision tree ensembles and build a formal verification framework for a parametrized variant of it, where we also take into account the confidence of the tree ensemble in its output. We start by showing theoretical (NP-)hardness of the problem and explain how it relates to other verification problems. Next, we provide a novel encoding of the problem using pseudo-Boolean constraints. Based on this encoding, we develop a tunable algorithm to perform sensitivity analysis, which can trade off precision for running time. We implement our algorithm and study its performance on a suite of GBDT benchmarks from the literature. Our experiments show the practical utility of our approach and its improved performance compared to existing approaches.

Decision: accept (poster)
Reviewer scores: 6, 8, 6, 6, 6

Reviews and discussion:
<thread>
creation date:
1730221101169

thread_type:
official_review

<thread_object>
creator: reviewer_xnqm

<content>
summary:
In the context of interpretable machine learning, this paper investigates the problem of "feature sensitivity" in tree ensembles. Specifically, given a classifier $ c $ and a set of features $ F $, the goal is to determine whether there exists an instance $ x $ such that the classification of $x$ by $c$ changes when only the values of the features in $ F $ are modified. The paper establishes that this problem is NP-complete for gradient-boosted trees, even when $ F $ consists of a single feature. The authors also explore an extension of this problem that considers the confidence associated with class changes, which is also shown to be NP-complete. To deal with this source of complexity, the authors propose a Pseudo-Boolean encoding for the feature sensitivity task, which they empirically validate on several benchmarks.

strengths:
**Novelty:**
Arguably, the main strength of this paper lies the novelty of the complexity results for deciding feature sensitivity when the predictive model is a binary-class gradient boosted tree. Notably, the fact that the problem remains NP-hard even in the case where the sensitivity analysis is reduced to a single feature is intriguing.

weaknesses:
**Clarity:** 
The scope of the paper is quite challenging to define. As indicated in the title, summary, and introduction, it seems that the authors aim to examine feature sensitivity for “tree ensembles,” which is a broad category that includes several model classes, such as gradient-boosted trees (GBTs) and random forests (RFs). This is further illustrated in Section 2, where the authors attempt to provide a general definition of tree ensembles (Lines 130-136). However, upon reviewing the technical sections of the study (Sections 3-5), it becomes clear that the results are exclusively related to GBTs. This focus is reiterated toward the end of the introduction (starting at Line 65), where the authors clarify their exclusive emphasis on GBTs.

Therefore, it is essential for the authors to establish a clear consensus on the scope of the paper in the revised version. If they intend to concentrate solely on GBTs, this specificity should be highlighted throughout the paper, beginning with the title and summary. The definition of tree ensembles in Section 2 should also be replaced with a definition of GBTs. Conversely, if the authors believe that their theoretical results could be easily extended to other tree ensemble classes (e.g., random forests), then the proofs in Section 4 should be modified accordingly (see Question 2).

At present, the definition of tree ensembles in Section 2 is somewhat unclear. If we denote by $c(x)$ the sum of the decisions $T_i(x)$ made by each of the $m$ decision trees $T_i$, then what class in $\mathcal{F}$ is predicted by $c$ on $x$? This is evident for GBTs when $\mathcal{F} = \\{-1,+1\\}$, using the sigmoid function $\sigma$, but it remains ambiguous for other classes of tree ensembles. If the authors’ goal is to address various classes of ensemble models, it is important to provide a comprehensive definition of “tree ensemble” that can be instantiated for both GBTs and random forests.

**Significance:**
The main theoretical contribution of this paper lies in Theorem 2, which establishes that single feature sensitivity is NP-hard for GBTs. Other NP-hardness results presented in this study stem from this case. While this finding is commendable, I remain unsure if it is sufficient for ICRL. To enhance the theoretical significance of this study, it would be beneficial to investigate whether this problem and its variants are W[1]-hard or if some of them are fixed-parameter tractable (FPT), with the parameter of interest being the maximum depth of the trees (See Question 1). Establishing hardness results for W[1] would indeed bolster the justification for the constraint programming approach discussed in Section 4.

questions:
(1) Can the NP-hardness of single feature sensitivity (Theorem 2) or subset feature sensitivity (Theorem 1) for GBTs be extended to W[1]-hardness? 

(2) Alternatively, can these hardness results for GBTs be extended to random forests?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730551912537

thread_type:
official_review

<thread_object>
creator: reviewer_mrks

<content>
summary:
The paper addresses the sensitivity verification problem of GBDTs by formalizing a pseudo-Boolean encoding. The authors claim their approach can achieve significant performance gains over existing sensitivity verification tools, specifically for GBDTs. However, the paper lacks a comprehensive presentation, robust mathematical formulation, and systematic experiments. As such, it would need major revisions to be accepted.

# Discussion phase
After a deep discussion phase during which the authors addressed all my weaknesses and improved their work, including a better result, I increased my overall score to 6/10. Specifically, I've changed only the scores while leaving the original review; I could also change the review if that's mandatory.

strengths:
- **S1:** The paper addresses an important issue aimed at verifying the sensitive features of GBDTs.
- **S2:** Mathematical proofs, which I would have expected to have a better presentation, but I appreciate the effort.
- **S3:** The authors present an approach using pseudo-Boolean encoding, arguing that it is more suitable than other methods.

weaknesses:
- **W1:** The notation is inconsistent and confuses readers, especially those who are unfamiliar with the topic. For example, input examples are denoted by $x$ and $x'$ in Def. 3.1, but then they are $x_1$ and $x_2$ in Def. 3.2; furthermore, in the proof of Th. 2 instances are symbolized $a$ and $b$ (a very unhappy notation). Similarly, trees are defined as $T$ in Section 2 but then symbolized with $D$ in the proof of Th. 1.
- **W2:** Certain mathematical expressions and definitions are unclear or incorrect. For example, $F = f$ instead of $F = \\{f\\}$ detracts from the overall comprehensibility. As another example, the set minus ($\setminus$) operation is properly used in Def. 3.1 but then in Section 4 is not used; that is, the authors use minus ($-$). A further example is when the authors use $\mathcal F = F \bigcup f$, which, again, is not a proper mathematical definition; it should perhaps be $\mathcal F = F \cup \\{ f \\}$.
- **W3:** The proofs suffer from inconsistent symbols, poor spacing, and cluttered notation, making the logical progression of arguments hard to follow. For example, while reading the proof of Th. 1, I had to stop and skip such proof because the notations became heavy, and my overall cognitive overload intensified. To give a precise idea of how it felt: in $c'(x) = -n$, $n$ is the same $n$ as the number of decision trees in the ensemble (line 205)? What is the $\Longrightarrow$ in the notation? What is $\wedge$? Etc. As you can see, there are too many doubts that the reader has at this point. I assumed the proof was correct, even though I hadn't thoroughly reviewed it. The problem with this way of writing the proof is that the authors mixed textual explanations with mathematical ones in an unpleased way. This point is very critical.
- **W4:** The experimental results lack clarity; terms like "maximum, minimum, and average" time are used ambiguously without explaining what they represent or if multiple runs were performed.
- **W5:** Despite the general title, the paper focuses solely on GBDTs, excluding other ensemble methods like random forests without justification. If that's not the case, I expected to see experiments with random forests as well.
- **W6:** The paper contains grammatical errors, inconsistent abbreviations (e.g., "wrt" vs. "w.r.t."), and informal language, which detracts from the overall presentation.

questions:
- **Q1:** Could you ensure consistent notation throughout, especially in proofs? E.g., $x$ and $x'$ vs $x_1$ and $x_2$.
- **Q2:** Why did you limit the work to GBDTs? Would your framework extend to other ensemble methods, such as random forests?
- **Q3:** Could you clarify the connection between sensitivity and $(p)$-sensitivity, especially after Definition 3.2? The special-case/general-case distinction you imply needs a clearer mathematical basis, and it is *not* easy to see (i.e., one uses the sigmoid function $\sigma$ and the other does not).
- **Q4:** Why do you use the sigmoid function $\sigma$ in Def. 3.2, and then decide to drop such "complexity" in Section 4 when you present the encoding? I would either drop it from the definition or introduce it in the encoding; either way would be acceptable, but please avoid the asymmetric treatment.
- **Q5:** What does "maximum, minimum, and average time" mean in your experiments? Were these metrics based on repeated runs, and if so, could you clarify the settings?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730733454394

thread_type:
official_review

<thread_object>
creator: reviewer_1wtc

<content>
summary:
The paper puts forward an approach for formal verification of feature sensitivity. Feature sensitivity is a characteristic of a model whereby the model changes its output depending on values of such features. In domains such as fairness checking for feature sensitivity is one of the ways in which fairness checks are meaningfully encoded.

The paper answers some complexity problems on answering features sensitivity, leaves some open. Crucially it provides a novel and efficient way based on pseudo-Boolean encodings to solve the verification problem. Some experimental results showing SoA performance are provided.

Overall this is a solid paper, arguably with some weaknesses, that advances the SoA of the area.

Post-rebuttal note: The authors answered by questions and provided additional material (developed post-submission) to solve some of the questions left unanswered in the paper. On the other hand I also noticed some presentation issues that I think can be fixed. I think the final answer on scalability on the point are raised remains unresolved; so it is still not 100% clear to me the extent to which the novel encoding is responsible for the gain. I do accept the authors point in as far as the comparison against SMT goes. 
Overall I am still mildly positive on the paper.

strengths:
The paper is very well presented (some very minor typos that can be fixed). I cannot judge the soundness of the encoding but it seems reasonable. I read the complexity proofs and appear correct (even if not surprising). In terms of advancement on SoA I judge this to be in line with the standards expected at ICLR, even if perhaps not as a top paper (see weaknesses below).

Most importantly solving model valuation for ensembles remains a key question in a variety of domains and this paper presents a principled and noteworthy contribution to the challenge. While the NP-hardness results may not be surprising they fill a gap in the knowledge in the area and the encoding presented achieves SoA performance.

weaknesses:
While the NP hardness won't be a surprise to most, not all the theoretical questions are answered in the paper with the obvious gap being trees of depth 2 and 3. I feel this has a considerable implication even in terms of architectural suggestions from this study. Has this question been answered by the authors in the meantime? To me these corner cases are actually the most interesting ones. Finding the the case for 3 is polynomial would be a very interesting result

The reasons as to whether the approach appears to scale considerably better than present SoA were not clear to me in the paper. Do the authors have an explanation? If so, could they provide it? The reason for asking is that in principle it could even be that their implementation is just more efficient and it does not have so much to do with the encoding.

questions:
See questions on the weaknesses above.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730816607937

thread_type:
official_review

<thread_object>
creator: reviewer_uli2

<content>
summary:
This submission considers the problem of sensitivity for tree ensemble classifiers, i.e. the question of determining if, for a selection \\(F\\) of features, there exists a pair of inputs that agree on all the features outside of \\(F\\) but get classified differently by the tree ensemble. This work also develops a quantitative version of sensitivity (Def 3.2), parametrised by a number \\(p\in[0,\frac{1}{2}]\\), that additionally lower-bounds the "distance" between the two classifications. 

The main theoretical contributions consist in proving that 
- the (non-quantitative) sensitivity problem is NP-hard (Thm 1)
- the sensitivity problem restricted to singleton feature sets F={f} is also NP-hard (Thm 2)

The main practical contribution is to show that the problem of establishing \\(p\\)-sensitivity can be encoded as the satisfiability of a system of pseudo-boolean constraints (Thm 3). Experimental evidence shows that this approach scales much better than SOTA methods.

strengths:
The paper is very well-written, with a good overview of the literature and easy-to-follow examples, proofs and discussions. In particular the proofs are easily understandable even by someone with very limited knowledge of computational complexity theory such as myself.

The main practical novelty of this paper -- using a pseudo-boolean satisfiability encoding -- is credibly shown to be superior to the SOTA methods in a short but convincing experimental section.

weaknesses:
Theorems 1 and 2 correspond to two extremes of the sensitivity problem: the first considers sensitivity w.r.t. the full set of features, the second considers only singleton subsets of features. It feels like the full story would be a result showing that sensitivity w.r.t. subsets of features of size \\(N\\) is NP-hard, for all \\\(N\\). Similarly, the story is slightly incomplete as in does not cover trees of depth 2 or 3 (as mentioned by the author(s)). The paper would be nicer (and stronger) if these questions were solved. too 

Here are some minor comments/corrections
* l69: when THE number
* l83: whether...whether
* l104: some OF these
* l117: of A \\(d\\)-dimensional
* l157: When \\(F=\\{f\\}\\)
* l168: two-tree
* l194: Def 3.2 is not really a special case of Def 3.1 in the sense that Def 3.1 does not correspond to a particular choice of \\(p\\). As it stands, Def 3.1 is equivalent to \\(\exists p.\\)Def 3.2 holds. To make Def 3.1 a special case of Def 3.2 I would change it to have \\(p\geq 0\\) and \\(\sigma(c(x_1))\geq 0.5+p, \sigma(c(x_2))< 0.5+p\\) (or the other way round). Then Def 3.1 would correspond to the case \\(p=0\\).
* In the proofs of thm 1 and thm 2, why not simply take \\(X_{k+1}=\\{-1,1\\}\\) and \\(X_0=\\{-1,1\\}\\)?
* l275: \\(F\cup\\{f\\}\\) (not \bigcup and singleton)
* l289: I don't understand the first sentence here. Which problem requires three variables \\(x_1,x_2,x\\)?
* l307 and l313: use \setminus for the set difference \\(\mathcal{F}\setminus F\\). Also, if you'd used \\(x,x'\\) or \\(x,y\\) instead of \\(x_1,x_2\\), you wouldn't have problems with double subscripts.
* l310: \log instead of log
* eq (2): shouldn't \\(j+1\\) in the RHS simply be \\(j\\)?
* l327-328: Incomplete sentence
* l328: Since THE root
* Thm 3: use \eqref in the conjunction, in order to get \\((1)\wedge\ldots\wedge(6)\\). Parentheses = equations. Conversely don't use (1) and (2) to refer to the two parts of the theorem, instead use 1. and 2., or better (i) and (ii).
* l394: mine -> us
* l420: p-sensitive -> \\(p\\)-sensitive

questions:
Do you think it is the case that sensitivity w.r.t. subsets of features of size \\(N\\) is NP-hard, for all \\\(N\\)? If yes, do you have any intuition about whether proving this is substantially harder than your existing proofs?

Same question for trees of depth 2 or 3.
</content>
</thread_object>

</thread>
<thread>
creation date:
1731255340601

thread_type:
official_review

<thread_object>
creator: reviewer_jog2

<content>
summary:
This paper addresses the feature sensitivity problem for ensembles of decision trees, with a focus on Gradient Boosted Decision Trees (GBDT). The authors demonstrate that this problem is NP-complete through a reduction from the SAT problem. They then propose an algorithm to solve the p-sensitivity problem by encoding it as pseudo-Boolean constraints. Finally, experimental results are provided, comparing the proposed approach to some existing methods.

strengths:
The paper is well-written, with a clear structure that makes it easy to follow. This clarity enhances the readability and understanding of the material.

The problem is well motivated.

The theoretical contributions are interesting and their proofs appear to be correct.

weaknesses:
The initial result on NP-hardness of sensitivity problem for all features seems redundant after establishing NP-completeness for a single feature. 

My main issue with this paper is with the experiments. The comparison with VERITAS seems a bit unfair. By limiting VERITAS to the same runtime as SENSPB, the comparison may not reflect its full potential. Allowing VERITAS more runtime might yield better results, or it could have already produced sufficiently good results within its runtime. A separate table detailing the number of instances each method solved and the time taken would provide additional insights.

**Minor Comments/Typos**
- Line 068: "just on" → "just one"
- Line 079: Rewrite this sentence for clarity: “Can we use other forms of powerful reasoning, Pseudo-Boolean solvers, that have shown to be effective in other problems (Mexi et al., 2023), for the sensitivity problem?”
- Line 162: "given set of sensitive features F" → "given set of features F"
- Caption of Table 1: "results than mine" → "results than our method"

questions:
Is there a reason why the NP-hardness of the all feature problem was included in the paper? If it can be useful in some cases, some explaination here can be beneficial.

It would be nice to know why the results are specific to GBDT and why they could/couldn't be directly extended to other ensemble models, such as random forests.
</content>
</thread_object>

</thread>
<thread>
creation date:
1731943674405

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Common response to all reviewers regarding random forests

comment:
We thank all the reviewers for their careful reading and useful feedback, comments, and questions. Here we address a common question posed by multiple reviewers so as to not duplicate our responses later, namely, whether our approach is specific to GBDT models or works for general tree ensembles. Our response is four-fold: 

- Our definitions of the sensitivity problem indeed hold for general tree ensembles. 
- Our hardness results also apply to tree ensembles. Note that in Section 3, we only use that it is a decision tree ensemble classifier. The only extra assumption we need is that the classifier “ensembles” the trees by summing up the decisions of individual trees (this is sometimes called additive tree ensembles , see e.g.,[1]). In particular, our results are independent of the way the tree ensemble was trained (e.g, gradient boosting etc). 
- Our encoding in Section 4 also directly works for any tree ensemble which aggregates the trees by summing up the individual tree decisions. 
- In our experiments, we focused on GBDT models because they are a large and well-known class that have (i) easy to access benchmarks and (ii) are additive.

In summary, we can write/extend our definitions, theoretical results as well as our encoding to random forests if they follow an additive prediction model.

A caveat is that the classical definition of random forests [2] computes the final answer by max-pooling rather than summing up, which we do not handle in this paper. We believe that our theoretical results and encodings can also be extended to the max-pool setting, but we leave this for future work. On the other hand, some famous implementations, such as Scikit-Learn [3], do use a weighted average of the individual tree predictions to make the final decisions, which can be incorporated into our approach by understanding and incorporating their weights. We did not run experiments for (additive) Random Forests separately, since from the point of view of our encoding, they are equivalent to GBDT models. 

We hope this answer also justifies the title of the paper and the focus on (additive) tree ensembles. We will edit our presentation in the paper (e.g., in the introduction) to rewrite and clarify these points.

[1] Veritas: Versatile Verification of Tree Ensembles. Laurens Devos, Wannes Meert, and Jesse Davis. ICML 2021 http://proceedings.mlr.press/v139/devos21a.html

[2] Random Forests. Breiman, L. Machine Learning 45, 5–32 (2001). https://doi.org/10.1023/A:1010933404324

[3] Scikit-Learn https://github.com/scikit-learn/scikit-learn/blob/6e9039160f0dfc3153643143af4cfdca941d2045/sklearn/ensemble/_forest.py#L883
</content>
</thread_object>

</thread>
<thread>
creation date:
1731946174554

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Common response regarding depth 3 hardness

comment:
A second common question of multiple reviewers is whether our results could be extended to decision tree ensembles of depth 2 and 3. Indeed, our current hardness results kick in only for decision tree ensembles of depth at least 4. But since the submission deadline, we have been able to modify the existing proofs to prove NP-hardness for depth 3 decision trees, a strictly stronger result than what is currently in the paper. We will add/replace it in the revised version of the paper, if permitted (and add hardness of distinguishing input as a corollary). This still leaves the case of depth 2 trees open. None of the present (including the new)  proofs can be extended to this case, since both our hardness reductions and results using evasiveness rely on hardness of 3-CNFSAT, which requires 3 variables per clause which we translate to depth 3 trees. However, 2-CNFSAT is poly-time solvable and hence not useful to show hardness. We expect that a different technique/reduction/encoding will be needed to resolve this question.

We sketch the depth 3 proof below:
----------
We reduce from 3CNF-SAT which asks given a Boolean formula in conjunctive normal form (CNF) with 3 variables per clause, whether it is satisfiable. Given an instance $\varphi$ of 3CNF-SAT, let $cl(\varphi)$ be the set of clauses $\{cl_1,cl_2,\dots,cl_m\}$, with $m=|cl(\varphi)|$ and let $var(\varphi)$ denote the set of variables \{$v_1,v_2,\dots,v_n$\}, with $n=|var(\varphi)|$. Then from $\varphi$ we start by creating the formula $\varphi' = \varphi \land (v_{n+1} \lor v_{n+1} \lor v_{n+1}) $ which is also a 3CNF formula with a new variable $v_{n+1}$ and a new clause $cl_{m+1} = (v_{n+1} \lor v_{n+1} \lor v_{n+1})$. Observe that $\varphi$ is satisfiable, i.e., there exists an input $x\in \{{0,1\}}^n$ that satisfies $\varphi$ iff there exists an input $x'\in \{0,1\}^{n+1}$ that satisfies $\varphi'$. We the construct a decision tree ensemble $d$ with depth 3, such that $d$ is 1-feature sensitive iff $\varphi'$ is satisfiable.

In formula $\varphi'$, for every clause $cl_i$, we create a depth-3 decision tree $T_i$ as depicted in Figure 3 from the submitted paper, where $m=|cl(\varphi)|$ is replaced by $m+1=|cl(\varphi')|$ (we replace the notation of variable $x_i$ by $v_i$ to avoid confusion). That is, for each literal (i.e., $v_i$ or $\neg v_i$) in the clause, we add a "true" branch with output $\frac{1}{|cl(\varphi')|}$, and a "false" branch where we either continue to next literal or return $-1$. For each literal, if it occurs positively as $v_i$ (resp. negatively as $\neg v_i)$, the true (resp. false) branch outputs $\frac{1}{|cl(\varphi')|}$. We form the decision tree ensemble $d$ using the above decision trees with trees enumerated $T_i$ for $i \in \{1,2,\dots, m+1=|cl(\varphi')|\}$. The domain of $d$, i.e., $\mathcal{X}={0,1}^{n+1}$ and $\mathcal{Y}=\{0,1\}$, where depending on whether the sum of values at the leaves of the trees is greater than 0 or not, we output 1 or 0.

Claim A: For all $x\in\{0,1\}^{n+1}$ we have $d(x)=1$ iff  $\varphi'(x)=1$, i.e., $x$ satisfies/models $\varphi'$. To see the proof of this claim, there are two cases: First, suppose the input satisfies the 3CNF formula $\varphi'$, i.e., $\varphi'(x)=1$. In this case, each of the $m+1$ clauses are satisfied in the input and thus, for all trees $T_i$ we have $T_i(x) = \frac{1}{m+1}$. Thus, $\Sigma_1^{m+1} T_i(x) = 1 > 0 \implies d(x) = 1$. Second, suppose the input doesn't satisfy the 3CNF formula $\varphi'$. Thus, there exists a clause which is not satisfied by the input. Let that clause be $cl_j$. By the construction of $d$, for the corresponding tree $T_j(x) = -1$ and $T_i(x) \leq \frac{1}{m+1}$ for all $i \neq j$. Thus, $\Sigma_1^{m+1} T_i(x) \leq -1 + \frac{m}{m+1} = \frac{-1}{m+1} < 0$ which implies that $d(x) = 0$.

Finally, let $F$ be the set containing the singleton ${n+1}^{th}$ feature corresponding to $v_{n+1}$. To complete the proof, we will show that $d$ is $F$-sensitive iff $\varphi'$ is satisfiable. If $d$ is $F$-sensitive, there exist two inputs where the answer is different, from which we infer that there exists $x$ s.t $d(x)=1$ which by above Claim A means $\varphi'$ is satisfiable. The other direction when $d$ is not $F$-sensitive, by considering $x_F=0$, we get $T_{m+1}$ will evaluate to $-1$ since $cl_{m+1}[v_{n+1}\mapsto 0]=0$. As a result, we can conclude that for any $x_{\bot F}\in \{0,1\}^n$, we have $\sum_1^{m+1}T_i(x_{\bot F}, 0) \leq -1+ \frac{m}{m+1}< 0$ and so $d(x_{\bot F},0)=0$. Thus, for any $x_F\in \{0,1\}$, since $d$ is not $F$-sensitive, we get $d(x_{\bot F},x_F)=0$, which implies that for all $x\in\{0,1\}^{n+1}$, $d(x)=0$. Again appealing to Claim A above, we can conclude that $\varphi'$ is not satisfiable, which completes the proof.
</content>
</thread_object>

</thread>
<thread>
creation date:
1732792860654

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Highlighted rebuttal revision

comment:
We have uploaded a highlighted version of our paper, which has all the main changes colored blue for your easy reference. We have tried to do all and only the changes that we promised in our response. We have also tried to fix the typos etc to the best of our ability (these minor changes are not highlighted).
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper considers the feature sensitivity problem for ensembles of decision trees in a verification context. 

The reviewers generally agree that there is sufficient novelty in using a pseudo-boolean satisfiability encoding. The experiments indicate that this method is often superior to the state-of-the-art. 

Moreover, several weaknesses regarding presentation and clarity have been mitigated in the rebuttal phase. In particular, the experiments were improved, and hence, we recommend acceptance of the paper.