⚡ electrical engineering

Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers

本文在 JAX 中引入了一种可并行化、可微分的可达性框架，该框架将泰勒模型流管与 CROWN 风格的界传播相结合，以支持在不确定性条件下对神经网络动力学和控制器的认证训练及基于梯度的规划。

原作者： Keyi Shen, Glen Chou

发布于 2026-05-26

📖 1 分钟阅读☕ 轻松阅读

原作者： Keyi Shen, Glen Chou

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

想象一下，你正在教机器人执行一项精细任务，比如将一个T形物体推过桌面，或驾驶无人机穿过狭窄缝隙。你使用一个“大脑”（神经网络）来帮助机器人决定如何移动。这个大脑极其擅长根据过往经验预测接下来会发生什么。

然而，存在一个大问题：如果机器人出现微小偏差怎么办？ 也许地面很滑，或者某个传感器对距离的读数出现了微小误差。在现实世界中，这些小错误会像滚雪球一样扩大。第一步的微小失误，可能导致第十步发生碰撞。

传统上，工程师有两种选择：

完全信任机器人：这速度快，且大多数情况下有效，但如果出现问题，机器人可能会因为未考虑“万一”的情况而撞毁。
进行形式化数学验证：通过计算所有可能结果来确保安全，但这过程过于缓慢且复杂，无法在机器人实际移动或学习时使用。

本文介绍了一种名为DiffReach的新工具，它像一个超快速安全计算器，能够实时运行。以下是其工作原理，借助一些日常类比来说明：

1. “影子”类比（可达性）

想象机器人是一个在雾中森林行走的人。你并不确切知道他在哪里，只知道他位于某个已知点周围的小圆圈内。

旧方法：为了安全，你可能会在人身后画出一个巨大且模糊的云团，每走一步它就变得更大，最终覆盖整片森林。这很安全，但过于令人担忧，因为它即使在人远离树木时也会说“他可能会撞到树”。
本文的方法：DiffReach 在机器人周围绘制一个紧密且灵活的影子。随着机器人移动，这个影子会拉伸和扭曲，精确跟随机器人的路径，但绝不会变得比必要更大。它会告诉你：“如果机器人从这里开始，它可能会出现在这个特定形状内的任何位置，但绝不会超出此范围。”

2. “流水线”类比（并行与可微分）

通常，计算这些影子就像单人在纸上做数学题，耗时极长。

创新之处：作者使用JAX（一个强大的计算引擎）构建了该工具。想象一下，不是一个人，而是拥有一个拥有数千名工人（GPU）的工厂，他们同时执行数学运算。
可微分：这是神奇的部分。通常，安全检查就像一个“停止标志”——你进行检查，如果不安全就停止。你无法利用这个停止标志来教导机器人如何更好地驾驶。DiffReach 则像一条平滑的滑道。因为数学是“可微分”的，机器人可以观察影子，看到哪里变得过宽，并立即调整其“大脑”（神经网络），使影子变得更紧凑。它将安全从“停止标志”转变为“方向盘”。

3. 双引擎结构

本文将两种不同的数学技术融合为一个无缝机器：

泰勒模型（解析部分）：对于机器人中可用物理规律理解的部分（如无人机的空气动力学），他们使用一种能像平滑曲线那样预测路径的方法。
CROWN（神经网络部分）：对于“大脑”部分（神经网络），他们使用一种检查 AI 猜测极限的技术。
统一化：他们创建了一种通用语言（“统一 TM-CROWN 接口”），使这两种不同方法能够相互沟通而不损失精度。这就像在物理学家和 AI 专家之间进行对话翻译，而不丢失任何细节。

4. 实际成果

作者不仅构建了该工具，还用它完成了两项具体工作：

认证训练：他们教导机器人的“大脑”具备“安全意识”。大脑不再仅仅学习如何击中目标，而是学会保持其“影子”尽可能小。如果影子变得过大（意味着机器人不确定），训练过程就会对其进行惩罚。结果是：机器人不仅同样擅长完成任务，而且在出错时更加安全。
安全规划（MPC）：他们使用该工具实时规划路径。
- 在仿真中：他们在机械臂和无人机群（高达72维运动空间！）上测试了该工具。该工具比之前的方法快100倍，同时保持了紧密的安全边界。
- 在现实世界中：他们在真实机械臂推动T形物体的任务中进行了测试。机器人成功规划了动作并避开了障碍物，即使环境略有不可预测性。

核心结论

本文提出了一种方法，使机器人能够同时兼具智能与安全。通过使安全检查速度快到足以在显卡（GPU）上运行，并灵活到能够融入学习过程，他们让机器人能够从经验中学习，同时不忘警惕“万一”的情况。

他们并未声称：

他们并未声称这已适用于医疗手术或公共道路上的自动驾驶。
他们并未声称它解决了所有安全问题（他们承认它在处理极长时间跨度或复杂物理接触（如弹跳球）方面仍存在困难）。
他们严格专注于机器人任务，如推动物体和飞行无人机。

技术摘要：用于学习与规划的并行可微可达性分析，结合认证神经动力学与控制器

问题陈述

神经网络（NN）动力学模型与控制策略已在机器人领域展现出强大的实证性能，特别是在解析建模不可行的复杂环境中。然而，在不确定性条件下为闭环神经网络系统提供鲁棒的安全保证仍是一项重大挑战。经典的可达性分析通过可达集过近似提供形式化保证，但往往扩展性差、难以处理神经网络组件，且产生的边界过于保守。相反，现代神经网络验证（NNV）方法（如 CROWN）虽能良好扩展至大型网络，但主要设计用于静态验证，缺乏对连续时间动力学的支持，且通常不可微。

因此，可达性分析通常仅限于事后认证，导致非认证训练、验证失败与重新训练之间形成高成本循环。亟需一种框架，将认证可达性直接集成到机器人学习与在线规划流程中，支持包含解析与基于神经网络的组件的连续及离散时间系统，同时保持可微性与高效性。

方法论

作者提出了 DiffReach，这是一个基于 JAX 实现的、可并行化的可微可达性框架。其核心创新在于一种统一表示，将用于解析动力学的 泰勒模型（TM）流管构建 与用于神经组件的 CROWN 风格线性界传播 相结合。

1. 统一表示（Taylor-CROWN 接口）

为实现 GPU 批处理计算与自动微分，该框架采用固定形状的泰勒模型表示。可达集不再表示为可变大小的多项式，而是表示为：
$F(z) = c + Az \oplus I \quad \text{或} \quad F(z) = c + Az + B \tau z \oplus I$
其中 $z$ 将状态与时间联合增强， $c$ 为常数， $A$ 和 $B$ 为捕捉仿射与准二次依赖关系的矩阵， $I$ 为区间余项。该表示在无需中间区间松弛的情况下保留了仿射依赖关系。

神经组件：框架利用 CROWN（通过 jax_verify）计算神经网络的仿射界。一项关键贡献是在 CROWN 中实施 共享斜率约束，确保上下界共享相同的线性项。这使得神经网络输出可表示为线性泰勒模型，从而保持与解析动力学流程的兼容性。
连续时间（CT）系统：对于带有神经网络反馈控制的连续时间系统，框架在以下两步间交替进行：
1. 控制器认证：利用 TM-CROWN 接口，根据当前状态的泰勒模型包络认证神经网络控制器的输出。
2. 动力学传播：在控制输入采用零阶保持策略下，利用泰勒模型流管传播系统动力学（解析或神经 ODE）。
离散时间（DT）系统：可达性简化为逐步传播，其中 TM-CROWN 接口在每个时间步认证单步映射。

2. DiffReach-机器人应用

基于 DiffReach 引擎，作者开发了两种面向机器人的方法：

认证训练：一种针对神经动力学与控制器的训练方法，在标准预测或跟踪损失基础上增加 可达性感知正则化项。该项惩罚在有界不确定性下认证可达集的体积增长。为稳定训练，采用课程学习策略，逐步增加展开时域并减小扰动半径。
可达性感知 MPC：一种将认证可达集集成到在线规划中的基于采样的模型预测控制（MPC）方案。规划器优化包含任务目标以及对不安全轨迹或过大可达集惩罚的成本函数。并行化允许高效评估大量候选轨迹，并对顶级候选应用基于梯度的细化以进一步降低保守性。

主要贡献

并行可微可达性框架：一种基于 JAX 的统一表示，结合泰勒模型流管与 CROWN 风格界传播，适用于包含解析与基于神经网络的动力学/控制器的连续及离散时间系统。
认证训练方法：一种利用可微可达集目标提升神经网络组件在不确定性下鲁棒性的学习方法，鼓励生成“可达性友好”模型。
可达性感知 MPC：一种在线规划方案，将认证可达集集成到基于采样的 MPC 中，并结合基于梯度的细化，实现“构建即验证”的规划。
实验验证：在非抓取操作（T 型推）与四旋翼任务上进行了全面评估，包括硬件实验与高维评估（高达 72 维），展示了具备认证保证的实际在线规划能力。

结果

该框架在 RTX 4090 GPU 上从多个维度进行了评估：

效率与紧致性：与最先进的离散时间（CROWN）与连续时间（immrax）基线相比，DiffReach 实现了相当的可达集紧致性，同时在离散时间系统上比 CROWN 快约 100 倍。对于连续时间系统，它产生的可达集比 immrax 显著更紧致，后者常因数值溢出和无限体积管而失效。
可扩展性：该框架有效扩展至高维系统，包括 6 架四旋翼编队（72 维状态）与 10 关节平面机械臂（40 维状态）。虽然内存按 $O(n^2)$ 扩展，但由于 GPU 并行矩阵运算，运行时间扩展性良好。
认证训练：经可达性正则化训练的模型在标称性能上与标准训练相当，但产生了 显著更紧致的可达集。这些集与采样的下界体积高度吻合，而非认证模型则产生松散且难以验证的预测。
鲁棒规划：在有界扰动下的 MPC 实验中，可达性感知规划器保持了高成功率并满足约束，而使用非认证模型的普通 MPC 在较大扰动下（如 T 型推任务中的意外接触）显著失效。
硬件部署：该系统部署于 Kuka iiwa 平台进行 T 型推操作，在线运行频率约为 10 Hz（含细化时为 5 Hz），证明了将可微可达性集成到实时机器人控制中的可行性。

意义与主张

本文主张 DiffReach 通过提供一种 可微、GPU 加速的可达性原语，弥合了形式化验证与机器人学习之间的鸿沟。与以往仅限于离线验证的方法不同，该框架允许可达集目标直接指导神经动力学与控制器的训练及在线规划的执行。

作者强调，其方法实现了 “构建即验证” 的学习与规划，减少了对昂贵事后认证循环的依赖。通过在单一计算图中统一泰勒模型与 CROWN，该方法保留了仿射依赖关系，并支持连续与离散时间系统，解决了当前神经网络在环分析工具中的关键局限。

文章最后承认了当前的局限性，如长时域保守性挑战以及混合/接触丰富动力学的困难，但指出该框架激发了未来关于可扩展可微可达性及形式化验证、机器人学习与控制之间更紧密整合的研究。