TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

O artigo apresenta o TaoBench, um novo benchmark derivado do livro "Analysis I" de Terence Tao que avalia a capacidade de generalização de provadores de teoremas automatizados para além do framework MathLib, revelando uma queda significativa de desempenho (cerca de 26%) quando os modelos enfrentam construções matemáticas personalizadas em vez de definições padrão.

O essencial

Imagine que você está aprendendo a cozinhar. Você passa anos estudando em uma escola famosa onde todos os pratos são feitos usando exatamente os mesmos ingredientes, as mesmas panelas e as mesmas receitas padronizadas. Você se torna um mestre nesses pratos específicos.

Agora, imagine que você vai trabalhar em um restaurante novo. O chefe diz: "Ótimo, você é um mestre! Mas aqui nós não usamos a panela 'Wok' padrão da escola. Nós usamos uma panela de ferro fundido feita à mão, e em vez de sal, usamos um tempero especial que só existe aqui. O prato é o mesmo (um frango assado), mas as ferramentas e os ingredientes são diferentes."

Se você tentar cozinhar o frango usando as mesmas técnicas que aprendeu na escola, vai falhar. Não porque você não sabe cozinhar frango, mas porque você não sabe como usar aquela panela específica ou como lidar com aquele tempero novo.

É exatamente isso que o artigo "TAOBENCH" descobriu sobre a Inteligência Artificial.

Aqui está a explicação simples do que os pesquisadores fizeram:

1. O Problema: A IA é "Muito Especializada"

Atualmente, os melhores programas de IA para provar teoremas matemáticos (como o DeepSeek-Prover ou Goedel-Prover) são treinados quase exclusivamente em uma biblioteca chamada MathLib.

• MathLib é como a "cozinha padrão" da matemática formal. É onde a maioria dos matemáticos e programadores trabalha.
• A IA aprendeu a resolver problemas incríveis nessa cozinha. Mas será que ela sabe cozinhar em outras cozinhas?

2. O Experimento: A Cozinha de Terence Tao

Os pesquisadores pegaram um livro de matemática famoso, Analysis I, escrito pelo lendário matemático Terence Tao.

• Tao escreveu o livro de uma forma muito particular. Ele construiu os conceitos matemáticos (como números, conjuntos e limites) do zero, usando suas próprias regras e definições, em vez de usar a biblioteca padrão (MathLib).
• É como se Tao tivesse escrito um livro de receitas usando apenas panelas de barro e temperos da sua própria horta, enquanto a IA foi treinada apenas com panelas de aço inox e temperos industriais.

3. O Teste: TAOBENCH

Os pesquisadores criaram um novo teste chamado TAOBENCH.

• Eles pegaram 150 exercícios do livro de Tao.
• Eles criaram duas versões de cada exercício:
  1. Versão Tao: O problema original, com as definições de Tao (a "panela de barro").
  2. Versão MathLib: O mesmo problema matemático, mas traduzido para a linguagem padrão que a IA conhece (a "panela de aço inox").

O objetivo era ver se a IA conseguia resolver o problema quando as ferramentas mudavam, mesmo que a matemática por trás fosse a mesma.

4. O Resultado Surpreendente

A IA funcionou muito bem na Versão MathLib (a cozinha que ela conhece). Mas, quando tentou resolver a Versão Tao (a cozinha nova), o desempenho caiu drasticamente, em média 26%.

O que isso significa?

• Não é que a IA ficou "burra" ou que o problema de Tao era mais difícil.
• O problema é que a IA aprendeu a decorar o caminho dentro da cozinha padrão, mas não aprendeu a pensar de forma flexível o suficiente para se adaptar a novas ferramentas.
• Quando as definições mudam (mesmo que o significado matemático seja o mesmo), a IA se perde. Ela não consegue generalizar o que aprendeu.

5. A Analogia do "Mapa vs. Bússola"

Pense na IA atual como alguém que tem um mapa muito detalhado de uma única cidade (MathLib). Se você a colocar naquela cidade, ela vai para qualquer lugar perfeitamente.
Mas, se você a colocar em uma cidade vizinha com ruas ligeiramente diferentes e nomes de ruas novos (o livro de Tao), ela fica confusa. Ela não tem uma bússola (capacidade de raciocínio geral) para navegar em ambientes desconhecidos; ela só sabe seguir o mapa que decorou.

Por que isso é importante?

Na pesquisa matemática real, os cientistas frequentemente criam novas definições e estruturas novas para explorar ideias que ainda não existem nos livros padrão.

• Se a IA só funciona bem no que já está "padronizado", ela não será útil para a ciência de ponta, onde a inovação acontece justamente fora do padrão.
• O TAOBENCH mostra que precisamos treinar as IAs para serem mais flexíveis, para que elas possam aprender a usar "panelas de barro" e "temperos novos" sem perder a capacidade de cozinhar.

Resumo final: A IA é um gênio em matemática, mas é um pouco "teimosa". Ela sabe resolver problemas incríveis, desde que as regras do jogo sejam exatamente as mesmas que ela viu durante o treinamento. O TAOBENCH nos diz que, para a IA ser uma verdadeira parceira na descoberta científica, ela precisa aprender a se adaptar a novas regras, não apenas a decorar as antigas.

Resumo técnico

1. O Problema

Os benchmarks atuais de Prova Automática de Teoremas (ATP) baseados em Grandes Modelos de Linguagem (LLMs) são quase exclusivamente construídos sobre o MathLib, a biblioteca matemática padrão para a linguagem de prova Lean 4. Isso cria um viés significativo: os modelos são treinados e avaliados dentro de um ecossistema definicional específico.

No entanto, a pesquisa matemática de ponta (frontier mathematics) é frequentemente exploratória e depende de construções ad hoc (sob medida) e definições personalizadas que se desviam das bibliotecas padrão. O artigo identifica uma lacuna crítica: os modelos ATP atuais conseguem generalizar para novos frameworks definicionais? A dificuldade observada em problemas fora do MathLib deve-se à complexidade matemática intrínseca ou à incapacidade do modelo de se adaptar a novas definições e notações?

2. Metodologia

Para investigar essa questão, os autores introduzem o TAOBENCH, um benchmark derivado da formalização em Lean do livro Analysis I de Terence Tao. A metodologia envolve três pilares principais:

• TAOBENCH (Framework de Tao): Um conjunto de 150 exercícios extraídos da formalização de Tao, que constrói conceitos centrais de análise (como números naturais, conjuntos e reais) a partir de princípios fundamentais, sem depender das definições do MathLib. O framework de Tao utiliza tipos indutivos personalizados, esquemas de nomenclatura diferentes e estruturas de namespaces específicas.
• TAOBENCHMATHLIB (Controle Emparelhado): Para cada problema no TAOBENCH, os autores criaram uma versão matematicamente equivalente traduzida para o framework do MathLib. Isso permite isolar o efeito do framework definicional da dificuldade matemática do problema.
• Pipeline Agente de Extração e Construção:
  • Extração de Contexto: Como os exercícios dependem de definições locais espalhadas por vários capítulos, os autores desenvolveram um pipeline agêntico (usando ferramentas como JiXia para análise estática e um verificador Lean) para extrair automaticamente um ambiente local compilável e autocontido para cada problema. Isso evita a necessidade de importar módulos externos e garante que o contexto seja fiel ao original.
  • Tradução e Verificação: Um pipeline automatizado (envolvendo GPT-5.1 com busca na web, verificação de compilação e verificação de equivalência) traduz os problemas de Tao para o MathLib. Um processo de verificação manual por especialistas garante a equivalência matemática entre as versões.

3. Principais Contribuições

1. TAOBENCH: O primeiro benchmark Lean projetado especificamente para medir a robustez da generalização além do MathLib, focando em um novo framework definicional.
2. TAOBENCHMATHLIB: Uma coleção de pares de problemas (Tao vs. MathLib) matematicamente equivalentes, permitindo uma avaliação controlada do impacto da mudança de framework.
3. Pipeline de Extração Agêntica: Uma metodologia escalável e de alta fidelidade para extrair contextos compiláveis de projetos Lean grandes e personalizados, além de gerar formalizações equivalentes em MathLib.
4. Análise de Generalização: Evidência empírica de que o desempenho dos modelos ATP cai drasticamente quando saem do domínio de treinamento (MathLib), mesmo com a matemática subjacente sendo idêntica.

4. Resultados

Os autores avaliaram vários modelos de ponta (SOTA), incluindo DeepSeek-Prover-V2, Goedel-Prover-V2 e Kimina-Prover, bem como modelos base (foundation models) como GPT-5.1 e Gemini 3 Pro.

• Queda de Desempenho: Enquanto os modelos performam bem no TAOBENCHMATHLIB (com taxas de sucesso frequentemente acima de 65-70%), o desempenho cai em média 26% no TAOBENCH (framework de Tao).
  • Exemplo: O modelo Goedel-Prover-V2-32B alcança 72,67% no MathLib, mas cai para 49,33% no TAOBENCH.
• Impacto do Comprimento do Contexto: A análise mostra que a queda de desempenho é severamente exacerbada pelo número de definições locais no contexto.
  • Para problemas sem definições locais ($n=0$), a diferença de desempenho é quase zero.
  • Para problemas com muitas definições locais ($n \ge 10$), a taxa de sucesso no TAOBENCH cai para cerca de 6,37%, enquanto no MathLib permanece em 53,43%.
• Modelos de Fronteira vs. Especialistas: Modelos de linguagem gerais (frontier models) que não são especializados em ATP, mas são bons em usar contexto, performam relativamente melhor no TAOBENCH do que os modelos especializados, sugerindo que a capacidade de aprender com exemplos in-context é mais valiosa do que o conhecimento prévio do MathLib para lidar com novos frameworks.
• Estudos de Caso:
  • Indução Reversa: O modelo falha no TAOBENCH porque precisa reconstruir lemas algébricos e de ordem localmente, enquanto no MathLib usa automação padrão.
  • Teorema do Confronto (Squeeze Theorem): A representação explícita de $\epsilon-\delta$ no TAOBENCH é mais fácil para alguns modelos do que a abstração baseada em filtros (Tendsto) do MathLib, mostrando que a "dificuldade" depende da representação, não da matemática.

5. Significado e Conclusão

O trabalho revela que o sucesso atual dos modelos ATP em benchmarks como MiniF2F ou PutnamBench é, em grande parte, um reflexo da familiaridade com o MathLib, e não necessariamente de uma capacidade robusta de raciocínio matemático generalizado.

• Limitação Fundamental: O treinamento atual em MathLib não transfere de forma confiável para formalismos desconhecidos, mesmo quando a matemática é equivalente.
• Implicação para Pesquisa: Para que os ATPs sejam úteis na matemática de pesquisa real (onde as definições mudam frequentemente), eles precisam ser treinados ou avaliados em ambientes que simulem essa variabilidade definicional.
• Futuro: O TAOBENCH serve como um teste concreto para alinhar futuros modelos de provadores com fluxos de trabalho matemáticos reais, onde a adaptação a novas definições é essencial.

Em resumo, o artigo demonstra que a "inteligência" matemática dos atuais LLMs é frágil e altamente dependente do ecossistema de definições em que foram treinados, apontando para a necessidade urgente de novos paradigmas de treinamento que priorizem a generalização definicional.