PaperlayerView exact revision on arXiv

Source-linked AI summary

Algebraic World Model: From Exploration to Proofs

Guancheng Pan, Qixin Tan, Yang Yuan, Andrew Chi-Chih Yao

arXiv:2610.40503v1cs.AIcs.LO

TL;DR

AI systems have made progress on machine-checked proofs, but typically start from predefined mathematical definitions rather than learning the rules of an unfamiliar world. AWM learns and formalizes explicit models through interaction; across 25 public ARC-AGI-3 games, it replays all 183 winning trajectories in Lean and reports a score of 99.9 with Opus 5.

  • Problem

    In unfamiliar environments, the objects and rules needed for rigorous reasoning must themselves be learned, unlike settings that begin with predefined mathematical definitions.

    Source: §1 · pp. 1–2

  • Method

    AWM tests and revises executable hypotheses through interaction, organizes them into typed objects and rules, and formalizes the model in Lean 4 for machine-checked reasoning.

    Source: §1 · p. 2, §2.4 · p. 5

  • Results

    Across all 25 public ARC-AGI-3 games, Lean replays winning trajectories for all 183 levels; with Opus 5, AWM scores 99.9 and its certified trajectories use 43% of the human baseline’s actions.

    Source: §1 · pp. 2–3

  • Takeaways & Limitations

    AWM makes learned mechanisms explicit and checkable while supporting kernel-checked proofs about reachability and impossibility, including sequences never explored.

    Source: §6 · pp. 10–11

    The demonstration covers ARC-like environments with discrete actions and immediate, observable feedback; richer hidden state, delayed feedback, and stochastic dynamics remain to be tested.

    Source: §6 · p. 10

Abstract

from arXiv · show

AI has made remarkable progress in mathematics, solving challenging problems with machine-checkable proofs in Lean, yet typically relying on predefined mathematical definitions and formal specifications. This raises a natural question: can it reason rigorously about an unknown world? We introduce the Algebraic World Model (AWM), a framework that turns interaction with unfamiliar environments into explicit mathematical models supporting formal reasoning. AWM explores the environment and develops executable Python hypotheses, continually testing and revising them against observations. It then structures these hypotheses into typed objects and shared rules, simplifies their structure through category-theory-guided transformations, and formalizes the resulting model in Lean 4 to prove reachability and impossibility. AWM can formally prove that a goal is unreachable, even beyond explored trajectories. On two impossible game levels, it constructs closed, kernel-checked Lean proofs excluding every legal winning sequence in all six runs, while Claude Opus 5.5 and GPT-6 Astra, equipped with coding tools, produce none in twelve baseline runs. Four of AWM's six initial bounds are correct, compared with one for Opus 5.5 and none for GPT-6 Astra; given only feedback that a cheaper win exists, AWM revises its rules and constructs new proofs, reaching six of six correct bounds. Moreover, AWM produces interpretable mathematical models whose rules can be inspected and tested step by step. Across all 25 public ARC-AGI-3 games, these models enable Lean to replay the winning trajectories of all 183 levels and generalize beyond observed play, predicting unseen transitions and detecting changes in game mechanics. With Claude Opus 5, AWM clears all levels with a score of 99.9, while its certified winning trajectories use only 43% of the human baseline's actions.

1 Introduction

AI proof systems typically rely on predefined definitions, leaving open whether they can reason rigorously about unfamiliar worlds whose objects and rules must first be learned. AWM learns and formalizes such models, producing certified proofs and inspectable trajectories across unfamiliar game environments.

1 Introduction

  • The motivating challenge is that unfamiliar environments require learning the objects and rules needed to reason about all legal sequences, not merely finding a winning trajectory.The Königsberg example illustrates how mathematical structure can rule out every route without enumerating them.Source: §1 · pp. 1–2
  • AWM learns explicit mathematical models through interaction, organizes them into typed objects and shared rules, and formalizes them in Lean 4 for proofs of reachability and impossibility.It tests and revises executable hypotheses against observed transitions, then applies category-theory-guided transformations checked in Lean.Source: §1 · p. 2, Figure 1 · p. 2
  • Six of six AWM runs produce closed, kernel-checked Lean proofs excluding every legal win on two impossible levels, while Opus 5.5 and GPT-6 Astra produce none in twelve runs.AWM’s initial bounds match minimum winning costs in four of six runs; after feedback that a cheaper win exists, it revises rules and reaches six of six correct bounds.Source: §1 · p. 2
  • 99.9 is AWM’s score with Opus 5 across all 25 public ARC-AGI-3 games, and its certified winning trajectories use 43% of the human baseline’s actions.Lean replays the winning trajectories of all 183 levels using models with a median of six object types and ten rules.Source: §1 · pp. 2–3
  • AWM’s typed objects and named rules make learned dynamics inspectable, and explicit proof dependencies identify which rules support a conclusion.Lean replay connects the formal representation to recorded behavior, supporting empirical checking and revision.Source: §1 · p. 3

2 Method

AWM turns interaction with unfamiliar environments into executable hypotheses, compact typed models, and Lean proofs. Its method combines active testing, structure-preserving transformations, and formal reasoning over legal action sequences.

2 Method

  • The method aims to build a coherent model that supports reasoning about action sequences the agent has never explored, through exploration, algebraic simplification, and Lean formalization.An executable representation supports empirical testing, while a formal representation supports mathematical reasoning.Source: §2 · p. 3

2.1 The Algebraic World Model

  • Typed objects describe valid states, while rules specify applicability, action effects and costs, and the goal predicate identifies successful states.Related mechanisms can share a parameterized operation, allowing common properties to be expressed and proved uniformly.Source: §2.1 · p. 3

2.2 Explore & Prototype

  • AWM actively probes the environment and maintains a concept book of executable Python hypotheses, revising or withdrawing concepts that fail against observed transitions.Each concept includes a claim, scope, supporting transitions, checker, and optional predictor; further interaction follows rechecking against the expanded corpus.Source: §2.2 · p. 4

2.3 Structure & Simplify

  • Structure & Simplify reorganizes fragmented concepts into compact models using decomposition, composition, generalization, and specialization guided by projective and inductive limits.Generalization extracts shared structure into a parameterized rule, while specialization makes distinctions explicit; transformations must preserve verdicts on recorded transitions and tested rejections.Source: §2.3 · pp. 4–5

2.4 Formalize & Prove

  • Lean 4 formalizes the simplified objects and rules, and proves reachability with a witness or impossibility using an invariant or a cost lower bound.For a budgeted task, a potential gives a lower bound on winning-sequence cost; proofs are closed and kernel-checked under explicit premises, and transfer to the environment under sufficient cover.Source: §2.4 · p. 5

2.5 Example: one rule for four mechanisms

  • In lp85, AWM generalizes eleven concepts for four button mechanisms into one permutation rule, then Lean certifies a five-click win and proves a recolored variant unwinnable.The shared rule retains all 55 recorded rejections and rejects 21 additional corrupted transitions; the final model has six object types and six rules and replays all 199 recorded transitions without mismatch.Source: §2.5 · pp. 5–6

3 Twenty-five public games

Across the 25 public ARC-AGI-3 games, AWM builds compact Lean-checkable models that replay winning trajectories and generalize to unseen transitions and changed mechanics. With Claude Opus 5, it clears every level with a score of 99.9 while using 43% of the human baseline’s certified actions.

Compact models that reproduce observed behavior

  • Lean replays the winning trajectories of all 183 levels from their initial states and checks each final state against the modeled goal.The models contain a median of six object types and ten rules per game.Source: §3 · p. 6
  • Across the 25 games, AWM retains 170 object types and 283 rules from 742 executable concepts, withdrawing 143 during revision.The retained models have a median of six types and ten rules per game.Source: §3 · p. 6

Generalization beyond observed transitions

  • Frozen rules predict all 4,160 modified lp85 layouts, reject all 4,031 changed-mechanic ft09 transitions, and accept 99.47–99.95% of unseen ls20 transitions, versus 67–70% before simplification.The tests use transitions from random play on previously unseen screens.Source: §3 · p. 7

Clearing the games with efficient solutions

  • 99.9 score; AWM clears every level across 25 public games, and its certified clears take 7,448 actions, 43% of the human baseline’s 17,135.The 99.9 score is reported for AWM with Opus 5; its 7,448 certified actions are the fewest among systems reporting that metric.Source: §3 · pp. 6–7

4 Proving impossibility

AWM uses learned algebraic models to prove that no legal winning sequence fits a sealed level’s budget, including sequences never explored. The experiments distinguish proof validity under a learned model from whether its bounds match the game, and test repairs and transfer to the original engines.

4.1 The game, the seal, and the baselines

  • The two sc25 variants preserve game mechanics but set budgets of 18 and 35, below their minimum winning costs of 19 and 36.The levels are sealed after selected elements are rearranged.Source: §4.1 · pp. 7–8

4.2 Certified lower bounds

  • All six AWM runs produce closed, kernel-checked impossibility proofs, unlike twelve baseline runs; initially, four of six AWM bounds are correct versus one for Opus 5.5 and none for Astra.For level 4, a lower bound of 19 and a matching witness establish a tight threshold under the learned model.Source: §4.2 · p. 8

4.3 Auditing premises and proving again

  • After feedback only that a cheaper win exists, AWM revises its rules and reaches correct bounds in all six runs; Astra corrects both baseline errors, while Opus corrects neither.The feedback does not reveal the cost, route, or faulty rule.Source: §4.3 · p. 9

4.4 From model proofs to the engine

  • Exhaustive checks of budget-feasible engine transitions extend five of the six model-level impossibility proofs to the original games.The checks test potential inequalities and invariant conditions from the model proofs.Source: §4.4 · p. 10

5 Related work

Prior work learns executable world models, certifies impossibility from supplied models, and formalizes given mathematics. AWM differs by learning an unfamiliar environment’s objects and rules, then checking model-based proofs against the game.

Executable world models

  • Executable world models are learned, refined, or composed for planning, while recent ARC-AGI-3 agents use simulators or rulebooks whose sampled-transition accuracy may miss key rules.AWM abstracts rules into shared structure, tests beyond the observed record, and proves reachability and impossibility.Source: §5 · p. 10

Certified impossibility

  • Prior impossibility certificates and verified certificate checkers start from a supplied model, whereas AWM learns its model through interaction and checks its rules against the game.The cited transfer approaches use broader abstraction coverage conditions; AWM’s sufficient-cover definition requires reproducing optimal winning sequences.Source: §5 · p. 10

Formal reasoning

  • Neural proving and autoformalization address given mathematics, while AWM must infer the dynamics, costs, objects, rules, and goals that its proofs quantify over.This makes the fidelity of AWM’s formal model an empirical question.Source: §5 · p. 10

6 Limitations and conclusion

AWM’s explicit learned rules support step-by-step checks and kernel-checked reachability and impossibility proofs, including claims about unexplored action sequences. The paper limits its demonstrated setting to ARC-like environments with discrete actions and immediate, observable feedback.

6 Limitations and conclusion

  • AWM’s Lean proofs are correct under the learned model’s explicit premises, while interaction tests whether those premises capture the environment.When a discrepancy arises, it can be traced to a learned rule and addressed through further exploration.Source: §6 · pp. 10–11
  • Richer hidden state, delayed feedback, and stochastic dynamics remain untested.Source: §6 · p. 10

Reproducibility Statement

  • The accompanying website provides models, tests, Lean proofs, official replays for all 25 public games, and sealed-level experiment materials.Source: Reproducibility Statement · p. 11

Statement on AI use

AI use formed part of the method and also supported text editing and analysis scripts; reported numbers came from scripts, and Lean proofs were checked independently by the Lean kernel.

Statement on AI use

  • The agents were LLMs, AI helped draft and edit the text and write analysis scripts, reported numbers came from script outputs, and the Lean kernel checked proofs independently.Source: Statement on AI use · p. 11

A Method details

The appendix details AWM’s environment and concept model, its category-guided transformations and checks, and the formal machinery for reasoning about action sequences and transferring impossibility results. It also points to per-game data and official scores.

A.1 Environment, concepts and the gate.

  • AWM models environments with states, actions, observations, deterministic transitions, an observation function, and goal states; concepts combine executable scopes, assertions, optional predictors, and evidence.The action gate refuses the next action when any concept has a FALSE or ERR verdict on a corpus transition.Source: §A.1 · p. 14
  • On lp85, the concept example matches all 20 tiles after the first certified-run click, while merging press_permutes preserves 55 rejections and adds 21 on 120 diagnostic transitions.The appendix cautions that lacking unique rejections alone does not justify deleting a rule.Source: Figure 5 · p. 14, Figure 6 · p. 15

A.3 Concepts as limits: presentations, transformations and their certificates.

  • Each transformation preserves recorded verdicts and task contracts; Lean verifies universal properties at hierarchy nodes, while task checks test whether representations agree with the environment.These are distinct forms of evidence: the kernel establishes what the model entails, and tasks establish agreement with the environment.Source: §A.3 · pp. 16–17
  • AWM represents object types and rules through limits and colimits, using four transformations: decomposition, composition, generalization, and specialization.The transformations are accepted only when task checks pass and the corresponding universal-construction statement compiles in Lean.Source: §A.3 · p. 16
  • Action sequences are modeled as words acting on states, and in lp85 Lean proves that every click sequence acts by composing the clicked buttons’ permutations.The appendix requires facts about action sequences to be checked on every level in the corpus.Source: §A.3 · p. 17
  • The Lean transition function replays recorded trajectories and reasons about unobserved sequences; budget-local transfer lemmas connect model impossibility to environment impossibility under stated preservation conditions.The potential-based certificate excludes a budgeted win when its initial value exceeds the budget after cost accounting.Source: §A.3 · pp. 17–18

B Twenty-five games; B.1 Per-game results.

  • The appendix supplies per-game data behind the main results and reports that Table 4 gives AWM’s game-level results and models, while Table 5 lists official system scores.Source: B Twenty-five games · p. 18, §B.1 · p. 18

B.2 Frozen rules on unseen transitions.

Frozen rules are tested on unseen screens, new trajectories, and modified levels to assess generalization and detection of changed mechanics. A separate proof experiment compares solving tasks under the original concepts and a merged rule.

B.2 Frozen rules on unseen transitions.

  • The unseen-screen evaluation freezes 19 lp85 concepts and 9 ft09 concepts, then tests rules reduced to 6 and 7, respectively, on random-press transitions.Source: §B.2 · p. 18
  • Frozen rules generalize to modified lp85 layouts and detect all tested transitions as inconsistent after the hidden click mechanic changes in ft09.The tests include original-level trajectories and two modified levels per game, with winnability verified by exhaustive search.Source: §B.2 · pp. 18–19
  • On unseen ls20 screens, frozen rules after Structure & Simplify accept 99.47–99.95% of valid transitions and reject 99.1–99.3% of corrupted transitions, versus 71.8–100% for concepts.The concepts charge for blocked moves only on levels where play recorded them, while the energy_cost rule charges every wall bump the level’s step cost.Source: §B.2 · p. 19

B.3 lp85: the complete model and proof size.

  • Across 102 runs, merged model B succeeds in all runs, compared with 99 for model A, and generally needs fewer auxiliary lemmas, shorter proofs, and less Lean checking time.There are no incorrect verdicts; model A has two timeouts and one run without an answer.Source: §B.2 · p. 19

B.4 Checking a model-level proof against the engine.

The section tests whether formal models support conclusions about the engine and establishes reference thresholds for sealed levels. It also evaluates generalization to unseen transitions and layouts.

B.4 Checking a model-level proof against the engine.

  • Lean checks the model-level unsolvability proof against an engine-derived graph of 7,500 configurations and 52,500 transitions, but graph extraction remains outside the kernel guarantee.The exported graph covers the seven nontrivial button actions.Source: §B.4 · pp. 19, 22
  • On unseen transitions, the frozen rules accept 0% of tested changed-mechanics cases, detecting clicks that change 110 or 146 cells instead of 38.The evaluation also tests generalization to modified layouts; its wrong-rejection range covers corruption operators readable by both rule sets.Source: Table 6 · p. 20
  • In lp85, Lean replays every recorded transition and proves both a winning witness and, after recoloring the only yellow tile, impossibility under the model.The conservation law of press_permutes rules out every click sequence in the recolored case.Source: Figure 7 · p. 21

C Sealed levels

  • Each sealed task lowers a solvable level’s budget to one unit below its minimum feasible cap B⋆; a winning witness exists at B⋆, but not at B⋆−1.Source: §C.1 · p. 22, Table 9 · p. 22

C.1 Construction and engine ground truth.

  • Exhaustive engine search establishes minimum caps of 19 and 36 for levels 4 and 5; the sealed caps are 18 and 35.The search covers all four opening facings and all 13 actions; it finds no winning route at the sealed caps.Source: §C.1 · p. 23

C.3 Proof validity and bound accuracy.

The initial runs distinguish the validity of an impossibility proof under a learned model from whether its reported bound matches the engine. Two AWM bounds were too high despite closed proofs.

C.3 Proof validity and bound accuracy.

  • All six AWM runs produced closed Lean impossibility proofs, but two initially reported overly high thresholds: 20 on level 4 and 47 on level 5.The errors arose because the learned rules excluded cheaper behavior allowed by the engine.Source: §C.3 · p. 24
  • The reference minimum costs were 19 on level 4 and 36 on level 5; bounds counted as correct when matching those values or differing only by specified free-winning-move charges.The allowed differences were 37 on level 5, or 42 actions against a budget of 41 in fbac96; this allowance applies to every agent.Source: §C.3 · p. 24
  • Table 10 reports verdicts, bounds, and whether each run produced a closed, kernel-checked impossibility theorem under its learned model.Correctness evaluates reported bounds against the engine; the accompanying text specifies timing and cost-accounting conventions.Source: Table 10 · p. 24, §C.3 · p. 24

C.4 Repairing the rules and proving again.

After feedback that cheaper wins exist, AWM revises specific rules and proves again. Post-hoc audits then test whether learned-model certificates hold on engine transitions.

C.4 Repairing the rules and proving again.

  • Given only feedback that a cheaper win exists, AWM is instructed to test disagreements, revise its rules, and prove again; each run receives at most four further attempts.The feedback reveals no rule, cost, or route.Source: §C.4 · p. 24
  • AWM’s level-4 repair models growing onto fuel, lowering its bound from 20 to 19; on level 5, it models terrain blocking a shot, lowering 47 to 37 under its run’s cost convention.Both repairs produce new closed Lean proofs; Astra corrects both bounds without formal proofs, while Opus 5.5 corrects neither.Source: §C.4 · p. 25

C.5 Transferring budget certificates to the engine.

  • Five proofs extend to the games in the post-hoc certificate audit, which checks model certificates against engine-generated transitions at the sealed caps.The audit is distinct from additional agent-produced proofs.Source: §C.4 · p. 25, Table 12 · p. 26
  • On level 5, the learned models omit blocked-turn, destroyed-target, and growth-placement transitions; completing the certificates on those transitions preserves their original lower bounds.None of the omitted transitions occurs on a cheapest winning route, and the certificate inequalities are verified again.Source: §C.5 · p. 26
  • The invariant from run 2a3cc5 V4 does not transfer because its model permits fuel collection where the game does not and misses a refund.The failure is confirmed on real engine transitions using the original Lean definitions.Source: §C.5 · p. 26
  • These are fixed-opening, post-hoc audits, not end-to-end Lean verification of engine extraction and correspondence.Their scope differs from the four-opening ground-truth search.Source: §C.5 · p. 26

C.6 Using proof dependencies to find model errors.

The section tests whether proof dependencies help locate faulty model rules and whether verification procedures detect injected errors. It also reproduces interview prompts that require agents to maintain and justify their formal systems.

C.6 Using proof dependencies to find model errors.

  • On L4, dependency information finds conflicting transitions in 29 of 42 runs, versus 16 of 42 without it; directly naming the faulty rule succeeds in 30 of 42.On L5’s 21-run sample, the counts are 3 of 21 with dependencies, 1 of 21 without, and 5 of 21 when told the faulty rule.Source: §C.6 · p. 26
  • Across both levels, providing proof dependencies finds counterexamples in 32 of 63 runs, versus 17 of 63 without them, and raises no false alarms on 12 error-free controls.The control condition without explicit dependencies raises 0.33 false alarms per run.Source: §C.6 · p. 26
  • A separate paired L5 comparison finds conflicts in 8 of 42 runs with dependencies and 5 of 42 without them.This uses a separate 42-run sample per condition and the same 5,000-action budget and discovery criterion as Table 13.Source: §C.6 · p. 27, Table 14 · p. 27

C.7 Additional tests of the verification procedure.

  • Both verification methods reject all 12 invalid certificates, while the Lean-based procedure additionally detects all three tested Python–Lean mismatches and all three reversed bounds.A separate statement audit flags six theorems that hold only because their premises are unsatisfiable or their starting-state set is empty.Source: §C.7 · p. 27, Table 15 · p. 27
  • Neither method detects injected model-rule errors or statements that refer to the wrong goal or model version, so a valid proof does not guarantee that the model describes the game.Source: §C.7 · p. 27

D Interview prompts

  • The interview prompts tell agents to amend an existing formal system, identify established assumptions, and avoid claiming a proof unless it compiles with clean axioms.They also require naming the rules used and stating any mismatch between the formal system and game.Source: D Interview prompts · p. 28

Related papers

Loading 2610.40503v1…