Towards Formal Verification of Neural Networks in Cyber-Physical Systems

Machine Learning approaches have been successfully used for the creation of high-performance control components of cyber-physical systems, where the control dynamics result from the combination of many subsystems. However, these approaches may lack the trustworthiness required to guarantee their reliable application in a safety-critical context. In this paper, we propose an approach to automatically translate entire feed-forward fully-connected neural networks into first-order logic formal models that can be used to analyse the prediction of the network. The approach exploits the Prototype Verification System theorem prover to model neural networks based on non-linear activation functions and prove the safety bounds of the output under safety-critical conditions. Finally, we show the application of the proposed approach to a model-predictive controller for autonomous driving.