Source-linked AI summary
World-Time Compute with Verified Code World Models
James Schwoebel, Ingrida Semenec, Jenia Rousseva, Marcos Ortiz, Collin Overbay, Christopher Klaus, Anderson Edmond, Manish Bhatt, Rome Thorstenson, Jessica Tsai, Martin G. Frasch
TL;DR
Most domains lack enough labeled examples for LLMs to generalize, so the paper uses verified executable world models to manufacture exact training trajectories. World-time compute improves generalization to unseen worlds, especially for smaller models and few-step symbolic reasoning, while gains weaken on longer, perception-heavy, saturated, or unrelated tasks.
Problem
Most domains lack the many real, labeled examples LLMs need to generalize, motivating a cheaper way to manufacture training data.
Method
World-time compute fine-tunes LLMs on exactly labeled trajectories generated by many executable, verifiable world models over symbolic state.
Results
40% on 60 held-out List Functions worlds versus 6% for a corrupted-label control, a +34-point lift; gains were largest at 0.5B and within noise by 32B.
Takeaways & Limitations
Verified worlds provide training signal for cross-world generalization, with the strongest benefits in few-step symbolic reasoning and smaller models.
Takeaways & Limitations
The demonstrated scope is symbolic-state worlds; pixel-native domains remain the territory of learned models, and performance drops as reasoning length or perceptual rule induction increases.
Abstract
from arXiv · showhide
LLMs generalize across a domain only after seeing many real, labeled examples, which most domains lack. We study a way to manufacture it cheaply. When a domain's dynamics can be written as code, one template instantiates into many world models: executable, verifiable programs over symbolic state, each an inexhaustible source of exactly-labeled trajectories. Fine-tuning an LLM on trajectories through many such worlds, which we call world-time compute, a training-time analogue of test-time compute, lifts generalization to held-out worlds it never trained on (synthesized world families). Gains are largest where capability is scarcest: +29 points at 0.5B; the largest model's lift is within noise, consistent with saturation. Labels can be trusted because the worlds are verified code: synthesized-then-checked dynamics are exact over 20-step rollouts and answer 10x out-of-distribution probes exactly (100%), whereas per-step LLM and MLP predictors compound error and collapse. Unlike domain randomization, each world is independently authored and verified; a corrupted-label control shows label exactness, not task variety, drives the gains. On real benchmarks (ARC-AGI grids, List Functions, CLRS) the same lever holds as per-world test-time training. On List Functions the harder cross-world form holds: one adapter trained on 128 disjoint worlds reaches 40% on held-out worlds versus 6% for a corrupted-label control (+34 points, CI [29, 39]). The gain is a saturating regularity, not a law: largest for few-step reasoning and small/weak models, fading for long chains, perception-induced tasks, and saturated tasks; cross-task transfer is weak without shared skill. Worlds are authored and served by OpenWorld, a zero-dependency framework (companion paper). Scope: symbolic state; pixel-native domains remain territory of learned models. All code, recipes, and this manuscript regenerate from one repository.
1 Introduction
The paper proposes manufacturing training experience from independently verified symbolic code worlds, then using trajectories through many worlds to improve generalization to held-out worlds. OpenWorld operationalizes this paradigm while showing that exact labels, rather than task variety alone, drive the gains.
- Code World Models use explicit, human-readable programs over symbolic state, trading perceptual breadth for auditable execution without compounding rollout error.They are intended for domains whose dynamics can be specified symbolically, not pixel-native or open-world 3D settings.
- OpenWorld combines plan–generate–verify synthesis, editable value specifications, automated tuning, and agents-as-a-judge into a reusable framework.Accepted transition code must pass parsing, sandbox, invariant, and optionally critic checks.
- +34 points: one adapter trained on 128 disjoint List Functions worlds reaches 40% on 60 held-out worlds versus 6% for corrupted-label control.The result is reported with CI [29] across three seeds.
- The approach differs from domain randomization and self-training because every world is independently synthesized and verified for label exactness.The paper tests whether exact labels, rather than task variety, explain held-out gains.
- Verified synthesized dynamics are exact on 24/24 20-step rollouts and answer 10× out-of-distribution probes at 100%, while LLM and MLP predictors fail.The per-step LLM proxy completes 0/24 rollouts, and the 10,000-transition MLP scores 0% out of distribution.
2 Problem Setting
The problem setting consists of symbolic environments with discrete actions and declarable dynamics, where an OpenWorld model must produce a faithful transition program and support exact training labels. Verification checks executable and invariant-consistent code, while acknowledging that this does not guarantee recovery of the true dynamics.
- OpenWorld targets JSON-serializable symbolic states, discrete action sets, and rule-based dynamics for operational simulations and program repair.Pixel-native domains are outside this setting.
- A world model contains symbolic states, actions, an initial state, a deterministic transition program, weighted objectives, and reachable-state invariants.The practitioner declares the schema, actions, rules, objectives, and invariants; the framework produces the transition.
- The setting separates world dynamics from perception, with raw-observation grounding treated as a distinct concern.The paper focuses on the dynamics-and-scoring core.
- World-time compute trains on exactly labeled examples produced by a verified world rather than rolling the transition forward during training.Labels may be answers fixed by hidden rules or next states computed by verified programs.
- OpenWorld synthesizes a transition program from natural-language rules and accepts it only after signature, sandbox, invariant, and optional critique checks.These checks certify invariant consistency, not equality with the true dynamics.
3 Experimental Setup
The experiments evaluate verified symbolic worlds, program repair, composition, changing rules, and learned-dynamics baselines using exact execution and reproducible statistical measures.
- Worlds with ground truth: Experiments compare synthesized and learned-style dynamics against three deterministic oracle worlds using exact state matching and fixed branch-covering probes.The oracle worlds are sprint, orchard, and triage; probes test clamping, empty queues, and interaction branches.
- The coding world: Program repair uses 20 buggy Python functions with hidden tests, bit-exact sandbox execution, and wall-clock alarms to score patches objectively.The tasks cover diverse defect archetypes, and looping patches fail instead of hanging.
- Benchmark-scale repair: Benchmark-scale repair compares single-shot completions with up to four in-world patch steps, where exact failing-test feedback begins after the first attempt.The suites require zero failures on both defect-targeting and regression-guarding tests.
- Composition, nesting, and changing rules: Composition experiments test monolithic versus modular synthesis, multi-level execution against an independent oracle, and phased rule changes against monolithic and next-state approaches.CompositeWorld preserves child namespaces and explicit couplings, while PhasedTransition advances ordered verified phases.
- Baselines: Learned-dynamics baselines include per-step LLM transitions, a two-hidden-layer MLP, and a 1-nearest-neighbor memorizer trained on 100, 1000, or 10000 transitions.The study explicitly distinguishes these baselines from trained Dreamer systems, whose pixel-native scale is infeasible on the stated hardware.
- Metrics and reproducibility: Evaluation reports exact-state fidelity, first-divergence step, final-state L1 error, pass@1, pass@budget, and confidence intervals or paired statistical tests where applicable.Seeds are fixed and all reported numbers regenerate through the paper’s asset-generation script; model-dependent results use specified Ollama snapshots and quantization.
4 Results
Verified code world models provide exact training trajectories that improve generalization to unseen worlds, with the largest gains for smaller models and short-step reasoning. The effect depends on label exactness, scales with world count when shared structure exists, and weakens on novel or harder real tasks.
- 4 Results: Verified synthesized engines achieve 24/24 exact 20-step rollouts, whereas per-step LLM prediction achieves 0/24.The verified engines also run at 14,997 steps/s versus 0.32 steps/s for the LLM engine after one-time synthesis.
- 4 Results: +29 points at 0.5B, from 37% to 66%, while the 32B lift is +3 points with a confidence interval including zero.The larger model is near the rules-given ceiling, so the gain is consistent with saturation.
- 4 Results: Held-out accuracy falls monotonically as training-label corruption increases, showing that label exactness, not task variety, drives the gain.The control keeps worlds, patients, prompts, and exact test labels fixed while varying only training-label corruption.
- 4 Results: World-time compute transfers across coding worlds in-domain but hurts 7B HumanEval greedy pass@1 from 78% to 70%, with positive transfer emerging at pass@5.The result supports scaling the verified world family rather than abandoning the approach.
- 4 Results: On ARC-AGI, per-world test-time training raises exact-match from 2% zero-shot to 10% heavy compute, while cross-task transfer remains weak.The corrupted-label ablation is used to test whether verified labels account for the lift.
5 Discussion and Limitations
Verified world models trade exact, auditable symbolic dynamics for limited scope, while world-time compute uses their trajectories to generalize across held-out worlds. The approach is most effective for few-step symbolic reasoning and remains distinct from ordinary fine-tuning through its dependence on verified labels and trajectory-level training.
- Interpretation: World-time compute is mechanically LoRA-SFT, but its distinguishing signal is unlimited, exactly labeled trajectories from verified dynamics rather than ordinary labeled data.Corrupted demonstrations on real ARC worlds fall to 2% versus the verified arm.
- Trajectory-level training: Verified trajectories outperform answer-pair training at the trained horizon, reaching 70% versus 58%, but the advantage reverses at longer rollout horizons.At the longer horizon, answer-pair training reaches 75% versus 68% for trajectory training, reflecting compounding in learned predictions.
- Operating regime: The method pays off most for few-step symbolic reasoning, while performance declines for longer chains, perception-induced tasks, and saturated tasks.The strongest reported regime includes List Functions, small grid transforms, and short-horizon planning.
- Routes: A verified world model can be served directly, distilled for tool-free inference, or traversed across a family for held-out-world generalization; a hybrid combines these routes.Table 7 distinguishes exactness and auditability, single-world amortization, family generalization, and their combination.
- Limitations: The approach is bounded by symbolic-state scope, while value alignment remains dependent on what structures and objectives the specification can express.The comparison is within the symbolic regime, and open specification manages rather than resolves the specification trap.
6 Conclusion
Verified code world models provide exact symbolic simulators that can support both planning and training. Traversing families of such worlds improves generalization to held-out worlds, but synthesis has a measured complexity boundary.
- Verified code world models are bit-exact where learned dynamics compound error and can support planning against ground truth.They are synthesized locally and verified before acceptance.
- Traversing many verified worlds lifts generalization to held-out worlds, making world-time compute a training-time analogue of test-time compute.The reported boundary is monolithic 7B synthesis failing past roughly eight interacting rules.
Declaration of generative AI use
The authors disclose using Claude 4.8 to implement, run, document, and edit the work under author direction. They retain responsibility, and report that results come from deterministic scripts rather than generative estimation.
- Claude 4.8 was used under author direction for framework implementation, experiments, figures, tables, and manuscript drafting and editing.
- The authors reviewed and edited the content, retain responsibility, and state that results were produced by released deterministic scripts.No AI tool is listed as an author.
Data and code availability
The complete research artifact is available in a repository, including code, benchmarks, scripts, raw results, and the manuscript build. The data are synthetic and contain no human-subject or patient data.
- Code, benchmarks, experiment scripts, raw result JSON, and the manuscript build are available at the OpenWorld repository.
- All data are synthetic, with no human-subject or patient data used.
Funding
The work received no specific external funding.
- The work received no specific external funding.
A Index of experiments
The paper indexes experiments E1–E85 as a navigation aid, while identifying retired, unused, and central world-time-compute experiments.
- Experiments E1–E85 are indexed by number with brief descriptions and locations to aid navigation.The experiments are introduced in thematic rather than numeric order.
- The index marks E14 and E53 as retired and several later experiments as unused or absent from the text.E28–E29 appear in setup but their dedicated results section was cut.
- The world-time-compute family E74–E85 carries the paper’s central result, including LODO fit, real-domain transfer, and trajectory-versus-answer training comparisons.E80 covers descriptive regularity, E81–E84 cover transfer and hybrid-loop results, and E85 compares training units.
B Detailed result tables
The detailed tables document synthesis reliability, verification-gate decomposition, scale-ladder accuracy, and tuning-strategy comparisons under specified experimental budgets.
- Synthesis reliability is reported across generator scales and model families with bounded attempts, repair iterations, and wall-clock accounting.Qwen rows use five compilation attempts per world; Llama and Gemma rows use three, with up to four verify–repair iterations.
- The verification-gate decomposition compares filtering and repair using paired high-temperature attempts from a 3B generator.The table uses eight paired attempts per regime.
- The remaining tables cover exact transition accuracy across a 1×/10×/100× scale ladder and tuning strategies on a 200-trial triage problem.The tuning comparison uses ten seeds per strategy.
C The synthesized dynamics artifact
The paper presents an accepted transition function synthesized by qwen2.5:7b and verified by the full gate, illustrating executable state updates for sprint-world actions.
- An accepted sprint-world transition synthesized by qwen2.5:7b and verified by the full gate underwrites Table 1’s exactness.
- The transition copies the state, reads the action name, and handles shipping when backlog is positive.Shipping decreases backlog, increases shipped work and debt, and adds bugs based on debt.
- The fix action reduces debt by two while clamping it at zero before returning the updated state.
D Example tasks and failure cases
The coding-world tasks expose bugs through hidden tests, while evaluation failures include repeated near-identical patches and order-sensitive judge behavior. These cases show both model-side local minima and judge-side auditing concerns.
- Hidden tests target concrete specification errors, including order-destroying deduplication and failure to detect early parenthesis imbalance.The examples contrast preserving first-seen order with list(set(xs)) and include the string ")(" as an early-imbalance case.
- High-temperature candidate sampling plus judge selection can escape a wrong initial specification reading that otherwise leads to repeated near-identical patches.The 1.5B baseline sometimes exhausted its attempt budget by resubmitting nearly identical patches.
- Judge outcomes require auditing because candidate-choice agreement fell to 28% under order reversal even when accuracy did not change.The passage identifies presentation order and judge criteria as concerns, while also noting score compression in mid-range episodes.
E Reproducibility
The paper rebuilds figures, tables, macros, and the PDF from committed experiment outputs through an automated asset pipeline. Reproducibility is exact for deterministic-offline runs and distributional for Ollama-dependent runs, with provenance and frozen artifacts recorded.
- The asset pipeline regenerates every figure, table, and numbers.tex macro from experiment JSON files, with fixed seeds recorded in source.
- A continuous-integration workflow reruns tests and asset generation, failing when generated numbers.tex would differ from committed results.The pipeline regenerates figures, tables, and macros from JSON before building the PDF.
- The experiment manifest classifies runs by determinism and records model provenance, while nine Ollama snapshots are used across the experiments.
- Deterministic-offline experiments reproduce bit-for-bit, whereas Ollama-dependent runs reproduce in distribution because Metal is not bit-deterministic at fixed seed.Dataset- and model-pinned frozen artifacts are used where exact numbers are cited, and result files record platform, versions, and timestamps.