Исследователи Чжэцзянского университета, Цинхуа и Shanghai QiZhi Institute представили Algebraic World Model (AWM): ИИ-агент изучает незнакомую среду и строит доказательства того, что цель недостижима при выученных правилах. Препринт вышел 29 октября и обновлён 30 октября.

Обычно формальная проверка начинается с уже заданных правил. Здесь агент сначала проверяет гипотезы действиями в игре, записывает модель на Python, затем переводит её в систему доказательств Lean 4. Это позволяет рассуждать и о последовательностях ходов, которые агент не пробовал.

По данным авторов, в опыте с двумя уровнями, где бюджета действий не хватало для победы, AWM на Claude Opus 5.5 получила проверенные Lean доказательства во всех шести запусках. Claude Opus 5.5 и GPT-6 Astra с обычными инструментами программирования не получили таких доказательств в двенадцати контрольных запусках.

Но логически верное доказательство может опираться на неверно выученные правила. Первоначально минимальный бюджет победы AWM определила правильно в четырёх случаях из шести; после сообщения, что существует более дешёвое решение, исправила остальные два. Дополнительная проверка позволила перенести пять из шести доказательств на настоящий игровой движок.

Авторы выложили материалы для проверки. Пока это исследовательская система для дискретных сред с немедленной обратной связью: работу со скрытым состоянием, задержками и случайностью ещё предстоит проверить.