Sensitivity Verification for Additive Decision Tree Ensembles
Authors: Arhaan Ahmad
Tanay Vineet Tayal
Ashutosh Gupta
S. Akshay
Venue: ICLR 2025 Poster (2025)
Keywords: Robustness verification
Sensitivity analysis
SAT solvers
efficient encodings
NP-hardness
fairness
confidence
Primary area: alignment, fairness, safety, privacy, and societal considerations
TL;DR: We ask if an (additive) decision tree ensemble is sensitive to (potentially small) changes to a given feature or set of features. We show theoretical NP-hardness results, and provide a pseudo-Boolean encoding to solve the problem.

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.

Published as a conference paper at ICLR 2025
SENSITIVITY VERIFICATION FOR ADDITIVE DECISION TREE ENSEMBLES
Arhaan Ahmad, Tanay V. Tayal, Ashutosh Gupta & S. Akshay Department of Computer Science and Engineering, Indian Institute of Technology Bombay, Mumbai, India.
(arhaan, tanaytayal, akg, akshayss]8cse. iith. aitb.ac.in
ABSTRACT
Tree ensemble models, such as Gradient Boosted Decision Trees (GBDTs) and random forests, are widely popular models for 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 specific problem of feature sensitivity for additive decision tree ensembles and build a formal verification framework for 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 relates other verification problems. Next, provide novel encoding of the problem using pseudo-Boolcan Boolean constraints. Based on this encoding, we develop a tunable algorithm perform sensitivity analysis, which can trade off precision for running time. We implement our algorithm and study its performance on suite of GBDT benchmarks from the literature. Our experiments show the practical utility of our approach and its improved performance compared to existing approaches.
INTRODUCTION
Tree ensemble models, such as gradient boosted decision trees (Friedman 2001 and random forests (Breiman, 2001). are now widely used for machine learning tasks in domains ranging from banking applications (Madaan et al.) 202T) to computer vision (Criminisi & Shotton (2133) to trans- portation (Podgorelec et al. 2002). The power of these models comes from the ensembling or boost- ing, which known to empirically improve performance, unlike single decision trees, which are explainable and simple to understand but unwieldy model complex behaviour. XGBoost (Chen & Guestrin 2016), one such popular tree ensemble learning algorithm, shows remarkable performance with tree ensembles of size 100, where each tree has depth most or 6. Of course, the tradeoff with such modelling power is that it becomes difficult to predict and analyze these models, i.e., to ensure that they are reliable, robust, and behave as expected. This has led rich line of work in the last decade on formalizing and verifying different properties of tree ensembles.
The first such property is robustness checking which asks whether there are adversarial input per- turbations that could lead to misclassification. This problem has been addressed by several works over the past years including Chen et al. (2019b); Einziger al. (2019); Devos et (202]) I). us- ing different techniques ranging from optimization/IILPPP
(Kantchelian et al.) 2016) to SMT- solver based approaches (Ignatiev et al. 2020a). Using SMT-solvvrs allows one to give guarantees of soundness and completeness, which is highly desirable when dealing with reliability issues but often less scalable than purely optimization- between local (checking robustness around given input) and global robustness (checking for all inputs) where the universal quantifier makes the latter problem significantly harder (Chen et al. 2019b Leino al. 1) Many techniques also apply approximations (Devos al. 2021 I look at subclasses (Andriushchenko & Hein, (019). Indeed, this is unsurprising since Kantchelian et al. (2016), was shown that very simple related problem is already NP-hard.
approaches. The literature also distinguishes

---

Published as a conference paper at ICLR 2025
Another property of interest is the sensitivity of subset of inputs or features. A model is sensitive to a set of features if by keeping other features fixed and changing those features, the output of the model changes. In practice, models which are sensitive to very small subset of features are prone to adversarial attacks. This question has also been seen as a way to formalize fairness (e.g., Dw.rk] et al. (2012) or causal discrimination (e.g. Galhotra al. 2017 sensitive features as protected, and changing the decision based only on these features can be seen as being unfair. This formulation was also adopted in Calzavara et al. (2023), where an approximation algorithm was provided for the same problem. Further, the generic tool Devos et al. (2021) solves verification questions including sensitiiity/fairness, but provides approximate answers using optimization. A formal methods approach towards the problem is also provided in [gnatiev et al. (2020a), where the authors show how the fairness problem can be modelled as a global robustness query and hence relate the above problems. Another related approach in Törnblom & Nadjm-TThhran (2020) used abstract interpretation techniques for verifying tree ensembles.
be seen
In this paper, we launch a deeper investigation into the sensitivity problem for decision tree ensemble models, both from theoretical and practical perspectives. We start by observing that in most models and benchmarks, input feature. So the first question we ask is whether the problem remains hard even for a bounded number of features being changed. Second, if look at tree ensemble training algorithms, like XGBoost, we observe that the decisions done at leaves, though binary, are derived from real number values, obtained from confidence. This leads us ask if we can use these numbers as parameters to obtain a parametric notion of sensitivity, which can quantify "how sensitive features are" instead of just saying if they are sensitive or not. Third, we observe that existing encodings of the sensitivity problem either use one extreme of Boolean reasoning (e.g, SMT solvers in Ignatiev et al. (2020a)) or the other extreme of purely optimization based reasoning (e.g, MILP solvers in in/Kattchelian et al. (0166). Can we use other forms of powerful reasoning, such as sseudo-Boolens solvers, that have shown to be effective in other problems (Mexi et al., 2023) for the sensitivity problem? This forms the third question that try address in this work.
are only interested in checking the sensitivity of fixed few or even just one
Surprisingly, we show that even for a single feature, the sensitivity problem remains NP-hard. To show this, provide a novel reduction from 3CNF-SAT which in fact shows that the problem is NP-hard even when restricted to decision tree ensembles with trees of depth at most 3. Next, we introduce threshold parameter p to define the class change confidence for the sensitivity problem. In other words, if the output of the classifier is above p threshold, we say that the decision is 1 and if the output the classifier is below 1- p, we say that decision is O. This gives a natural tunable ver- sion of the sensitivity problem. Using this, we formulate the sensitivity problem as pseudo- -oooeen constraints. Our novelty in the encoding includes a new encoding of trees as geudo-Boolean con- straints, which is rather different from the encoding of trees done in Ignatiev et al.) (2020a) for the robustness verification problem. Using this novel encoding we model our property so that we can take advantage of recent advances in pseudo-Booles form experiments to illustrate that our algorithm has an order of magnitude better performance than the state-of-the--ar, In sum, our contributions are the following:
solving towards this problem. We then per-
1. We formulate parametric and bounded version sensitivity problem for additive decision tree ensembles and show that it is co-cleeee
2. We develop novel encoding of this problem using Boolean constraints.
3. We implement our algorithm and show that it outperforms state-of-the-arr publicly avail- able tools in suite of benchmarks.
We highlight that our hardness results and encoding ideas work for any tree ensemble which aggre- gates the trees by summing up the individual tree outputs (these sometimes called additive tree ensembles, see e.g., Devos et al. (202I).. Such models include GBDTs and random forests which follow an additive predictive model. In particular, our results are independent of the way by which the tree ensemble was trained (e.g, gradient boosting, etc.).
Other Related Work In addition to the work mentioned above, there are a few other lines of related work. SMT solvers and basver-based approaches and non-trivial encodings have been widely used for certifying robustness in neural networks and detailed frameworks such as DeepPoly (Singh
et al. 2019) and a, 3-Crown (Zhang al. 2018 2022 and some of these could also be related
2

---

Published as a conference paper at ICLR 2025
to sensitivity verification. However, there is comparatively less work using these approaches for decision tree ensembles, beyond the works mentioned the introduction. Another rich line of related work is to train robust tree ensembles. Calzavara et al. (2020), for instance, trains trees to make them more evasion aware while Chen et al. (2019a) provides a training method that makes the trees more robust. Our current foeus is verifying sensitivity but it would also be interesting to extend this to training insensitive models of tree ensembles. Finally, there is a relation between notions of explainability such as contrastive explainability and abductive explainability (Ignatiev et al., 2020b) and sensitivity or fairness. However, there is marked difference as we focus on global sensitivity based on given features, while explainability refers to the change of class with respect to or around an input. However, global notions of contrastive explainability could perhaps be related to our approach. As explained above, our approach works for random forests as well. A caveat is that the classical definition of random forests (Breiman] 200T) computes the final answer by max- maxx-pooiig rather than summing up. 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 Seikit-Learn (Pedregosa et al., 2011), do use a weighted average of the individual tree predictions to make the final decisions, which can be incorporated into our approach.
2 PRELIMINARIES
In the classification setting, given an input space X' C Rdd defined over d-dimensional space of features F, and an output space y which is a discrete subset of IR, there exists a unknown function : X + y that maps each element of X' its corresponding correct output in V. A classifier is function from X' to y which approximates / by learning from data. Decision trees and tree ensembles are well-known models used define classifiers.
Decision Trees A decision tree T' either a Icaf n with label n.val IR or an internal node n with two children n.yes and n.no decision trees, and a guard n.g. which is a Boolean formula involving the imput features. Typically, the Boolean formula is a linear inequality of the form f v, where f is a feature and is a real constant. Given an input z E X' the (binary) decision tree evaluates it top-down from the root, by evaluating the Boolean formulae the guards to determine the child to go to, and finally reach a leaf, where it returns the output value of the leaf encountered. For instance, guard = f < U, g(x) ) is true if xy < U, where I = (xy) This defines the output or outcome T(x) of tree T on input E X as follows: T(z) T.val, if T is leaf, else, it is recursively evaluated, i.e., if T (T()) is true, it is (T)) and if T. (g() is false, it is T.no(z).
Decision Tree Ensembles Rather than relying on a single tree to approximate the underlying function, decision tree ensembles utilize multiple trees, each learning different parts of the problem and then aggregating them to produce a single output. There are many different methods to train decision tree ensembles, and in this paper, focus on XGBoost (Chen & Guestrin 2016). a popular gradient-boosting algorithm. Formally, an ensemble model c [Ti,..., T' } is a set of decision trees. The ensemble model sums up the results of the member trees. We define the outcome of the ensemble model c as c(x) Ex= Tx(x). We will often refer to this value as the model's 's raw output. Note that the decision tree ensembles we consider in this paper are always additive (even we do not explicitly mention it), i.e., they aggregate the trees by summing up the results of individual trees.
Tree Ensemble Classifiers For classification tasks in many real-world applications. the output space )/ is finite, meaning that the set of possible outputs, commonly known as labels in this scenario, discretized. A tree ensemble classifier e decision tree ensemble with an output space y {0, 1.... A 1} where & is the total number of distinct classes. The output of the tree ensemble classifier is acquired by first calculating the raw output of the tree ensemble model c(x) E R and then mapping c(x) to its label from y We denote the output of the model Clabel X ).
A binary tree ensemble classifier a decision tree ensemble with an output space of size 2. To map the raw output binary output, i.c., in {0, 1}. one way is to set the output to 1 if c(x) 2 0 and 0 otherwise. However, widely used training methodologies (for instance, the XGBoost algorithm introduced in Chen & Guestrin (2016)) require to calculate intermediate value by applying
3

---

Published as a conference paper at ICLR 2025
the sigmoid function to the output. This can also be interpreted as a measure of the confidence of the model. and is of interest to us. Let c(z) be the raw output of the ensemble for imput z. To map this to probability space [o. 1), the sigmoid function is applied on c(x) making the
output: a (c(x)) = I+e stay This transformation gives us a (c(x)), which represents the probability that the input x belongs to the positive class (1). The closer a (c(()) is to 1, the higher the likelihood that æ is positive example, and vice versa. To calculate the final output (Charet), the output of the
sigmoid function is greater than equal to 0.5, we assign it to the class (1), and if the output is less than 0.5, we assign it to the class (0).
THE SENSITIVITY PROBLEM: MODELING AND HARDNESS
We now define the sensitivity problem for tree ensembles. For input X' and set of features F C F, let &p denote the projection of x onto F. When F = { we use xy to denote the scalar. Definition 3.1. Given tree ensemble classifier c is said to be F-sensitive, if we can find two inputs x, x' E X' such that ZF(F = z and Glael (x) + (xb). The sensitivity problem asks whether given tree ensemble classifier is F-sensitive to a given set of features F.
X' - V. and set of features F S F.
One issue with the above definition is that it just requires the two witness inputs to be classified dif- ferently but does not take into account their distance from the decision boundary (of the classifier). As explained earlier, classifier learning algorithms, in fact, provide this information. Consider the example in Figure [. where we have a two-tree Ti, T2 ensemble e that is trained to be a recommen- dation system for television shows. The input contains three features f1, [2 and fa that may take values between 0 and 30 with y = {0, 1}. It is easy to see that a₁ = (6, 2,4) and 02 (6, 17) are two imputs that vary only on feature fa but have c(a1)
0.1 1.2 -1.1 while c(a2) 0.7,
i.c., (a1) * (a2). However, the pair 31 = (6, 4, 14) and 82 = (8, 4, 14) varies only in feature fi and again has Gabel (B1) # Guaeel (532), but we notice that c(33) = 10.1 and c(32) = 9.9.
In practical scenario, one may argue that (31. (22 is much more interesting pair of inputs since it takes an almost sure positive prediction to a quite sure negative prediction, which can potentially be very harmful compared to an unsure prediction getting flipped.
f1 < 10
f2 < 3
F
T
F
T
fa
10
f2 <
f3
< 15
F
T
F
T
F
T
F
T
1.2
1.1
0.1
10
10
0.6
1.22
Figure 1: A tree ensemble with two trees 71, T2 having real-valued (raw) outputs on its leaves.
This motivates more nuanced definition that is parametrized by the difference using the sigmoid function a that we want to see in the inputs that witness the change in classification with respect to the sensitive features.
Definition 3.2. Given tree ensemble classifier e: X - V. a set of sensitive features F C F and parameter 2 0, is said to be (p, -ssensiiivee, if we can find two inputs x, X such that FF = x FiF and (c(x)) Z 0.5 + p. (c(x')) S 0.5 - p. The (p, F)-sensitivity problem asks given tree ensemble is (p, -)-snsiitiee with respect to given set of sensitive features F.
It easy see that the F-sensitivity problem is special case of the (p, F)--ssinitivitty problem. Hence, for our hardness results, we will focus on the F-sensitivity problem. However, for our
We note that this problem has been called causal discrimination in Calzavara et al. (2033 and faimeess in Dwork et al. (2012). While these are valid applications of the definition, the problem is itself closer to the analysis of sensitive features, and hence, we have called it such. Further, there many competing definitions of fairness in the MI. literature, and while this certainly one formulation, it is not the only one.
4

---

Published as a conference paper at ICLR 2025
encoding and algorithm in the next section, as well as experimental results later, we will use (p. F)- sensitivity.
Sensitivity checking for single tree decision models is known to be in polynomial time (Chen al. 2019b), but as we show next, this is not the case for general decision tree ensembles. We consider three variants of the problem, based on the size of the set of sensitive features F: (i) |F] 1 or the single feature sensitivity problem, (ii) |F] = A for any fixed constant & which we call the k-sized subset feature sensitivity problem and (iii) |P| FF the all-feature sensitivity problem. Note that the single feature sensitivity is the same as 1-subset feature sensitivity. Second, the k-sized subset feature sensitivity problem is only defined if the number of features in the problem instance i.e., [F] 2 k. Finally, the all-feature sensitivity cannot be seen as specific instance of the k-sized subset sensitivity problem since in the latter, k is a part of the input, while in the former, not.
We will now show that all three variants are NP-hard. We start by showing the NP-hardness of the single feature sensitivity problem and obtain the others as corollaries. Before going into our proof, we recall that the robustness verification problem for decision tree ensembles was shown to be NP- hard using a reduction from the so-called evasion problem for decision tree ensembles, which was shown to be NP-hard in Kantchelian et al. (2016) (where, evasion for given tree ensemble model c, asks whether there exists an æ E X such that c(x) > 0). However, while evasiveness can potentially be used to show hardness for the all-feature sensitivity problem, it cannot be easily lifted to show single or fixed subset feature hardness. Instead, we come up with a novel and direct reduction from the 3CNF-SAT problem show that single feature sensitivity is already NP-hard.
Theorem 1. The single feature sensitivity problem, i.c., checking whether given tree ensemble classifier is F-sensitive for FP = 1, is NP-hard.
Proof. We will show a reduction from 3CN,-SAT, the classical NP-hard question, which asks, given Boolean formula in conjunctive normal form (CNF) with 3 variables per clause, whether it is
satisfiable. Given an instance oo of 3CNF-SAT, let cl(pp) be the set of clauses {ch1, cla,,,l...........,.,,... el }. with [c(({)) and let var(p) denote the set of variables (UI, 02,-.., Un), with = |
Then from o we start by creating the formula g = = (#a+1 V Un41 V (2+1) which is also a 3CNF (Un41 V Un41 0n41). Observe that is satisfiable, i.e., there exists an input x E {0. 1)"h that satisfies sp iff yo is satisfiable, i.e., there exists an input x' {0, 13 |a+1 that satisfies yp. We will now show reduction to the (single feature) sensitivity problem. That is, we will construct a decision tree ensemble e with depth 3, such that c I-feature sensitive iff yp satisfiable.
formula with a new variable 1n+1 and new clause clm+1
In formula v², for every clause cl,, we create depth-3 decision tree T; as depicted in Figure 2 where m + = |cl()²)). That is, for each literal (i.e., e2 or mu;) in the clause, we add a "true" branch with output [ and "false" branch where we either continue to next literal or return -1 if there no more literals left in the clause. This is slight abuse of notation our definition earlier had guards of the form f < v, but this can easily be adapted. Now, for each literal, if it occurs positively as ii (resp. negatively as -u;), the true (resp. false) branch outputs ".P...
We form the decision tree ensemble e using the above decision trees with trees enumerated T, for
i E (1,2,..., m + = [cl(s')]), Note that in this case, the domain of e, i.e., X' {0, 10.1 1
U1
T
02
T
U3
1/S
F
[
(a): Clause 01 V 02 V U/
(b): Clause U1 V -U2 V -23
Figure 2: Given formula with [x)( clauses, each clause is replaced by tree above.
5

---

Published as a conference paper at ICLR 2025
Lemma 1. For all x E {0, 1]m+ we have (1)) iff ('(x) =1, ie.. xr satisfiess/models yp.
Proof of Lemmal
There are two possible scenarios for an input
The input satisfies the 3CNF formula yp,, i.e., (x())) = 1. In this case, each of the m clauses satisfied the input, and thus, for all trees T, we have (x)x) m+11 Thus,
Eee (x) > 0
(a)) =
The input does not satisfy the 3CNF formula y Thus, clause exists that is not satisfied by the input. Let that clause be clj. By the construction of for the corresponding tree, Ty (x) 1 and for all i + j. (xx) m-1 Thus, Dm1 D.t.s Claba( = O. 0
(x) -1+ m+1 m+1
Now, we use the above lemma to prove hardness of sensitivity. More precisely, we will check sensirivity with respect to the single Boolean variable tn+1- Call the of all features F and the set for sensitivity checking F = [#a+1]- To complete the proof, we will show that e is F-sensitive iff xp' is satisfiable.
In one direction, if is F-sensitive, by definition, there exist x, x' E {0, 1] with #1F d'IF such that (aaee (x) 1 and Caree O. Thus, we immediately infer that there exists æ such that (z) = 1, which by the above lemma means that x satisfies of and hence of is satisfiable. In the other direction, if is not F-sensitive. Then for all ILF E {0,1)", 1)", for all possible choices = (11F(( But now, if we consider 2r = 0,
of Tx, p'p. we must have (Z then the decision tree Tm+1 will evaluate to since cl [M++1 +> = 0. As result, we can conclude that for any ILF E {0, 1]", we have E (T(LFF 0) < -1+ m+1 < 0 and so Qlael (# r. 0) O. Thus, for any P5 E 1), Glabel FF. = O, which implies that for all {0, 1]=+1, (x) satisfiable.
m
Again, appealing to Lemma Jbbve, we can conclude that yp is not
Thus, have reduced the problem of finding satisfiability of o' to that of checking sensitivity for feature set of size 1, and hence, the latter problem is NP-hard.
We can now infer some interesting corollaries. First, we observe that the above proof can be lifted from single feature sensitivity to k-sized subset feature sensitivity for any fixed k. Given an arbitrary instance of the single feature sensitivity problem, we can construct an instance of k-sized subset feature sensitivity (for |F| k) by introducing k - 1 new dummy variables to the problem. These dummy variables are part of our input to sensitivity checking, but they not affect the tree's output in any way (formally, one way to do this is to have decision tree stumps on these variables that output zero irrespective of the variables' values). Thus, checking for sensitivity for k-sized subset of features will be equivalent to checking for sensitivity for just the first feature in the original instance and hence, checking sensitivity with respect to a given fixed size the subset of features is also NP-hard.
Corollary 1.
For any fixed constant k, the k-sized subset feature sensitivity problem for decision tree ensembles is NP-hard.
The above argument holds for any k-sized sensitive feature set. But this does not immediately imply that it can be lifted to the case where all features are sensitive, i.e., Fl = [F]. Indeed, one could imagine that the all-feature sensitivity problem could be easier. However, by modifying the proof above, we can show that this problem is also NP-hard. As the proof is very similar, we leave its details to Appendix A
Corollary 2. The all- ill-feature sensitivity problem for decision tree ensembles is NP-hard.
Finally, important remark is that our NP-hardness proof requires trees in the ensembles that have depth 3. This leaves open the intriguing question of whether the (single/k-sized subset/all) sensitivity problem is NP-hard for tree ensembles where the depth of each tree is at most 2. Unfortunately,

---

Published as a conference paper at ICLR 2025
proofs cannot be extended to this since they rely the hardness of 3CNF-SAT, which requires variables per clause, which we translate to depth trees. However, 2CNF-SAT is poly-time solvable and hence not useful for showing hardness. We expect that different techiqque/rcducctooneeoodoii will be needed to resolve this question, and we will leave this for future work. We also note that fix the number of trees and vary the depth, or if we fix the depth and vary the number of trees, NP-hardness follows, while if we fix both the number of trees and depth, then the problem is easy.
Above, considered hardness results. On the other hand, for all the problems mentioned above, can obtain NP upper bounds. To see this, note that given a candidate solution i.e., values of inputs x and x' that only differ on the set of sensitive features we can evaluate the decision tree top-down and check whether it is valid solution or not, i.c., the decision for z differs from the decision for x'. Thus, both F Fenssitvvity and (p, -ssesiiiiv problems are NP hence they are NP-complete.
ENCODING THE SENSITIVITY PROBLEM
In this section, will consider encoding the problem of sensitivity of binary tree ensemble classifier e into solving a set of pseudo- Boolean constraints (Boros & Hammer 2002), which are arithmetic constraints containing only Boolean variables.
First, we observe that the general p-sensitivity problem in Definition 3.2 can be written as the prob- lem of the search of the p-sensitive pairs of inputs x, x'' for the set of features F as follows
Bx, x', (A 2f z'y Ao(c(z)) 2 0.5 ppoo(((('())) 0.5 -p
J'EF(F
Since the output of the classifiers is via the sigmoid function, we compute the inverse of the function to compute the required gap between the inputs the sigmoid function. Let = a (0.5 + p)
log 0.5+p
where - is the inverse of sigmoid. Let be decision tree ensemble with m trees
0.5 0.5-P)
Ti.... Tm The problem translates into
2f = o'p (A
Dx,z',
A P'EFFF
T((x) 28))
Tx())s
Let us start encoding the above constraints using a pscudo-Boolean encoding.
Encoding inputs The range of feature f is [-oc, oo]. However, naturally divides the input into segments, which we define as follows. Let Gy be the set of guards on feature f e. Let the set of thresholds be Cy {ulf < divided in by + 1 segments by Cy. We can encode the segments using ky bits. For 0 < j< [C let bit bifj indicate that feature is less than Cy[i] in input and let bit bafj indicate that feature less than Cy in input x'. We need to include constraints which encode that the boundaries are in increasing order, follows
G2} sorted in ascending order and let ky = =Cyll The range of
befs + bof(++)
(I)
We also need to say for each f $ F, and x' will agree. Therefore, for each j E (1...ky. ky we add
bifi= = b2fi
Encoding tree We need to encode the structure of the trees in constraints. Let lajin indicate that the node E T7 is visited when evaluating Tx(r))). Let the root node of T, be denoted by r,, Since the roots of all the trees are necessarily visited, the following bits are always true
tgrrs
(3)
For each internal node n E Tú, let (f < <) that if is visited, and (f v) is true, then n.yes is visited otherwise. n.no is visited.
= n.g such that Cy = v for some j. We need to say
(tqin A buts tgg((.gess) A (tgin A -bys3 tgs((.no))
(4)

---

Published as a conference paper at ICLR 2025
For each tree T, may also optionally add the following constraints to help the solver to know that, at most one leaf of T2 can visited by the input. We denote the set of leaf nodes for a tree Tç by Felleeess
Egin =
(5)
Encoding output We need encode the condition that the sum of the tree outputs is greater than 5 for x and less than 6 for x'. Remember that the label of a leaf E Ti is real value with infinite precision. We discretize this real value into steps of size 1/ax where is the precision factor in our encoding. For the encoding of z, we multiply the leaf value n.val by and take the ceiling of the result. This constant integer then multiplied by the corresponding tin-- The ceiling operation increases the sum, which is then compared to the bounds derived from the floor of aò. Similarly, we impose constraints for the output of x'.
m
m Σ
Σ
tion jat.val]
2 |ad] A
tzin lat.val)
s [-00
(6)
M.T..eeavee
lnneess
The above equations are the set of pseudo- pseudo-Boolean Boolean constraints.
Our encoding of the problem differs significantly from the presented in Ignatiev al. (2020a) which a direct SMT encoding of trees and their verification query. The problem we address is similar to the knapsack problem, and an appropriate encoding for it seems to be through pseudo- Boolean constraints. Encoding the problem as SMT constraints, as done by [gnatiev et al. (2020a), may result loss of structural information, preventing the solver from fully leveraging the pseudo- Boolean nature of the constraints. We solve these constraints using pseudo-Boolean Boolean solver to check for p-sensitivity. We have the the following guarantees for the result that we obtain.
Theorem 2 (Completeness and a-soundness).
1. If conjunction ①1
6 is unsatisfiable then the classifier is not (p, F) -senssivee
2. Otherwise, there is a counterexample pair (ar, such that e(x) 2
8
T22 +1 and c(x') <
-6 + m+1 where 8 log
0.5+2 and is the precision parameter of our analysis.
0.5
Proof sketch. Since the floor and ceiling operations are in conservative directions, 1 is true. In case of satisfiable constraints, there will be exactly m bits that are the sum in (6). The pre-sigmoid output in the reported counterexamples will be closer to zero by amount (m + 1)/a in 6, due to m ceiling/floor operations on the left-hand side of the incqualities and one ceiling/floor operation on the right-hand side in 6 Therefore, 2 holds.
As increase a, the precision of our counterexamples improves. Thus, corollary, which states that if a is sufficiently large, the counterexamples will be precise.
prove the following
Corollary 3. There exists an a such that every counterexample pair (r, x') satisfying the above Axeudo-Boolean formula will satisfy a (c(x)) 2 0.5 + and (c((r)) < 0.5 -
Proof Sketch. In the non-approximated constraint Σm difference between 5 and the sum closest to, but less than 8. If this difference is larger than (m + 1)/a, then there can be no extra counterexamples due to the imprecision of the encoding by Theorem
Jeaves lintt.al 6, consider the
EXPERIMENTS
In this section, we present our tool. SENSPE which implements the above method for p-sensitivity checking. The tool is developed in Python and utilizes Z3 (de Moura & Bjorner (008) as its backend Beuue-Booleann solver. We also tried dedicated pseudo-Boolean solver (Elffers & Nordström) 2018), but its performance was similar, so we kept to Z33 Our tool accepts input binary classifier
https::/ httpps///ggtthb...co///aaa/////
8

---

Published as a conference paper at ICLR 2025
Details
SENSPB time taken (s)
Benchmark Name
SMT
#Trees
Depth
#Feat
Min
Max
Average
Breast cancer robust
4
5
2.72
2.81
2.76
2.76
Breast cancer unrobust
4
6
11
2.75
2.82
2.8
2.8
Diabetes robust
20
5
3
3.2
3.02
3.443
Diabetes unrobust
20
5
3.4
23
5.8
57.2
Cod-rna unrobust
80
4
8
7.2
12.9
8.3
106
Binary MNIST robust
50
784
14.6
15.3
14.9
тO
Higgs unrobust
100
8
28
130
TO
1188
TO
IJCNN robust
60
8
16
TO
330.7
TO
Synthetic
100
6
10
5.36
5,85
5.57
TO
Synthetic
125
6
10
6
6.35
6.2
TO
Synthetic
150
6
10
7.09
8.19
7.36
TO
Synthetic
175
6
10
6.25
6.57
6.37
TO
Synthetic
200
10
4.40
124.51
16.48
TО
Table 1: Times taken for verifying countering sensitivity of all singular feature sets. The Min, Max and Averages SENSPB times are taken by running the tool with different features of the benchmark tree ensembles the sensitive feature. More information on these experiments is avail- able in Appendix B
XGBoost model, set of features for which sensitivity is being assessed, the parameter p, and precision parameter a. If the model is not sensitive, the tool outputs "pass". Otherwise, returns pair of inputs that demonstrate p-sensitivity the specified features.
To assess our method, we begin by running our tool on a set XGBoost models from Chen et al. (2019b). Additionally, evaluate the performance our tool, train XGBoost models with varying numbers of ensemble trees on 100,000 randomly generated data samples. 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 ran the experiments on an Ubuntu machine with 20 1.3GHz cores, which has 64GB RAM.
There have been several tools Devos et al. 2021
Torbblom & Nadjm-Tehranii 2020 Chen et al.,
2019h, Ignatiev et al. 2020a Calzavara al.) 2023] Kantchelian et al., 2016) that implement dif- ferent variants of verification for tree ensembles. In our experiment, we compare SENSPB with the closest approach in VERITAS (Devos et al. 2021) and an SMT-based approach presented in Ignaticv We used own implementation of the SMT-based approach with Z3 (de Moura & Bjørner 2008 as the SMT solver. We did not compare with Calzavara et al. (2033) as it only sup- ports random forest trees and we unable to make work with XGBoost models. Finally, did not include a comparison with Kantchelian et al. (2016) since VERITAS has already demonstrated superior performance over this tool, albeit for the problem of local robustness verification.
et al. (220aa.
We ran SENSPB on the benchmarks, and the results are presented in Table For each benchmark ensemble, in one experiment we pick feature f and run SENSPB on the ensemble to check whether the classifier is p-sensitive to f. We repeat this experiment over all possible f. and the maximum, minimum and average time taken by for termination is reported. We set timeout of I hour for each experiment. In our experiments, we have set gap p 0.15 and precision a 10 x # [Tees]]. For the SMT solver-based approach, our experimental setup is the same as SENSPB and we report the average time taken. More experiments can be found in Appendix C
VERITAS does not solve the sensitivity problem directly. We instead ask VERITAS to maximise the difference between the outputs produced by two inputs which differ only in feature. We define the bounds found by VERITAS being "better than" the ones found by SENSPB the difference in the upper and lower bounds found by VERITAS is greater than 2p. Note that this is very relaxed defi- nition since the bounds found by VERITAS might have a larger spread but might still be lying in the same output class. Since we considered two kinds of experiments for fine- tineggrined comparisons between the performance of SENSPB and VERITAS.
stop V VERITAS anytime and observe the best solution found till then,

---

Published as a conference paper at ICLR 2025
Time Taken (in seconds)
Accuracy comparison
Benchmark Name
SENSPB
VERITAS
1x
2x
5x
3600
Breast cancer robust
2.7
2.5
81.82%
81.82%
81.82%
81.82%
Breast cancer unrobust
2.7
2.53
45.45 %
45.45%
45.45%
45.45%
Diabetes robust
3.0
3.2
77.78%
77.78%
77.78%
77.78%
Diabetes unrobust
5.9
198.1
55.56%
66.67%
77.78%
88.89%
Cod-rna unrobust
8.3
346.2
0.00%
0%
25.00% TO
37.50%
Binary-mnist robust
14.9
TO
TO
TO
TO
Higgs unrobust
1188
TO
TO
TO
TO
TO
IJCNN unrobust
330
OOM
TO
TO
0%
OOM
Table Runtime Comparison by letting VERITAS run on benchmarks with a timeout of 3600s. 2) Accuracy analysis of VERITAS with the timeouts set to different values, depending on the time took SENsPB. The percentages recorded represent that fraction features where VERITAS gave better than or equívalent results as compared to SENSPB. For Time Analysis, TO implies that VER- ITAS timed out without reaching an optimal difference, while in the Accuracy measurements, TO means that VERITAS timed out without producing single valid solution.
Firstly, we asked if we fix timeout of 3600s, how does the performance of VERITAS compare with SENSPB, i.e., how long does it take VERITAS to reach an optimal solution? The results are present in the Time Analysis part T For the Binary MNIST robust and the Higgs unrobust benchmark ensembles, VERITAS always times out without producing single solution. For IJCNN robust, VERITAS runs out of memory after roughly 900s.
Secondly, we asked if we VERITAS for the time relative to the time taken by SENSPB, what would be the relative performance? Let the time taken by SENSPB be æ. We run VERITAS for sensitivity analysis, look at the bound produced by VERITAS at the end of the timeout and compare this bound to the bound found by SENSPB. In the accuracy comparison section of Table 2 report the percentage of features in which VERITAS performed better than or equivalent to SENSPB. As expected, on increasing the time given VERITAS, starts performing better more and more features, e.g., Diabetes unrobust and Cod-rna unrobust. However, even on running VERITAS for 3600s, there are many features in which SENsPB performs better. As noted earlier, for our three largest benchmarks, VERITAS does not produce a single solution in the time given.
feature at a time, with the following timcouts: I, 2x, 5z and 3600. We
Our experiments clearly demonstrate that our pseudo-Boolean encoding significantly outperforms both the standard encoding and output coniguration-basee approaches by an order of magni- tude. Given that the problem NP-hard, SMT-based approaches are likely to surpass output configuration-based methods unless those methods are highly optimized. An SMT solver typically uses CDCL along with Simplex to solve the problem but may not fully exploit the specialized nature of our problem, particularly the limited role of arithmetic during bit summation the output. As result, pseudo-Boodd Boolean solvers specifically designed for such problems are expected to deliver the best performance. Our encoding allows to not only use pseudo- pseudo-Boolean Boolean solvers but also provide new sets of benchmarks for the solvers. The availability of the henchmarks would likely improve the performances of the solvers.
CONCLUSION
In this paper, we investigated the sensitivity problem in two variants, the exact and a parametrized version. We presented new hardness proofs as well as an efficient encoding into gseudo-Boolcan constraints. Our implementation allowed us to exploit the recent advances in Aseudo-Booless solvers to solve the p-sensitivity problem. We successfully addressed XGBoost models of prac- tical sizes, including scores features, hundreds of trees, and a depth of 6-8. We believe that our work, especially the pseudo-Booleat encoding, opens new direction for scalable solutions for sen- sitivity and general verification problems for tree ensembles. For instance, an immediate extension would be to consider other tree ensemble models, such as random forests. Another natural future direction is also towards the question of multiclass labels, e.g., as done in Devos et al. (2024) for robustness verification.
10

---

Published as a conference paper at ICLR 2025
ACKNOWLEDGEMENTS
We acknowledge the SBI Foundation Hub for Data Science & Analytics, IIT Bombay for supporting the work done in this project.
REFERENCES
Maksym Andriushchenko and Matthias Hein. Provably robust boosted decision stumps and trees against adversarial attacks. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelz- imer, Florence d' Alché-Buc, Emily B. Fox, and Roman Garnett (eds.), Advances in Neu- ral Information Processing Systems 32: Annual Conference on Neural Information Pro- cessing Systems 2019, NeurlPS 2019, December 8-14, 2019, Vancouver, BC, Canada, pp. 12997-13008 2019. URL
wtt../ipp...pppppee///00... html
Endre Boros and Peter L. Hammer. Pseudo-boolean optimization. Discrete Applied Mathemat- ics, 123(1):155-225, 2002. ISSN 0166-218X. doi: http::/ooioog//o0000666666666662
00341-9. URL https: www.ncewww....ii..tctcct rect /eaect.cco//cceeee/aarttll/////
50166218X01 01662288000034111
Leo Breiman. Random forests. Mach. Learn., 45(1))5-32, 2001. doi: 10.1023/A110109333444222
URL httt:ps:/doo..rr/11.11222222
Calzavara, L. Cazzaro, C. Lucchese, and F. Mareuzzi. Explainable global fairness verifica- tion of tree-based classifiers. In 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SuTML), pp. 1-17, Los Alamitos, CA, USA, feb 2023. IEEE Computer Society. doi: 10.1109/SaTMMI54400 2023.00011. URL atttps://dii eeeecompttersccieey..org N0.1109/SaaML5544 2023. 00011
Stefano Calzavara, Claudio Lucchese, Gabriele Tolomei, Seyum Assefa Abebe, and Salvatore training evasion-aware decision trees. Data Min. Knowl. Discov. 34(5): 1390-1420, September 2020. ISSN 1384-5810.
Orlando. Treant:
doi: (0077//10611-020-0066000 000000064--99
URL
https://doo orooorgggoo.ooo /10 1007/s
Hongge Chen, Huan Zhang, Duane S. Boning, and Cho-Jui Hsieh. Robust decision trees against adversarial examples. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp. 1122 1131.PMLR. 2019a. URL httt:::/proceeddiiiett
m.r. wwt....ww.sss..../.m wwtp//////hheeee 9m. html
Hongge Chen, Huan Zhang, Si Si, Yang Li, Duane S. Boning, and Cho-Jui Hsich. Ro- bustness verification of tree-based models. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d' d'Alché-Buc, Emily B. Fox, and Roman Gareet (eds.), Advances in Neural Information Processing Systems 32: Anmual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC. Canada, pp. 12317-12328, 2019b. URL httpsss/ppooeeeeingggssssss/ssst neurrip wwteerris.cc/ppapa.. catssscccpppppp pctpappr/20199
Tianqi Chen and Carlos Guestrin. Xghoost: A scalable tree boosting system. In Balaji Krishnapu- ram, Mohak Shah, Alexander J. Smola, Charu C. Aggarwal, Dou Shen, and Rajeev Rastogi (eds.), Proceedings of the 22nd ACM SIGKDD International Conference Knowledge Discovery and Data Mining, San Francisco, CA, USA, August 13-17, 2016, pp. 785-794, ACM, 2016. doi: 10. 111144/2999622.99977777 URL hwtph:tt/////m /oi wtt.://...rr...................0
htttss://do..rgg.
Antonio Criminisi and Jamie Shotton. Decision forests for computer vision and medical image analysis. Springer Science & Business Media, 2013.
Leonardo de Moura and Nikolaj Bjørner. Z3: an efficient smt solver. volume 4963, pp. 337-340, 04 2008. ISBN
doi: 100009978-3-544-78800 24.

---

Published as a conference paper at ICLR 2025
Laurens Devos, Wannes Meert, and Jesse Davis. Versatile verification of tree ensembles. In Ma- rina Meila and Tong Zhang (eds.), Proceedings of the 38th Interationnal Conference on Ma- chine Learning, ICML 2021, 18-24 July 2021, Virtual Event, volume 139 of Proceedings of Ma- chine Learning Research, pp. 2654-2664. PMLR, 2021. URL http:httt:///oroe
ngs mmlr.
press/v 31sss//vl3d//vvs2llls html
Laurens Devos, Lorenzo Cascioli, and Jesse Davis. Robustess verification of multi-class tree en- sembles. Proceedings of the AAAI Conference on Artificial Intelligence, 38(19):21019-21028, Mar. 2024. doi:
wwtp://aaa..iiii....... 930093. UtI.httss://ojs..... aaaii http:/inex..ppppp php/ AAAT SAAT/artiicleeveeww//aao..
Cynthia Dwork, Moritz Hardt, Toniann Pitassi, Omer Reingold, and Richard S. Zemel. Fairness through awareness. In Shafi Goldwasser (ed.). Innovations in Theoretical Computer Science 2012, Cambridge. MA, USA, January 8-10, 2012, pp. 214-226, ACM, 2012. doi: 10.1145/ 2090236.000055.. URL
2tt.a//c.r....1115000002266662.0 2090255
Gil Einziger, Maayan Goldstein, Yaniv Sa'ar, and Itai Segall. Verifying robustness of gradient boosted models. In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances Artificial Intelligence, EAAI 2019, Hon- olulu, Hawaii, USA, January 27 February 1, 2019, pp. 10. (1GG0//AAAAAL3330..3330000
AAAI Press, 2019. doi: URL https: /dwi wrg.i..rg/100 1609/ aaaii v33101.
33012446
Jan Elffers and Jakob Nordström. Divide and conquer: Towards faster pseudo-boolent solving. In Jérôme Lang (ed.), Proceedings of the Wwenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pp. /1119////11111111111111111111110 htttpp:://cc...or////.. 2wwp2//4c3ccc.....//.//..
ijcai.org, 2018.
doi: 10.24963///CAAA2001//////
Jerome H. Friedman. Greedy function approximation: A gradient boosting machine. The Annals of Statisstics, 29(5): 189 1232, 2001. doi: 10. (0.1214//00/0001333555 URL https:///oi.
org 10. 11w............... aos wtw.///////s//// 1000003511112335
Sainyam Galhotra, Yuriy Brun, and Alexandra Meliou. Fairness testing: Testing software for dis- crimination. CoRR, abs/170090333
2017. URL http::////// wwapezivv.rrggaaao org /abs/ aaaaaasss/1///
Alexey Ignatiev, Martin C. Cooper, Mohamed Siala, Emmanuel Hebrard, and João Marques Marques-Silva. Towards formal fairness in machine learning. In Helmut Simonis (ed.), Principles and Practice of Constraint Programming 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings. volume 12333 of Lecture Notes in Computer Science, pp. 846-867. Springer. 2020a. doi: 10. 000007778--000584447 10. 1.01000/978 3 030 58475-7-444 49
URL httpt:tt////// org/
Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and João Marques- From contrastive to ab- ductive explanations and back again. In Matteo Baldoni and Stefania Bandini (eds.), AIxIA 2020 Advances in Artificial Intelligence XIXth International Conference of the Italian Association for Artificial Intelligence, Virtual Event, November 25-27, 2020, Revised Selected Papers, vol- ume 12414 of Lecture Notes in Computer Science, pp. 335-355- Springer, 2020b. doi: 10.1007/ 97
77091-4),91111 21. URL https: /tops://doo.. /oii.iiioo///o wrt. /0/ 100 101-11100077-----008 3-
21
Alex Kantchelian, J. D. Tygar, and Anthony D. Joseph. Evasion and hardening of tree ensemble classifiers. In Maria-Florina Balcan and Kilian Q. Weinberger (eds.), Proceedings of the 33nd International Conference on Machine Learning, ICML 2016, New York City, NY, USA, June 19- 24, 2016, volume 48 of JMLR Workshop and Conference Proceedings, pp. 2887-2396.. JMLR.org, 2016. URL http:lttp:p//e htttp::/proceeednggg
ml http:///weeeaeen..reeprreereeear liweschhhhiinnnn ian 1 6. html
Klas Leino, Zifan Wang, and Matt Fredrikson. Globally-robust neural networks. In Marina Meila and Tong Zhang (eds.), Proceedings of the 38th International Conference on Machine Learning, ICML 2021, 18-24 July 2021, Virtual Event, volume 139 of Proceedings of Machine Learning Research, pp. 2212-6221 PMLR, 2021. URLhttp: /ttp:////cccc.cc...c/ooo mlr. .press/s133/ leino21s La..a.......... html
12

---

Published as a conference paper at ICLR 2025
Mehul Madaan, Aniket Kumar, Chirag Keshri, Rachna Jain, and Preeti Nagrath. Loan default predic- tion using decision trees and random forest: A comparative study, 1OP Conference Series: Mate- rials Science and Engineering. 1022:012042, 01 2021. doi: 10.
Gioni Mexi, Timo Berthold, Ambros M. Gleixner, and Jakob Nordström. Improving conflict analysis in MIP solvers by pseudo-boolean reasoning. In Roland H. C. Yap (ed.), 29th In- ternational Conference on Principles and Practice of Constraint Programming, CP 2023, Au- gust 27-31, 2023, Toronto, Canada, volume 280 of LIPlcs, pp. 27:1-27:19, Schloss Dagstuhl LLibmniz-Zentrum für Informatik, 2023. doi: 01.42300LPPCCSS.CP2222222 URL. https: //dei.
11/30/LIPICS. CP. 2023.27
F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Pretten- hofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-leam: Machine learning in Python. Journal of Machine Learning Research, 12:2825-2830, 2011.
Vili Podgorelec, Peter Kokol, Bruno Stiglic, and Ivan Rozman. Decision trees: an overview and their use medicine. Journal of medical systems, 26:445 16155-463,41 2002.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3(POPL):41:1-41:30 2019, doi: 10. 1145/3290354. URL https:://oi. wwt.:ooi.orgggggoo org/ 0145/ 3290354
John Törnblom and Simin Nadjm-Tehrani.. Formal verification of input-output mappings of tree
ensembles. Science of Computer Programming, 194:102450, 2020. ISSN 0167-6423. doi:
https://doi.org/100 /10. 10100.000////cccc22000000 1024,000 102450. URL httpt:ttt//// /tttps::/www.... sciencedi reett com/
Huan Zhang, Tsui-Wei Weng. Pin-Ye Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett (eds.), Advances in Neural Information Processing Systems 31: Annual Conference on Neural Infor- mation Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, pp.
2018. URL https: htRpLhtttt///toooo// /ttp:ee:///proceiigggs.. hww.eeeeddinnn........s.......ss CC/ 00 -bsttratttttttte.ttttt.t........ .htt..ttll...........
Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. General cutting planes for bound- prondddpopagainn-baaa based neural network verification. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Ad- vances Neural Information Processing Systems 35: Annual Conference on Neural Informa- tion Processing Systems 2022, NeurlPS 2022, New Orleans, LA, USA, November 28 December wwwppppp.cppppp.pppppppp filerrrffieeeeee httppp/p..ppppppppeeeeee/ee/////
9, 2022, 2022. URL h (ol.eeee7eeebe333eee333331111313 Corere
13

---

Published as a conference paper at ICLR 2025
A ADDITIONAL THEORETICAL RESULTS
A.1 PROOF FOR COROLLARY 2
The proof of Theorem I can be directly lifted with some minor changes to prove Corollary Instead of checking sensitivity for F = {*n+1). we check sensitivity for F in the same setting. The first direction holds with the same argument as before. The reverse direction also holds with the same argument with the following changes.
TLF F is empty
zF E {0, 1),1)*+1 m+ instead of {0, 1}
However, for the sake of completeness, we give the full proof below.
Proof. As before, we show reduction from 3CNF-SAT. Given an instance y 3CNF-SAT, let cl(pp) be the set of clauses {cl,, cl,...,.ccc
of variables {ui, 02 ....... J, with cl "p' = A (Vn+1 V Un+1 V #a+1) which is also 3CNF formula with new variable Un+1 and a new clause clm+1 = (Ux+1 V Un+1 V en+1). Observe that & is satisfiable, i.c., there exists an input E {0, 1)" that satisfies ip iff yp is satisfiable, i.c., there exists input x' E {0, 1]ntt that satisfies s². We will now show a reduction to the (single feature) sensitivity problem. That is, we will construct decision tree ensemble with depth 3, such that is 1-feature sensitive iff o is satisfiable.
with m = |cl(pp) and let var(f) denote the set [ Then from y we start by creating the formula
In formula x for every clause el,, we create depth-3 decision tree T; depicted in Figure where m + = ccl())). That is, for each literal (i.e., ii or mi;) in the clause, we add a "true" branch with output [ and "false" branch where either continue next literal return
-1 there are no more literals left in the clause. For each literal, if it occurs positively as o; (resp.
negatively as -w;), the true (resp. false) branch outputs [e](or]] We form the decision tree ensemble
e using the above decision trees with trees enumerated T, for E {1, ..... + |cl()')) }
Note that in this case, the domain of c, i.e., X' = {0. 1).1)*+1 Remember that Lemma 1 says that for all E {0, 1) 1 we have c(x) = 1 iff (xx = 1, i.e., æ satisfies/models y'
Now, we use Lemma prove the hardness of sensitivity. More precisely, we will check sensitivity with respect to the singleton Boolean variable Un+1. Call the set of all features F and the set for sensitivity checking F = F. To complete the proof, we will show that c is F-sensitive iff s is satisfiable.
In one direction, if è is F-sensitive, by definition, there exist x, x' E [0,13**+ such that c(x) = and c(x') 0. Thus, we immediately infer that there exists such that c(x) 1, which by Lemma means that x satisfies s and hence ş is satisfiable. In the other direction, if is not F-sensitive. Then for all possible choices of æ. F
must have c(ær) c(x'r) But now, if we consider Teat1 = 0, then the decision tree Tm+1 will evaluate to -1 since cl [Vn+1 - 0 = 0. As
result, we can conclude that for any IF((e. 1} E {0, 13", we have Em+1 (I m 0 and so c(IrM/vt+1> 0) 0. Thus, for any oF E {0, 11m+1, c(IF) O, which
implies that for all æ E {0,1] c(x)) = 0. Again, appealing to Lemma we can conclude that op' is not satisfiable.
Thus, we have reduced finding satisfiability of up' to checking sensitivity for the whole input feature set, and hence, the latter problem is NP-hard.
An interesting question that arises from the above proof is the requirement of the new clause clm+11- What we require is input which does not satisfy y'. If there is no such input, then even when the decision tree ensemble is insensitive to the set F, the 3CNF formula yf can satisfiable. Thus, to ensure such an input exists, add the clause el.
14

---

Published as a conference paper at ICLR 2025
A.2 HARDNESS OF THE DIFFERENTIATING INPUT PROBLEM
From the same construction of trees in Theorem | we can show that a novel yet interesting problem. which we call the differentiating input problem, also NP-hard.
Definition A.I. Given two tree ensemble classifiers
X' - y and c' X - V we say a differentiating input for them c(z) * d((x). Given two tree ensemble classifiers y. the differentiating input problem asks if there exists a differentiating input, i.e.,
I E X
c, X R E & c(x) # (z))
Corollary 4. The differentiating input problem for decision tree ensembles NP-Hard.
Proof. We will show reduction from 3CNF-SAT this problem. Given an arbitrary 3CNE-SAT
problem, we can create a decision tree classifier that solves this problem. Given an instance of 3CNF-SAT, let el())) be the set of clauses {cl1, clg,..., clm.. J, with m |cl())]. Then, for each clause cl, = 1 V 12 V la in the 3CNF-SAT problem, create a decision tree, T; such that Tx(x) = 1 satisfies the clause and (x = otherwise. Two examples for the same are shown in Figure 2 a) and b). The ensemble = {7i, T2...., m outputs positive class (+1) if and only if the 3CNF-SAT formula was satisfiable as shown in the proof of Theorem []
m
Finally, we create another tree ensemble c'. which always returns a negative class(-1). Thus, asking whether there is a differentiating input for these tree ensembles equivalent to asking whether the 3CNF-SAT formula was satisfiable, thus completing the hardness proof.
B MORE INFORMATION ON THE EXPERIMENTS
The following table gives the fraction of all the features to which the benchmark trees are singularly sensitive.
Benchmark Name
Number of Features Ran On Percentage of Sensitive Features
Breast cancer robust
18.2
Breast cancer unrobust
36.4
Diabetes robust
44.4
Diabetes unrobust
80
Cod-rna unrobust
100
Binary mnist robust
10
Higgs unrobust
10
100
IJCNN robust
100
Table 3: Percentage of Sensitive Features
C ADDITIONAL EXPERIMENTS
We run experiments understand the effects of changing p and a (separately) on the running time of our algorithm. For these, we work only on the IJCNN robust benchmark, which has 60 trees, with maximum depth of 80 and 23 features and is good representative of the kind of ensembles we aim to verify. While changing p. we keep the value of a fixed to the value we used in the main experiments (i.e. x #Trees)) ). Likewise, while varying a, we keep p fixed to 0.15. These results are present in Tables [] We also give table detailing the fraction of features where SENSPB performs better than VERITAS, see Table 6
15

---

Published as a conference paper at ICLR 2025
Time (s)
100
16.26
200
15.79
Time (s)
500
15.79
0.1
15.8
700
16.17
0.15
16
1000
15.67
0.2
17.0
1500
22.39
0.4
1100.0
2000
19.01
0.45
923.4
5000
19.63
100000
16.58
Table 4: Effect of changing gap
1000000
16.71
Table 5: Effect of changing precision
Benchmark Name
VERITAS better
%SENSPB better
Breast cancer robust
81.82%
18%
Breast cancer unrobust
45.45 %
54.55%
Diabetes robust
77.78%
22.2%
Diabetes unrobust
55.56%
44.44%
Cod-rna unrobust
0.00%
100%
Binary-mma robust
TO
100%
Higgs unrobust
TO
100%
IJCNN unrobust
TO
100%
Table Comparison between the features where VERITAS finds a better bound than SENSPB. We first run SENSPB and then run VERITAS for the same amount of time. We look at the best results produced by VERITAS this time limit and use that value for the comparison.
16


Reviews:
[{"review_id": "COqiAvFGAD", "reviewer": "Reviewer_joG2", "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.", "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.\n\nIt 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.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 2, "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.\n\nThe problem is well motivated.\n\nThe 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. \n\nMy 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.\n\n**Minor Comments/Typos**\n- Line 068: \"just on\" → \"just one\"\n- 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?”\n- Line 162: \"given set of sensitive features F\" → \"given set of features F\"\n- Caption of Table 1: \"results than mine\" → \"results than our method\"", "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": "", "extra_scores": {}}, {"review_id": "7fFh0hrKpm", "reviewer": "Reviewer_ULi2", "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. \n\nThe main theoretical contributions consist in proving that \n- the (non-quantitative) sensitivity problem is NP-hard (Thm 1)\n- the sensitivity problem restricted to singleton feature sets F={f} is also NP-hard (Thm 2)\n\nThe 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.", "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?\n\nSame question for trees of depth 2 or 3.", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 3, "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.\n\nThe 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 \n\nHere are some minor comments/corrections\n* l69: when THE number\n* l83: whether...whether\n* l104: some OF these\n* l117: of A \\\\(d\\\\)-dimensional\n* l157: When \\\\(F=\\\\{f\\\\}\\\\)\n* l168: two-tree\n* 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\\\\).\n* In the proofs of thm 1 and thm 2, why not simply take \\\\(X_{k+1}=\\\\{-1,1\\\\}\\\\) and \\\\(X_0=\\\\{-1,1\\\\}\\\\)?\n* l275: \\\\(F\\cup\\\\{f\\\\}\\\\) (not \\bigcup and singleton)\n* l289: I don't understand the first sentence here. Which problem requires three variables \\\\(x_1,x_2,x\\\\)?\n* 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.\n* l310: \\log instead of log\n* eq (2): shouldn't \\\\(j+1\\\\) in the RHS simply be \\\\(j\\\\)?\n* l327-328: Incomplete sentence\n* l328: Since THE root\n* 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).\n* l394: mine -> us\n* l420: p-sensitive -> \\\\(p\\\\)-sensitive", "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": "", "extra_scores": {}}, {"review_id": "8qdjyTOVGG", "reviewer": "Reviewer_1wTC", "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.\n\nThe 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.\n\nOverall this is a solid paper, arguably with some weaknesses, that advances the SoA of the area.\n\nPost-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. \nOverall I am still mildly positive on the paper.", "questions": "See questions on the weaknesses above.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 4, "presentation": 3, "contribution": 2, "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).\n\nMost 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\n\nThe 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.", "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": "", "extra_scores": {}}, {"review_id": "syc4YXbk4n", "reviewer": "Reviewer_Mrks", "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.\n\n# Discussion phase\nAfter 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.", "questions": "- **Q1:** Could you ensure consistent notation throughout, especially in proofs? E.g., $x$ and $x'$ vs $x_1$ and $x_2$.\n- **Q2:** Why did you limit the work to GBDTs? Would your framework extend to other ensemble methods, such as random forests?\n- **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).\n- **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.\n- **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?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- **S1:** The paper addresses an important issue aimed at verifying the sensitive features of GBDTs.\n- **S2:** Mathematical proofs, which I would have expected to have a better presentation, but I appreciate the effort.\n- **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.\n- **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 \\\\}$.\n- **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.\n- **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.\n- **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.\n- **W6:** The paper contains grammatical errors, inconsistent abbreviations (e.g., \"wrt\" vs. \"w.r.t.\"), and informal language, which detracts from the overall presentation.", "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": "", "extra_scores": {}}, {"review_id": "92AtuMqoFp", "reviewer": "Reviewer_XnQM", "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.", "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? \n\n(2) Alternatively, can these hardness results for GBTs be extended to random forests?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "**Novelty:**\nArguably, 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:** \nThe 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.\n\nTherefore, 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).\n\nAt 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.\n\n**Significance:**\nThe 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.", "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": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)