arXiv CSopen access

Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approach

2026 · arxiv_cs

arXiv CS · Papers · License: Open Access · 2026

machine learning, deep learning, neural networks

Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approach S. Akshay1 , Chaitanya Garg1 , Ashutosh Gupta1 , Kuldeep S. Meel2 , and Ajinkya Naik1

arXiv:2605.13830v1 [cs.AI] 13 May 2026

Indian Institute of Technology Bombay, India 2 University of Toronto, Canada

Abstract. Decision tree ensembles (DTE) are a popular model for a wide range of AI classification tasks, used in multiple safety critical domains, and hence verifying properties on these models has been an active topic of study over the last decade. One such verification question is the problem of sensitivity, which asks, given a DTE, whether a small change in subset of features can lead to misclassification of the input. In this work, our focus is to build a quantitative notion of sensitivity, tailored to DTEs, by discretizing the input space of the model and enumerating the regions which are susceptible to sensitivity. We propose a novel algorithmic technique that can perform this computation efficiently, within a certified error and confidence bound. Our approach is based on encoding the problem as an algebraic decision diagram (ADD), and further splitting it into subproblems that can be solved efficiently and make the computation compositional and scalable. We evaluate the performance of our technique over benchmarks of varying size in terms of number of trees and depth, comparing it against the performance of model counters over the same problem encoding. Experimental results show that our tool XCount achieves significant speedup over other approaches and can scale well with the increasing sizes of the ensembles. Keywords: Individual fairness · Decision tree ensembles · Algebraic Decision Diagrams · Model counting

Introduction

Artificial Intelligence (AI) models are now ubiquitous in their use in almost all walks of life. While complex models such as transformers, variants of neural networks, and the like, now scale to millions of variables, a major concern has been the difficulty in interpretability and verifiability of such models. At the other end of the spectrum, decision trees are classical models which are known to be interpretable, but are not really scalable. A middle path that has proven to be effective is to train collections of decision trees, called Decision Tree Ensembles (DTEs), that tread the fine line between expressivity and scalability. Since the seminal paper of [12], introduced the XGBOOST training algorithm that has since been used, adapted, analyzed and improved over the last decade in different applications and settings [5]. Today different training algorithms for DTEs

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

including XGBOOST, random forests [35], LGBMs [28] etc are routinely used in many applications [38, 34, 21], especially in the financial sector [31, 9] due to the ease of modeling tabular data using DTEs. Given its many applications, a rich line of work has considered formal verfication of different properties over DTEs [27, 8, 16, 10, 11, 15, 43, 24, 25]. These properties include, evasion, local robustness, sensitivity, fairness, explainability and more. A recent work in [1] considered the problem of sensitivity, which asks if a given DTE is sensitive to a set of features, i.e., does there exist a pair of inputs (called a sensitive pair) such that they differ only on sensitive features (by potentially a small margin), but their outputs are classified differently (with a high confidence). Sensitivity is closely related to individual fairness or causal discrimination [20, 19, 23], since any such sensitive pair is a witness to unfairness, when sensitive features are seen as protected features. This problem is quite different from the well-studied local robustness problem, which asks if a model is robust around a given instance. The main difference is that while local robustness can be solved by searching around the neighborhood of a given input, sensitivity (much like the harder global robustness problem), requires searching across the entire input space (of a dimension that is related to the number of non-sensitive features). In [1], the authors show NP-hardness of the problem and use a pseudo-Boolean encoding showing that their resulting tool could check and produce sensitive pairs for reasonably large DTE benchmarks. In [42], an optimized MILP encoding was proposed for solving this problem, that not only extends to larger and multi-class tree ensembles, but also finds sensitive pairs that are close to the data-distribution. However, a shortcoming in both these works, was that they only check presence of a single sensitive pair, which does not necessarily capture sensitivity of the model. Indeed, what is needed is to quantify the sensitivity of a DTE, ie., to count the number of the sensitive pairs (or estimate the volume of the sensitive region) in a DTE. In fact, it would be even more useful to count the number of input regions for which we witness sensitivity of the model, i.e., existence of sensitive pairs, one inside this region and another outside, as this captures a quantitative measure of sensitivity of the model. This is the problem that we address in this paper. Quantitative verification problems are evidently harder to tackle than plain checking existence or satisfiability. Even for the simple setting of Boolean formulae, this is complexity-theoretically captured by the difference between #P hardness vs NP-hardness, with real difference being seen in tools; SAT-solvers routinely scale to millions of variables, while model counters (that count the number of satisfying assignments) are much more conservative. Most exact model counters, including the state-of-the-art d4 [30] and Ganak [41, 37] work by knowledge compilation, i.e., compiling the formula into a form in which counting is easy. Approximate model counters such as ApproxMC [44, 40] often scale better at the cost of providing PAC-guarantees rather than exact guarantees. Recent work has considered quantitative notions of robustness for neural networks [17, 29], but to the best of our knowledge, we do not know any work that deals with quantitative versions of sensitivity or fairness in decision tree ensembles.

Quantifying Sensitivity for Tree Ensembles

While moving from counting models in Boolean formulae to counting sensitive pairs or regions in DTEs, there are three questions that immediately present themselves. First, what should be the quantitative notion of sensitivity in DTEs? Second, what could be a knowledge representation form for such a quantitative version of sensitivity? Third, can we obtain algorithms at scale at the cost of getting an approximate count with formal guarantees? In this paper, we address these three questions and develop a new compositional algorithm that combines ideas from exact and approximate model counting, knowledge compilation and sensitivity verification tailored for decision tree ensembles. We implement the resulting algorithm and present experimental results to show the effectiveness of our solution. Our contributions are as follows: 1. We exploit the inherent structure of DTEs to formulate a discretized quantitative version of the problem of counting sensitive regions. We can then use Algebraic decision diagrams (ADDs) [3], a quantitative extension of Binary decision diagrams (BDDs) [7] as a natural model to obtain the exact count. However, compiling a DTE to ADD is rather cumbersome and does not lead to efficient algorithms. 2. As our main algorithmic contribution, we develop a novel compositional technique, that subdivides the problem into subproblems for each of which we can obtain the count separately and in parallel. However, these counts may overlap, and the critical difficulty we have to overcome is to obtain a correct total count from overlapping subproblem counts. Our key contribution is to design a splitting and merging strategy that gives an approximate count with strong theoretical soundness guarantees. To do this, we adapt a technique to approximate the volume of the union of sets in the streaming model from database theory [32, 39]. 3. We implement our algorithm and perform experiments on a large suite of 3194 benchmark instances coming from 10 different datasets, with trees ranging from 10 to 100, depth varying from 3 to 6, with at least 8 features. We compare our approach against the ADD-monolithic baseline, the state-ofthe-art tools for exact and approximate model counting. Our experimental results show that outperform the other approaches by an order of magnitude, while maintaining errors within the prescribed margin. 4. We also provide an application and validation of our counting approach and model, by showing that it can be used to check effectiveness of regularization techniques in DTEs. More precisely, we validate that when a given DTE is regularized, the count of sensitivity decreases. Our paper is structured as follows. In Section 2, we start with some preliminaries followed by the problem statement and example in Section 3. Our algorithm is presented in Section 4 and we present our experimental results in Section 5. Finally, we provide a case-study regarding utility of counting sensitivity in DTE which also helps establish validity of our results in Section 6 followed by a brief conclusion in Section 7. Several additional details and further experiments are given in the Appendix.

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

Related Work. For neural networks, the question of global robustness and individual fairness was dealt with recently in [2], where the authors consider Deep Neural Networks (DNNs) and focus on a linear approximation of the softmax, extending a state-of-the-art local robustness neural network verifier to handle global fairness. An approach using an SMT-based approach was developed in [4], where the authors exploit the fact that several neurons in the network remain inactive to prune the network and make it amenable for formal verification. Neither of these approaches consider quantitative notions. In a very recent work [29] the authors quantify the degree of fairness in DNNs by computing the percentages of inputs whose classification outputs can be certified as fair or falsified as unfair. But their method is incomplete as it uses counter-example guided refinement and stops after some number of iterations declaring the remaining inputs as undecided. Sound but incomplete approaches for arbitrary ML models were also considered in [26] for linear and kernelized polynomial models using semi-definite programming for verification. Different from all these works, our approach is deeply embedded in the DTE formalism, uses ADD based compilation and probabilistic reasoning to remain sound and complete with Probably Approximately Correct (PAC) guarantees. As mentioned earlier, for DTEs, the literature has mainly focussed on local robustness verification, with different techniques such as abstract-interpretation [36], dynamic programming based [43] and clique-based approaches [16, 15]. For sensitivity and individual fairness [1] uses a pseudo-Boolean encoding, while [42] uses an MILP encoding.However, none of these approaches consider quantitative notions of sensitivity and hence are rather different from our work. Finally, normal forms including BDDs, ADDs and variants of decomposable Negation normal forms have often been explored for model counting in the literature e.g.,[18, 13]. Recent work for DNF model counting [39] built on ideas of approximating the volume of union of sets from [32] while also using compositionality. Some model counting based ideas were exploited for group fairness verification in [22], but these do not lift to sensitivity.

Preliminaries and Notation

In this section, we establish the notations used throughout the paper. We denote the set of real numbers by R, natural numbers by N and Booleans {0,1} by B. Vectors are represented by bold lowercase letters (e.g., x), while their individual components are indicated by subscripts (e.g., xi ). The set of satisfying assignments of a Boolean formula φ is denoted by Sol(φ), with its cardinality |Sol(φ)|. We consider the standard supervised learning setting where an input vector x is drawn from a feature space D ⊆ Rm and mapped to an output y ∈ R by a learned function h : D → R. Decision Tree Ensembles. Let F = {1, . . . , k} be a set of k feature indices. An input instance is as a vector x = (x1 , . . . , xk ), where each xf corresponds to the value of feature f ∈ F . A Decision Tree Ensemble (DTE) is a predictive model

Quantifying Sensitivity for Tree Ensembles f0 < 4

Leaf: 30

f0 < 3

Leaf: 35

f1 < 3

Leaf: -30

(a) Tree 1

Leaf: -45

f1 < 2

Leaf: 40

Leaf: -40

(b) Tree 2

Fig. 1: Two-tree ensemble represented as decision trees.

composed of a collection of n decision trees, denoted by T = {T1 , . . . , Tn } [6]. Each individual tree Ti : D → R is a rooted binary structure where: – Each internal node u performs a split based on a guard predicate g(x) ≡ (xf ≤ θ), where f ∈ F is the splitting feature and θ ∈ R is a threshold. – Each leaf node l stores a constant prediction value vl ∈ R. Figure 1 illustrates a simple ensemble of two decision trees. Each internal node contains a guard predicate (in this case there are 4 i.e f0 < 3, f0 < 4, f1 < 2, f1 < 3) that directs the traversal based on the input features, while each leaf node provides a constant output value (six leaf nodes with values 30, -30, 35, 40, -40, -45). Decision trees are trained on tabular data and are widely used in various applications, including classification and regression tasks. They are particularly favored for their interpretability and ability to capture complex feature interactions. The output of a single tree, T (x), is determined by traversing the tree from the root to a leaf according to the guard predicates. Usually a single decision tree is not sufficient to achieve high performance on tasks such as regression or classification, hence the need for ensembles in which the output of multiple trees is combined. There are a number of different ways of aggregating the outputs of individual trees. In this work, we focus on additive ensembles, such as Gradient Boosted Trees (GBTs) [28], where the final Pnensemble prediction T (x) is the sum of the individual tree predictions: T (x) = i=1 Ti (x). Without any modification, our analysis method will work for random forest ensembles [6] as well, where the final prediction is obtained by averaging the outputs of individual trees. Model Sensitivity. Beyond predictive accuracy, we are concerned with the changes in model’s decisions based on changes to certain number of feature values of the input. We define our problem through the lens of individual fairness, a principle requiring that a model yields similar outputs for similar individuals [19]. To formalize this, we partition the feature set F into two disjoint subsets: – Sensitive Features (S ⊆ F ), which model protected attributes such as race, gender, or age, and – Non-Sensitive Features (S̄ = F \ S), which include all other attributes, such as income or education level.

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

For instance, in the ensemble shown in Figure 1, if we consider f0 as the sensitive feature and f1 as the non-sensitive feature, then S = {f0 } and S̄ = {f1 }. For an input vector x, we use xS̄ to denote the components of x corresponding to non-sensitive features, and similarly xS for sensitive features. Definition 1 (Sensitivity). An ensemble T is sensitive with respect to a subset S of features F if there is a pair of inputs x, x′ ∈ D, such that Dist(xS̄ , x′S̄ ) = 0 and Dist(x, x′ ) ≤ δ, the following holds: |T (x) − T (x′ )| > ϵ, where ϵ, δ ∈ R are user-defined tolerance thresholds, and Dist is a chosen distance metric. Symbolic Representations: Algebraic Decision Diagrams. Our framework relies on Algebraic Decision Diagrams (ADDs) [3], which generalize Binary Decision Diagrams (BDDs) [7] to represent functions f : {0, 1}n → R. Let X = {x1 , . . . , xn } be a finite set of Boolean variables and let D be a finite set of terminal values, real numbers in our case. An Algebraic Decision Diagram (ADD) over X and D is a rooted directed acyclic graph A = (V, E, r, var, low, high, val), where V is a finite set of nodes, E is a finite set of edges and r ∈ V is the root, each non-terminal node v is labeled by a Boolean variable var(v) ∈ X and has exactly two outgoing edges: a low edge low(v), followed when var(v) = 0, and a high edge high(v), followed when var(v) = 1; each terminal node t is labeled by a value val(t) ∈ D; and along every root-to-terminal path, variables appear according to a fixed variable ordering. The ADD represents a function fA : {0, 1}n → D. For an assignment α ∈ {0, 1}n , the value fA (α) is obtained by starting at the root and recursively following the low edge whenever the current variable evaluates to 0, and the high edge whenever it evaluates to 1, until a terminal node is reached. The label of that terminal node is the value of fA (α). The core advantage of ADDs in our context is the efficient Apply operator, which performs pointwise arithmetic on the symbolic structures. We construct the symbolic representation of the entire ensemble, PM TADD , by summing the ADDs of individual trees (Ti,ADD ) directly: TADD = i=1 Ti,ADD . Notion of Distance. In this work, we will use Hamming distance as the measure of similarity between a pair of inputs. Hamming distance for a pair of vectors of equal length is defined as the of features for which the two of them Pnumber k differ: HammingDist(x, x′ ) = i=1 1[xi ̸= x′i ]. As the inputs to the models are fixed length vectors, choosing Hamming distance as the metric is natural.

Problem Statement

In this section, we develop a quantitative notion of sensitivity that captures how much of the input space is sensitive. Decision tree ensembles, by their design, split the input space of the model into regions such that the output of the model for all points belonging to a region is the same. This natural property of these models can be used to ask questions of a quantitative variety as the input space is discretized into a finite number of regions. This property motivates our approach towards quantifying sensitivity over the discrete space of input regions.

Quantifying Sensitivity for Tree Ensembles

As the model under focus is a decision tree model, we have a set of guard predicates which can be considered essentially as a set of feature-threshold pairs. For a feature f ∈ F , let ordered set Gf be the list of sorted thresholds θ1 , θ2 , . . . , θmf occurring in the guards of the decision nodes of the ensemble involving feature mf f , where mf = |Gf |. Further, for feature f , let Bf be the ordered set (bf,i )i=1 of Boolean variables. Also, let bf,i represent the decision xf < θi . The Boolean variables corresponding to feature f must satisfy the monotonicity constraint: bf,θ1 ⇒ bf,θ2 ⇒ · · · ⇒ bf,θmf . This ensures that Boolean assignments correspond to valid numeric orderings. Let B be the ordered set of all Boolean variables corresponding to all features P in F . Formally, B = (B1 , B2 , . . . , Bk ). Let M = |B| = m f . Thus, any f ∈F M b ∈ B is an M dimensional vector (bf,i )i∈[1,mf ],f ∈F . Let bS , bF/S denote b ↾i∈[1,mf ],f ∈S and b ↾i∈[1,mf ],f ∈F/S respectively, i.e, b projected over a Boolean variables belonging to sensitive and non-sensitive features respectively. Definition 2. We define a mapping function ϕ : Rk ,→ BM that maps a input vector x (consisting of |F | feature values) to an output Boolean vector b (consisting of M Boolean variables) as follows ( 1, if xf < θi , ϕ(x)f,i = 0, otherwise. We also define a valuation map V : BM → R be defined as: V (b) = T (x) for some x such that b = ϕ(x). Note that V is well-defined. From the definition of sensitivity, we want to check if our model is sensitive to a subset of features S i.e perturbation in the input with respect to these features, all else being the same, leads to a significant difference in the model output. To operationalize this, we consider pairs of inputs x and x′ and their corresponding Boolean encodings b = ϕ(x) and b′ = ϕ(x′ ). The following three conditions must be satisfied for x and x′ to witness a sensitivity violation: (1) Equality of non-sensitive features. All Boolean variables of non-sensitive features must be identical between b and b′ : ^ bf,i = b′f,i (C1) i∈[0,mf ],f ∈F \S

(2) Sensitive similarity. The sensitive features must differ as quantified by a Hamming distance threshold d: HammingDist(b, b′ ) ≤ d

(C2)

(3) Prediction-gap condition. A fairness violation occurs when the ensemble’s predictions for x and x′ differ by at least a user-specified margin G: |V (b) − V (b′ )| > G

(C3)

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

Having defined the discretized notion of sensitivity above, we lift it to capture a quantitative version that measures sensitivity in the input space. As each input x is mapped to a Boolean vector b, we have essentially divided the input space into a finite set of regions, each corresponding to a Boolean vector. Input data points which belong to the same region have the same output when evaluated over the model. Hence, a region can be considered as the discrete object over which we can define a notion of quantitative sensitivity. We propose an approach where we want to enumerate all regions for which there exists at least one other region such that this pair satisfies the notion of sensitivity defined as above. Therefore, our goal is to enumerate the number of distinct Boolean vectors b that admit at least one counterpart b′ satisfying all three conditions above. Definition 3. Given a DTE T over a set of input features F , with S ⊆ F , d ∈ N and G ∈ R the counting objective can be defined as : n C(S, d, G) = # b ∈ {0, 1}M

∃ b′ ∈ {0, 1}M :

bf,i = b′f,i

i∈[0,mf ],f ∈F \S

HammingDist(b, b′ ) ≤ d, ^ o |V (b) − V (b′ )| > G .

The quantity C counts the number of Boolean encodings (hence input regions) for which there exists at least one assignment (subject to conditions above) such that there is a significant difference in model output for the two assignments. This quantity serves as a symbolic measure of fairness. Since every Boolean vector b uniquely identifies a discrete region of the input space, we use the terms interchangeably. We can then define a sensitive region as any region b that admits a witness b′ satisfying the constraints established in the counting objective. Thus, our primary objective is to compute the number of sensitive regions. Consider again the two-tree ensemble as presented earlier in Figure 1. This model has two features f0 and f1 . Let f0 be the sensitive feature. There are a total of four guards - f0 < 3, f0 < 4, f1 < 2, f1 < 3. These can be represented by four Boolean variables - bf0 ,3 , bf0 ,4 , bf1 ,2 , bf1 ,3 . As f0 < 3 being true implies f0 < 4, the Boolean variables bf0 ,3 , bf0 ,4 must satisfy the constraint bf0 ,3 ⇒ bf0 ,4 . Likewise for Boolean variables for feature f1 i.e bf1 ,2 ⇒ bf1 ,3 . So, essentially the Boolean assignments that variables (bf0 ,3 , bf0 ,4 ) and (bf1 ,2 , bf1 ,3 ) can take are - {(0,0),(0,1),(1,1)}. Therefore, over the 4 Boolean variables there are a total 3*3 = 9 assignments possible. Any input x to the model maps to one these 9 assignments, and each assignment maps to an output T (x). The objective is to count the number of assignments from the set of all possible assignments (9 in this case) for which there exists another corresponding assignment such that they differ by at most d Boolean variables belonging to sensitive feature, all other Boolean variables being equal, and their outputs differ by a

Quantifying Sensitivity for Tree Ensembles

given gap G . For instance, for this example let’s assume d = 1 and G = 80. In this example, out of 9, there are two assignments (bf0 ,3 = 0, bf0 ,4 = 1, bf1 ,2 = 1, bf1 ,3 = 1) and (bf0 ,3 = 1, bf0 ,4 = 1, bf1 ,2 = 1, bf1 ,3 = 1), which differ in the bit bf0 ,3 , and have outputs -15 and 70 respectively, and hence are witnesses of each other for satisfying the sensitivity condition stated above. Hence C(S = {f0 }, d = 1, G = 80) for this example amounts to 2, out of 9 assignments.

ExactCount(T , S, d, G) 1: Asum ← 0 2: for all Ti ∈ T do 3: Ai ← ToADD(Ti ) 4: Asum ← Asum + Ai 5: A1 ← Asum , A2 ← Asum 6: for all f ∈ S do 7: A2 ← ReplaceBits(A2 , Bits(f )) 8: ∆ ← A2 − A1 9: Φd ← AtMostDistance(Bits(f ), Bits(f ′ ), d) bit differences 10: BG ← ToBDD(∆, G) 11: BG ← BG ∧ Φd 12: C ← |Sol(BG )| 13: return C

▷ BDD constraint allowing at most d ▷ Map each leaf v to 1 iff v > G

ADD based approach for exact count. An ADD based approach for computing the exact count C is outlined in Algorithm ExactCount For the computation of C, we can exploit the tree-like structure of the ensemble. This can be done by encoding the trees of the ensemble as ADDs (in line 2-4 of the Algorithm), so that operations over trees can be efficiently done over a data structure that captures the tree-like properties of our input. Each non-leaf node of the ADD forms an ADD variable/bit, representing the decision node of the tree ensemble. This conversion is achieved through the ToADD function. The complete ensemble can be represented by taking the sum of all ADDs, we refer to the resultant ADD as Asum Post computation of Asum , the monotonicity constraints between bits of each feature must be enforced. Post this computation, two copies of Asum can be created (A1 ,A2 ), followed by replacing ADD variables i.e bits of features f ⊆ S in one of the copies with their corresponding copies (let the copies be represented by the set Bits(f ′ )), referred to in the algorithm by ReplaceBits function (line 7 of the algorithm), taking the difference of the two copies, and applying the constraint that only upto d bits of the f ⊆ S can differ (represented by AtMostDistance, line 9 of the algorithm) . After these operations, the resultant object that we get is a ADD that represents the difference between two outputs of the ensemble when a subset of features is allowed to change by a certain amount. The leaf nodes of this ADD represents all the possible difference values that can be obtained between the two models. Then we convert this ADD to

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

a BDD with the following rule - leaf nodes of ADD having values greater than G take value 1 in the BDD or else 0, with internal nodes remaining the same (referred to as ToBDD function in the algorithm, in line 10 of the algorithm), followed by applying the distance constraints. Counting the satisfying assignments over the resultant BDD achieves our original task of counting the regions.

An Approximate Counting Algorithm

In this section, we describe the primary technical contributions of our work : a procedure XCount that efficiently counts the number of regions in the input space of a given decision tree ensemble that are sensitive with respect to given feature set, bit distance and output threshold. We first give a technical overview of the overall algorithm and then describe each of its components in detail. 4.1

Overview

The input to our algorithm is a decision tree ensemble T = {Ti }ni=1 having n binary trees over a feature space F of k features. The goal is to compute C(S, d, G) i.e enumerate the count of the regions of input space that are sensitive for a given feature set S ⊆ F , given a maximum perturbation of d bits and a difference margin of G. Encoding the trees of the decision tree ensemble as algebraic decision diagrams (ADDs) is central to our approach for computing the count in an efficient way. Subproblem division and approximate counting. We gave an outline of an ADDbased approach in the previous section. The problem with that approach is that as the number of trees in the ensemble increase or the trees of greater depth are present, the computation of sum-ADD overwhelms memory and is much slower to compute. Therefore, we adopt a divide-and-conquer approach - as the change is restricted to the variables of the sensitive features (by a given bit-distance), we break the computation into subproblems, where each subproblem is a pair of bit vectors, with each bit vector being an assignment over variables of sensitive features, and the two differing in d bits. Moreover, as these bits are fixed for each subproblem, certain branches of the ADDs become unreachable, hence the computations can be performed on a pruned version of ADDs. Furthermore, instead of exact counting over each subproblem, we adopt b of the an approximate counting approach where we compute an estimate C exact count C(S, d, G) by taking the count of the union of all solutions over all b we get is within a factor of (1 ± ϵ) subproblems within a (ϵ, δ) guarantee where C of the actual count with at least (1 − δ) confidence. Application of approximate counting. To illustrate how the probabilistic soundness guarantee with (ϵ, δ) values applies in practice, consider a financial institution evaluating a credit scoring model for deployment. A regulator may require that the model exhibit sensitivity on at most, say, 1% of the input space. Our method returns an estimate together with a guarantee: with probability at

Quantifying Sensitivity for Tree Ensembles

least 1 − δ, the estimate is within a factor of (1 ± ε) of the true value. Thus, the institution can conclude, with high confidence, that the model satisfies the 1% sensitivity threshold without performing exact, and potentially intractable, counting. Conversely, if the estimate exceeds the threshold even within the error margin, the model can be safely rejected. More generally, since ε and δ are user-controlled hyperparameters, practitioners can tune the strength of the guarantee depending on available computational resources and the application—for instance, using stricter confidence levels for regulatory compliance and more relaxed ones during model development. 4.2

Description of the algorithm

In Algorithm 1 we lay out the main framework XCount along with the procedures used by it. Each decision node of the tree is of the form (xf < θ). These nodes form a set of predicates over which we can define a set of boolean variables. We also maintain the count of guards for each feature, denoted by mf . Out of these, the variables belonging to the sensitive feature set S is the one over which we want to check if changing d bits from them leads to a swing in the output of the ensemble by G. These bits are subject to monotonicity constraints, hence if there n number of bits of a particular feature, then there are (n + 1) boolean evaluations possible. A set of these evaluations, referred to as bit-masks (mask in the algorithm), in the form of bit-vectors is computed in advance by BitMaskGen (Algorithm 3) and stored in BitMasks. If more than one feature given as sensitive, then we take a cross-product of the bit-masks of all such features - by taking all permutations of bit-masks over all features and appending them, and storing all such bit-masks as a global set. These operations are carried out in line 1-4 of Algorithm 1. Breaking-up the problem. In line 5-10 of Algorithm 1, we break the original problem into subproblems. A pair of bitmasks from the set BitMasks, which lie within a Hamming distance of d are the pair of assignments of interest to the sensitivity problem. Hence any such tuple forms a subproblem, and all such tuples form the set Probs. Each subproblem is processed by the function ProcessSubproblem. The function PruneTree uses the bit-mask input to prune the branches of the trees of the ensemble which are rendered unreachable due to fixing the nodes according to the values of bit-mask. Procedure EncodeADD encodes each tree as an ADD, by coverting each tree node into an ADD node and each leaf value to terminal node (leaf) of the ADD . We take a pair-wise difference of each tree in the ensemble to get DiffADDs that encodes the difference and add all such ADDs to get DiffSum ADD, which encodes the sum of all differences, essentially encoding the difference between the output of the two ensembles. This holds true as the difference between two sums over the ADDs is equal to the sum of the pair-wise differences between the corressponding ADDs of the two ensembles. The procedure ToBDD (Algorithm 6) converts this ADD to a BDD by keeping the internal nodes same and values of the leaves into boolean values based on whether they exceed G. This resultant BDD, labeled as φ, is the

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

Algorithm 1 XCount(T , S, d, G, ϵ, δ) 1: n ← |T |, k ← |F |, BitMasks ← ∅, Probs ← ∅ 2: for f ∈ S do 3: BitMasks ← (f, BitMaskGen(mf )) Q 4: GlobalMaskSet ← f ∈S BitMasks(f ) 5: for mask1 , mask2 ∈ GlobalMaskSet do 6: if HammingDist(mask1 , mask2 ) ≤ d then 7: Probs ← (mask1 , mask2) 8: X ← ∅, p ← 1, Thresh ← max 12 · ln(24/δ) , 6 ln 6δ + ln |Probs| ϵ2 9: for pair ∈ Probs do 10: φ ← ProcessSubproblem(T , pair, G) 11: t ← |Sol(φ)| 12: for b ∈ X do 13: if bF/S |= φ then 14: if bS = pair.mask1 ∨ bS = pair.mask2 then 15: remove b from X 16: Nk ← Poisson(t.p) 17: while Nk + |X| ≥ Thresh do 18: Remove each assignment from X with 0.5 probability 19: p ← p/2 20: Nk ← Binomial(Nk , 0.5) 21: Samples ← SampleBDD(φ, Nk , pair) 22: X.Append(Samples) b ← |X|/p 23: return C

object over which the approximate satisfying assignments are computed. Exact implementation of the functions above are provided in Appendix B. Merging the subproblems. In line 11-24 of Algorithm 1, computes the union of set of satisfying assignments over all subproblems, each being a BDD, with a (ϵ, δ) guarantee. The threshold parameter Thresh is pre-computed as: 12 ln(24/δ) Thresh = max , 6 ln(6/δ) + ln |Probs| ε2 The set of satisfying assignments is initially empty before we start iterating through the subproblems. Each assignment is over M bits which together form a bit-vector b ∈ BM . The constituent bits bf,i of b can be divided into two disjoint sets bS and bF/S , as defined in Section 3. The φ we get is formed over nodes belonging to non-sensitive features, as we had fixed the nodes belonging to sensitive features when it was formed. So essentially a satisfying assignment of the BDD paired with either of the bits pair.mask1 or pair.mask2 forms the complete satisfying assignment. At the start of processing each subproblem, we first remove assignments from X that satisfy the current BDD and whose values over bits of sensitive features also match either of the current bit-mask pair. Then we compute the number of solutions Nk that is to be sampled from from

Quantifying Sensitivity for Tree Ensembles

Algorithm 2 ProcessSubproblem(T , p, G) 1: T ′ ← ∅,T ′′ ← ∅ 2: for i = 1 to |T | do 3: T ′ .Append(PruneTree(Ti .root, p.mask1 )) 4: T ′′ .Append(PruneTree(Ti .root, p.mask2 )) 5: DiffSum ← 0 6: for i = 1 to |T | do ′′ ′ 7: DiffADD ← EncodeADD(Ti .root) − EncodeADD(Ti .root) 8: DiffSum ← DiffSum + DiffADD 9: φ ← ToBDD(DiffSum, G) 10: return φ

the φ, whose distribution is simulated by Poisson distribution. At any point of time, we want to store Thresh number of solutions in X, if Nk +|X| is larger than Thresh, then p is halved and Nk is adjusted by samping from Binomial(Nk ,0.5) and removing each solution from X with 0.5 probability. After adjusting, we have to sample Nk solutions of φ uniformly at random. This is done by the sub-routine SampleBDD (Algorithm 7) which samples assignments from a given BDD in two steps, as follows. For each node u in the BDD, we compute p(u) the probability that sub-BDD rooted at u evaluates to 1 under a uniform random assignment of variables. For terminal nodes, p(0) = 0 and p(1) = 1. For non-terminal nodes with children else ) uthen and uelse , we have p(u) = p(uthen )+p(u . To draw a sample, we start at 2 the root of the BDD and repeatedly choose the next edge (then or else) using the probabilities above. This determines truth assignments for all variables encountered along the path. Variables that do not appear on the path are assigned uniformly at random. The result is a full assignment x. Each assignment is paired with a bitmask choice and inserted into a X. If p denotes the effective sampling b = |X| . probability, we obtain the final estimate as C p A full running example of our algorithm is presented in Appendix E. 4.3

Theoretical Guarantees

We now establish the correctness of XCount, formalized as follows: h i b ≤ (1 + ϵ)C(S, d, G) ≥ 1 − δ, where C b Theorem 1. Pr (1 − ϵ)C(S, d, G) ≤ C is the output of XCount. Proof. We adapt the proof technique from [39] and provide the main derivation below, with more details in Appendix A. Let m = |Probs| be the number of subproblems. For each i ∈ [m], let Ui ⊆ {0, 1}F denote the set of assignments Si from the i-th subproblem, and define Si = t=1 Ut so that |Sm | = C(S, d, G). (i) For j ≥ 0, let pj = 2−j and let Xj denote the random multiset after processing i subproblems with sampling probability pj . Since the algorithm draws

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

Nt ∼ Poisson(|Ut |pj ) samples from each Ut , each element s ∈ Si appears inde(i) pendently with Poisson(pj ) multiplicity, giving |Xj | ∼ Poisson(|Si |pj ). (i)

Let Ej

denote the event that the algorithm has sampling probability pj (i)

(i)

after i subproblems, and define Aj = {|Xj | ̸∈ [|Si |pj (1 − ϵ), |Si |pj (1 + ϵ)]}. Let b = |X (m) |/pj on event j ⋆ be the smallest j with pj < Thresh/(4|Sm |). Since C j

(m)

, we have

b ̸∈ [(1 − ϵ)C(S, d, G), (1 + ϵ)C(S, d, G)]] ≤ Pr[C

⋆ jX −1

j=0

 (m)

Pr[Aj

] + Pr

 [

(m) 

j≥j ⋆

(m)

For j < j ⋆ , we have |Xj | ∼ Poisson(λj ) with λj = |Sm |pj ≥ Thresh/4. By standard Poisson concentration, Pr[|X − λ| ≥ ϵλ] ≤ 2 exp(−ϵ2 λ/3) for Pj ⋆ −1 (m) (m) X ∼ Poisson(λ). Thus Pr[Aj ] ≤ 2 exp(−ϵ2 Thresh/12), and j=0 Pr[Aj ] ≤ 2j ⋆ exp(−ϵ2 Thresh/12) ≤ δ/6 by our choice of Thresh. S (m) (i) The event j≥j ⋆ Ej occurs only if |Xj ⋆ −1 | ≥ Thresh for some i ∈ [m]. (i)

(i)

Since |Xj ⋆ −1 | ∼ Poisson(|Si |pj ⋆ −1 ) ≤ Poisson(Thresh/2), we have Pr[|Xj ⋆ −1 | ≥ S (m) Thresh] ≤ exp(−Thresh/6) ≤ δ/(6m). By union bound, Pr[ j≥j ⋆ Ej ] ≤ δ/6. b ̸∈ [(1 − Substituting both bounds into the decomposition above yields Pr[C ϵ)C(S, d, G), (1 + ϵ)C(S, d, G)]] ≤ δ/6 + δ/6 < δ, which establishes the theorem. ⊔ ⊓

Experiments

We now evaluate the performance and accuracy of our proposed method, XCount, on a set of decision tree ensemble models trained on tabular datasets. Implementation details. We implemented our tool XCount in C++, using the CUDD package for the implementation of ADDs and BDDs. The tool takes following command inputs - a decision tree ensemble in the form of a JSON file, the input feature(s) of the ensemble to test for sensitivity (S), the precision that is required of the leaf values of the ensemble, the gap threshold (G), the bit distance allowed between sensitive features (d), the confidence parameter (δ) b within and error parameter (ϵ). The output of the tool is the count estimate C, a factor of (1 ± ϵ) with a confidence of (1-δ) of the actual count C(S, d, G) as outlined in section 4. Benchmarks We evaluated our approach on ten standard tabular datasets: Diabetes, Adult, Covtype, Protein-structure, Mnist, Webspam, Wine-quality, Supersymmetry, Higgs, and Fashion-MNIST. To construct a comprehensive benchmark suite, we trained multiple distinct ensemble models for each dataset. We varied the ensemble size from 10 to 100 in increments of 10 (10 sizes), and tree depths from 3 to 6 (4 depths). For each configuration of (Dataset × Ensemble

Quantifying Sensitivity for Tree Ensembles

Size × Depth), we generated multiple instances by sweeping over different feature thresholds and decision points naturally arising from the data. For each model generated, we randomly chose a set of 8 features present in to model as the features to be tested for sensitivity analysis. This leads to total benchmark instances of 10*4*8 = 320 for each dataset (there are 316, 319, 319 instances for Adult, Supersymmetry and Protein structure, respectively, as smaller ensemble models of these datasets have features less than 8, in such case we have picked all features present in the model without any randomization). Table 1 summarizes the characteristics of these datasets, along with the min and max number of guards for each datatset, as this captures both depth and number of trees. Dataset Benchmark Instances Guards (Min) Guards (Max) Diabetes 320 41 1176 Adult 316 18 712 Covtype 320 36 1301 Mnist 320 58 4597 Webspam 320 36 1156 Wine-quality 320 41 998 Supersymmetry 319 67 2561 Higgs 320 70 2559 Fashion-MNIST 320 51 2513 Protein structure 319 49 1696

Table 1: Benchmark instances for each dataset

All experiments were conducted on a high-performance server equipped with an AMD EPYC 7742 64-Core Processor and 629GiB of RAM, running Ubuntu 22.04.5 LTS. To ensure fair comparison and resource isolation, we enforced a 4GB memory limit per instance and a strict timeout of 1800 seconds. Comparisons baselines. To establish a comparative baseline for quantitative verification of decision tree ensembles, we developed a module that encodes the verification problem into Conjunctive Normal Form (CNF). This encoding enables us to leverage standard, state of the art model counting engines–specifically Ganak and ApproxMC to solve the generated instances. We also compare the performance against an ADD-baseline. Thus we compare against: – CNF + Ganak : We encode the verification problem into CNF and use Ganak, a projected model counter, to obtain exact counts. – CNF + ApproxMC : Using the same CNF encoding, we employ ApproxMC to obtain approximate counts with (ϵ, δ)-guarantees. – ADD-baseline: A naive exact counting approach where the full ensemble is encoded into a single monolithic Algebraic Decision Diagram (ADD). For consistency, we utilized a gap threshold of 2, bit-distance of 1, ϵ to 0.1, δ to 0.1, and set the leaf value precision to 3 decimal places across all experiments. However, for the datasets Higgs and Supersymmetry we used a gap threshold of

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik Tool Solved PAR2 ADD-baseline 153 3428.461 ApproxMC 579 3005.374 Ganak 721 2901.421 XCount 1552 1937.474

Fig. 2: Cactus plots comparing execution time across all benchmarks.

Table 2: Aggregate statistics for each configuration. PAR2 is the Penalized Average Runtime - if instance is solved then its runtime is counted, and if it times out then twice the timeout (2*1800=3600 s) value is used.

0.05, due to the leaf values of these two datasets being much smaller to record difference of more than 2, leading to no possible solutions in case a gap threshold of 2 is selected. The value of a meaningful gap threshold to be given as input to the model is closely related to the scale of values in the leaves, as it captures the absolute difference between the output of the ensemble (i.e the sum of leaves) for two different inputs. Therefore, for any meaningful analysis of sensitivity, the gap threshold given must be proportionate to leaf values of the model. Experimental evaluation of varying gap thresholds over the performance of XCount can be found in section C of the appendix. Our results. We present our results in four parts: (i) we discuss the results of our performance in comparison to the baseline; (ii) we check the accuracy of our approximate count; (iii) we demonstrate scalability of the tool varying size of the ensemble, and (iv) we highlight the impact of different optimizations in our tool through ablation studies. Performance results. We conducted a detailed experimental evaluation to compare XCount against Ganak and ApproxMC. Table 2 gives the overall statistics regarding the completed number of runs by each tool and the corresponding PAR-2 scores. Figure 2 presents the cactus plots for the ten datasets, visualizing the number of benchmark instances solved (x-axis) within a given time limit (y-axis). The plots for each datasets can be referred to in Appendix C. As shown in Figure 2, XCount demonstrates significantly higher instance completion rates compared to the generic CNF-based pipelines. For smaller instances, ADD-baseline is faster compared to CNF + Ganak/ApproxMC pipelines but scales poorly with respect to size of the ensemble, whereas the latter is able to scale. However, XCount performs better than both of these, both in terms of timing and scalability. In summary, out of 3194 benchmark instances, XCount is able to handle 1552, about 1.15 times more than the next best approach, as well as clocking a PAR-2 score of 1937.474, an improvement of 33% over the next best approach and 43% improvement over the ADD baseline approach.

Quantifying Sensitivity for Tree Ensembles

Accuracy wrt approximation guarantees. We quantified the deviation of our approximate counts against the exact counts provided by the CNF + Ganak pipeline (for instances where Ganak did not time out). Figure 3 depicts the relative error distribution. The majority of solved instances exhibit negligible error, confirming that XCount maintains high fidelity to the exact count while offering improved scalability.

Fig. 3: Relative error of XCount compared to exact counts across all benchmarks.

Scalability. We evaluate the scalability of the tool with increasing size of the ensemble. Figure 4a depicts a heat map of experiments over all datasets to illustrate a relation between the number of trees of the ensemble and the max depth of the trees of the ensemble. The higher shades indicated the greater time taken by the instances that fall in that category. A better metric is to enumerate the total number of guards present in the ensemble. In Figure 4b, we depict a plot the ratio of completed instances to total number of instances for each range of guard values. The plot shows that as the number of guards increase, the performance of XCount goes down, with less than 50% of the instances getting completed when guards are more than 400. Ablation Studies. Finally, we discuss the impact of the various optimizations embedded in our tool. The first is encoding the problem as an ADD (Opt-1). Second, when we break the problem into subproblems, and take the union of satisfying assignments over them, one design based optimization is to take pairwise difference of individual ADDs and then add them, instead of adding them first and then taking difference (Opt-2). Finally, merging the satisfying solutions of subproblems by taking a probabilistic approach (pepin) instead of exact count, to obtain the final count estimate (Opt-3). To illustrate the relative impact of each of these optimizations we conduct a comprehensive set of experiments across four configurations: (i) Encoding the problem as a single monolithic ADD without any of the other optimizations (Opt-1 or ADD-baseline). (ii) Adding all optimizations except Opt-2 i.e first adding ADDs then taking pairwise difference (Opt 1+3). (iii) Adding all optimizations except Opt-3 i.e doing exact counting instead of probabilistic counting (Opt 1+2). (iv) Adding all other optimizations except Opt-1 i.e breaking the problem into subproblems and passing the CNF

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

(a) Heat map of trees, depth vs time across all benchmarks

(b) Completion ratio vs guard ranges

Fig. 4: Scalability analysis of XCount wrt ensemble size across all benchmarks.

Tool Opt 1 (ADD-baseline) Opt 1+3 Opt 1+2 Subp + CNF XCount

Fig. 5: Cactus plots for ablation experiments on Adult dataset

Solved

PAR2

68 197 289 33 345

3122.31 2275.374 1635.355 3408.22 1304.486

Table 3: Aggregate statistics for each configuration. For configuration Subp + Cnf, only subproblems are solved without merging the solutions of subproblems.

encoding of subproblems to Ganak (Subp + CNF). Note that for this configuration only the total time for solving individual subproblems is summed up, without calculating the final count as its performance was already worse than other configurations. We compare the performance of these four with performance of XCount. For this set of experiments we train models on the Adult dataset by varying the number of trees from 10 to 100 with a step size of 10 trees, and varying the depth from 3 to 6, leading to 10*4 = 40 tree models. For each of these models, we run the tool taking over all the features that are present in the model, leading to a total of 509 instances (Adult has 14 features, but the number of instances is slightly less than 14*40 = 560 as not all features appear in the trained models if the models are small i.e having less number of trees). Figure 5 and Table 3 summarize the results for the experiments on configurations listed above. We see that solving the problem becomes faster when encoded as an ADD, but this does

Quantifying Sensitivity for Tree Ensembles

not scale to larger ensembles. Each of the other optimizations lead to benefits with the best performance coming from adding all of them. In summary, XCount outperforms the other baseline approaches by a significant margin especially as sizes of ensembles increases, while the accuracy of the count remains well within the bounds of the theoretical guarantees (for ϵ = 0.1, δ = 0.1) with 99% of counts being within 10% error. We also analyzed scalability with increasing size of the ensembles and role played by each optimization, collectively highlighting the efficacy of our approach.

Application of XCount to regularization validation

In this section, we present a case-study to illustrate a potential application of counting sensitivity, by relating it to the level of L1 regularization used during training of the models. A tree ensemble model, such as Gradient Boosted Tree or Random Forest, is trained by splitting a node at a time and prone to overfitting if not properly regularized. L1 regularization, uses a penalty term in the loss function, which encourages fewer splits in the tree. If a node is deeper in a tree the penalty is larger, proportional to the regularization parameter α [33] (see Appendix D.1 for more details). Our hypothesis is that smaller α leads to overfitting and increased sensitivity, while larger α promotes generalization and fewer sensitive regions. By quantifying the number of sensitive regions, we can gain insights into the training process of the model, if we do not have access to the model’s internal parameters, and assess its potential overfitting. We used Adult dataset for this study. We trained several models with varying levels of regularization and compare the number of sensitive regions in each model. We repeat this process by varying the other configurations such as depth of trees and number of trees in the ensemble. We consider models of depth 3 and 4, with number of trees as 20, 30 and 40. For each configuration, we trained models with L1 regularization parameters of 0, 1, 5 and 10. Table 4 in Appendix shows Fig. 6: Relative sensitivity Cα /C0 for that our choice of hyperparameters en- regularized models (α ∈ {1, 5, 10}) sures that increasing the L1 regulariza- against the unregularized baseline. The tion parameter α had a negligible impact yellow line marks the median; boxes and on predictive performance. This stability whiskers show the IQR and 1.5× IQR allows us to compare the models’ sensi- range. tivity under the assumption that they are functionally equivalent in terms of standard performance metrics. We selected thirteen sensitive features from the dataset: age, workclass, fnlwgt, education, education-num, marital-status, occupation, relationship, race, sex, capital-gain, capital-loss, hours-per-week for our sensitivity analysis. In to-

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

tal, we have 78 configurations (2 depths × 3 number of trees × 13 sensitive features) for our study. For each configuration and sensitive feature, we computed the number of sensitive regions using XCount, for each of the regularization parameters. To ensure that the discretization of the input space was consistent across four models, we included the guard predicates from all the models during the execution of XCount. We excluded instances where the baseline model yielded zero sensitive regions and the sensitive feature is missing in the models. We used gap 0.5 for our study. Let C0 be the count of sensitive regions for the model with no regularization (α = 0). We define the relative sensitivity for a model with regularization parameter α as: Cα /C0 , where Cα is the count of sensitive regions for the model with regularization parameter α. In Figure 6, we present the results of our study. The box plots show the distribution of relative sensitivity counts across all configurations for each regularization parameter. We observe a clear trend where increasing the regularization parameter leads to a decrease in the number of sensitive regions, confirming our hypothesis that counting sensitive regions provides a useful metric to validate the impact of regularization on model behavior.

Conclusion

In this work, we built a quantitative notion of sensitivity over decision tree ensembles and presented XCount, a novel algorithmic technique that can quantify sensitivity over DTEs. The challenges of scale are handled by using a novel compositional and probabilistic approach that provides concrete guarantees. Experimental evaluation over an extensive set of benchmarks show the effectiveness of our method over the baseline and other model counting based approaches. As future work, we would like use our sensitivity counts to rank DTE models. While our work focused on XGBoost models, our approach and technique work immediately for any decision tree ensemble model. We would like hence to apply this to wider classes of benchmarks, and find other applications for which counting sensitivity could be useful.

Acknowledgements We acknowledge the State Bank of India (SBI) Foundation Hub for Data Science & Analytics , IIT Bombay for supporting the work done in this project. We thank Shri Shakeel Ahmed Agasimani, Deputy General Manager, Analytics Department, C Ramesh Chander, Assistant General Manager (Statistician), Muthukumaran M S, Chief Manager (Data Scientist), Komaragiri Srinivas Jagannath, Manager (Data Scientist), Neha Maheswari, Manager (Data Scientist), State Bank of India, for multiple wide-ranging discussions and feedback.

Quantifying Sensitivity for Tree Ensembles

References 1. Ahmad, A., Tayal, T.V., Gupta, A., Akshay, S.: Sensitivity verification for additive decision tree ensembles. In: The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net (2025), https://openreview.net/forum?id=h0vC0fm1q7 2. Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Nickovic, D., Weissenbacher, G.: Verifying global two-safety properties in neural networks with confidence. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 2427, 2024, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14682, pp. 329–351. Springer (2024). https://doi.org/10.1007/978-3-031-65630-9\_17, https://doi.org/10.1007/978-3-031-65630-9_17 3. Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Formal methods in system design 10(2), 171–206 (1997) 4. Biswas, S., Rajan, H.: Fairify: Fairness verification of neural networks. In: 45th IEEE/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023. pp. 1546–1558. IEEE (2023). https://doi.org/10.1109/ICSE48619.2023.00134, https://doi.org/10.1109/ICSE48619.2023.00134 5. Blockeel, H., Devos, L., Frénay, B., Nanfack, G., Nijssen, S.: Decision trees: from efficient prediction to responsible ai. Frontiers in Artificial Intelligence 6 (2023). https://doi.org/10.3389/frai.2023.1124553, https://www.frontiersin.org/journals/artificial-intelligence/articles/10.3389/frai.2023.1124553 6. Breiman, L.: Random forests. Machine learning 45(1), 5–32 (2001) 7. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 100(8), 677–691 (1986) 8. Calzavara, S., Cazzaro, L., Lucchese, C., Marcuzzi, F.: Explainable global fairness verification of tree-based classifiers. 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML) pp. 1–17 (2022), https://api.semanticscholar.org/CorpusID:252545325 9. Chang, Y.C., Chang, K.H., Wu, G.J.: Application of extreme gradient boosting trees in the construction of credit risk assessment models for financial institutions. Applied Soft Computing 73, 914– 920 (2018). https://doi.org/https://doi.org/10.1016/j.asoc.2018.09.029, https://www.sciencedirect.com/science/article/pii/S1568494618305465 10. Chen, H., Zhang, H., Boning, D., Hsieh, C.J.: Robust decision trees against adversarial examples. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol. 97, pp. 1122–1131. PMLR (09–15 Jun 2019), https://proceedings.mlr.press/v97/chen19m.html 11. Chen, H., Zhang, H., Si, S., Li, Y., Boning, D.S., Hsieh, C.: Robustness verification of tree-based models. In: Wallach, H.M., Larochelle, H., Beygelzimer, A., d’Alché-Buc, F., Fox, E.B., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada. pp. 12317–12328 (2019), https://proceedings.neurips.cc/paper/2019/hash/cd9508fdaa5c1390e9cc329001cf1459Abstract.html

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

12. Chen, T., Guestrin, C.: XGBoost: A scalable tree boosting system. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. pp. 785–794. KDD ’16, ACM, New York, NY, USA (2016). https://doi.org/10.1145/2939672.2939785, http://doi.acm.org/10.1145/2939672.2939785 13. de Colnet, A., Szeider, S., Zhang, T.: Compilation and fast model counting beyond CNF. In: Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024. pp. 3315–3323. ijcai.org (2024), https://www.ijcai.org/proceedings/2024/367 14. Developers, X.: Xgboost documentation. https://xgboost.readthedocs.io, accessed: 2026 15. Devos, L., Cascioli, L., Davis, J.: Robustness verification of multi-class tree ensembles. Proceedings of the AAAI Conference on Artificial Intelligence 38(19), 21019–21028 (Mar 2024). https://doi.org/10.1609/aaai.v38i19.30093, https://ojs.aaai.org/index.php/AAAI/article/view/30093 16. Devos, L., Meert, W., Davis, J.: Versatile verification of tree ensembles. In: Meila, M., Zhang, T. (eds.) Proceedings of the 38th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol. 139, pp. 2654–2664. PMLR (18–24 Jul 2021), https://proceedings.mlr.press/v139/devos21a.html 17. Downing, M., Eiers, W., DeLong, E., Lodha, A., Burns, B.O., Kadron, I.B., Bultan, T.: Quantitative symbolic robustness verification for quantized neural networks. In: Ogata, K., Méry, D., Sun, M., Liu, S. (eds.) Formal Methods and Software Engineering - 25th International Conference on Formal Engineering Methods, ICFEM 2024, Hiroshima, Japan, December 2-6, 2024, Proceedings. Lecture Notes in Computer Science, vol. 15394, pp. 125–145. Springer (2024). https://doi.org/10.1007/978-981-96-0617-7\_8, https://doi.org/10.1007/978-98196-0617-7_8 18. Dudek, J.M., Phan, V., Vardi, M.Y.: ADDMC: weighted model counting with algebraic decision diagrams. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020. pp. 1468–1476. AAAI Press (2020). https://doi.org/10.1609/AAAI.V34I02.5505, https://doi.org/10.1609/aaai.v34i02.5505 19. Dwork, C., Hardt, M., Pitassi, T., Reingold, O., Zemel, R.: Fairness through awareness. In: Proceedings of the 3rd innovations in theoretical computer science conference. pp. 214–226 (2012) 20. Galhotra, S., Brun, Y., Meliou, A.: Fairness testing: testing software for discrimination. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering. p. 498–510. ESEC/FSE 2017, Association for Computing Machinery, New York, NY, USA (2017). https://doi.org/10.1145/3106237.3106277, https://doi.org/10.1145/3106237.3106277 21. Ghiasi, M.M., Zendehboudi, S.: Application of decision treebased ensemble learning in the classification of breast cancer. Computers in Biology and Medicine 128, 104089 (2021). https://doi.org/https://doi.org/10.1016/j.compbiomed.2020.104089, https://www.sciencedirect.com/science/article/pii/S0010482520304200 22. Ghosh, B., Basu, D., Meel, K.S.: Algorithmic fairness verification with graphical models. In: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI

Quantifying Sensitivity for Tree Ensembles

2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022. pp. 9539–9548. AAAI Press (2022). https://doi.org/10.1609/AAAI.V36I9.21187, https://doi.org/10.1609/aaai.v36i9.21187 23. Gupta, A., Henzinger, T.A., Kueffner, K., Mallik, K., Pape, D.: Monitoring robustness and individual fairness. In: Antonie, L., Pei, J., Yu, X., Chierichetti, F., Lauw, H.W., Sun, Y., Parthasarathy, S. (eds.) Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining, V.2, KDD 2025, Toronto ON, Canada, August 37, 2025. pp. 790–801. ACM (2025). https://doi.org/10.1145/3711896.3737054, https://doi.org/10.1145/3711896.3737054 24. Ignatiev, A., Izza, Y., Stuckey, P.J., Marques-Silva, J.: Using maxsat for efficient explanations of tree ensembles. In: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022. pp. 3776–3785. AAAI Press (2022). https://doi.org/10.1609/AAAI.V36I4.20292, https://doi.org/10.1609/aaai.v36i4.20292 25. Izza, Y., Ignatiev, A., Rubin, S., Marques-Silva, J., Stuckey, P.J.: Most general explanations of tree ensembles. In: Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2025, Montreal, Canada, August 16-22, 2025. pp. 5463–5471. ijcai.org (2025). https://doi.org/10.24963/IJCAI.2025/608, https://doi.org/10.24963/ijcai.2025/608 26. John, P.G., Vijaykeerthy, D., Saha, D.: Verifying individual fairness in machine learning models. In: Adams, R.P., Gogate, V. (eds.) Proceedings of the ThirtySixth Conference on Uncertainty in Artificial Intelligence, UAI 2020, virtual online, August 3-6, 2020. Proceedings of Machine Learning Research, vol. 124, pp. 749– 758. AUAI Press (2020), http://proceedings.mlr.press/v124/george-john20a.html 27. Kantchelian, A., Tygar, J.D., Joseph, A.D.: Evasion and hardening of tree ensemble classifiers. In: Balcan, M., Weinberger, K.Q. (eds.) Proceedings of the 33nd International Conference on Machine Learning, ICML 2016, New York City, NY, USA, June 19-24, 2016. JMLR Workshop and Conference Proceedings, vol. 48, pp. 2387– 2396. JMLR.org (2016), http://proceedings.mlr.press/v48/kantchelian16.html 28. Ke, G., Meng, Q., Finley, T., Wang, T., Chen, W., Ma, W., Ye, Q., Liu, T.Y.: Lightgbm: A highly efficient gradient boosting decision tree. Advances in neural information processing systems 30, 3146–3154 (2017) 29. Kim, B.H., Wang, J., Wang, C.: Fairquant: Certifying and quantifying fairness of deep neural networks. In: 47th IEEE/ACM International Conference on Software Engineering, ICSE 2025, Ottawa, ON, Canada, April 26 - May 6, 2025. pp. 527–539. IEEE (2025). https://doi.org/10.1109/ICSE55347.2025.00016, https://doi.org/10.1109/ICSE55347.2025.00016 30. Lagniez, J., Marquis, P., Biere, A.: Dynamic blocked clause elimination for projected model counting. In: Chakraborty, S., Jiang, J.R. (eds.) 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, Pune, India, August 21-24, 2024. LIPIcs, vol. 305, pp. 21:1–21:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2024). https://doi.org/10.4230/LIPICS.SAT.2024.21, https://doi.org/10.4230/LIPIcs.SAT.2024.21

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

31. Madaan, M., Kumar, A., Keshri, C., Jain, R., Nagrath, P.: Loan default prediction using decision trees and random forest: A comparative study. IOP Conference Series: Materials Science and Engineering 1022(1), 012042 (jan 2021). https://doi.org/10.1088/1757-899X/1022/1/012042, https://dx.doi.org/10.1088/1757-899X/1022/1/012042 32. Meel, K.S., Vinodchandran, N.V., Chakraborty, S.: Estimating the size of union of sets in streaming models. In: Libkin, L., Pichler, R., Guagliardo, P. (eds.) PODS’21: Proceedings of the 40th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, Virtual Event, China, June 2025, 2021. pp. 126–137. ACM (2021). https://doi.org/10.1145/3452021.3458333, https://doi.org/10.1145/3452021.3458333 33. Ng, A.Y.: Feature selection, l1 vs. l2 regularization, and rotational invariance. In: Proceedings of the Twenty-First International Conference on Machine Learning. p. 78. ICML ’04, Association for Computing Machinery, New York, NY, USA (2004). https://doi.org/10.1145/1015330.1015435, https://doi.org/10.1145/1015330.1015435 34. Niazkar, M., Menapace, A., Brentan, B., Piraei, R., Jimenez, D., Dhawan, P., Righetti, M.: Applications of xgboost in water resources engineering: A systematic literature review (dec 2018–may 2023). Environmental Modelling and Software 174, 105971 (2024). https://doi.org/https://doi.org/10.1016/j.envsoft.2024.105971, https://www.sciencedirect.com/science/article/pii/S136481522400032X 35. Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., et al.: Scikit-learn: Machine learning in python. Journal of machine learning research 12(Oct), 2825–2830 (2011) 36. Ranzato, F., Zanella, M.: Abstract interpretation of decision tree ensemble classifiers. Proceedings of the AAAI Conference on Artificial Intelligence 34(04), 5478–5486 (Apr 2020). https://doi.org/10.1609/aaai.v34i04.5998, https://ojs.aaai.org/index.php/AAAI/article/view/5998 37. Sharma, S., Roy, S., Soos, M., Meel, K.S.: Ganak: A scalable probabilistic exact model counter. In: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI) (2019) 38. Shrestha, S.M., Shakya, A.: A customer churn prediction model using xgboost for the telecommunication industry in nepal. Procedia Computer Science 215, 652–661 (2022). https://doi.org/https://doi.org/10.1016/j.procs.2022.12.067, https://www.sciencedirect.com/science/article/pii/S187705092202138X, 4th International Conference on Innovative Data Communication Technology and Application 39. Soos, M., Aggarwal, D., Chakraborty, S., Meel, K.S., Obremski, M.: Engineering an efficient approximate dnf-counter. In: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China. pp. 2031–2038. ijcai.org (2023). https://doi.org/10.24963/IJCAI.2023/226, https://doi.org/10.24963/ijcai.2023/226 40. Soos, M., Gocht, S., Meel, K.S.: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12224, pp. 463–484. Springer (2020). https://doi.org/10.1007/978-3030-53288-8\_22, https://doi.org/10.1007/978-3-030-53288-8_22

Quantifying Sensitivity for Tree Ensembles

41. Soos, M., Meel, K.S.: Engineering an efficient probabilistic exact model counter. In: Proceedings of the International Conference on Computer Aided Verification (CAV) (2025) 42. Varshney, N., Gupta, A., Ahmad, A., Tayal, T.V., Akshay, S.: Dataaware and scalable sensitivity analysis for decision tree ensembles. In: The Fourteenth International Conference on Learning Representations, ICLR 2026, Rio de Janeiro, April 23-27, 2026. OpenReview.net (2026), https://openreview.net/pdf?id=q8KqAvdfZK 43. Wang, Y., Zhang, H., Chen, H., Boning, D.S., Hsieh, C.: On lp-norm robustness of ensemble decision stumps and trees. In: Proceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event. Proceedings of Machine Learning Research, vol. 119, pp. 10104–10114. PMLR (2020), http://proceedings.mlr.press/v119/wang20aa.html 44. Yang, J., Meel, K.S.: Rounding meets approximate model counting. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 132–162. Springer (2023). https://doi.org/10.1007/978-3-031-37703-7\_7, https://doi.org/10.1007/978-3031-37703-7_7

Appendix This section is divided into five subsections : (i) self-contained proof of Theorem 1, (ii) the pseudocode of the subroutines used by the main algorithms, (iii) the experimental plots for each of the datasets and the plots for performance comparison over varying gap thresholds, (iv) extra details regarding the regularization application, and (v) a detailed explanation of the algorithm through an example.

Expanded Proof of Theorem 1

For completeness, we present a self-contained proof of Theorem 1. The argument relies on a standard concentration inequality for Poisson random variables, stated below for reference. Lemma 1 (Poisson concentration). Let X ∼ Poisson(λ) for λ > 0. Then for any x > 0, x2 Pr[|X − λ| ≥ x] ≤ 2 exp − . 2λ + x In particular, for any ϵ ∈ (0, 1], 2 ϵ λ Pr[|X − λ| ≥ ϵλ] ≤ 2 exp − . 3 We now give the detailed proof of Theorem 1.

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

Proof (Proof of Theorem 1). Fix an ordering of the subproblems processed by XCount. For each iteration i ∈ [m], let Ui ⊆ {0, 1}F denote the set of assignments generated by the i-th subproblem and define Si :=

i [

Ut ,

Sm :=

t=1

m [

Ut .

t=1

By construction, |Sm | = C(S, d, G). (i)

For j ≥ 0, let pj := 2−j . For i ∈ [m], define Xj to be the random multiset obtained after processing the first i subproblems, conditioned on the sampling probability being pj . For each t ≤ i, the algorithm draws Nt ∼ Poisson(|Ut | pj ) samples uniformly from Ut . For a fixed s ∈ Si , the total number of times s is generated is the sum of independent Poisson variables, one from each Ut containing s. This sum is Poisson with mean pj , and the multiplicities are independent across distinct s. Consequently, (i)

|Xj | ∼ Poisson(|Si |pj ). For 1 ≤ i ≤ m and j ≥ 0, define (i)

Ej := “after processing the first i subproblems, the algorithm has sampling probability pj ”, n o (i) (i) Aj := |Xj | ̸∈ |Si |pj (1 − ϵ), |Si |pj (1 + ϵ) . Let j ⋆ be the smallest integer j such that pj < (m)

On event Ej

Thresh . 4|Sm |

, the algorithm outputs (m)

b= C

|Xj | . pj

Hence,   ⋆ −1 h i jX [ (m) (m) b ̸∈ [(1 − ϵ)|Sm |, (1 + ϵ)|Sm |] ≤ Pr C Pr[Aj ] + Pr Ej  . j=0

j≥j ⋆

For j < j ⋆ , (m)

|Xj

| ∼ Poisson(λj ),

λj := |Sm |pj ≥ Thresh/4.

Quantifying Sensitivity for Tree Ensembles

Applying Lemma 1, (m) Pr[Aj ] ≤ 2 exp

ϵ2 λ j − 3

2 ϵ Thresh ≤ 2 exp − , 12

and therefore ⋆ jX −1

(m)

Pr[Aj

j=0

The event

2 δ ϵ Thresh ≤ . ] ≤ 2j ⋆ exp − 12 6

(m) can occur only if, for some i ∈ [m], j≥j ⋆ Ej (i)

|Xj ⋆ −1 | ≥ Thresh. For any fixed i, (i)

|Xj ⋆ −1 | ∼ Poisson(|Si |pj ⋆ −1 ) ≤ Poisson(Thresh/2), since Si ⊆ Sm and pj ⋆ −1 < Thresh/(2|Sm |). Applying Lemma 1, h i δ (i) . Pr |Xj ⋆ −1 | ≥ Thresh ≤ exp(−Thresh/6) ≤ 6m A union bound over i ∈ [m] yields   [ (m) δ Pr Ej  ≤ . 6 ⋆ j≥j

Combining the bounds, h i b ̸∈ [(1 − ϵ)|Sm |, (1 + ϵ)|Sm |] ≤ δ. Pr C Since |Sm | = C(S, d, G), the theorem follows.

Details of Section 4

This section contains the details of the procedures used by the primary algorithms listed in Section 4. The subroutine BitMaskGen takes as input an integer k and gives (k + 1) bit vectors, each of size k, such that for each bit vector the monotonicity property is followed - bit preceding a given bit must be greater that or equal to it.

Algorithm 3 BitMaskGen(k) 1: M askSet ← ∅ 2: BitM ask[k] ← 1 3: for i = 1 to k do 4: BitM ask[i] ← 0 5: M askSet ← BitM ask 6: return M askSet

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

The subroutine PruneTree takes a node of the tree as input and recursively prunes it by traversing the tree and checking decision at each node against the given assignment set m.

Algorithm 4 PruneTree(n, m) 1: if n is leaf then return 2: n.yes ← PruneTree(n.yes, m) 3: n.no ← PruneTree(n.no, m) 4: if (n.f eature, n.threshold) ∈ / m then return n 5: i ← index of (n.f eature, n.threshold) in m 6: nodes keep ← nullptr, discard ← nullptr 7: if m[i] == 1 then 8: keep ← n.yes 9: discard ← n.no 10: else 11: keep ← n.no 12: discard ← n.yes 13: return keep

The subroutine EncodeADD takes a decision tree node and recursively encodes it as an ADD by traversing through the tree by making the tree nodes as the nodes of the ADD, and the leaf value as the terminal node of the ADD which stores the real value.

Algorithm 5 EncodeADD(n) 1: init ADD node A 2: if n is a leaf node then return A ← n.val 3: else 4: A.true ← EncodeADD(n.yes) 5: A.f alse ← EncodeADD(n.no) 6: return A

The subroutine ToBDD converts an ADD to a BDD by taking a threshold value and constructing the terminal nodes of the BDD according to the decision whether the real value in the terminal node of the ADD is greater than the threshold.

Quantifying Sensitivity for Tree Ensembles

Algorithm 6 ToBDD(n) 1: if n is a leaf node then 2: if n.val > G then return 1 3: elsereturn 0 4: else 5: ToBDD(n.yes) 6: ToBDD(n.no) 7: return

The subroutine SampleBDD takes a BDD, an integer N and a pair of bitmasks, and samples satisfying assignments from the BDD uniformly, appends it with either one of the masks (randomly selected) to form the complete assignment and returns all such complete assignments.

Algorithm 7 SampleBDD(BDD,N ,pair) 1: S ← ∅ 2: for i = 1 to N do 3: Sample assignment x via top-down traversal using transition probabilities p(u → v) 4: m ← Sample one from bitmask pair (pair.m1 , pair.m2 ) with 0.5 probability 5: S.Append((x, m)) 6: return S

Details of Section 5

C.1

Plots for all datasets

In this section, we present the plots of experimental evaluation for each of the datasets in figure 7. C.2

Performance across varying gap thresholds

To test the performance of XCount across varying scales of gap thresholds, we tested it on 509 benchmark instances of models trained on Adult dataset, generated as per methodology outlined in ablation in 5 and running the instances for varying gap thresholds through 0.02, 0.2, 2 and 20, while keeping precision of leaves fixed at 3 decimal places. We observe that for lower gap threhold the performance of XCount slows down. This is expected as lowering the gap threshold effectively translates to counting assignments that lie closer to each other in terms of their ensemble output, and as we approach the scale of smallest difference possible between two ensemble outputs this would effectively count all possible assignments as satisfying the gap threshold.

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

(a) Diabetes

(b) Adult

(d) Protein structure

(e) Mnist

(f) Webspam

Fig. 7: Cactus plots comparing execution time. Lower curves indicate better performance.

Details on Section 6

D.1

L1 Regularization Parameter (α)

To understand the role of α, we first consider the standard objective function for tree ensemble models.

Quantifying Sensitivity for Tree Ensembles

(g) Wine-quality

(h) Fashion-Mnist

(i) Higgs

(j) Supersymmetry

Fig. 7: Cactus plots comparing execution time. Lower curves indicate better performance.

Fig. 8: Performance of XCount across gap values for models of Adult dataset.

Objective Function without Regularization In a typical gradient boosting framework, the goal is to minimize a loss function l that measures the difference between the predicted value ŷi and the actual value yi for each instance i. Without regularization, the objective function at iteration t aims solely to minimize this empirical loss [12]:

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

L(t) unreg =

n X

(t)

l(yi , ŷi )

(1)

i=1 (t)

where ŷi is the prediction at step t. Minimizing only this term often leads to complex models that fit the noise in the training data (overfitting).

Introducing Regularization To improve generalization, a regularization term Ω is added to the objective function. The regularized objective becomes [12]:

(t)

n X

(t) l(yi , ŷi ) +

i=1

K X

Ω(fk )

(2)

k=1

Here, Ω(fk ) penalizes the complexity of the k-th tree, discouraging overly complex models. The specific complexity penalty Ω(f ) used in our study includes both L1 and L2 components and is defined as:

Ω(f ) = γT + α

T X

1 X 2 w |wj | + λ 2 j=1 j j=1

(3)

This regularization term follows the standard XGBoost objective [12, 14] where: – T is the number of leaves in the tree. – wj is the weight (score) assigned to the j-th leaf. – γ (Minimum Split Loss): This parameter penalizes the number of leaves in a tree by adding a fixed cost for each leaf. A split is only performed if it results in a loss reduction greater than γ. – α (L1 Regularization Parameter): This parameter controls the strength of the L1 penalty applied to the leaf weights. – λ (L2 Regularization Parameter): This parameter controls the L2 penalty on the leaf weights. Unlike L1 regularization, L2 regularization does not enforce sparsity but instead shrinks large weights. The L1 term grows with the number of leaves and the magnitude of their weights. Since each additional split typically increases the number of leaves T , a larger α discourages overly complex trees and encourages fewer splits unless they significantly reduce the loss. Although the penalty does not explicitly depend on depth, deeper trees often contain more leaves, which indirectly increases the total regularization cost.

Quantifying Sensitivity for Tree Ensembles

Table 4: Accuracy, Precision, Recall, F1, AUC for all 24 models across varying Depths (d), Number of Trees (n), and L1 Regularization parameters (α). α=0 α=1 α=5 α = 10 Depth Trees Acc Prec Rec F1 AUC Acc Prec Rec F1 AUC Acc Prec Rec F1 AUC Acc Prec Rec F1 AUC d=3

n=20 0.859 0.671 0.229 0.341 0.857 0.859 0.671 0.226 0.338 0.857 0.859 0.672 0.225 0.337 0.857 0.858 0.675 0.218 0.330 0.857 n=30 0.858 0.680 0.213 0.325 0.863 0.857 0.665 0.210 0.319 0.864 0.858 0.669 0.217 0.328 0.864 0.859 0.681 0.222 0.335 0.863 n=40 0.859 0.684 0.218 0.330 0.867 0.858 0.672 0.216 0.327 0.867 0.857 0.668 0.209 0.319 0.867 0.858 0.668 0.218 0.329 0.867

d=4

n=20 0.859 0.676 0.227 0.339 0.864 0.859 0.676 0.228 0.341 0.865 0.858 0.654 0.229 0.339 0.865 0.859 0.666 0.231 0.343 0.864 n=30 0.859 0.677 0.229 0.342 0.869 0.859 0.666 0.239 0.352 0.869 0.859 0.652 0.237 0.348 0.869 0.859 0.666 0.234 0.346 0.868 n=40 0.859 0.656 0.254 0.366 0.872 0.859 0.656 0.252 0.364 0.872 0.859 0.652 0.250 0.361 0.872 0.859 0.654 0.245 0.356 0.871

D.2

Evaluation Metrics for the Models

To assess the predictive performance of the tree ensemble models, we utilize standard binary classification metrics derived from the confusion matrix. Let T P (True Positives) be the number of positive instances correctly classified, T N (True Negatives) be the number of negative instances correctly classified, F P (False Positives) be the number of negative instances incorrectly classified as positive, and F N (False Negatives) be the number of positive instances incorrectly classified as negative. The metrics presented in Table 4 are defined as follows: – Accuracy (Acc): The ratio of correctly predicted observations to the total observations. It measures the overall effectiveness of the classifier. Accuracy =

TP + TN TP + TN + FP + FN

(4)

– Precision (Prec): Also known as the positive predictive value, this metric measures the accuracy of the positive predictions. It indicates how many of the instances predicted as positive are actually positive. Precision =

TP TP + FP

(5)

– Recall (Rec): Also known as sensitivity or the true positive rate (TPR), this measures the ability of the classifier to find all the positive samples. It indicates what proportion of actual positive instances were identified correctly. TP (6) Recall = TP + FN – F1-Score (F1): The harmonic mean of Precision and Recall. It is particularly useful when the class distribution is imbalanced, as it seeks a balance between precision and recall. F1 = 2 ·

Precision · Recall Precision + Recall

(7)

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

– AUC (Area Under the ROC Curve): The Receiver Operating Characteristic (ROC) curve plots the True Positive Rate (Recall) against the False P Positive Rate (F P R = T NF+F P ) at various threshold settings. The AUC represents the degree of separability between classes. Probabilistically, the AUC corresponds to the probability that the classifier ranks a randomly chosen positive instance higher than a randomly chosen negative instance. An AUC of 0.5 suggests no discrimination (random guessing), while an AUC of 1.0 implies perfect discrimination.

Example Run: Step-by-Step Execution of XCount

This section provides a detailed walkthrough of the algorithm using a example. We demonstrate how XCount processes a small decision tree ensemble to count sensitive regions, referencing the procedures outlined in Section 4 and the actual data structures used in the implementation. E.1

Input Configuration

We consider an XGBoost regression model with 3 trees of depth 2 trained on the Diabetes dataset. The configuration for the sensitivity query is a sensitive feature f2 (feature index 2), a bit distance d = 1, and a gap threshold G = 0.1. E.2

Original Ensemble

Figure 9 shows the three decision trees (T ). Note that the trees split on the sensitive feature we chose (i.e. f2 ), as well as the non-sensitive features (f3 and f8 ). E.3

Extracting Splits and Generating Bitmasks

The execution begins by traversing the ensemble and identify all split conditions. The extracted thresholds on the feature f2 are θ1 = 0.005, θ2 = 0.009, and θ3 = 0.073. Following Algorithm 3 (BitMaskGen), we enforce the monotonicity constraint (bθ1 ⇒ bθ2 ⇒ bθ3 ) to generate the valid discretized regions. In the implementation, this set of valid masks (M askSet) is stored as a vector of bitmasks: Mask ID BitMask (bθ1 , bθ2 , bθ3 ) Interpretation (f2 range) m0 (0, 0, 0) f2 > 0.073 m1 (0, 0, 1) 0.009 < f2 ≤ 0.073 m2 (0, 1, 1) 0.005 < f2 ≤ 0.009 m3 (1, 1, 1) f2 ≤ 0.005

Quantifying Sensitivity for Tree Ensembles

(a) Tree 0

(b) Tree 1

Fig. 9: The three decision trees in the ensemble. Internal nodes show split conditions of the form “fi ≤ θ”. E.4

Subproblem Generation

The algorithm iterates through the M askSet to generate subproblems. The total number of subproblems depends on the number of valid masks (M = |M askSet|) and the bit distance d. For a single sensitive feature with monotonic constraints, the masks form a linear sequence where the Hamming distance between any two masks mi and mj corresponds to their index difference |i − j|. A subproblem is generated for every ordered pair (mi , mj ) where 1 ≤ |i − j| ≤ d. For this example, with M = 4 and d = 1, we consider only immediate neighbors (|i − j| = 1). The total count is calculated as: Total Subproblems =

d X

2 · (M − k) = 2 · (4 − 1) = 6

k=1

These are collected into the subpArray structure, shown below as a vector of pairs: Index Element (pair<Mask, Mask>) 0 ⟨(1, 1, 1), (0, 1, 1)⟩ 1 ⟨(0, 1, 1), (1, 1, 1)⟩ 2 ⟨(0, 1, 1), (0, 0, 1)⟩ 3 ⟨(0, 0, 1), (0, 1, 1)⟩ 4 ⟨(0, 0, 1), (0, 0, 0)⟩ 5 ⟨(0, 0, 0), (0, 0, 1)⟩ We focus our trace on Subproblem 1 (Index 1), which contains the pair ⟨(0, 1, 1), (1, 1, 1)⟩, and for the rest of the subproblems, we summarize the final results.

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

It is crucial to note that within the context of a specific subproblem, the ADDs generated are no longer functions of the sensitive feature f2 . The subproblem explicitly fixes the range of f2 , causing all f2 nodes to resolve during pruning.

E.5

Processing Subproblem 1

In Algorithm 2, we present the ProcessSubproblem procedure. It initializes the DiffSum ADD to zero and iterates through the trees, as can be seen in line 5 of Algorithm 2.

Tree Pruning and Encoding In Algorithm 2, the PruneTree function ( Algorithm 4), is called to prune each tree based on the masks in the subproblem. For each tree T ∈ T , the algorithm prunes it twice: once for Mask m2 and once for Mask m3 . For Mask m2 (0.005 < f2 ≤ 0.009), the check f2 ≤ 0.005 evaluates to False. Conversely, for Mask m3 (f2 ≤ 0.005), the same check evaluates to True. Figure 10 displays the ADD structures for all three trees immediately after this pruning step. At this stage (before constraints are enforced), the ADDs may still contain paths that are logically inconsistent with the feature monotonicity constraints. To ensure the consistency, the algorithm applies the constraints to the ADDs. This results in the structures shown in Figure 11.

(a) Tree 0, Mask m2

(d) Tree 1, Mask m3

(b) Tree 0, Mask m3

(e) Tree 2, Mask m2

(f) Tree 2, Mask m3

Fig. 10: ADDs for Trees 0, 1, and 2 immediately after pruning with Masks m2 and m3 , but before standardizing constraints are applied.

Quantifying Sensitivity for Tree Ensembles

(a) Tree 0, Mask m2

(b) Tree 0, Mask m3

(d) Tree 1, Mask m3

(e) Tree 2, Mask m2

(f) Tree 2, Mask m3

Fig. 11: ADDs for Trees 0, 1, and 2 after pruning and applying constraints.

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

Subtraction and Accumulation In Line 7 of Algorithm 2, the algorithm computes DiffADD, which is the difference between the pair of ADDs obtained by pruning the same tree with the two differing masks. In Line 8, this difference is accumulated into the DiffSum ADD. Figure 12 shows the growth of the DiffSum ADD as we aggregate the differences from Tree 0, Tree 1, and Tree 2.

(a) After Tree 0

(b) After Tree 1

Fig. 12: Evolution of the cumulative DiffSum ADD for Subproblem 1. The ADD in 12c shows the final DiffSum for the Subproblem.

E.6

Merging Subproblems and Counting

After processing all trees, we obtain the symbolic representation of the prediction difference for a subproblem. Figure 13 displays these final ADDs for all 6 subproblems generated by the decomposition. We then transform these ADDs into a boolean representation (BDDs) by applying the gap threshold G. Terminal nodes in the ADD are checked: if value > G, the path maps to 1 (sensitive). The resulting BDDs are shown in Figure 14. It is important to recognize that a single satisfying assignment in this resulting BDD corresponds to two distinct sensitive regions in the original input

Quantifying Sensitivity for Tree Ensembles

(a) Subproblem 0

(b) Subproblem 1

(d) Subproblem 3

(e) Subproblem 4

(f) Subproblem 5

Fig. 13: Final DiffSum ADDs for subproblems 0–5. These graphs represent the accumulated ensemble prediction difference for each mask pair before applying the gap threshold.

S. Akshay, C. Garg, A. Gupta, K.S. Meel, A. Naik

space—one for each mask involved in the subproblem pair. Since the decomposition process generates subproblems for adjacent mask pairs, the resulting sets of sensitive regions frequently overlap. Figure 14 demonstrates this phenomenon (e.g., between Subproblem 1 and Subproblem 3, which share mask m2 ).

(a) Subproblem 1

(b) Subproblem 3

Fig. 14: Final BDDs for subproblems 1, 3 and 5, where the ADD did not evaluate to 0 upon applying the threshold. The rest of the ADDs resulted in BDDs that evaluate to 0 as all the leaf values were below the gap threshold G = 0.1. Each BDD represents the sensitive regions found for a specific pair of bitmasks. Overlaps between these BDDs necessitate the use of the Pepin counting technique.

To address the overlap, XCount utilizes the sampling-based Pepin counting technique (detailed in Section 4). Conceptually, this involves a global solution set (referred to as X in the algorithm) where satisfying assignments from the BDDs of different subproblems are aggregated. The algorithm statistically estimates the size of the union of these sets to produce the final count of unique sensitive regions.

Record · ID 180641 · SHA-256 8958d9200de19595
Retrieved via Conceptio — every document is proof-bundled with source, license, and retrieval metadata.