Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

Este artigo apresenta o Ciclo de Conjectura-Prova (CPL), um pipeline que aproveita a aprendizagem em contexto ao alimentar iterativamente um LLM com seus próprios teoremas e provas formalmente verificados em Lean 4, a fim de melhorar significativamente a taxa de descoberta e o sucesso de conjecturas matemáticas novas e difíceis de provar.

O essencial

Imagine que você está tentando ensinar um robô muito inteligente, mas ligeiramente esquecido, a resolver quebra-cabeças matemáticos complexos. O robô é um Modelo de Linguagem de Grande Porte (LLM), e os quebra-cabeças são provas matemáticas formais escritas em uma linguagem de computador estrita chamada Lean.

O artigo apresenta uma nova maneira de ensinar esse robô, chamada de Loop de Conjectura-Prova (CPL). Eis como funciona, explicado através de analogias simples:

O Problema: A Armadilha do "Adivinhar e Verificar"

Geralmente, quando as pessoas tentam fazer a IA fazer matemática, elas pedem que ela adivinhe um quebra-cabeça e o resolva de uma só vez.

• A Analogia: Imagine pedir a um aluno para "Escrever um problema de matemática e resolvê-lo imediatamente".
• O Problema: O aluno fica preguiçoso. Ele escreve problemas fáceis (como "2 + 2 = 4") porque são fáceis de resolver. Ele evita problemas difíceis porque sabe que pode falhar. A IA acaba gerando milhares de provas fáceis e chatas, perdendo as difíceis e interessantes.

A Solução: A "Dança de Dois Passos" (CPL)

Os autores dividem o processo em duas funções distintas: um Conjeturador (o Gerador de Ideias) e um Provador (o Solucionador).

1. O Conjeturador (O Arquiteto): Esta parte da IA examina uma biblioteca de regras matemáticas existentes e cria novas ideias (conjecturas). Ela não tenta resolvê-las ainda; apenas as escreve.
2. O Provador (O Construtor): Esta parte pega as ideias e tenta construir uma prova para elas. Se falhar, tenta novamente. Continua tentando até ter sucesso ou esgotar as tentativas.
3. A Biblioteca (A Memória): Toda vez que o Provador constrói com sucesso uma prova, essa prova é adicionada à biblioteca.

O Ingrediente Mágico: Aprendizado em Contexto
Aqui está a parte inteligente: o Provador não olha apenas para as regras matemáticas originais. Ele olha para a biblioteca de provas que já construiu com sucesso durante a sessão atual.

• A Analogia: Imagine um aluno fazendo uma prova. Na maneira antiga, ele tinha que confiar apenas no que memorizou antes do início da prova. Nesta nova maneira, toda vez que o aluno resolve um problema corretamente, ele tem permissão para ler sua própria solução antes de enfrentar o próximo problema. Ele aprende os "truques" e "estratégias" de seus próprios sucessos recentes.

O Que Eles Encontraram

Os pesquisadores testaram isso em alguns conceitos complicados de topologia (um ramo da matemática que lida com formas e espaços) que a IA ainda não conhecia bem.

• Quantidade vs. Qualidade: O método antigo (adivinhar e resolver de uma vez) gerou mais teoremas no total, mas a maioria era curta e fácil. O novo método (CPL) gerou menos teoremas no total, mas eles eram muito mais difíceis e longos.
• O Grande Ganho: O novo método descobriu com sucesso um teorema específico e difícil sobre "conjuntos alpha-abertos" que o método antigo nunca encontrou, mesmo após 20 tentativas.
• Aprendizado com o Sucesso: Quando a IA recebeu a biblioteca de suas próprias provas anteriores como uma "cola" (contexto), ela conseguiu provar teoremas difíceis que não conseguia resolver sem esse contexto. Mesmo quando a IA não conseguia provar o teorema em inglês simples, ela conseguia prová-lo em código Lean assim que havia visto provas bem-sucedidas semelhantes.

A Conclusão

O artigo afirma que, ao separar a "geração de ideias" da "resolução de provas" e permitir que a IA aprenda com seus próprios sucessos verificados em tempo real, podemos fazê-la descobrir verdades matemáticas mais difíceis e complexas que de outra forma ela perderia. É como dar à IA uma vantagem inicial, permitindo que ela estude sua própria lição de casa antes de fazer a prova final.

Nota: O artigo foca estritamente neste método para gerar e verificar teoremas matemáticos. Ele não afirma que este método funciona para diagnóstico médico, previsão financeira ou outras aplicações do mundo real fora da matemática formal.

Resumo técnico

Resumo Técnico: Descobrindo Novos Teoremas via LLMs com Aprendizado de Prova em Contexto em Lean

Declaração do Problema
Modelos de Linguagem de Grande Escala (LLMs) demonstraram promessa na prova formal de teoremas, mas enfrentam desafios significativos: podem alucinar, e a geração simultânea de uma conjectura matemática e sua prova frequentemente leva à convergência para teoremas triviais ou fáceis. Abordagens existentes geralmente dependem de Ajuste Fino Supervisionado (SFT) ou Aprendizado por Reforço com Recompensas Verificadas (RLVR), que exigem dados de treinamento extensos e são difíceis de aplicar a modelos de código fechado. Além disso, os métodos atuais frequentemente lutam para descobrir teoremas "difíceis de provar", porque a probabilidade de gerar um teorema é fortemente ponderada pela taxa de sucesso imediata de prová-lo, fazendo com que a busca colapse em provas simples e curtas.

Metodologia: O Loop de Conjectura-Prova (CPL)
Os autores propõem o Loop de Conjectura-Prova (CPL), um pipeline projetado para gerar automaticamente conjecturas matemáticas e verificá-las em Lean 4. O framework separa a geração de conjecturas da geração de provas, utilizando uma biblioteca de teoremas previamente verificados como contexto para ambas as etapas.

O pipeline opera através de quatro componentes principais: um Conjeturador (agente LLM), um Provedor (agente LLM), um Servidor Lean e uma Biblioteca (dados de código Lean).

1. Fase de Conjectura: O Conjeturador gera novas declarações matemáticas no formato Lean 4 com base na biblioteca atual. Ele consulta o Servidor Lean para garantir validade sintática e novidade (verificando que a declaração não seja já provável por teoremas existentes no Mathlib4 ou na biblioteca atual).
2. Fase de Prova: Para cada conjectura válida, o Provedor tenta construir uma prova formal. Crucialmente, o Provedor recebe a biblioteca (contendo teoremas e provas previamente verificados) como contexto. Isso permite que o LLM aprenda estratégias de prova via aprendizado em contexto sem re-treinamento do modelo. O Provedor itera até um número máximo de tentativas (definido como 16 nos experimentos), usando mensagens de erro do Servidor Lean para refinar suas tentativas.
3. Iteração: Pares verificados de conjecturas e provas são adicionados à biblioteca, que então serve como contexto para iterações subsequentes.

Essa separação permite que o sistema aloque recursos de busca com base na dificuldade da prova. Diferentemente de um loop simples (SL) onde uma declaração e uma prova são geradas simultaneamente, o CPL tenta múltiplas provas para uma única declaração antes de descartá-la. Isso desloca a distribuição dos teoremas gerados para aqueles que são prováveis, mas difíceis, em vez daqueles que são meramente fáceis de provar.

Principais Contribuições

1. Proposta de Pipeline: A introdução do CPL, um framework que desacopla a geração de conjecturas da geração de provas, permitindo a descoberta de provas mais longas e complexas.
2. Aprendizado em Contexto para Modelos de Código Fechado: A demonstração de que LLMs de código fechado (especificamente o ChatGPT-o3) podem melhorar suas capacidades de prova através do aprendizado em contexto a partir de suas próprias saídas previamente verificadas, eliminando a necessidade de atualizações de parâmetros ou ajuste fino.
3. Validação Teórica e Empírica: O artigo fornece um modelo teórico mostrando que o CPL aumenta a probabilidade de gerar teoremas difíceis de provar em comparação com frameworks de geração simultânea. Experimentalmente, verifica que o CPL redescobriu com sucesso um teorema específico de nível de pesquisa que o framework de base não conseguiu encontrar.

Resultados Experimentais
Os autores avaliaram o CPL contra uma base de referência de Loop Simples (SL) usando noções topológicas (semi-abertura, $\alpha$-abertura e pré-abertura) definidas dentro do Mathlib, mas ainda não incluídas na biblioteca. O alvo foi o teorema afirmando que a interseção de dois conjuntos $\alpha$-abertos é $\alpha$-aberta.

• Taxa de Descoberta: Em 20 execuções experimentais, o CPL descobriu o teorema alvo 5 vezes. Em contraste, o framework SL, que gerou significativamente mais teoremas em média (328 vs. 106), não conseguiu gerar o teorema alvo nem uma única vez. O teste exato de Fisher confirmou que essa diferença foi estatisticamente significativa ($p = 0.024$).
• Comprimento da Prova: O CPL gerou teoremas com comprimentos de prova significativamente maiores (em contagem de caracteres) em comparação com o SL, apoiando a afirmação teórica de que o framework desloca o foco para provas mais difíceis.
• Eficácia do Contexto:
  • Re-prova: Ao re-provar teoremas gerados, fornecer a biblioteca como contexto aumentou a taxa de sucesso de 91% para 99% ($p = 4 \times 10^{-35}$).
  • Teorema Alvo: Ao tentar re-provar o teorema alvo de interseção $\alpha$-aberta, o provedor teve sucesso 7 vezes em 80 tentativas quando fornecido com a biblioteca gerada como contexto. Sem a biblioteca, falhou 100% das vezes.
  • Base de Referência em Linguagem Natural: Ao ser solicitado a provar o teorema em linguagem natural, o ChatGPT-4o frequentemente julgou o teorema falso ou forneceu provas incorretas, e o ChatGPT-o3 consistentemente julgou-o falso, indicando que o teorema estava fora do conhecimento pré-treinado dos modelos. O sucesso em Lean 4 foi atribuído ao aprendizado em contexto de estratégias de prova a partir da biblioteca gerada.

Significado e Afirmações
O artigo afirma que o CPL aborda efetivamente a limitação dos LLMs na descoberta de teoremas não triviais, aproveitando o aprendizado em contexto a partir de provas verificadas auto-geradas. Os autores enfatizam que essa abordagem permite a expansão automática de bibliotecas de matemática formal (como o Mathlib) gerando proposições sobre noções dadas que podem não ser explicitamente conhecidas pelo LLM. O trabalho sugere que separar as fases de conjectura e prova, combinado com o enriquecimento iterativo de contexto, é uma estratégia viável para prova neural de teoremas, particularmente para modelos de código fechado onde métodos tradicionais de treinamento não são aplicáveis. Os autores mantêm uma postura modesta, observando que, embora o framework tenha redescoberto com sucesso um teorema conhecido de nível de pesquisa, trabalhos futuros são necessários para refinar o processo de geração para declarações matemáticas mais profundas e perspicazes.