安全强化学习的可验证性：综述与基准

Provably Safe Reinforcement Learning: Conceptual Analysis, Survey, and Benchmarking

安全强化学习的可验证性：综述与基准

https://arxiv.org/pdf/2205.06750

摘要 确保强化学习（RL）算法的安全性对于释放其在众多现实任务中的潜力至关重要。然而，传统的RL及大多数安全RL方法都无法保证安全性。近年来，已提出若干方法以提供可证明的安全性保障，这对于不安全动作可能带来灾难性后果的应用场景至关重要。尽管如此，目前尚无对这些可证明安全RL方法的全面比较。因此，我们引入了对现有可证明安全RL方法的分类，阐述了其在连续与离散动作空间中的概念基础，并对现有方法进行了实证基准测试。我们根据动作调整方式将方法分为三类：动作替换、动作投影和动作遮蔽。在倒立摆和四旋翼稳定任务上的实验表明，尽管实现相对简单，动作替换方法在这些应用中表现最佳。此外，在每次安全验证被触发时添加奖励惩罚，在我们的实验中提升了训练性能。最后，我们为根据安全规范、RL算法和动作空间类型选择可证明安全RL方法提供了实用指导。

1 引言 强化学习（RL）推动了机器人学（El-Shamouty 等人，2020；Zhao 等人，2020）、自主系统（Kiran 等人，2022；Ye 等人，2021）和游戏（Mnih 等人，2013；Silver 等人，2017）等挑战性研究领域的许多近期进展。传统的RL智能体通常通过随机探索并多次执行不期望的动作来学习如何获得最高可能的奖励。然而，许多应用对安全性有重要要求。因此，安全RL应运而生，其学习过程被调整，使智能体在训练和/或运行期间将安全因素与性能一并考虑（García & Fernández，2015）。安全RL方法对安全性的考虑程度各不相同。首先，一些方法仅融入安全因素但不提供形式化保证。例如，通过添加表示风险的奖励项或调整探索策略使智能体更倾向于选择安全动作。其次，一些方法提供概率性安全保证，例如使用概率模型判断安全动作（Könighofer 等人，2021）。然而，当失败后果灾难性且必须在训练和部署期间不惜一切代价避免时，对RL智能体而言，硬性安全保证是必要的。此类安全关键应用包括自动驾驶、人机协作和能源电网。我们将这种在训练和运行期间均提供硬性安全保证的安全RL方法的第三种子类称为“可证明安全的RL”（provably safe RL）。

我们首次为连续和离散动作空间中的可证明安全RL提供了统一的概念框架、全面的文献综述，并在两个广泛使用的控制基准上对可证明安全的RL方法进行了比较。可证明安全RL方法之间的核心区别在于它们如何调整智能体的动作。因此，我们将其分为三类：动作替换、动作投影和动作遮蔽。我们提出的可证明安全RL分类法，为该研究领域提供了简洁的呈现，通过清晰的术语和全面的文献回顾帮助研究人员实现可证明安全的RL，并为这三个类别内的未来研究指明了方向。此外，我们对这些方法进行了实验评估。实验的三个主要发现是：所有可证明安全的RL方法确实保证了安全性；在五种测试的RL算法上，动作替换方法平均表现最佳；在使用安全函数时向奖励添加惩罚能进一步提升性能。

我们的贡献有四个方面。第一，我们引入了对可证明安全RL方法的全面分类及其形式化描述。这种分类使我们能够比较和评估选择特定类型动作修改对智能体学习能力的影响。第二，我们提出了针对连续动作空间的动作遮蔽（action masking）的首个形式化方案。第三，我们对以往可证明安全RL的研究工作进行了系统而全面的综述，并将其归入上述三类。最后，我们是首个在两个常见控制基准上评估所有三种可证明安全RL方法性能的研究。这一比较揭示了不同可证明安全RL方法的优缺点，使我们能够提供针对特定问题选择最合适方法的建议，且该建议独立于所使用的安全验证方法。

本文其余部分结构如下。首先，在第1.1节中简要回顾安全RL和可证明安全RL的历史发展。在第2节中介绍预备概念，并提出我们的分类方法。然后，在第3节中展示相关可证明安全RL文献如何符合我们的分类。第4节在二维（2D）四旋翼稳定任务上对不同的可证明安全RL类别进行实验比较。第5节讨论实验评估结果及其带来的实际考量。最后，我们在第6节总结本研究。

1.1 向可证明安全RL的演进

强化学习（RL）中的风险与安全概念至少自20世纪90年代起就被讨论（Heger, 1994）。将安全与RL结合的原因在于将学习集中在相关或安全的区域，并提高收敛速度。因此，安全RL领域开始发展，2015年，García & Fernández (2015) 首次对安全RL方法进行了归类。他们提出了两个高层次的类别：修改优化准则的方法和修改探索策略的方法。自2015年以来，无模型RL的重大进展以及深度RL应用性的增强改变了安全RL的研究重点。特别是，无模型深度RL的高效率使其在现实世界中的应用变得切实可行，从而放大了对安全RL中形式化保证的需求。Brunke 等人 (2022) 的综述也反映了这一点，他们研究了安全机器人学中控制与学习交叉领域的最新发展。他们将更广泛的安全控制学习领域的目标定义为：在确保形式化安全保证的同时，所需系统知识尽可能少（Brunke 等人, 2022, 图4）。在现有的安全RL方法中，可证明安全RL研究正处在这个前沿的新兴领域，因为它在学习和部署期间都提供硬性安全保证。尽管Brunke 等人 (2022) 提到的少数论文属于可证明安全RL，但这并非他们工作的重点。

在接下来的段落中，我们采用按安全规范类型划分的通用分类法（即软约束、概率性保证和硬性保证），来定位可证明安全RL在安全RL领域中的位置。

软约束采用软约束的方法将安全性直接纳入其优化目标中，因此智能体可以探索所有动作和状态，而无需考虑安全性。因此，这些方法在训练期间（尤其是初期）可能是不安全的，但通常在经过足够多的训练步骤后会收敛到一个更安全的策略，且不提供形式化的安全保证。告知RL智能体安全约束最简单的方法是通过其奖励函数。尽管这种方法很优雅，但也存在许多潜在陷阱。首先，奖励函数可能定义不当，无论是手动调整还是从人类输入中学习得到的。当手动定义时，奖励函数可能忽略某些特征或细节，导致出现可被“利用”（hackable）的奖励（Skalse 等人, 2022），智能体可能因此学会不安全的行为。从人类反馈中学习奖励函数（Christiano 等人, 2017）也容易出错，因为将安全约束与性能指标一并传达，对于稀疏、非线性、条件性或罕见发生的约束来说非常困难。其次，即使奖励函数定义正确，也无法保证训练出的策略是安全的；例如，Packer 等人 (2018) 已证明，RL智能体在部署期间对分布外状态的处理能力较差。第三，智能体可能学会安全地执行动作，但由于目标错误泛化（goal misgeneralization）（Langosco 等人, 2022）而忽略任务目标。尽管如此，大多数安全RL研究都将安全方面视为软约束，因此我们将在下一段提供软约束方法的简要概述。

为了减轻手动设计奖励的负担，近期的一些工作将任务及其安全规范形式化为时序逻辑公式。然后，通过直接使用与该公式相关的鲁棒性度量作为奖励（Aksaray 等人, 2016; Li 等人, 2017; Varnai & Dimarogonas, 2020），或将时序逻辑公式转换为生成奖励的自动机（Camacho 等人, 2019; Hahn 等人, 2019; Cai 等人, 2021; Hasanbeig 等人, 2022; Alur 等人, 2023），将时序逻辑公式转换为RL奖励。对于某些算法，甚至可以确保策略收敛到最优策略，即最大程度满足时序逻辑规范的策略（Alur 等人, 2022; Yang 等人, 2022）。另一种告知RL智能体安全性的方法是将其表述为约束优化问题。在约束RL方面（Altman, 1998; Achiam 等人, 2017; Stooke 等人, 2020），已有许多近期进展，其策略旨在最大化奖励的同时满足用户定义的规范。这些规范可以被表述为约束函数（Chow 等人, 2018; Stooke 等人, 2020; Yang 等人, 2020; Marvi & Kiumarsi, 2021）或时序逻辑公式（De Giacomo 等人, 2021; Hasanbeig 等人, 2019a;b; 2020）。与概率性或硬性约束方法相比，软约束方法的主要优势在于不需要智能体动力学或环境的显式模型，因为智能体通过经验来学习安全方面。因此，这类安全RL方法在非关键场景中具有巨大潜力，其中不安全动作不会造成重大损害。

概率性保证概率性安全RL方法依赖于概率模型，或从采样数据中合成模型。在此类方法中，动作和状态空间可以根据概率进行限制。然而，不安全动作有时无法被检测到，可能会偶尔发生。一些工作（Turchetta 等人, 2016; Berkenkamp 等人, 2017; Mannucci 等人, 2018）试图通过从一个通常由用户定义的保守集合开始，并用收集到的学习经验逐步扩展，来确定最大的安全状态集。其他方法（Könighofer 等人, 2021; Thananjeyan 等人, 2021; Dalal 等人, 2018; Zanon & Gros, 2021; Yang 等人, 2021; Gillula & Tomlin, 2013）基于构建概率模型来识别某个动作的安全概率。总体而言，依赖概率性方法的方法特别适用于无法用集合来界定测量误差、建模误差和干扰的场景。

硬性保证可证明安全RL的特征是提供硬性安全保证，这是通过将先验系统知识整合到学习过程中来实现的。在此类方法中，智能体仅探索安全的动作，并且仅进入满足安全规范的状态。可证明安全RL在学习过程中就已经满足了给定的安全规范，这对于在物理世界中训练或微调安全关键任务的智能体至关重要。因此，我们将那些仅对已学习策略进行验证的方法（Bastani 等人, 2018; Schmidt 等人, 2021）排除在本综述之外。我们专注于无模型RL算法，即不显式学习或使用系统动力学模型来优化策略的算法。近年来，将学习到的控制器部署到物理世界变得越来越现实，因此对可证明安全RL的需求日益增长，也催生了更多的可证明安全RL方法。通过本研究，我们旨在为这一不断发展的领域提供结构化的框架和实用的见解。

2 概念分析

我们通过在一个统一的概念框架内提供其形式化描述，引入了三种可证明安全的强化学习（RL）类别。该框架阐明了这三类方法之间的差异，并有助于后续的文献综述和基准测试。

可证明安全的强化学习（Provably safe RL）依赖于模型知识来提供安全保证，即需要一个与安全相关的系统和环境动力学相一致的模型。只要该模型是对真实系统的保真抽象（Roehm 等人，2019；Liu 等人，2023），即它能同时对偶然性（aleatoric）和认知性（epistemic）不确定性进行过近似（over-approximates），并涵盖所有相关的安全方面，验证过程就可以使用这种抽象。这有助于实现高效的验证，因为抽象模型的复杂性通常远低于底层马尔可夫决策过程（MDP）的复杂性。在无法获得此类安全模型的系统中，可证明安全的RL方法不适用，只能使用第1节中讨论的非可证明安全方法。在实践中，安全规范通常被弱化为合法安全（legal safety）或被动安全（passive safety）。在这种情况下，由其他智能体引起的不可避免的安全违规不被视为该智能体的过错，因此不被认为是不安全的。例如，自主驾驶（Pek 等人，2020）和机器人学（Bouraine 等人，2012）领域已有证明合法安全的案例。

确保RL系统可证明安全的方法有多种，我们将其总结为三类：动作替换（action replacement），即安全方法将智能体输出的所有不安全动作替换为安全动作；动作投影（action projection），即将不安全动作投影到安全的动作空间上；以及动作遮蔽（action masking），即智能体只能从安全的动作空间中选择动作。我们选择这种分类方式，因为它代表了文献中为修改动作以确保RL安全性的三种主要方法。动作替换和动作投影是在智能体输出动作之后对其进行修改，而动作遮蔽则让智能体直接从安全的动作空间中进行选择。图1展示了这些方法的基本概念。接下来的小节将分别描述每种方法的概念、数学形式化及其实际影响。

2.1 动作替换

被执行。我们在附录中讨论了这种动作替换如何改变马尔可夫决策过程（MDP），并额外参考了感兴趣的读者到Hunt等人（2021年）的研究。

2.2 动作投影

与动作替换不同，在动作替换中替换的动作不一定与智能体的原始动作相关，而动作投影则返回与原始动作最接近的、可证明安全的动作，该距离是相对于某个距离函数而言的。为此，我们定义如下优化问题：

2.3 动作屏蔽

将遮蔽机制集成到特定学习算法中并非易事。Krasowski 等人 (2020) 和 Huang & Ontañón (2022) 讨论了其对策略优化方法的影响。对于学习Q函数的强化学习算法，我们以深度Q网络（DQN）(Mnih 等人, 2013) 为例，讨论离散动作遮蔽的影响，DQN 是离散动作Q学习中最常用的方法。在使用动作遮蔽进行探索时，智能体从安全动作集 Aφ 中均匀采样动作。当智能体利用Q函数进行决策时，它只在 Aφ 中选择最优动作，即 arg maxa∈Aφ Q(s, a)。用于更新Q函数 Q(s, a) 的时间差分误差为 (Mnih 等人, 2017, 公式3)：

2.4 对动作分布的影响

前述三种可证明安全的强化学习方法对结果动作分布有不同的影响，如图2所示，针对一维连续动作空间和概率策略。

2.5 学习元组

在改变强化学习（RL）动作时，可以使用四种可能的学习元组进行智能体的训练：

3 文献综述

在本节中，我们总结了先前在可证明安全的强化学习（RL）方面的工作，并将它们归类到我们提出的类别中。为了识别相关文献，我们使用了Scopus和IEEEXplore搜索引擎的搜索字符串TITLE-ABS("reinforcement learning") AND TITLE(learning) AND [TITLE(safe*) OR TITLE(verif*) OR TITLE(formal*) OR TITLE(shield*)] AND LIMIT-TO(LANGUAGE,"English")，这导致在去除重复项后共得到620篇论文。然后，我们通过标题和摘要筛选论文，以识别160篇看似相关的论文。经过仔细检查，我们确定这160篇论文中有47篇是可证明安全的RL工作。我们在表1中概述了所有与应用无关的可证明安全的RL工作，并在表2中根据应用将所有47篇可证明安全的RL工作进行分类。表1中的一些方法针对的是无界干扰。在这种情况下，通常无法实现硬安全保证。尽管如此，我们还是包括了在假设干扰有限的情况下可以被证明安全的方法。

Shao 等人 (2021) 使用基于集合可达性分析（set-based reachability analysis）的轨迹保护机制作为 φ(s, a)。只要初始状态、系统动力学和输入扰动来源于一个紧致集，集合可达性分析就适用于具有不确定性的通用非线性系统的避障-到达问题，参见 Althoff 等人 (2021)。如 Althoff 等人 (2021) 所述，对于大多数集合表示形式，集合可达性分析在状态维度上具有多项式复杂度。然而，与 Hamilton-Jacobi-Isaacs 可达性分析相比，集合可达性分析无法处理任意非凸集合，而是依赖于特定的集合表示形式。Shao 等人 (2021) 在动作不安全时，在其附近随机采样 n 个新动作，然后执行与原始（不安全）动作最接近的安全动作。如果这 n 个新动作均不安全，则执行一个失效保护动作 ψfailsafe(s)。Shao 等人 (2021) 使用朴素学习元组（naive learning tuple）训练其智能体。Selim 等人 (2022b) 也使用集合可达性分析来验证动作的安全性。他们提出了一种对 ψ(s) 的改进型替换方法，使得受控系统的可达集远离不安全集 S \ Ss。作者还提出了一种方法，利用所谓的“黑箱可达性分析”（black-box reachability analysis）来处理未知的系统动力学。他们使用带适应性惩罚的学习元组（adaption penalty learning tuple），并展示了该方法在三个用例中实现了可证明的安全性。

Hunt 等人 (2021) 通过微分动态逻辑（differential dynamic logic）公式的定理证明来构建验证函数 φ(s, a)。利用 φ(s, a)，他们确定离散动作空间下的安全动作集 Aφ(s)，并使用 ψfailsafe(s) 进行替换。他们进一步展示了如何通过控制器和模型监控器实现可证明安全的端到端学习。他们在无人机示例上使用朴素学习元组训练了RL智能体。Anderson 等人 (2020) 的工作提出将 Sφ 定义为一个鲁棒控制不变集，并基于系统动力学的最坏情况线性模型来构建安全函数 φ(s, a)。另一项值得注意的工作是 Bastani (2021)，该工作提出在训练好的策略旁边使用一个模型预测保护罩（model predictive shield），该保护罩使用 ψfailsafe(s) 进行动作替换。

从发表的文献数量来看，动作替换是最流行的方法。这一点也体现在大量针对特定应用的方法上，例如用于飞行器（Shyamsundar 等人, 2017; Harris & Schaub, 2020; Nazmy 等人, 2022）、自动驾驶（Chen 等人, 2020; 2022a; Lee & Kwon, 2022; Wang 等人, 2023; Evans 等人, 2023）、电力系统（Ceusters 等人, 2023）、机器人操作（Thumm & Althoff, 2022）、主动悬架系统（Li 等人, 2019b）以及计算机网络交通工程（Wang 等人, 2022）。特别是 Ceusters 等人 (2023) 比较了失效保护动作替换和基于采样的动作替换。他们观察到，这两种方法的初始性能均高于不安全的RL基线，且失效保护动作替换的表现优于基于采样的版本。

动作投影 关于动作投影的研究通常在连续的动作空间和状态空间中进行。该类别中不同研究的主要区别在于投影优化问题的具体设定。首先，Pham等人（2018）通过一种称为OptLayer的可微分约束优化层来保证安全性。他们的方法仅限于二次规划问题，因此系统模型和约束必须是线性的。尽管存在这些限制，他们仍在一个简单的机械臂避障任务中展示了该方法的有效性。Cheng等人（2019）通过控制屏障函数（CBF）来定义优化问题中的安全约束φ(s, a) = 1。因此，公式（3）中的优化问题转化为一个二次规划问题。理论上，CBF方法适用于具有来自紧致集扰动的一般控制仿射系统，用于实现“到达-避免”类规范。然而，寻找CBF并非易事，其综合过程在系统维度上可能是指数级复杂的（Ames等，2019）。为了更高效地在线求解（3），Cheng等人（2019）在第2.2节所述方法的基础上引入了一个神经网络，用于近似CBF带来的修正量。动作在优化前先根据该近似值进行调整。这种调整提高了实现效率，同时仍能保证安全性，因为动作在调整后通常已经满足安全要求，无需再求解优化问题。他们在倒立摆和车辆跟驰任务上的安全学习实验表明，使用CBF的方法比传统的强化学习收敛速度更快。Li等人（2019a）提出了一种从自动机构造连续CBF的方法，该自动机由线性时序逻辑公式定义。他们进一步从给定的自动机构造引导奖励，以提升学习性能。所提出的方法能够安全地学习高维协同操作任务。Marvi和Kiumarsi（2022）则定义了一个不同的问题，假设系统模型是确定性的但未知。他们迭代地学习最优控制器和系统动力学，并在每次迭代中逐步降低CBF的保守性。该方法对无扰动的线性时不变（LTI）系统具有可证明的安全性。

Gros等人（2020）和Wabersich与Zeilinger（2021）将优化问题实现为如公式（7）所定义的鲁棒模型预测控制（MPC）问题。MPC适用于存在测量和状态扰动的“到达-避免”问题。然而，在控制高速系统时，鲁棒MPC通常仅限于线性系统（Zeilinger等，2014）。Gros等人（2020）主要讨论了在使用动作投影时，不同强化学习算法的学习更新应如何调整。对于Q学习，他们发现当使用原始经验元组时，无需对学习算法进行任何修改。而对于策略梯度方法，他们认为为了实现稳定学习，必须将投影过程也纳入梯度计算中（Gros等，2020，第3节）。Gros等人（2020）和Wabersich与Zeilinger（2021）所采用的鲁棒MPC公式的缺点之一是，环境中移动障碍物或行人的动态约束难以直接整合。他们使用高斯过程（GP）对系统动态进行近似，因此无法提供严格的安全性保证。然而，如果像前述方法那样假设系统动力学为确定性且具有有界扰动，则他们本可以保证严格的安全性规范。Gros等人（2020）在简单的二维LTI系统上评估了他们的方法，而Wabersich与Zeilinger（2021）则在倒立摆和四旋翼飞行器任务中展示了其方法的有效性。

与Selim等人（2022b）之前的成果相反，Selim等人（2022a）提出通过求解一个优化问题来寻找最近的安全动作，而不是使用启发式的替代方法。他们再次使用基于集合的可达性分析来构建φ(s, a)。他们在四旋翼飞行器和移动机器人基准任务上测试了该方法。Kochdumper等人（2023）利用基于集合的可达性分析来验证动作是否满足φ(s, a)。他们针对动作空间的参数化形式构建了投影问题，并将其转化为一个带有多项式约束的混合整数二次规划问题。他们的方法能够为具有有界扰动的非线性系统提供可证明的安全性，并在两个四旋翼任务、高速公路自动驾驶以及一辆真实的F1TENTH小车上进行了验证。

除了这些概念性方法外，动作投影算法也被专门应用于多种信息物理系统，例如自动驾驶（Wang, 2022；Hailemichael等, 2022a;b）、电力系统（Eichelbeck等, 2022；Chen等, 2022b；Zhang等, 2023；Yu等, 2023）以及发动机排放控制（Norouzi等, 2023）。Wang（2022）比较了离散动作掩码方法与其连续动作投影方法的部署效果。结果显示，离散动作掩码方法的目标达成性能较低。然而，这可能是由于动作空间被粗略地离散为仅三个动作所致。

动作掩码 据我们所知，现有文献仅针对离散动作空间考虑动作掩码。Huang与Ontañón（2022）分析了离散动作掩码对强化学习中策略梯度算法的影响，但他们假设可行动作集As是已知的，而这种情况通常仅出现在游戏或网格世界环境中。

研究动作掩码的两篇主要工作是Fulton与Platzer（2018）和Fulton与Platzer（2019）。他们基于微分动态逻辑规范的定理证明，构建了控制器监控器和模型监控器（参见Platzer, 2008）。控制器监控器用于生成掩码η(s)，而模型监控器则根据先前的状态转移验证底层系统模型是否正确。在每个状态中，智能体可以从控制器监控器验证为安全的动作集合中进行选择。识别正确的系统可能具有挑战性，因此他们还引入了一种自动生成候选模型的方法。如果初始模型始终正确（Fulton & Platzer, 2018），或提供了多个模型且其中至少有一个始终正确（Fulton & Platzer, 2019），则他们的方法具有可证明的安全性。他们在自适应巡航控制任务中验证了这种可证明安全的动作掩码方法。

除了上述工作外，还有一些研究将动作掩码应用于特定领域，包括自动驾驶（Mirchevska等, 2018；Krasowski等, 2020；Brosowsky等, 2021；Krasowski等, 2022）、电力系统（Tabas & Zhang, 2022）、计算网络中的自适应路由（Seetanadi等, 2020）以及城市交通信号控制（Müller & Sabatelli, 2022）。其中，唯一将动作掩码与其他可证明安全的强化学习方法进行比较的特定应用研究是Brosowsky等人（2021）。他们观察到，其掩码方法的收敛速度略快于动作投影方法。

4 实验比较 在本节中，我们评估了第2节中介绍的三类可证明安全的强化学习方法以及四种学习元组的性能。为了进行比较，我们选择倒立摆和二维四旋翼飞行器稳定任务作为基准，因为这些基准在表1所列的相关研究中被广泛使用。三种方法的安全状态集 Sφ是相同的，因此具有可比性。我们在基准任务中加入了系统扰动，以使其更贴近实际，并验证这些可证明安全的强化学习方法能够处理从紧致扰动集中采样的扰动。尽管这些任务的维度较低，但我们的结果很可能可推广到实际系统，因为在实际应用中，通常通过使用低维抽象模型并附加扰动项来简化现实世界的复杂性。随后，一致性检查技术（Roehm 等, 2019；Liu 等, 2023）可以保证该抽象模型包含了系统在真实世界中的记录行为。

本节展示的算法包括：使用 ψsample(s)的动作替换、使用仿射约束的动作投影，以及动作掩码。我们对每种配置在十个不同的随机种子下进行实验，并结合五种常见的强化学习算法进行比较：连续动作空间的双延迟深度确定性策略梯度算法（TD3）(Fujimoto 等, 2018)、连续软演员-评论家算法（SAC）(Haarnoja 等, 2018)、离散动作空间的DQN (Mnih 等, 2013)，以及连续和离散版本的近端策略优化算法（PPO）(Schulman 等, 2017)。

4.1 环境 我们在倒立摆和二维四旋翼飞行器稳定任务上对可证明安全的强化学习方法进行比较。

4.2 安全状态集的计算

4.3 结果

我们还比较了三种安全机制的干预率。对于动作替换和投影，我们的干预率指标表示在RL步骤中，安全函数改变动作的步骤所占的比例。对于动作屏蔽，干预率比较了在系统平衡点处，可能安全动作集的平均体积与可能安全动作集的体积之比。图3b显示，动作替换在安全机制上的依赖性明显低于投影和屏蔽。通常，我们报告较低的干预率往往与较高的奖励一致。

学习元组的比较 我们在图4中评估了不同学习元组对所有五个强化学习算法性能和干预率的影响。当使用动作屏蔽时，只能采样安全动作，即只有朴素元组有意义；因此我们在这次评估中省略了动作屏蔽。对于动作替换和投影，适应惩罚元组导致最高性能和最低的安全干预率，甚至超过了基线平均值。在动作投影中，朴素元组的表现明显不如动作替换。安全动作元组和两者元组似乎只有在使用动作投影时才有益，而在使用动作替换时会降低性能。

5 讨论

我们的实验证实了理论陈述，即当命题1成立时，可证明安全的RL方法总是安全的。在两个测试环境中，所研究的RL基线在训练期间显示出非零的安全违规，即使在收敛后也是如此。随后，我们讨论了实验得出的五个结论，为实施可证明安全的RL提供直觉，总结局限性，并确定可证明安全RL的未来研究方向。

选择可证明安全的RL方法 首先，我们想总结一下在两个调查基准上使用三种可证明安全的RL类别的经验。动作替换是连续动作空间中最容易实现的方法。它表现出非常好的性能和低干预率。在这里，使用适应惩罚的故障安全动作进行替换易于实现，并且在我们的实验中表现最佳。然而，从安全动作空间中随机采样可能优于故障安全动作。因此，如果可以直接从安全动作空间中采样，例如在离散动作空间中，就不需要故障安全控制器。动作投影在实践中往往由于小的数值误差而出现问题，导致不可行的优化问题。因此，我们必须重用以前的优化结果，例如在Schürmann等人（2018年）的鲁棒MPC中，或者如果优化问题不可解，则使用故障安全控制器。结合与动作替换相比更高的干预率和复杂的实现，根据我们的经验，我们不建议使用动作投影。然而，如果已经有一个CBF或MPC公式，它可能是最合适的解决方案。动作屏蔽在离散动作空间中特别容易实现，并且在该设置中表现良好。然而，对于连续动作空间中的动作屏蔽，还没有一个有效且通用的算法可以处理与轴对齐盒子显著不同的安全动作空间。通常，不同的方法也可以在一定程度上结合使用。例如，如果动作投影的优化问题变得不可行，可以使用故障安全控制器。

选择学习元组 适应惩罚学习元组表现最佳，特别是在使用动作投影时。在我们的实验中，简单的恒定奖励惩罚已经提高了性能。其他环境可能需要更仔细的奖励调整，或者由于奖励黑客攻击（Skalse等人，2022年）或目标错误泛化（Langosco等人，2022年），适应惩罚元组可能完全失败。图4中的进一步结果表明，使用训练元组中的安全动作 a~，即配置两者和安全动作，有利于动作投影方法的性能，但会损害使用动作替换的训练。这种效果可能源于动作替换比动作投影更改变动作，导致改变后的动作更不可能来自RL策略。附录中的评估表明，当使用PPO时，这种效果尤为明显。这种基于策略的算法假设当前批次的训练数据来自当前策略。因此，我们建议在可能的情况下使用适应惩罚元组，并且仅在与离策略方法结合时使用安全动作。

计算复杂性 这三种方法的计算复杂性高度依赖于特定场景的实现。对于动作投影，主要的实现挑战是保证优化问题始终可行。如果优化问题可以表述为二次规划，计算复杂性是多项式的，如Vavasis（2001年）所示。相反，动作替换和动作屏蔽的计算复杂性高度依赖于识别动作安全性的算法。对于离散动作屏蔽，计算复杂性显然与动作总数

成线性关系。对于动作替换，我们只需要一个安全动作，因此在理想情况下，例如使用故障安全控制器，计算复杂性与动作总数无关。假设动作替换方法需要确定整个安全动作集，显然它与动作屏蔽在动作数量方面的计算复杂性相同。识别连续安全动作空间的计算复杂性取决于任务特定的实现。一种可能性是使用基于集合的可达性分析计算安全动作空间，我们希望感兴趣的读者参考Althoff等人（2021年）的不同方法。

在线与离线实现 在线和离线在可证明安全的RL中有两个含义：在线与离线安全验证和在线与离线RL。安全函数通常需要在线评估，因为对于连续状态空间，预先计算所有状态的安全动作集通常不可行。因此，安全函数的计算复杂性对于实时应用很重要，如前一段所讨论的。如果状态和动作空间是离散的，可以离线预先计算安全动作（Alshiekh等人，2018年；Huang & Ontañón，2022年）。一般来说，只有在安全函数集成在代理和环境之间以纠正动作时，才能保证安全（见图1）。在这项研究中，我们比较了在线基于策略和离线基于策略的RL算法（Levine等人，2020年），因为它们被用于现有的可证明安全的RL研究。尽管如此，可证明安全的RL也可以用于离线RL，其中安全函数将在部署期间集成，并且在数据收集阶段很可能也会集成，如果这个阶段是在安全关键环境中进行的。然而，关于离线可证明安全的RL的更具体建议需要通过实验评估来证实，因此，这是未来研究的一个主题。

提高可证明安全的RL的适用性 尽管第3节讨论的先前工作很有前途，但关于高维非线性系统和有限的真实世界应用的工作还很少。我们建议未来研究可以在五个主要因素上提高适用性。首先，一些方法需要在计算上更高效才能适用于真实世界。如前所述，验证方法的计算效率特别相关，应该提高。其次，我们观察到使用的元组对某些RL算法的智能体性能有显著影响。此外，还需要更多的理论研究可证明安全的RL方法如何影响收敛到最优策略。对可证明安全的RL及其学习元组对收敛的影响进行更多的实证和理论研究是可取的。第三，需要共同的基准来评估新的可证明安全的RL方法。此外，应该在更复杂的基准上比较这三种动作校正策略，以澄清我们的观察是否可以扩展到它们。这种基准测试将使可证明安全的RL研究更具可比性，便于开始可证明安全的RL研究，并提供更多证据来决定最合适的可证明安全的RL方法。第四，最近的工作中显示出安全规范的多样性较低，主要包含稳定和可达-避免规范。相反，真实世界的安全更复杂，例如，交通规则如红灯等待和绿灯安全但快速移动。最后，可证明安全的RL需要专家验证方法的知识。未来的研究可以通过模块化和自动化方法来减轻这一点，其中需要更少的工程决策，并且更多的参数自动调整。随着这些进步，可证明安全的RL可以将RL和形式规范的最佳元素结合起来，朝着需要尽可能少的专家知识并为复杂安全规范提供正式保证的RL方法发展，以实现可靠和可信的网络物理系统。

6 结论

总之，我们将可证明安全的RL方法进行分类，以从机器学习的角度整理文献。我们从概念角度介绍可证明安全的RL方法，并讨论了必要的假设。我们提出的分类为动作替换、动作投影和动作屏蔽，支持研究人员比较他们的工作，并为选择可证明安全的RL方法提供宝贵的见解。在2D四旋翼和倒立摆稳定基准上对四种可证明安全的RL实现的比较，为不同任务的最佳方法提供了进一步的见解。我们进一步提出了选择可证明安全的RL方法和学习元组的实际建议，这对于新接触RL或形式方法的研究人员来说将是有价值的。最后，如第5节所讨论的，我们提出的分类法和实验评估产生了多个有前景的未来研究方向。

原文链接：https://arxiv.org/pdf/2205.06750