Verifying Neural Network Controlled Systems Using Neural Networks

Safety verification is an essential requirement of neural network controlled systems when they are adopted in safety-critical fields. This paper proposes a novel approach to synthesizing neural networks as barrier certificates, which can provide safety guarantees for neural network controlled systems. We first propose the construction conditions of neural network barrier certificates, followed by an iterative framework to synthesize them. Each iteration trains a neural network as the candidate barrier certificate using the training datasets sampled from the neural network controlled system. After training, identifying whether the candidate barrier certificate is a real one for the neural network controlled system is transformed into a group of mixed-integer programming problems, which the numerical optimization solver solves with guaranteed results. We implement the tool NetBC and evaluate its performance over 6 practical benchmark examples. The experimental results show that NetBC is more effective and scalable than the existing polynomial barrier certificate-based method.