SorryDB: Can AI Provers Complete Real-World Lean Theorems?

O artigo apresenta o SorryDB, um benchmark dinâmico e atualizado de tarefas reais em Lean extraídas de projetos do GitHub para avaliar e alinhar provadores de IA às necessidades da comunidade, demonstrando que abordagens atuais, como modelos de linguagem, agentes e provadores simbólicos, são complementares em vez de uma ser estritamente superior às outras.

O essencial

Imagine que você está construindo uma cidade de Lego gigante, chamada Lean. Nessa cidade, os arquitetos (matemáticos) escrevem regras e constroem prédios (teoremas) que provam coisas incríveis, como "o círculo é redondo" ou "o número 2 é primo".

Mas, às vezes, um arquiteto chega em um prédio, diz: "Eu sei como esse prédio deve ficar, mas estou com pressa e não tenho tempo de colocar os tijolos finais agora". Então, ele deixa um espaço vazio marcado com um adesivo escrito "Sorry" (Desculpe, vou terminar depois).

Agora, imagine que temos robôs (Inteligências Artificiais) que prometem terminar esses prédios para os arquitetos. O problema é: como sabemos se esses robôs são bons de verdade?

O Problema: As Provas de Condução Falsas

Até agora, para testar esses robôs, os cientistas usavam "provas de condução" muito específicas e antigas, como resolver quebra-cabeças de matemática de Olimpíadas (como o Putnam ou a IMO).

O problema é que:

1. São muito fáceis para os robôs hoje: Os robôs já "decoraram" essas provas antigas. É como se você estivesse testando a direção de um piloto em uma pista que ele já percorreu 100 vezes. Ele não está realmente dirigindo; está apenas lembrando a rota.
2. Não refletem a vida real: Na vida real, construir matemática é bagunçado. Você precisa usar peças de outros prédios, lidar com erros de compilação e entender contextos complexos. As provas antigas não testam isso.

A Solução: O "SorryDB" (O Banco de Dados de Desculpas)

Os autores deste paper criaram algo novo chamado SorryDB. Em vez de usar provas antigas, eles foram até o "GitHub" (o local onde os projetos de código são guardados) e pegaram 78 projetos reais que estão sendo construídos agora.

Eles coletaram todos os adesivos "Sorry" que os matemáticos deixaram para trás.

• Analogia: Imagine que, em vez de testar um mecânico em um carro de brinquedo de plástico, você pega 1.000 carros reais que estão na oficina com o capô aberto e diz: "Conserte este problema específico".
• O SorryDB é um banco de dados vivo. Ele se atualiza constantemente. Assim que os robôs resolvem um problema, os matemáticos deixam um novo, mais difícil. É um "tiro de meta" que se move para frente, impedindo que os robôs apenas decorem as respostas.

O Grande Teste: Quem é o Melhor Mecânico?

Os autores pegaram 1.000 desses problemas "pendentes" e testaram vários tipos de robôs:

1. Robôs Gerais: Modelos de IA comuns (como GPT, Claude, Gemini) que sabem de tudo um pouco.
2. Robôs Especialistas: IAs treinadas especificamente para matemática.
3. Robôs com "Auto-Correção": IAs que tentam, erram, leem o erro e tentam de novo.
4. Agentes: IAs que podem "olhar" em bibliotecas de peças (ferramentas de busca) para achar a peça certa antes de tentar montar.

O Que Eles Descobriram?

Os resultados foram surpreendentes e ensinaram lições importantes:

• A "Memória" não é tudo: Os robôs que apenas "chutam" a resposta de primeira (pass@1) falharam muito.
• O Poder do "Tente de Novo": Os robôs que conseguiam ler o erro do computador, entender onde erraram e tentar de novo (abordagem iterativa ou "agente") foram muito melhores.
  • Analogia: É como um aluno que faz a prova, vê que errou a conta, pega a calculadora, refaz e só então entrega. Esse aluno passa. O aluno que chuta e entrega na primeira tentativa reprovou.
• Nenhum Robô é o "Super-Homem": Não existe um único robô que resolve tudo.
  • Um robô é ótimo em problemas de lógica pura.
  • Outro é ótimo em encontrar peças em bibliotecas gigantes.
  • Outro é ótimo em corrigir seus próprios erros.
  • Conclusão: O melhor sistema é uma equipe onde cada robô faz o que sabe fazer melhor. Juntos, eles resolveram 35% dos problemas, enquanto o melhor robô sozinho resolveu apenas 30%.

Por que isso importa?

O SorryDB mostra que a Inteligência Artificial para matemática não está apenas "decorando" provas antigas. Ela está começando a aprender a trabalhar de verdade, em ambientes bagunçados e complexos, ajudando os humanos a construir o futuro da matemática.

É como se, antes, estivessem testando robôs em um videogame fácil. Agora, com o SorryDB, eles estão jogando no modo "Realidade" com o capô aberto, e os robôs estão finalmente começando a aprender a mexer nas ferramentas de verdade.

Resumo técnico

Resumo Técnico: SORRYDB

1. O Problema

O campo de provadores de teoremas automatizados (ATP) enfrenta três limitações críticas nos benchmarks atuais:

1. Saturação e Vazamento de Dados: Os conjuntos de dados existentes (como miniF2F e PutnamBench) baseiam-se em problemas de competições matemáticas (Olimpíadas). Esses conjuntos estão saturados, e as soluções frequentemente vazaram para os dados de treinamento de modelos de linguagem (LLMs), dificultando a distinção entre raciocínio geral e memorização.
2. Desalinhamento com a Realidade: Problemas de competição são frequentemente isolados e não refletem os desafios do mundo real da formalização matemática, que envolvem dependências complexas de bibliotecas, contexto de projeto específico e "bagunça" de desenvolvimento de software.
3. Falta de Utilidade Prática: Não há uma métrica robusta para avaliar a capacidade de um agente de contribuir para projetos de formalização matemática em andamento, onde o objetivo é preencher lacunas em teoremas não totalmente provados.

2. Metodologia: O Dataset SORRYDB

Os autores propõem o SORRYDB, um benchmark dinâmico e em atualização contínua, inspirado no SWE-bench (para engenharia de software), mas focado em provadores de teoremas.

Coleta e Extração

• Fonte: O dataset é extraído de 78 repositórios ativos no GitHub que utilizam o provador interativo Lean 4.
• Critério de Seleção: Projetos são considerados ativos se tiverem pelo menos um commit nos últimos três meses.
• Mecanismo de Extração: O sistema identifica e extrai todas as ocorrências da palavra-chave sorry no código Lean. No Lean, sorry é um placeholder usado por desenvolvedores para marcar teoremas ou passos intermediários que ainda não foram provados, permitindo que o projeto compile enquanto o trabalho continua.
• Tarefa Definida: O desafio é "preencher o sorry" (fill-in-the-sorry). O modelo deve fornecer o código que substitui o sorry para completar a prova específica, sem necessariamente provar o teorema inteiro se houver múltiplos sorrys.
• Validação: A correção é verificada deterministicamente tentando compilar o projeto com a nova prova. Se o código compilar e o sorry for removido (sem erros de tipo), a tarefa é considerada resolvida.

Estrutura do Dataset

O dataset inicial (SORRYDB-2601) contém 5.663 tarefas, das quais um snapshot de 1.000 tarefas foi selecionado para avaliação, garantindo diversidade de repositórios e recência (baseado na data do git blame). As tarefas são categorizadas em:

• Pedagógico: Tutoriais e materiais de ensino.
• Ferramentas (Tooling): Utilitários e desenvolvimento de ferramentas Lean.
• Benchmark: Problemas de competições (ex: Putnam).
• Bibliotecas: Bibliotecas matemáticas reutilizáveis (ex: Mathlib).
• Formalização: Projetos de formalização de teoremas específicos (ex: Teorema de Fermat, Teorema de Carleson).

3. Contribuições Principais

1. Dataset Dinâmico e Realista: Criação de um benchmark que reflete o uso diário de um desenvolvedor Lean, evitando a saturação ao focar em tarefas não resolvidas em projetos ativos.
2. Framework de Validação Automatizada: Um pipeline que clona repositórios, substitui o sorry pela proposta do modelo e verifica a compilação e o estado da prova, eliminando a necessidade de rótulos manuais.
3. Avaliação Comparativa Abrangente: Análise de diversas abordagens, desde táticas determinísticas até LLMs generalistas, modelos especializados e arquiteturas agênticas.

4. Resultados Experimentais

Os autores avaliaram 1.000 tarefas do snapshot SORRYDB-2601 com diversas abordagens:

Desempenho por Categoria de Modelo

• Táticas Determinísticas: Táticas simples (trivial, ring, linarith) e automatizadas (grind, simp) resolveram cerca de 8,4% das tarefas.
• LLMs Generalistas (Pass@1): Modelos como Gemini Flash 3 e Claude Opus 4.5 alcançaram taxas de sucesso entre 6,2% e 11,0% em uma única tentativa.
• Modelos Especializados: Modelos treinados especificamente para provas (ex: Goedel Prover V2, Kimina Prover) tiveram desempenho inferior aos generalistas no contexto de "preencher sorry" (ex: Goedel em 2,7% pass@1), possivelmente devido a incompatibilidade de versões do Lean ou foco excessivo em competições.
• Abordagens Iterativas e Agênticas (O Grande Diferencial):
  • Modelos com Auto-correção (Self-Correcting) e abordagens Agênticas (que usam ferramentas de busca e feedback de erro) superaram significativamente as abordagens de "passagem única" (one-shot).
  • O Gemini Flash 3 (Agêntico) alcançou 30,3% de sucesso.
  • O Claude Opus 4.5 (Auto-correção) alcançou 27,1%.
  • Conclusão Chave: O acesso ao ambiente do projeto e o feedback de compilação (erros de build) são mais valiosos do que um orçamento de raciocínio maior ou fine-tuning em dados estáticos.

Complementaridade

• A análise de sobreposição (Upset Plot) mostrou que os provadores são complementares. Um modelo forte em uma categoria (ex: Goedel em benchmarks) falha em outras onde um modelo mais fraco ou uma tática simples tem sucesso.
• A combinação de todos os provadores resolveu 35,7% das tarefas, indicando que nenhum modelo único domina todas as situações.

Análise de Falhas

• Dependência de Ferramentas: Modelos agênticos que dependem excessivamente de ferramentas de busca de biblioteca às vezes falham em construir provas do zero quando a biblioteca não possui o lema exato (ex: exemplo do movimento browniano).
• Versão do Lean: Modelos especializados treinados em versões antigas do Lean tiveram desempenho prejudicado pela incompatibilidade de versão.

5. Significado e Impacto

O trabalho do SORRYDB representa um avanço significativo na avaliação de IA para matemática formal:

• Mudança de Paradigma: Move o foco de "resolver problemas de olimpíada" para "contribuir com projetos de pesquisa reais".
• Resiliência à Contaminação: Por ser dinâmico e focado em tarefas não resolvidas em repositórios ativos, o benchmark é resistente à contaminação de dados de treinamento, oferecendo uma métrica mais justa para o progresso futuro.
• Direção para Agentes Autônomos: Os resultados sugerem que o futuro dos provadores de teoremas não reside apenas em modelos de linguagem maiores, mas em agentes iterativos capazes de interagir com o ambiente de desenvolvimento, compilar código e corrigir erros com base no feedback do kernel do Lean.
• Utilidade Prática: O dataset demonstra que a utilidade prática de um provador depende da sua capacidade de navegar em contextos locais complexos e dependências de bibliotecas, algo que os benchmarks estáticos atuais não capturam adequadamente.

Em resumo, o SORRYDB estabelece um novo padrão para avaliar a capacidade de IA de atuar como um colaborador real na matemática formal, destacando que a interação iterativa com o ambiente de prova é a chave para o sucesso em cenários do mundo real.