LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

O artigo apresenta o LeanCat, um conjunto de benchmarks desafiador para a teoria de categorias em Lean, que revela uma lacuna significativa na capacidade de raciocínio abstrato dos modelos de linguagem atuais e demonstra que a recuperação dinâmica de bibliotecas combinada com refinamento iterativo é essencial para superar essas limitações.

O essencial

Imagine que você está tentando ensinar um supercomputador (uma Inteligência Artificial) a ser um matemático de elite. Até agora, esses computadores eram ótimos em resolver quebra-cabeças de lógica simples ou fazer contas de cabeça rápidas. Mas o mundo real da matemática avançada não é sobre quebra-cabeças; é sobre construir edifícios inteiros usando blocos de Lego que já existem, onde cada bloco tem uma função muito específica e complexa.

Este artigo apresenta o LeanCat, um novo "teste de estresse" para essas IAs, focado em uma área chamada Teoria das Categorias.

Aqui está a explicação simplificada, usando analogias do dia a dia:

1. O Problema: O "Abismo da Abstração"

Pense na matemática como uma biblioteca gigante.

• Os testes antigos (como miniF2F): Eram como pedir para a IA resolver um problema de matemática do ensino médio. A IA precisava apenas de "truques rápidos" ou memória para acertar. Era como pedir para alguém montar um quebra-cabeça de 50 peças.
• O novo teste (LeanCat): É como pedir para a IA projetar um arranha-céu, mas ela não pode usar apenas os blocos que ela "decorou". Ela precisa saber onde encontrar os blocos certos na biblioteca gigante (chamada Mathlib), entender como eles se encaixam e montar a estrutura inteira sozinha.

O que aconteceu?
Quando os pesquisadores testaram as melhores IAs do mundo (como o GPT-5 e o Claude) nesse novo teste, elas falharam miseravelmente em problemas difíceis.

• Em problemas fáceis, elas acertaram cerca de 55%.
• Em problemas difíceis? 0%.
  Isso mostra que as IAs são ótimas em "chutar" a resposta, mas péssimas em navegar por uma biblioteca complexa e conectar ideias abstratas de forma consistente. Elas se perdem no meio do caminho.

2. A Solução: O "Detetive LeanBridge"

Como as IAs estavam travando, os autores criaram um novo agente chamado LeanBridge.

Imagine que a IA normal é um estudante que tenta resolver um problema sozinho, sem consultar o professor ou o livro, apenas tentando adivinhar.
O LeanBridge é como um estudante que tem um assistente de pesquisa.

• O Ciclo Mágico: O LeanBridge funciona em um loop de três passos:
  1. Pesquisar: Antes de tentar provar algo, ele vai à biblioteca digital e procura definições e teoremas que podem ajudar.
  2. Gerar: Ele tenta escrever a prova usando o que achou.
  3. Verificar: Ele tenta "compilar" a prova. Se der erro (e vai dar, porque é difícil), ele lê o erro, volta à biblioteca para buscar mais informações e tenta de novo.

O Resultado:
Com esse "assistente", a taxa de sucesso dobrou! A IA conseguiu resolver problemas que antes eram impossíveis para ela. Isso prova que, para matemática complexa, a IA não precisa apenas ser "mais inteligente" (ter mais dados), ela precisa saber como usar as ferramentas e a biblioteca corretamente.

3. Por que isso importa?

A Teoria das Categorias é a "língua franca" da matemática moderna. É usada para conectar áreas totalmente diferentes (como física, computação e biologia) através de estruturas comuns.

• Para a IA: Este teste mostra que para avançar, as IAs precisam aprender a ser "engenheiras de conhecimento", não apenas "calculadoras". Elas precisam saber navegar em bibliotecas de código e conceitos, não apenas memorizar fórmulas.
• Para a Matemática: O LeanCat ajuda a encontrar onde a biblioteca de matemática formal (Mathlib) está incompleta. Se a IA não consegue provar algo, pode ser porque falta uma "peça de Lego" na biblioteca que os humanos precisam criar.

Resumo em uma frase

O artigo diz: "As IAs atuais são ótimas em quebra-cabeças simples, mas falham em matemática complexa porque não sabem usar a biblioteca de ferramentas. Quando damos a elas um 'assistente de pesquisa' que as ajuda a buscar e verificar informações passo a passo, elas finalmente conseguem construir pontes entre ideias abstratas."

O LeanCat é o novo campo de treinamento onde vamos ver se as IAs estão prontas para se tornar verdadeiros parceiros na pesquisa matemática do futuro.

Resumo técnico

Resumo Técnico: LEANCAT

1. O Problema: A Lacuna de Abstração em Provas Formais

O artigo identifica uma limitação crítica nos atuais benchmarks de prova de teoremas formais assistidos por Inteligência Artificial (IA). Embora modelos de linguagem grandes (LLMs) tenham demonstrado capacidades impressionantes em matemática de nível olímpico ou cálculo (como em miniF2F ou ProofNet), eles falham em raciocínio baseado em abstrações de bibliotecas (library-grounded abstraction).

• A Deficiência Atual: Os benchmarks existentes tendem a recompensar "truques" inteligentes de curto prazo ou computação algébrica, em vez de exigir trabalho sustentado dentro de estruturas abstratas complexas e reutilizáveis.
• O Desafio da Teoria das Categorias: A teoria das categorias é apresentada como o "estresse-teste" definitivo para esse tipo de raciocínio. Ela exige o uso de interfaces de alto nível (funtores, transformações naturais, adjunções, limites/colimites) e raciocínio diagramático, onde o sucesso depende da capacidade de navegar em grandes bibliotecas de definições e composições, e não apenas de uma única ideia brilhante.
• A Lacuna de Abstração: Os modelos atuais sofrem de uma "lacuna de abstração", onde o desempenho colapsa drasticamente à medida que a dificuldade aumenta, falhando em generalizar composicionalmente em domínios abstratos.

2. Metodologia e Design do Benchmark (LeanCat)

Os autores introduzem o LeanCat, um conjunto de benchmark composto por 100 problemas de teoria das categorias totalmente formalizados em Lean 4 (utilizando a biblioteca Mathlib).

• Estrutura dos Dados:
  • Fontes: Problemas extraídos de livros-texto padrão (Category Theory in Context, Categories for the Working Mathematician) e artigos de pesquisa.
  • Escopo: Os problemas cobrem oito clusters temáticos, desde propriedades básicas de categorias até estruturas avançadas como Categorias Abelianas e Monads.
  • Nível de Dificuldade: Os problemas são classificados em Fácil, Médio e Difícil. A classificação utiliza um pipeline híbrido:
    1. Avaliação por LLM: Modelos tentam provar os problemas; a dificuldade é calculada com base na taxa de sucesso.
    2. Avaliação Humana: Matemáticos especialistas com experiência em Lean atribuem notas baseadas na complexidade da prova e na necessidade de lemas intermediários.
  • Formato: É um benchmark de nível de declaração (statement-level), onde o modelo deve provar um teorema isolado sem lemas intermediários fornecidos, forçando o modelo a gerenciar definições e abstrações autonomamente.

3. Abordagem Experimental e Agentes

O estudo compara duas estratégias de inferência:

1. Baselines Estáticos (Amostragem Paralela):

   • Modelos de ponta (GPT-5.2, Claude-Opus-4.5, DeepSeek-Prover-V2, etc.) recebem apenas a declaração formal do teorema.
   • Métrica: Pass@k (o problema é considerado resolvido se qualquer uma das $k$ tentativas for bem-sucedida).
   • Inclui tanto modelos generalistas quanto provadores especializados treinados especificamente para matemática formal.

2. LeanBridge (Agente com Augmentação por Recuperação):

   • Um agente autônomo que implementa um loop dinâmico de Recuperar-Generar-Verificar (retrieve–generate–verify).
   • Mecanismo: O agente consulta ativamente a biblioteca Mathlib (via LeanExplore) para encontrar definições e lemas relevantes antes e durante a geração da prova.
   • Iteração: O sistema analisa mensagens de erro do compilador Lean, refina a busca e tenta novamente (até 4 iterações).
   • Configurações: Testado com entrada apenas em linguagem natural (NL) e com entrada combinada (NL + Declaração Formal).

4. Resultados Principais

• Desempenho dos Baselines (A Lacuna Confirmada):

  • O desempenho geral é baixo. O melhor modelo estático (Claude-Opus-4.5) alcança apenas 12,0% de sucesso em Pass@4.
  • Colapso de Desempenho: Há uma queda drástica conforme a dificuldade aumenta:
    • Fácil: ~55%
    • Médio: ~2,5%
    • Difícil: 0,0%
  • Provedores especializados (como DeepSeek-Prover-V2) falham em generalizar, obtendo 0% em tarefas Médias e Difíceis, indicando overfitting em dados de treinamento de nível olímpico/undergraduate.

• Desempenho do LeanBridge:

  • O agente com recuperação dinâmica dobra o desempenho dos melhores baselines estáticos, alcançando 24,0% de sucesso no total.
  • Superação da Lacuna: O LeanBridge é o único método capaz de resolver problemas de alta dificuldade (atingindo 2,5% em tarefas Difíceis), onde todos os baselines falharam completamente.
  • Importância da Declaração Formal: A configuração que inclui a declaração formal (NL+Statement) supera significativamente a configuração apenas com linguagem natural, especialmente em tarefas Médias e Difíceis, demonstrando que definições formais atuam como âncoras essenciais para o planejamento de longo prazo.

• Análise de Falhas:

  • As falhas não são apenas sintáticas. Os principais modos de falha incluem:
    1. Falha Matemática: Estratégia incorreta (ex: tentar provar existencial com um conjunto vazio).
    2. Alucinação: Invocação de lemas ou constantes que não existem na biblioteca.
    3. Falha "Preguiçosa" (Lazy): O modelo tenta usar placeholders ou inferências automáticas em vez de construir lemas intermediários necessários que não estão na biblioteca.
    4. Hack: Alterar o significado formal do teorema para torná-lo trivialmente provável.

5. Contribuições e Significado

• Novo Benchmark (LeanCat): O primeiro conjunto de dados dedicado à teoria das categorias formalizada, servindo como um teste rigoroso para o raciocínio estrutural e de interface de alto nível.
• Validação da Necessidade de Recuperação Dinâmica: O estudo prova empiricamente que, em domínios abstratos, a simples escala de amostragem (scaling up sampling) ou o treinamento especializado não são suficientes. A recuperação iterativa de bibliotecas e o refinamento são necessidades estritas para o raciocínio neuro-simbólico eficaz.
• Impacto na Pesquisa de IA: O LeanCat estabelece um novo patamar para avaliar a capacidade de modelos de IA de navegar em grandes bases de conhecimento matemático, sugerindo que o futuro da prova formal reside em agentes que interagem dinamicamente com bibliotecas, e não apenas em modelos estáticos.
• Impacto na Matemática: O benchmark ajuda a identificar lacunas na biblioteca Mathlib e áreas onde a formalização ainda é elusiva para humanos e máquinas.

Em suma, o artigo demonstra que a prova de teoremas em matemática avançada e abstrata exige uma mudança de paradigma: de modelos que "adivinham" provas para agentes que navegam, recuperam e compõem conhecimento estrutural de bibliotecas formais.