ABSTRACT. Machine Learning approaches have been successfully used for the creation of high performance control components of cyber-physical systems, where the control dynamics results from the combination of many subsystems. However, these approaches may lack the explainability required to guarantee their reliable application in 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 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.

ABSTRACT. The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Network Controlled Systems (NNCS) persists. This paper introduces a novel approach to NNCS safety verification, leveraging the inductive invariant method. Verifying the inductiveness of a candidate inductive invariant in the context of NNCS is hard because of the scale and nonlinearity of neural networks. Our compositional method makes this verification process manageable by decomposing the inductiveness proof obligation into smaller, more tractable subproblems. Alongside the high-level method, we present an algorithm capable of automatically verifying the inductiveness of given candidates by automatically inferring the necessary decomposition predicates. The algorithm significantly outperforms the baseline method and shows remarkable reductions in execution time in our case studies, shortening the verification time from hours (or timeout) to seconds.

ABSTRACT. We consider the problem of approximate conformance checking on deep neural networks. More precisely, given two neural networks and a conformance bound ε, we need to check if the neural network outputs are within ε given the same inputs from the input set. Our approach reduces the approximate conformance checking problem to a reachability analysis problem using transformations of neural networks. We provide experimental comparison of ε-conformance checking based on our approach using various reachability analysis tools as well as other alternate ε-conformance checking algorithms. We illustrate the benefits of our approach as well as identify reachability analysis tools that are conducive for conformance checking.