🤖 machine learning

Deterministic World Models for Verification of Closed-loop Vision-based Systems

本文提出了一种确定性世界模型（DWM），通过消除随机潜在变量并结合控制差异损失与星形可达性分析，显著提升了闭环视觉控制系统验证的精度并缩小了可达集范围。

原作者： Yuang Geng, Zhuoyang Zhou, Zhongzheng Zhang, Siyuan Pan, Hoang-Dung Tran, Ivan Ruchkin

发布于 2026-04-03

📖 1 分钟阅读☕ 轻松阅读

原作者： Yuang Geng, Zhuoyang Zhou, Zhongzheng Zhang, Siyuan Pan, Hoang-Dung Tran, Ivan Ruchkin

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

这篇论文解决了一个非常棘手的问题：如何确保那些“只靠眼睛看”的自动驾驶或机器人系统（端到端视觉控制器）是绝对安全的？

想象一下，你给机器人装了一个摄像头，它不看代码，只看图片，然后直接决定“向左转”还是“踩刹车”。这很酷，但也很危险。如果我们要用数学证明它永远不会撞车，就会遇到两个大麻烦。

这篇论文提出了一套名为**“确定性世界模型”（DWM）**的新方法，就像给机器人装了一个“超级预言家”和“安全网”。

下面我用几个生活中的比喻来解释这篇论文的核心思想：

1. 核心难题：为什么现在的验证方法行不通？

挑战一：没有“翻译官”

现状：机器人的大脑（控制器）看的是图片，但它的身体（物理世界）是由位置、速度等数字组成的。
比喻：想象你要验证一个司机是否安全。你只能看到司机眼前的风景画（图片），但你需要知道风景画里具体的距离和速度（物理状态）。
问题：以前没有一种数学公式能把“风景画”完美地翻译回“距离和速度”。就像你没法用数学公式直接算出“这张照片里树有多远”，除非你重新画一遍。

挑战二：噪音太大，吓死人

现状：以前的方法试图用一种叫“生成对抗网络（GAN）”的 AI 来模拟摄像头。这种 AI 为了生成多样的图片，会引入一个“随机噪音”（潜变量）。
比喻：这就像你让一个画家画“一辆车”，但他手里拿着一把随机撒盐的勺子。
- 如果盐撒多了，画出来的车可能像被炸过一样；
- 如果盐撒少了，车可能像融化的冰淇淋。
- 为了安全起见，验证者必须假设“所有可能的画”都是真的。结果就是，验证者认为车可能会出现在整个宇宙的任何地方，于是得出结论：“这系统太危险了，不能上路！”（这就是过度保守，把安全的系统误判为不安全）。

2. 解决方案：确定性世界模型 (DWM)

作者说：“别撒盐了！我们要一个** deterministic（确定性）**的模型。”

核心思想：如果物理状态（比如车在坐标 100，速度 50）是确定的，那么摄像头拍出来的照片必须也是确定的。
比喻：我们训练一个**“超级摄影师”**。
- 只要给他输入“车在 100 米处”，他就只画这一张唯一的照片。
- 没有随机噪音，没有“可能像冰淇淋”的画。
- 这样，验证者就能精确地知道：在这个状态下，摄像头会看到什么，机器人会做出什么反应。

3. 训练秘诀：双重损失函数 (Dual Loss)

怎么训练这个“超级摄影师”呢？光画得像还不够，还得听话。

第一重：像素级还原（画得像）
- 让生成的图片和真实照片长得一模一样。
第二重：控制一致性（听话）
- 这是最关键的创新！
- 比喻：假设摄影师画了一辆车，位置稍微偏了一点点（肉眼几乎看不出来）。
  - 对于普通画家，这没关系。
  - 但对于机器人，这可能导致它以为前面有墙，于是猛踩刹车，结果导致追尾。
- 所以，作者加了一个惩罚机制：“如果你画的图让机器人做出了和真实情况不同的动作，我就罚你！”
- 这确保了模型不仅“像”，而且“懂行”，能做出正确的决策。

4. 最后的保险：共形预测 (Conformal Prediction)

虽然我们的“超级摄影师”很厉害，但它毕竟不是真的摄像头，总会有细微的误差。怎么保证 100% 安全？

比喻：我们给机器人的安全范围套上一个**“弹性气球”**。
- 我们先在真实世界里跑很多趟，看看“超级摄影师”预测的路径和真实路径最大能差多少（比如最大差 0.5 米）。
- 然后，我们在验证时，把机器人的安全范围扩大 0.5 米（这就是“充气”）。
- 结果：只要在这个“充气后”的安全范围内没出事，我们就有 95% 以上的把握说：真实的机器人也不会出事！
- 这就把“模型的安全”完美转移到了“现实的安全”。

5. 实验结果：真的好用吗？

作者测试了四个场景（像倒立摆、爬坡车、刹车系统等）：

对比旧方法（cGAN）：旧方法因为“撒盐”（随机噪音），把安全范围画得巨大无比，导致很多本来安全的路线被误判为“危险”，验证通过率很低。
新方法（DWM）：
- 更精准：安全范围画得很小、很紧，能区分出真正的危险和真正的安全。
- 更聪明：因为加了“控制一致性”训练，机器人不会因为图片的一点点瑕疵就发疯。
- 结果：在四个测试中，新方法的准确率（F1 分数）都远高于旧方法，尤其是在复杂的刹车系统中，表现最好。

总结

这篇论文就像是为自动驾驶机器人设计了一套**“无噪音的模拟眼镜”和“带弹性的安全网”**：

去掉随机噪音：让模拟世界和物理世界一一对应，不再乱猜。
关注决策后果：不仅要求图片像，更要求图片能做出正确的驾驶决定。
统计保险：用数学方法给模拟结果加一层保险，确保现实世界也安全。

这就让那些“只靠眼睛看”的 AI 系统，第一次有了数学上可证明的、令人放心的安全保障。

1. 研究背景与问题定义 (Problem)

背景：
端到端（End-to-End）的视觉控制器直接将原始相机帧映射到控制动作，广泛应用于自动驾驶、机器人操作等安全关键系统。然而，对这类系统的闭环行为进行形式化验证（Formal Verification）面临巨大挑战。

核心挑战：
现有的神经控制器验证工具通常假设输入是低维状态向量（如位置、速度），但视觉控制器的输入是高维图像。这导致了两个根本性难题：

缺乏通用的“状态到图像”模型： 物理动力学有明确的数学方程，但相机如何将物理状态映射为像素图像没有封闭形式的解析表达式。没有这个映射，验证循环无法闭合。
高维图像导致的过近似爆炸（Over-approximation Growth）： 即使存在映射，将图像集合通过深度卷积网络传播时，每一层都会引入过近似误差。在多个时间步长后，这些误差累积导致可达集（Reachable Sets）变得过大，使得验证器错误地将安全轨迹标记为不安全（即误报率极高）。

现有方法的局限：

符号抽象法： 仅适用于结构化环境（如车道保持），无法处理动态或非结构化环境。
生成式代理模型（如 cGAN）： 使用条件生成对抗网络（cGAN）作为相机代理。但 cGAN 依赖随机潜在变量（Latent Variables）来增加图像多样性。在验证中，这些无物理意义的潜在变量必须被保守地界定，导致生成的图像集合远大于真实系统产生的集合，加剧了过近似问题，使验证变得不可行。

2. 方法论 (Methodology)

作者提出了一种**确定性世界模型（Deterministic World Model, DWM）**框架，包含三个核心组成部分：

A. 确定性世界模型 (DWM)

核心思想： 移除生成模型中的随机潜在变量，仅由物理状态（如位置、速度）直接控制图像生成。
架构： 一个无潜在变量的神经解码器（Neural Decoder），将物理状态 $s$ 直接映射为合成图像 $\hat{I} = g_\theta(s)$ 。
优势： 确保了图像集中的每一个图像都对应一个物理上可实现的真实状态，消除了由潜在变量引起的无意义变异性。

B. 双损失训练策略 (Dual Loss Training)

为了训练 DWM，作者设计了一个结合了两个互补项的损失函数：

像素级重建损失 (Pixel-level Reconstruction Loss)： 确保生成的图像在视觉上与真实图像高度一致。特别地，引入了加权机制，对控制决策相关的区域（如车辆、杆）赋予更高权重，对背景赋予低权重。
控制一致性损失 (Control-Consistent Loss)： 这是一个关键创新。它惩罚由生成图像和真实图像分别输入控制器后产生的动作差异（ $L_{ctrl} = \| C(\hat{I}) - C(I) \|^2$ ）。这确保了模型不仅“看起来像”，而且“行为像”，防止微小的视觉偏差导致控制器动作的巨大改变。

C. 基于 Star 集的闭环验证流水线

验证流程： 将 DWM 集成到基于 Star 集（Star-based）的验证框架中。
1. 物理状态集合（Star Set）输入 DWM，通过转置卷积层传播，生成图像集合（ImageStar）。
2. 图像集合输入 CNN 控制器，生成动作集合。
3. 动作集合通过非线性动力学（使用 PyBDR 工具）更新到下一状态。
闭环： 形成 $状态 \to 图像 \to 动作 \to 新状态$ 的完整闭环验证。

D. 共形预测 (Conformal Prediction, CP) 转移保障

由于代理模型（DWM）不完美，需要将其验证结果转移到真实系统：

方法： 利用共形预测计算真实轨迹与世界模型轨迹之间的最大偏差边界（ $\Delta_{1-\alpha}$ ）。
膨胀（Inflation）： 将验证得到的可达集通过 Minkowski 和膨胀 $\Delta_{1-\alpha}$ 。
结果： 提供了分布无关的统计保证：以至少 $1-\alpha$ 的概率，真实系统的轨迹包含在膨胀后的可达集中。

3. 主要贡献 (Key Contributions)

确定性世界建模方法： 提出了一种去除随机潜在变量的生成式代理模型，实现了可验证的相机传感器代理，解决了状态到图像映射的封闭形式问题。
首个基于 Star 集的视觉系统闭环验证扩展： 将 Star 集可达性分析成功扩展到了包含图像输入和卷积神经网络的闭环视觉系统中。
基于共形预测的真实系统保障： 提出了一种统计转移机制，将代理模型的验证结果转化为具有概率保证的真实系统安全结论。
控制一致性损失： 引入控制一致性损失，显著降低了建模误差，使生成的图像在行为上更符合真实控制器的需求。

4. 实验结果 (Results)

作者在四个基准测试（CartPole, MountainCar, Pendulum, Braking System）上进行了评估，并与 cGAN 基线进行了对比。

验证精度显著提升：
- DWM 在所有四个基准测试中的 F1 分数均显著高于 cGAN 基线（例如，MountainCar 上 DWM 为 0.9817，cGAN 为 0.7990；Braking System 上 DWM 为 0.9842，cGAN 为 0.6639）。
- 真负率 (TNR)： DWM 在所有测试中达到了 1.0（完美识别安全区域），而 cGAN 在 MountainCar 和 Braking System 上 TNR 为 0.0（将所有区域误判为不安全），说明 cGAN 的过近似过于保守。
图像集更紧凑：
- 实验显示，cGAN 由于潜在变量的存在，生成的图像像素区间非常大（例如背景噪声被放大），导致可达集迅速膨胀。DWM 消除了这种无意义的变异性，生成了更紧致的图像集。
消融实验：
- 移除潜在变量本身就能大幅降低共形预测边界（ $\Delta_{0.95}$ ）。
- 进一步加入控制一致性损失（ $L_{ctrl}$ ）能再次降低边界，证明该损失有效减少了轨迹级别的建模误差。
真实系统保障：
- 应用共形预测膨胀后，虽然部分高敏感系统（如 CartPole）的召回率因保守性增加而下降，但这反映了严谨性带来的代价，而非模型失效。对于低敏感系统（如 MountainCar），在保持高召回率的同时获得了严格的数学保障。

5. 意义与影响 (Significance)

理论突破： 解决了高维视觉输入下闭环形式化验证的“不可行”问题，证明了通过去除随机性并引入行为一致性约束，可以构建既精确又可验证的世界模型。
工程价值： 为自动驾驶和机器人等安全关键系统提供了一种实用的验证工具，能够在不牺牲安全性的前提下，有效区分安全与不安全轨迹，减少误报。
方法论启示： 揭示了在验证任务中，生成模型的“多样性”（通常由潜在变量提供）与“可验证性”（需要紧致、确定的边界）之间存在根本冲突，并提出了以“可验证性”和“重建质量”优先的解决方案。

局限性：
目前模型在处理极其复杂的场景（如杂乱背景、多移动物体、大光照变化）时仍有困难，且验证计算时间较长（Braking System 需 13.5 小时）。未来工作将集中在改进复杂场景处理能力、利用显著性图减少计算量以及扩展到在线运行时监控。