Learning-Based Shielding for Safe Autonomy under Unknown Dynamics
作者: Robert Reed, Morteza Lahijanian
分类: eess.SY, cs.LG
发布日期: 2024-10-07
备注: 8 pages, 3 figures
💡 一句话要点
提出基于学习的屏蔽方法，保障未知动态下自主系统的安全性
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)
关键词: 安全自主 深度核学习 区间MDP 屏蔽方法 未知动态 安全线性时序逻辑 强化学习
📋 核心要点
- 现有屏蔽方法依赖于已知或有限状态模型，难以应用于具有未知动态的深度强化学习系统。
- 论文提出一种基于深度核学习的屏蔽方法，对系统动态进行建模并量化不确定性，构建区间MDP。
- 实验证明该方法在非线性系统中有效，包括高维自主航天器场景，验证了算法的可靠性。
📝 摘要（中文）
本文提出了一种数据驱动的屏蔽方法，用于保证黑盒控制器（例如深度强化学习中的神经网络控制器）控制下未知系统的安全性。现有屏蔽方法依赖于马尔可夫决策过程（MDP）的正式验证，假设系统模型已知或为有限状态，这限制了其在具有未知连续状态系统的深度强化学习环境中的应用。本文利用深度核学习对系统的一步演化进行建模，并量化不确定性，构建一个有限状态抽象，即区间MDP（IMDP）。通过关注用安全线性时序逻辑（safe LTL）表达的安全性属性，我们开发了一种算法，用于计算IMDP上最大许可的安全策略集，确保避免不安全状态。理论证明和包括高维自主航天器场景在内的非线性系统实验验证了该算法的可靠性和计算复杂度。
🔬 方法详解
问题定义：论文旨在解决在未知动态环境下，如何保证由黑盒控制器（如深度强化学习控制器）控制的自主系统的安全性问题。现有基于MDP的屏蔽方法依赖于对系统动态的精确建模，这在实际应用中往往难以实现，尤其是在深度强化学习场景中，系统动态通常是未知的或难以建模的。因此，如何设计一种能够在未知动态下保证系统安全性的屏蔽方法是一个关键挑战。
核心思路：论文的核心思路是利用数据驱动的方法学习系统动态，并量化学习过程中的不确定性。具体而言，论文使用深度核学习（Deep Kernel Learning）来建模系统的一步演化过程，并估计模型的不确定性。然后，基于学习到的动态模型和不确定性，构建一个区间MDP（IMDP），将连续状态空间抽象为有限状态空间，从而可以使用基于MDP的验证方法来保证系统的安全性。
技术框架：整体框架包括以下几个主要步骤：1) 使用深度核学习从数据中学习系统动态模型，并量化模型的不确定性；2) 基于学习到的动态模型和不确定性，构建一个区间MDP（IMDP），将连续状态空间抽象为有限状态空间；3) 定义安全线性时序逻辑（safe LTL）来描述系统的安全规范；4) 开发一种算法，用于计算IMDP上最大许可的安全策略集，确保避免不安全状态。
关键创新：论文最重要的技术创新点在于提出了一种基于学习的屏蔽方法，能够在未知动态下保证系统的安全性。与现有方法相比，该方法不需要对系统动态进行精确建模，而是通过数据驱动的方式学习系统动态，并量化学习过程中的不确定性。此外，论文还提出了一种新的算法，用于计算IMDP上最大许可的安全策略集，能够有效地保证系统的安全性。
关键设计：论文使用深度核学习来建模系统动态，深度核学习结合了深度学习和高斯过程的优点，能够有效地学习复杂的非线性动态模型，并提供不确定性估计。论文使用safe LTL来描述系统的安全规范，safe LTL是一种形式化的语言，能够精确地描述系统的安全属性。论文提出的算法基于值迭代，通过迭代计算每个状态的安全值函数，从而找到最大许可的安全策略集。
🖼️ 关键图片
📊 实验亮点
论文通过在非线性系统（包括高维自主航天器场景）上的实验验证了所提出方法的有效性。实验结果表明，该方法能够在未知动态下有效地保证系统的安全性，并且具有良好的计算效率。具体的性能数据和对比基线在论文中有详细描述，证明了该方法的优越性。
🎯 应用场景
该研究成果可应用于各种需要安全保障的自主系统，例如自动驾驶汽车、无人机、机器人等。特别是在系统动态未知或难以建模的情况下，该方法能够有效地保证系统的安全性，具有重要的实际应用价值。未来，该方法可以进一步扩展到更复杂的系统和更丰富的安全规范。
📄 摘要（原文）
Shielding is a common method used to guarantee the safety of a system under a black-box controller, such as a neural network controller from deep reinforcement learning (DRL), with simpler, verified controllers. Existing shielding methods rely on formal verification through Markov Decision Processes (MDPs), assuming either known or finite-state models, which limits their applicability to DRL settings with unknown, continuous-state systems. This paper addresses these limitations by proposing a data-driven shielding methodology that guarantees safety for unknown systems under black-box controllers. The approach leverages Deep Kernel Learning to model the systems' one-step evolution with uncertainty quantification and constructs a finite-state abstraction as an Interval MDP (IMDP). By focusing on safety properties expressed in safe linear temporal logic (safe LTL), we develop an algorithm that computes the maximally permissive set of safe policies on the IMDP, ensuring avoidance of unsafe states. The algorithms soundness and computational complexity are demonstrated through theoretical proofs and experiments on nonlinear systems, including a high-dimensional autonomous spacecraft scenario.