Resumo Técnico: CAM-Bench

Declaração do Problema

Os benchmarks existentes de prova de teoremas formais para Grandes Modelos de Linguagem (LLMs) focam predominantemente em problemas no estilo de Olimpíadas e domínios algébricos (por exemplo, MiniF2F, PutnamBench, ProofNet). Embora esses benchmarks tenham impulsionado o progresso no raciocínio formal, eles deixam a matemática computacional e aplicada significativamente sub-representada.

Problemas em matemática aplicada (por exemplo, otimização, álgebra linear numérica, análise numérica) diferem fundamentalmente de declarações de teoremas isolados. Eles são frequentemente dependentes de contexto, dependendo de:

• Definições, notações e algoritmos introduzidos localmente.
• Convenções e resultados elementares específicos de capítulos.
• Pressupostos herdados que não são explicitamente declarados no exercício, mas são necessários para uma formalização fiel.

Os benchmarks atuais lutam para avaliar se os modelos conseguem rastrear essas suposições locais, decompor provas com base em contextos de livros didáticos e aplicar resultados elementares que ainda não estão disponíveis como lemas padrão em bibliotecas formais como o Mathlib4. Há uma necessidade de um benchmark que vise problemas de matemática aplicada onde o "contexto local" é tão crítico quanto a própria declaração do teorema.

Metodologia

Os autores introduzem o CAM-Bench, um benchmark de prova de teoremas em Lean 4 composto por 1.000 alvos de prova derivados de 778 exercícios de livros didáticos em otimização, álgebra linear numérica e análise numérica. A construção deste benchmark baseia-se em um novo pipeline de recuperação de dependências e formalização projetado para transformar exercícios dependentes de contexto em alvos autossuficientes e verificáveis por máquina.

1. Pipeline de Recuperação e Enriquecimento de Dependências

Para abordar a natureza não autossuficiente dos exercícios de livros didáticos, os autores desenvolveram um procedimento recursivo de expansão de dependências (Algoritmo 1):

• Expansão Recursiva: Começando com um exercício bruto, o sistema extrai referências (teoremas, equações, algoritmos) e recupera recursivamente suas definições e dependências até uma profundidade limitada.
• Naturalização de Baixo para Cima: A árvore de dependências é processada de baixo para cima. Um naturalizador de LLM mescla representações enriquecidas, resolvendo referências locais, padronizando notações e suavizando transições para garantir que definições de nível inferior sejam incorporadas antes que dependências de nível superior as utilizem.
• Recuperação de Condições Implícitas: O sistema torna explícitas as suposições necessárias (por exemplo, restrições de domínio, positividade, convexidade) apenas quando apoiado pelo problema original ou contexto recuperado. Este enriquecimento é fundamentado na fonte; ele não conjectura dependências ausentes, mas as exclui se não puderem ser recuperadas.
• Revisão de Múltiplas Rodadas: Declarações enriquecidas passam por um loop de validação para verificar suposições ausentes, desvio de tarefa e adequação ao Lean. Reparos são restritos para corrigir defeitos locais sem alterar o objetivo matemático ou inventar dependências não suportadas.

2. Formalização em Lean Impulsionada por Modularização

Uma vez estabelecido um alvo informal, o sistema o converte em código Lean 4 usando uma estratégia de construção em blocos com contexto congelado:

• Decomposição Semântica em Blocos: Exercícios heterogêneos são decompostos em blocos semânticos tipados (definições, problemas de otimização, algoritmos, alvos de teorema). Isso separa o contexto de suporte do objetivo final do teorema.
• Tradução Incremental: O sistema traduz blocos sequencialmente. Declarações previamente aceitas são mantidas como um contexto congelado e somente leitura. Isso previne erros em cascata e localiza falhas no bloco atual.
• Reparo Guiado por Compilador e Semântico:
  • Reparo de Compilação: Se um bloco falhar em compilar, um corretor usa diagnósticos do compilador para gerar patches locais (sintaxe, anotações de tipo, resolução de namespaces).
  • Revisão Semântica: Um revisor compara o candidato compilável com o bloco informal para garantir fidelidade semântica (preservando variáveis, suposições e conclusões). Incompatibilidades acionam reescrita semântica.
• Controle Consciente do Histórico: O sistema mantém um histórico de tentativas falhas e motivos de rejeição para evitar oscilação e orientar reparos subsequentes para longe de direções anteriormente falhas.

3. Construção e Validação do Benchmark

O conjunto de dados final inclui o exercício bruto, o contexto recuperado, o teorema informal normalizado e o alvo Lean final. A validação ocorre em dois níveis:

• Nível de Fonte: Garante que o alvo informal seja fiel ao exercício do livro didático e autossuficiente.
• Nível Lean: Garante que a declaração formal preserve o alvo informal revisado. Apenas 92,5% das declarações candidatas foram consideradas utilizáveis após validação semântica, destacando a dificuldade da autoformalização fiel.

Principais Contribuições

1. Conjunto de Dados CAM-Bench: Um benchmark curado de 1.000 alvos de prova em Lean abrangendo otimização, álgebra linear numérica e análise numérica. Ele fornece artefatos rastreáveis desde exercícios brutos até alvos Lean verificados por máquina, preenchendo a lacuna na avaliação de matemática aplicada.
2. Pipeline de Recuperação de Dependências: Um método inovador para construir alvos Lean fiéis a partir de exercícios dependentes de contexto. Combina expansão recursiva de dependências, enriquecimento fundamentado na fonte e reparo restrito para lidar com definições e suposições locais que não são lemas padrão do Mathlib4.
3. Avaliação Abrangente e Análise de Erros: O artigo avalia LLMs de ponta e agentes de formalização no CAM-Bench. Identifica modos de falha específicos:
   • Fundamentação em Biblioteca/API: Modelos falham em fundamentar provas na infraestrutura disponível do Mathlib, alucinando APIs ou perdendo resultados de ponte.
   • Representação Formal: Erros em disciplina de tipo, incompatibilidades de dimensão/índice e falhas de coerção.
   • Decomposição de Prova: Incapacidade de decompor provas de longo horizonte em lemas auxiliares ou manter controle sobre argumentos complexos de otimização/numéricos.

Resultados

Desempenho de Linha de Base

• Modelos Não-Agentivos: Mesmo as linhas de base não-agentivas mais fortes (por exemplo, Deepseek-v4-pro, Claude-sonnet-4-6) alcançaram baixa precisão verificada em Lean, com a melhor atingindo 19,67% (Pass@32).
• Lacuna entre Informal e Formal: Há uma discrepância significativa entre a correção informal (Precisão informal Pass@1 ~70–84%) e a correção Lean verificada (<20%). Modelos capturam argumentos de alto nível, mas falham em satisfazer sintaxe estrita do Lean, disciplina de tipo e restrições de biblioteca.
• Melhoria Agentiva: Sistemas de busca de prova agentivos (por exemplo, GPT-5.4 com reparo iterativo e uso de ferramentas) melhoraram significativamente o desempenho, atingindo 44,00% de precisão verificada. No entanto, isso veio a um alto custo de tokens (~1,96M tokens vs. ~0,26–0,70M para linhas de base).

Avaliação de Agentes Externos

Dois sistemas agentivos externos, M2F e Aristotle, foram avaliados em 200 instâncias amostradas com um orçamento de tempo de 8 horas:

• M2F: Resolveu 143/200 instâncias (71,5%).
• Aristotle: Resolveu 125/200 instâncias (62,5%).
• Apesar dessas melhorias, o benchmark permanece insaturado. Muitas falhas foram atribuídas à infraestrutura matemática ausente, cadeias longas de lemas auxiliares e raciocínio específico de otimização.

Significado e Alegações

O artigo afirma que o CAM-Bench serve como um complemento crítico aos benchmarks formais existentes ao visar problemas de matemática aplicada que dependem de conceitos de livros didáticos e teoremas elementares. Seu significado reside em:

1. Avaliar Raciocínio Dependente de Contexto: Testa a capacidade de um modelo de rastrear suposições locais e reconstruir contexto, uma capacidade essencial para formalização do mundo real, mas frequentemente ignorada por benchmarks de teoremas isolados.
2. Diagnosticar Gargalos Sistêmicos: Os resultados destacam que os provadores atuais baseados em LLM lutam não apenas com sintaxe, mas com fundamentação no Mathlib, disciplina de tipo e decomposição de prova de longo horizonte.
3. Impulsionar o Desenvolvimento de Infraestrutura: O benchmark sugere que o progresso na matemática aplicada formal requer infraestrutura Mathlib mais forte (por exemplo, para matrizes, espectros, convexidade) e agentes mais capazes que possam gerenciar trajetórias de prova de longo horizonte.

Os autores mantêm uma postura modesta, observando que, embora os sistemas agentivos melhorem o desempenho, o benchmark permanece desafiador, e os resultados devem ser vistos como estimativas das capacidades atuais, e não como um problema resolvido. O benchmark destina-se a ser um componente de uma suite de avaliação mais ampla para sistemas de raciocínio matemático.