Stochastic World Models for Verifying Vision-Based Neural Feedback Systems

What it claims

A vision-based neural feedback system can be treated as a state-based one whose sensor is a generative model g(s, z): state in, latents in, image out. With that framing, state-based reach-avoid verification carries over directly. The perception surrogate is a small stochastic world model whose only source of variation is a few latents tied to physical quantities, such as sun altitude, haze or blur, each ranging over an interval. A verified result therefore covers a nameable box of environmental conditions, not a box of GAN noise with no physical meaning. Per the abstract, the model reproduces held-out frames better than GAN surrogates with up to 130× more parameters. The verification procedure resolves the whole grayscale emergency-braking state space, where the prior verifier (Cai et al., 2025) left 38% unresolved, and over 80% of the RGB variant, which had no prior verification results.

How it works

Renderer. It is a DCGAN/DreamerV3-style deconvolutional decoder:

1. A linear layer lifts the state to a coarse feature map.
2. L stages of transposed convolution, batch norm and ReLU each double the resolution.
3. Latents enter only through two FiLM modulations, one on the last feature map and one on the image before the output tanh.
4. Both FiLM projections are zero-initialised, so training starts as a state-only decoder. Geometry stays tied to the state and appearance to the latents.

Built to be verifiable.

• It uses only linear, convolution, batch-norm, ReLU and tanh layers, plus the FiLM product.
• Batch norm is chosen over layer or group norm because batch norm is affine at inference. Layer and group norm divide by an input-dependent standard deviation, which verifiers bound loosely.
• The FiLM product γ(z)⊙h is bounded with a McCormick relaxation.

Training.

• Supervised regression on simulated images from closed-loop rollouts, with the controller acting on the true state.
• Latents are fixed within a rollout and varied across rollouts.
• Loss is pixel ℓ1 plus (1 − SSIM), equally weighted.
• The model is never tuned to the controller or the verifier.
• Training takes under a minute on a single H100.

Verification (Algorithm 1). The initial set is partitioned uniformly into Nⁿ cells. Each cell goes through:

flowchart TD
  C[Cell of initial set] --> F{Falsifier finds<br/>unsafe trajectory?}
  F -- yes --> X[Whole cell FALSIFIED]
  F -- no --> FW[Forward analysis<br/>+ refinement]
  FW --> SY[Symbolic analysis<br/>on leftovers]
  SY --> BW[Backward analysis<br/>on leftovers]
  BW --> R{Subproblems left?}
  R -- none --> V[VERIFIED]
  R -- some --> U[UNRESOLVED]

• Falsification densely samples initial states and latents. Candidate failures are re-checked in higher precision. The authors report that uniform sampling finds most failing trajectories.
• Forward analysis builds on α,β-CROWN-style bounding (Xu et al., 2021; Wang et al., 2021). It adds abstraction optimisation, which tunes free parameters such as ReLU relaxation slopes.
• Refinement depth is set separately for each analysis.
• Each later analysis only works on the subproblems the previous one could not verify.

Limits

• Coverage only as good as the surrogate. The guarantee holds for the real system only to the extent the world model is faithful. It covers only the latent box Z the authors chose.
• Conservative falsification. A falsified cell is marked unsafe in its entirety, even if it contains safe states. The verified region is a sound under-approximation and may understate the true safe set.
• Latents vary freely in verification. The surrogate lets z vary independently at every step, while training data holds z fixed per rollout.
• Narrow evaluation.
• The verification procedure is evaluated only on emergency braking.
• The world model is evaluated on that benchmark and on aircraft taxiing.
• The full grayscale result uses the released GAN surrogate. The RGB result uses the world model.
• Truncated page. The fetched text stops inside the description of adaptive refinement. The following are not available here:
• experimental tables, runtimes and fidelity metrics
• the latent definitions (Appendix B)
• any code or release details
• the authors' own limitations section