Safety Certification for Stochastic Systems via Neural Barrier Functions

Providing non-trivial certificates of safety for non-linear stochastic systems is an important open problem. One promising solution to address this problem is the use of barrier functions. Barrier functions are functions whose composition with the system forms a Martingale and enable the computation of the probability that the system stays within a safe set over a finite time horizon. However, existing approaches to find barrier functions generally restrict the search to a small class of functions, often leading to conservatism. To address this problem, in this letter, we parameterize barrier functions as neural networks and show that bound propagation techniques and linear programming can be successfully employed to find Neural Barrier Functions. Further, we develop a branch-and-bound scheme based on linear relaxations that improves the scalability of the proposed framework. On several case studies we show that our approach scales to neural networks of hundreds of neurons and multiple hidden layers and often produces certificates of safety that are tighter than state-of-the-art methods.