Yao's team proposes the Algebraic World Model AWM, using Lean 4 to prove that a game has no solution

The previous question could be answered by finding any single winning route, but to prove that no solution exists, one must rule out all legal routes, including those not yet tried. If a game does not even disclose its rules, the AI first needs to figure out what exactly it is proving. Clearing the game and proving it unsolvable are completely different in difficulty.

To this end, the team of Turing Award laureate, Academician of the Chinese Academy of Sciences, and Dean of the Institute for Interdisciplinary Information Sciences at Tsinghua University Andrew Yao proposed the "Algebraic World Model" (AWM), a framework that transforms interaction with an unfamiliar environment into an explicit mathematical model that supports formal reasoning.

AWM first explores the environment through interaction, proposes and revises rule hypotheses, then organizes these rules into a mathematical model, and finally writes them into Lean 4 to construct formal proofs that can be checked by the kernel. With this approach, AI can not only answer how to win, but also prove why winning is impossible under given constraints.

The core of this work is to connect empirical observations with the premises on which proofs depend. Traditional formal reasoning usually starts from pre-given mathematical definitions and rules. AWM, by contrast, needs to actively discover these structures from an unfamiliar environment and continuously test and revise the learned rules in subsequent interactions.

The whole process is divided into three stages.

In the first stage, the agent actively explores the environment, writes its guesses about the mechanisms as executable Python hypotheses, and then tests these hypotheses using the observed state changes. When predictions and feedback are inconsistent, the system does not directly treat existing experience as definite rules, but instead chooses to continue revising the model.

Figure | The three-stage pipeline of AWM

In the second stage, AWM organizes the hypotheses into typed objects and rules, and transforms the structures under the guidance of category theory to identify commonalities and simplify representations. Specifically, the system reorganizes object types and rules through four transformations: decomposition, composition, generalization, and specialization. These transformations all need to be checked in Lean to ensure that the model preserves the already-verified behavioral characteristics during simplification.

Figure | Four types of transformations guided by projective limits and inductive limits, acting on object types and rules

In the third stage, the system completes formal modeling in Lean 4 and constructs corresponding proofs. For levels that can be cleared, a legal sequence of winning actions is enough to prove that the goal is reachable. For levels that cannot be cleared within the budget, the system can seek invariants that always hold during the action process, or prove a lower bound on the cost required by any winning sequence, thereby ruling out all legal winning routes within the budget.

Figure | AWM induces shared color permutation rules from four types of button mechanisms

The team tested this unreachability reasoning capability on ARC-AGI-3. These games do not disclose their rules and goals in advance. Based on two levels of sc25, they retained the mechanisms and set the action budget slightly below the minimum winning cost, constructing two variants that cannot be cleared within the budget.

Each level was run three times, and AWM constructed closed proofs that passed the Lean kernel check in all six runs, ruling out all legal winning sequences within the budget under the learned model. The team reported that Claude Opus 5.5 and GPT-6 Astra, equipped with programming tools, did not produce such proofs in a total of twelve baseline runs.

However, a proof passing the check does not mean that the system has learned completely correct environment rules. Among the winning-cost lower bounds given by AWM in its first six runs, four matched the true minimum cost. Opus 5.5 gave a correct bound once but without a proof, while Astra did not give a correct bound. The remaining baseline runs had incorrect bounds or failed to reach a conclusion.

One example occurred at level 4. GPT-6 Astra claimed that the minimum winning cost was 22 but provided no proof. AWM, under the learned model, proved a tight lower bound of 19 and verified a winning route with cost 19, consistent with the game's actual minimum winning cost.

Figure | The two agents disagree on the minimum cost required to clear the game

For the other two inaccurate bounds from AWM, they only fed back that a lower-cost winning plan existed, and the system then revised the rules and reconstructed the proofs, ultimately making all six runs' bounds correct.

This also highlights two types of errors that must be distinguished: reasoning may strictly follow the rules, but the rules themselves may still fail to match the environment. Formal proofs cannot replace the testing of modeling premises.

They also examined whether the model could accurately express the observed game processes. Among the models AWM built for all 25 public games, the median number of object types was 6, and the median number of rules was 10. These models support replaying the winning trajectories of all 183 levels in Lean, checking the state transitions and final goal conditions represented by the model.

In addition, the team tested the model's ability to predict unobserved behavior. In some games, AWM froze the rules learned during the exploration stage and then applied them to random game trajectories and modified game mechanisms. Experiments showed that the model could predict unseen layout changes and could also identify mechanism changes inconsistent with the original rules, indicating that the learned rules have a certain generalization ability.

In terms of clearing performance, AWM using Claude Opus 5 achieved a score of 99.9 across all levels, approaching the performance of leading code-execution-based systems. Its certified winning trajectories used a total of 7,448 actions, only 43% of the human baseline of 17,135 actions.

It should be noted that these groups of experiments respectively examined the model's reproduction of observed behavior, generalization to unseen behavior, and game-clearing efficiency. They can demonstrate AWM's performance in environment modeling and task execution, but still need to be distinguished from unreachability proofs about real environments.

Figure | Official scores on 25 public ARC-AGI-3 games

They also pointed out the limitations of this research: currently, AWM has mainly been validated in ARC-type environments with discrete actions and immediately observable feedback. For environments containing more complex hidden states, delayed feedback, and stochastic dynamics, its applicability still needs further testing.

In addition, Lean can guarantee that proofs proceed correctly from the premises explicitly given by the model according to formal rules, but whether these premises accurately describe the real environment still needs to be confirmed through interaction. The research team believes that AWM explicitly presents model rules and proof dependencies, which helps locate problems and correct errors through further exploration. In the future, this formal reasoning capability still needs to be tested in more types of environments and tasks.

Overall, AWM attempts to enable AI, in environments with unknown rules, to first discover objects and patterns through interaction, then organize them into explicit algebraic models, and use Lean to prove whether goals can be achieved.

The significance of this approach lies in enabling AI's reasoning to cover action sequences that have not yet been explored, while making the assumptions on which conclusions depend clear and checkable. When the model deviates from the real environment, the system can also trace the specific rules on which the proof depends and correct the model through further exploration.

From empirical exploration to mathematical modeling and then to formal proof, AWM provides a new technical path for AI to carry out rigorous reasoning in unknown environments.

For more technical details, see the original paper.

This article is from the WeChat public account "Academic Headlines" (ID: SciTouTiao), author: Zhang Jiayi, published by 36Kr with authorization.