Resumo Técnico: APE-Bench: Avaliando a Engenharia de Provas Automatizada para Bibliotecas de Matemática Formal

Declaração do Problema

Os benchmarks de avaliação atuais para matemática formal baseados em Grandes Modelos de Linguagem (LLMs), como o miniF2F e o FATE, concentram-se primariamente na provação de teoremas isolados. Esses benchmarks exigem que agentes sintetizem um termo de prova para um determinado enunciado formal que passe na verificação de tipos. No entanto, a prática do desenvolvimento de matemática formal em ambientes de produção (ex: Mathlib) evoluiu para a engenharia de provas em escala de repositório. O desenvolvimento no mundo real envolve coordenação entre múltiplos arquivos, evolução da biblioteca, gerenciamento de dependências entre arquivos e manutenção sob mudanças — tarefas que os benchmarks de provação de teoremas isolados falham em capturar. Ferramentas existentes para manutenção de provas (ex: iCoq, REPLICA) permanecem amplamente heurísticas e exigem esforço manual significativo. Há uma carência de um framework sistemático para avaliar agentes de IA nas atividades de engenharia de escala de repositório que caracterizam o desenvolvimento real de matemática formal.

Metodologia

1. Formulação de Engenharia de Provas Automatizada (APE)

Os autores introduzem a Engenharia de Provas Automatizada (APE) como uma formulação de tarefa que operacionaliza a engenharia de provas em escala de repositório. Uma tarefa de APE é definida por três componentes:

• Ambiente Fixado (Pinned Environment): Um commit específico do repositório e uma versão da ferramenta (toolchain).
• Instrução em Linguagem Natural: Uma descrição do objetivo de engenharia (ex: "refatorar", "adicionar automação").
• Verificação Dupla:
  • Corretude Sintática: O código modificado deve compilar com sucesso dentro do ambiente fixado.
  • Corretude Semântica: A solução deve satisfazer os requisitos de linguagem natural e manter o controle de escopo (evitando mudanças gratuitas), validada via LLM-as-Judge (LLM como juiz).

Esta formulação espelha o paradigma SWE-bench para engenharia de software, mas o adapta para a matemática formal ao substituir testes unitários por validação baseada em julgamento, já que tarefas de prova frequentemente carecem de suítes de testes pré-existentes.

2. Infraestrutura APE-Harness

Para suportar a avaliação sistemática, os autores construíram o APE-Harness, uma infraestrutura de execução baseada em Abstração de Contrato de Tarefa.

• Contratos de Tarefa: Especificações declarativas que separam os requisitos da tarefa (objetivos, limites, vínculos de ambiente, protocolos de verificação) das estratégias de execução. Isso permite que diferentes scaffolds de agentes executem a mesma tarefa sob as mesmas restrições.
• Serviços de Infraestrutura:
  • Serviços de Execução: Compila o código do agente contra instalações de bibliotecas alvo imutáveis.
  • Serviços de Recuperação: Permite a busca semântica restrita a versões específicas da biblioteca.
  • Isolamento de Workspace: Impõe acesso apenas de leitura às bibliotecas alvo e acesso de escrita a workspaces de rascunho (scratch).
• Eficiência Multi-Versão: O sistema utiliza armazenamento endereçável por conteúdo (hashing criptográfico) para deduplicar arquivos idênticos entre 67 versões diferentes da biblioteca, alcançando economia de recursos de ordem de magnitude em armazenamento e custos de embedding.

3. Construção do APE-Bench

O APE-Bench é um pipeline automatizado que extrai tarefas de engenharia de provas do histórico de commits reais da Mathlib.

• Processo: Ele filtra commits por modificações substantivas de nível de arquivo (5–100 linhas) e, em seguida, usa um agente para sintetizar instruções em linguagem natural a partir dos diffs.
• Validação: O pipeline garante que as tarefas sejam solucionáveis e que o patch original satisfaça a instrução gerada sob verificação dupla.
• Dataset: O lançamento inicial contém 100 tarefas extraídas de 67 commits (datados de 2026-01-01 em diante) para garantir zero contaminação de dados de treinamento para modelos de fronteira.

4. Scaffolds de Avaliação

O framework suporta a intercambialidade de scaffolds. Os autores fornecem o APE-Agent (um scaffold estilo ReAct com verificação integrada) e o avaliam junto ao Claude Code e Codex CLI para demonstrar que a infraestrutura pode comparar de forma justa diferentes implementações de agentes.

Principais Contribuições

1. Formulação e Benchmark de APE: A primeira infraestrutura completa para avaliação de engenharia de provas em escala de repositório, apresentando um pipeline automatizado (APE-Bench) que minera tarefas da evolução real de bibliotecas.
2. Benchmark de Validação por LLM Judge: Um dataset de 64 soluções de agentes anotadas por especialistas com classificações tridimensionais de qualidade (corretude semântica, alinhamento de requisitos, controle de escopo) para validar a confiabilidade de juízes LLM.
3. APE-Harness: Uma infraestrutura de execução baseada em contrato de tarefa que permite avaliação unificada entre diversos tipos de tarefas, suporta fluxos de trabalho funcionais (como síntese de instrução) e permite a intercambialidade de scaffolds.
4. APE-Agent: Um scaffold de caixa branca, estilo ReAct, com ferramentas integradas de sistema de arquivos e verificação para facilitar a pesquisa e comparação.
5. Serviços de Execução Multi-Versão: Implementação de serviços eficientes de compilação e recuperação através de múltiplas versões de biblioteca usando deduplicação de conteúdo.

Resultados

Desempenho dos Modelos

Os autores avaliaram modelos de fronteira (GPT-5.2, Gemini 3 Pro, Gemini 3 Flash) no APE-Bench, miniF2F e miniCTX usando um orçamento fixo de $3 por tarefa.

• Dificuldade do APE-Bench: A engenharia em escala de repositório provou ser significativamente mais difícil do que a provação isolada. No APE-Bench, o Gemini 3 Flash alcançou uma taxa de aprovação de 47,0%, superando o GPT-5.2 (27,0%) e o Gemini 3 Pro (24,0%).
• Comparação com Provação Isolada: No miniF2F e miniCTX, os modelos alcançaram taxas de aprovação muito mais altas (73–94%), indicando que a dificuldade no APE-Bench advém da complexidade da engenharia (coordenação, controle de escopo) e não da pura capacidade de prova de teoremas.
• Eficiência: As lacunas de desempenho foram impulsionadas pela eficiência de custo. O Gemini 3 Flash alcançou taxas de sucesso mais altas não por um raciocínio superior por turno, mas por evitar o esgotamento prematuro do orçamento causado por chamadas de ferramentas caras ou prompts verbosos.

Análise de Scaffold e Ferramenta

• Intercambialidade de Scaffold: O APE-Agent superou significativamente o Claude Code e o Codex CLI (por 15–23 pontos percentuais) em tarefas idênticas.
  • Razões: A verificação integrada do APE-Agent (edição atômica + compilação) reduziu chamadas redundantes. Em contraste, o Claude Code e o Codex incorreram em custos mais altos devido a prompts verbosos, chamadas de execução separadas e padrões de recuperação conservadores.
• Ablação de Ferramentas: A remoção de recuperação, shell ou operações de arquivo resultou em quedas de desempenho apenas marginais (faixa de 44–47%). Isso sugere que o principal gargalo são as capacidades de raciocínio dos modelos para tarefas de escala de repositório, não a disponibilidade de ferramentas específicas.

Confiabilidade do Juiz

O pipeline LLM-as-Judge demonstrou alta precisão (90,6% no total) em relação às anotações de especialistas humanos em dimensões de corretude semântica, alinhamento de requisitos e controle de escopo, validando seu uso para avaliação automatizada.

Eficiência da Infraestrutura

A deduplicação de conteúdo reduziu os requisitos de armazenamento de 67 versões de biblioteca de 480GB para 71GB (redução de 85%) e reduziu os custos de embedding para serviços de recuperação em 98,5% (\12,9K para \197).

Significância

O artigo afirma estabelecer uma base para a avaliação sistemática de agentes de IA em desenvolvimento de matemática formal em escala de repositório. Ao mudar o paradigma de avaliação da provação de teoremas isolados para a engenharia de provas, o APE-Bench aborda a lacuna entre as capacidades atuais de IA e as demandas reais de manutenção de bibliotecas formais de produção. O trabalho demonstra que:

1. A engenharia de provas em escala de repositório é uma tarefa distinta e significativamente mais desafiadora do que a provação de teoremas isolados.
2. A abstração de contrato de tarefa permite a comparação justa e padronizada de diversas arquiteturas de agentes.
3. Os modelos de fronteira atuais mostram promessa, mas enfrentam obstáculos substanciais em disciplina de engenharia, controle de escopo e eficiência de custo quando aplicados à manutenção de bibliotecas do mundo real.

Os autores liberam todo o código e o dataset do benchmark como código aberto para facilitar pesquisas adicionais neste domínio.