Provably safe neural network controllers via differential dynamic logic

While neural networks (NNs) have potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of NN based control systems (NNCSs) poses significant challenges for the practical use of NNs, especially when safety is needed for unbounded time horizons. One reason is the intractability of analyzing NNs, ODEs and hybrid systems. To this end, the paper introduces VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The first general approach that allows reusing control theory results for NNCS verification. By joining forces, the approach exploits the efficiency of NN verification (NNV) tools while retaining the rigor of differential dynamic logic (dL), a program logic allowing the proof of infinite-time safety for abstract, nondeterministic control strategies. Based on provably safe control envelopes in dL, the paper derives specifications for the NN which is proven via NN verification. A proof of the NN adhering to the specification is mirrored by a dL proof on the infinite-time safety of the NNCS. The NN verification properties resulting from hybrid systems typically contain nonlinear arithmetic and arbitrary logical structures while efficient NN verification merely supports linear constraints. To overcome this divide, the paper presents Mosaic: An efficient, sound and complete verification approach for polynomial real arithmetic properties on piece-wise linear NNs. Mosaic partitions complex verification queries into simple queries and lifts off-the-shelf linear constraint tools to the nonlinear setting in a completeness-preserving manner by combining approximation with exact reasoning for counterexample regions. The evaluation demonstrates the versatility of VerSAILLE and Mosaic: The approach proves infinite-time safety on the classical Vertical Airborne Collision Avoidance NNCS verification benchmark for two scenarios while (exhaustively) enumerating counterexample regions in unsafe scenarios. The approach also significantly outperforms State-of-the-Art tools in closed-loop NNV. The results underscore the categorical difference of the approach to closed-loop neural network verification techniques, opening the door for developing goal-oriented and infinite-time horizon safe NNCSs in the real world. Mosaic may be of interest even beyond VerSAILLE, since nonlinear open-loop neural network verification is also required in other contexts, for example neural barrier certificate verification.