Title:	Formal Verification of Machine Learning Models: A Comparative Tool Study
DNr:	LiU-compute-2020-5
Project Type:	LiU Compute
Principal Investigator:	John Törnblom <john.tornblom@liu.se>
Affiliation:	Linköpings universitet
Duration:	2020-03-04 – 2020-06-01
Classification:	10201
Homepage:	https://liu.se/en/article/verifikation-av-larande-mjukvara-for-sakerhetskritiska-system
Keywords:

Abstract

In this project, we validate the correctness of formal verification tools for tree ensembles, developed by independent researchers. In particular, we compare the two tools Silva and VoTE, both capable of quantifying the robustness of tree ensembles against additive input perturbations. Both tools implement the theory of abstract interpretation, but with slight differences in search heuristics, yielding different performance metrics depending on the problem instance subject to verification. More interestingly, our comparison unveil differences in quantified robustness, resulting in the discovery of bugs in both tools, thus demonstrating the importance of independent implementations of formal verification tools.