Pesquisadores criam agente que prova níveis impossíveis no ARC-AGI-3

Pesquisadores da Universidade de Tsinghua e da Universidade de Zhejiang apresentaram o Algebraic World Model (AWM), um agente capaz de jogar e demonstrar formalmente quando uma etapa não tem solução nos desafios interativos do ARC-AGI-3. O artigo científico foi publicado no repositório arXiv em 29 de outubro de 2026, com cobertura divulgada pelo site QbitAI em 1º de novembro e detalhada em reportagem do Pandaily publicada em 2 de novembro de 2026.

Como funciona o modelo

O estudo foi desenvolvido pelos pesquisadores Guancheng Pan, da Universidade de Zhejiang, e por Qixin Tan, Yang Yuan e Andrew Chi-Chih Yao, da Universidade de Tsinghua. A atuação do AWM ocorre em três etapas encadeadas:

• Exploração e hipóteses: o agente explora o jogo e escreve hipóteses em linguagem Python sobre o comportamento do ambiente, revisando-as sempre que as observações discordam das premissas.
• Estruturação teórica: o sistema simplifica essas hipóteses em um modelo estruturado de objetos, regras e metas, orientado por conceitos da teoria das categorias.
• Formalização e verificação: o modelo é formalizado no assistente de provas Lean 4, onde declarações como a possibilidade de vencer um nível podem ser checadas por máquina.

Desempenho em testes com restrição de passos

Os pesquisadores testaram o sistema em seis níveis selados com orçamentos de passos que tornam a vitória impossível. O AWM produziu demonstrações formais de impossibilidade no Lean 4 para todos os seis níveis. Em contrapartida, 12 execuções dos modelos Claude Opus 5.5 e GPT-6 Astra não geraram nenhuma prova.

Em um exemplo relatado, a solução mais barata para vencer exigia 19 passos contra um orçamento limite de 18; o Astra alegou uma solução de 22 passos. O AWM apresentou limites iniciais corretos em quatro das seis etapas, contra uma do Opus 5.5 e nenhuma do Astra. Após receber sinalizações de feedback, o AWM atingiu os limites corretos em todas as seis etapas.

Resultados nos jogos públicos e integração com jogadores

Nos 25 jogos públicos do ARC-AGI-3, todos os 183 níveis foram reproduzidos dentro do assistente Lean 4. Os modelos aprendidos previram todas as 4.160 transições em cenários inéditos e rejeitaram todas as 4.031 transições após uma alteração nas mecânicas do jogo.

Quando associado ao Claude Opus 5 atuando como jogador, a utilização do AWM elevou a pontuação de 40,7 para 99,9. A combinação consumiu 43% da quantidade de ações registradas na linha de base da referência humana.

Limitações indicadas pelos autores

Os autores ressaltam que as demonstrações dependem diretamente da precisão do modelo aprendido pelo agente. Dessa forma, um resultado de impossibilidade obtido pelo sistema é válido dentro do modelo do jogo formulado pelo AWM, e não necessariamente em relação ao código real do jogo.