Formally Verified Neural Network Control Barrier Certificates for Unknown Systems

This paper is concerned with the controller synthesis problem for discrete-time unknown systems against safety specifications via control barrier certificates. Typically, control barrier certificates provide sufficient conditions for the satisfaction of safety specifications by separating the safe and unsafe regions of the system. By synthesizing these certificates in conjunction with control policies, one is able to keep the system safe. In our work, we parameterize the control barrier certificates and corresponding control policies as neural networks and learn them simultaneously by utilizing finitely many data samples obtained from the unknown system. We derive a so-called validity condition to formally verify the obtained certificates and integrate this condition within the training framework to achieve provably correct guarantees at the end of training time. In particular, we exploit Lipschitz continuity properties of the neural networks and utilize robust training techniques to ensure that the trained networks not only satisfy the required control barrier certificate conditions across the finitely many training data samples but over the entire state set. We then demonstrate the effectiveness of our approach with the help of a case study.