Safe Reinforcement Learning for NN-Controlled Systems with Neural Barrier Certificate Guidance

Safe controller synthesis is crucial for safety-critical applications. This article presents a novel reinforcement learning (RL) approach to synthesize safe controllers for neural network (NN)-controlled systems. The core idea leverages an iterative scheme that combines controller learning with neural barrier certificate (BC) verification, ultimately producing a provably safe deep neural network (DNN) controller with formal safety guarantees. The process begins by pretraining a well-performing DNN controller as an 'oracle' via deep RL (DRL). To formally verify the safety properties of the closed-loop system under the base controller, we devise a formal verification procedure that approximates the DNN controller using polynomial inclusion, followed by synthesizing neural BCs via sum-of-squares (SOS) relaxation. In cases where the base controller is insufficient to yield a real BC, the current spurious BC is incorporated as an additional penalty term to reshape the RL reward function, guiding the iterative refinement for new controllers. We implement an automated tool, neural BC-guided safe RL NBCRL, and experimental results demonstrate the benefits of our method in terms of efficiency and scalability even for a nonlinear system with a dimension up to 12.