🤖 machine learning

Contract-Based Compositional Shielding for Safe Multi-Agent Reinforcement Learning

本文提出了一种用于多智能体强化学习的基于契约的组合屏蔽框架，该框架通过利用非平稳多臂老虎机选择器来认证局部线性时序逻辑（LTL）义务元组，从而在确保确定性安全保证的同时，在去中心化执行下恢复团队最优行为。

原作者： Omar Adalat, Edwin Hamel-De le Court, Francesco Belardinelli

发布于 2026-06-15

📖 1 分钟阅读☕ 轻松阅读

原作者： Omar Adalat, Edwin Hamel-De le Court, Francesco Belardinelli

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你正在训练一支机器人团队协同工作，就像是一群负责运送包裹的无人机编队，或者是在仓库里整理物品的机器人。目标是让它们学习如何尽可能快速、高效地完成工作。然而，这里有一个难点：如果它们犯了错，可能会互相碰撞或损坏物品。

问题在于，什么是对一个机器人而言“安全”的，往往取决于其他机器人在做什么。如果机器人 A 向左移动，那是安全的。但如果机器人 B 在同一时间也向左移动，它们就会相撞。

旧方法：过度保护的家长

传统上，为了保证机器人的安全，研究人员会使用一个“中央屏蔽器”（central shield）。这就像是一个盯着整个团队的严厉家长。家长观察每一个可能的动作，并说：“好吧，你可以向左移动，但前提是你必须绝对确定没有其他人也会向左移动。”

为了确保万无一失，这个家长往往会过于谨慎。他们可能会说：“我不能让任何人向左移动，以防万一，”因为他们无法完美地预测其他机器人的行为。这会导致机器人无法进行那些能让工作高效完成的巧妙协作动作。这就像一位家长告诉一群孩子：“别玩捉迷藏了，因为可能会有人摔跤，”于是孩子们就只能坐着不动。他们很安全，但他们无法学习，也玩得不开心。

新方法：“契约”系统

这篇论文介绍了一种更聪明的方法，可以在不那么具有限制性的情况下保持团队安全。他们称之为基于契约的组合式屏蔽（Contract-Based Compositional Shielding）。

它是这样运作的，用一个简单的类比来说明：

1. 团队契约
与其使用一本大规则书，不如让团队达成一系列局部契约。

机器人 A 说： “我承诺始终留在房间的左侧。”
机器人 B 说： “我承诺始终留在房间的右侧。”

这些是“局部义务”。它们是每个机器人对自己行为做出的简单承诺。

2. 魔法检查（认证）
在机器人开始学习之前，一台计算机也会检查这些承诺是否能协同工作。它会问：“如果机器人 A 遵守它的承诺，且机器人 B 也遵守它的承诺，它们是否永远不会相撞？”

如果答案是**“是”**，则该契约被“认证”通过。
如果答案是**“否”**，则该契约会被废弃。

这就是“循环”的部分。机器人 A 依赖于机器人 B 的承诺，而机器人 B 也依赖于机器人 A 的承诺。只要计算机证明这两个承诺结合在一起能保证安全，那么这个团队就可以出发了。

3. 局部屏蔽器
一旦契约得到认证，每个机器人都会获得自己的微型“屏蔽器”（过滤器）。

机器人 A 的屏蔽器只观察机器人 A 的动作。它会说：“你可以向左、向右或向前移动，只要你保持在左侧即可。”它不需要知道机器人 B 在做什么，因为它信任机器人 B 的契约。
机器人 B 也会获得类似的屏蔽器。

因为这些屏蔽器是基于这些受信任的承诺，所以机器人 A 被允许做出那些旧有的“严厉家长”会禁止的行为。机器人 A 可以向左移动，因为它知道机器人 B 已经承诺留在右侧。这使得团队能够执行那些以往无法实现的、高速度的协调动作。

学习过程：“游戏节目”选择器

论文还描述了机器人如何学习挑选最佳契约。
假设机器人拥有一套不同的契约库（例如，“留在左侧”、“留在右侧”、“慢速移动”、“快速移动”）。

它们尝试运行一个契约一段时间。
它们观察表现如何（是否拿到了包裹？是否发生了碰撞？）。
一个“选择器”（就像游戏节目的主持人一样）会挑选出目前为止效果最好的契约，并坚持使用它。
如果某个契约不再奏效，它们就会从库中切换到另一个新契约。

至关重要的一点是，它们只会切换到那些已经被认证为安全的契约。它们绝不会去尝试一个未经检查的“盲目猜测”型契约。这意味着它们可以在从未面临碰撞风险的情况下，学习并提高速度。

实验结果

作者在六个不同的机器人场景（如仓库机器人和无人机群）中测试了该方法。他们发现：

安全性： 机器人从未发生碰撞，因为契约在数学上被证明是安全的。
性能： 与旧有的“严厉家长”方法相比，机器人学会了更好地协同工作。它们找回了那种被旧方法视为理所当然而舍弃掉的“最优”（最佳）协作方式。

总结

简而言之，这篇论文解决了这样一个问题：“我们如何在不需要中央控制器时刻监控的情况下，让机器人团队进行复杂的协作？”

旧方法： “除非我确定对所有人来说都是 100% 安全的，否则不要动。”（太慢，太保守）。
新方法： “你承诺做 X，我承诺做 Y。如果我们都遵守承诺，我们就是安全的。让我们快点把工作做完吧！”（快速、协调，且依然安全）。

论文证明了这种“契约”方法允许机器人团队在无需中央控制器每秒钟都在监视的情况下，学习复杂的、安全的团队协作。

技术摘要：基于契约的组合式屏蔽技术，用于安全多智能体强化学习

问题陈述

在协作式多智能体强化学习（MARL）中，由于任何单个智能体都无法单方面强制执行全局安全约束，确保训练和部署过程中的安全性具有挑战性。在“安全协调问题”中，一个智能体动作的可容许性取决于其队友的非平稳策略。标准方法通常依赖于集中式屏蔽（centralized shielding），即计算一个全局安全的动作关系；或者依赖于单边（因子化）掩码（unilateral/factorized masking），即每个智能体根据最坏情况假设独立地限制其动作。

本文指出单边掩码的一个关键局限性：它往往会丢弃那些需要协调才能实现的优化安全行为。正如论文的动机示例（图1）所示，如果智能体 A 的安全动作取决于智能体 B 选择特定动作，那么纯粹的单边掩码为了对智能体 B 的所有可能动作保持安全，会禁止智能体 A 的该动作。这导致了“保守的笛卡尔分解（conservative Cartesian decomposition）”，从而排除了安全的、高回报的协调联合动作。目标是在实现去中心化执行（智能体基于局部信息行动）的同时，恢复团队最优的安全行为，而不必回归到中心化的运行时控制。

方法论

作者提出了**基于契约的组合式屏蔽（Contract-Based Compositional Shielding）**框架，该框架将共享的全局安全规范分解为局部时序契约。该方法由三个主要阶段组成：

1. 形式化框架与假设

全局规范： 安全性由线性时序逻辑（LTL）安全片段中的单个全局公式 $\Phi_{safe}$ 定义。
局部契约： 全局规范被分解为一个局部义务元组 $C = \langle \phi_i \rangle_{i=1}^n$ ，其中每个 $\phi_i$ 是关于智能体 $i$ 局部字母表的 $LTL_{safe}$ 公式。
循环假设-保证（Circular Assume-Guarantee）： 与要求无环依赖结构的以往工作不同，本方法允许循环假设。智能体 $i$ 假设所有其他智能体 $j \neq i$ 都满足其义务 $\phi_j$ 。这种循环性不是通过固定顺序解决的，而是通过同时认证整个元组来解决。

2. 屏蔽合成（离线）

合成过程构建了一个经过认证的契约库：

自动机构建： 每个局部义务 $\phi_i$ 被编译为一个确定性安全自动机 $A^C_i$ ，其包含一组代表违规的“坏状态”。
契约乘积： 在状态空间 $S \times Q_1 \times \dots \times Q_n$ 上构建一个全局乘积自动机。
不动点认证： 作者使用假设-保证前驱算子计算一个最大不动点（即“矩形获胜区域” $Win^\square_C$ $W i n_{C}^{□}$ ）。该区域代表了从该状态出发，可以维持一个非空笛卡尔动作掩码（即“矩形”）的状态集合，使得：
1. 联合动作保持在获胜区域内。
2. 不会到达坏状态。
认证准则： 一个契约元组被视为“已认证”，需满足：
1. 局部义务的合取在语义上蕴含全局安全目标（ $C \models^\uparrow \Phi_{safe}$ ）。
2. 系统初始状态位于计算出的获胜区域内。
投影： 一旦完成认证，获胜区域将被投影以生成每个智能体的局部动作掩码。这些掩码是“局部可掩码识别的（locally mask-identifiable）”，这意味着智能体可以仅利用其局部观测历史和激活的契约标识符来确定其允许的动作，而无需重建其他智能体的掩码。

3. 学习与选择（在线）

库构建： 在训练前，通过有界搜索枚举候选契约元组（受限于公式深度和有限语言）。每个候选元组都会进行认证测试。成功的元组集合构成了认证库（ $\mathcal{L}_{cert}$ ）。
强盗算法选择器（Bandit Selector）： 在训练期间，使用一种非平稳多臂强盗算法来选择要在给定训练块中强制执行的契约。
- 每个契约充当一个“臂”。
- 选择器旨在优化团队回报，同时确保安全性。
- 它使用**折扣置信区间上界（D-UCB）**策略，以适应学习过程中的非平稳特性（随着策略的改进，不同契约的价值会发生变化）。
安全保证： 定理 3 保证，只要选择器仅在回合边界切换契约，并且始终从预先认证的库中进行选择，系统就能实现端到端的安全。

核心贡献

论文概述了四个主要贡献：

分解与编译： 一种将共享的全局 $LTL_{safe}$ 规范分解为候选局部义务，并将其编译为确定性安全自动机以进行屏蔽合成的方法。
形式化完备性与可恢复性： 基于循环假设-保证推理和契约乘积不动点的、针对去中心化屏蔽的正式保证。作者证明，如果最优安全确定性策略可以由库中的某个契约表示，则该框架可以恢复该策略。
认证下的优化： 一种利用有界认证剖面搜索和折扣 UCB 选择机制来降低保守性的机制。这使得系统能够选择那些能暴露高回报协调行为且不牺牲确定性安全的契约。
实证评估： 在 6 个协作多智能体环境（包括 Flatland、RWARE 和 Pressure Plate）以及 15 种算法变体上进行了广泛评估，证明了该方法的有效性。

结果

实证评估将所提出的 Contract-IPPO 和 Contract-IQL 与标准 MARL 算法（IPPO、IQL、MAPPO）以及各种屏蔽基准（单边屏蔽、集中式屏蔽）进行了对比。

性能： 在单边因子化掩码过于保守的环境中（如 RWARE、Pressure Plate、Connector），基于契约的屏蔽显著提高了团队回报，其表现趋近于集中式屏蔽（如 Shielded-Joint-PPO）的性能。
安全性： 安全性是结构化强制执行的；图 4 中的曲线衡量的是保留的回报，这意味着安全性违规已被掩码本身所阻止。
可扩展性： 在最大的环境中，有界搜索考虑了多达 12,001 个剖面，其中多达 390 个被认证为安全，证明了离线枚举方法的可行性。
具体发现： 在“Pressure Plate”环境中，标准的因子化屏蔽迫使跑步者为了对任何持有者行为保持安全而远离受保护的门区域。基于契约的屏蔽方法通过依赖持有者对留在板上的认证承诺，允许跑步者通过，从而恢复了协调的最优行为。

重要性与主张

论文声称解决了安全 MARL 中去中心化执行与最优协调之间的根本权衡。

恢复协调： 作者断言，其方法可以恢复通常在纯因子化（单边）屏蔽中丢失的“团队最优安全行为”。通过允许智能体依赖同时被认证的循环假设，该系统避免了丢弃安全联合动作的“保守笛卡尔分解”。
端到端安全性： 该框架将奖励适应（学习）与安全性强制执行（屏蔽）分离。学习过程可以在预认证契约的边界内进行探索和优化，确保在训练和部署期间都不会引入不安全行为。
研究范围的局限性： 论文对其局限性进行了客观说明。作者承认，能否恢复全局最优解取决于最优策略在有限契约库中的可表示性。如果契约语言的表达能力不足（例如深度限制 $D$ 过低）以捕捉必要的协调，则系统无法恢复全局最优解。此外，目前的方法依赖于对契约进行详尽（尽管是有界的）枚举，作者建议未来的工作可以探索寻找近优契约的启发式方法，而非进行完全枚举。

总之，本文提出了一种严谨的、经过形式化验证的方法，用于安全 MARL，它使去中心化智能体能够在无需中心化运行时控制的情况下进行有效的协调，弥合了形式化验证与强化学习优化之间的鸿沟。