Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates

• URL: http://arxiv.org/abs/2405.14058v2
• Date: Wed, 14 Aug 2024 18:45:17 GMT
• Title: Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
• Authors: Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, Clark Barrett,
• Abstract summary: 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. We demonstrate the merits of our approach with a case study on providing safety and liveness guarantees for a DRL-controlled spacecraft.
• Score: 2.0611129932396164
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems [0.5249805590164903]
  The KI-LOK project explores new methods for certifying and safely integrating AI components into autonomous trains. We pursue a two-layered approach: (1) ensuring the safety of the steering system by formal analysis using the B method, and (2) improving the reliability of the perception system with a runtime certificate checker. This work links both strategies within a demonstrator that runs simulations on the formal model, controlled by the real AI output and the real certificate checker.
  arXiv  Detail & Related papers  (2024-11-21T18:09:04Z)
• Transfer of Safety Controllers Through Learning Deep Inverse Dynamics Model [4.7962647777554634]
  Control barrier certificates have proven effective in formally guaranteeing the safety of the control systems. Design of a control barrier certificate is a time-consuming and computationally expensive endeavor. We propose a validity condition that, when met, guarantees correctness of the controller.
  arXiv  Detail & Related papers  (2024-05-22T15:28:43Z)
• Safe Online Dynamics Learning with Initially Unknown Models and Infeasible Safety Certificates [45.72598064481916]
  This paper considers a learning-based setting with a robust safety certificate based on a control barrier function (CBF) second-order cone program. If the control barrier function certificate is feasible, our approach leverages it to guarantee safety. Otherwise, our method explores the system dynamics to collect data and recover the feasibility of the control barrier function constraint.
  arXiv  Detail & Related papers  (2023-11-03T14:23:57Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Approximate Model-Based Shielding for Safe Reinforcement Learning [83.55437924143615]
  We propose a principled look-ahead shielding algorithm for verifying the performance of learned RL policies. Our algorithm differs from other shielding approaches in that it does not require prior knowledge of the safety-relevant dynamics of the system. We demonstrate superior performance to other safety-aware approaches on a set of Atari games with state-dependent safety-labels.
  arXiv  Detail & Related papers  (2023-07-27T15:19:45Z)
• Value Functions are Control Barrier Functions: Verification of Safe Policies using Control Theory [46.85103495283037]
  We propose a new approach to apply verification methods from control theory to learned value functions. We formalize original theorems that establish links between value functions and control barrier functions. Our work marks a significant step towards a formal framework for the general, scalable, and verifiable design of RL-based control systems.
  arXiv  Detail & Related papers  (2023-06-06T21:41:31Z)
• COPA: Certifying Robust Policies for Offline Reinforcement Learning against Poisoning Attacks [49.15885037760725]
  We focus on certifying the robustness of offline reinforcement learning (RL) in the presence of poisoning attacks. We propose the first certification framework, COPA, to certify the number of poisoning trajectories that can be tolerated. We prove that some of the proposed certification methods are theoretically tight and some are NP-Complete problems.
  arXiv  Detail & Related papers  (2022-03-16T05:02:47Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)
• CRFL: Certifiably Robust Federated Learning against Backdoor Attacks [59.61565692464579]
  This paper provides the first general framework, Certifiably Robust Federated Learning (CRFL), to train certifiably robust FL models against backdoors. Our method exploits clipping and smoothing on model parameters to control the global model smoothness, which yields a sample-wise robustness certification on backdoors with limited magnitude.
  arXiv  Detail & Related papers  (2021-06-15T16:50:54Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.