Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

O artigo descreve o experimento "Agent Hunt", que utiliza um mercado simulado baseado em recompensas para coordenar múltiplos agentes de LLM em uma busca colaborativa e descentralizada por provas e definições formais de topologia algébrica dentro de um ambiente de Prova Teórica Interativa.

O essencial

Imagine que você precisa construir uma catedral gigante de matemática, chamada "Topologia Algébrica". Essa catedral é tão complexa que nem os melhores arquitetos humanos conseguem desenhá-la sozinhos em tempo hábil.

O artigo que você leu descreve um experimento ousado: em vez de contratar um único mestre construtor, os pesquisadores criaram um mercado de trabalho virtual onde quatro "robôs inteligentes" (chamados Agentes LLM) competem e cooperam para construir essa catedral, tijolo por tijolo.

Aqui está a explicação simples, usando analogias do dia a dia:

1. O Problema: A Montanha de Trabalho

Antes, tentaram usar apenas um robô para escrever todo o código matemático. O problema? Era lento. Era como tentar pintar um mural gigante sozinho; você cansa, demora e pode errar detalhes. O projeto de topologia geral já estava em andamento há meses e ainda não tinha acabado.

2. A Solução: O "Mercado de Recompensas" (Bounty Market)

Os pesquisadores criaram um sistema inspirado em jogos de vídeo ou em caça ao tesouro:

• O Tesouro: Cada teorema (uma afirmação matemática) que precisa ser provado recebe uma recompensa (chamada de "bounty"), como se fosse um prêmio em dinheiro fictício.
• Os Agentes: Quatro robôs (Alice, Bob, Charlie e Dave) são os "caçadores".
• A Dinâmica:
  • Eles podem apostarem em um teorema: "Eu vou provar isso!" e bloqueiam a tarefa por um tempo.
  • Eles podem competir: Se dois robôs tentam provar a mesma coisa, quem fizer primeiro ganha o prêmio.
  • Eles podem colaborar: Às vezes, um robô prova uma parte difícil e deixa o resto para outro, ou eles dividem o trabalho para ganhar bônus por terminar rápido.

É como se fosse um Uber de matemática: em vez de um único motorista levar você até o destino, vários motoristas disputam a corrida, mas se precisam de ajuda para subir uma ladeira, eles podem se unir para empurrar o carro juntos.

3. Como Eles Trabalham Juntos?

Os robôs não apenas escrevem código; eles interagem com um "juiz" (o sistema de prova matemática) que verifica se o trabalho está correto.

• O Juiz (Megalodon): É um árbitro rigoroso. Se o robô tentar trapacear ou escrever algo errado, o juiz não aceita e o robô não ganha o prêmio.
• A Estratégia: Os robôs são espertos. Eles decidem: "Vou provar esse teorema difícil sozinho para ganhar tudo" ou "Vou provar essa parte fácil e deixar o teorema grande para o colega, porque assim ganhamos ambos".
• O Resultado: Em apenas dois dias, eles produziram o equivalente a 39.000 linhas de código matemático. Para comparação, o projeto antigo (com um único robô) fazia cerca de 7.000 linhas por dia. Foi uma aceleração massiva!

4. Os Obstáculos e Lições

Nem tudo foi perfeito, e o experimento mostrou algumas coisas engraçadas e importantes:

• O Erro dos Exercícios: No livro de matemática original, havia exercícios sem respostas. Os robôs tentaram provar esses exercícios, gastaram horas (e "dinheiro" virtual) e ganharam prêmios ridículos (como 10 moedas por 800 linhas de código). Eles aprenderam a ignorar essas "armadilhas".
• A Definição de Seno e Cosseno: Houve um momento em que os robôs travaram porque a definição matemática de seno e cosseno usada no sistema era falha (permitia múltiplas respostas erradas). Foi como tentar construir uma casa em um terreno que afunda. Eles precisaram parar e corrigir os alicerces antes de continuar.
• Divisão de Trabalho: Cada robô desenvolveu uma "personalidade". O Bob ficou bom em "grupos fundamentais" (uma parte abstrata), o Charlie em geometria, a Alice em conexões básicas. Eles acabaram se especializando naturalmente, como uma equipe de futebol onde cada um joga na sua posição favorita.

5. Conclusão: O Que Isso Significa?

Este experimento mostrou que, para tarefas gigantes e complexas, não precisamos de um super-herói solitário. Em vez disso, podemos criar um sistema de mercado onde muitos agentes inteligentes competem e colaboram.

É como transformar a construção de uma catedral de um trabalho solitário e lento em um festival de construção comunitária, onde todos têm incentivos para trabalhar rápido, ajudar uns aos outros e garantir que cada pedra esteja no lugar certo.

Resumo em uma frase:
Os pesquisadores criaram um "mercado de recompensas" onde quatro IAs competem e cooperam para provar teoremas matemáticos difíceis, conseguindo trabalhar muito mais rápido e de forma mais eficiente do que um único robô sozinho.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents", apresentado em português.

1. O Problema

A autoformalização de grandes volumes de textos matemáticos (como livros didáticos) usando Agentes de Linguagem (LLMs) tem demonstrado resultados promissores, mas enfrenta desafios de escala e eficiência quando realizada por um único agente. O projeto "General Topology" mencionado no artigo, por exemplo, levou mais de dois meses para processar 350 mil linhas, indicando que a abordagem sequencial de um único agente é lenta e difícil de escalar para projetos massivos.

O principal desafio identificado é a coordenação descentralizada: como distribuir o trabalho de prova e formalização entre múltiplos agentes de forma eficiente, sem a necessidade de um planejamento centralizado rígido e manual, que muitas vezes falha diante de imprevistos (como lacunas nas provas ou referências futuras) em grandes formalizações.

2. Metodologia

Os autores propõem um ambiente de mercado baseado em recompensas (bounties) para orquestrar múltiplos agentes LLM em um sistema de Prova de Teorema Interativo (ITP).

• Ambiente e Ferramentas:

  • Domínio: Topologia Algébrica (Partes II, Capítulos 9-14 do livro Munkres).
  • Prova Assistida: Uso do verificador de teoria de conjuntos de ordem superior Megalodon.
  • Agentes: Quatro agentes LLM distintos (nomes: Alice, Bob, Charlie e Dave), utilizando modelos como ChatGPT Pro Codex e Claude (Opus e Sonnet).

• Mecanismo de Mercado (Bounty System):

  • Definição Inicial: Um agente inicial (Claude Opus 4.6) formalizou as definições e teoremas sem provas (usando Admitted), mas com estimativas de esforço e recompensas (bounties) em tokens simulados (USD).
  • Competição e Colaboração: Os agentes competem para provar teoremas e coletar as recompensas. No entanto, o sistema incentiva a colaboração para finalizar o projeto mais rápido.
  • Mecânica de Bloqueio (Locking): Um agente pode "travar" um teorema pagando 10% da recompensa, garantindo o direito de coletar o valor total se concluir a prova. Isso evita que múltiplos agentes trabalhem no mesmo teorema simultaneamente de forma redundante.
  • Sub-bounties: Agentes podem criar novas recompensas para lemas intermediários necessários para provar um teorema maior.

• Regras e Segurança:

  • Disciplina de Commit: Os agentes não podem modificar definições ou estados de prova de outros agentes.
  • Scripts de Guarda (Guard Scripts): Scripts locais validam invariantes do sistema (saldos não negativos, expiração de travas, imutabilidade de definições) antes de cada commit, prevenindo violações de regras e "gaming" do sistema.
  • Adaptação do Verificador: O Megalodon foi modificado para lidar melhor com arquivos longos gerados por LLMs, incluindo mensagens de erro mais claras e restrições no comando Qed (provas só podem ser fechadas se todas as dependências forem verificadas).

3. Principais Contribuições

1. Arquitetura Descentralizada de Prova: Demonstração de que um sistema de mercado baseado em recompensas pode coordenar efetivamente múltiplos agentes LLM para tarefas complexas de raciocínio matemático, superando a necessidade de um planejador central.
2. Escalabilidade em Autoformalização: O método permite paralelização massiva, onde agentes podem trabalhar em diferentes partes da teoria simultaneamente, resolvendo dependências conforme necessário.
3. Mecanismos de Incentivo e Segurança: A introdução de travas (locks) e scripts de validação local para garantir a integridade do repositório de provas e a distribuição justa de recompensas.
4. Integração com ITP: O trabalho conecta diretamente os agentes ao sistema de prova interativo, permitindo que eles inspecionem estados de prova, analisem falhas de táticas e refinem scripts iterativamente.

4. Resultados

• Velocidade de Produção: Em um período de aproximadamente 2 dias e 15 horas, quatro agentes produziram coletivamente cerca de 39.000 linhas de código formalizado (normalizado). Isso representa uma média de ~7.000 linhas/dia por agente, comparado a ~7.000 linhas/dia totais do projeto anterior de um único agente (que levou 60 dias para 406k linhas).
• Crescimento Linear: O tamanho da formalização cresceu de forma quase linear, com apenas pequenas quedas locais devido a refatorações.
• Dinâmica de Colaboração:
  • Dos 709 tokens de recompensas colocados em novos lemas, 279 foram provados pelo criador, 114 por outro agente (colaboração cruzada) e 312 permaneceram ativos.
  • Houve divisão de trabalho temática clara: Bob focou em homotopia e grupos fundamentais; Charlie em topologia geométrica; Alice em leis de grupo e concatenação de caminhos; e Dave em suporte de teoria de grupos abstratos.
• Teoremas Maiores: Foram provados teoremas significativos, incluindo o Teorema do Ponto Fixo de Brouwer (com uma prova de 1.564 linhas, dependendo de um teorema não provado sobre o grupo fundamental do círculo) e teoremas sobre grupos cíclicos e produtos de espaços.
• Custo: O custo estimado do experimento foi de cerca de **US$150**, o que equivale a pouco mais de US$ 1 por 1.000 linhas normalizadas.

5. Significado e Observações Finais

O estudo "Agent Hunt" valida a hipótese de que mecanismos de mercado inspirados em economia podem ser uma solução viável para escalar a autoformalização matemática. Ao substituir o planejamento centralizado por incentivos descentralizados, o sistema consegue lidar com a imprevisibilidade de grandes formalizações (como lacunas ou referências futuras) de forma mais flexível.

Desafios Identificados:

• Qualidade das Definições Iniciais: Definições incorretas (como a definição de seno e cosseno usada no experimento, que não era única) podem levar os agentes a tentar provar propriedades impossíveis, desperdiçando recursos.
• Estimativa de Esforço: Exercícios de livros didáticos, que muitas vezes não têm soluções nos livros, levaram a estimativas de custo enganosas e recompensas desproporcionais.
• Dependências Críticas: A prova do Teorema de Brouwer ficou pendente devido à falta de uma definição correta e provada do grupo fundamental do círculo, destacando a necessidade de definições fundamentais robustas antes da prova de teoremas complexos.

Em suma, o trabalho abre caminho para uma nova era de pesquisa de prova colaborativa e descentralizada, onde múltiplos agentes de IA podem construir teorias matemáticas complexas de forma eficiente, segura e economicamente viável.