ProofCouncil: An LLM Agent for Solving Open Mathematical Problems
Este artigo apresenta o ProofCouncil, um agente de LLM de código aberto que utiliza uma arquitetura autor-crítico e alcançou o estado da arte no desafio FirstProof ao resolver autonomamente seis de dez problemas matemáticos do mundo real e demonstrar progresso significativo em um conjunto mais amplo de problemas abertos.
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 que você entregou a um robô novinho em folha, superinteligente, uma pilha dos enigmas matemáticos mais intrigantes do mundo. Estes não são os enigmas padrão de "encontre o número que falta"; são problemas abertos sobre os quais matemáticos humanos estão coçando a cabeça há anos, sem que ninguém saiba a resposta até agora.
Entra em cena o ProofCouncil. Pense nele não como um único robô, mas como um pequeno workshop de matemática de alto nível.
A Equipe do Workshop: Autor, Crítico e o Esquadrão
O coração deste sistema é um jogo inteligente de "batata quente" jogado entre dois personagens principais: o Autor e o Crítico.
- O Autor é o sonhador. É uma IA que se senta para tentar escrever uma prova perfeita (um argumento matemático passo a passo) para um problema. Ele tem um caderno mágico onde rabisca ideias, testa códigos e até pesquisa na web em busca de pistas.
- O Crítico é o editor rigoroso. Ele lê o que o Autor escreveu e diz: "Espere, este passo não faz sentido" ou "Você esqueceu de provar esta parte!". Ele não apenas diz que está errado; ele fornece feedback específico sobre como corrigir as lacunas.
A reviravolta é que o Autor não escreve apenas uma vez. Ele escreve, recebe críticas, reescreve, recebe críticas novamente e continua o processo. É como um escritor e um editor trancados em uma sala, polindo uma história até que ela esteja perfeita.
Mas, às vezes, o Autor fica travado. É aí que ele convoca o Conselho e o Nó de Computação.
- O Conselho é um painel de outras IAs superinteligentes (como uma equipe de especialistas convidados). O Autor pergunta a eles: "Ei, estou travado nesta parte específica; existe uma maneira diferente de olhar para isso?".
- O Nó de Computação é o braço forte. Se o problema exigir um cálculo massivo ou uma ferramenta de software matemático especializada que o Autor não consegue rodar sozinho, este nó realiza o trabalho pesado, executando códigos e processando números para verificar se um palpite é verdadeiro.
A cada poucos ciclos, o Crítico faz uma "pausa mental" e começa do zero com uma folha limpa. Isso é crucial porque, se o Crítico se acostumar demais com os erros do Autor, ele pode parar de percebê-los. Um par de olhos frescos garante que a prova seja realmente sólida.
O Grande Teste: O Desafio FirstProof
A equipe colocou o ProofCouncil à prova definitiva: um desafio chamado FirstProof. As regras eram simples, mas brutais: resolver 10 problemas matemáticos reais e não resolvidos em 24 horas, usando apenas ferramentas públicas.
Os resultados? O ProofCouncil foi a estrela do show. Dos 10 problemas, ele conseguiu produzir soluções para 6 deles que os juízes humanos julgaram corretas (necessitando apenas de pequenos ajustes menores). Este foi o melhor desempenho de qualquer equipe na competição.
Eles também testaram em 30 outros problemas abertos enviados por matemáticos reais. Dos 21 problemas sobre os quais receberam feedback:
- 5 foram julgados como soluções completamente corretas.
- 2 foram vistos como muito promissores, apenas aguardando uma verificação final.
- 8 fizeram progressos úteis, mesmo que não tenham concluído o trabalho.
- 4 não apresentaram erros, mas não mudaram muito o cenário.
- 2 entenderam mal a questão e resolveram uma versão mais fácil dela.
Importante ressaltar que nenhum especialista disse que os outputs estavam matematicamente errados de uma forma que quebrasse a lógica. A principal falha não foi matemática ruim; foi, às vezes, interpretar mal o enunciado do problema.
O Custo do Gênio
Aqui está o detalhe: ser tão inteligente é caro. Rodar o ProofCouncil em um único problema custou cerca de US$ 350 em tempo de computação e chamadas de modelos. Compare isso com uma tentativa de IA de disparo único, mais simples, que custou apenas US$ 12, mas resolveu menos problemas. O artigo sugere que, embora a "abordagem de equipe" funcione melhor, ela é atualmente um item de luxo. Os autores admitem que ainda não tentaram torná-lo mais barato, deixando isso como um trabalho para pesquisadores futuros.
O Que Ele Não Fez (E O Que Não Alegou)
É importante saber o que este robô não fez.
- Ele não resolveu todos os 10 problemas do desafio (ele perdeu 4).
- Ele não produziu um artigo de pesquisa polido e pronto para publicação. Os matemáticos que revisaram o trabalho observaram que a escrita era densa e precisava de edição humana para ser legível por não especialistas.
- Ele não "provou" que a IA pode resolver qualquer problema matemático. Ele mostrou que, para alguns problemas difíceis, uma equipe de IAs trabalhando juntas é melhor do que uma única IA trabalhando sozinha.
A Conclusão
O ProofCouncil sugere que, se você quiser resolver um problema matemático aberto e realmente difícil, não deve apenas pedir a uma IA para "dar um jeito nisso". Em vez disso, você precisa de um sistema onde uma IA escreva, outra desmonte o que foi escrito, uma terceira ofereça novas perspectivas e uma quarta realize os cálculos matemáticos pesados.
No mundo do desafio FirstProof, esta estratégia de "Autor-Crítico-Conselho" foi a estratégia mais bem-sucedida testada até agora. Ela não conquistou a montanha inteira, mas escalou mais alto do que qualquer outra, provando que, quando agentes de IA trabalham juntos como uma equipe de pesquisa humana, eles podem enfrentar problemas que antes eram considerados fora de alcance.
Afogado em artigos na sua área?
Receba digests diários dos artigos mais recentes que correspondam às suas palavras-chave de pesquisa — com resumos técnicos, no seu idioma.