Formally Solving Answer-Construction Problems in Lean

Resumo Técnico: Resolvendo Formalmente Problemas de Construção de Resposta em Lean

Definição do Problema
Problemas de competições matemáticas geralmente se dividem em duas categorias: prova de teoremas (verificação de uma afirmação dada) e construção de resposta (construção de um objeto específico que satisfaça uma propriedade). Embora avanços recentes em Grandes Modelos de Linguagem (LLMs) tenham melhorado significativamente a prova formal de teoremas, a construção formal de respostas permanece subexplorada. Existe uma lacuna crítica entre sistemas de raciocínio informal, que são fortes em conjecturar, mas fracos em verificação formal, e LLMs de prova formal, que são otimizados para provas, mas têm dificuldade em descobrir os testemunhos necessários para eliminar quantificadores existenciais.

Um desafio específico na formalização da construção de respostas é a admissibilidade. Verificadores de prova Lean padrão verificam se um termo de prova possui o tipo correto, mas não impõem inerentemente que o testemunho construído seja uma resposta canônica e de forma fechada. Por exemplo, uma prova pode satisfazer uma afirmação existencial $\exists x, P(x)$ retornando um termo não canônico como sInf PropertySet (o ínfimo do conjunto sendo definido) em vez de um número natural explícito (por exemplo, 245). Tais testemunhos "circulares" ou de forma não fechada são matematicamente válidos dentro da lógica, mas inadmissíveis como respostas de concursos.

Metodologia: Enumerar-Conjecturar-Provar (ECP)
Para enfrentar esses desafios, os autores introduzem o Enumerate-Conjecture-Prove (ECP), um framework neuro-simbólico projetado para a construção de respostas de ponta a ponta com provas formais em Lean 4. O ECP separa o processo em estágios distintos, mantendo um loop de verificação formal:

1. Formalização do Problema e Verificação de Admissibilidade:

   • Os problemas são formalizados como tarefas de síntese funcional: encontrar uma função $\Psi$ tal que $\forall X, P(X) \to Q(X, \Psi(X))$.
   • Um verificador de admissibilidade é implementado para garantir que a resposta sintetizada use apenas um "vocabulário admissível" pré-definido (ex: constantes específicas, operadores aritméticos e construtores padrão). Ele extrai estruturalmente constantes semânticas do termo Lean e filtra constantes administrativas (como instâncias de typeclass ou artefatos do compilador) e definições não canônicas (como sInf).

2. Estágio de Enumeração (Exploração Assistida por Ferramentas):

   • Um LLM de propósito geral (ex: GPT-5.4) é equipado com capacidades de execução de ferramentas Python.
   • O LLM escreve e executa código Python para realizar enumeração limitada sobre domínios pequenos para encontrar tuplas que satisfaçam as restrições do problema.
   • Esses rastreios de execução servem como evidência empírica para identificar padrões, invariantes e formas funcionais.

3. Estágio de Conjectura (Síntese de Resposta):

   • Usando a evidência do estágio de Enumeração, o mesmo LLM de propósito geral sintetiza uma função de resposta candidata $\Psi'$.
   • A candidata passa por dois filtros antes de prosseguir:
     • Verificação Sintática: O termo deve compilar em Lean com o tipo correto.
     • Verificação de Admissibilidade: O termo deve usar apenas constantes do vocabulário permitido.
   • Se uma candidata falhar, o sistema itera incluindo a mensagem de erro no prompt.

4. Estágio de Prova (Verificação Formal):

   • Uma vez construída uma candidata válida $\Psi'$, o sistema tenta provar o teorema instanciado $Stmt(T)|_{\Psi=\Psi'}$.
   • Loop de Refutação: Antes de tentar uma prova, o sistema tenta refutar a candidata provando a negação. Se a refutação for bem-sucedida, a candidata é descartada e o sistema retorna ao estágio de Conjectura.
   • Geração de Prova: Se a refutação falhar, o sistema tenta provar a afirmação positiva usando uma combinação da automação integrada do Lean (táticas como simp, aesop, ring, norm_num) e um prover LLM especializado (ex: Goedel-Prover-V2). Se a automação falhar, o prover LLM é invocado com um loop de reparação para gerar ou corrigir a prova.

Principais Contribuições

• Framework para Construção de Respostas: O ECP é o primeiro framework que separa explicitamente a construção de respostas da geração de provas, enquanto impõe restrições de admissibilidade dentro de um loop de verificação formal.
• Imposição de Admissibilidade: O artigo introduz um método estrutural para filtrar testemunhos não canônicos (ex: definições circulares) que os verificadores padrão do Lean aceitariam, garantindo que a saída corresponda aos requisitos de concursos.
• Integração Neuro-Simbólica: O framework combina efetivamente o raciocínio exploratório de LLMs gerais com ferramentas Python e as capacidades rigorosas de prova de LLMs de prova especializados.
• Benchmarks e Autoformalização: Os autores autoformalizaram 75 problemas das finais de 2026 do MathArena (AIME, HMMT, APEX) e 346 problemas de construção de resposta do PutnamBench, criando um novo padrão de avaliação para este tipo de problema.

Resultados Experimentais
O sistema foi avaliado no MathArena 2026 (75 problemas) e no PutnamBench (346 problemas) contra baselines incluindo LLMs de geração de prova direta (GPT-5.4, Goedel-Prover-V2).

• Desempenho Ponta a Ponta: O ECP superou as baselines de geração de prova direta.
  • MathArena: O ECP resolveu 18/75 problemas (Pass@32), comparado a 13/75 para a melhor baseline apenas de LLM (GPT-5.4).
  • PutnamBench: O ECP resolveu 17/346 problemas (Pass@32), comparado a 8/346 para GPT-5.4 e 7/346 para Goedel-Prover-V2-32B.
• Precisão de Apenas Resposta: A construção de resposta assistida por ferramentas melhorou significativamente a precisão dos LLMs gerais na geração de candidatos corretos. Para o GPT-5.4, o uso de ferramentas aumentou a construção de respostas corretas no PutnamBench de 290/346 para 303/346.
• Impacto da Admissibilidade: A análise revelou que muitas provas geradas pelas baselines eram compiláveis em Lean, mas continham respostas inadmissíveis (ex: testemunhos circulares). O check de admissibilidade explícito do ECP foi crucial para filtrá-las.
• Estudos de Ablação:
  • Remover o passo de correção do prover LLM reduziu o desempenho no MathArena (18 $\to$ 16) e no PutnamBench (17 $\to$ 16).
  • Remover a automação do Lean teve um impacto severo no MathArena (18 $\to$ 11), mas menos no PutnamBench na execução específica, sugerindo que os problemas do MathArena dependem mais de táticas de automação, enquanto o PutnamBench depende mais da capacidade do prover.
  • Usar um prover menor (8B) manteve o desempenho no MathArena, mas reduziu significativamente os resultados do PutnamBench (17 $\to$ 7), indicando que os problemas do Putnam são mais limitados pela busca de prova.

Significância e Alegações
O artigo alega que o ECP consegue preencher a lacuna entre a geração de respostas informais e a prova de teoremas formal. Ao lidar explicitamente com a fase de "construção de resposta" e impor a admissibilidade, o ECP resolve instâncias que são atualmente intratáveis para abordagens de geração de prova direta. Os autores enfatizam que sua abordagem é particularmente eficaz para problemas que exigem a construção de um testemunho específico (quantificação existencial) em vez de apenas verificar uma conclusão fixa.

O trabalho destaca que os benchmarks formais atuais frequentemente omitem a dificuldade da construção de respostas, focando em vez disso em versões de problemas "com resposta". O ECP demonstra que combinar LLMs gerais com execução de ferramentas para enumeração, seguido por LLMs de prova especializados para verificação, é um caminho viável para resolver problemas matemáticos complexos e abertos em sistemas formais. Os autores observam limitações quanto à natureza heurística da rotulagem do vocabulário admissível e o potencial de explosão combinatória na etapa de enumeração para problemas de combinatória altamente complexos.