使用Lyapunov障碍证书形式化验证深度强化学习控制器

深度强化学习（DRL）是生成控制自主系统的智能体的一种强大机器学习范式。然而，DRL智能体的“黑箱”性质限制了其在现实世界安全关键应用中的部署。为智能体行为提供强保证的一种有前景的方法是使用神经Lyapunov障碍（NLB）证书，这些证书是在系统上学习的函数，其性质间接暗示智能体按期望方式行为。然而，基于NLB的证书通常难以学习，更难以验证，尤其是对于复杂系统。在这项工作中，我们提出了一种训练和验证离散时间系统基于NLB的证书的新方法。具体来说，我们引入了一种证书组合技术，通过策略性地设计一系列证书来简化高度复杂系统的验证。当与神经网络验证引擎联合验证时，这些证书提供了DRL智能体既实现其目标又避免不安全行为的形式化保证。此外，我们引入了一种证书过滤技术，显著简化了生成形式化验证证书的过程。我们通过一个为DRL控制的航天器提供安全性和活性保证的案例研究展示了我们方法的优点。