Resumo Técnico: MATHLIBPR – Um Benchmark para Preparação de Revisão de Bibliotecas Matemáticas Formais

1. Definição do Problema

O ecossistema de Lean e Mathlib tornou-se o padrão para raciocínio formal assistido por modelos de linguagem de grande escala (LLM), com sucessos recentes na resolução de problemas de nível olímpico (MiniF2F), matemática competitiva (AlphaProof) e projetos de formalização em larga escala (agente Gauss). No entanto, esses sistemas principalmente consumem o Mathlib como dependência, em vez de contribuir para ele. Embora o código gerado por LLMs possa ser verificado quanto à correção pelo kernel do Lean, determinar se uma contribuição está "pronta para mesclagem" — ou seja, aderindo às convenções da comunidade, mantendo a coerência da biblioteca e sendo adequada para manutenção de longo prazo — exige revisão humana.

A revisão humana é atualmente o principal gargalo para o crescimento do Mathlib, com um backlog de aproximadamente 300 pull requests (PRs) e tempos médios de espera de duas semanas. A questão central abordada por este artigo é: Os LLMs podem ajudar a revisar PRs do Mathlib? Especificamente, eles conseguem distinguir entre código que passa na compilação e está pronto para integração e código que passa na compilação mas requer revisão ou será rejeitado?

2. Metodologia

2.1 Construção do Conjunto de Dados: MATHLIBPR

Os autores apresentam o MATHLIBPR, um benchmark construído a partir de históricos reais de PRs do Mathlib4.

• Fonte: PRs fechados do repositório leanprover-community/mathlib4 (até 5 de abril de 2026).
• Critérios de Seleção: O benchmark foca exclusivamente em snapshots que passam na compilação. Isso elimina estratégias triviais baseadas em erros de sintaxe ou falhas de compilação, forçando os modelos a julgarem com base na qualidade do código e nas convenções.
• Rótulos:
  • Pronto para Mesclagem: Snapshots aceitos na branch master.
  • Não Pronto para Mesclagem: Snapshots que passaram nos testes de compilação, mas foram revisados antes da aceitação ou pertenciam a PRs que nunca foram mesclados.
• Composição: O conjunto de dados final contém 15.895 snapshots rotulados de 12.063 PRs (11.409 prontos para mesclagem, 4.486 não prontos para mesclagem). Inclui 3.687 pares dentro do PR (um snapshot anterior que passa na compilação versus a versão final aceita) para testar o reconhecimento do progresso de revisão.

2.2 Protocolo de Avaliação

Os autores propõem um protocolo de avaliação em três estágios que fornece progressivamente contexto mais rico aos modelos:

• Estágio 1: Evidência local do código (diff, arquivos alterados) e resumos compactos das diretrizes do Mathlib (nomeação, estilo, documentação).
• Estágio 2: Adiciona diagnósticos estruturados (linting, imports, posicionamento de declarações, adequação à API) derivados de registros históricos de verificações do GitHub ou preenchidos localmente.
• Estágio 3: Adiciona título e descrição do PR como intenção declarada.

2.3 Sistemas Avaliados

O benchmark avalia duas classes de sistemas:

1. Modelos LLM: DeepSeek-R1-Distill-Qwen, Qwen3-8B, Goedel-Prover-V2-32B (pré-ajustado no Mathlib) e Kimina-Prover-Distill-8B.
2. Agentes LLM: Codex (GPT-5.4) e Claude Code (Claude Sonnet 4.6). Os agentes operam em uma cópia local de repositório somente leitura, restritos de editar arquivos, acessar a web ou recuperar resultados de PRs.

2.4 Esquema de Saída e Métricas

Os sistemas são obrigados a emitir uma revisão estruturada em JSON, em vez de texto livre. O esquema inclui:

• Veredito: merge_ready, not_merge_ready ou uncertain.
• Pontuação: Uma pontuação escalar de prontidão para mesclagem ($p_{merge\_ready}$).
• Eixos: Avaliações em oito dimensões de rubrica (nomeação, documentação, estrutura local, posicionamento de arquivos, imports, legibilidade de provas, adequação à API, sobreposição de repositório).

Métricas:

• Recall MR/NMR: Recall para as classes pronto para mesclagem e não pronto para mesclagem (tratando uncertain e saídas inválidas como erros).
• Acurácia Balanceada: Média do recall MR e NMR.
• Taxa de Saída Válida: Porcentagem de saídas válidas conforme o esquema dentro dos orçamentos de tempo de execução.
• AUROC: Área sob a curva ROC baseada em pontuações escalares.

3. Resultados Principais

3.1 Desempenho Geral

• Baixa Acurácia: Nenhum sistema distingue de forma confiável snapshots prontos para mesclagem de snapshots não prontos para mesclagem. O modelo de melhor desempenho (DeepSeek) alcançou uma Acurácia Balanceada de 36,0% no Estágio 3, significativamente abaixo da linha de base de 50% de chance para uma tarefa balanceada (embora o conjunto de dados seja desbalanceado, as métricas de recall destacam a falha).
• Assimetria de Classes: Os sistemas exibem um forte viés em direção à previsão de merge_ready.
  • DeepSeek (Estágio 3): 69,8% de Recall MR, mas apenas 2,3% de Recall NMR.
  • Qwen (Estágio 3): 48,3% de Recall MR, 0,0% de Recall NMR.
  • Codex (Agente): 92,0% de Recall MR, mas apenas 12,0% de Recall NMR.
• Impacto do Contexto: Adicionar diagnósticos e intenção do PR (Estágios 2 e 3) produziu ganhos limitados e desiguais. Por exemplo, a acurácia balanceada do DeepSeek melhorou de 18,1% para 36,0%, mas sua capacidade de identificar código não pronto para mesclagem permaneceu próxima de zero.

3.2 Desempenho Agente vs. Modelo

• Agentes: Embora o Codex tenha mostrado alta confiabilidade operacional (99,9% de taxa de saída válida) e alto Recall MR, ele falhou em identificar código não pronto para mesclagem. O Claude Code teve menor confiabilidade (56,4% de taxa válida) e recall NMR igualmente pobre.
• Modelos Especializados: Goedel e Kimina, apesar de treinados em provas formais, tiveram desempenho ruim. A taxa de saída válida do Goedel colapsou de 68,3% (Estágio 1) para 13,5% (Estágio 3), e ambos os modelos frequentemente produziram saídas inválidas (prosa ou blocos de código) em vez do esquema JSON exigido.

3.3 Análise Dentro do PR

Em uma comparação controlada de snapshots anteriores que passam na compilação versus snapshots finais aceitos do mesmo PR:

• Os modelos mal superaram o acaso. A acurácia em pares do DeepSeek estagnou em 51,1% (Estágio 3), e o Qwen permaneceu próximo de 49,1%.
• Isso indica que os modelos não conseguem detectar de forma confiável as melhorias específicas que levaram à aceitação de um PR, mesmo ao comparar duas versões da mesma contribuição.

3.4 Análise de Erros

• Abstenção: Os sistemas frequentemente abstenham-se (uncertain) nos eixos de documentação ou legibilidade de provas.
• Saídas Inválidas: Uma parte significativa das saídas de modelos especializados (Goedel, Kimina) e agentes (Claude Code) foi inválida devido a violações de esquema, tempos esgotados ou falha em produzir JSON. Isso sugere uma incompatibilidade entre os objetivos de treinamento dos modelos (prova de teoremas) e a interface estruturada de revisão.

4. Contribuições

1. Benchmark MATHLIBPR: O primeiro benchmark para avaliar LLMs na prontidão para mesclagem de contribuições do Mathlib que passam na compilação, derivado de históricos reais de PRs.
2. Protocolo de Avaliação em Estágios: Um protocolo que testa sistematicamente se um contexto mais rico (diagnósticos, intenção do PR) melhora o julgamento semelhante ao de um revisor.
3. Estudo Empírico: Uma avaliação abrangente mostrando que LLMs e agentes atuais lutam para distinguir código pronto para mesclagem de código que passa na compilação mas requer revisão, destacando uma lacuna entre a correção do código e a qualidade de integração na biblioteca.

5. Significado e Afirmações

O artigo afirma que o MATHLIBPR fornece um passo em direção a assistentes de revisão e modelos de recompensa para bibliotecas matemáticas formais.

• Estado Atual: Os resultados demonstram que julgar a prontidão para mesclagem é uma capacidade substancialmente mais difícil do que detectar erros de sintaxe ou falhas de compilação. Os sistemas atuais falham em capturar as normas de revisão sutis necessárias para curar uma biblioteca matemática integrada.
• Utilidade Futura: O benchmark destina-se a ser usado para:
  • Assistência ao Revisor: Triagem e destaque de prováveis bloqueios para revisores humanos.
  • Modelagem de Recompensa: Treinar modelos de recompensa usando a estrutura de pares dentro do PR (preferindo o snapshot final aceito sobre um anterior que passa na compilação) para orientar LLMs a gerar código que não apenas seja correto, mas também mantível e pronto para mesclagem.
• Limitações: Os autores reconhecem que o benchmark cobre uma fatia seletiva da história dos PRs e que os rótulos são derivados de decisões históricas de mantenedores, que podem incluir fatores não técnicos. Eles afirmam explicitamente que o objetivo não é substituir revisores humanos, mas fornecer um sinal consultivo.

Em conclusão, embora os LLMs tenham tido sucesso em gerar provas corretas, a transição para contribuir com o Mathlib exige um nível de julgamento sobre estilo de código, documentação e adequação à biblioteca que os modelos atuais ainda não dominaram. O MATHLIBPR estabelece a linha de base para medir o progresso nessa direção.