Resumo Técnico: LEAP: Potencializando LLMs para Matemática Formal com Estruturas Agênticas

1. Definição do Problema

Modelos de Linguagem de Grande Escala (LLMs) demonstraram capacidades robustas em raciocínio matemático "informal" (linguagem natural), mas enfrentam dificuldades para gerar provas mecanicamente verificáveis em linguagens formais como o Lean. Embora modelos especializados, ajustados finamente (fine-tuned) em corpora formais, tenham mostrado promessa, modelos de fundação de uso geral frequentemente apresentam desempenho insuficiente em prova de teoremas formais de tentativa única (one-shot). Além disso, os benchmarks existentes (ex: MiniF2F, PutnamBench) estão se tornando saturados, e os sistemas especializados atuais muitas vezes dependem de componentes de código fechado ou falham em escalar para provas altamente não rotineiras e de múltiplos passos, exigidas por competições avançadas como a Olimpíada Internacional de Matemática (IMO).

O desafio central é preencher a lacuna entre o forte raciocínio informal dos LLMs de uso geral e os requisitos rigorosos de verificação de máquina para a matemática formal, sem depender exclusivamente de ajuste fino especializado.

2. Metodologia: Estrutura LEAP

Os autores introduzem o LEAP (LLM-in-Lean Environment Agentic Prover), uma estrutura agêntica projetada para permitir que modelos de fundação de uso geral alcancem o estado da arte em prova automática de teoremas formais. O LEAP não depende de modelos de prova especializados e ajustados finamente, mas sim aproveita as habilidades complementares dos LLMs de uso geral: raciocínio informal, seguimento de instruções, uso de ferramentas e autorrefinamento iterativo.

2.1. Decomposição Hierárquica Baseada em Blueprint

Inspirado no fluxo de trabalho matemático humano e na ferramenta Lean Blueprint, o LEAP decompõe provas complexas em unidades gerenciáveis. O sistema opera em um Grafo Acíclico Dirigido (DAG) AND-OR:

• Nós OR: Representam objetivos abertos ou enunciados de lemas que podem ser resolvidos por qualquer estratégia de prova válida.
• Nós AND: Representam decomposições candidatas onde o objetivo pai é considerado provado apenas se todos os subobjetivos constituintes forem provados.

2.2. Fluxo de Trabalho e Refinamento Iterativo

O LEAP segue um fluxo de trabalho de múltiplos estágios (ilustrado na Figura 1 do artigo):

1. Tentativa de Formalização Direta: O agente primeiro tenta gerar uma prova informal direta, traduzi-la para Lean e verificá-la com o compilador Lean.
2. Decomposição (Blueprinting): Se a prova direta falhar, o LEAP elabora um blueprint informal propondo lemas intermediários. Este blueprint é traduzido em um esboço de prova formal.
   • O esboço prova o objetivo atual assumindo os lemas propostos (usando marcadores sorry apenas para os novos lemas).
   • Se o esboço for sintaticamente válido e tipologicamente correto, ele é adicionado como um nó AND, e os lemas propostos tornam-se nós filhos OR.
3. Busca Guiada por Verificação:
   • Feedback do Compilador: O compilador Lean valida a sintaxe e os tipos.
   • Revisor LLM: Um componente crítico onde um revisor LLM avalia a qualidade da decomposição. Ele filtra ramos improdutivos (ex: subobjetivos que são tão difíceis quanto o problema original ou sintaticamente idênticos ao pai) para evitar a explosão da busca.
4. Memoização Hierárquica: A estrutura de DAG permite o armazenamento e reuso de lemas intermediários entre diferentes ramos, evitando derivações redundantes e suportando o "planejamento antecipatório de lemas" (propor lemas que não são imediatamente necessários, mas que serão úteis posteriormente).

3. Principais Contribuições

3.1. A Estrutura Agêntica LEAP

O artigo demonstra que o estado da arte em prova de teoremas formais pode ser alcançado usando apenas LLMs de uso geral quando acoplados a uma estrutura agêntica estruturada. Isso desafia a suposição predominante de que o ajuste fino especializado é indispensável para tarefas formais rigorosas. A estrutura codifica um fluxo de trabalho humano: esboço de blueprint de alto nível seguido por geração formal de baixo nível e feedback iterativo do compilador.

3.2. Conjunto de Dados Lean-IMO-Bench

Para avaliar o progresso além dos benchmarks saturados, os autores introduzem o Lean-IMO-Bench, um novo conjunto de dados que formaliza 60 problemas do IMO-Bench (Luong et al., 2025) em Lean.

• Estrutura: Dividido em um conjunto "Básico" (pré-IMO até IMO-Médio) e um conjunto "Avançado" (até IMO-Difícil).
• Características: Os problemas apresentam enunciados curtos, mas exigem provas altamente não rotineiras, de múltiplos passos e estruturalmente intrincadas.
• Verificação: Todos os 60 enunciados de problemas foram formalizados manualmente e verificados por especialistas em Lean para garantir a precisão.

3.3. Resultados Empíricos e Análise

O artigo fornece evidências empíricas extensas em dois grandes benchmarks:

• Putnam 2025: O LEAP resolveu 100% dos 12 problemas (12/12), igualando o desempenho de sistemas de código fechado de fronteira (Aristotle, Numina) e superando significativamente as linhas de base diretas (0% de taxa de resolução para LLMs gerais e modelos especializados em configurações one-shot).
• Lean-IMO-Bench: O LEAP aumentou a taxa de resolução formal one-shot de LLMs de uso geral de <10% para 70%. Notavelmente, superou modelos de ATP especializados (5%) e o sistema de calibre de medalha de ouro Aristotle (48%). O LEAP alcançou taxas de resolução de 100% em Álgebra e Teoria dos Números em ambos os níveis de dificuldade.

3.4. Estudos de Ablação

Os autores realizaram estudos de ablação para isolar as contribuições dos componentes do LEAP:

• Iterativo vs. One-Shot: LLMs gerais (Gemini-1.5-Pro) melhoraram significativamente (de 20% para 36,6%) com o feedback iterativo do compilador, enquanto modelos especializados (Goedel-Prover-V2) não se beneficiaram tanto, destacando a importância das capacidades de raciocínio geral.
• DAG vs. Árvore: Remover a memoização de grafo global (usando uma estrutura de árvore ingênua) reduziu o desempenho de 83,3% para 73,3% no conjunto Básico, confirmando o valor do reuso de lemas e do contexto de grafo.
• Revisor LLM: Remover o revisor de decomposição baseado em LLM fez com que o agente falhasse em problemas complexos (ex: Putnam A5) devido a decomposições cíclicas improdutivas, provando a necessidade do filtro de busca semântica.

4. Significância e Alegações

O artigo afirma que o principal gargalo para LLMs de uso geral em matemática formal não é a compreensão de linguagem, mas a falta de interação estruturada e iterativa com o ambiente de prova. Ao fornecer suporte aos LLMs gerais com uma estrutura agêntica que inclui decomposição hierárquica, feedback do compilador e revisão semântica, o sistema pode preencher a lacuna entre o raciocínio informal e a verificação formal.

Os autores demonstram que modelos de fundação gerais, quando colocados no ambiente agêntico correto, podem progredir de um desempenho próximo de zero em matemática formal para a resolução de problemas de pesquisa abertos e altamente complexos. Isso é evidenciado pela formalização autônoma pelo LEAP de um subproblema chave na decomposição de Hamiltonian de Knuth para grafos de Cayley de ordem par, um desafio combinatório complexo que requer mais de 5.000 linhas de código Lean verificado.

O trabalho sugere uma mudança de paradigma: em vez de depender apenas de pequenos modelos especializados treinados em corpora formais, o campo pode aproveitar o vasto conhecimento, a capacidade de seguir instruções e as habilidades de autocorreção dos modelos de fundação gerais para alcançar resultados competitivos e, em alguns casos, superiores na prova de teoremas formais.