🤖 AI

Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph

O artigo apresenta o Aria, um agente baseado em recuperação que emprega um processo de Grafo de Pensamento de duas fases e um pontuador fundamentado em definições para alcançar a precisidade de estado da arte na autoformalização de nível de conjectura de matemática de pesquisa em Lean, superando efetivamente limitações comuns de LLMs, como alucinações e incompatibilidades semânticas.

Autores originais: Hanyu Wang, Ruohan Xie, Yutong Wang, Guoxiong Gao, Xintao Yu, Bin Dong

Publicado 2026-07-03

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Hanyu Wang, Ruohan Xie, Yutong Wang, Guoxiong Gao, Xintao Yu, Bin Dong

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

O Grande Problema: A Lacuna da "Perda na Tradução"

Imagine que você tem um matemático brilhante que fala "Matemática Humana" (linguagem natural, como o inglês ou português) e um computador super rigoroso que só fala "Matemática Formal" (uma linguagem de programação rígida chamada Lean). O computador é incrivelmente poderoso; ele pode provar teoremas sem cometer erros. Mas ele tem um grande problema: não entende a matemática humana, a menos que ela seja traduzida perfeitamente.

Se você traduzir uma frase matemática mesmo que ligeiramente errado, o computador a rejeita. Os modelos de IA atuais (LLMs) são como tradutores entusiastas, mas inexperientes. Eles frequentemente:

Alucinam: Inventam palavras ou regras que não existem no dicionário do computador.
Entendem o significado errado: Usam as palavras certas, mas na ordem errada, mudando completamente o sentido.
Desistem de coisas difíceis: Diante de um problema de pesquisa novo e complexo, eles travam porque não têm uma resposta pré-escrita em sua memória.

A Solução: Conheça a Aria

Os autores construíram um novo agente de IA chamado Aria. Pense na Aria não como uma tradutora, mas como uma Arquiteta Mestra que constrói uma ponte entre a Matemática Humana e a Matemática de Computador.

A Aria não apenas adivinha a tradução. Ela usa um processo de três etapas para garantir que a ponte seja sólida:

1. O "Mapa de Dependências" (Graph-of-Thought)

A Analogia: Imagine que você está tentando construir um arranha-céu. Você não pode simplesmente despejar concreto para o último andar; você precisa da fundação, das vigas de aço e do encanamento primeiro.
Como a Aria faz: Em vez de tentar traduzir todo o problema matemático de uma vez, a Aria o decompõe. Ela desenha um mapa (um grafo) mostrando como cada conceito depende de outros.

Exemplo: Para entender "Módulo de Cohen-Macaulay", você primeiro precisa entender "Anel de Noetheriano", que precisa de "Ideal", que precisa de "Anel".
A Aria constrói a ponte de baixo para cima, garantindo que cada tijolo seja colocado corretamente antes de passar para o próximo nível.

2. O "Detetive de Biblioteca" (Retrieval-Augmented Generation)

A Analogia: Imagine um estudante fazendo uma prova que tem permissão para usar uma biblioteca, mas não tem permissão para memorizar os livros. Se o estudante tentar inventar uma regra, ele será pego.
Como a Aria faz: As bibliotecas matemáticas (como a Mathlib) são constantemente atualizadas com novas regras. Modelos antigos de IA dependem do que memorizaram anos atrás, o que costuma estar desatualizado ou errado.

A Aria age como um detetive. Antes de escrever uma única linha de código, ela pesquisa a biblioteca atual para encontrar a definição exata e oficial dos termos que precisa.
Se a biblioteca não tiver uma definição para um novo conceito, a Aria sabe que precisa inventar uma do zero, mas faz isso cuidadosamente, checando seu trabalho contra as regras que acabou de encontrar.

3. O "Ciclo de Autocorreção" (Iterative Reflection)

A Analogia: Pense em um escultor esculpindo uma estátua. Eles não apenas esculpem uma vez e esperam pelo melhor resultado. Eles esculpem, recuam, observam, veem uma falha e esculpem novamente.
Como a Aria faz:

A Aria escreve um trecho de código.
Ela o executa através do compilador do computador (o juiz rigoroso).
Se o computador disser "Erro", a Aria não entra em pânico. Ela lê o erro, entende o que deu errado e tenta novamente.
Ela repete este ciclo de "tentar-falhar-corrigir" até que o código compile perfeitamente.

O "Detector de Verdade": AriaScorer

Mesmo que o código compile (rode sem travar), ele ainda pode significar a coisa errada. Isso é como uma frase que é gramaticalmente perfeita, mas diz: "O céu é verde".

Os autores construíram uma ferramenta especial chamada AriaScorer para verificar o significado.

O Jeito Antigo: Ferramentas anteriores apenas comparavam as palavras. Se o humano disse "Anel" e o código disse "Anel", elas achavam que era uma correspondência.
O Jeio da Aria: O AriaScorer é um investigador profundo. Ele busca a definição real de "Anel" na biblioteca do computador e compara essa definição profunda com a intenção humana.
Ele detecta truques sutis, como quando a IA troca a ordem dos ingredientes em uma receita. Ele garante que a versão do computador seja matematicamente idêntica à ideia do humano, não apenas parecida visualmente.

Os Resultados: Quão boa é a Aria?

A equipe testou a Aria em três níveis de dificuldade:

Matemática de Graduação (ProofNet): A Aria acertou 68,5% das traduções difíceis, superando todos os modelos anteriores.
Matemática de Nível de Doutorado (FATE-X): É aqui que outros modelos geralmente falham. A Aria acertou 44,0%, enquanto o segundo melhor modelo conseguiu apenas 24,0%.
Conjecturas de Pesquisa Real (O "Teste Impossível"): A equipe deu à Aria 14 problemas matemáticos novos e não resolvidos de matemáticos reais.
- Outros modelos de IA: 0% de sucesso. Eles nem conseguiram começar.
- Aria: 42,9% de sucesso. Ela conseguiu traduzir quase metade desses problemas novos e nunca antes vistos para um formato que o computador pudesse entender.

Resumo

A Aria é um sistema que impede a IA de "inventar coisas" ao realizar matemática avançada. Em vez de adivinhar, ela:

Mapeia as dependências (como um projeto/blueprint).
Pesquisa a biblioteca oficial para encontrar regras atuais (como um detetive).
Itera e corrige seus próprios erros (como um escultor).
Verifica o significado profundo, não apenas as palavras superficiais (como um detector de verdade).

Isso permite que ela lide com problemas matemáticos complexos, de nível de pesquisa, que sistemas de IA anteriores simplesmente não conseguiam tocar.

Resumo Técnico: ARIA – Um Agente para Recuperação e Autoformalização Iterativa via Grafo de Dependência

1. Declaração do Problema

A autoformalização precisa de enunciados de teoremas — traduzindo texto matemático informal em linguagens formais como Lean 4 — é um gargalo crítico para o avanço da descoberta e verificação automatizada na matemática de nível de pesquisa. Embora os Grandes Modelos de Linguagem (LLMs) tenham mostrado promessa em tarefas de nível de graduação, eles enfrentam dificuldades significativas com enunciados de nível de conjectura devido a três modos principais de falha:

Alucinações e Incompatibilidades Semânticas: Os LLMs frequentemente geram código usando funções ou definições que não existem na biblioteca (Mathlib) ou interpretam incorretamente a intenção semântica de conceitos matemáticos.
Incapacidade de Sintetizar Novas Definições: A matemática de nível de pesquisa frequentemente requer a definição de novos objetos não presentes nas bibliotecas existentes. Métodos estáticos de geração em etapa única falham porque não conseguem sintetizar espontaneamente essas definições.
Limitações de Verificação Semântica: Verificadores semânticos existentes muitas vezes dependem de similaridade textual superficial ou retro-tradução, falhando em detectar discrepâncias sutis entre conceitos informais e seus equivalentes formais em Lean (por exemplo, coerções de tipo incorretas ou ordem de parâmetros invertida).

Esses problemas levam a traduções não fiéis que descarrilam pipelines de geração de dados em larga escala e impedem a exploração autônoma de problemas matemáticos abertos.

2. Metodologia

O artigo apresenta o ARIA (Agente para Recuperação e Autoformalização Iterativa), um sistema projetado para emular o raciocínio de especialistas humanos através de um processo de Grafo de Pensamento (GoT - Graph-of-Thought) de duas fases. O pipeline é estruturado da seguinte forma:

2.1 O Pipeline de Grafo de Pensamento (GoT)

Ao contrário da geração direta em etapa única, o ARIA decompõe a tarefa de formalização em um grafo de dependência estruturado:

Fase 1: Decomposição GoT (Top-Down): O agente recebe um enunciado informal e o decompõe recursivamente em um grafo de dependência de conceitos. Cada nó representa uma definição, estrutura ou classe.
- Fundamentação (Grounding): Para cada conceito, o agente consulta o LeanSearch (um mecanismo de recuperação que indexa a versão mais recente da Mathlib) para encontrar definições canônicas.
- Raciocínio: Um LLM analisa os candidatos recuperados para identificar a melhor correspondência canônica. Se nenhuma correspondência existir (o conceito é novo), o nó é marcado para síntese.
Fase 2: Síntese GoT (Bottom-Up): O agente sintetiza definições formais começando pelos nós folha (conceitos fundamentados) até o nó raiz (o teorema principal).
- Compilador no Loop (Compiler-in-the-Loop): Em cada etapa de síntese, o código gerado é imediatamente compilado. Se a compilação falhar, a mensagem de erro é alimentada de volta ao LLM para refinamento (autorreflexão).
- Síntese de Novos Conceitos: Para nós não fundamentados, o agente gera novas definições utilizando o código verificado de suas dependências como contexto.

2.2 AriaScorer: Verificador Semântico Fundamentado em Nível de Termo

Para garantir a correção semântica além da compilação sintática, os autores introduzem o AriaScorer.

Recuperação em Nível de Termo: Antes de avaliar um enunciado formal, o AriaScorer utiliza um analisador estático (jixia) para extrair todos os termos Lean referenciados no código. Ele consulta um conjunto de dados curado da Mathlib para recuperar as definições, tipos e descrições informais autoritativas desses termos.
Decomposição de Subtarefas: O enunciado informal é decomposto em premissas e conclusões atômicas.
Avaliação Fundamentada: O LLM avalia a correspondência entre as subtarefas informais e o código formal, mas, crucialmente, é fornecido com as definições formais recuperadas como contexto. Isso permite que o verificador raciocine sobre a verdadeira semântica dos termos Lean, em vez de depender apenas de similaridade de texto superficial.
Pontuação: As subtarefas são rotuladas como "Correspondência Perfeita", "Inconsistência Menor" ou "Inconsistência Maior". Estas são agregadas via um integral difuso para uma pontuação final (0 a 1), que é submetida a um limiar para tomar uma decisão binária de aceitação/rejeição.

3. Principais Contribuições

Agente Aria: Um novo agente de autoformalização que integra Geração Aumentada por Recuperação (RAG), planejamento de Grafo de Pensamento e autorreflexão guiada pelo compilador. É o primeiro sistema capaz de sintetizar autonomamente definições complexas e inéditas necessárias para a formalização de nível de conjectura.
AriaScorer: Um verificador semântico fundamentado em nível de termo que recupera definições autoritativas da Mathlib para verificar a correção matemática das formalizações, reduzindo significamente os falsos positivos causados por alucinações semânticas.
Desempenho de Estado da Arte: O sistema alcança melhorias significativas sobre métodos existentes em múltiplos benchmarks, particularmente em problemas de nível de pesquisa onde modelos anteriores falham completamente.

4. Resultados Experimentais

Os autores avaliaram o ARIA em diversos benchmarks, medindo a Acurácia Final (a proporção de enunciados que passam tanto na compilação quanto nos testes semânticos).

ProofNet (Nível de Graduação): O ARIA alcançou uma taxa de sucesso de compilação de 91,6% e uma acurácia final de 68,5%, superando métodos anteriores.
FATE-H (Exames Finais de Álgebra): O ARIA alcançou 71,0% de acurácia final, superando o melhor baseline (Goedel-V2 pass@128) que obteve 43,0%.
FATE-X (Nível de Doutorado/Pesquisa): O ARIA alcançou 44,0% de acurácia final, comparado a 24,0% do melhor baseline.
Conjecturas Homológicas (Pesquisa Real): Em um conjunto de 14 conjecturas desafiadoras de álgebra comutativa, o ARIA alcançou uma taxa de sucesso de 42,9%, enquanto todos os outros modelos baseline (incluindo Goedel-V2 e Gemini-2.5-Pro) obtiveram 0%.

Estudos de Ablação:

Remover o mecanismo de Reflexão causou o colapso do desempenho (0% de sucesso em Conjecturas).
Remover o planejador GoT reduziu o sucesso em Conjecturas de 6/14 para 1/14.
Desativar o módulo RAG resultou em 0% de sucesso em Conjecturas, confirmando que o conhecimento pré-treinado estático é insuficiente para definições de nível de pesquisa.

Validação do Verificador Semântico:
No benchmark FATE-X, o AriaScorer alcançou 89,9% de acurácia (com $\alpha=0$ ) e 95,5% de precisão (com $\alpha=0,9$ ), superando significativamente os baselines LeanScorer e Back-Translation. Estudos de caso demonstraram sua capacidade de detectar "Discrepâncias de Definição" (ex: diferenças sutis nas regras de multiplicação para álgebras de quatérnios) e suprimir alucinações ao fundamentar a avaliação nas definições reais da biblioteca.

5. Significância e Alegações

O artigo afirma que o ARIA representa um passo fundamental em direção à descoberta matemática autônoma. Ao abordar os "gargalos fundamentais" da alucinação e da incapacidade de sintetizar novas definições, o ARIA permite a formalização confiável de problemas de nível de conjectura.

Os autores enfatizam que a formalização precisa de enunciados é um pré-requisito para a prova de teoremas. O sucesso do ARIA no conjunto de dados de Conjecturas Homológicas demonstra uma capacidade única de lidar com problemas de pesquisa ativa que eram anteriormente inacessíveis para sistemas automatizados. A integração da fundamentação em nível de termo na verificação semântica (AriaScorer) é apresentada como uma evolução necessária além das métricas de similaridade textual, fornecendo um padrão rigoroso para verificar a fidelidade matemática das formalizações geradas por IA.

O trabalho sugere que futuros sistemas de prova matemática automatizada devem depender de agentes estruturados, aumentados por recuperação e autorreflexivos para navegar na complexidade das bibliotecas matemáticas modernas e das fronteiras de pesquisa.