💻 computer science

Certifying Plans under Model Mismatch: A Trilemma for Reachability from Scarce Data

本文确立了在数据匮乏且存在模型失配的情况下，对控制计划进行认证时存在的一个基本三难困境，即任何可靠的确定性认证器都必须在牺牲轨迹包含性、接受任意大的不确定性或限制模型误差行为之间做出权衡，并提出了 ForeReach 方法，通过构建集合成员包络和分带状管状区域，在数据支持不足时安全地拒绝认证。

原作者： Yanliang Huang, Zhen Zhang, Ahmad Hafez, Wenyuan Wu, Peng Xie, Zhuoqi Zeng, Amr Alanwar

发布于 2026-08-04

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Yanliang Huang, Zhen Zhang, Ahmad Hafez, Wenyuan Wu, Peng Xie, Zhuoqi Zeng, Amr Alanwar

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

想象一下，你正在教一个机器人开车。你不能直接把它丢到真实的公路上；那太危险了。相反，你在一个视频游戏模拟器中训练它。这个模拟器很棒，但并不完美。游戏中的物理法则可能与现实世界略有“偏差”——也许轮胎的抓地力稍有不同，或者风吹动车子的方式在游戏中并未被预见。这种游戏世界与现实世界之间的差异被称为“模型误差”。

现在，假设机器人学到了一个很酷的新驾驶动作。在让它在真实街道上尝试这个动作之前，你需要一名安全检查员来核查：“如果机器人这样做，它会撞车吗？”检查员手里有一份模拟器规则的地图，但他们只有关于真实车辆实际表现的少量零散笔记。这些笔记就像是孤立的快照：“在这个特定的速度和转弯处，车子行驶到了这里。”大问题在于：仅凭这几张快照，我们能否保证机器人的安全性，即使机器人在一个完全没有笔记记录的地方尝试动作？这篇论文探讨了正是这样一个谜题，探索了当我们对现实世界了解极少时，我们所能知的极限。

研究这些课题的研究人员（与慕尼黑工业大学和海南师范大学合作）发现了一个基本的“三难困境”——一个你无法全都要的局面。他们证明了，如果你试图仅用一些零散的数据点来认证机器人的计划，你会面临三个不可能的选择：

绝对安全（可靠性/Sound）： 你的安全保证必须涵盖现实世界可能表现出的每一种方式。
有用（信息量/Informative）： 你的安全区域不应该大到覆盖整个宇宙；它需要足够紧凑，以便告诉你机器人是否真的会撞墙。
开放心态（无限制/Unrestricted）： 你不应该在你尚未观察到的地方，凭空编造关于现实世界如何运作的规则。

论文证明，你只能在这三者中选二。如果你拒绝对未知领域编造规则（保持模型“无限制”），并且要求绝对安全，那么你的安全区域会变得无限宽广。这就像一名保安，看到沙滩上留下了一些脚印，为了百分之百确定没有入侵者溜进来，他决定假设入侵者可能出现在整个城市里的任何地方。这是一个安全的假设，但对于抓捕小偷来说并没什么帮助。

为了解决这个问题，作者提出了一种名为 ForeReach 的新方法。ForeReach 不再盲目猜测，而是向机器人的设计者索要一份“旁注”：一份关于现实世界的行为变化速度可以有多快的承诺。你可以把它理解为机器人“困惑度”的速度限制。设计者必须声明：“我们的游戏与现实之间的差异变化速度不会超过这个数值。”随后，ForeReach 会检查我们拥有的这些数据点是否符合这一承诺。如果符合，它就会在机器人的路径周围构建一个“管状区域”（一条安全路径）。

它的实际工作原理如下：

检查： 它观察零散的数据点。如果两个点表明“困惑度的速度限制”被打破了，它会立即说：“不，你的承诺错了”，然后停止。
管状区域： 如果承诺成立，它会在机器人的路径周围画出一个安全的管状区域。随着机器人远离已知数据点，这个管状区域会变得越来越宽，因为不确定性在增加。
判决： 如果管状区域保持在“安全区”内并避开了障碍物，机器人就会获得绿灯。但如果机器人试图驶入一个我们没有数据的区域，且管状区域变得过宽（或撞上了墙），ForeReach 会礼貌地拒绝认证该计划。它会说：“我无法在此保证安全，因为我是在盲目驾驶。”

研究人员在两个系统上测试了该方法：一个简单的质点机器人和一个更复杂的“动力自行车”（汽车的模型）。他们将 ForeReach 与其他试图通过统计学或全局规则来猜测安全区域的方法进行了对比。结果很明确：其他方法经常仅仅因为它们“不知道情况更好”就给出了危险的计划以“绿灯”，从而导致模拟中的碰撞。然而，ForeReach 是诚实的。当机器人试图驶入一个没有数据的区域时，ForeReach 会说：“我无法在此进行认证”，并拒绝给出证书。但当机器人在有数据（或“速度限制”承诺足够紧凑）的区域行驶时，ForeReach 成功地用一个非常窄且实用的安全管状区域认证了计划。

在一个关于自行车模型的特定测试中，当机器人试图驶入一个不受支持的区域时，其他方法在数据量较低时，有 42% 的时间声称路径是安全的，但这些路径实际上是不安全的。而 ForeReach 则正确地在 100% 的情况下拒绝了对这些危险路径进行认证。当他们在机器人实际行驶的路径上增加更多数据点时，ForeReach 的“认证召回率”（即它正确说出“是的，这是安全的”的频率）从 49% 跳升到了 98%。

这篇论文并不声称已经解决了机器人安全性的终极问题。相反，它划定了一条清晰的界限：如果你想要一个既完美可靠又具有实用精确度的安全保证，你就不能只靠几个数据点，你必须拥有关于世界运行方式的一些额外信息。你不能只依赖于几个数据点来告诉你一切。你需要来自设计者的关于极限的“声明”。如果这个声明是真实的，ForeReach 就能完美运作。如果声明是错误的，该方法有时可以捕捉到错误，但它不能仅通过观察数据来证明声明是正确的。

最终，这项工作教会了我们，在机器人领域，“更多的数据”并不总是灵丹妙药。有时候，最重要的事情是知道世界遵循什么样的规则，即便是在我们尚未观察到的地方。如果没有这些规则，最好的安全检查员只能说：“我不知道”，而作者认为，这才是唯一诚实的回答。

技术摘要：模型失配下的规划认证：稀疏数据下可达性的三难困境

问题陈述
本文探讨了在真实机器人系统部署固定控制序列（例如来自 Diffusion Policy 或 $\pi_0$ 等学习策略的动作块）时面临的认证挑战，其中系统动力学与标称仿真模型存在差异。核心难点在于目标系统仅提供稀疏的、孤立的一步转移数据。在这种设定下，认证器必须确定：尽管存在标称模型 $f_0$ 与真实目标动力学 $f^\star$ 之间的未知模型误差（残差），规划出的轨迹是否仍能保持安全（避开不安全集合 $O$ ）。

作者指出了一项基本局限性：在观测数据点之外，模型误差可以在一个微小的邻域内任意变化，且不与观测结果相矛盾。在这种情况下，若模型误差不受限制，两个基于相同稀疏数据构建的平滑目标系统，一旦规划进入未观测区域，其偏差可能会发生剧烈分歧。因此，任何要求具备一致性均匀完备性（即保证对所有一致系统都安全）的确定性认证器，要么必须拒绝认证，要么必须返回一个投影宽度过大的可达管状区域，从而导致认证结果失去参考价值。

方法论：ForeReach
作者提出了 ForeReach，一种通过引入辅助信息来应对上述局限性的预执行认证器。该方法在以下框架下运行：

辅助信息要求： ForeReach 要求在给定的认证定义域 ( $Z_{cert}$ ) 内，提供一个关于模型误差的分量级 Lipschitz 边界（ $L$ ）。该边界必须独立于稀疏数据进行建立（例如，通过具有有界参数的解析动力学或单独认证的残差模型）。
成对一致性测试： 在进行传播之前，该方法会检查观测到的残差对是否与提供的 Lipschitz 边界相矛盾。如果 $|e_{r_i, k} - e_{r_j, k}| > \sum L_{k\ell}|z_{i,\ell} - z_{j,\ell}| + 2\sigma_k$ ，则声明被拒绝，认证器选择弃权。
集合成员包络（Set-Membership Envelope）： 在满足边界条件的条件下，该方法会在每个查询的状态-输入集合处构建一个残差的集合成员包络。该包络是通过将观测值的边界通过 Lipschitz 常数进行扩展（McShane 扩展）并结合观测噪声边界而推导出的。
分量化（Zonotopic）传播： 使用标称模型 $f_0$ 进行前向不确定性传播。可达集以分量化（Zonotope）形式表示，其中包含了标称映射包络（使用用于非线性余项的区间 Hessian 边界）以及残差包络。
认证逻辑： 仅当满足以下条件时，认证器才会发布安全证书：
- 传播过程始终处于认证定义域 ( $Z_{cert}$ ) 内。
- 可达管状区域的每一个投影切片都避开了不安全集合 ( $O$ )。
- 该方法能够区分三种类型的弃权：成对矛盾 ( $\perp_F$ )、定义域退出 ( $\perp_D$ ) 以及安全性失败 ( $\perp_S$ )。

核心贡献

三难困境定理（The Trilemma Theorem）： 作者证明了使用有限一步数据的确定性认证器的“三难困境”。一个认证器无法同时具备以下特性：
- 对不受限残差类的均匀完备性（Uniform Soundness）。
- $\bar{\rho}$ -信息量（返回具有有限投影宽度的管状区域）。
- 在观测范围之外不受限制。
  他们进一步推导了对于有界平滑类模型误差的有限且与规划相关的投影宽度下界，表明即使存在平滑性约束，数据缺失造成的间隙仍会迫使产生非零宽度。
ForeReach 算法： 一种实用的方法，它结合了提供的 Lipschitz 边界、成对一致性检查以及分量化传播，以在给定声明有效性的条件下提供轨迹包含性。
实验验证： 在两个基准系统（一个仿射质点系统和一个六状态动态自行车系统）上的实验表明，ForeReach 在规划进入不支持区域时能正确弃权（确保了完备性/可靠性），并在相关目标数据可用时恢复认证能力。

实验结果

质点系统： 全局校准基线会对不支持的规划进行认证，但无法包含目标轨迹（覆盖率为 0%），导致高误报率（false-safe rates）。ForeReach 通过弃权实现了对不支持规划的 100% 完全管状覆盖，并在受支持的路径上实现了 99.8% 的认证召回率。
动态自行车系统： 观察到了类似的趋势。全局校准和其他基线（如高斯过程、符合性方法）要么产生无意义的管状区域，要么在不支持区域无法包含轨迹。ForeReach 在不支持规划上保持了 100% 的覆盖（通过弃权），并在 $N=400$ 个样本的支持走廊内实现了 98.3% 的认证召回率。
学习到的动作块： 当应用于由学习策略生成的规划时，其弃权率与规划的标称展开距离最近观测点的距离呈现强相关性（Spearman $\rho=0.697}$ ），有效地追踪了数据的“支撑集”。
错误声明： 研究表明，如果提供的 Lipschitz 边界过小（低估了正则性），虽然成对测试可能通过（如果不存在局部矛盾），但生成的管状区域可能过窄，无法包含真实轨迹，从而导致错误的证书。这强调了该方法的完备性取决于外部声明的正确性。

意义与主张
本文声称，在认证来自稀疏数据的规划时，主要限制不在于数据的数量，而在于对未观测区域模型误差的约束缺失。作者认为，一个可用的证书需要从外部提供的结构化信息（如 Lipschitz 边界）。虽然数据可以证伪错误的声明，但无法在未观测区域证实正确的声明。

这项工作的意义在于：

形式化了使用稀疏、孤立转移进行数据驱动可达性分析的理论极限（三难困境）。
提供了一种方法，根据辅助信息的有效性在完备性（Soundness）与信息量（Informativeness）之间进行显式权衡，而不是假设数据的全局属性。
证明了当规划离开数据支撑集时，“弃权”是一种必要且具有信息意义的结果，这与可能产生狭窄但不可靠证书的基线方法形成了对比。

作者强调其保证是有条件的：只有当提供的 Lipschitz 边界在整个认证定义域内均成立时，证书才是有效的。该方法并不从稀疏数据中学习该边界，而是利用它来构建一个完备的包络。

技术摘要：模型失配下的规划认证：稀疏数据下可达性的三难困境

类似论文