Formal Synthesis of Certifiably Robust Neural Lyapunov-Barrier Certificates

TL;DR

This paper develops a method to synthesize neural Lyapunov and barrier certificates that are robust to system perturbations, enhancing safety and stability guarantees in reinforcement learning controllers under real-world uncertainties.

Contribution

It introduces a formal definition of robust neural Lyapunov barrier certificates and practical training methods to enforce robustness against bounded dynamics perturbations.

Findings

Significantly improves certified robustness bounds (up to 4.6x).

Increases success rates under perturbations (up to 2.4x).

Validated on Inverted Pendulum and 2D Docking environments.

Abstract

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.