Formal Verification of Machine Learning Models: A Comparative Tool Study
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.