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

📄 arXiv: 2605.25346v1 📥 PDF

作者: Keyi Shen, Glen Chou

分类: cs.RO, cs.AI, cs.LG, eess.SY, math.OC

发布日期: 2026-05-25

备注: Robotics: Science and Systems XXII (RSS 2026)

💡 一句话要点

提出并行可微可达性框架，用于学习和规划具有认证神经动力学和控制器的系统

🎯 匹配领域: 支柱一：机器人控制 (Robot Control)

关键词: 可达性分析 神经网络控制 形式化验证 机器人规划 泰勒模型 CROWN GPU加速

📋 核心要点

  1. 现有可达性分析工具在为闭环神经网络系统提供形式化保证方面存在不足，如不可微、过于保守或速度慢。
  2. 论文提出了一个并行化、可微分的可达性框架，结合泰勒模型和CROWN风格的线性边界传播，支持GPU加速和自动微分。
  3. 实验表明，该方法在非抓取操作和四旋翼任务中，能够在有界不确定性下进行在线规划，并保持认证的可达集过近似。

📝 摘要（中文）

本文提出了一种并行化的、可微分的可达性框架，该框架基于JAX，适用于具有解析和基于神经网络(NN)的动力学和控制器的连续和离散时间系统。该框架结合了泰勒模型流管构造与CROWN风格的线性边界传播，通过统一的表示来保留仿射依赖关系，同时支持GPU批处理计算和自动微分。基于此可达性原语，我们开发了(i)一种认证训练方法，鼓励可达性友好的动力学模型和控制器，以及(ii)一种具有基于梯度的细化的可达性感知采样MPC方案。在非抓取操作和四旋翼任务（包括硬件和更高维度评估，高达72D）上的实验表明，在有界不确定性下，该方法能够进行实际的在线规划，同时保持认证的可达集过近似。

🔬 方法详解

问题定义：论文旨在解决在机器人领域中，如何为基于神经网络的动力学模型和控制器提供可靠的形式化保证的问题。现有的可达性分析工具通常存在不可微、过于保守或计算速度慢等问题，难以应用于现代学习和在线规划流程。

核心思路：论文的核心思路是将泰勒模型流管构造与CROWN风格的线性边界传播相结合，构建一个并行化、可微分的可达性分析框架。通过统一的表示来保留仿射依赖关系，从而减少保守性，并利用GPU批处理计算和自动微分来提高计算效率。

技术框架：该框架主要包含以下几个部分：1) 动力学模型和控制器，可以是解析的或基于神经网络的；2) 泰勒模型流管构造，用于计算状态轨迹的过近似；3) CROWN风格的线性边界传播，用于估计神经网络的不确定性；4) 可达性感知的训练方法，用于优化动力学模型和控制器，使其更易于进行可达性分析；5) 可达性感知的采样MPC方案，用于在线规划。

关键创新：该论文的关键创新在于提出了一个并行化、可微分的可达性分析框架，该框架能够有效地处理基于神经网络的动力学模型和控制器，并提供可靠的形式化保证。此外，该框架还支持GPU加速和自动微分，从而提高了计算效率。

关键设计：论文中使用了泰勒模型来近似状态轨迹，并使用CROWN风格的线性边界传播来估计神经网络的不确定性。此外，论文还设计了一种可达性感知的训练方法，通过添加额外的损失函数来鼓励动力学模型和控制器生成更易于进行可达性分析的轨迹。在MPC方案中，使用了可达性信息来指导采样，并使用梯度下降来优化控制序列。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，该方法在非抓取操作和四旋翼任务中，能够在有界不确定性下进行实际的在线规划，并保持认证的可达集过近似。在高维任务（高达72D）和硬件实验中也取得了良好的效果，验证了该方法的实用性和可扩展性。该方法能够有效地处理基于神经网络的动力学模型和控制器，并提供可靠的形式化保证。

🎯 应用场景

该研究成果可应用于对安全性要求较高的机器人应用领域，如自动驾驶、无人机导航、医疗机器人等。通过提供形式化的安全保证，可以提高这些系统的可靠性和安全性，降低事故发生的风险。此外，该方法还可以用于优化机器人控制策略，提高其性能和鲁棒性。

📄 摘要（原文）

Neural network (NN) dynamics models and control policies achieve strong performance in robotics, but providing sound guarantees under uncertainty remains difficult, especially for closed-loop NN systems. Existing reachability tools provide formal over-approximations, yet are often non-differentiable, overly conservative, or too slow for modern learning and online planning pipelines. To address this, we present a parallelizable, differentiable reachability framework in JAX for continuous- and discrete-time systems with analytical and NN-based dynamics and controllers. Our framework combines Taylor-model flowpipe construction with CROWN-style linear bound propagation through a unified representation that preserves affine dependencies while supporting GPU-batched computation and automatic differentiation. Building on this reachability primitive, we develop (i) a certified training method that encourages reachability-friendly dynamics models and controllers, and (ii) a reachability-aware sampling-based MPC scheme with gradient-based refinement. Experiments on non-prehensile manipulation and quadrotor tasks, including hardware and higher-dimensional evaluations (up to 72D), demonstrate practical online planning while maintaining certified reachable-set over-approximations under bounded uncertainty.