Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates

TL;DR

This work tackles the challenge of formally verifying DRL-controlled dynamical systems by introducing Neural Lyapunov Barrier (NLB) certificates and two scalability-enhancing techniques: certificate filtering (FRWA) and compositional certificates (CRWA). It combines NLB-based guarantees with off-the-shelf DNN verification engines through a counterexample-guided inductive synthesis (CEGIS) loop, enabling simultaneous safety and liveness (reach-while-avoid) guarantees for complex tasks. The authors demonstrate significant scalability gains on a 2D spacecraft docking case, showing that FRWA outperforms standard RWA approaches and that CRWA enables verification over substantially larger state spaces. Collectively, the approach facilitates safe, verifiable deployment of DRL controllers in real-world, safety-critical settings by providing rigorous, verifiable certificates that co-operate with neural controllers.

Abstract

Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the ``black box'' nature of DRL agents limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent's behavior is to use Neural Lyapunov Barrier (NLB) certificates, which are learned functions over the system whose properties indirectly imply that an agent behaves as desired. However, NLB-based certificates are typically difficult to learn and even more difficult to verify, especially for complex systems. In this work, we present a novel method for training and verifying NLB-based certificates for discrete-time systems. Specifically, we introduce a technique for certificate composition, which simplifies the verification of highly-complex systems by strategically designing a sequence of certificates. When jointly verified with neural network verification engines, these certificates provide a formal guarantee that a DRL agent both achieves its goals and avoids unsafe behavior. Furthermore, we introduce a technique for certificate filtering, which significantly simplifies the process of producing formally verified certificates. We demonstrate the merits of our approach with a case study on providing safety and liveness guarantees for a DRL-controlled spacecraft.

Figures (9)

• Figure 1: The CEGIS Loop used to iteratively train and verify controller $\pi\xspace$ and certificate $V$. Verification counterexamples are used to augment the training dataset.
• Figure 2: Visualization of how consecutive certificates relate when building a CRWA certificate. Note that $\mathcal{X}\xspace_G$ need not be a subset of $\mathcal{X}\xspace_I$. The dotted lines indicate that the unsafe state region extends infinitely outside the solid line box. Wavy lines indicate outer boundaries for initial or goal regions.
• Figure 3: A spiral trajectory: The DRL-controlled spacecraft (starting from the red point) eventually reaches the destination (orange) point within the docking region.
• Figure 4: The first 2 rows show average times and success rates for creating verified certificates over 5 trials. The bottom 2 rows show specific times for each trial, separated into failed ("F-") and verified ("V-") certificates. CFRWA-1, CFRWA-2, and CFRWA-3 refer to the first (up to) three CRWA tasks for the given starting region, corresponding, respectively to the first (up to) three rows for that starting region in Table \ref{['table:compositionalFRWA']}.
• Figure 5: A scheme of the DNN controller architecture for the 2D docking benchmark. Given an input state of the system, $\boldsymbol{x} = [x_{t}, y_{t}, \dot{x_{t}}, \dot{y_{t}}]^T$, the DNN outputs the forces $[F_x,F_y]$, which are converted using dynamics $f$ to produce the next state. The states generated in this trajectory pertain to the deputy spacecraft, which attempts to safely maneuver into close proximity of a chief spacecraft.

Theorems & Definitions (5)

• definition 1: Reach-while-Avoid Task
• Lemma 1
• Lemma 2
• Lemma 1
• Lemma 2