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

TL;DR

This paper introduces a deterministic world model for verifying vision-based control systems, reducing overapproximation errors and improving verification accuracy through a novel modeling and analysis pipeline.

Contribution

The authors propose a deterministic world model that directly maps states to images, eliminating stochastic latent variables, and integrate it with reachability analysis for more precise verification.

Findings

Tighter reachable sets compared to latent-variable models

Improved verification performance on benchmark tasks

Effective use of conformal prediction for statistical bounds

Abstract

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.