Synthesizing Barrier Certificates Using Neural Networks

This paper presents an approach of safety verification based on neural networks for continuous dynamical systems which are modeled as a system of ordinary differential equations. We adopt the deductive verification methods based on barrier certificates. These are functions over the states of the dynamical system with certain constraints the existence of which entails the safety of the system under consideration. We propose to represent the barrier function by neural networks and provide a comprehensive synthesis framework. In particular, we devise a new type of activation functions, i.e., Bent-ReLU, for the neural networks; we provide sampling based approaches to generate training sets and formulate the loss functions for neural network training which can capture the essence of barrier certificate; we also present practical methods to check a learnt candidate barrier certificate against the criteria of barrier certificates as a formal guarantee. We implement our approaches via proof-of-concept experiments with encouraging results.