AI turned game exploration into models with checked proofs
On two impossible game levels, the framework produced checked proofs in all six runs; two models with coding tools produced none in twelve comparison runs.
Edited by Boris Djordjevic · Paperfoot
The Algebraic World Model (AWM) framework turned interaction with unfamiliar games into mathematical models supporting proofs of reachable and unreachable goals. It tested and revised Python programs against observations, then formalized its models in Lean 4, software that checks mathematical proofs.
On two impossible game levels, AWM produced checked proofs excluding every legal winning sequence in all six runs. Claude Opus 5.5 and GPT-6 Astra, both equipped with coding tools, produced none across twelve baseline runs. Across ARC-AGI-3, a collection of 25 public games, AWM’s models let Lean replay winning sequences for all 183 levels. The models also predicted unseen transitions and detected changes in game mechanics.
Why it matters
The game tests demonstrated a path from observations to inspectable mathematical rules and machine-checked proofs, including conclusions about impossibility beyond explored play.
Caveats
The proofs concerned learned mathematical models, whose rules AWM tested against game observations. The work is a preprint and has not been peer-reviewed.
From the paper
- Limitation
We demonstrate AWM on ARC-like environments with discrete actions and immediate, observable feedback, where learned rules can be checked against recorded transitions; richer hidden state, delayed feedback and stochastic dynamics remain to be tested.
Quoted word for word from the full text on arXiv.
In this paper
reasoning rigorously about an unknown world
- Methods
- Algebraic World Model (AWM) (this paper)Claude Opus 5.5 (baseline)GPT-6 Astra (baseline)Memento 3 (baseline)Claude Opus 5Lean 4
- Datasets
- ARC-AGI-3 (evaluated)sc25 (evaluated)lp85 (evaluated)ft09 (evaluated)ls20 (evaluated)
- Links
- Project page
Results
- Algebraic World Model (AWM), actions, certified clears: 7,448
Its certified clears require 7,448 actions, only 43% of the human baseline’s 17,135 and the fewest among systems reporting this metric, compared with 7,518 for Memento 3 and 8,347 for.
Clearing the games with efficient solutions.
- Algebraic World Model (AWM), score, on ARC-AGI-3, With Claude Opus 5: 99.9
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.
Abstract
- Algebraic World Model (AWM), engine actions, total: 24,604
Including exploration and other sessions, AWM uses 24,604 engine actions in total (Appendix B).
Clearing the games with efficient solutions.
- Algebraic World Model (AWM), closed, kernel-checked Lean proofs excluding every legal winning sequence, two impossible game levels: all six runs
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.
Abstract
- Algebraic World Model (AWM), correct bounds, initial bounds: four of AWM's six; Algebraic World Model (AWM), correct bounds, given only feedback that a cheaper win exists: six of six
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.
Abstract
- Algebraic World Model (AWM), next tile layout predictions, on lp85, two modified lp85 layout sets: all 4,160 cases
On the two modified lp85 layout sets, they predict the next tile layout in all 4,160 cases; on the two changed-mechanic ft09 sets, they reject all 4,031 transitions.
Generalization beyond observed transitions.
What it shows
- On two impossible game levels, AWM constructs closed, kernel-checked Lean proofs excluding every legal winning sequence across all six runs, while baseline models produce none across twelve runs.
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.
Abstract
- Proof dependencies substantially improve error discovery when locating faulty rules, nearly matching the benefit of directly identifying the faulty rule.
Thus, proof dependencies substantially improve error discovery, nearly matching the benefit of identifying the faulty rule directly (Appendix C).
Proof dependencies help locate faulty rules.
- AWM is demonstrated on ARC-like environments with discrete actions and immediate, observable feedback, leaving richer hidden state, delayed feedback, and stochastic dynamics to be tested.
We demonstrate AWM on ARC-like environments with discrete actions and immediate, observable feedback, where learned rules can be checked against recorded transitions; richer hidden state, delayed feedback and stochastic dynamics remain to be tested.
Limitations.
Quoted word for word from the full text on arXiv.
The paper
Algebraic World Model: From Exploration to Proofs
arXiv, Oct 29, 2026, Open access, Preprint, not peer-reviewed
doi.org/10.48550/arxiv.2610.40503
arXiv:2610.40503v1 in cs.AI, also cs.LO
Comments: 29 pages, 9 figures, 14 tables. Project page: https://ephemeral6.github.io/awm-site/. Ancillary files contain the Lean 4 model of the running example lp85
Cite as BibTeX
@misc{pan2026algebraic,
title = {Algebraic World Model: From Exploration to Proofs},
author = {Pan, Guancheng and Tan, Qixin and Yuan, Yang and Yao, Andrew Chi-Chih},
year = {2026},
eprint = {2610.40503},
archivePrefix = {arXiv},
primaryClass = {cs.AI},
doi = {10.48550/arxiv.2610.40503},
url = {https://arxiv.org/abs/2610.40503}
}