Formal Synthesis of Certifiably Robust Neural Lyapunov-Barrier Certificates
This work addresses the reliability of safety-critical autonomous systems by providing robust certificates against dynamics uncertainties, representing an incremental advance over existing methods.
The paper tackles the problem of synthesizing robust neural Lyapunov-barrier certificates to verify safety and stability in deep reinforcement learning controllers under perturbed dynamics, achieving up to 4.6 times improvement in certified robustness bounds and up to 2.4 times better empirical success rates compared to baselines.
Neural Lyapunov and barrier certificates have recently been used as powerful tools for verifying the safety and stability properties of deep reinforcement learning (RL) controllers. However, existing methods offer guarantees only under fixed ideal unperturbed dynamics, limiting their reliability in real-world applications where dynamics may deviate due to uncertainties. In this work, we study the problem of synthesizing \emph{robust neural Lyapunov barrier certificates} that maintain their guarantees under perturbations in system dynamics. We formally define a robust Lyapunov barrier function and specify sufficient conditions based on Lipschitz continuity that ensure robustness against bounded perturbations. We propose practical training objectives that enforce these conditions via adversarial training, Lipschitz neighborhood bound, and global Lipschitz regularization. We validate our approach in two practically relevant environments, Inverted Pendulum and 2D Docking. The former is a widely studied benchmark, while the latter is a safety-critical task in autonomous systems. We show that our methods significantly improve both certified robustness bounds (up to $4.6$ times) and empirical success rates under strong perturbations (up to $2.4$ times) compared to the baseline. Our results demonstrate effectiveness of training robust neural certificates for safe RL under perturbations in dynamics.