# Formal Verification of Input-Output Mappings of Tree Ensembles

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 May 2019.

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

- [How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review](https://mlsanity.com/paper/2107.12045/) (2021)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Mo"ET: Mixture of Expert Trees and its Application to Verifiable Reinforcement Learning](https://mlsanity.com/paper/1906.06717/) (2019)
- [Responsible and Regulatory Conform Machine Learning for Medicine: A Survey of Challenges and Solutions](https://mlsanity.com/paper/2107.09546/) (2021)
- [Explainable Global Fairness Verification of Tree-Based Classifiers](https://mlsanity.com/paper/2209.13179/) (2022)
- [Beyond Robustness: Resilience Verification of Tree-Based Classifiers](https://mlsanity.com/paper/2112.02705/) (2021)
- [Verifiable Learning for Robust Tree Ensembles](https://mlsanity.com/paper/2305.03626/) (2023)
- [Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles](https://mlsanity.com/paper/2105.02595/) (2021)
- [Finding Minimum-Cost Explanations for Predictions made by Tree Ensembles](https://mlsanity.com/paper/2303.09271/) (2023)
- [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)
- [Verifiable Boosted Tree Ensembles](https://mlsanity.com/paper/2402.14988/) (2024)
- [Formal verification of tree-based machine learning models for lateral spreading](https://mlsanity.com/paper/2603.16983/) (2026)

## Abstract (arXiv)

Recent advances in machine learning and artificial intelligence are now being considered in safety-critical autonomous systems where software defects may cause severe harm to humans and the environment. Design organizations in these domains are currently unable to provide convincing arguments that their systems are safe to operate when machine learning algorithms are used to implement their software. In this paper, we present an efficient method to extract equivalence classes from decision trees and tree ensembles, and to formally verify that their input-output mappings comply with requirements. The idea is that, given that safety requirements can be traced to desirable properties on system input-output patterns, we can use positive verification outcomes in safety arguments. This paper presents the implementation of the method in the tool VoTE (Verifier of Tree Ensembles), and evaluates its scalability on two case studies presented in current literature. We demonstrate that our method is practical for tree ensembles trained on low-dimensional data with up to 25 decision trees and tree depths of up to 20. Our work also studies the limitations of the method with high-dimensional data and preliminarily investigates the trade-off between large number of trees and time taken for verification.