RECORD
Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles
Machine Learning · Submitted 6 May 2021
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim 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.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
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.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | 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. | background 1.00 | 0.04 | 0.03 | asserted 0.96 |
| s1 | 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. | background 0.89 | 0.05 | 0.03 | asserted 0.96 |
| s2 | 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. | contribution 0.99 | 0.93 | 0.08 | asserted 0.99 |
| s3 | 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. | contribution 0.71 | 0.95 | 0.51 | asserted 1.00 |
| s4 | 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. | contribution 0.61 | 0.95 | 0.11 | asserted 1.00 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
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.
Human review
References
How the literature uses it
1 arXiv paper cite this in 1 sentence
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.