Lean-GAP: A Dataset of Formalized Graduate Algebra Problems

Resumo Técnico do LEAN-GAP: Um Conjunto de Dados de Problemas de Álgebra de Graduação Formalizados

Problema
Apesar dos avanços significativos no raciocínio automatizado e em modelos de linguagem de grande escala (LLMs), permanece uma lacuna substancial entre o conhecimento matemático informal e suas contrapartes formais em assistentes de prova como o Lean 4. Embora esforços recentes tenham formalizado com sucesso problemas de estilo competição ou teoremas altamente especializados, há uma escassez de conjuntos de dados representativos e estruturados que cubram o material padrão de nível de pós-graduação. Essa falta de dados curriculares fundamentais prejudica o desenvolvimento de sistemas de raciocínio automatizado, pois eles são frequentemente treinados em "problemas desafiadores" sem o desenvolvimento conceitual sistemático encontrado em livros didáticos padrão. Além disso, embora a autoformalização tenha progredido, verificar se uma afirmação formal gerada captura fielmente o significado pretendido de uma afirmação informal continua sendo um gargalo crítico e não resolvido.

Metodologia
Os autores apresentam o LEAN-GAP (Lean-Graduate Algebra Problems), um conjunto de dados derivado de 430 exercícios formalizados do livro Abstract Algebra, de Dummit e Foote. O projeto emprega um pipeline escalável de três estágios:

1. Pré-processamento PDF-para-LATEX: Páginas de PDF digitalizadas do livro didático são renderizadas como imagens, recortadas para remover elementos estranhos e processadas via API Mathpix Convert para gerar transcrições iniciais de LATEX das afirmações dos exercícios.
2. Autoformalização LATEX-para-Lean: Uma abordagem baseada em prompts utilizando vários LLMs traduz as afirmações em LATEX para código Lean 4. Os prompts impõem convenções de nomenclatura consistentes (ex: DF_{sec}_{subsec}_{exercise_num}), compatibilidade com o Mathlib e a inclusão de placeholders sorry para provas. Os autores avaliaram seis sistemas: cinco modelos de disparo único (GPT-5, Gemma4-31B, Goedel-Formalizer-V2-32B, Qwen3.6-35B-A3B, DeepSeek-R1-Distill-Qwen-32B) e um loop de agente iterativo (Codex).
3. Verificação da Correspondência Informal–Formal: Reconhecendo que a compilação bem-sucedida não garante a correção semântica, os autores implementaram um fluxo de trabalho rigoroso de verificação com participação humana (human-in-the-loop).
   • Fase do Contribuidor: Um contribuidor reescreve o exercício como uma afirmação de teorema autossuficiente, formaliza-o em Lean e envia um Pull Request (PR).
   • Verificação Automatizada: O GitHub CI verifica se o código Lean elabora contra uma revisão fixa do Mathlib.
   • Revisão do Mantenedor: Um mantenedor independente realiza uma revisão semântica, garantindo que a declaração em Lean capture o conteúdo matemático da afirmação informal.
   • Correção Assistida por IA: Ferramentas como Claude Opus 4.7 e Aristotle são utilizadas como "segundos leitores" para detectar erros semânticos sutis, como quantificadores invertidos ou restrições ausentes (ex: $n \ge 2$) que os revisores humanos podem inicialmente negligenciar.

Principais Contribuições

1. O Conjunto de Dados LEAN-GAP: Um corpus estruturado de 430 exercícios de álgebra de graduação formalizados, organizados por tópico e dificuldade, cobrindo teoria de grupos, teoria de anéis, teoria de corpos e teoria de Galois.
2. Pipeline de Formalização Sistemática: Uma metodologia reproduzível para converter exercícios de livros didáticos em afirmações formais, destacando a necessidade de supervisão humana na etapa de verificação.
3. Análise de Desafios de Formalização: Um exame detalhado de gargalos recorrentes, incluindo:
   • Argumentos geométricos: Exercícios envolvendo construções com régua e compasso são difíceis de formalizar devido à falta de uma infraestrutura geométrica robusta no Mathlib.
   • Formalização com resposta embutida: Problemas que exigem a enumeração de soluções apresentam desafios ao distinguir entre verificar uma resposta dada e descobri-la.
   • Definições ausentes: Exercícios que exigem conceitos ainda não presentes no Mathlib (ex: grupos de Frobenius específicos) necessitam de definições customizadas que devem ser cuidadosamente construídas para corresponder à intenção do livro.
   • Ambiguidades sutis: Afirmações informais frequentemente contêm restrições implícitas (ex: $n \ge 2$) que, se omitidas, tornam a afirmação formal falsa na lógica do Lean (ex: devido ao comportamento de subtração de números naturais).

Resultados
Os autores avaliaram o desempenho de diferentes modelos de autoformalização no conjunto completo de 1.966 exercícios:

• Sucesso de Elaboração: O Codex (um loop de agente iterativo) alcançou a maior taxa de sucesso de 95,5%, superando significativamente os modelos de disparo único. O GPT-5 liderou os modelos de disparo único com 44,1% dos exercícios totalmente elaborados.
• Fidelidade Semântica: Embora o sucesso sintático (elaboração) seja necessário, ele não é suficiente. Um juiz semântico baseado em LLM (Claude Opus 4.7) avaliou a fidelidade das afirmações. O GPT-5 obteve uma pontuação média de 3,45/5, com 45,1% das saídas consideradas "fiéis". Em contraste, o DeepSeek-R1 obteve uma pontuação significativamente menor (1,15/5), falhando frequentemente em emitir declarações ou produzindo afirmações vazias.
• Complementaridade de Modelos: Os modelos exibiram alto nível de discordância; apenas 7 exercícios foram resolvidos por todos os sistemas, enquanto 654 foram resolvidos por exatamente um. Isso ressalta o valor de executar modelos em paralelo.
• Necessidade de Verificação Humana: A etapa de verificação provou ser a mais trabalhosa. Mesmo com altas taxas de elaboração, muitas afirmações continham erros semânticos (ex: nomes de grupos errados, quantificadores invertidos) que exigiram intervenção humana especializada para serem resolvidos.

Significância
O artigo postula que o LEAN-GAP aborda uma lacuna crítica nos dados de treinamento para sistemas de IA, indo além dos benchmarks de competição para o currículo padrão de graduação. O trabalho demonstra que, embora os LLMs possam automatizar a tradução inicial de texto matemático, eles ainda não podem servir como autoformalizadores de ponta a ponta para material padrão devido a persistentes lacunas semânticas. Os autores argumentam que o futuro da formalização reside na colaboração produtiva entre humano e IA, onde a IA atua como um "segundo leitor" para identificar erros sutis e hipóteses não declaradas, enquanto matemáticos humanos fornecem a supervisão necessária para a fidelidade semântica. Esta abordagem oferece um modelo para escalar a formalização de materiais de treinamento matemático padrão, servindo potencialmente como base para o desenvolvimento de "estudantes de matemática de IA" capazes de dominar currículos padrão.