# Stochastic World Models for Verifying Vision-Based Neural Feedback Systems

arXiv: https://arxiv.org/abs/2609.38120 · HTML: https://mlsanity.com/paper/2609.38120/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Latent predictive world models, one of 11 directions in World models.
- Builds on 32 of its 41 references that are in the map.
- First posted on arXiv 29 Sep 2026.

## Placed in

- World models / [Latent predictive world models](https://mlsanity.com/wm/latent-predictive-world-models/)

## Builds on (most cited first, 30 of 32)

- [Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift](https://mlsanity.com/paper/1502.03167/) (2015)
- [FiLM: Visual Reasoning with a General Conditioning Layer](https://mlsanity.com/paper/1709.07871/) (2017)
- [Conditional Generative Adversarial Nets](https://mlsanity.com/paper/1411.1784/) (2014)
- [Unsupervised Representation Learning with Deep Convolutional Generative Adversarial Networks](https://mlsanity.com/paper/1511.06434/) (2015)
- [Mastering Atari with Discrete World Models](https://mlsanity.com/paper/2010.02193/) (2020)
- [Self-Attention Generative Adversarial Networks](https://mlsanity.com/paper/1805.08318/) (2018)
- [DriveDreamer: Towards Real-world-driven World Models for Autonomous Driving](https://mlsanity.com/paper/2309.09777/) (2023)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Real-World Humanoid Locomotion with Reinforcement Learning](https://mlsanity.com/paper/2303.03381/) (2023)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems](https://mlsanity.com/paper/2108.01220/) (2021)
- [Compositional Falsification of Cyber-Physical Systems with Machine Learning Components](https://mlsanity.com/paper/1703.00978/) (2017)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1912.07084/) (2019)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [Verifying Controllers with Convolutional Neural Network-based Perception: A Case for Intelligible, Safe, and Precise Abstractions](https://mlsanity.com/paper/2111.05534/) (2021)
- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Foundational World Models Accurately Detect Bimanual Manipulator Failures](https://mlsanity.com/paper/2603.06987/) (2026)
- [Four Principles for Physically Interpretable World Models](https://mlsanity.com/paper/2503.02143/) (2025)
- [Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling](https://mlsanity.com/paper/2405.18554/) (2024)
- [Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops](https://mlsanity.com/paper/2410.00145/) (2024)
- [Physically Interpretable World Models via Weakly Supervised Representation Learning](https://mlsanity.com/paper/2412.12870/) (2024)
- [Polyhedral Enclosures: An Efficient Combinatorial Abstraction for Nonlinear Neural Feedback Systems](https://mlsanity.com/paper/2503.22660/) (2025)
- [The Era of End-to-End Autonomy: Transitioning from Rule-Based Driving to Large Driving Models](https://mlsanity.com/paper/2603.16050/) (2026)
- [Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles](https://mlsanity.com/paper/2501.14009/) (2025)
- [Deterministic World Models for Closed-loop Reachability Analysis of End-to-End Vision-based Control](https://mlsanity.com/paper/2512.08991/) (2025)
- [RampoNN: A Reachability-Guided System Falsification for Efficient Cyber-Kinetic Vulnerability Detection](https://mlsanity.com/paper/2511.16765/) (2025)

## Abstract (arXiv)

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.