# Versatile Verification of Tree Ensembles

arXiv: https://arxiv.org/abs/2010.13880 · HTML: https://mlsanity.com/paper/2010.13880/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Oct 2020.

## Built on by (most cited first, 12 of 12)

- [Machine Learning with a Reject Option: A survey](https://mlsanity.com/paper/2107.11277/) (2021)
- [On the Safety of Interpretable Machine Learning: A Maximum Deviation Approach](https://mlsanity.com/paper/2211.01498/) (2022)
- [Beyond Discriminant Patterns: On the Robustness of Decision Rule Ensembles](https://mlsanity.com/paper/2109.10432/) (2021)
- [SaDe: Learning Models that Provably Satisfy Domain Constraints](https://mlsanity.com/paper/2112.00552/) (2021)
- [Data-Aware and Scalable Sensitivity Analysis for Decision Tree Ensembles](https://mlsanity.com/paper/2602.07453/) (2026)
- [Faster Repeated Evasion Attacks in Tree Ensembles](https://mlsanity.com/paper/2402.08586/) (2024)
- [Adversarial Example Detection in Deployed Tree Ensembles](https://mlsanity.com/paper/2206.13083/) (2022)
- [Pruning-Based Extraction of Descriptions from Probabilistic Circuits](https://mlsanity.com/paper/2311.13379/) (2023)
- [Probabilistic ML Verification via Weighted Model Integration](https://mlsanity.com/paper/2402.04892/) (2024)
- [Formal verification of tree-based machine learning models for lateral spreading](https://mlsanity.com/paper/2603.16983/) (2026)
- [Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approach](https://mlsanity.com/paper/2605.13830/) (2026)
- [PINE: Pruning Boosted Tree Ensembles with Conformal In-Distribution Prediction Equivalence](https://mlsanity.com/paper/2605.28068/) (2026)

## Abstract (arXiv)

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.