VoTE (Verifier of Tree Ensembles)

VoTE (Verifier of Tree Ensembles) is a toolsuite for analyzing input/output mappings of decision trees and tree ensembles. VoTE consists of two distinct type of components, VoTE Core and VoTE Property Checker. VoTE Core takes as input a tree ensemble with corresponding input domain, and emits a sequence of equivalence classes, i.e. sets of points in the input domain that yield the same output. These equivalence classes are then processed by a VoTE Property Checker that checks that all input/output mappings captured by an equivalence class complies with some requirement.

For more information, see related publications.

Building

On Debian-flavored operating systems (tested with Debian 11.1), you can invoke the following commands to install dependencies, generate makefiles, and compile the source code.

john@localhost:VoTE$ sudo apt-get install autoconf libtool build-essential
john@localhost:VoTE$ sudo apt-get install python3-cffi python3-setuptools python3-dev
john@localhost:VoTE$ ./bootstrap.sh
john@localhost:VoTE$ ./configure
john@localhost:VoTE$ make

VoTE includes Python bindings for easy prototyping and testing of domain-specific property checkers. See example.py for a simple example. To invoke a test suite for the python bindings, run the following command:

john@localhost:VoTE$ sudo apt-get install python3-sklearn python3-xgboost python3-pip
john@localhost:VoTE$ python3 -m pip install catboost --user
john@localhost:VoTE$ python3 bindings/python/setup.py test

Running Case Studies

VoTE also includes example case studies that use scikit-learn and catboost to train tree ensembles, and VoTE to verify requirements. To run a collision detection verification case study, invoke the following command:

john@localhost:VoTE$ ./support/collision_detection.sh

Reporting Bugs

If you encounter problems with VoTE, please file a github issue. If you plan on sending pull requests which affect more than a few lines of code, please file an issue before you start to work on you changes. This will allow us to discuss the solution properly before you commit time and effort.

Related Publications

• J. Törnblom and S. Nadjm-Tehrani, Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles, arXiv preprint arXiv:1905.04194, 2021.

• J. Törnblom and S. Nadjm-Tehrani, An Abstraction-Refinement Approach to Formal Verification of Tree Ensembles, in proceedings of 2nd International workshop on Artificial Intelligence Safety Engineering, held in conjunction with SAFECOMP, Springer, 2019. DOI: 10.1007/978-3-030-26250-1_24. Available as preprint.

• J. Törnblom and S. Nadjm-Tehrani, Formal Verification of Input-Output Mappings of Tree Ensembles. in Science of Computer Programming, Special issue on Formal Techniques in Safety-critical Systems, Elsevier, 2020. DOI: 10.1016/j.scico.2020.102450. Available as preprint.

• J. Törnblom and S. Nadjm-Tehrani, Formal Verification of Random Forests in Safety-Critical Applications, in International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), Springer, 2019. DOI: 10.1007/978-3-030-12988-0_4. Available as preprint.

License

VoTE Core is licensed under the LGPLv3+, and programs linking to VoTE Core are licensed under the GPLv3+, see COPYING and COPYING.LESSER for more information. Files in the ext folder are copyrighted by external entities. In particular, VoTE Core use parson to parse JSON-persisted models. Parson is licened under the MIT license.