⚡ electrical engineering

Neural Cooperative Reach-While-Avoid Certificates for Interconnected Systems

本文提出了一种可扩展的框架，该框架利用带有动态局部向量控制李雅普诺夫与障碍函数的神经协同到达-同时避障证书，为大规模互联系统中的神经网络控制器提供形式化的安全性与稳定性保证，并通过多机器人及车辆编队实验进行了验证。

原作者： Jingyuan Zhou, Haoze Wu, Kaidi Yang

发布于 2026-01-29

📖 1 分钟阅读☕ 轻松阅读

原作者： Jingyuan Zhou, Haoze Wu, Kaidi Yang

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

宏观图景：教一群“蜂群”跳舞而不发生碰撞

想象一下，你正在试图教一大群鸟（或是一支自动驾驶车队）如何协同飞行。它们需要同时完成两件事：

到达目的地（生存性/Liveness）：它们都必须到达一个特定的位置。
避免碰撞（安全性/Safety）：它们绝不能互相撞击或撞到障碍物。

问题在于，这些“鸟儿”是由神经网络（AI 大脑）控制的。虽然 AI 擅长学习复杂的动作，但它是一个“黑盒”。我们不知道它为什么做出某个决定，也无法轻易证明它不会突然决定撞上一棵树。

这篇论文介绍了一种构建这些 AI 控制器的新方法，使得我们可以从数学上保证它们在数百个智能体协同工作时，既能成功达成目标，又不会发生碰撞。

核心问题：“黑盒”与“大群体”

1. 黑盒问题：
传统的安全规则就像一位严格的老师，在你迈出每一步之前都要进行检查。但 AI 控制器就像一位即兴演奏的爵士乐手；它们灵活但难以预测。现有的方法试图在 AI 训练过程中“软性”地鼓励安全性，但这就像是告诉司机“请不要撞车”，却并没有真正踩下刹车。如果 AI 感到困惑，它仍然可能发生碰撞。

2. 规模问题：
检查单个机器人的安全性很难。而检查 100 个机器人在一起是否安全，就像是在解一个谜题，其中每个碎片都在每一秒钟都在改变形状。目前大多数方法要么太慢，要么太简单，无法处理大型群体。它们往往忽略了智能体之间是如何相互帮助（或相互阻碍）的。

解决方案：“神经协作到达-避障证书”（Neural Cooperative Reach-While-Avoid Certificates）

作者提出了一种名为 Neural Cooperative Reach-While-Avoid (Co-RWA) Certificates 的新系统。你可以把它想象成给集群中的每个智能体发了一本个人安全手册和一份团队契约，且这两者在数学上都是经过证明行之有效的。

以下是该方案三个主要部分的运作方式：

1. “动态邻域”（局部圈子）

在一个巨大的群体中，你无法与所有人交流。你只能与紧挨着你的那些人交流。

类比： 想象一个舞池。你不需要知道房间另一头的人在哪里；你只需要知道紧邻你的那三个人在哪里，就能避免撞到他们。
论文的创新点： 该系统创建了一个“状态相关邻域”。随着智能体的移动，它们的邻居圈也在动态变化。AI 只观察其紧邻的局部圈子来做出决策，这使得数学计算变得更快、更容易解决。

2. “向量证书”（团队计分卡）

系统没有使用一个针对整个群体的巨大且复杂的规则，而是使用了向量控制李雅普诺夫与障碍函数（Vector Control Lyapunov and Barrier Functions）。

类比： 想象一支运动队。与其让一名教练对着整个体育场大喊大叫，不如让每位球员都持有一张小小的计分卡。
- 李雅普诺夫部分（目标）： 这是一张计分卡，上面写着：“如果我保持这样移动，我保证会离目标越来越近。”它确保团队最终能赢得比赛。
- 障碍函数部分（安全）： 这是一张计分卡，上面写着：“如果我待在这个区域内，我保证不会撞到任何人。”它确保团队永远不会因为碰撞而损失队员。
神奇之处： 这些计分卡是基于“向量”的，这意味着它们被分解成了许多细小的局部部分。这使得系统可以通过检查 100 个简单的小规则，来验证 100 个机器人整体的安全性，而不是去处理一个不可能实现的庞大规则。

3. “CEGIS 循环”（练习与测试周期）

他们如何训练 AI 来遵循这些规则？他们使用了一种称为**反例引导的归纳合成（Counterexample-Guided Inductive Synthesis, CEGIS）**的方法。

类比： 想象一个正在学习驾驶的学生。
1. 学生驾驶（训练 AI）。
2. 一位严格的考官（验证器）寻找错误。
3. 如果考官发现了一个错误（一个汽车差点撞车的“反例”），他会将这个错误展示给学生。
4. 学生专门针对这个错误进行练习，直到做对为止。
5. 考官再次检查。
- 这个循环不断重复，直到考官无法再找到任何错误。此时，该学生就被“认证”为安全了。

4. “结构复用”（乐高技巧）

这是该论文实现规模化扩展的秘密武器。

类比： 假设你为一个小型的 3 人团队构建了一个完美的、安全的机器人。现在你需要为一个 100 人团队构建机器人。与其从头开始，不如观察这个 100 人团队并意识到：“嘿，这里的这 5 个人组成的结构，和我们那个小型的 3 人团队完全一样！”
论文的创新点： 他们使用了子结构同构（Substructure Isomorphism）。如果一个大系统的某个小部分看起来与他们已经解决过的小系统一致，他们就可以直接将小系统的安全规则和控制器进行复制粘贴。他们不需要重新训练或重新验证整个系统。这就像是用预制好的乐高积木来搭建更大的城堡。

他们证明了什么？

作者在两个场景中测试了该系统：

多机器人协作： 一组机器人协同移动。
车辆编队： 一列紧密编队的自动驾驶汽车。

结果显示：

系统成功引导智能体到达了目标。
系统保证即使存在建模误差（不完美的数据），也不会发生碰撞。
通过使用“复制粘贴”（结构复用）方法，他们可以将规模扩展到大型系统，而不会导致计算机崩溃或计算时间过长。

总结

这篇论文解决了如何信任大规模群体中 AI 的问题。它通过以下方式实现：

将群体分解为局部邻域。
为每个智能体提供一份经过数学证明的“安全契约”。
通过不断测试并修复错误来训练 AI。
复用小规模群体的解决方案，从而瞬间解决大规模问题。

其结果是，提供了一种部署 AI 智能体集群的方法，使它们不仅“聪明”，而且在形式上保证是安全且成功的。

技术摘要：互联系统中的神经协作趋向-避障证书

1. 问题陈述

本文解决了在由神经网络策略控制的大规模互联系统中，提供稳定性与安全性形式化保证这一根本挑战。虽然基于学习的控制器（如深度强化学习）在处理智能交通和机器人等应用中的复杂、不确定动力学方面表现出色，但其“黑盒”性质阻碍了严谨的验证。现有的形式化方法通常依赖于精确的系统模型，或者在规模扩展方面表现不佳；而目前的神经证书方法通常忽略了多智能体系统中固有的协作交互和动态邻域结构。

本文所阐述的具体问题是**多智能体趋向-避障（Multi-Agent Reach-While-Avoid, MARWA）**任务。一组由 $q$ 个智能体组成的团队必须完成以下任务：

趋向（Reach）： 收敛至目标集 $X_{i,G}$ （活性/存活性）。
避障（Avoid）： 绝不进入不安全集 $X_{i,U}$ （安全性）。
协作（Cooperate）： 在有限的通信范围内运行，其中智能体仅与感知半径 $R_c$ 内的邻居进行交互，且这些邻域随状态动态变化。

由于高维联合状态空间的限制，标准的标量李雅普诺夫函数（Lyapunov functions）和障碍函数（Barrier functions）被认为是处理大规模系统时难以实现的。

2. 方法论

作者提出了一个以神经协作趋向-避障（Co-RWA）证书为核心的框架，该框架将理论控制保证与可扩展的神经网络合成相结合。

A. 理论基础：DL-VCLFs 与 DL-VCBFs

为了处理去中心化和动态交互，本文引入了两种新型向量值证书概念：

动态局部向量控制李雅普诺夫函数（DL-VCLFs）： 用于确保全局指数稳定性（GES）。与标量函数不同，DL-VCLF 使用向量 $V(x) = (V_1, \dots, V_q)$ ，其中每个分量 $V_i$ 取决于局部状态和动态邻域指示器 $A_i(x)$ 。其稳定性条件受 Metzler 和 Hurwitz 矩阵 $\Lambda$ 控制，确保每个智能体的李雅普诺夫函数的衰减率取决于其当前邻居的状态。
动态局部向量控制障碍函数（DL-VCBFs）： 用于确保安全性（前向不变性）。与 DL-VCLF 类似，它们使用向量 $h(x)$ 和 Metzler 矩阵 $\Upsilon$ 来强制系统即使在邻域结构发生变化时，仍保持在安全集 $C = \prod C_i$ 内。

两者共同构成了 Co-RWA 证书，提供了去中心化的保证，使智能体能够在协作趋向目标的同时避免碰撞。

B. 可扩展合成与验证框架

本文开发了一个**反例引导的归纳合成（CEGIS）**循环，用于联合训练控制器和证书：

训练公式化： 将问题转化为约束优化问题，旨在最小化平衡以下各项的损失函数：
- 对标称控制器（如来自 RL 的控制器）的模仿。
- DL-VCLF 条件的可行性（李雅普诺夫衰减）。
- DL-VCBF 条件的可行性（障碍安全性）。
- 严格的安全裕度（在安全区域内 $h \geq \epsilon_0$ ，在不安全区域内 $h < 0$ ）。
包含建模误差的验证： 由于验证工具是在离散时间模型上运行的，作者推导出了考虑以下因素的充分条件（定理 3）：
- 离散化误差： 连续动力学与欧拉近似之间的差异。
- 近似误差： 真实动力学与神经网络代理模型之间的差异。
  这些误差被界定并传播到证书不等式中，从而确保如果离散时间神经模型满足条件，则真实的连续时间系统在安全性与稳定性方面均得到保证。
迭代细化： 如果形式化验证器找到了违反证书的反例，则增加数据并重新训练网络。

C. 用于可扩展性的结构重用

为了克服验证大规模系统的计算瓶颈，作者引入了结构重用机制。

子结构同构（Substructure Isomorphism）： 定义为一种映射，其中较小的子系统与较大的系统共享相同的局部动力学和邻域拓扑结构。
可迁移性： 定理 4 证明，如果一个小系统与一个大系统是结构同构的，那么学习到的控制器和证书可以直接迁移，无需重新训练或重新验证。这实现了从小型测试平台到大规模部署的扩展。

3. 核心贡献

神经 Co-RWA 证书： 开启了通过动态局部向量函数显式建模协作动力学和状态相关邻域的神经证书研究，提供了指数稳定性和安全性的理论保证。
可扩展验证框架： 开发了一个统一的训练与验证流水线，将建模误差（离散化和近似误差）纳入验证条件中，确保了底层连续系统的形式化保证。
结构重用机制： 提供了一种在结构同构系统之间迁移控制器和证书的方法，显著提升了大规模互联系统的可扩展性。
实证验证： 通过多机器人协作和车辆编队场景验证了该框架，展示了具有强控制性能的 Co-RWA 表现。

4. 结果与验证

该方法通过广泛的数值模拟得到了验证：

场景： 框架在全向移动机器人和车辆编队场景中进行了测试。
性能： 结果表明，合成的控制器成功确保了智能体在严格避免不安全区域（碰撞）的同时，达到了其目标集。
可扩展性： 结构重用机制允许将证书从较小的系统迁移到较大的系统，验证了该框架可以在不产生过高计算成本的情况下处理大规模互联系统。
验证： 在验证过程中加入误差界限，确保了尽管使用了神经网络代理和离散时间近似，形式化保证依然成立。

5. 意义与主张

本文声称解决了在部署用于安全性至关重要的规模化系统中的学习型控制器时面临的关键空白。其重要性在于：

超越了“软”约束（损失函数），实现了在协作多智能体设置下对稳定性与安全性的形式化、严谨的保证。
解决了此前阻碍大规模互联系统形式化验证的可扩展性瓶颈，这主要通过引入向量值证书和结构重用得以实现。
提供了一个实用的合成循环（CEGIS），弥合了理论控制论与现代深度学习之间的鸿沟，使得训练出即使在存在建模不确定性时也能证明安全且稳定的神经控制器成为可能。

作者将这项工作定位为在复杂、现实世界环境中安全部署自主系统迈出的重要一步，在这些环境中，协作与安全性至关重要。