Algebraic world model builds executable math proofs from unknown games
Algebraic World Model: From Exploration to Proofs
Artificial IntelligenceLogic in Computer Science
Summary
Solving mathematical problems with AI usually needs clear rules and definitions, but what if the rules are unknown? The authors created the Algebraic World Model (AWM), which explores new environments to figure out how they work by making and testing guesses. It turns these guesses into a precise math model that can prove whether certain goals are achievable or not, even beyond what has been tried. This lets AWM solve and prove outcomes for complex game levels where other advanced AI systems fail, producing clear, inspectable mathematical rules. The model can also replay known solutions and predict unseen changes in game mechanics.
What this means in practice
- •For game developers: Automatically verify which game levels can or cannot be solved to improve game design quality and balance.
- •For software verification teams: Construct executable formal models of unknown software behaviors and prove reachability or impossibility properties to detect bugs or security issues.
Authors
Guancheng Pan, Qixin Tan, Yang Yuan, Andrew Chi-Chih Yao
Abstract
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.