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

📄 arXiv: 2512.08991v1 📥 PDF

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

分类: cs.CV, cs.LG

发布日期: 2025-12-08

备注: 22 pages, 10 figures. Submitted to FM 2026

💡 一句话要点

提出确定性世界模型，用于验证基于视觉的闭环系统，提升验证精度。

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)

关键词: 确定性世界模型 闭环系统验证 视觉控制系统 Reachability分析 共形预测

📋 核心要点

  1. 基于视觉的闭环控制系统验证面临图像高维和环境建模难的挑战，现有生成模型引入了不必要的过度近似误差。
  2. 论文提出确定性世界模型（DWM），直接将系统状态映射到生成图像，避免了随机潜在变量，从而提升验证精度。
  3. 实验表明，DWM能产生更紧凑的可达集，验证性能优于基于潜在变量的方法，验证效果更好。

📝 摘要（中文）

验证基于视觉的闭环控制系统仍然是一个根本性的挑战，这主要是由于图像的高维度以及视觉环境建模的困难。虽然生成模型越来越多地被用作验证中的相机替代，但它们对随机潜在变量的依赖引入了不必要的过度近似误差。为了解决这个瓶颈，我们提出了一种确定性世界模型（DWM），该模型将系统状态直接映射到生成图像，有效地消除了不可解释的潜在变量，以确保精确的输入边界。DWM采用双目标损失函数进行训练，该函数结合了像素级重建精度和控制差异损失，以保持与真实系统的一致性。我们将DWM集成到使用基于Star的Reachability分析（StarV）的验证流程中，并采用共形预测来推导世界模型和实际视觉系统之间轨迹偏差的严格统计界限。在标准基准上的实验表明，与潜在变量基线相比，我们的方法产生了明显更严格的可达集和更好的验证性能。

🔬 方法详解

问题定义：现有基于视觉的闭环控制系统验证方法，特别是使用生成模型作为相机替代时，由于生成模型依赖随机潜在变量，导致不必要的过度近似误差，降低了验证的精确性。问题在于如何消除这些不确定性，从而更准确地验证系统的安全性和可靠性。

核心思路：论文的核心思路是使用确定性世界模型（DWM）来直接建立系统状态到生成图像的映射关系。通过消除随机潜在变量，DWM能够提供更精确的输入边界，从而减少验证过程中的过度近似。这种确定性映射使得能够更准确地预测系统在视觉环境中的行为。

技术框架：该方法将DWM集成到验证流程中，主要包含以下几个阶段：1) 训练DWM：使用双目标损失函数训练DWM，该损失函数结合了像素级重建精度和控制差异损失，以确保DWM生成的图像既能准确重建真实图像，又能保持与真实系统一致的控制行为。2) Reachability分析：使用基于Star的Reachability分析（StarV）来计算系统的可达集。3) 轨迹偏差界定：采用共形预测来推导世界模型和实际视觉系统之间轨迹偏差的严格统计界限。

关键创新：最重要的技术创新点在于提出了确定性世界模型（DWM），它与传统的基于潜在变量的生成模型不同，DWM直接将系统状态映射到生成图像，消除了不确定性，从而提高了验证的精度。这种确定性映射是与现有方法的本质区别。

关键设计：DWM使用双目标损失函数进行训练，包括：1) 像素级重建损失：衡量生成图像与真实图像之间的差异，保证DWM能够准确重建视觉环境。2) 控制差异损失：衡量DWM生成的图像所对应的控制行为与真实系统控制行为之间的差异，保证DWM能够模拟真实系统的动力学特性。网络结构方面，具体结构未知，但需要能够实现从系统状态到图像的确定性映射。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，与基于潜在变量的基线方法相比，DWM能够产生更紧凑的可达集，这意味着验证结果更加精确，过度近似误差更小。具体的性能数据和提升幅度在论文中进行了详细的量化分析，证明了DWM在验证性能上的显著优势。

🎯 应用场景

该研究成果可应用于自动驾驶、机器人导航、无人机控制等领域，尤其是在安全攸关的应用中，例如自动驾驶汽车在复杂交通环境下的安全性验证。通过更精确的验证，可以提高系统的可靠性，降低事故风险，具有重要的实际价值和潜在的社会影响。

📄 摘要（原文）

Verifying closed-loop vision-based control systems remains a fundamental challenge due to the high dimensionality of images and the difficulty of modeling visual environments. While generative models are increasingly used as camera surrogates in verification, their reliance on stochastic latent variables introduces unnecessary overapproximation error. To address this bottleneck, we propose a Deterministic World Model (DWM) that maps system states directly to generative images, effectively eliminating uninterpretable latent variables to ensure precise input bounds. The DWM is trained with a dual-objective loss function that combines pixel-level reconstruction accuracy with a control difference loss to maintain behavioral consistency with the real system. We integrate DWM into a verification pipeline utilizing Star-based reachability analysis (StarV) and employ conformal prediction to derive rigorous statistical bounds on the trajectory deviation between the world model and the actual vision-based system. Experiments on standard benchmarks show that our approach yields significantly tighter reachable sets and better verification performance than a latent-variable baseline.