📌 Highlights
AWM's central claim is that an agent can discover an explicit algebraic model of an unknown interactive environment and then use Lean 4 to prove both reachability and impossibility. The strongest evidence is complementary: all six AWM sealed-level runs produced closed kernel-checked impossibility proofs, while the ARC-AGI-3 study showed broad replay and competitive task performance. The main caveat is that proof correctness is conditional on the learned model and its coverage of relevant environment behavior.
- AWM formalized 25 learned world models, replayed 183 of 183 levels, and generated 220 Lean rules and 1,374 theorems.
- On ARC-AGI-3, AWM achieved a mean score of 99.9, cleared 23 games at 100, and used 7,448 certified actions, or 0.43 of the human baseline.
- On six sealed sc25 runs, AWM produced kernel-checked proofs in 6/6 runs and improved correct bounds from 4/6 to 6/6 after feedback.
- Two initial bounds were wrong because the learned rules were overly restrictive, demonstrating that formal validity and environmental fidelity are separate questions.
🎯 Introduction
The paper starts from a limitation of formal mathematical reasoning: existing AI systems generally receive predefined objects, definitions, and specifications. In an unfamiliar environment, an agent must infer the objects, action effects, costs, and success condition before it can reason rigorously. A winning trajectory establishes reachability, but impossibility requires excluding every legal winning sequence, including sequences never explored. AWM addresses this by learning executable hypotheses from interaction, organizing them into algebraic structure, and formalizing the resulting model so that Lean can check quantified claims about its dynamics.
🔬 Methodology
AWM models deterministic, goal-directed environments with partial observations in a POMDP setting. Observations, history, and auxiliary information are parsed into typed states w; rules specify applicability, effects, and costs; and a goal predicate identifies successful states. During Explore & Prototype, the concept book is repeatedly checked against the transition corpus using the exploration gate in equation 1. This prevents contradicted or failing hypotheses from silently remaining active while the agent continues probing.
Structure & Simplify rewrites concepts over typed objects and applies four transformations. Decomposition and composition use projective-limit structure to split or assemble compatible components; generalization and specialization use inductive-limit structure to extract shared rules or restore case-specific distinctions. Replacements must preserve recorded transition coverage and satisfy equation 2 on diagnostic rejections. In Formalize & Prove, Lean represents the objects and rules, replays observed winning trajectories, and checks reachability witnesses, invariants, or potential certificates. Equation 3 turns a potential into a lower bound on every winning sequence, while equation 4 illustrates the universal form of a sealed-level impossibility claim.
equation 1
Meaning: This is the exploration gate: every retained concept must remain consistent or out of scope on every recorded transition before further interaction is allowed.
equation 2
Meaning: When rules S are replaced by rules T, the simplified rules must preserve at least the rejected diagnostic transitions identified by the source rules.
equation 3
Meaning: The potential function supplies a lower bound on the remaining cost of reaching the goal and therefore supports budget-based impossibility proofs.
equation 4
Meaning: This sealed-level certificate states that every action list under budget 18 fails to win in the learned model, while a separate witness establishes a win at cost 19.
📊 Experiments
The main benchmark is ARC-AGI-3, consisting of 25 public games and 183 levels whose rules and goals are not revealed. AWM runs with Claude Opus 5, starts each game with an empty concept book, and evaluates score, cleared games, certified action counts, Lean replay, compactness, and generalization beyond observed trajectories. The official standard harness gives Claude Opus 5 and GPT-6 Astra no code execution, while AWM and other listed systems execute code; this distinction is part of the reported setup. AWM clears every level with a mean score of 99.9, reaches 100 on 23 games, scores at least 97.6 on every game, and uses 7,448 certified actions, 43% of the human baseline's 17,135.
The formalization results cover all 183 winning trajectories with 220 rules and 1,374 theorems, using only Lean's listed logical axioms. For generalization, frozen lp85 and ft09 models accept every valid transition in new-trajectory sets; they predict all 4,160 transitions in two modified lp85 layouts and reject all 4,031 transitions in two changed-mechanic ft09 sets. On ls20, final rules accept 99.47–99.95% of valid transitions on previously unseen screens, compared with 67–70% before Structure & Simplify. In the impossibility study, two constructed sc25 variants are sealed at budgets 18 and 35 while exhaustive engine search establishes minimum winning costs of 19 and 36. AWM produces proofs in all six runs, initially gets four of six bounds correct, and reaches six of six after feedback; five of the six model-level proofs are extended to the original games through engine-derived certificate checks.
tab:scores
Caption: Official scores on the 25 public ARC-AGI-3 games. Claude Opus~5 and GPT-6 Astra run under the official standard harness, which provides no code execution; the other systems execute code. AWM's certified clears follow uncertified sessions of the same run in 22 games. The actions for Rodionov's agent are from its ARC Prize scorecard and Memento~3's as reported in~ zhao2026memento3.
| System | Code | Mean score | Games at 100 | Certified actions | Actions / human |
|---|---|---|---|---|---|
| Claude Opus~5 | no | 40.7 | 5 | — | — |
| GPT-6 Astra | no | 68.3 | 10 | — | — |
| GPT-6 Astra (adapter) | yes | 100.0 | 25 | — | — |
| Rodionov (2026b) | yes | 99.0 | 23 | 8,347 | 0.49 |
| Memento~3 | yes | 100.0 | 25 | 7,518 | 0.44 |
| AWM (ours) | yes | 99.9 | 23 | 7,448 | 0.43 |
Why It Matters: This table reports the paper's ARC-AGI-3 score, clearance, and certified-action comparisons while preserving the different code-execution conditions.
tab:lean
Caption: Formalization and verification of the 25 learned world models in Lean~4. Axioms are those Lean's own logic uses; no proof adds axioms of its own.
| Levels replayed | Rules formalized in Lean | Theorems | Axioms |
|---|---|---|---|
| 183 / 183 | 220 | 1,374 | only propext, Classical.choice, Quot.sound |
Why It Matters: It quantifies the extent of formal coverage and records the logical assumptions used by the Lean developments.
tab:verdicts
Caption: Impossibility reasoning across six runs per agent. Bound accuracy is evaluated against the games' minimum winning costs before and after feedback-guided repair. First claim averages the earliest impossibility claim among runs making one, including later withdrawals; it is not proof-completion time. Per-run results are in Appendix~app:mainruns.
| Agent | Kernel-checked model proofs | Runs claiming impossible | Correct bounds initial → feedback | First claim (attempt) |
|---|---|---|---|---|
| Claude Opus~5.5 | 0/6 | 3/6 | 1/6 → 1/6 | 5.3 |
| GPT-6 Astra | 0/6 | 2/6 | 0/6 → 2/6 | 8.0 |
| AWM | 6/6 | 6/6 | 4/6 → 6/6 | 2.0 |
Why It Matters: The table separates formal proof production, willingness to claim impossibility, numerical bound accuracy, and the timing of the first claim.
fig:steps
Caption: AWM's three-stage pipeline: interactive exploration builds a provisional executable model, algebraic transformations reveal and simplify its structure, and Lean~4 formalization enables certified proofs of reachability or impossibility.
Why It Matters: This is the core system overview, showing how empirical exploration, algebraic abstraction, and formal proof fit together.
fig:condensation
Caption: Four transformations guided by projective and inductive limits, applied to object types and rules. Dashed boxes mark removed components and bold boxes mark introduced components; arrows indicate relationships between components. Generalization uses $r( )$, and an instance is written $r( _i)$; specialization makes distinctions explicit through case-specific types or parameters.
Why It Matters: The figure clarifies the algebraic operations used to compress fragmented concepts into shared or more specific rules.
fig:algebra
Caption: From shared structure to formal proofs in lp85. (a) Eleven concepts describing four button mechanisms are generalized into a shared permutation rule. Each before/after pair shows a recorded press, with the pressed button circled and changed tiles outlined. (b) A five-click sequence witnesses reachability. (c) Recoloring the only yellow tile makes the goal unreachable, since every press preserves color counts. Both conclusions are formally proved in Lean~4.
Why It Matters: This example demonstrates how abstraction reduces multiple mechanisms to one rule and supports both positive and negative formal conclusions.
fig:l4attempts
Caption: Sealed sc25 level 4. AWM proves in Lean that the minimum winning cost under its learned model is 19, one unit above the budget, and verifies a route at that cost; GPT-6 Astra claims 22 without a proof.
Why It Matters: The comparison makes the distinction between a kernel-checked tight lower bound and an unproved numerical claim concrete.
🔮 Conclusion
The paper presents AWM as a bridge from empirical exploration to formal reasoning. Its learned models are explicit enough to inspect and revise, while Lean checks replayed behavior, reachability witnesses, and impossibility certificates over arbitrary legal action sequences under the model. The ARC-AGI-3 results show that formalization can coexist with efficient play, and the sealed-level study shows that proof construction can expose the difference between a verified lower bound and an unsupported claim of optimality. At the same time, the two initially incorrect bounds demonstrate that kernel correctness does not by itself guarantee that the learned model captures the environment.
🛠️ Future Research Improvements
The clearest next step is to test whether the exploration, algebraic simplification, and proof-transfer workflow survives richer dynamics. The paper explicitly identifies hidden state, delayed feedback, and stochastic behavior as untested. Future evaluations should also measure how much exploration is required to achieve sufficient cover, how often overly restrictive rules create false lower bounds, and whether proof dependencies consistently guide repair across environments rather than only in the reported sc25 setting.
- Extend the model language to delayed observations, stochastic transitions, and persistent hidden state.
- Design benchmarks where the cheapest winning route is deliberately outside the initial exploration distribution.
- Separate model-relative proof validity, environment-level proof transfer, and task performance as independent evaluation targets.
- Measure exploration cost and repair cost alongside certified solution efficiency.
🏭 Potential Industry Use Scenarios
If the model-learning and proof-transfer assumptions generalize, AWM could support interactive systems that must learn operational rules and provide auditable guarantees rather than opaque success predictions. Plausible applications include verification of game-like planning environments, automated testing of stateful workflows, and safety analysis for bounded action sequences. These are forward-looking scenarios: the paper directly validates ARC-like games, not production workflows, robotics, or stochastic control systems, so deployment would require domain-specific observation models, cost definitions, and coverage checks.
- Auditable planning assistants for bounded, rule-based interactive tasks.
- Model-based testing that turns observed failures into explicit rule revisions and counterexamples.
- Formal safety or impossibility checks for workflow states when transition rules are discrete and inspectable.
- Verification layers for AI agents that must expose the assumptions behind a claimed lower bound or failed plan.
💬 Critical Analysis
AWM's strongest design choice is the separation between learned-model fidelity and proof validity. The concept book, typed rules, diagnostic rejections, replay checks, and explicit proof dependencies make it possible to identify whether a failure came from reasoning or from an omitted environmental rule. The sc25 results support this distinction: all six AWM runs produced closed proofs, but two initial bounds were wrong; feedback-guided repair corrected both, and five of six model proofs transferred to the original games under certificate-level checks.
The main unresolved issue is coverage. Sufficient cover is a meaningful bridge from model-relative theorem to environment-level claim, but establishing it can require exhaustive engine-derived checks that may not be available in a genuinely unknown world. The ARC results also combine different execution harnesses, and the impossibility study uses only two constructed variants. Overall, the paper provides unusually concrete evidence that formal proof can be integrated with interactive model discovery, while leaving open whether the same approach remains tractable and reliable when observations are delayed, stochastic, high-dimensional, or only partially diagnostic.