Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
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.
Code (1)
Tasks
Deep Reinforcement Learningreinforcement-learningReinforcement LearningSimilar Papers 제목 키워드 기반
Formal Synthesis of Certifiably Robust Neural Lyapunov-Barrier Certificates
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 guaran…
Reinforcement LearningSafe and Reliable Training of Learning-Based Aerospace Controllers
In recent years, deep reinforcement learning (DRL) approaches have generated highly successful controllers for a myriad of complex domains. However, the opaque nature of these models limits their applicability in aerospa…
Deep Reinforcement LearningJoint Differentiable Optimization and Verification for Certified Reinforcement Learning
In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties (e.g., safety, stability) under the learned controller. However, as existing methods typica…
Bilevel OptimizationModel-based Reinforcement Learningreinforcement-learningReinforcement Learning+1Greedy Synthesis of Event- and Self-Triggered Controls with Control Lyapunov-Barrier Function
This paper addresses the co-design problem of control inputs and execution decisions for event- and self-triggered controls subject to constraints given by the control Lyapunov function and control barrier function. The …
Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions
Safety and stability are common requirements for robotic control systems; however, designing safe, stable controllers remains difficult for nonlinear and uncertain models. We develop a model-based learning approach to sy…