⚡ electrical engineering

Efficient Dynamic Shielding for Parametric Safety Specifications

本文引入了用于参数化安全规范的动态屏蔽机制，使人工智能控制的自主系统能够在运行时高效地适应不断演化的安全需求，而无需经历传统静态重计算所带来的高昂延迟。

原作者： Davide Corsi, Kaushik Mallik, Andoni Rodriguez, Cesar Sanchez

发布于 2026-08-19

📖 1 分钟阅读☕ 轻松阅读

原作者： Davide Corsi, Kaushik Mallik, Andoni Rodriguez, Cesar Sanchez

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

想象一辆正在陌生城市中行驶的自动驾驶汽车。它的人工智能大脑在学习驾驶方面非常出色，但它并不能始终被信任能够完全掌握交通规则，尤其是在突然出现新障碍物时。为了保障人们的安全，工程师在人工智能与汽车方向盘之间放置了一个数字守护者，称为“屏蔽器”（shield）。这个守护者会监视人工智能想要做出的每一个动作。如果人工智能试图撞向墙壁或行人，守护者会瞬间覆盖其指令，并将汽车转向安全的方向。多年来，这些守护者都是基于一套单一、固定的规则构建的。它们在汽车离开工厂之前就已经设计好了，预设世界会完全符合工程师的预期。但现实世界是混乱且不断变化的。如果出现了一个新的施工区域或道路意外封闭，静态的守护者可能不知道该如何反应，或者更糟的是，它可能需要在行驶过程中被彻底重建。这种延迟可能是致命的。

加州大学欧文分校和西班牙 IMDEA 软件研究所的研究人员开发了一种可以即时适应的新型守护者。他们没有构建一套单一、僵化的规则，而是创建了一个能够理解整个“可能安全规则家族”的系统。你可以把它想象成一个工具箱，而不仅仅是单一的一种工具。在机器人开始移动之前，工程师会为机器人可能遇到的每种类型的障碍物（例如左侧有墙、右侧有墙或前方有墙）准备一个基础安全响应库。这些就是“原子级”的组成部分。当机器人在实际驾驶并看到新障碍物时，系统不会停下来从头设计一个新的守护者，而是会瞬间将匹配当前情况的预制部件拼接在一起，在不到一秒的时间内形成一个新的定制化守护者。这使得机器人即使在周围世界地图发生变化时也能保持安全，其反应速度能与人类驾驶员一样快。

团队用一个在充满静态障碍物的未知领域中导航的机器人测试了这个想法。机器人只能看到其周围一小块正方形区域，就像驾驶员在浓雾中只能看到前方几辆车的距离一样。随着机器人的移动，新的障碍物会在其视野边缘出现，旧的障碍物则会消失。在传统方法中，计算机每次视图变化时都必须暂停并重新计算整个安全计划。研究人员发现，这种旧方法太慢了，耗时比他们的新方法长达五倍。他们使用名为 Mascot-SDS 的原型工具构建的动态系统，只需几分钟即可设计出初始的安全性组件库。一旦机器人开始移动，系统可以在不到一秒的时间内适应新障碍物，有时仅需零点几秒。这种速度至关重要，因为在自动驾驶车辆的世界里，等待甚至几秒钟去应对突发危险，可能意味着安全停车与发生碰撞之间的区别。

该团队解决的一个主要挑战是确保机器人永远不会陷入困境。当机器人在不同时刻之间移动时，由于视野的变化，安全规则也会随之改变。研究人员必须保证机器人现在的行动不会使其陷入下一刻无法采取任何安全行动的境地。为了处理这个问题，他们采用了保守策略：系统假设任何看不见的区域都是危险的。它会建立一个临时安全区，在可见区域周围设置一层“人工围栏”缓冲带。如果机器人移动到了无法立即构建新屏蔽器的位置，系统会继续沿用旧的屏蔽器，直到新的屏蔽器可用。这确保了机器人永远不会处于没有安全路径可循的状态。在实验中，该系统从未出现无法找到安全行动的情况，证明了即使环境在周围发生变化，机器人仍能安全持续移动。

这项工作的成果表明，开发既严谨又灵活的安全系统是可能的。通过将繁重的设计工作分为预规划阶段和轻量化适配阶段，研究人员创造了一种比每次从头解决问题要快得多的方法。他们的模拟显示，虽然标准方法可能需要数秒来计算新的安全计划，但他们的动态方法在眨眼间便完成了。这种效率意味着在未来，自动驾驶系统可以在高度不可预测的环境中安全运行——从繁忙城市中的自动驾驶汽车到灾难区域的探索机器人——而无需在世界每次发生变化时都停下来重新编程。这项工作并不声称已经解决了机器人安全的所有问题，但它展示了一种实用且有效的方法，来应对最常见也最危险的情景：意外。

技术摘要：面向参数化安全规范的高效动态屏蔽技术

问题陈述

传统的针对 AI 控制自主系统的屏蔽方法依赖于为特定的、固定的安全需求而设计的静态屏蔽。虽然这种方法在静态环境中行之有效，但当安全规范因运行环境的变化（例如，机器人由于在未知工作空间中发现新障碍物）而在运行时发生演变时，该范式便会失效。在这种场景下，每一步都重新计算一个屏蔽（“纯在线”方法）会引入致命的延迟；而为所有可能的规范组合预先计算屏蔽（“纯离线”方法）则会因为存在指数级的子集数量而导致计算上不可行。

本文解决了参数化安全规范下的动态屏蔽问题。其目标是设计一种系统，该系统为一组可能的原子安全目标集合进行静态合成，同时具备在运行时动态适配并组合这些组件的能力，以应对被揭示出的特定合取安全规范。

方法论

1. 参数化安全框架

作者将参数化安全规范 $P\text{-Safety}(\mathcal{R})$ 形式化为基于有限原子安全集 $\mathcal{R} = \{G_0, \dots, G_l\}$ 的集合。运行时遇到的实际安全规范是这些原子集的一个任意子集的交集（ $G = \bigcap G_i$ ）。

目标： 合成一个动态屏蔽，使其能够将任何有效的 $G \in P\text{-Safety}(\mathcal{R})$ 映射为一个针对该特定 $G$ 的最小干预屏蔽。

2. 混合离线/在线合成算法

所提出的解决方案通过两阶段法，在离线和在线计算之间取得了平衡：

离线阶段： 为每个原子安全规范 $G_i \in \mathcal{R}$ 计算非阻塞、最大允许（n.m.p.）安全控制器。这需要解决线性数量的合成问题（每个原子集一个），而非指数数量。
在线阶段： 当新的运行时规范 $G = G_{i_1} \cap G_{i_2} \cap \dots$ $G = G_{i_{1}} \cap G_{i_{2}} \cap \dots$ 被揭示时，系统通过动态组合预计算好的原子控制器（ $C^*_{G_{i_1}}, C^*_{G_{i_2}}, \dots$ $C_{G_{i_{1}}}^{*}, C_{G_{i_{2}}}^{*}, \dots$ ）来生成当前步骤的屏蔽。
- 组合机制： 组合过程包含两个步骤：
  1. 乘积运算： 对各个原子控制器的允许控制输入进行求交（ $C^*_{G_{i_1}} \cap C^*_{G_{i_2}} \dots$ ）。
  2. 非阻塞强制执行： 计算该乘积的最大非阻塞子控制器，以确保系统不会进入不存在安全动作的状态。这利用了这样一个性质：对于交集而言，其 n.m.p. 控制器是各单个 n.m.p. 控制器乘积的最大非阻塞子控制器。

3. 基于抽象的控制 (ABC) 实现

为了处理连续状态系统，作者采用了基于抽象的控制框架：

抽象： 使用反馈细化关系 (FRR) 将连续系统近似为一个有限的基于网格的抽象。
符号实现： 合成和组合算法使用二元决策图 (BDD) 进行实现，以高效处理状态空间。
安全交接： 为了解决在安全规范变化时切换屏蔽所带来的挑战（即新屏蔽的定义域可能不包含当前状态），作者提出了一个保守的“安全交接”机制。如果新屏蔽无法立即部署，系统将继续使用之前的屏蔽，直到新屏蔽变得有效，从而确保无限时界的安全性与非阻塞性。

核心贡献

动态屏蔽框架： 提出了一种针对参数化安全规范的新型框架，该框架通过协调离线原子屏蔽合成与轻量级在线适配程序，避免了指数级的离线成本或高延迟的在线重计算。
符号实现： 展示了如何利用基于抽象的控制范式和 BDD 将这些算法进行符号化实现。
安全交接策略： 提供了一种实用的方法，用于保证在未知领域导航任务中，动态适配屏蔽之间的转换过程中的安全性。
性能验证： 通过实验证据证明了该动态方法相对于纯在线基准方法的计算优越性。

实验结果

作者使用 Mascot-SDS 工具实现了一个原型，并在涉及 Dubins 车辆模型的未知领域机器人导航问题上进行了测试。

离线设计： 用于动态屏蔽的离线计算（合成原子控制器）耗时在 2 分钟到 10 分钟 之间，具体取决于抽象粒度。
在线适配： 每一步的在线适配时间范围在不到一秒到几秒之间。
对比： 研究发现，该动态方法比纯在线基准方法（即每一步都从头开始重新计算屏蔽）快 5 倍。
安全性： 所有合成的屏蔽均实现了 100% 的安全性，这与其作为形式化验证安全控制器的构造属性一致。

重要性与主张

本文声称，动态屏蔽为在安全需求并非静态的环境中部署安全关键型 AI 控制器提供了一种切实可行的解决方案。通过将原子安全属性的合成与它们的运行时组合解耦，该方法使得在约束不断变化（如未知障碍物场）的场景中使用经过形式化验证的屏蔽成为可能，且无需承担纯离线或纯在线策略所带来的高昂计算成本。

作者明确指出，其方法依赖于抽象，这意味着最大允许性保证是相对于抽象而非原始连续系统而言的（这是 ABC 中的已知权衡）。他们同时也承认，虽然其安全交接机制是保守的，但它保证了安全性和非阻塞性，尽管未来可以探索更先进的程序。这项工作旨在填补屏蔽文献中关于变化的定性安全规范的空白，这与现有关注改变模型参数或定量阈值的工作有所区别。