确定性世界模型用于闭环视觉系统验证
Deterministic World Models for Closed-loop Reachability Analysis of End-to-End Vision-based Control
AI总结：
本文提出确定性世界模型，通过直接映射系统状态到生成图像，消除不可解释的潜在变量，提升闭环视觉系统验证的精度与性能。
摘要：
验证闭环视觉控制系统仍是一个基本挑战，由于图像的高维性和视觉环境建模的困难。尽管生成模型越来越多地用作摄像头替代品进行验证，但其对随机潜在变量的依赖引入了不必要的过度近似误差。为解决这一瓶颈，我们提出了一种确定性世界模型（DWM），该模型将系统状态直接映射到生成图像，有效消除不可解释的潜在变量，以确保精确的输入边界。DWM通过结合像素级重建精度和控制差异损失的双目标损失函数进行训练，以保持与真实系统的行为一致性。我们将DWM集成到使用基于星的可达性分析（StarV）的验证流程中，并利用符合预测法推导出世界模型与实际视觉系统轨迹偏差的严格统计边界。在标准基准测试中，我们的方法在可达集的紧致性和验证性能方面优于潜在变量基线。
英文摘要：
End-to-end image controllers that map raw camera frames directly to control actions are increasingly deployed in safety-critical systems. However, formally verifying their closed-loop behavior remains an open challenge because cameras produce high-dimensional images whose generation cannot easily be described in a closed mathematical form. We propose a Deterministic World Model (DWM), a latent-free neural decoder that maps physical states (e.g., position and velocity) directly to synthetic camera images, enabling closed-loop reachability analysis without the overapproximation caused by stochastic latent variables. The DWM is trained with a novel dual loss combining saliency-map reconstruction and a control-consistent term that preserves behavioral consistency with the real controller. We integrate the DWM into closed-loop reachability analysis and apply conformal prediction to inflate the reachable sets by a distribution-free trajectory-tube deviation bound, transferring the surrogate guarantee to the real system with high probability. Experiments on a CARLA braking system and three Gym benchmarks (CartPole, MountainCar, Pendulum) show that the DWM produces substantially tighter reachable tubes than a cGAN and trajectory predictor baselines while meeting the target coverage after conformal inflation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
