Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
作者: 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
分类: cs.AI, cs.LG, eess.SY
发布日期: 2024-05-22 (更新: 2024-08-14)
备注: To appear in FMCAD 2024
💡 一句话要点
提出基于Lyapunov Barrier证书的深度强化学习控制器形式化验证方法，保障自主系统安全。
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)
关键词: 深度强化学习 形式化验证 Lyapunov Barrier证书 神经网络验证 自主系统
📋 核心要点
- 深度强化学习控制器在安全关键应用中部署受限，主要挑战在于其黑盒特性和缺乏形式化验证手段。
- 论文提出一种基于神经Lyapunov Barrier证书的验证方法，通过证书组合与过滤简化复杂系统验证。
- 通过航天器控制案例研究，验证了该方法在提供安全和活性保证方面的有效性，提升了系统可靠性。
📝 摘要（中文）
深度强化学习(DRL)是一种强大的机器学习范式，用于生成控制自主系统的智能体。然而，DRL智能体的“黑盒”特性限制了它们在现实世界安全关键型应用中的部署。一种有前景的方法是使用神经Lyapunov Barrier (NLB)证书，这是一种在系统上学习的函数，其属性间接意味着智能体的行为符合预期。然而，基于NLB的证书通常难以学习，更难以验证，特别是对于复杂系统。本文提出了一种新的训练和验证离散时间系统NLB证书的方法。具体来说，我们引入了一种证书组合技术，通过策略性地设计一系列证书来简化高度复杂系统的验证。当与神经网络验证引擎联合验证时，这些证书提供了形式化的保证，即DRL智能体既能实现其目标，又能避免不安全行为。此外，我们还引入了一种证书过滤技术，显著简化了生成形式化验证证书的过程。我们通过一个关于为DRL控制的航天器提供安全和活性保证的案例研究，证明了我们方法的优点。
🔬 方法详解
问题定义：深度强化学习（DRL）控制器在自主系统中的应用日益广泛，但其“黑盒”特性使得难以保证其安全性和可靠性，尤其是在安全关键型应用中。现有的验证方法，如直接验证神经网络的输出，计算复杂度高，难以扩展到复杂系统。基于Lyapunov Barrier证书的方法虽然有潜力，但证书的训练和验证过程非常困难，特别是对于复杂系统，证书的设计和验证面临挑战。
核心思路：论文的核心思路是将复杂的系统验证问题分解为一系列更简单的子问题，并为每个子问题设计相应的Lyapunov Barrier证书。通过“证书组合”技术，将这些子证书组合起来，共同证明整个系统的安全性和活性。此外，引入“证书过滤”技术，减少需要验证的证书数量，从而降低验证的计算复杂度。这种分而治之的策略使得复杂系统的形式化验证成为可能。
技术框架：该方法包含以下几个主要阶段：1) 系统建模：将待验证的自主系统建模为离散时间系统。2) 证书设计：根据系统特性和安全目标，设计一系列Lyapunov Barrier证书。3) 证书训练：使用神经网络学习这些证书。4) 证书组合：将多个证书组合成一个整体，以覆盖整个系统的状态空间。5) 证书过滤：筛选出对验证至关重要的证书，减少验证的计算量。6) 形式化验证：使用神经网络验证引擎，对组合后的证书进行形式化验证，确保其满足Lyapunov Barrier的条件。
关键创新：该方法最重要的创新点在于“证书组合”和“证书过滤”技术。证书组合允许将复杂系统的验证问题分解为多个子问题，降低了单个证书设计的难度。证书过滤则通过筛选关键证书，显著减少了验证的计算量，使得该方法能够扩展到更复杂的系统。与现有方法相比，该方法不需要直接验证整个DRL控制器的输出，而是通过验证一系列相对简单的证书，间接证明控制器的安全性。
关键设计：在证书设计方面，需要根据系统的动力学特性和安全约束，选择合适的Lyapunov函数和Barrier函数。证书的训练通常采用监督学习的方式，通过最小化损失函数来优化神经网络的参数。损失函数的设计需要考虑Lyapunov Barrier的条件，例如Lyapunov函数的负定性和Barrier函数在安全区域内的正定性。证书过滤可以通过分析证书之间的依赖关系，或者通过实验评估每个证书对验证结果的影响来实现。
🖼️ 关键图片
📊 实验亮点
在航天器控制的案例研究中，该方法成功地为DRL控制器提供了安全和活性保证。实验结果表明，通过证书组合和过滤技术，验证的计算复杂度显著降低，使得对复杂系统的形式化验证成为可能。虽然论文中没有给出具体的性能数据，但案例研究证明了该方法在实际应用中的有效性。
🎯 应用场景
该研究成果可应用于各种安全关键型自主系统，例如无人驾驶汽车、无人机、机器人和航天器等。通过形式化验证，可以提高这些系统在复杂环境下的安全性和可靠性，降低事故发生的风险。该方法还有助于提升人们对人工智能系统安全性的信任，促进其在更多领域的应用。
📄 摘要（原文）
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.