Resumo Técnico: Construção–Verificação: Um Benchmark para a Formalização da Matemática Aplicada em Lean 4

1. Declaração do Problema

Os benchmarks atuais para prova de teoremas automatizada, como MiniF2F e ProofNet, concentram-se predominantemente na verificação lógica de proposições declarativas (ou seja, provar a existência de uma solução). Este paradigma é insuficiente para a matemática aplicada, onde o objetivo primário é frequentemente a derivação de valores concretos, algoritmos executáveis ou transformações estruturais, em vez de meras provas de existência.

Os conjuntos de dados existentes sofrem de duas limitações críticas neste domínio:

1. Lacuna de Escopo: Carecem de cobertura de matemática aplicada de nível de graduação e superior, incluindo análise convexa, otimização, álgebra numérica e probabilidade de alta dimensão.
2. Déficit Construtivo: Falham em impor um fluxo de trabalho de "construção–verificação". Na matemática aplicada, um modelo deve sintetizar explicitamente uma solução (por exemplo, um algoritmo ou um valor específico) antes de provar sua corretude. Os benchmarks atuais permitem que os modelos contornem isso usando táticas não construtivas (por exemplo, provar a existência via teorema do valor extremo sem calcular o ótimo específico), o que representa erroneamente a capacidade do modelo de realizar raciocínio computacional.

2. Metodologia

O Framework de Construção–Verificação

Os autores propõem um paradigma de formalização em Lean 4 que impõe estruturalmente um fluxo de trabalho de dois estágios: Construção seguida de Verificação. Este framework impede que agentes explorem atalhos não construtivos ao exigir definições explícitas antes das provas. O framework aborda três categorias específicas de tarefas de matemática aplicada:

• Problemas de Avaliação: Em vez de provar $\exists x, Q(x)$, o agente deve definir uma função def x (V) := ... que computa a solução $x(V)$ baseada em parâmetros $V$, seguido por um teorema provando $Q(x(V), V)$. A assinatura da função restringe estritamente as entradas aos parâmetros brutos, impedindo o modelo de usar a propriedade alvo para "trapacear" a construção.
• Problemas de Design de Algoritmo: O agente deve definir uma função recursiva que represente um processo iterativo (por exemplo, Gradiente Descendente). A tarefa exige o preenchimento da regra de transição (o corpo do loop) para o passo $(n+1)$, seguido de uma prova de propriedades como convergência ou monotonicidade.
• Transformação de Representação: O agente deve modelar uma instância de problema bruta como uma forma canônica alvo (por exemplo, transformar um problema de corte de grafo em uma formulação de agrupamento espectral). Isso envolve definir o novo domínio, restrições e função objetivo, e provar uma relação de relaxação ou equivalência entre o problema de origem e o alvo.
• Prova de Teoremas: Um subconjunto de base de tarefas dedutivas tradicionais é incluído para medir as capacidades de raciocínio lógico puro distintas da síntese construtiva.

Curadoria do Benchmark (AMBER)

Os autores introduzem o AMBER (Applied Mathematics BEnchmark for Reasoning), um conjunto de dados que abrange quatro domínios principais:

1. Análise Convexa
2. Otimização
3. Álgebra Numérica
4. Probabilidade de Alta Dimensão

Fontes de Dados e Dificuldade: Os problemas são extraídos de livros didáticos clássicos (ex: Boyd & Vandenberghe, Vershynin) e categorizados por dificuldade (Fácil: exercícios padrão; Difícil: nível de exame de qualificação de doutorado).
Formalização e Validação: 50 problemas por subcampo foram formalizados por usuários experientes de Lean. A validação envolveu um processo de dois estágios: uma verificação semântica baseada em LLM seguida de uma rigorosa validação cruzada manual por contribuidores do Mathlib para garantir o alinhamento estrito com as declarações matemáticas originais.
Métricas de Complexidade: O benchmark é caracterizado por uma alta densidade de dependência semântica. Usando uma análise de grafo de dependência ($k=3$), o AMBER exibe uma densidade de dependência média de 164,21, significativamente superior à do MiniF2F (29,72), ProofNet (33,95) e FATE (51,14), indicando uma exigência mais profunda de recuperação e raciocínio sobre conceitos matemáticos complexos.

3. Principais Contribuições

1. Mudança de Paradigma: O artigo propõe uma mudança da verificação de proposições existenciais para a síntese de soluções construtivas, alinhando tarefas formais com a intuição computacional da matemática aplicada.
2. Benchmark AMBER: Um conjunto de dados abrangente cobrindo núcleos de domínios aplicados com níveis de dificuldade variados, apresentando tarefas complexas como design de algoritmos e transformação de representação, não apenas prova de teoremas.
3. Padrões de Formalização: Templates especializados de Lean 4 para avaliação, design de algoritmo e transformação de representação que impõem barreiras sintáticas estritas contra o raciocínio não construtivo.
4. Análise Empírica: Uma avaliação sistemática que revela um trade-off fundamental em sistemas neuro-simbólicos atuais: a tensão entre proficiência tática local (provers especializados) e síntese algorítmica de alto nível (modelos gerais).

4. Resultados Experimentais

Desempenho dos Modelos

Os autores avaliaram um conjunto diversificado de modelos, incluindo agentes de raciocínio de propósito geral (DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro) e provadores de teoremas especializados (Goedel Prover-32B, Kimina Prover-72B).

• Dificuldade Geral: O desempenho em todos os modelos é notavelmente baixo. No subconjunto "Difícil", as taxas de sucesso são próximas de zero para quase todos os modelos.
• Geral vs. Especializado: Contrariando a tendência em benchmarks de matemática pura, modelos de raciocínio de propósito geral superam consistentemente os provadores especializados.
  • Pass@16 (AMBER Completo): Modelos gerais alcançaram 4,50%–6,00%, enquanto provadores especializados alcançaram 4,00%.
  • Pass@16 (Subconjunto Difícil): Modelos gerais alcançaram 0%–0% (com alguma variação nos subconjuntos Fáceis), enquanto os provadores especializados também tiveram dificuldades significativas.
• Estudo de Ablação: A estratégia de prompt de construção–verificação rendeu uma taxa de sucesso de 8% em um subconjunto de 100 problemas, superando a conclusão de código padrão (6%) e os prompts tradicionais de apenas prova (5%). Prompts de apenas prova frequentemente levaram os modelos a usar atalhos não construtivos (ex: Classical.choice).

Análise de Erros

Uma análise de 3.189 mensagens de erro do modelo DeepSeek-R1 revelou:

1. Alucinação (47,3%): O modo de falha mais comum, onde os modelos invocam teoremas ou definições inexistentes (ex: convexHull eq sInter).
2. Competência de Formalização (32,7%): Aplicação incorreta de táticas válidas ou falha em cumprir condições laterais.
3. Saídas Incompletas (15,2%): Falha em fornecer código totalmente executável, frequentemente deixando placeholders sorry em passos indutivos complexos.
4. Formatação/Sintaxe (4,8%): Erros básicos de markdown ou sintaxe.

5. Significância e Alegações

O artigo afirma que o cenário atual da formalização automatizada enfrenta um fenômeno de "sobreajuste tático". Modelos especializados, extensivamente ajustados em corpora de provas, parecem degradar suas capacidades gerais de seguimento de instruções. Eles tratam cada desafio estrutural como uma tarefa pura de prova de teoremas, muitas vezes ignorando os requisitos de múltiplos estágios da matemática aplicada (ex: definir uma função antes de prová-la).

Em contraste, modelos de propósito geral retêm a versatilidade necessária para fazer a ponte entre a intenção informal e a sintaxe formal, sintetizando objetos matemáticos com sucesso antes de entrar na etapa de verificação. Os autores concluem que o avanço da matemática aplicada formalizada exige ir além da busca pura por provas em direção a sistemas neuro-simbólicos que integrem o raciocínio algorítmico de alto nível com a verificação formal rigorosa. O benchmark AMBER serve como uma fundação para pesquisas futuras na expansão das fronteiras da matemática aplicada formalizada, fornecendo um padrão que exige síntese construtiva em vez de mera validade lógica.