Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles

TL;DR

This paper formalizes and extends a scalable verification tool for tree ensembles, demonstrating its effectiveness in verifying robustness properties in safety-critical machine learning applications through case studies.

Contribution

It introduces mechanisms for systematic scalability analysis and shows how property checking can be separated from core verification, enabling verification of diverse requirements.

Findings

The tool scales well in time and memory usage.

Separation of property checking enhances versatility.

The algorithm is highly parallelizable.

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.