PaperlayerView exact revision on arXiv

Source-linked AI summary

Stochastic World Models for Verifying Vision-Based Neural Feedback Systems

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

arXiv:2609.38120v1cs.AIcs.SYeess.SY

TL;DR

Vision-based verification needs a tractable model of the observations and variation a controller encounters. The paper formalizes perception surrogates, trains stochastic world models with physically grounded latents, and combines verification analyses. The models better reproduce held-out frames with fewer parameters than GANs, while the procedure resolves all grayscale benchmark cells and over 80% of RGB cells.

  • Problem

    Vision-based neural feedback verification needs a faithful, tractable model of sensor observations, but existing GAN and alternative surrogates have limitations in fidelity or closed-loop tractability.

    Source: §1 · p. 1

  • Method

    The paper formalizes the sensor as a generative model and trains stochastic world models with physically grounded latents, then combines falsification, refinement, symbolic, and backward analyses for verification.

    Source: §1 · p. 2, §3.1 · p. 3, §4 · p. 4

  • Results

    With up to 130 times fewer parameters, world models better reproduce held-out frames; the procedure resolves every grayscale AEBS cell and over 80% of RGB AEBS cells.

    Source: §1 · p. 2, §6.2 · p. 7, §6.3 · p. 8

  • Takeaways & Limitations

    Higher-fidelity surrogates make verification results more informative about the systems they represent, while the reported guarantees remain guarantees for the surrogate system.

    Source: §6.2 · p. 7, §7 · p. 9

    The world models are trained and evaluated on simulated frames, and no formal guarantee relates the surrogate to the camera it replaces.

    Source: §7 · p. 9

Abstract

from arXiv · show

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

Vision-based verification must model image variation while remaining tractable for closed-loop analysis, a balance prior perception surrogates have not resolved. The paper introduces physically grounded stochastic world models and a combined verification procedure.

1 INTRODUCTION

  • Vision-based systems close a neural feedback loop through image observations, but their verification remains challenging because the environment and sensor must be modeled faithfully and tractably.The safety guarantee for the real system holds to the extent that its model is faithful.Source: §1 · p. 1
  • Earlier GAN surrogates leave systems partly unresolved, while other surrogates either fail to capture sensor-image variation or are intractable to verify in closed loop.A deterministic world model produces one observation per state and therefore does not model environmental variation.Source: §1 · p. 1
  • The procedure resolves every cell of grayscale emergency braking and over 80% of RGB emergency braking, while the world models outperform GAN surrogates in held-out-frame fidelity with up to 130 times fewer parameters.The grayscale benchmark includes the 38% of state space the state-of-the-art verifier left unresolved.Source: §1 · p. 2
  • The world model concentrates image variation in a few physically grounded latents, and the verification procedure combines falsification, adaptive refinement, symbolic, and backward analyses.The model is built from operations that standard verifiers bound and is trained on closed-loop controller rollouts.Source: §1 · p. 2

2 RELATED WORK

Prior work supplies tools for neural-network and state-based verification and explores several perception surrogates. The paper's context highlights a gap between modeling observation variation and keeping verification tractable.

2 RELATED WORK

  • State-based neural feedback verification builds on network bounds and refinement, with forward methods propagating reachable sets and backward methods finding states related to unsafe or goal sets.The passage cites LiRPA, mixed-integer encodings, and refinement methods.Source: §2 · p. 2
  • Perception surrogates range from conditional GANs to variational autoencoders, formal perception models, and deterministic world models, each with different modeling or verification limitations.Cai et al. (2025) leave 38% of the grayscale emergency-braking system unresolved and report no result for its RGB version.Source: §2 · p. 2
  • World models serve as environment surrogates across domains, but their latents typically lack physical meaning, so a guarantee over them does not specify which conditions it covers.Prior work has argued for physically interpretable latents by construction (Peper et al., 2025) and learned them under weak supervision.Source: §2 · p. 2
  • Figure 1 contrasts cGAN variation from an ungrounded Gaussian latent, a deterministic model with no variation, and a stochastic world model with bounded physical latents.The surrogate determines the variation the closed loop can see.Source: Figure 1 · p. 3
  • Combined verification strategies use refinement, falsification-guided reachability, and integrated forward and backward analyses to help decide properties when one analysis is insufficient.The cited examples include refinement where counterexamples are spurious (Li et al., 2026) and integrated reachability for neural feedback systems (Akinwande et al., 2026a).Source: §2 · p. 3

3 PROBLEM FORMULATION

The formulation represents a neural feedback system as a discrete-time dynamical system with a sensor, controller, and reach-avoid objective. A generative perception surrogate places vision-based systems in this framework, where reachability analyses can be applied.

3 PROBLEM FORMULATION

  • The notation defines 2X as the power set, [i..j] as an integer range, [n] as [1..n], and S_t as the t-th element of sequence S.Functions applied to sets act elementwise, with results unioned.Source: §3 · p. 3

3.1 NEURAL FEEDBACK SYSTEMS

  • The system tuple specifies state dynamics, perturbations, sensor, controller, initial set, time horizon, goal, and time-indexed unsafe states.Its next-state relation applies the vector field and controller-driven action, with perturbation and sensor input, over step length δ.Source: §3.1 · p. 3
  • For vision-based systems, the camera sensor is replaced by a generative surrogate mapping state and latent inputs to observations, extending state-based verification techniques to the setting.The state-based case is recovered when the sensor is the identity map.Source: §3.1 · p. 3
  • A reach-avoid specification requires every trajectory to reach the goal and avoid unsafe states at every step, yielding safety across the environmental inputs in Ξ.The forward and backward examples show initial sets classified as safe or unsafe according to their relation to reachable and unsafe states.Source: §3.1 · p. 4, Figure 2 · p. 4

3.2 REACHABILITY ANALYSIS

  • Forward analysis over-approximates trajectories to check unsafe sets and the goal, whereas backward analysis approximates states that can reach unsafe states or the goal.Both accumulate approximation error over the horizon; adaptive refinement, symbolic analysis, and combined forward-backward analysis reduce it.Source: §3.2 · p. 4

4 STOCHASTIC WORLD MODELS

The stochastic world model renders images from system states and physically grounded latents, making sensor variation correspond to ranges of environmental conditions. Its decoder is designed around verifier-boundable operations and trained on simulated camera images.

4 STOCHASTIC WORLD MODELS

  • Physically grounded latents range over a box of conditions, so the renderer's possible images correspond to environmental conditions at each state.The latent vector is the renderer's only source of variation and may range independently at every step.Source: §4 · p. 4
  • A linear layer lifts the state to a coarse feature map, then L transposed-convolution stages upsample it.The stages use batch normalization and ReLU.Source: §4 · p. 4, Figure 3 · p. 5
  • Two FiLM modulations let latents rescale and shift the last feature map and image, with zero-initialized projections starting as identity.This initialization starts training from a state-only decoder, leaving image geometry tied to state and appearance to latents.Source: §4 · p. 4
  • Except for the FiLM product, the renderer uses linear, convolution, batch-normalization, ReLU, and tanh operations that standard verifiers bound.The FiLM product is bounded with the McCormick relaxation for a product of bounded quantities.Source: §4 · pp. 4–5
  • The model is trained by supervised regression on simulated camera images using equally weighted pixel-wise ℓ1 and SSIM losses.Training rollouts hold latents fixed within a rollout and vary them across rollouts to cover Z; the model is not tuned to the controller or verification process.Source: §4 · p. 5

5 VERIFICATION PROCEDURE

The procedure partitions the initial state set and applies falsification, forward analysis, adaptive refinement, symbolic analysis, and backward analysis to resolve cells. Costlier analyses are reserved for cells left unresolved by earlier stages.

5 VERIFICATION PROCEDURE

  • The procedure partitions the initial set into cells, tries falsification first, then applies forward, symbolic, and backward analyses to remaining subproblems.The algorithm marks a cell verified only when no subproblems remain unresolved.Source: §5 · pp. 5–6
  • Falsification densely samples initial states and latents, simulates trajectories, and confirms unsafe trajectories at higher precision.A cell with a confirmed unsafe trajectory is marked falsified; the whole cell is marked unsafe to keep the verified region a sound under-approximation of the safe set.Source: §5 · p. 5
  • Forward analysis bounds reachable states per step and verifies a cell when its sound over-approximation satisfies the reach-avoid specifications.Abstraction optimization tunes free parameters, such as ReLU relaxation slopes, to reduce conservatism.Source: §5 · p. 5
  • Adaptive refinement splits problems by input, neuron, or enclosure and verifies a cell only when all resulting subproblems are verified.Refinement stops at a fixed depth, after which remaining subproblems proceed to symbolic analysis.Source: §5 · p. 6
  • Symbolic analysis unrolls the closed loop and bounds multi-step trajectories together, retaining correlations discarded by per-step forward analysis.Because it is expensive, it is reserved for cells unresolved by earlier analyses.Source: §5 · p. 6
  • Backward analysis over-approximates states that can reach the unsafe set and can rule out unsafe reachability from an intermediate forward bound.Combining it with forward analysis resolves cells that forward analysis alone cannot.Source: §5 · p. 6

6 EVALUATIONS

The evaluations compare surrogate fidelity on aircraft taxiing and emergency braking, then test verification on grayscale and RGB AEBS benchmarks. World models improve held-out-frame fidelity, while the verification procedure resolves all grayscale AEBS cells and over 80% of the RGB state space.

6.1 CASE STUDIES

  • The two case studies are aircraft taxiing, with camera-based state estimation and steering control, and AEBS, where a camera-based distance estimate informs braking.Both benchmarks are evaluated for world-model fidelity; verification is also run on the emergency-braking benchmark.Source: §6 · p. 6, §6.1 · pp. 6–7

6.2 MODELING QUALITY

  • World models beat GANs on held-out fidelity in both benchmarks; the 50k taxiing model beats 2.76M DCGAN and 232k MLP GAN, and AEBS models beat GANs 14–130× larger.The AEBS fidelity gap is largest in SSIM, which measures whether scene structure is preserved.Source: §6.2 · p. 7, Figure 4 · p. 7, Table 1 · p. 8

6.3 VERIFICATION RESULTS

  • All 10,000 grayscale AEBS cells were resolved, versus 38% unresolved for Cai et al.; the RGB world-model run resolved over 80%.Most of the 1,822 unresolved RGB cells had not yet been analyzed.Source: Table 2 · p. 8, §6.3 · p. 8, Figure 5 · p. 9
  • Within 10 GPU-hours, the convolutional head verifies 120 cells versus 55 for a similarly sized attention head; the released 1.73M-parameter attention head verifies 10.The larger attention head reads distances from held-out frames more than twice as accurately.Source: §6.3 · p. 8, Table 3 · p. 9

7 CONCLUSIONS AND FUTURE WORK

The paper formalizes vision-based neural feedback systems for verification and reports more faithful world-model surrogates and stronger benchmark coverage. Its case-study definitions specify the aircraft-taxiing and emergency-braking states, observations, and control loops.

7 CONCLUSIONS AND FUTURE WORK

  • Despite up to 130 times fewer parameters, world models reproduce held-out frames more faithfully; verification resolves every grayscale cell and over 80% of the RGB state space.The grayscale result includes the 38% of cells left unresolved by the state-of-the-art verifier.Source: §7 · p. 9
  • The verification procedure combines falsification, forward analysis with abstraction optimization and adaptive refinement, symbolic analysis, and backward analysis.The system is formalized as a state-based system with a generative-model sensor, extending state-based verification techniques to vision-based systems.Source: §7 · p. 9

A NEURAL FEEDBACK SYSTEM DEFINITIONS

  • Aircraft Taxiing uses crosstrack position and heading error as state; a wing camera feeds TinyTaxiNet estimates into proportional steering, with frame variation represented in Ξ.The benchmark uses a 5 m/s taxi speed, a 0.05 s step, and a 16 s verification window.Source: A NEURAL FEEDBACK SYSTEM DEFINITIONS · p. 13
  • AEBS uses obstacle distance and vehicle speed as state; grayscale or RGB camera frames and speed feed a distance-estimating perception head and the released DDPG actor.Its observation has 1025 entries for grayscale or 3073 for RGB; lighting and weather variation are represented in Ξ.Source: A NEURAL FEEDBACK SYSTEM DEFINITIONS · p. 13

B WORLD MODEL TRAINING

The RGB emergency-braking world model is trained on simulated CARLA rollouts, with sun altitude as a rollout-level latent and a held-out split by trajectory.

B WORLD MODEL TRAINING

  • 240 CARLA rollouts yield 13,056 frames, split by rollout into 150 training, 40 validation, and 50 held-out rollouts stratified by sun altitude.Initial states are stratified over distance 5–60 and speed 2–30; sun altitude is drawn once per rollout from 0° to 90°.Source: B WORLD MODEL TRAINING · p. 14
  • The RGB world model has 28,591 parameters and is trained for 120 epochs with Adam, using the final weights without early stopping.Its architecture lifts state to a 32 × 4 × 4 map, then uses three stages with 32, 16, and 8 channels and a 3×3 output convolution.Source: B WORLD MODEL TRAINING · p. 14
  • RGB perception heads use the same rollout split and optimizer settings, trained for 60 epochs with an ℓ1 loss on distance divided by 60.Source: B WORLD MODEL TRAINING · p. 14

C FIDELITY EVALUATION

Fidelity is evaluated by rendering surrogates at held-out frame states and scoring image similarity; the emergency-braking GAN comparison has an unresolved training-data overlap caveat.

C FIDELITY EVALUATION

  • Surrogate fidelity is scored against held-out frames using pixel-and-channel RMSE and SSIM averaged over channels for RGB.The RGB world model also receives each frame’s sun altitude; GAN latents and world-model latents without a physical latent are set to their range centers.Source: C FIDELITY EVALUATION · p. 14
  • For emergency braking, 2,487 held-out frames come from the RGB world model’s split, but overlap with cGAN and SAGAN training data cannot be confirmed.Those generators’ training data was not published.Source: C FIDELITY EVALUATION · p. 14
  • Aircraft taxiing uses 1,002 held-out frames; the MLP GAN was distilled from a DCGAN trained on all 10,000 frames, so it saw those held-out frames during training.The DCGAN weights were unavailable, so it was retrained from the cited code on the same training frames.Source: C FIDELITY EVALUATION · p. 14

D VERIFICATION PROCEDURE SETTINGS

The verification settings partition emergency braking into grid cells and apply different refinement budgets; numerical soundness is not claimed against floating-point error inside the bounding library.

D VERIFICATION PROCEDURE SETTINGS

  • The 100 × 100 emergency-braking grid is refined into K × K sub-cells, and a cell is verified only if every sub-cell is verified.Sub-cells remain unresolved if they reach the horizon without a falsification or verification decision.Source: D VERIFICATION PROCEDURE SETTINGS · p. 14
  • At K ∈ {4, 6}, a pass stops at its first failing sub-cell; at K ∈ {1, 2}, all sub-cells are analyzed so verified pieces can be reused.Table 4 lists settings for grayscale cGAN and RGB world-model experiments, with “Same” denoting the cGAN setting.Source: D VERIFICATION PROCEDURE SETTINGS · p. 14, Table 4 · p. 15
  • Bounds use float32 GPU computation with TF32 disabled and float64 sign tests, but soundness against floating-point error inside the bounding library is not claimed.Float32–float64 discrepancies are recorded to detect floating-point errors in the bounding library.Source: D VERIFICATION PROCEDURE SETTINGS · p. 14
  • The perception-head budget compares three heads on the same 10 × 10 cell block; up to three processes share one H100, and runs stop at 10 hours.The block spans distance 10.8–16.8 and speed 8.7–11.7; GPU-hours sum per-cell wall-clock times, including contention.Source: D VERIFICATION PROCEDURE SETTINGS · pp. 14–15

E VERIFICATION BREAKDOWN BY ANALYSIS

Tables 5 and 6 attribute each of the 10,000 benchmark cells to the Section 5 analysis that decided it. The tables cover grayscale and RGB AEBS benchmarks using different surrogates.

E VERIFICATION BREAKDOWN BY ANALYSIS

  • Tables 5 and 6 attribute each of the 10,000 cells to the Section 5 analysis that decided it.Source: E VERIFICATION BREAKDOWN BY ANALYSIS · p. 15
  • 2,669 grayscale AEBS cells verified by Cai et al. (2025) are all decided by backward analysis on the released cGAN surrogate.Table 5 reports this result for the grayscale benchmark.Source: Table 5 · p. 15
  • Of 1,825 unresolved RGB AEBS cells on the world-model surrogate, 1,822 have not yet been analyzed.Table 6 reports the RGB benchmark breakdown.Source: Table 6 · p. 15
Loading 2609.38120v1…