Deterministic World Models for Verification of Closed-loop Vision-based Systems
This work addresses the verification problem for safety-critical vision-based systems, offering an incremental improvement by replacing stochastic models with deterministic ones to enhance precision.
The paper tackles the challenge of verifying closed-loop vision-based control systems by proposing a Deterministic World Model (DWM) that eliminates stochastic latent variables to reduce overapproximation error, resulting in significantly tighter reachable sets and better verification performance compared to a baseline.
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.