Formal Synthesis of Neural Barrier Certificates for Continuous Systems via Counterexample Guided Learning

This paper presents a novel approach to safety verification based on neural barrier certificates synthesis for continuous dynamical systems. We construct the synthesis framework as an inductive loop between a Learner and a Verifier based on barrier certificate learning and counterexample guidance. Compared with the counterexample-guided verification method based on the SMT solver, we design and learn neural barrier functions with special structure, and use the special form to convert the counterexample generation into a polynomial optimization problem for obtaining the optimal counterexample. In the verification phase, the task of identifying the real barrier certificate can be tackled by solving the Linear Matrix Inequalities (LMI) feasibility problem, which is efficient and makes the proposed method formally sound. The experimental results demonstrate that our approach is more effective and practical than the traditional SOS-based barrier certificates synthesis and the state-of-the-art neural barrier certificates learning approach.