# Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 21 references that are in the map.
- First posted on arXiv 6 May 2021.

## Builds on (most cited first, 10 of 10)

- [Explainable Artificial Intelligence (XAI): Concepts, Taxonomies, Opportunities and Challenges toward Responsible AI](https://mlsanity.com/paper/1910.10045/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [A Survey on Explainable Artificial Intelligence (XAI): Towards Medical XAI](https://mlsanity.com/paper/1907.07374/) (2019)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Adversarial Robustness Toolbox v1.0.0](https://mlsanity.com/paper/1807.01069/) (2018)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1912.07084/) (2019)
- [Formal Verification of Input-Output Mappings of Tree Ensembles](https://mlsanity.com/paper/1905.04194/) (2019)
- [Verifying Robustness of Gradient Boosted Models](https://mlsanity.com/paper/1906.10991/) (2019)
- [Verifying Tree Ensembles by Reasoning about Potential Instances](https://mlsanity.com/paper/2001.11905/) (2020)

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

- [Finding Minimum-Cost Explanations for Predictions made by Tree Ensembles](https://mlsanity.com/paper/2303.09271/) (2023)
- [ReCatcher: Towards LLMs Regression Testing for Code Generation](https://mlsanity.com/paper/2507.19390/) (2025)

## Abstract (arXiv)

To guarantee that machine learning models yield outputs that are not only accurate, but also robust, recent works propose formally verifying robustness properties of machine learning models. To be applicable to realistic safety-critical systems, the used verification algorithms need to manage the combinatorial explosion resulting from vast variations in the input domain, and be able to verify correctness properties derived from versatile and domain-specific requirements. In this paper, we formalise the VoTE algorithm presented earlier as a tool description, and extend the tool set with mechanisms for systematic scalability studies. In particular, we show a) how the separation of property checking from the core verification engine enables verification of versatile requirements, b) the scalability of the tool, both in terms of time taken for verification and use of memory, and c) that the algorithm has attractive properties that lend themselves well for massive parallelisation. We demonstrate the application of the tool in two case studies, namely digit recognition and aircraft collision avoidance, where the first case study serves to assess the resource utilisation of the tool, and the second to assess the ability to verify versatile correctness properties.