mlsanityData to 14 Oct 2026

Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates

arXiv 2405.14058 ↗First posted 22 May 2024cs.AI cs.LG cs.SYcited by 16

On the map: Deep reinforcement learning methods → Safe and constrained RL

Abstract (arXiv)

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.

Key facts. Cited by 16 papers in the map (data through 14 Oct 2026). Placed in Safe and constrained RL, one of 15 directions in Deep reinforcement learning methods. Builds on 56 of its 99 references that are in the map. First posted on arXiv 22 May 2024.

Builds on

56 of 99 references.

References · 56

  1. 2013Playing Atari with Deep Reinforcement Learningcited by 3,274
  2. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
  3. 2017Safe Reinforcement Learning via Shieldingcited by 449
  4. 2019Control Barrier Functions: Theory and Applicationscited by 372
  5. 2021Safe Learning in Robotics: From Learning-Based Control to Safe Reinforcement Learningcited by 371
  6. 2018A Lyapunov-based Approach to Safe Reinforcement Learningcited by 297
  7. 2016Control Barrier Function Based Quadratic Programs for Safety Critical Systemscited by 287
  8. 2017Hamilton-Jacobi Reachability: A Brief Overview and Recent Advancescited by 201
  9. 2022Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methodscited by 151
  10. 2020Neural Lyapunov Controlcited by 142
  11. 2021Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functionscited by 94
  12. 2018The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systemscited by 88
38 more
  1. 2024Marabou 2.0: A Versatile Formal Analyzer of Neural Networkscited by 81
  2. 2021Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificatescited by 74
  3. 2020Reinforcement Learning for Safety-Critical Control under Model Uncertainty, using Control Lyapunov Functions and Control Barrier Functionscited by 68
  4. 2022Reachability Constrained Reinforcement Learningcited by 59
  5. 2021Safety and Liveness Guarantees through Reach-Avoid Reinforcement Learningcited by 49
  6. 2020An SMT-Based Approach for Verifying Binarized Neural Networkscited by 47
  7. 2020Learning Stability Certificates from Datacited by 45
  8. 2014Reach-Avoid Problems with Time-Varying Dynamics, Targets and Constraintscited by 44
  9. 2015Shield Synthesis: Runtime Enforcement for Reactive Systemscited by 42
  10. 2022Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guaranteescited by 40
  11. 2019Fastened CROWN: Tightened Neural Network Robustness Certificatescited by 39
  12. 2021OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systemscited by 38
  13. 2023The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Resultscited by 38
  14. 2023Iterative Reachability Estimation for Safe Reinforcement Learningcited by 37
  15. 2021Neural Network Robustness as a Verification Property: A Principled Case Studycited by 35
  16. 2021Stabilizing Neural Control Using Self-Learned Almost Lyapunov Criticscited by 35
  17. 2021Towards Scalable Verification of Deep Reinforcement Learningcited by 33
  18. 2022Verifying Learning-Based Robotic Navigation Systemscited by 33
  19. 2016Robustness of Control Barrier Functions for Safety Critical Controlcited by 30
  20. 2016Funnel Libraries for Real-Time Robust Feedback Motion Planningcited by 29
  21. 2023Solving Stabilize-Avoid Optimal Control via Epigraph Form and Deep Reinforcement Learningcited by 24
  22. 2023Formally Explaining Neural Networks within Reactive Systemscited by 24
  23. 2023Neural Lyapunov Control for Discrete-Time Systemscited by 23
  24. 2021Pruning and Slicing Neural Networks using Formal Verificationcited by 20
  25. 2019Exploring applications of deep reinforcement learning for real-world autonomous driving systemscited by 18
  26. 2020Adaptive Shielding under Uncertaintycited by 18
  27. 2022Verification-Aided Deep Ensemble Selectioncited by 18
  28. 2022Enforcing safety for vision-based controllers via Control Barrier Functions and Neural Radiance Fieldscited by 16
  29. 2023Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Modelscited by 15
  30. 2021Minimal Multi-Layer Modifications of Deep Neural Networkscited by 14
  31. 2023Exact Verification of ReLU Neural Control Barrier Functionscited by 14
  32. 2022veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection Systemcited by 12
  33. 2022Constrained Reinforcement Learning for Robotics via Scenario-Based Programmingcited by 11
  34. 2023Verifying Generalization in Deep Learningcited by 11
  35. 2020Automated and Sound Synthesis of Lyapunov Functions with SMT Solverscited by 10
  36. 2022Quantifying Safety of Learning-based Self-Driving Control Using Almost-Barrier Functionscited by 10
  37. 2023Learning Stabilization Control from Observations by Learning Lyapunov-like Proxy Modelscited by 10
  38. 2023Sequential Neural Barriers for Scalable Dynamic Obstacle Avoidancecited by 9

50 most cited of 56 All 56 (JSON)

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2024: 5; 2025: 5; 2026: 6.

16 papers.

Sort:

By area:

  1. 2024Verification-Guided Shielding for Deep Reinforcement Learningcited by 13
  2. 2024Shield Synthesis for LTL Modulo Theoriescited by 12
  3. 2025Neural Network Verification is a Programming Language Challengecited by 12
  4. 2024Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretationcited by 11
  5. 2024Neural Continuous-Time Supermartingale Certificatescited by 5
  6. 2024Safe and Reliable Training of Learning-Based Aerospace Controllerscited by 4
  7. 2025A Review On Safe Reinforcement Learning Using Lyapunov and Barrier Functionscited by 4
  8. 2026Incremental Neural Network Verification via Learned Conflictscited by 2
  9. 2025Proof-Carrying Neuro-Symbolic Codecited by 1
  10. 2025Formal Verification of Neural Certificates Done Dynamicallycited by 1
  11. 2026The FABRIC Strategy for Verifying Neural Feedback Systemscited by 1
  12. 2025On Improving Deep Active Learning with Formal Verificationcited by 0
4 more
  1. 2026A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systemscited by 0
  2. 2026Formal Synthesis of Certifiably Robust Neural Lyapunov-Barrier Certificatescited by 0
  3. 2026Neural Network Verification using Partial Multi-Neuron Relaxationcited by 0
  4. 2026Mining Verdict Boundaries for Neural Network Verificationcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2024Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
  2. 2026Scenario Generation for Risk-Aware Reinforcement Learning with Probably Approximately Safe Guarantees
  3. 2020Safety Considerations in Deep Control Policies with Safety Barrier Certificates Under Uncertainty
  4. 2025Scalable Synthesis and Verification of String Stable Neural Certificates for Interconnected Systems ↗
  5. 2025BarrierBench: Evaluating Large Language Models for Safety Verification in Dynamical Systems
  6. 2022Deep Binary Reinforcement Learning for Scalable Verification
  7. 2024Verified Safe Reinforcement Learning for Neural Network Dynamic Models
  8. 2024Learning-Based Shielding for Safe Autonomy under Unknown Dynamics