{'fraction_non_alphanumeric': 0.03719463740996129, 'fraction_numerical': 0.014867601445746071, 'mean_word_length': 4.266909680032402, 'pattern_counts': {'":': 0, '<': 16, '<?xml version=': 0, '>': 3, 'https://': 3, 'lorem ipsum': 0, 'www.': 3, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 11, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Versatile Verification of Tree Ensembles

Machine learned models often must abide by certain requirements (e.g., fairness or legal). This has spurred interested in developing approaches that can provably verify whether a model satisfies certain properties. This paper introduces a generic algorithm called Veritas that enables tackling multiple different verification tasks for tree ensemble models like random forests (RFs) and gradient boosting decision trees (GBDTs). This generality contrasts with previous work, which has focused exclusively on either adversarial example generation or robustness checking. Veritas formulates the verification task as a generic optimization problem and introduces a novel search space representation. Veritas offers two key advantages. First, it provides anytime lower and upper bounds when the optimization problem cannot be solved exactly. In contrast, many existing methods have focused on exact solutions and are thus limited by the verification problem being NP-complete. Second, Veritas produces full (bounded suboptimal) solutions that can be used to generate concrete examples. We experimentally show that Veritas outperforms the previous state of the art by (a) generating exact solutions more frequently, (b) producing tighter bounds when (a) is not possible, and (c) offering orders of magnitude speed ups. Subsequently, Veritas enables tackling more and larger real-world verification scenarios.


Introduction
Currently, it is becoming more common for deployed machine learned models to conform to requirements (e.g., legal) or exhibit specific properties (e.g., fairness). This has motivated the development of verification approaches that are applicable to learned models. Given a specific property, these techniques verify, that is, prove whether or not the property holds. Some examples of verification questions are: • Adversarial example generation: Given a data example, can slightly perturbing it cause its predicted label to flip? • Fairness: Do two instances exist that differ only their protected attributes (e.g. sex, race, age) or a proxy variable, but have different predicted labels? (Dwork et al. 2012) If a property is violated, it is desirable to also return constructed counter examples. For instance, if an adversarial example exists it is useful to see one concrete instance as this could, for example, be added to the training set. The popularity of additive tree ensembles (e.g., random forests (Breiman 2001) and gradient boosting tree models (Chen and Guestrin 2016;Ke et al. 2017;Devos, Meert, and Davis 2019)) has motivated interest in developing verification techniques for this model class. Most current work is characterized by its focus on (1) solving one specific type of verification problem (e.g., adversarial example generation (Einziger et al. 2019) or robustness checking (Chen et al. 2019b; Törnblom and Nadjm-Tehrani 2020; Ranzato and Zanella 2020)) and (2) developing exact solutions. While exact solutions are desirable, in practice they are not always feasible because verification tasks on additive ensembles are NP-complete (Kantchelian, Tygar, and Joseph 2016).
Recently, Chen et al. (2019b) took a first step towards overcoming (2) by developing a graph-based approach that computes an upper bound rather than a full solution if time and space limits are exceeded. However, this approach has three important limitations. First, the search steps are very coarse-grained, and the algorithm often terminates after only a few steps. Second, the algorithm is not guided by a heuristic, so a selected step may not improve the bound. Practically, this translates into the algorithm generating looser bounds. Third, the approach only is able to generate an example if the search terminates.
This paper introduces a generic anytime algorithm called VERITAS -Verification of Trees using Anytime Searchfor addressing multiple different types of verification task on tree ensembles. This contrast with existing work that focuses on a single verification task. The key insight underlying VERITAS is that a large class of verification problems can be posed as a generic constrained optimization problem. We propose a novel search space for which an admissible heuristic exists, which confers two advantages. First, it provides anytime upper and lower bounds. Second, it can generate a concrete example using the current lower bound. Empirically, we evaluate our approach on a number of verification tasks and show that we outperform the state of art by (1) generating exact solutions more frequently, (2) producing tighter bounds when no exact solution is found (3) offering orders of magnitude speed ups.

Additive Tree Ensembles
The framework described in this paper reasons about additive ensembles of binary trees. 1 A binary tree T consists of two types of nodes. An internal node stores a split condition and references to a left and a right child node. The split condition is a less-than comparison X < τ defined on an attribute X for some threshold τ . Splits on binary attributes are possible using τ = 0.5. A leaf node has no children and simply stores an output value ν called the leaf value. The root node is the only node that has no parent.
Given a data example x from the input space X , a tree is evaluated by recursively traversing it starting from the root node. For internal nodes, the node's split condition is tested on x; if the test succeeds, the procedure is recursively applied to the left child node, else, it is applied to the right child node. If a leaf node is encountered, the leaf value is returned and the procedure terminates.
The box of leaf l, denoted box(l), defines a hypercube of the input space by conjoining all split condition from the root to l. All data examples x ∈ box(l) evaluate to leaf l. For example, box(l 2 2 ) in Figure 1 equals {Age < 50, Height ≥ 200}. We also extend the definition of box to a set of leafs: box(l 1 , . . . , l M ) = m box(l m ). Two leafs overlap when the intersection of their boxes is non-empty. For example, in Figure 1, leaf l 2 2 overlaps with l 1 1 , but does not with l 3 3 . An additive ensemble of trees is a sum of trees T = T 1 + · · · + T M . We use l m i to denote the ith leaf of tree T m . Given a data example x, T evaluates to the sum of the evaluations of all trees. The set of leaf nodes whose leaf values contribute to the output of the ensemble is called an output configuration of the ensemble. The box of an output configuration is by definition non-empty. For all data examples x in an output configuration's box, the output of the ensemble is fixed because the same leafs are activated each time. For example, in Figure 1, box(l 1 1 , l 2 1 , l 3 1 ) = {Age < 40, Height < 200, BMI < 28}. All data examples in that box will evaluate to ν 1 1 + ν 2 1 + ν 3 1 .

MERGE: Robustness Verification
Chen et al. (2019b) present a method for robustness verification of tree ensembles. Their algorithm produces a lower bound δ on the distance to the closest adversarial example for a particular example x and uses a 10-step binary search. Given a model T , a data example x with predicted label T (x), and a maximum distance δ, they verify whether an examplex in the area of x, ||x −x|| ∞ < δ, exists that flips 1 Note that all trees can be represented as binary trees. its multipartite graph transformation G, with l m i the ith leaf of tree T m . The graph consists of M = 3 independent sets, one for each tree, and are denoted by a gray rectangular background. Edges in G connect leafs that have overlapping boxes. A max-clique contains exactly one vertex from each independent set (tree), and corresponds to an output configuration of the ensemble. An example max-clique in G is [l 1 1 , l 2 1 , l 3 1 ] denoted by bold vertexes and bold edges.
the predicted label: T (x) = T (x). If such an example exists, the area surrounding x is shrunk by decreasing δ, else, the area is expanded by increasing δ. This is repeated 10 times or until enough precision on δ is obtained.
To prove that nox exists with a flipped label within a distance δ from x, Chen et al. use a graph representation of the ensemble model and a merge procedure defined on the independent sets 2 of the graph to compute an upper bound on the ensemble's output. When the upper bound is less than zero, it is impossible for the ensemble to output the positive class for any example in the area surrounding x.
The graph G has one vertex for each leaf l m i of each tree T m in ensemble T . Two vertexes are connected by an edge when their boxes overlap. Figure 1 shows an ensemble and its corresponding graph representation. When verifying robustness, only the neighborhood surrounding an example x is considered. This is accomplished by including only the leafs that are accessible by examples close to x. Specifically, only leafs l m i for which ax ∈ box(l m i ), ||x −x|| ∞ < δ exists are included in the graph. For example in Figure 1, with δ = 5 and x = {Age: 60, Height: 180, BMI: 21}, only leafs l 1 2 , l 2 1 , and l 3 1 are included. The graph has two key properties: (1) there is a one-toone correspondence between the trees in the ensemble and the independent sets, and (2) there is a one-to-one correspondence between an output configuration and a max-clique.
Lemma 1 (Lemma 1, proof in (Chen et al. 2019b)). A set of leafs is a max-clique in G iff it is an output configuration.
Chen et al.'s main contribution is realizing that merging independent sets maintains the property in Lemma 1 and improves the upper bound on the ensemble's outputb: where m ranges over the remaining independent sets and ν m i are the leaf values of the vertexes in independent set m.
The MERGE algorithm has three major drawbacks. First, it is coarse-grained: the number of steps is at most log 2 (M ) . The computational difficulty of each step grows exponentially, so the algorithm stalls after only a few steps. Second, it is not guided by a heuristic and most of its work does not improve the bound in Equation 1. Third, the algorithm only produces a full solution when it runs to completion, i.e., all independent sets are merged into one.

VERITAS: Verification as a Constrained Optimization Problem
Consider the following optimization problems: Robustness checking Let T be a binary classifier that classifies example x as negative. If max ||x−x|| ∞ <δ T (x) < 0, then no positively classified perturbed example can exist within distance δ from x.
Fairness Suppose an insurance company estimates its clients' health scores using model T and wants to know which attributes affect the health score of middle-aged women the most. Given two middle-aged female individuals x 1 and x 2 that differ only in a single attribute, the most dominant attribute is the one that maximizes T (x 2 ) − T (x 1 ). The insurance company could take precautions if the most dominant attribute is a protected attribute, because that could be considered unfair. Both these example belong to a class of verification problems that can be modeled as a generic optimization problem: find two examples that (1) satisfy the given constraints and (2) maximize the difference between the outputs of two models. Formally, the optimization problem is: where T 1 and T 2 are models, x 1 and x 2 are examples from the input space X , and C : X 2 → {true, false} is a function defining constraints on the input space. In many cases, we only consider a single model T . Taking T 1 to be the trivial model that always predicts 0.0, and T 2 = T , yields the maximization problem: Minimizing T is also possible by taking T 1 = T , and making T 2 the trivial model. Note that we simplify C because the example of the trivial model does not affect the outcome. The algorithm presented in this paper, VERITAS, is a search algorithm that solves the optimization problem in Equation 2. The algorithm operates in a novel search space derived from Chen et al.'s graph representation G. It is finegrained as a single step is cheap, heuristically guided and does not waste time in irrelevant parts of the search space. The algorithm is anytime and outputs ever-improving upper bounds, lower bounds, and suboptimal full solutions as it is running. As more time and memory is provided, the bounds grow closer until the exact full solution is found. As this problem is NP-complete (Kantchelian, Tygar, and Joseph 2016), it might take a long time until the bounds converge to an exact solution. This makes the anytime nature of VER-ITAS particularly compelling.
We will first introduce the search space. Then, we will show how this space is used to solve the optimization problem in Equation 2. For ease of explanation, we will first tackle the single-instance setting in Equation 3, and then extend our method to support the two-instance setting.

The Search Space S
The search is not executed directly in G, but rather in a sound and complete search space S derived from G. The states of S are cliques in G and are represented as sequences of leaf nodes. Starting from the initial empty sequence [ ] at depth 0, the search space recursively builds up output configurations by adding leafs to the state in order, one leaf per tree. Specifically, a state s = [l 1 i1 , . . . , l m im ] at depth m is expanded to states C(s) at depth m + 1: where L m+1 is the set of all leafs of tree T m+1 . The expand function C ensures that each expanded state is again a clique in G by allowing only states with non-empty boxes. When depth m = M is reached, an output configuration, or equivalently a max-clique is found. The search space has two important properties. For brevity, we will write box(s) to indicate the box of the set of leafs in the search state s ∈ S.
Theorem 1. Each state at depth m = M corresponds to an output configuration (i.e., a max-clique in G), and the search space enumerates all output configurations, that is, the enumeration is sound and complete.
Proof. We show that S is sound and complete. Soundness: We show that any state s = [l 1 i1 , . . . , l M i M ] is an output configuration. By definition of C in Equation 4, the box of the state is non-empty. For each data example x in the state's box, it holds that x ∈ box(l m im ), m = 1, . . . , M . Because of the properties of tree evaluation and the definition of box, tree T m evaluates x to leaf l m im . Therefore, a data example x exists that activates all leaf nodes in s, and the configuration is valid. Using Lemma 1, it follows that s is a max-clique in G.
Completeness: Assume an output ⊆ O be sequences of leaf nodes such that s is a state in S, but t is not. It must be that t / ∈ C(s). This can only be true when box(t) = box(l 1 i1 , . . . , l m im , l m+1 im+1 ) = m+1 m =1 box(l m i m ) = ∅. This contradicts the fact that O is an output configuration.

Finding The Best State at Depth M
To solve the optimization problem in Equation 3, we need to find the state in S at depth M with the maximum output that adheres to the constraints C. Constructing S explicitly and choosing the optimal state by enumerating all possibilities is intractable in practice. For that reason, we introduce an admissible and consistent heuristic to traverse the space in a best-first fashion. This allows us to only materialize the parts of S that are relevant to the problem.
The search is based on A*. It maintains an OPEN list of states in S and repeatedly expands the state in OPEN with the best f -value until a state at depth M is found. It removes the current best state s = [l 1 i1 , . . . , l m im ] from OPEN and adds all its successors C(s) to OPEN. The f -value is the sum of two values: g(s), the sum of the leaf values of the leafs in the state, and the heuristic h(s), an estimation of the remaining value to a state at depth M : Intuitively, the heuristic h(s) sums upper bounds h m (s) for all remaining trees T m for which no leaf has been added to the state yet. The upper bound h m (s) is the maximum leaf value of any leaf of T m that overlaps with all leafs in s. Note that we do not need to keep a VISITED list, because there are no cycles. We show that this heuristic leads us to the optimal solution next.
Theorem 2. The heuristic search in S is guaranteed to find the max-clique in G which corresponds to the optimal output configuration of the optimization problem in Equation 3.
Proof. We need to show that the heuristic is admissible and consistent (Dechter and Pearl 1985). Admissible: For maximization problems, a heuristic is admissible when it never underestimates the remaining value to the goal state. This is the case because each leaf considered for extension in Equation 4 is also considered in the max of Equation 7.

Anytime Upper and Lower Bound Estimates
Depending on the size and difficulty of the problem, the search defined above might take a long time to find a solution. However, even when the search is terminated prematurely, the current best state in the OPEN list still contains useful information: because h is admissible, the current best f -value is an upper boundb on the optimal output.
To also produce a lower bound on the maximum output of the ensemble, we borrow ideas from Anytime Repairing A* (ARA*) (Likhachev, Gordon, and Thrun 2004). The importance of the heuristic in the f -value is reduced by , 0 < ≤ 1 as follows: This promotes deeper solutions, yielding full solutions much quicker. However, when < 1, the solutions might no longer be optimal because h(s) is no longer an admissible heuristic. Nonetheless, the suboptimality is bounded by : for a suboptimal solutionx, the optimal solution's output is no larger than T (x)/ . A suboptimal solutionx is at least as good as the optimal solution, so T (x) is a lower bound b on the optimal output. Both the upper bound and the lower bound are anytime: The best f -value in the OPEN list is always accessible. The value in the relaxed f -score of Equation 8 can be gradually increased each time a suboptimal solution is found. Using ARA* means that it is not necessary to restart the search from scratch: the OPEN list can be reused, making the incremental increase of a cheap operation. 3

Incorporating Constraints into the Search
A naive way of incorporating the constraint function C in Equations 2 and 3 is to ignore it during the search, and filter solutions returned by the search. This is inefficient, as the constraints often rule out large chunks of the search space.
For that reason, we lift C to the search state level. For example, considering the example in Figure 1 and the constraint Age > 60, we reject states [l 1 1 ], [l 1 2 , l 2 2 ], and [l 1 2 , l 2 1 , l 3 2 ]. Let C s : S → {true, false} be a function mapping the states of the search space to accept or reject. The function has the following two properties: 1. It is consistent with C: a state s is accepted by C s if and only if it is possible to find a data example x that sorts to the leafs in s and C(x) is true. 2. It is consistent across states: if C s (s) = false, and t ⊇ s is a descendant from s, then C s (t) = false. In words: if a state is rejected by C s , then all its state expansions must also be rejected. This property ensures that we do not reject states that are the predecessor of a valid state. Because all split conditions in the tree ensemble are simple linear constraints, the two properties are trivially satisfied. The constraint function C s can be integrated into the search procedure by only adding accepted states to the OPEN list. For simple linear constraints, we can prune the graph G before the search starts, just like in the MERGE algorithm.

Maximizing the Difference Between Two Models
Now we explain the necessary adjustments to enable solving Equation 2. The search space is modified as follows: a state is extended to consist of two sequences of leafs, one sequence for each instance. The expand function alternately expands the first and the second instance using Equation 4. The f -value maximized by the search is updated to the difference between the f -values of the two instances: The g ( Equation 5) and h 2 (Equation 6) remain unchanged.
The first heuristic h 1 is an admissible and consistent heuristic with respect to the minimizing variant of Equation 3 obtained by replacing max by min in Equation 7. This makes h 2 − h 1 an admissible and consistent heuristic for the optimization problem in Equation 2 (proof in appendix).

Summarizing the Setup
We now have all necessary tools to answer verification questions. First, train a tree ensemble. Second, define the constraint function C s . The complexity of this step greatly depends on the verification question. 4 Third, give the learned model and C s to VERITAS, which will produce a stream of decreasing upper boundsb, and a stream of increasing lower bounds b = T (x), withx suboptimal full solutions. Given infinite time and memory, the bounds converge:b = b, and the lastx is the optimal solution.

Experimental Evaluation
We compare our method to MERGE on four tasks: (1) robustness verification, MERGE's core task, (2) a stress test on four datasets with varying model sizes, (3) randomly generated verification questions, and (4) two new general use cases. The last task surpasses MERGE's capabilities. MERGE is the current state of the art for robustness verification. It outperforms an exact mixed-integer linear programming (MILP) approach (Kantchelian, Tygar, and Joseph 2016), and a linear programming relaxation of the MILP approach. MERGE is orders of magnitude faster than the former and offers a better bound than the latter. We do not compare to Silva (Ranzato and Zanella 2020) and VoTE (Törnblom and Nadjm-Tehrani 2020) because their systems do not estimate the distance to the closest adversarial example. Rather, they only check robustness for δ = 1, the easiest, most restrictive case. Furthermore, as Törnblom and Nadjm-Tehrani also indicate, VoTE struggles to scale to datasets with a larger number of attributes like MNIST.
To compare the run times of VERITAS and MERGE, we measure the time taken by VERITAS to reach MERGE's best bound. We refer to this as the time to bound or TTB statistic. We set MERGE's L parameter (the number of independent sets merged per step) to 2 to make MERGE as fine-grained as possible. We run MERGE until either it finds the optimal solution or time or memory runs out. Originally, MERGE only produced an upper boundb. We use Equation 1 with max replaced by min as a lower bound for MERGE.
We use XGBoost to train GBDT models. As we will be comparing different model sizes, we choose an appropriate tree depth and ensemble size per experiment, and use hyperparameter optimization to find a suitable learning rate for a particular tree depth and ensemble size pair. All experiments ran on an Intel(R) Core(TM) i7-2600 CPU with 16GB of memory. Details about datasets, timeouts, memory limits, and model parameters can be found in the appendix.

Verifying Robustness
In this first experiment, we show how better upper bounds b on the ensemble's output improve δ, the lower bound estimate on the distance to the closest adversarial example. We trained a multi-classification GBDT model T with 50 trees of depth 5 on MNIST. The model consists of one binary onevs-all classifier T y per digit. We pick a random digit x with predicted label y = T (x) from the dataset and a target label y = y, and use the binary search procedure to compute δ for the closest adversarial example labeled y instead of y. The binary search uses the upper boundb on the maximal value of T y (x) − T y (x), ||x −x|| ∞ < δ, to direct its updates to δ. It starts at δ = 20 and increases δ when no adversarial example exists (b < 0), or decreases δ when an adversarial example may exist (b ≥ 0). The search takes 10 such steps and ultimately produces a lower bound δ. This procedure is repeated 1260 times, yielding 12,600 upper boundb calculations. The performance of VERITAS and MERGE is summarized below:

VERITAS generates a better upper boundb in all cases.
This leads to a divergence in the binary search in 15.5% of the cases, resulting in better lower bounds δ. In all other cases, VERITAS and MERGE produce the same δ.
2. VERITAS can prove that its δ value is optimal in 99% of the cases. It does this by generating an adversarial exam-  Figure 3: Illustrations of two binary search executions on two MNIST digits, a 5 and an 8. VERITAS and MERGE compute a lower bound δ on the distance to the closest adversarial example that is classified as a 4 (left) and a 3 (right). The background colors indicate the remaining binary search interval on δ. A higher δ value is better. ple (a full solution) for a δ 1 , and proving that no adversarial example for a δ 2 exists, and δ 1 = δ 2 . Because MNIST attribute values are integers, the minimal distance is the integer that has δ 1 and δ 2 on either side.
3. VERITAS is faster than MERGE for 98% of theb calculations using the TTB statistic. In 59% of the cases, our algorithm is more than 1000 times faster.
Two example binary search executions are illustrated in Figure 3. The left shows an example where both lower bounds δ converge. The right shows an example where VERITAS outputs a better δ value.

Stress Testing
Robustness verification is inherently strongly constrained: it only considers a small neighborhood surrounding a particular fully defined example. This greatly reduces the complexity of the verification problem. In terms of the number of possible solutions, the most difficult verification task is simply "what is the maximal output value of the ensemble?" We compare VERITAS and MERGE on this task for four datasets: Covertype, Allstate, California housing, and Higgs. To explore how the approaches scale on this task, we vary both the number of trees in the ensemble (M ∈ {50, 100, 200, 400}) and the maximum depth of the learned trees. Figure 4 shows the upper and lower bounds for both methods for the Covertype dataset. VERITAS finds substantially tighter bounds than MERGE in all cases and produces usable bounds even for large and deep models. The same holds for the other datasets (results in appendix).

Randomly Generated Verification Tasks
To get a better idea of how both VERITAS and MERGE perform on a wide range of verification questions, we randomly generate τ min ≤ X < τ max constraints on the input attributes of the Allstate, California housing, Covertype and Higgs datasets. We then compute the maximum output of an ensemble trained on a particular dataset given the generated constraints. Recall that a leaf is unreachable given a constraint on an input attribute when the constraint conflicts with the leaf's box. For example, in Figure 1, the constraint Age < 55 makes l 1 2 , l 2 3 , and l 3 3 unreachable. We tune the difficulty of a problem by varying the number of accessible leafs; for the easiest problems, only 10% of the leafs are reachable, whereas for the hardest problems, (nearly) all leafs are reachable. Reducing the number of accessible leafs ultimately reduces the number of possible output configurations, which in turn cuts down the number of possible outcomes of the search problem. The ensembles uniformly range in size from 25 to 500 trees and in tree depth from 3 to 8. Table 1 shows the aggregated results for 2160 generated problems per dataset. The upper bound of VERITAS is better in all cases. The lower bound is better in more than 99% of the cases, and is worse only when the relaxed search cannot find a suboptimal full solution in time. Table 1 contains three more per-dataset statistics. The second and third columns show that VERITAS is capable of finding the exact optimal solution 3 to 5 times more frequently than MERGE. To compare the quality of the bounds when the optimal solution is not found, we measure the relative gap size (b − b)/b between the upper and the lower boundsb and b. A smaller gap indicates tighter bounds. The gap histograms show that the bounds generated by VERI-TAS are much better than those generated by MERGE. For the first three datasets, VERITAS's gap is at most 50% in more than 95% of the cases (69% for Higgs). This statistic is between 3 and 11% for MERGE. As in the robustness experiment, we use the TTB statistic to show that VERITAS is often orders of magnitude faster than MERGE. Overall, our algorithm is faster in 98% of the cases (90% for Higgs), and in 15% to 25% of the cases, our algorithm is more than 1000 times faster.

Two New Verification Use Cases
We now present two examples of real-world verification questions that our approach can solve but MERGE cannot because it lacks support for a state constraint function C s and lacks the ability to generate suboptimal full solutions.
Finding Dominant Attributes: YouTube For this experiment we use a dataset generated from trending YouTube videos. The task is to predict the order of magnitude of views given a bag-of-words representation of the words used in the title and description of the video. We use a GBDT model with 100 trees of depth 10. Given a number of initial words, we ask VERITAS to produce k additional words such that the predicted views count is maximized. The state function C s checks the at-most-k constraint. Some examples: • live, breaking, news, war → adding words big and trailers increases the prediction by 2 orders of magnitude.
• epic, challenge → adding words album, video, and remix increases the prediction by almost 5 orders of magnitude.
This approach is very general: it is a generic strategy that allows reasoning about the importance or dominance of one or more attributes. Other examples are fairness: given a set of constraints on the input space, maximize or minimize the output of the ensemble when only varying the values of one or more protected (proxy) attributes. If VERITAS finds examples of individuals that are treated significantly differently, then that might indicate unwanted model behavior.
Domain Specific Questions: Soccer For this experiment we train a model that predicts the probability of scoring a goal in soccer within the next 10 actions (Decroos et al. 2019). The model has 126 trees (early stopping) of depth 10.
The input for the model is two consecutive game states described by the position of the ball and the two action types (pass, shot, etc.). We can ask a number of interesting domain specific questions: what ball action do we need to perform to maximize the goal probability? or in which contexts does a backwards pass increase the probability of scoring in the next 10 actions? Figure 5 shows two generated instances. The state constraint function C s checks two oneout-of-k constraints corresponding to the one-hot-encoded action types.

Related work
A considerable amount of work has been done on verification of tree ensembles. Most work has focused on adversar- Törnblom and Nadjm-Tehrani introduced the VoTE framework, a system that enumerates all equivalence classessets of data examples that evaluate to the same output value, equivalent to the concept of output configurations in this paper -and checks whether some property holds.
The properties that can be tested are general. However, the approach is limited by the number of equivalence classes, which quickly grows exponentially large (Törnblom and Nadjm-Tehrani 2018; Törnblom and Nadjm-Tehrani 2019; Törnblom and Nadjm-Tehrani 2020). Logical SMT theorem provers have also been used (Einziger et al. 2019;Sato et al. 2019;Devos, Meert, and Davis 2020), as have mixed-integer linear programming tools (Kantchelian, Tygar, and Joseph 2016). These approaches translate ensemble models to their respective languages and apply general purpose solvers to prove certain properties of the models. Others have applied tools from program analysis like abstract interpretation to verification of tree ensembles (Ranzato and Zanella 2020;Drews, Albarghouthi, and D'Antoni 2020;Calzavara, Ferrara, and Lucchese 2020). There is also work that focuses on learning robust models (Chen et al. 2019a;Calzavara, Lucchese, and Tolomei 2019). Rather than verifying the robustness of existing models, these methods build models that are less susceptible to adversarial attacks.

Conclusion
We introduced VERITAS, a tree ensemble verification tool that is capable of solving verification tasks that can be modeled as a generic optimization problem. It operates in a novel sound and complete search space and traverses that space using an admissible and consistent heuristic. VERITAS is the first anytime algorithm to produce both an upper and a lower bound on the output of a tree ensemble model. Additionally, it also generates full suboptimal solutions that converge to the optimal solution when given enough time and memory. We empirically show that VERITAS outperforms the state of the art both in terms of quality of the bounds, as well as in terms of run time.

Potential Ethical Impact
This work takes us a step closer toward machine learning models with verified properties. The properties themselves can, for example, reflect issues concerning discrimination, fairness, and safety. Having the ability to identify such issues in models could have a large impact on machine learning in general. First of all, the ability to avoid the aforementioned issues is by itself a leap forward. Second, having models with verified properties could improve the trust in machine learning, and further accelerate its adoption, especially to application areas that are currently hesitant or legally prohibited to adopt machine learning in practice. Third, the ability to query the model and generate (counter-)examples improves the interpretability and explainability of the learned model.

A.1 Proof of Consistent Heuristic
We prove that h 2 (s 1 ) − h 1 (s 1 ) is a consistent heuristic for the optimization problem in Equation 2 of the main paper (admissibility follows from consistency). First, we show that h 1 is a consistent heuristic: Theorem 3. The heuristic obtained by replacing max by min in Equation 7 in the main paper, i.e., box(l 1 i1 , . . . , l m im , l m ) = ∅ }, is a consistent heuristic for the minimization problem min x1 T 1 (x 1 ).
Proof. For minimization problems, consistent means that h 1 (s 1 ) ≤ ν + h 1 (t 1 ) for two consecutive states s 1 and t 1 , and the leaf value ν added to g 1 (t 1 ) = g 1 (s 1 ) + ν. This proof is analogous to the proof of Theorem 2 in the main paper.
We use the fact that h 1 is a consistent heuristic with respect to the minimization of T 1 (x 1 ) (h 1 (s 1 ) ≤ ν 1 + h 1 (t 1 )) and h 2 is a consistent heuristic with respect to the maximization of T 2 (x 2 ) (h 2 (s 2 ) ≥ ν 2 + h 2 (t 2 )).

A.2 Experiments
Dataset Details We used the following datasets in our experiments.
• Allstate: an insurance claim dataset available from https: //www.kaggle.com/c/allstate-claims-severity with 116 categorical and 14 numerical features and 188k rows. Each row describes an insurance claim, and the target variable is a continuous loss.
• California housing: a well-known dataset available from https://github.com/ageron/handson-ml/tree/master/ datasets/housing with 10 attributes and 20k rows. The task is to predict the median income of a census block.
• Covertype: a forestry dataset available from https: //archive.ics.uci.edu/ml/datasets/covertype with 54 attributes and 581k rows. The task is to predict one out of seven forest cover types. We turned it into a balanced binary classification task by predicting class 2 versus all.
• Higgs: a high energy physics dataset available from https: //www.kaggle.com/c/higgs-boson/data. There are multiple versions of this dataset; we used the version from Kaggle. It has 33 attributes and 250k rows. The task is to classify whether the rows represents a decaying Higgs boson or not.
• YouTube: a dataset derived from the collection of trending videos available from https://www.kaggle.com/ datasnaek/youtube-new (US, UK and CA only). We trained on a bag-of-words representation of the text in the title and the description of the video. The target is the log of the total number of views of the video. The 330 binary attributes represent the presence of individual words (no n-grams) for 120k videos. • Soccer: This is the only non-public dataset. The data can be purchased from providers like Opta. We used two consecutive ball actions described by their x and y coordinates on the pitch, and the two corresponding action types as the input data. The target is to predict whether a goal occurs within the next 10 actions. We obtained a model by following the steps at https://github.com/ML-KULeuven/socceraction.

A.3 Experiment Parameters
We use the default XGBoost parameters with the exception of number of trees, tree depth, and learning rate. The learning rate is always determined using hyper-parameter optimization given an ensemble size and a tree depth. We train models with learning rates 0.1, 0.2, 0.3, . . . , 0.9, 1.0, pick the best value r, and then again train models with learning rates r − 0.08, r − 0.06, . . . , r + 0.06, r + 0.08. We use the value with the best predictive performance on the test set. The number of trees and tree depth parameters are either varied (stress test and random verification tasks experiment), or provided in the main paper (robustness experiment and the two use cases).
In the robustness experiment, we used a timeout of 10 seconds for both VERITAS and MERGE perb calculation. The memory limit was set to 4Gb for both methods. In the stress test experiment, we used a timeout of 120 seconds and a memory limit of 4Gb. In the random verification task experiment, we used a timeout of 30 seconds and memory limit of 4Gb. For the last two use cases, we used 30 and 10 seconds for the YouTube and soccer tasks respectively, with again a memory limit of 4Gb.
A.4 Additional Results for Stress Test Figure 6 shows the results for the stress test experiment for all datasets.

A.5 Extended Results for Random Verification Task Experiment
Tables 2 and 3 contain the same results as in the main paper but the results are split up per ensemble size and tree depth respectively. Both ensemble size and tree depth positively correlate with the relative gap size. Unsurprisingly, smaller ensembles with shallower trees are easier to verify. The run time performance is fairly consistent across model sizes.   Table 3: Results for randomly generated problems per tree depth for Allstate (A), California housing (CH), Covertype (CT), and Higgs (H). Tree depths are 3, 4, 5, 6, 7, and 8. Each row summarizes 360 random problems. The second and third column show how often a problem is solved exactly by the two methods. The gap ((b−b)/b) columns show the relative gap distributions. The bars show the fraction of cases where the gap is <1% (blue), up to 20%, 50%, 100%, and >100%. A smaller gap is better. The TTB histogram shows the fraction of cases where VERITAS is slower (first bar), or faster by a factor of up to 10, 100, 1000, and >1000 (next 4 green bars).