Are Formal Methods Applicable To Machine Learning And Artificial Intelligence?

Formal approaches can provide strict correctness guarantees for the development of both hardware and software systems. In this work, we examine state-of-the-art formal methods for the verification and validation of machine learning systems in particular. We first provide a brief summary of existing formal approaches in general. After that, we report on formal methods developed for validating data preparation and training phases. Then, we go over the formal methods used for the verification of machine learning systems. At this level, we consider both partial and exhaustive techniques. In addition, we review research works dedicated to the verification of support vector machines and decision tree ensembles. Finally, we propose several potential future directions for formal verification of machine learning systems.