💻 computer science

MathAtlas: A Benchmark for Autoformalization in the Wild

Este artigo apresenta o MathAtlas, o primeiro benchmark de autoformalização em larga escala, composto por aproximadamente 52.000 conceitos matemáticos de nível de pós-graduação provenientes de 103 livros didáticos, o que revela a extrema dificuldade dos modelos atuais em lidar com matemática de pesquisa complexa e rica em dependências.

Autores originais: Nilay Patel, Noah Arias, Davit Babayan, Victoria Cochran, Timothy Libman, Hafsah Mahmood, Liam McCarty, Soli Munoz, Laurel Willey, Jeffrey Flanigan

Publicado 2026-05-15

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Nilay Patel, Noah Arias, Davit Babayan, Victoria Cochran, Timothy Libman, Hafsah Mahmood, Liam McCarty, Soli Munoz, Laurel Willey, Jeffrey Flanigan

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você tem um tradutor brilhante capaz de transformar histórias humanas em uma linguagem estrita e legível por computador chamada "Lean". Por muito tempo, esse tradutor só foi testado em histórias simples — como problemas de matemática do ensino médio ou quebra-cabeças básicos. O computador conseguia traduzi-los facilmente porque as regras eram simples e o computador já havia visto regras semelhantes antes.

Mas o que acontece quando você pede a esse tradutor que traduza um artigo de pesquisa complexo, de nível de pós-graduação? Esse é o problema que o MathAtlas aborda.

Aqui está uma explicação simples do que o artigo faz, usando algumas analogias do cotidiano:

1. O Problema: A "Biblioteca" é Grande Demais

Imagine que você está tentando construir uma casa (uma prova formal) com base em um projeto (um livro didático de matemática).

Benchmarks Antigos: Testes anteriores só pediam ao tradutor que construísse uma pequena cabana. Os materiais estavam todos ali na caixa de ferramentas, e as instruções eram curtas.
O Mundo Real: A matemática de pós-graduação é como tentar construir um arranha-céu. Para construir o último andar, você precisa do 50º andar. Para construir o 50º andar, você precisa do 49º, e assim por diante, até chegar à fundação.
O Problema: Na matemática avançada, a "fundação" (definições e teorias) muitas vezes ainda não foi construída na linguagem do computador. Se o tradutor não conhece a definição de uma "Álgebra de Lie" (um conceito complexo), ele não consegue traduzir o teorema que a utiliza.

2. A Solução: MathAtlas (O Mapa "Selvagem")

Os autores criaram o MathAtlas, um novo conjunto de testes massivo.

A Escala: Eles coletaram dados de 103 livros didáticos de matemática de pós-graduação. É como pegar uma biblioteca de 52.000 páginas de matemática avançada e transformá-la em um mapa digital.
O "Grafo de Dependência": Este é o superpoder do artigo. Imagine um livro "Escolha Sua Própria Aventura" onde cada página tem setas apontando para outras páginas que você precisa ler primeiro. O MathAtlas desenha essas setas. Ele mostra que, para entender a Proposição 15, você primeiro precisa entender os Anéis de Dedekind, que por sua vez precisam dos Ideais Primos.
Por que isso importa: Isso força a IA não apenas a traduzir uma frase, mas a descobrir: "Tenho as ferramentas para construir isso? Se não, consigo encontrar ou construir as ferramentas primeiro?"

3. Os Resultados: A IA Está Presa na Lama

Os autores testaram os modelos de IA mais inteligentes disponíveis no MathAtlas, e os resultados foram humildes.

A Pontuação: Mesmo a melhor IA acertou menos de 10% das afirmações de teoremas. Para definições, foi cerca de 16%.
A Armadilha da "Profundidade": Quanto mais profunda a "árvore de dependência" (mais passos você precisa dar para trás para encontrar as definições), pior a IA se saiu.
- Analogia: Se a IA precisa consultar 10 conceitos anteriores para traduzir uma frase, ela fica confusa e desiste. Nos problemas mais difíceis (onde a árvore de dependência era mais profunda), a IA acertou apenas 2,6%.
O Efeito "Mathlib": A IA se saiu ligeiramente melhor quando o conceito que precisava traduzir já estava em uma famosa biblioteca chamada "Mathlib" (que é como uma caixa de ferramentas pré-construída que a IA provavelmente estudou). Se o conceito era novo e não estava naquela biblioteca, a IA lutou muito mais.

4. O Teste de "Confiança" (MA-Align)

O artigo também criou um novo teste chamado MA-Align.

O Problema: Às vezes, uma IA traduz uma frase para um código que parece perfeito e roda sem erros, mas na verdade significa algo completamente diferente da matemática original. É como traduzir "O gato sentou no tapete" para um programa de computador que diz "O cachorro comeu a pizza". O programa funciona, mas está errado.
O Teste: Eles pediram a juízes de IA que verificassem se a tradução era "fiel" (verdadeira ao significado). Eles descobriram que até os melhores juízes de IA eram frequentemente enganados, especialmente com definições complexas de nível de pós-graduação.

A Conclusão

O artigo conclui que, embora a IA esteja ficando boa em matemática simples, atualmente ela é terrível na tradução de matemática de pós-graduação complexa e do mundo real. O principal gargalo não é apenas traduzir palavras; é entender a vasta rede de conexões entre ideias e saber como construir as "ferramentas" necessárias (definições) antes de construir a "casa" (teoremas).

O MathAtlas agora está aberto para que todos o utilizem como um curso de desafio para ajudar a IA a aprender a lidar com essas dependências profundas e complexas.

Resumo Técnico: MathAtlas: Um Benchmark para Autoformalização no Mundo Real

Declaração do Problema

Os benchmarks atuais de autoformalização focam principalmente em domínios mais simples, como matemática olímpica ou de graduação, onde o material pré-requisito é limitado e frequentemente já está formalizado em bibliotecas como a Mathlib. No entanto, a matemática de pós-graduação e de pesquisa permanece pouco explorada. Nesses domínios avançados, a autoformalização é significativamente mais complexa porque:

Profundidade dos Pré-requisitos: A matemática avançada depende de uma teoria pré-requisita extensa, grande parte da qual ainda não foi formalizada. Um sistema eficaz deve não apenas formalizar a declaração-alvo, mas também recuperar ou sintetizar as teorias dependentes necessárias.
Lacuna de Definições: Os benchmarks existentes ignoram em grande parte a formalização de definições matemáticas. Sistemas que conseguem apenas lidar com declarações de teoremas são limitados pela teoria formal existente; eles não podem formalizar teoremas que envolvem conceitos para os quais não existem definições.
Falta de Dados do Mundo Real: Há uma escassez de benchmarks em grande escala e do mundo real que capturem a complexidade "no mundo real" da matemática de pós-graduação, incluindo dependências contextuais ricas e relações entre entidades.

Metodologia

Construção do Conjunto de Dados: MathAtlas

Os autores apresentam o MathAtlas, o primeiro benchmark de autoformalização em grande escala para matemática de pós-graduação.

Material de Origem: O conjunto de dados é extraído de 103 livros didáticos de matemática de pós-graduação cobrindo 87 campos distintos (por exemplo, análise real, geometria diferencial, teoria das categorias, grupos quânticos).
Escala e Composição: O MathAtlas contém aproximadamente 52.052 entidades, compreendendo:
- ~18.000 teoremas
- ~10.000 exercícios
- ~10.000 definições
- ~10.000 provas
- ~5.000 exemplos
Grafo de Dependência: Uma característica fundamental é o enriquecimento do conjunto de dados com um grafo de dependência matemática contendo ~178.000 relações. Este grafo liga entidades a:
- Referências a Objetos: Conceitos matemáticos nomeados (por exemplo, "anel de Dedekind") que requerem definições externas.
- Referências a Entidades: Referências a outros teoremas ou definições específicos dentro do texto.
- Referências a Variáveis Locais: Símbolos usados sem introdução local explícita.
- Profundidade de Dependência: A altura máxima da árvore de dependência de uma entidade (profundidade média de 30, variando até 80), que varia significativamente por campo (por exemplo, álgebra de Lie possui árvores mais profundas que a teoria dos conjuntos).

Pipeline de Construção:

Conversão: PDFs são convertidos para Markdown Matemático (MMD) usando o Nougat.
Extração: Um LLM com prompt de poucos exemplos (gpt-oss-120b) extrai entidades (definições, teoremas, etc.) e seus identificadores.
Extração de Referências: Um segundo modelo identifica referências a objetos, entidades e variáveis locais dentro do texto extraído.
Extração de Relações: Um sistema associa referências a entidades-alvo (usando LeanSearch para fundamentação na Mathlib e LLMs para correspondência interna) para construir o grafo de dependência.
Controle de Qualidade: A avaliação humana em amostras aleatórias indica 90,4% de validade para extração de entidades e uma pontuação F1 de 94,8% para extração de relações.

Métricas de Avaliação

O artigo avalia o desempenho de autoformalização usando uma métrica composta chamada Corretude, que exige que uma formalização satisfaça duas condições:

Compilação: O código Lean 4 gerado deve compilar com sucesso.
Fidelidade Semântica: A declaração formal deve ser semanticamente equivalente à fonte informal.
- Para medir a fidelidade, os autores introduzem o MA-Align, um benchmark de classificação binária de 200 entidades (declarações e definições) do MathAtlas, anotadas como "alinhadas" ou "desalinhadas".
- Eles avaliam sistemas existentes de "LLM como juiz" (por exemplo, CriticLean) e descobrem que, embora performem bem em benchmarks anteriores (ConsistencyCheck, CriticLeanBench), sua precisão cai significativamente no MA-Align, destacando uma lacuna na avaliação de definições de nível de pós-graduação.

Configuração Experimental

Os autores testaram várias linhas de base no MathAtlas, incluindo:

Modelos com Prompt: Prompting zero-shot e few-shot com gpt-oss-20b e gpt-oss-120b.
Modelos Ajustados (Fine-Tuned): Herald, Kimina, ATLAS-L, Goedel e ReForm.
Estudos de Ablação: Testando o impacto do contexto local (500 tokens anteriores), prompts engenharia e exemplos de treinamento específicos.
Subconjunto MA-Hard: Um subconjunto específico de ~700 entidades com as árvores de dependência mais profundas (profundidade média >50) para testar os limites dos sistemas atuais.

Resultados Principais

Desempenho Geral

O MathAtlas prova ser um benchmark extremamente desafiador. Linhas de base fortes alcançam baixas taxas de corretude:

Declarações (Teoremas, Exemplos, Exercícios): A melhor linha de base (ReForm 8B) alcança apenas 9,8% de corretude.
Definições: A melhor linha de base (gpt-oss-120b com prompting few-shot) alcança 16,7% de corretude.
Disparidade: Há uma lacuna significativa entre as taxas de compilação e a corretude (por exemplo, o Kimina 7B compila 27,3% das declarações, mas apenas 2,3% são fiéis), indicando que o sucesso sintático não garante precisão semântica.

Profundidade de Dependência e Dificuldade

O desempenho degrada substancialmente à medida que a profundidade de dependência aumenta:

No MA-Hard (as 700 entidades com as árvores de dependência mais profundas), o melhor modelo alcança apenas 2,6% de corretude.
Análise estatística (teste de Kolmogorov–Smirnov) confirma uma diferença significativa nas distribuições de corretude entre árvores de dependência rasas e profundas ( $p < 0,001$ ).

Contexto e Fundamentação

Contexto Local: Adicionar contexto local (500 tokens anteriores) ao prompt diminuiu o desempenho para modelos com prompt (caindo de 20,3% para 17,4% em definições), sugerindo que os modelos atuais lutam para integrar contexto de longo alcance de forma eficaz.
Fundamentação na Mathlib: Entidades que puderam ser fundamentadas em formalizações existentes na Mathlib foram significativamente mais propensas a serem formalizadas corretamente (27,9% vs. 16,8% para definições não fundamentadas), sugerindo que os LLMs se beneficiam da exposição prévia a teoria formalizada em seus dados de treinamento.

Significado e Contribuições

O artigo reivindica o seguinte significado para o campo:

Primeiro Benchmark de Nível de Pós-Graduação: O MathAtlas é o primeiro benchmark em grande escala e "no mundo real" para matemática de pós-graduação, indo além das restrições de conjuntos de dados olímpicos e de graduação.
Avaliação Consciente de Dependência: É o primeiro benchmark a incluir grafos de dependência ricos e relações entre entidades, permitindo a avaliação de sistemas que devem lidar com teoria pré-requisita e síntese de definições.
Destacando a Lacuna de Definições: Os resultados demonstram que os modelos atuais de última geração lutam significativamente com definições e cadeias profundas de dependência, revelando um gargalo crítico na escalabilidade da autoformalização para matemática avançada.
Limitações da Métrica de Fidelidade: A introdução do MA-Align e os experimentos subsequentes mostram que as métricas existentes de fidelidade semântica (como CriticLean) não se generalizam bem para definições de nível de pós-graduação, necessitando de novas abordagens de avaliação.
Recurso para a Comunidade: Os autores liberam o MathAtlas, o MA-Align e o código experimental para facilitar pesquisas futuras sobre autoformalização consciente de dependência e a formalização de conceitos matemáticos avançados.

Os autores concluem que, embora os sistemas atuais mostrem promessa, a lacuna entre as capacidades existentes e os requisitos da matemática de pós-graduação permanece vasta, particularmente no que diz respeito à síntese de teoria pré-requisita e à formalização de definições.