Formally Verifying the Robustness of Machine Learning Models : A Comparative Study

Abstract: Machine learning models have become increasingly popular in recent years, and not without reason. They enable software to become more powerful, and with less human involvement. As a consequence however, the actions of the software are hard for a human to understand and anticipate. This prohibits the use of machine learning in systems where safety has to be assured, typically using formal proofs of relevant properties. This thesis is focused on robustness - one of many properties that can impact the safety of a system. There are several tools available that enable formal robustness verification of machine learning models, and a goal of this thesis is to evaluate their performance. A variety of machine learning models are also assessed according to how robust they can be proved to be. A digit recognition problem was used in order to evaluate how sensitive different model types are to perturbations of pixels in an image, and also to assess the performance of applicable verification tools. On this particular problem, we discovered that a Support Vector Machine demonstrates the highest degree of robustness, which could be verified with short enough time using the tool SAVer. In addition, machine learning models were trained on a data set consisting of Android applications that are labelled either as malware or benign. In this verification problem, we check whether adding permission requests to an application that is malware can make it become labelled as benign. For this problem, a Gradient Boosting Machine proved to be the most robust with a very short verification time using the tool VoTE. Although not the most robust, Neural Networks were proved to be relatively robust on both problems using the tool ERAN, whereas Random Forests performed the worst, in terms of robustness.