Neural Barrier Certificates Synthesis of NN-Controlled Continuous Systems via Counterexample-Guided Learning

Neural Barrier Certificates Synthesis of NN-Controlled Continuous Systems via Counterexample-Guided Learning

연구 분야: Verification

학회: DAC '24: Proceedings of the 61st ACM/IEEE Design Automation Conference

There is a pressing need to ensure the safety of closed-loop systems with neural network controllers, as they are often incorporated into safety-critical applications. To address this issue, we propose a novel approach for generating barrier certificates, which combines counterexample-guided learning with efficient Sum-Of-Squares (SOS) based verification. By leveraging barrier certificate candidates obtained from the learning phase, our proposed method offers an efficient verification procedure that solves three Linear Matrix Inequality (LMI) constraint feasibility testing problems, instead of relying on an SMT solver to verify the barrier certificate conditions. We conduct comparison experiments on a set of benchmarks, demonstrating the advantages of our method in terms of efficiency and scalability, which enable effective verification of high-dimensional systems.