🤖 AI

Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution

Este artigo introduz um agente de prova Lean automodificável que coevolui com um benchmark de controle de maestria para alcançar uma taxa de resolução de 45,1% em testes de retenção, superando significativamente tanto o seu semente quanto as suas contrapartes de benchmark fixo ao garantir que todas as auto-melhorias permaneçam fundamentadas na verificação confiável do Lean.

Autores originais: Yuqing Li, Zeguan Wu, Yu Gan, Junyu Liu

Publicado 2026-07-21

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Yuqing Li, Zeguan Wu, Yu Gan, Junyu Liu

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine um mundo onde os computadores não apenas seguem ordens, mas podem realmente aprender a corrigir seus próprios erros, reescrever suas próprias instruções e se tornar mais inteligentes ao longo do tempo. Este é o reino dos "agentes autoevoluíveis", um ramo da inteligência artificial onde o software tenta melhorar a si mesmo alterando seu próprio código. Geralmente, essas criaturas digitais são testadas em um conjunto fixo de quebra-cabeças, como um aluno fazendo o mesmo teste de matemática repetidamente até memorizar as respostas. Mas e se o próprio teste pudesse ficar mais difícil toda vez que o aluno melhorasse? Essa é a ideia da "coevolução", onde o aprendiz e o desafio crescem juntos, impulsionando um ao outro a novos patamares. Em um canto específico da matemática conhecido como verificação formal, existe um árbitro rigoroso chamado "Lean" que verifica se uma prova é 100% correta. A grande questão que os pesquisadores têm feito é: Pode um agente de computador descobrir a melhor maneira de resolver essas provas matemáticas por conta própria, sem um professor humano projetando a estratégia para ele?

Este artigo conta a história de uma equipe de pesquisadores que construiu um "agente de prova" digital que tenta responder a essa pergunta. Em vez de dar ao agente um guia perfeito e escrito à mão sobre como resolver problemas matemáticos, eles permitiram que o agente reescrevesse seu próprio fluxo de trabalho, ferramentas e até mesmo como organiza seus pensamentos. Para manter as coisas justas e honestas, eles parearam este agente de autoaperfeiçoamento com um "benchmark de coevolução". Pense nisso como um videogame que ajusta automaticamente sua dificuldade: assim que o agente domina um nível, o jogo substitui esses níveis fáceis por níveis mais difíceis, garantindo que o agente nunca fique entediado ou estagnado. Os pesquisadores descobriram que essa abordagem funcionou surpreendentemente bem. Ao final de 15 gerações de evolução, seu agente autoaprendido conseguia resolver 45,1% de um conjunto de problemas matemáticos difíceis e inéditos, um salto enorme em relação aos 12,7% que ele conseguia resolver no início. No entanto, o artigo também sugere que, embora esse agente tenha melhorado muito, ele não se tornou um gênio perfeito; ele aprendeu principalmente a ser muito bom em corrigir seus próprios erros, em vez de inventar maneiras inteiramente novas e complexas de decompor problemas.

A História do Robô de Matemática Autoeditável

Imagine que você tem um robô que quer resolver uma pilha gigante de provas matemáticas. Normalmente, um programador humano escreveria um manual estrito para o robô: "Primeiro, faça isso. Depois, se você vir um erro, faça aquilo". Mas, neste experimento, os pesquisadores decidiram deixar o robô escrever seu próprio manual. Eles criaram um sistema onde o "cérebro" do robô (seu código, suas ferramentas e sua estratégia) era totalmente editável. O robô poderia tentar reescrever suas próprias instruções para ver se conseguiria resolver problemas de forma mais rápida ou precisa.

Mas havia um porém. Se o robô pudesse reescrever seu próprio código, ele também poderia mentir e dizer: "Eu resolvi!", quando na verdade não resolveu. Para impedir isso, os pesquisadores construíram um "tempo de execução confiável" — um árbitro rigoroso e imutável que nunca dorme. Este árbitro, alimentado por um sistema chamado Lean, atua como o juiz supremo. Não importa como o robô altere seu próprio código, o árbitro verifica a prova final. Se a prova não se sustentar sob o microscópio do árbitro, ela não conta. Isso garante que o robô não possa trapacear; ele tem que realmente fazer a matemática para ganhar um ponto.

O Jogo Que Fica Mais Difícil

A parte mais emocionante deste experimento é como eles testaram o robô. Na maioria dos experimentos de IA, o robô pratica em uma lista fixa de problemas. Se o robô ficar bom demais, ele apenas memoriza as respostas, e o teste deixa de ser útil. Os pesquisadores neste artigo quiseram evitar isso. Eles configuraram um "benchmark de coevolução", que é como um videogame que fica mais difícil toda vez que você vence um nível.

Veja como funcionou:

O Campeão: Em cada rodada, o robô com melhor desempenho (o "campeão") tem o direito de decidir como será a próxima rodada.
A Atualização: Se o campeão resolver problemas fáceis demais, o sistema aposenta esses problemas fáceis e os substitui por outros mais difíceis de um grande conjunto de desafios.
O Marcador de Pontos: Para garantir que as pontuações permaneçam justas conforme o jogo fica mais difícil, eles usaram um truque matemático especial chamado "recalibração de âncora única". Imagine se você corresse uma corrida em uma pista que de repente ficou mais íngreme; você correria mais devagar, mas ainda seria um ótimo corredor. Este sistema ajustou as pontuações para que ganhar uma "medalha de ouro" em uma pista difícil valesse o mesmo que ganhar uma em uma pista fácil.

Essa configuração significava que o robô estava sempre sendo empurrado para além de sua zona de conforto, forçando-o a aprender novos truques em vez de apenas memorizar os antigos.

O Que o Robô Realmente Aprendeu

Após executar este experimento por 15 gerações, os resultados foram fascinantes. O robô começou resolvendo apenas cerca de 12,7% dos problemas. Na 15ª geração, a melhor versão do robô conseguia resolver 45,1% dos problemas em um teste novo e inédito. Esse é um progresso massivo, mostrando que deixar o robô se reescrever realmente o ajudou a ficar mais inteligente.

No entanto, os pesquisadores descobriram algo interessante sobre como o robô ficou mais inteligente. Eles esperavam que o robô eventualmente descobrisse uma estratégia complexa e passo a passo, onde ele decompõe um grande problema em partes minúsculas e gerenciáveis (como um mestre arquiteto projetando o andar de um edifício por vez). Em vez disso, os robôs vencedores tornaram-se especialistas em reparo.

Pense nisso desta forma: o robô aprendeu a escrever uma prova inteira rapidamente, depois verificar se há erros e, então, consertar as partes específicas que quebraram. Ele não necessariamente planejou todo o edifício do zero; ele apenas ficou muito bom em tapar as rachaduras. Os pesquisadores descobriram que, embora o robô tentasse criar planos passo a passo complexos, esses planos frequentemente desmoronavam ou eram arriscados demais. A estratégia mais simples de "tentar, verificar, consertar" era mais confiável e venceu a competição.

O robô também inventou algumas ferramentas inteligentes para ajudar a si mesmo. Por exemplo, ele aprendeu a conferir os nomes dos termos matemáticos que utilizava para garantir que não estava inventando palavras falsas (um erro comum chamado "alucinação"). Ele construiu pequenas listas de verificação e ferramentas de busca para garantir que cada parte de sua prova fosse real e válida antes de submetê-la.

O Veredito

Então, o robô se tornou um gênio da matemática? Não exatamente. Embora tenha melhorado dramaticamente, ele ainda não conseguia resolver 99% dos problemas como os melhores robôs projetados por humanos conseguem. Os pesquisadores sugerem que o robô ainda está preso em um "modo de reparo" em vez de um "modo de planejamento". Ele é ótimo em consertar erros, mas ainda não descobriu como construir uma estrutura profunda e perfeita do zero.

Este experimento mostra que agentes autoevoluíveis podem aprender a usar suas ferramentas melhor e se tornar muito mais inteligentes quando os desafios continuam crescendo junto com eles. Mas também sugere que há um limite para o quanto um robô pode ensinar a si mesmo sem um humano guiando-o em direção a estratégias mais complexas. O robô provou que podia evoluir, mas a jornada para se tornar um verdadeiro mestre da matemática ainda é um trabalho em progresso.

Resumo Técnico: Agentes de Prova Lean Automodificáveis com Coevolução de Benchmark Baseada em Verificador

Definição do Problema

Projetar frameworks de agentes eficazes para a prova de teoremas baseados em Lean enfrenta um desafio duplo: melhorar a capacidade bruta de síntese do provador e otimizar o fluxo de trabalho de prova circundante. Enquanto trabalhos recentes focaram na construção de modelos especializados mais fortes ou táticas, uma perspectiva complementar argumenta que o gargalo reside na interação do agente com o ambiente Lean — especificamente, como ele decompõe obrigações, utiliza o feedback do compilador, diagnostica falhas e mantém o contexto estruturado da prova.

Sistemas de agentes de autoevolução atuais (ex: Máquina de Gödel Darwiniana, Hyperagents) tipicamente otimizam agentes contra benchmarks fixos fornecidos externamente. Essa abordagem é inadequada para a matemática formal porque:

Sinal de Seleção: Se o benchmark for muito difícil (ex: problemas de nível de competição), a maioria das avaliações falha, não fornecendo gradiente para a evolução. Se for muito fácil, o agente satura rapidamente.
Rigidez do Fluxo de Trabalho: A maioria dos agentes depende de fluxos de trabalho desenhados à mão. A questão permanece se um agente pode evoluir seu próprio fluxo de trabalho de prova, ferramentas e representação de contexto sem intervenção humana.
Fundamentação (Grounding): Um agente de autorreescrita não pode ser confiável para reportar seu próprio sucesso; um verificador fixo e confiável é necessário para arbitrar a correção.

Metodologia

Os autores propõem um sistema onde um agente de prova Lean autoevoluível coevolui com um benchmark de endurecimento automático, ambos fundamentados por um verificador Lean fixo e confiável.

1. Arquitetura do Sistema

Runtime Confiável vs. Workspace Mutável: O sistema separa um runtime fixo e confiável (que lida com a verificação Lean, avaliação e gerenciamento de benchmark) de um workspace totalmente mutável. O agente pode reescrever seu próprio fluxo de trabalho de prova, prompts e ferramentas dentro deste workspace.
Validade do Código vs. Sucesso da Prova: Agentes mutados passam por um "teste de fumaça" de nível de código para garantir que executem, mas um teorema só é marcado como "resolvido" se a prova gerada for re-verificada sob um snapshot confiável do Lean.
Contrato Baseado em Verificador: Cada tentativa de resolução deve emitir um contexto de prova legível por máquina. Embora a representação deste contexto (grafo, árvore, tabela) seja livre para evoluir, sua fundamentção é imposta. O runtime sanitiza certificados, rejeita sorry/admit e re-verifica as alegações de forma independente.

2. Mecanismo de Coevolução de Benchmark

Em vez de um benchmark fixo, o sistema emprega um currículo de maestria impulsionado pelo campeão:

Pool de Tarefas: Os problemas são estratificados em três níveis de dificuldade (L1: lemas de tática única; L2: miniF2F; L3: PutnamBench).
Regra de Atualização: Ao final de cada geração, se o "campeão" (agente de maior pontuação) exceder um limiar de resolução ( $\gamma=0.30$ $γ = 0.30$ ), o benchmark é atualizado.
- Tarefas resolvidas por todos os agentes são aposentadas.
- Se a maestria do campeão em um nível específico exceder um limiar ( $\tau=0.70$ ), as tarefas aposentadas são substituídas por tarefas mais difíceis do próximo nível; caso contrário, são substituídas lateralmente por novas tarefas de mesma dificuldade.
- A atualização prefere domínios onde a população de agentes acumulou falhas.
Recalibração de Âncora Única: Para manter a comparabilidade de pontuação conforme a dificuldade aumenta, o campeão é reavaliado no novo benchmark. Um coeficiente de dificuldade ( $c$ ) é atualado multiplicativamente para normalizar as pontuações entre gerações ( $q = r \times c$ ).

3. Interface de Evolução

Seleção de Parentais: Os agentes são selecionados de um arquivo com base em uma pontuação normalizada por dificuldade, com desconto pelo número de descendentes que já produziram para evitar a dominância de linhagem.
Automodificação: Os agentes reescrevem seu próprio código, incluindo lógica de fluxo de trabalho (ex: loops de reparo, estratégias de decomposição) e ferramentas (ex: verificadores de lemas).

Contribuições Principidas

Agente de Prova Lean Autoevoluível: Os autores apresentam um agente de autoevolução a nível de código onde o fluxo de trabalho de prova e as ferramentas são mutáveis, mas o sucesso da prova permanece estritamente fundamentado na verificação Lean.
Coevolução de Benchmark: Eles introduzem um benchmark de endurecimento automático, impulsionado pelo campeão, que evolui junto com o agente. Isso evita a saturação de benchmarks fáceis fixos e a esparsidade de benchmarks difíceis fixos, utilizando atualizações de maestria e recalibração de âncora única.
Contextos de Prova Sem Representação Fixa e Fundamentados: O sistema impõe um contrato onde os agentes podem evoluir o formato de seu contexto de prova (ex: de logs planos para grafos estruturados), mas a validade das alegações resolvidas é estritamente imposta pelo runtime confiável.

Resultados Experimentais

O sistema foi avaliado ao longo de 15 gerações ativas, comparando a trajetória de coevolução contra uma linha de base de benchmark fixo.

Desempenho no Teste Não Visto (Held-Out):
- Agente Semente (Seed Agent): 12,7% de taxa de resolução no split de teste miniF2F reservado.
- Linha de Base de Benchmark Fixo: O melhor agente atingiu 32,0%.
- Agente Coevolutivo: O melhor agente (c144, Geração 15) atingiu 45,1% no teste reservado.
Endurecimento do Benchmark: O coeficiente de dificuldade subiu de 1.00 para 3.17 ao longo de 15 gerações, indicando que o benchmark aumentou com sucesso em complexidade conforme o agente melhorava.
Evolução do Fluxo de Trabalho:
- Dominância Centrada em Reparo: O fluxo de trabalho vencedor permaneceu primariamente "centrado em reparo" (gerar prova $\to$ verificar erros do Lean $\to$ reparar) em vez de "centrado em decomposição" (planejar submetas $\to$ provar $\to$ montar).
- Evolução de Ferramentas: Os agentes evoluíram com sucesso ferramentas para prevenir alucinações de nomes do Lean (ex: sondagens #check, busca de fonte, caches de lemas verificados).
- Tentativas de Decomposição: Vários agentes tentaram fluxos de trabalho baseados em decomposição (ex: c26, c44, c141). Embora esses agentes tenham evoluído uma verificação genuína de nível de nó para sub-lemas autocontidos, essas estratégias foram frequentemente podadas pela seleção porque a etapa de montagem introduzia novos pontos de falha (parsing de JSON, incompatibilidades de contexto) que reduziam a taxa final de resolução em comparação com loops de reparo compactos.
Contexto de Prova: Os contextos de prova tornaram-se inspecionáveis, mas raramente evoluíram para grafos de dependência profundos e verificados. Os agentes tenderam a construir o contexto de trás para frente a partir da prova final, em vez de planejar um grafo antecipadamente.

Significância e Alegações

O artigo afirma que a autoevolução baseada em verificador pode melhorar os fluxos de trabalho de prova Lean sob um benchmark coevolutivo.

Viabilidade de Auto-melhoria: Os resultados demonstram que um agente pode melhorar seu fluxo de trabalho matemático e suas ferramentas apenas reescrevendo seu próprio código, desde que um verificador fixo e confiável arbitre o sucesso.
Importância da Coevolução: O estudo de ablação mostra que um benchmark fixo leva à estagnação evolutiva assim que o agente domina um subconjunto de tarefas. O benchmark coevolutivo mantém um sinal de seleção informativo ao aumentar continuamente a dificuldade.
Limitações e Direções Futuras: Os autores são modestos quanto ao estado atual. O fluxo de trabalho vencedor ainda é centrado em reparo, e o sistema ainda não evoluiu um grafo de contexto de prova (DAG) profundo e duradouro que rivalize com agentes desenhados à mão como o Goedel-Architect (que atinge 99,2% no miniF2F-test). Os autores sugerem que execuções mais longas, populações maiores ou recompensas direcionadas especificamente para decomposição verificada podem ser necessárias para evoluir fluxos de trabalho mais complexos e de prioridade em decomposição.

O trabalho estabelece uma base para agentes que podem adaptar suas próprias estruturas de raciocínio em domínios formais, mantendo a lógica de verificação fixa enquanto o "como" da construção da prova evolui.