cs.AISep 29, 2026

Stochastic World Models for Verifying Vision-Based Neural Feedback Systems

Authors: I. Samuel Akinwande, Mykel J. Kochenderfer, Clark Barrett

Organizations: Department of Aeronautics and Astronautics, Stanford University · Department of Computer Science, Stanford University

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Verifying a vision-based neural feedback system requires a model of the observations its controller acts upon. Such a model must capture the variation the sensor produces, while remaining tractable for closed-loop analysis. Generative adversarial networks (GANs) have served as perception surrogates, but they are large, reproduce complex scenes poorly, and are hard to verify. We explore stochastic world models as a richer class of perception surrogates. We train a world model with physically grounded latents, built from operations that standard verifiers bound. It reproduces held-out frames more faithfully than GAN surrogates with up to 130 times as many parameters. To verify these surrogates, we develop a procedure that combines falsification, adaptive refinement, symbolic, and backward analyses. On an emergency braking benchmark with a GAN surrogate, our procedure resolves the entire state space, 38% of which the state-of-the-art verifier left unresolved. On the RGB version of the benchmark, where no verification results have previously been reported, our procedure resolves over 80% of the state space with a world model surrogate.

Figures & tables

Figure 1: Perception surrogates for vision-based neural feedback systems. The surrogate gg supplies the observation ot{\bm{o}}_{t} the controller acts upon, and so determines the variation the closed loop can see. (a) A cGAN draws its variation from a Gaussian latent with no direct physical meaning. (b) A deterministic world model has no latent and no variation. (c) Our stochastic world model draws its variation from a few physically grounded latents, whose ranges form a box that verifiers can bound.
Figure 2: Reach-avoid verification. Forward analysis encloses the states reachable from I\mathbf{I} (black) in boxes (blue) that miss each A(t)\mathbf{A}(t) and end in G\mathbf{G} , so I\mathbf{I} is safe. Backward analysis encloses the states that reach A(t1)\mathbf{A}(t_{1}) (gold), and these states meet I′\mathbf{I}^{\prime} , so I′\mathbf{I}^{\prime} is unsafe.
Figure 3: The world model renderer gg . A linear layer lifts the state s{\bm{s}} to a coarse feature map, and LL stages of transposed convolution, batch normalization, and ReLU upsample it. The latents z{\bm{z}} act through two FiLM modulations, which rescale and shift the last feature map and the image.
Figure 4: Held-out frames and each surrogate’s rendering at the same state. The GAN row shows the released generator of each benchmark at zero latent, and the world model row shows our model at the center of its latent box. The plots below show the state the perception network estimates from each source’s frames (crosstrack position for taxiing, distance for AEBS) against the true state, as a median and a 25–75% band over the held-out set.
BenchmarkSurrogateParamsRMSE ↓\downarrowSSIM ↑\uparrow
Aircraft TaxiingDCGAN ( Katz et al., 2022 )2.76M0.04140.855
 MLP GAN ( Katz et al., 2022 )232k0.04070.849
 World model (ours)50k0.03680.867
 World model (ours)136k0.03300.898
 World model (ours)231k0.03200.904
AEBS (gray)cGAN ( Cai et al., 2025 )430k0.18620.449
Table 1: Surrogate fidelity on held-out frames. The MLP GAN is distilled from the DCGAN. Bold marks the best value for each benchmark.
SurrogateVerifierGPU-hoursVerifiedFalsifiedUnresolved
cGAN (grayscale)Cai et al. (2025)3742,6693,4633,868
cGAN (grayscale)Ours1,0436,5363,4640
World model (RGB)Ours5504,6773,4981,825
Table 2: Verification results on the 10,000 cells of the AEBS benchmark. Bold marks the better verified and unresolved counts on the cGAN. On the world model, 1,822 unresolved cells are not yet analyzed.
Figure 5: Each cell of the AEBS benchmark, colored by the analysis that decided it, on the released grayscale cGAN and on our RGB world model. Abstraction optimization includes adaptive refinement, and backward analysis decides every cell the baseline verifies. Most unresolved cells on the world model have not yet been analyzed. Each circle marks one cell per outcome, rendered below by that surrogate and framed in the outcome’s color.
Perception headParamsVerifiedGPU-hoursError (m)
Convolutional98k1209.750.384
Attention, small112k559.910.383
Attention, released size1.73M109.670.166
Table 3: Cells verified within 10 GPU-hours on the RGB world model, starting from a 10×1010\times 10 block, using various perception heads. Error is the mean absolute distance error on held-out frames.
Appendix figures & tables3 assets

Supplementary material from the paper’s appendix.

Appendix

SettingcGANWorld model
Falsification5,000 samples per cellsame
Targeted falsification4,000 samples, 5 roundssame
Refinement KK{1,2,4,6}\{1,2,4,6\} ; 12 for three cells{1,2,4,6}\{1,2,4,6\}
Abstraction optimization20 iterations, then 5 per step; rate 0.5same
Neuron splittingoff16–64 domains; 300 s per cell
Symbolic analysis3,600 s budget120 s budget
Appendix
Table 4: Procedure settings for the grayscale (cGAN) and RGB (world model) experiments. “Same” means the cGAN setting.
AnalysisVerifiedFalsified
Falsification 3,464
Forward analysis2,208 
Abstraction optimization and refinement551 
Symbolic analysis3 
Backward analysis3,774 
Total6,5363,464
Appendix
Table 5: Cells of the grayscale AEBS benchmark decided by each analysis, on the released cGAN surrogate. Backward analysis decides all 2,669 cells that Cai et al. (2025) verify.
AnalysisVerifiedFalsified
Falsification 3,498
Forward analysis305 
Abstraction optimization and refinement156 
Symbolic analysis0 
Backward analysis4,216 
Total4,6773,498
Appendix
Table 6: Cells of the RGB AEBS benchmark decided by each analysis, on the world-model surrogate. Of the 1,825 unresolved cells, 1,822 have not yet been analyzed.

Explore similar work

CardsList

  1. Validate the Dream Before You Trust Its Verdict: Admissibility for World-Model Simulators

    Jul 8, 2026Christian Oefinger, Finn Rasmus Schäfer, Korbinian Moller +2World ModelsAdmissibility

    Autonomous Vehicle Systems Lab, Technical University of Munich, Garching b. München, Germany

  2. Current World Models Lack a Persistent State Core

    Jun 18, 2026Jinpeng Lu, Dexu Zhu, Haoyuan Shi +8World ModelsLong-Horizon Inference

    University of Science and Technology of China · Beijing Innovation Center of Humanoid Robotics (X-Humanoid) · NLPR, Institute of Automation, Chinese Academy of Sciences +3

  3. Hallucination in World Models is Predictable and Preventable

    Jun 25, 2026Nicklas Hansen, Xiaolong WangWorld ModelsCitation Hallucination

    1UC San Diego