Originality: The robustness verification methods presented in the paper is new and interesting. The authors provided a fair list of related work and compared the existing methods with their method in the experiment section. Quality: The paper provides a complete presentation of three verification methods, 1) verifying the robustness of a single decision tree, 2) verifying the robustness of a tree ensemble using existing algorithms for finding k-cliques, and 3) a fast and approximate method for estimating a lower bound on the robustness. The theoretical claims and their proofs make sense to me. Overall the empirical evaluation is well designed and convincing. I only have two questions: 1. What are the ensemble sizes for the models trained on the datasets presented in Table 1 and 2? 2. How much does the parameters T and L effect the running time? Clarity: This paper is well written and well organized. The authors did a good work on describing the objective of their method, and provided a fair amount of introduction on the background and related work. It would be desirable if the authors consider releasing the source code of their method, which is not provided with this submission (though pseudo code is provided in the appendix). Significance: The robustness of the tree models are attracting increasing attention due to their popularity in the real-world applications. This paper presents an effective method for quantifying the robustness of tree ensembles. Empirical evaluation shows that the proposed method can provide evaluation in seconds per example, which is often order of magnitude faster than the existing methods. Overall I think this paper is valuable for the practitioner for evaluating the robustness of the tree ensembles. --- Update: The authors clarified my questions. I also found the answer to measuring the feature importance (a question from Reviewer #2) could be a very good addition to the text. Overall, I maintain my original assessment that this is a good submission.

Novelty: The theoretical results and the algorithm are new, and it's clear how they are different from the related work cited in the paper. It's also nice that they reduced this problem to a well-studied one. Quality: Overall, the paper is well put together, in that it presents a problem that was recognized as important, followed by a formalization and solution in a simple case, then the main theoretical result which appears to be sound, then a pertinent algorithm which provides fast solutions, and finally an evaluation of this algorithm in terms of speed and minimal adversarial perturbation. That the procedure can also be used to find features that are unimportant and 'immune' to perturbation is also a point it its favour, tough wouldn't we just be able to identify these by calculating variable importance in a forest? There is one point that I'm not convinced about: the authors rely on the conclusion by previous work that adversarial attacks can have a significant influence on model performance (references 8,12,18). [12] introduces a new type of attack, which as far as I can tell does not affect the results in this paper. However, [8] and [18] introduce methods for strengthening ensembles against adversarial perturbations. How do the bounds hold if these methods are applied instead of standard trees, which is the case for any application where adversarial attacks are expected? The algorithm is applied on [8] (robust GBDT) which is the more recent work. It does seem to be the case that the bounds are much closer to the MILP ones in this case (Fig 2 right). Clarity: The paper is clear and well organized. The main paper introduces enough information for an implementation of the algorithm, but the appendix would be needed to actually replicate the results. Update following the author response: The authors answered my comments. I liked the feature importance example - perhaps it could be included in the appendix?

This paper studied the robustness verification problem for tree-based model. Although formal robustness verification is NP-complete, they give a more precise complexity characterization. For general problems, by exploiting the boxicity of the graph, they develop an efficient multi-level verification algorithm. The idea is novel and interesting. The proposed algorithm can give tight lower bounds on robustness of decision tree ensembles, while allowing iterative improvement and any-time termination. Experiments on 10 datasets show the superior performance of the proposed method. This paper is well written and easy to follow.