精读笔记

Problem Setting

论文标题：Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers（arXiv preprint / 2026）。

这篇论文不是在重新定义 reachability，而是在解决一个更实际的系统问题：如何让 NN dynamics / NN controller 的闭环机器人系统在训练和在线规划时就携带 sound reachable-set over-approximation，而不是部署后再做离线认证。

真正困难点有三层。第一，闭环 NN 系统的 reachable set 需要穿过 analytical ODE、learned discrete dynamics、NN controller 等异质模块，传统 reachability 和 NNV 的表示接口不一致。第二，机器人 MPC 需要对大量 candidate action sequences 反复算 reachable tubes，离线工具的速度和不可微性直接不适用。第三，可达集必须足够紧，否则安全约束会变成无意义的保守约束；但 tightness 通常依赖高阶表示或 splitting，和在线计算矛盾。

以前方法主要卡在接口和用途上：Flow*/POLAR/CROWN-Reach 这类组合工具能做认证，但多是 post-hoc/offline；NNV 能算 NN affine bound，但不处理连续时间 flowpipe；JAX interval/mixed-monotone 工具可微并行，但 interval 表示太容易爆。关键矛盾是：形式化保证需要依赖关系和严谨余项，学习/规划需要固定形状、快速、可微、批量化。这篇论文试图用同一套表示同时满足这两个世界的最低要求。

Motivation

已有路线不够的根因不是缺一个更强的单点 verifier，而是 verification 和 robot learning pipeline 的耦合方式错了。大多数方法把 reachability 当成训练后的审计工具，因此模型训练时完全没有被“可达性友好”这个目标约束。结果是 nominal loss 很低，但 reachable tube 巨大；事后认证失败后只能调模型、重训、再认证。

作者的核心观察是：Taylor model 和 CROWN 本质上都可以看作 affine dependency + remainder/bound 的传播，只是一个来自动力系统 flowpipe，一个来自 NN verification。如果能把二者对齐成同一种可微 tensor representation，就可以把 reachable set 变成 loss、constraint、MPC cost，而不只是证书。

关键缺口是一个 differentiable reachability layer：它要 sound、要保留 affine dependencies、要能处理 CT/DT 和 NN components、还要能 GPU batch。论文的动机非常 engineering-realistic：不是证明一个更漂亮的 reachability theorem，而是把已有 formal tools 改造成现代 learning/planning stack 可调用的 primitive。

Core Idea

核心思想可以概括为 representation alignment：用固定形状的 linear / quasi-quadratic Taylor model 作为全局中间表示，把 analytical dynamics 的 TM flowpipe 和 neural network 的 CROWN affine bounds 接到同一条信息流里。这样，连续时间部分用 Picard/TM 传播，神经网络部分用 CROWN 认证，但两者交换的不是粗糙 interval，而是保留相关性的 affine object。

本质区别在于它改变了模块之间的信息接口。prior 中常见做法是 TM 到 NN 前先 intervalize，NN bound 后再作为 interval 输入后续 dynamics；这一步会系统性丢失 cross-state correlation，长 horizon 下保守性放大。本文强制 CROWN 输出共享斜率的 affine bounds，并把 NN output 投影回 linear TM，使依赖关系可以跨 analytical/NN 边界延续。这个设计牺牲了部分 CROWN bound 自由度和高阶 TM 表达力，但换来了固定形状、JAX-friendly、可微、可批量计算。

它引入的 inductive bias 是：训练出来的 dynamics/controller 不仅要预测准，还要对有界扰动有小的 certified amplification。换句话说，模型被显式偏置到 verification-friendly 的函数类附近。这一点比单纯加 Lipschitz regularization 更贴近 downstream reachable-set 目标。

Method

1. 固定形状 Taylor model：解决 classical TM monomial explosion 和 GPU 不友好的问题。作者把 polynomial part 限制在线性或准二次形式，核心变化是从高表达力 symbolic polynomial 转向 dense tensor affine propagation。它不是理论上最强的 TM，而是可被 JAX/JIT/AD 消费的 TM。

2. TM flowpipe for analytical CT dynamics：解决连续时间 dynamics 的 sound propagation。Picard iteration + interval remainder validation 提供形式化余项，preconditioning / reparameterization 控制 wrapping。这里的关键不是新 flowpipe theory，而是把它改写成固定形状矩阵操作，使其能作为 batched computation 出现在 learning/planning loop 中。

3. TM-CROWN interface：解决 NN component 和 TM flowpipe 的表示断裂。对 linear TM input 做 reparameterization，把 NN 看成作用在 latent box variables 和 TM remainder 上的网络，再用 CROWN 求 affine bound；通过 shared-slope constraint 把上下界重新合成为 linear TM。它的必要性在于避免 intermediate interval relaxation，这是 tightness 的关键机制。

4. Closed-loop CT reachability：解决 NN feedback controller 与 ODE 交替的问题。每个 control interval 先对 controller output 做 CROWN certification，再把控制作为 zero-order-hold augmented state 进入 TM flowpipe。机制上是“认证 controller map + 传播 controlled dynamics”的交替组合，不是端到端求 closed-loop exact flow。

5. Certified training：解决模型 nominally accurate 但 reachable set 巨大的问题。reachable tube width/volume proxy 直接进入 loss，迫使 dynamics/controller 在训练数据附近学习更小的 certified sensitivity。curriculum 主要是优化稳定器，不是核心理论贡献。

6. Reachability-aware MPC：解决在线 action selection 不考虑 uncertainty amplification 的问题。采样候选轨迹时同时计算 nominal cost 和 reachable-set penalty，再对优选解做 gradient refinement。核心变化是把 reachability 从 constraint checking 变成 action scoring 的一部分。

Key Insight / Why It Works

最重要的 insight 是：很多机器人 NN 系统的认证困难，并不是因为真实系统的 reachable set 必然巨大，而是因为表示接口反复丢失依赖关系，导致 over-approximation 人为膨胀。本文通过统一 affine representation 把这种损失推迟或减少了。因此它有效的第一来源是 representation alignment，而不是某个单独算法更强。

第二个有效来源是把 reachability objective 放进训练。certified training 实际上在学习一个更小局部增益、更少扰动放大的模型/控制器；它不一定更真实，但更容易被当前 verifier 证明。这是一个非常实用但也需要警惕的点：模型可能变得 verification-friendly，而不是 physics-faithful。论文显示 nominal performance 没明显下降，但没有充分证明在复杂分布外接触动力学中也成立。

第三个来源是 scaling：JAX、固定形状 tensor、GPU batch、parallel splitting、batched candidate MPC。这部分很重要，但主要是系统工程贡献。若没有这些，方法无法进入 MPC；但若只看理论 tightness，它未必比最强离线工具更优。论文的价值在于把“足够紧的 sound bound”做到“足够快且可微”。

哪些是核心贡献：TM-CROWN shared affine interface 和 differentiable reachable-set-as-objective 是核心；固定形状 TM 是必要工程抽象；curriculum、log volume loss、gradient refinement、input splitting更多是让系统可用的辅助。

哪些增益归因不清：实验中 certified model + reachability-aware planner + splitting/refinement 往往同时出现，因此成功率提升到底来自更好的模型、更保守的 planner、还是 disturbance setting 与 reachable penalty 匹配，文中未充分说明。长 horizon CT 中仍出现 infinite-volume / conservatism blow-up，说明核心表示并没有根治 wrapping 和 nonlinear accumulation。

Relation To Prior Work

这篇工作最接近 Flow*/POLAR/CROWN-Reach 这条“Taylor model reachability + NN bound propagation”谱系，也和 immrax/GoTube 这类 JAX-based differentiable reachability 工具有交集。它不是从零提出新的 reachability calculus，而是把已有两类技术重新组织到一个可微、GPU-parallel、robotics-facing 的计算图里。

与 POLAR/CROWN-Reach 的本质差异在接口和使用方式：prior 更偏离线验证，且常通过 interval-only 接口连接 TM 与 NN；本文强调统一 linear-TM 表示，尽量保留 affine dependencies，并使结果可反传到模型和 action。这个差异是实质性的，因为它改变了 reachability 在系统中的角色：从 post-hoc certificate 变为 optimization primitive。

与普通 CROWN/αβ-CROWN 的差异是动态系统语境：CROWN 负责 NN static map 的 bound，本文把它嵌入 time propagation 和 closed-loop execution。与 classical robust MPC/funnel/HJ/SOS 的差异是可处理 learned NN components 且更适合 batch planning，但保证也更依赖 over-approximation 和模型假设。

看似新的部分中，Taylor flowpipe、CROWN bound、reachability regularization、sampling MPC 都不是新思想；真正新增的信息是把它们用 affine-preserving representation 串起来，并证明这在现代机器人 learning/planning loop 中有足够好的速度-紧度折中。

Dataset / Evaluation

实验覆盖 T-pushing、真实硬件 T-pushing、quadrotor、6-quadrotor swarm、10-joint planar arm，任务选择基本覆盖了 manipulation、aerial control、moderately high-dimensional dynamics。真实世界部分存在，但更像 feasibility demo，不是严格的 real-world safety validation。

评价确实支持两个核心 claim：第一，JAX/GPU differentiable reachability 可以足够快地用于在线或准在线规划；第二，reachability-aware training/planning 可以缩小 certified tubes 并提升大扰动下的稳定性。尤其是对比 interval/mixed-monotone 工具时，tightness 优势符合方法机制。

但 evaluation 的边界也明显。任务仍相对结构化，uncertainty 是预设 bounded box，模型误差的真实校准没有作为主实验展开。T-pushing 虽有接触，但 learned dynamics 和 planner 的 guarantee 主要相对于模型；真实接触中的 hybrid discontinuity 没有被严格覆盖。高维实验更多证明 runtime scaling 和 reasonable conservativeness，不等于证明复杂高维闭环系统长期可认证。

此外，文中没有足够 ablation 来拆开 shared-slope CROWN、TM representation、certified training、splitting、gradient refinement 各自贡献。benchmark 支持系统有效，但对“哪个机制真正导致成功”的证明不够干净。

Limitation

最根本限制是 guarantee 的对象。论文给的是相对于 analytical / learned dynamics 和指定 bounded disturbance 的 reachable-set over-approximation；如果 learned dynamics 本身错，certificate 仍可能是模型内自洽而非真实安全。作者提到可用 conformal prediction 加 model-error bounds，但这不是本文主要完成的部分。

第二，scalability 有明确上限。固定 affine/quasi-quadratic TM 的内存至少 O(n^2)，高维强耦合系统会迅速吃掉 tightness；进一步提升只能靠 splitting，而 splitting 本质上是指数型 trade-off 的工程缓解。72D swarm 的结果有意义，但该系统结构较规整，不能直接外推到高维接触、多刚体、视觉闭环。

第三，连续时间长 horizon 仍难。实验中 CT quadrotor 长 horizon conservatism 明显增长，甚至需要对关键姿态维度 splitting 才缓解。这说明方法没有消除 wrapping effect，只是通过 better interface 和 GPU parallelism 推迟爆炸。

第四，shared-slope CROWN 是双刃剑。它让 NN output 可回到 linear TM，但也限制了上下界斜率自由度，可能在某些网络/输入域下比普通 CROWN 更松。文中未充分说明这个约束的 tightness 代价。

第五，certified training 可能学习 verifier-friendly dynamics，而不是更好的真实 dynamics。reachable-set loss 会惩罚 sensitivity，这可能压低模型局部增益、平滑掉真实不连续或接触效应。若数据覆盖不足，核心能力可能主要来自训练分布覆盖，而非真正泛化。

第六，reachability-aware MPC 的长期 reasoning 能力有限。它仍是有限 horizon sampling-based MPC + penalty，不是形成全局 safety strategy；在复杂障碍、长时约束、不可逆失败状态下，局部 reachable penalty 可能只是让短期动作更保守。

Takeaway

• 1. 最值得记住的是“reachability as differentiable primitive”：形式化方法如果不能进入训练和规划 loop，就只能做昂贵的事后审计；本文展示了把 certificate object 变成 loss/cost 的一条可行路线。
• 2. 表示接口比单个 verifier 更关键。
• TM 和 CROWN 的组合并不新，但避免 interval-only stitching、保留 affine dependency，是 tightness 和可用性的核心。
• 3. 未来这条线大概率会沿着三个方向演化：更强的 dependency-preserving representation、更系统的 model-error calibration、更适合 hybrid/contact dynamics 的可微 reachability。

一句话总结

这篇论文是把 Taylor-model reachability 与 CROWN verification 通过 affine-preserving、JAX-friendly 表示重组为可微机器人学习/规划 primitive 的系统型工作，真正贡献在于让 certified reachable sets 从离线验证对象变成训练和 MPC 可优化的对象。