Stochastic World Models for Verifying Vision-Based... | AI Research

What the paper is about

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.

What it covers

Stochastic World Models for Verifying Vision-Based Neural Feedback Systems I. Samuel Akinwande Affiliation: Department of Aeronautics and Astronautics, Stanford University Email: [email protected] Mykel J. Kochenderfer Affiliation: Department of Aeronautics and Astronautics, Stanford University Email: [email protected] Clark Barrett Affiliation: Department of Computer Science, Stanford University Email: [email protected] 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. 1 Introduction Modern autonomous systems act on uncertain, high-dimensional observations instead of exact state information. These observations are often images, and a neural network maps them to control actions, closing the loop between perception and actuation. Systems in which a neural network closes the feedback loop are called neural feedback systems , and they are increasingly deployed in safety-critical domains such as aerial navigation ( Kaufmann et al., 2023 ) , humanoid robotics ( Radosavovic et al., 2024 ) , and autonomous driving ( Nebot & Berrio Perez, 2026 ) . Verification can establish that such a system is safe before it is deployed, and while mature methods exist for classical control systems ( Mitchell et al., 2005 ; Bansal et al., 2017 ) , verifying neural feedback systems remains a challenge. Recent work verifies state-based neural feedback systems, whose controllers compute actions directly from the state ( Akinwande et al., 2025 ; Akinwande et al., 2026b ; Kochdumper et al., 2023 ; Rober et al., 2023 ) , but the vision-based case remains largely open. The main obstacle is modeling the environment. Verifying a vision-based system requires a model of the sensor and the scene it observes, and the resulting safety guarantee holds for the real system to the extent that this model is faithful. The model must be expressive enough to capture the variation in the images the system will encounter, yet compact enough for a verifier to reason about, and these requirements often conflict. Prior work replaces the camera with a generative adversarial network (GAN) that renders images for each state ( Katz et al., 2022 ; Cai et al., 2025 ) , but existing verifiers leave the resulting surrogate systems partly unresolved ( Cai et al., 2025 ) . Alternative surrogates, including variational autoencoders and formal perception models ( Parameshwaran & Wang, 2025 ; Hsieh et al., 2022 ) , either fail to capture the variation in the sensor’s images or are intractable to verify in closed loop. World models learn to generate the observations of an environment, and failure modes found in them have been shown to transfer to the real world ( Ward et al., 2026 ) . Geng et al. (2025) use a world model for closed-loop verification, but its architecture is deterministic. It produces a single observation per state and does not model the environmental variation that makes vision-based verification hard. We claim that careful surrogate design can ease the tension between expressiveness and tractability. A GAN draws its variation from a noise vector with no direct physical meaning, so the box of noise values a verifier bounds corresponds to no clear range of conditions. A deterministic world model is easier to verify but has no variation to bound. We instead train a stochastic world model that concentrates the variation in a few latents grounded in physical quantities (Figure 1 ). We frame a vision-based neural feedback system as a state-based system whose sensor is a generative model. To verify the resulting systems, we build a procedure that combines falsification, adaptive refinement, symbolic, and backward analyses. We evaluate the world model on aircraft taxiing and emergency braking case studies, and the procedure on emergency braking. Our contributions are as follows:

• Formalization. A formalization of vision-based neural feedback systems as state-based systems whose sensor is a generative model over a set of latents. In this formalization, the state-based case is the special case where the sensor is the identity map, so analysis techniques for state-based systems extend to the vision-based setting.

• Improved Modeling. A stochastic world model with latents grounded in physical quantities, so that the possible observations at a state correspond to a box of environmental conditions. The model is built from operations that standard verifiers bound, is trained on closed-loop rollouts of the controller, and reproduces held-out frames more faithfully than the GAN surrogates of both case studies, with up to 130 times fewer parameters.

• Verification Procedure. A verification procedure that combines falsification, adaptive refinement, symbolic, and backward analyses. On the emergency braking benchmark, it resolves the entire state space with the released GAN surrogate, 38% of which the state-of-the-art verifier left unresolved. On the RGB version of the benchmark, it resolves over 80% of the state space with a world model surrogate. 2 Related Work Verification algorithms. A few families of methods bound a network’s behavior over an input set. Linear relaxation-based perturbation analysis (LiRPA) ( Xu et al., 2020 ) propagates linear bounds built from per-node abstractions that are exact at affine layers and sound at nonlinearities. Mixed-integer encodings represent a piecewise-linear network exactly, defining a binary variable for each unstable neuron ( Tjeng et al., 2019 ) . Abstractions may be too loose to decide a property, so complete verifiers pair abstractions with refinement via branch and bound ( Xu et al., 2021 ; Wang et al., 2021 ) . Refinement partitions the input set or fixes unstable activations, bounds each subproblem, and verifies the property on every subproblem, or refutes it once one subproblem yields a counterexample. Verifiers for state-based neural feedback systems build on this machinery by composing the dynamics with the controller. Forward methods over-approximate the reachable set one step at a time, either by encoding the dynamics and controller together as a mixed-integer program ( Sidrane et al., 2022 ; Akinwande et al., 2025 ) or by propagating sets or bounds through their composition ( Kochdumper et al., 2023 ; Akinwande et al., 2026b ) . Backward methods compute the states from which the unsafe set is reachable ( Rober et al., 2023 ) or the states that reach the goal ( Akinwande et al., 2026a ) . Perception surrogates. A perception surrogate stands in for the sensor during verification. Katz et al. (2022) replace a camera with a conditional GAN ( Mirza & Osindero, 2014 ) that generates observations from the low-dimensional state, yielding a map from states to observations that neural network verifiers can analyze ( Julian & Kochenderfer, 2019 ) . Cai et al. (2025) verify this benchmark and introduce an emergency braking benchmark with grayscale and RGB variants ( Zhang et al., 2019 ) , leaving 38% of the grayscale system unresolved and the RGB system unverified. Other surrogates include variational autoencoders ( Parameshwaran & Wang, 2025 ) , formal models of the perception pipeline ( Santa Cruz & Shoukry, 2022 ; Hsieh et al., 2022 ) , and deterministic world models ( Geng et al., 2025 ) , which decode a single observation per state. World models. World models learned from pixels have been applied to game-playing ( Hafner et al., 2021 ) and have since served as environment surrogates across domains ( Hafner et al., 2025 ) , including driving ( Wang et al., 2024 ) . Failures found in world models have been shown to transfer to real systems ( Ward et al., 2026 ) . The latents of a world model typically carry no physical meaning, so a guarantee over a set of latents does not say which conditions it covers. Recent work argues for latents that are physically interpretable by construction ( Peper et al., 2025 ) and learns such representations under weak supervision ( Mao et al., 2026 ) . Combined strategies. When no single analysis decides a property, prior work combines several. Refinement tightens bounds at the cost of more subproblems, whether by partitioning the input ( Everett et al., 2021 ) , splitting only where a candidate violation survives ( Rober & How, 2024 ) , or refining wherever a counterexample proves spurious ( Elboher et al., 2020 ; Li et al., 2026 ) . Falsification has been paired with reachability so that one analysis directs the other ( Dreossi et al., 2019a ; Dreossi et al., 2019b ; Tsujio et al., 2025 ) , and forward and backward reachability have been integrated into a single procedure for neural feedback systems ( Akinwande et al., 2026a ) . 3 Problem Formulation Notation. We write 2 𝐗 2^{\mathbf{X}} for the power set of 𝐗 \mathbf{X} , [ i . . j ] [i..j] for { i , … , j } {i,\ldots,j} , [ n ] [n] for [ 1 . . n ] [1..n] , and S t S_{t} for the t t -th element of a sequence S S . Functions apply to sets elementwise, with the results unioned. 3.1 Neural Feedback Systems A neural feedback system is a dynamical system controlled by a neural network. We model the system in discrete time, with a controller that acts on observations of the state, and represent it by the tuple 𝒟 = ⟨ m , n , d , 𝐈 , 𝐅 , 𝐄 , 𝚵 , h , 𝐮 , B , δ , T , 𝐆 , 𝐀 ⟩ \mathcal{D}=\langle m,n,d,\mathbf{I},\mathbf{F},\mathbf{E},\bm{\Xi},h,\mathbf{u},B,\delta,T,\mathbf{G},\mathbf{A}\rangle . The state 𝒔 ∈ ℝ n {\bm{s}}\in\mathbb{R}^{n} evolves under a vector field 𝐅 = ( f 1 , … , f n ) \mathbf{F}=(f_{1},\ldots,f_{n}) with f i : ℝ n → ℝ f_{i}:\mathbb{R}^{n}\to\mathbb{R} , subject to perturbations drawn from 𝐄 ⊆ ℝ n \mathbf{E}\subseteq\mathbb{R}^{n} . A sensor h : ℝ n × 𝚵 → ℝ d h:\mathbb{R}^{n}\times\bm{\Xi}\to\mathbb{R}^{d} maps the state and an exogenous input 𝝃 ∈ 𝚵 \bm{\xi}\in\bm{\Xi} to an observation 𝒐 ∈ ℝ d {\bm{o}}\in\mathbb{R}^{d} . The controller 𝐮 : ℝ d → ℝ m \mathbf{u}:\mathbb{R}^{d}\to\mathbb{R}^{m} computes an action from the observation, and the action drives the dynamics through a controller-input matrix B ∈ ℝ n × m B\in\mathbb{R}^{n\times m} . The system starts in 𝐈 ⊆ ℝ n \mathbf{I}\subseteq\mathbb{R}^{n} , advances in steps of length δ \delta for T T steps, and is evaluated against a goal set 𝐆 ⊆ ℝ n \mathbf{G}\subseteq\mathbb{R}^{n} and time-indexed unsafe states 𝐀 : [ 0 . . T ] → 2 ℝ n \mathbf{A}:[0..T]\to 2^{\mathbb{R}^{n}} . One step of the closed loop is 𝑛𝑒𝑥𝑡 𝒟 ​ ( 𝒔 ) \displaystyle\mathit{next}^{\mathcal{D}}({\bm{s}}) ≔ { 𝒔 + ( 𝐅 ( 𝒔 ) + B 𝐮 ( h ( 𝒔 , 𝝃 ) ) + ϵ ) δ ∣ ϵ ∈ 𝐄 , 𝝃 ∈ 𝚵 } . \displaystyle\coloneqq{{\bm{s}}+(\mathbf{F}({\bm{s}})+B\mathbf{u}(h({\bm{s}},\bm{\xi}))+\bm{\epsilon}),\delta\mid\bm{\epsilon}\in\mathbf{E},\ \bm{\xi}\in\bm{\Xi}}. (1) Starting from 𝐗 0 ⊆ 𝐈 \mathbf{X}{0}\subseteq\mathbf{I} , the trajectory τ 𝒟 ​ ( 𝐗 0 ) ≔ ( 𝐗 0 , … , 𝐗 T ) \tau^{\mathcal{D}}(\mathbf{X}{0})\coloneqq(\mathbf{X}{0},\ldots,\mathbf{X}{T}) with 𝐗 t ≔ 𝑛𝑒𝑥𝑡 𝒟 ​ ( 𝐗 t − 1 ) \mathbf{X}{t}\coloneqq\mathit{next}^{\mathcal{D}}(\mathbf{X}{t-1}) for t ∈ [ T ] t\in[T] denotes the states that can be reached at each time step. 𝒔 t {\bm{s}}{t} perception surrogate g g 𝒐 t {\bm{o}}{t} vision-based controller 𝐮 \mathbf{u} dynamics 𝐅 \mathbf{F} 𝒂 t {\bm{a}}{t} 𝒔 t + 1 {\bm{s}}{t+1} (a) cGAN decoder (b) deterministic world model decoder (c) stochastic world model decoder 𝒛 ∼ 𝒩 ⁡ ( 𝟎 , 𝑰 ) {\bm{z}}\sim{\mathcal{N}}({\bm{0}},{\bm{I}}) ungrounded latents random, non-semantic variation no latents no variation light haze blur semantic variation Figure 1: Perception surrogates for vision-based neural feedback systems. The surrogate g g supplies the observation 𝒐 t {\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. The verification literature has focused on the state-based case, where d = n d=n and h ⁡ ( 𝒔 , 𝝃 ) = 𝒔 h({\bm{s}},\bm{\xi})={\bm{s}} . In that setting, the controller observes the state exactly, and 𝚵 \bm{\Xi} plays no role. This paper addresses the vision-based case, where h h is a camera, d ≫ n d\gg n , and 𝝃 \bm{\xi} denotes environmental factors such as lighting and weather. Such a sensor has no closed-form description, so we introduce a perception surrogate g : ℝ n × ℤ → ℝ d g:\mathbb{R}^{n}\times{\mathbb{Z}}\to\mathbb{R}^{d} , a generative model that maps a state and a latent 𝒛 ∈ ℤ {\bm{z}}\in{\mathbb{Z}} to an observation. Substituting g g for h h and ℤ {\mathbb{Z}} for 𝚵 \bm{\Xi} in 𝒟 \mathcal{D} yields the surrogate system . This framing places vision-based systems within the state-based formalism, so state-based verification techniques extend to them. 𝐈 ′ \mathbf{I}^{\prime} 𝐈 \mathbf{I} 𝐀 ⁡ ( t 1 ) \mathbf{A}(t{1}) 𝐀 ⁡ ( t 2 ) \mathbf{A}(t_{2}) 𝐆 \mathbf{G} Figure 2: Reach-avoid verification. Forward analysis encloses the states reachable from 𝐈 \mathbf{I} (black) in boxes (blue) that miss each 𝐀 ⁡ ( t ) \mathbf{A}(t) and end in 𝐆 \mathbf{G} , so 𝐈 \mathbf{I} is safe. Backward analysis encloses the states that reach 𝐀 ⁡ ( t 1 ) \mathbf{A}(t_{1}) (gold), and these states meet 𝐈 ′ \mathbf{I}^{\prime} , so 𝐈 ′ \mathbf{I}^{\prime} is unsafe. Reach-Avoid Specifications. The system 𝒟 \mathcal{D} is safe if every trajectory enters the goal set at some step and no trajectory intersects the unsafe states at any step: ∀ 𝒔 ∈ 𝐈 . ∃ t ∈ [ 0 . . T ] . τ 𝒟 ( { 𝒔 } ) t ⊆ 𝐆 , \displaystyle\forall{\bm{s}}\in\mathbf{I}.\ \exists t\in[0..T].\ \tau^{\mathcal{D}}({{\bm{s}}}){t}\subseteq\mathbf{G}, (2) ∀ t ∈ [ 0 . . T ] . τ 𝒟 ( 𝐈 ) t ∩ 𝐀 ( t ) = ∅ . \displaystyle\forall t\in[0..T].\ \tau^{\mathcal{D}}(\mathbf{I}){t}\cap\mathbf{A}(t)=\emptyset. (3) Equations 2 and 3 are the reach and avoid properties (Figure 2 ). Since 𝑛𝑒𝑥𝑡 𝒟 \mathit{next}^{\mathcal{D}} ranges over every 𝝃 ∈ 𝚵 \bm{\xi}\in\bm{\Xi} , a system satisfying these properties is safe for every environmental condition in 𝚵 \bm{\Xi} . 3.2 Reachability Analysis Verifying a reach-avoid specification requires sound approximations of the trajectory τ 𝒟 ​ ( 𝐗 0 ) \tau^{\mathcal{D}}(\mathbf{X}{0}) . Forward analysis over-approximates τ 𝒟 ​ ( 𝐗 0 ) \tau^{\mathcal{D}}(\mathbf{X}{0}) and checks it against 𝐀 ⁡ ( t ) \mathbf{A}(t) and 𝐆 \mathbf{G} at each step. Backward analysis instead over-approximates the set of states from which 𝐀 \mathbf{A} is reachable within the horizon and checks that it is disjoint from 𝐈 \mathbf{I} , or under-approximates the set of states that reach 𝐆 \mathbf{G} and checks that it contains 𝐈 \mathbf{I} . Both analyses accumulate approximation error over the horizon, since each step starts from the previous step’s approximation. Adaptive refinement ( Rober & How, 2024 ) , symbolic analysis ( Akinwande et al., 2025 ) , and combinations of forward and backward analysis ( Akinwande et al., 2026a ) reduce this error. 4 Stochastic World Models Our world model is a renderer g : ℝ n × ℤ → ℝ d g:\mathbb{R}^{n}\times{\mathbb{Z}}\to\mathbb{R}^{d} that maps a state 𝒔 {\bm{s}} and a vector of latents 𝒛 ∈ ℤ {\bm{z}}\in{\mathbb{Z}} to an image. The state determines the geometry of the scene, and the latents account for variations between two images at the same state, such as the lighting. The model has no noise input, so the latents are its only source of variation. Each latent is a physical quantity ranging over an interval, so ℤ {\mathbb{Z}} is a box of physical conditions. The set of images the controller can observe in state 𝒔 {\bm{s}} , g ⁡ ( 𝒔 , ℤ ) = { g ⁡ ( 𝒔 , 𝒛 ) ∣ 𝒛 ∈ ℤ } , g({\bm{s}},{\mathbb{Z}})={,g({\bm{s}},{\bm{z}})\mid{\bm{z}}\in{\mathbb{Z}},}, (4) is then the set of images taken under those conditions. Taking g g as the perception surrogate yields a system in which 𝒛 {\bm{z}} ranges over ℤ {\mathbb{Z}} independently at every step. Architecture. The model is a deconvolutional decoder in the style of DCGAN generators ( Radford et al., 2016 ) and the DreamerV3 image decoder ( Hafner et al., 2025 ) . A linear layer lifts the state to a coarse feature map, and L L transposed-convolution stages double its resolution in turn: h 0 \displaystyle h_{0} = reshape ⁡ ( W 0 ​ 𝒔 + b 0 ) , h k = ReLU ⁡ ( BN k ⁡ ( ConvT k ⁡ ( h k − 1 ) ) ) , k ∈ [ L ] . \displaystyle=\operatorname{reshape}(W_{0}{\bm{s}}+b_{0}),\qquad h_{k}=\operatorname{ReLU}\bigl(\operatorname{BN}{k}(\operatorname{ConvT}{k}(h_{k-1}))\bigr),\quad k\in[L]. (5) Latents enter through feature-wise linear modulation (FiLM) ( Perez et al., 2018 ) , which rescales and shifts a feature map per channel by an affine function of 𝒛 {\bm{z}} : FiLM ⁡ ( h ; 𝒛 ) = ( 1 + γ ⁡ ( 𝒛 ) ) ⊙ h + β ⁡ ( 𝒛 ) , ( γ , β ) ​ ( 𝒛 ) = W ​ 𝒛 + b . \operatorname{FiLM}(h;{\bm{z}})=\bigl(1+\gamma({\bm{z}})\bigr)\odot h+\beta({\bm{z}}),\qquad(\gamma,\beta)({\bm{z}})=W{\bm{z}}+b. (6) FiLM is applied once to the last feature map and once to the image before the output nonlinearity, with a separate projection ( W , b ) (W,b) each time: g ⁡ ( 𝒔 , 𝒛 ) = tanh ⁡ ( FiLM ⁡ ( Conv ⁡ ( FiLM ⁡ ( h L ; 𝒛 ) ) ; 𝒛 ) ) . g({\bm{s}},{\bm{z}})=\tanh\Bigl(\operatorname{FiLM}\bigl(\operatorname{Conv}\bigl(\operatorname{FiLM}(h_{L};{\bm{z}})\bigr);{\bm{z}}\bigr)\Bigr). (7) We initialize both projections to zero, so FiLM starts as the identity and training begins from a state-only decoder, with the latent modulation learned on top of it. The zero initialization, together with FiLM acting per channel, keeps the geometry of the image tied to the state and leaves its appearance to the latents. Verifiability. Apart from the FiLM product, the model uses only linear, convolution, batch normalization, ReLU, and tanh \tanh layers, all of which standard verifiers bound. Batch normalization ( Ioffe & Szegedy, 2015 ) is a per-channel affine map at inference. Layer and group normalization instead compute their statistics from the input and divide by an input-dependent standard deviation, a division that verifiers bound loosely. The FiLM product γ ⁡ ( 𝒛 ) ⊙ h \gamma({\bm{z}})\odot h multiplies an affine function of 𝒛 {\bm{z}} by a feature map that depends on 𝒔 {\bm{s}} , and we bound it with the standard McCormick relaxation ( McCormick, 1976 ) for a product of two bounded quantities. Training. The model is trained by supervised regression on simulated camera images. We collect closed-loop rollouts in which the controller acts on the true state, and record each image together with the state 𝒔 {\bm{s}} and latents 𝒛 {\bm{z}} at which it was rendered. The latents are held fixed within a rollout and varied across rollouts to cover ℤ {\mathbb{Z}} (Appendix B ). The objective is a pixel-wise ℓ 1 \ell_{1} loss plus a structural similarity (SSIM) term ( Wang et al., 2004 ) with equal weights, ℒ = ∥ g ⁡ ( 𝒔 , 𝒛 ) − 𝒐 ∥ 1 + 1 − SSIM ⁡ ( g ⁡ ( 𝒔 , 𝒛 ) , 𝒐 ) \mathcal{L}=\lVert g({\bm{s}},{\bm{z}})-{\bm{o}}\rVert_{1}+1-\mathrm{SSIM}(g({\bm{s}},{\bm{z}}),{\bm{o}}) . The model is fit to the images alone and is never tuned to the controller or the verification process. It is small enough to train in under a minute on a single H100. 𝒔 {\bm{s}} linear reshape h 0 h_{0} h 1 h_{1} h k h_{k} h L h_{L} FiLM Conv FiLM tanh \tanh g ⁡ ( 𝒔 , 𝒛 ) g({\bm{s}},{\bm{z}}) L × L\times ConvT → \to BatchNorm → \to ReLU sun altitude 𝒛 ∈ ℤ {\bm{z}}\in{\mathbb{Z}} ( γ , β ) = W ​ 𝒛 + b (\gamma,\beta)=W{\bm{z}}+b 𝒛 {\bm{z}} modulates appearance through FiLM Figure 3: The world model renderer g g . A linear layer lifts the state 𝒔 {\bm{s}} to a coarse feature map, and L L stages of transposed convolution, batch normalization, and ReLU upsample it. The latents 𝒛 {\bm{z}} act through two FiLM modulations, which rescale and shift the last feature map and the image. 5 Verification Procedure We extend state-based verification of neural feedback systems to the vision-based setting, building on the formalization in Section 3 . Recent state-based methods combine open- and closed-loop verification ( Kochdumper et al., 2023 ; Akinwande et al., 2026b ) , and we take the same approach. We start from an existing open-loop verifier ( Xu et al., 2021 ; Wang et al., 2021 ) and add methods to support closed-loop analysis. We partition the initial set 𝐈 \mathbf{I} uniformly into cells and resolve each cell with falsification, forward analysis, adaptive refinement, symbolic analysis, and backward analysis, which the following paragraphs describe (Algorithm 1 ). Falsification is the cheapest part of the procedure, and in our experiments, uniform sampling of initial states and latents finds most failing trajectories. For each cell, the falsifier samples initial states and latents densely, and simulates each sample through the perception surrogate, the controller, and the dynamics. Trajectories that enter an unsafe set are reevaluated in higher-precision arithmetic. A cell with a confirmed unsafe trajectory is falsified , and every other cell is unresolved . A falsified cell may still contain safe states, but we mark the whole cell unsafe so that the verified region remains a sound under-approximation of the safe set. Forward analysis computes per-step bounds on the states reachable from each unresolved cell. Sound bounds on the next states require bounds on the observations the perception surrogate can produce from the current states and any latents in ℤ {\mathbb{Z}} , on the actions the controller can take on those observations, and on the states the vector field 𝐅 \mathbf{F} reaches under those actions. We compute these bounds by building on existing algorithms and abstractions for verifying neural networks ( Wang et al., 2021 ) and state-based neural feedback systems ( Akinwande et al., 2026b ) . The result is a sound over-approximation of the forward trajectories of every state in the cell. If the over-approximation satisfies the reach-avoid specifications, the cell is verified ; otherwise, it remains unresolved. To reduce the conservatism of the over-approximation, we apply abstraction optimization , which tunes the free parameters of each abstraction, such as the slopes of ReLU relaxations. Our scheme builds on similar schemes for neural network ( Xu et al., 2021 ) and state-based system ( Akinwande et al., 2026b ) verification. Algorithm 1 Verification procedure. 1: surrogate system 𝒟 \mathcal{D} with latent box ℤ {\mathbb{Z}} ; partition resolution N N ; refinement depth D A D_{A} for each analysis A A 2: for each cell C C of the uniform partition of 𝐈 \mathbf{I} into N n N^{n} cells do 3: if Falsify ( C C ) then 4: mark C C falsified 5: else 6: Q ← { C } Q\leftarrow{C} 7: for A ∈ ( Forward , Symbolic , Backward ) A\in(\textsc{Forward},\textsc{Symbolic},\textsc{Backward}) do 8: Q ← Resolve ​ ( A , Q , D A ) Q\leftarrow\textsc{Resolve}(A,Q,D_{A}) ⊳ \triangleright refined subproblems A A leaves unverified 9: end for 10: mark C C verified if Q = ∅ Q=\emptyset , and unresolved otherwise 11: end if 12: end for Adaptive refinement reduces conservatism further by shrinking the domain over which each abstraction is built, since abstraction optimization alone can leave large portions of the state space unresolved. Our scheme combines input splitting ( Rober & How, 2024 ) , neuron splitting ( Wang et al., 2021 ) , and enclosure refinement ( Akinwande et al., 2026b ) . Each refinement splits the problem into subproblems, and a cell is verified only if all of its subproblems are. We refine up to a fixed depth, and subproblems that remain unverified at that depth are evaluated via symbolic analysis. Symbolic analysis keeps the correlations between steps that per-step forward analysis discards. It unrolls the closed loop over several steps, and bounds the trajectory in one shot, minimizing the approximation error that accumulates over the horizon (Section 3.2 ), and that abstraction optimization and refinement often cannot recover. Symbolic analysis was developed for state-based systems ( Sidrane et al., 2022 ) , and has since been extended to the vision-based setting ( Cai et al., 2025 ) . We build on the vision-based method with optimizations that make the analysis tractable for our surrogates. Symbolic analysis remains expensive, so we reserve it for the cells that the previous analyses leave unresolved. Backward analysis over-approximates the set of states from which the closed loop reaches the unsafe set 𝐀 \mathbf{A} . Forward analysis must propagate its over-approximation over the full horizon, and its abstractions loosen as that set grows, so some of its conservatism is inherent to its direction. For some problems, the backward computation is tighter. Recent work combines backward and forward analysis to verify reach-avoid specifications ( Akinwande et al., 2026a ) , and we extend this idea to the vision-based setting. We carry the forward bound to an intermediate step, and use backward analysis from 𝐀 \mathbf{A} to show that the forward set at that step cannot reach 𝐀 \mathbf{A} within the remaining horizon. This combination resolves cells that forward analysis alone cannot. 6 Evaluations We evaluate on two vision-based control benchmarks from the surrogate verification literature. On both, we measure the fidelity of the world model against held-out images (Section 6.2 ). On emergency braking, the benchmark that remains open, we also run our verification procedure (Section 6.3 ). All bound computations run on an NVIDIA H100, and we report cost in GPU-hours. 6.1 Case studies Aircraft Taxiing. We wish to verify that an aircraft taxiing down a runway stays on the runway. The state is the aircraft’s crosstrack position p p and heading error θ \theta , which evolve under a nonlinear map. A camera mounted on the wing captures images, a perception network reads them to estimate the state, and a proportional controller uses the estimate to set the steering angle. Baselines. Authors in Katz et al. (2022) replace the camera with a conditional GAN (cGAN) trained on X-Plane images, with a two-dimensional latent that covers variation at a fixed state. To keep the resulting system verifiable, they distill the GAN into a smaller MLP. They partition the initial set into 128 × 128 128\times 128 cells and verify the surrogate system with standard neural network verification tools. Cai et al. (2025) have since verified the benchmark as well, so we focus on the modeling problem. Appendix A gives further details on the benchmark. Automatic Emergency Braking (AEBS). We wish to verify that an autonomous vehicle stops short of a stationary obstacle. The state is the distance to the obstacle and the vehicle’s speed. A front-facing camera captures images, a perception network reads them to estimate the distance, and a controller trained with deep deterministic policy gradient (DDPG) maps the estimate and the true speed to a braking command at 20 Hz. Baselines. Authors in Cai et al. (2025) replace the camera with a GAN and check the property for every state in each cell of a 100 × 100 100\times 100 grid over the initial set and for every image the surrogate can render. They test a grayscale cGAN with a convolutional perception head and an RGB self-attention GAN (SAGAN) with an attention head. Their approach leaves 38% of the state space unresolved with the cGAN and reports no results for the SAGAN at 20 Hz. 6.2 Modeling Quality Held-out GAN World model Aircraft Taxiing AEBS − 10 -10 − 5 -5 0 0 5 5 10 10 true state estimated state Held-out GAN World model 0 0 10 10 20 20 30 30 40 40 true state 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. Our world models reproduce held-out frames more faithfully than the GAN surrogates on both case studies. Since a verification result covers the set of images the surrogate can render, a higher-fidelity surrogate makes that result more informative about the system it stands in for. We measure fidelity on held-out frames by root mean square error (RMSE) and by structural similarity (SSIM), and report the results in Table 1 . On Aircraft Taxiing, even our smallest world model, with 50k parameters, renders the scene better th The same ai evaluation question is explored in NNV3, which adds a research perspective. as detailed in the full paper on Arxiv The robotics story also surfaces in MIT Researchers Develop Method to Make..., adding another angle.