Stable and Verifiable Latent Dynamics
for World Models

Abstract

World models of the Dreamer family optimize policies over latent trajectories imagined by a recurrent state-space model, yet nothing in their training constrains those latent dynamics to be stable, and the categorical latent output blocks direct formal certification. We report two measured obstacles and an evaluation standard. First, a sampling-to-proof gap audit of the one-step latent map under a frozen actor: a Lyapunov decrease condition, a large random-sampling baseline, and branch-and-bound verification with a reachability gate. Second, a measured verifier wall: interval bound propagation asserts on the categorical output at any useful width, so every branch-and-bound box is recorded as unknown with its reason — never as a violation and never as certification. Third, a five-mode failure atlas from a controlled latent-space study shows why naive stability constraints fail, from which we derive design rules and an aliveness-gated evaluation standard. All claims name the object, region, and condition that produced them.

TL;DR: DreamerV3's latent map is sampled-clean but not provable (categorical wall), and bolting stability onto it fails five documented ways — here is the audit, the wall, the atlas, and the rules.

The audited object

DreamerV3's world model factorizes the transition into a deterministic recurrent core and a stochastic posterior over discrete classes. The object this project audits is the one-step latent map under a frozen deterministic actor,

where the stochastic output is replaced by the mean of the prior categorical, \(\pi(\mathbf{z}) = \tanh(\mathrm{mean}(\mathrm{actor}))\), and the model is audited as trained — only the Lyapunov candidate \(V\) moves. Nothing about the imagined multi-step rollout is certified, and nothing larger than the size-1M configuration (deter 512, hidden 64, stoch \(32 \times 4\)) is considered.

The condition is the Lyapunov decrease \(\mathrm{cond}(\mathbf{z}) = V(\mathbf{z}) - V(\mathbf{z}') > 0\), verified over a region built from the model's own on-policy latent states: the certified region is on-distribution by construction, and the certified map (the prior-mean surrogate) is recorded distinctly from the region's source, never conflated.

The sampling-to-proof gap audit

The audit asks one question: are there latent states where a large random-sampling audit of the decrease condition finds nothing, yet branch-and-bound verification finds a genuine violation that the model's own dynamics actually reach? The pipeline: fit \(V\) on samples from the region; run a sampling baseline (\(N\) i.i.d. draws, worst condition and count); run branch-and-bound over an annulus around the latent fixed point (holed along the \(k\) widest dimensions, so box count scales with \(k\), not with the 640-D latent); apply a reachability gate to every candidate violation — off-distribution counterexamples are discarded, not reported with a caveat.

The measured verifier wall

The certified graph contains the categorical output \(\mathbf{s}' = \mathrm{softmax}(\mathrm{logits}')\), i.e. an \(\exp / \sum \exp\) with a division by the relaxed sum. Interval bound propagation asserts on this node whenever the relaxed logits interval spans a region where the softmax denominator can be non-positive in the bound computation — at the measured vacuity of intermediate bounds, this happens on the first box (AssertionError in BoundReciprocal), and the same structural failure repeats identically on every box. Because the bound-graph build dominates per-box cost (~4 minutes on a size-1M graph on CPU), running full branch-and-bound without the wall gate wastes hours to rediscover the same assertion.

The audit therefore probes the wall once and records every box as unknown with the reason — never certified, never a violation. The sampling baseline is the empirical result, and a sampling violation is the only thing that can become a finding.

The smoke configuration is a weight-initialized surrogate, not a trained model; its numbers establish that the pipeline is sound and reproducible, which is their only claim. The trained-model audit on dm_control cartpole_balance is the open item (GPU run); on the categorical wall its expected verdict is unknown, which is verifier incompleteness, not a finding.

The failure atlas of latent-space stabilization

The wall says the frozen model cannot be certified directly. The remaining question is whether it can be stabilized — and the atlas is the answer, from a controlled latent-space study: a JEPA predictor with a Hamiltonian / metriplectic structure trained end to end on chaotic Lorenz-63 under a nonlinear coordinate warp, five ablation arms, matched data and steps. Imposing physical or thermodynamic constraints inside a self-supervised latent space does not, by itself, yield physical dynamics: the optimizer routes around each scalar constraint through a geometric exploit.

The headline is failure 4: pinning the divergence pins the sum of the Lyapunov spectrum, but the sum does not pin any individual exponent — confirmed four times, all with the "correct" sum. A scalar volume constraint is structurally incapable of shaping the leading exponent. And the overlap trap: Chamfer/Hausdorff distance to the encoded attractor rewards a frozen predictor, so geometric overlap must be gated on the rollout being alive and chaotic (\(\lambda_1 > 0\), sane motion ratio) — or replaced by a motion-invariant statistic.

Design rules

1. Certify a verifiable surrogate, not the categorical output. Certification must target the deterministic component of the latent map or a structurally verifiable surrogate; the stochastic output is the documented boundary of the toolchain.
2. Constrain modes, not sums. Constrain per-mode radii and verify the leading exponent directly, never the aggregate.
3. Break dead saddles with principled initialization. Factorized dissipation needs a nonzero init and a gradient-path check.
4. Use shape constraints, not raw magnitudes. Scale-free (z-score / correlation) anchors prevent scale-starvation.
5. Curriculize the horizon and gate evaluation on aliveness. Long-horizon rollouts, an aliveness gate, a leading-exponent check — never attractor overlap without them.
6. Report the gap honestly. unknown is verifier incompleteness; only a reachable violation counts, and it must survive the reachability gate.

Status and reproducibility

• The audit pipeline runs end to end on CPU (the smoke run above, ~2 minutes).
• The failure atlas is reproduced on CPU (single seed, 250-step schedule, 2026-08-13): every documented mode reappears with its own numbers (table below; full record in results/atlas_reproduction_cpu.md).
• The trained-model heavy run is a turnkey Colab notebook: train size-1M on dm_control cartpole_balance from pixels, export the JAX weights under the upstream key names, roll out the on-policy latent support, run the audit, and produce results/d1_seed0.json as the artifact.
• Everything is pinned: the dreamerv3 commit (whose vendored embodied is the exact math the torch port transcribes), the verifier (auto_LiRPA 0.7.2 at its validated commit, plus the SHA-256 of the driver), and the sources of every number.

Honest reading of the heavy run: sampling-clean + branch-and-bound unknown on the categorical wall is a null result — verifier incompleteness, not a gap, and not email material on its own. Only a sampling violation that survives the reachability gate counts.

Citation