Исследователи из Университета Цинхуа и Чжэцзянского университета представили Модель алгебраического мира (AWM) — агента, который способен не только проходить интерактивные головоломки ARC-AGI-3, но и формально доказывать, когда пройти определенный уровень невозможно.
Работа, опубликованная на arXiv 29 октября и освещенная QbitAI 1 ноября, была выполнена Гуанчэном Панем из Чжэцзянского университета, а также Цисинь Таном, Яном Юанем и Эндрю Чи-Чи Яо из Университета Цинхуа.
AWM функционирует в три этапа. Сначала он исследует игру и формирует гипотезы на Python относительно поведения среды, корректируя их при получении противоречивых наблюдений. Затем эти гипотезы упрощаются до структурированной модели, описывающей правила, цели и объекты, опираясь на концепции теории категорий. Завершающим шагом является формализация этой модели в помощнике доказательств Lean 4, где машина может проверять утверждения, например, о возможности прохождения уровня.
Команда провела тестирование на закрытых уровнях, где бюджет шагов делал победу невозможной. AWM смог предоставить доказательства невозможности с помощью Lean для всех шести таких уровней, тогда как 12 запусков Claude Opus 5.5 и GPT-6 Astra не смогли этого сделать. В одном примере, где минимальная победа требовала 19 шагов при бюджете в 18, Astra заявила о решении в 22 шага, в то время как AWM установил корректные начальные границы для четырех из шести уровней, против одного для Opus 5.5 и нуля для Astra, достигнув результата для всех шести после обратной связи.
В ходе повторного проигрывания всех 183 уровней из 25 публичных игр внутри Lean, изученные модели смогли предсказать все 4160 переходов на невиданных раскладках и отклонили все 4031 переход после изменения игровой механики. При использовании Claude Opus 5 в качестве игрока, AWM поднял свой балл с 40.7 до 99.9, используя при этом всего 43% действий, принятых в базовом человеческом варианте.
Авторы отмечают существенное ограничение: достоверность доказательств зависит от качества самой изученной модели, следовательно, результат о невозможности верен в рамках модели игры AWM, а не в отношении фактического кода игры.



