💬 NLP

Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving

O artigo apresenta o KG-prover, um novo quadro que aprimora modelos de linguagem grandes de propósito geral com grafos de conhecimento extraídos de textos matemáticos para melhorar a prova automática de teoremas, demonstrando ganhos significativos de desempenho em múltiplos conjuntos de dados sem exigir ajuste fino adicional.

Autores originais: Vincent Li, Tim Knappe, Yule Fu, Kevin Han, Kevin Zhu

Publicado 2026-05-26

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Vincent Li, Tim Knappe, Yule Fu, Kevin Han, Kevin Zhu

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

A Grande Ideia: Dar aos Modelos de Matemática uma "Cola"

Imagine que você está tentando resolver um quebra-cabeça matemático muito difícil. Você tem um amigo superinteligente (um Modelo de Linguagem Grande, ou LLM) que sabe muita matemática, mas às vezes ele fica travado porque não consegue lembrar de uma regra específica ou não consegue ver como duas ideias diferentes se conectam.

Geralmente, para tornar esses amigos mais inteligentes, você precisa enviá-los de volta à escola por anos de treinamento (ajuste fino). Este artigo diz: "Não há necessidade de escola extra!" Em vez disso, podemos simplesmente dar a eles um mapa melhor e uma biblioteca melhor enquanto eles trabalham no problema.

Os autores construíram um sistema chamado KG-Prover. É como dar ao seu amigo inteligente uma teia gigante e interconectada de fatos matemáticos (um Grafo de Conhecimento) e permitir que eles "consultem" as pistas certas em tempo real enquanto tentam resolver o quebra-cabeça.

Como Funciona: A Analogia do Detetive

Pense na IA como um detetive tentando resolver um crime (o teorema matemático).

A Cena do Crime (O Problema): O detetive recebe uma declaração que precisa provar ser verdadeira.
A Biblioteca (O Grafo de Conhecimento): Os autores construíram uma biblioteca massiva a partir do ProofWiki (um site cheio de provas matemáticas). Eles transformaram essa biblioteca em uma teia de aranha gigante onde cada conceito matemático é um nó, e as linhas que os conectam mostram como eles se relacionam (por exemplo, "O Teorema A usa a Definição B").
A Investigação (A Busca):
- Em vez de adivinhar, o detetive olha para a teia de aranha.
- Eles começam na cena do crime e perguntam: "Quem está relacionado a isso?"
- Eles seguem as linhas para encontrar conceitos, definições e provas anteriores semelhantes.
- Se ficarem presos, não desistem; eles vão mais fundo na teia, seguindo mais linhas para encontrar pistas escondidas. Isso é chamado de "escalonamento do cálculo de tempo de teste" — basicamente, gastar mais tempo e esforço durante a investigação para encontrar a resposta.
O Rascunho (Prova Informal): O detetive escreve um rascunho da solução em inglês simples (linguagem natural), usando as pistas que encontrou.
A Tradução (Formalização): Um tradutor especializado (outra IA) pega esse rascunho em inglês e o transforma em código estrito e legível por computador (Lean 4).
O Juiz (Verificação): Um árbitro rigoroso verifica o código. Se estiver errado, o detetive recebe uma dica sobre o que deu errado, volta à teia de aranha, encontra uma nova pista e tenta novamente.

A "Cola" que Funciona

O artigo afirma que, ao fazer esse processo de "buscar e recuperar", eles não precisaram retreinar os modelos de IA. Eles apenas usaram modelos existentes e de propósito geral (como GPT-4o-mini ou Llama 3) e permitiram que eles usassem o mapa.

Os Resultados:

Melhores Pontuações: Quando adicionaram esse "mapa de teia de aranha", a taxa de sucesso da IA em problemas matemáticos aumentou significativamente (de 2% a 21%, dependendo do teste).
O Efeito "Mergulho Profundo": Quanto mais a IA foi permitida a buscar mais fundo no grafo (seguindo mais conexões), melhor ela ficou em resolver problemas difíceis. É como dizer: "Se você não consegue resolver em um minuto, leve dez minutos e olhe cada livro relacionado na biblioteca."
Sem Treinamento Extra: A maior vitória é que eles não precisaram gastar milhões de dólares treinando um novo modelo. Eles apenas deram aos modelos antigos uma ferramenta melhor para usar enquanto trabalhavam.

As Limitações (Onde o Detetive Fica Preso)

O artigo é honesto sobre onde esse método falha:

A Lacuna de Tradução: Às vezes, o detetive escreve uma explicação perfeita em inglês, mas o tradutor erra ao transformá-la em código estrito. A lógica matemática estava certa, mas a "gramática" da linguagem de computador estava errada.
Pistas Faltantes: Se a resposta exigir um fato matemático muito obscuro que não está em sua biblioteca (ProofWiki), o detetive não consegue encontrá-lo, não importa o quanto busque fundo.
Muitas Ruídos: Se a teia de aranha estiver muito bagunçada, o detetive pode ficar confuso com informações irrelevantes.

Resumo

Este artigo apresenta uma maneira de tornar especialistas em matemática de IA mais inteligentes sem re treiná-los. É como dar a um estudante genial um smartphone com uma enciclopédia perfeita e interconectada e dizer a ele: "Tome seu tempo, consulte cada fato relacionado que precisar e escreva a prova." Ao permitir que a IA "pense mais" e busque mais fundo em seu grafo de conhecimento durante o teste, ela resolve mais problemas corretamente.

Resumo Técnico: Escalonamento de Computação em Tempo de Teste Baseada em Grafos de Linguagem Natural para Prova Automatizada de Teoremas

Declaração do Problema

Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham demonstrado capacidades em raciocínio lógico de múltiplos passos, a prova automatizada de teoremas permanece desafiadora. Obstáculos específicos incluem a identificação precisa de conceitos matemáticos-chave, a compreensão de suas inter-relações e a formalização correta de provas dentro de linguagem natural ou sistemas formais. Abordagens existentes frequentemente dependem de ajuste fino intensivo, iteração de especialistas ou treinamento em grandes volumes de dados formais (por exemplo, Lean), o que pode ser pesado em termos de recursos e limitar a capacidade do modelo de aproveitar conhecimentos matemáticos mais amplos e informais. Além disso, abordagens puramente formais podem lutar com a flexibilidade do raciocínio natural, enquanto abordagens puramente em linguagem natural enfrentam ambiguidade ao traduzir para sistemas de verificação formal.

Metodologia: KG-Prover

Os autores introduzem o KG-Prover, um novo framework que aprimora LLMs de propósito geral com um grafo de conhecimento (KG) extraído de textos matemáticos reputados (especificamente o ProofWiki) para construir e formalizar provas. O sistema opera sem ajuste fino adicional do LLM base, confiando, em vez disso, no escalonamento de computação em tempo de teste e na geração aumentada por recuperação.

Componentes Principais

Construção do Grafo de Conhecimento:
- Fonte: O grafo é construído analisando o ProofWiki, extraindo nós de namespaces como "Definição", "Axioma" e "Prova".
- Estrutura: Cada nó representa uma afirmação matemática autossuficiente (por exemplo, uma proposição de teorema ou definição). As arestas representam hiperlinks encontrados no texto, capturando dependências e relações conceituais.
- Escala: O grafo resultante contém mais de 60.000 nós e 300.000 arestas.
- Embeddings: Os nós são aprimorados com vetores de embedding pré-calculados (usando text-embedding-3-large) para facilitar a recuperação semântica.
Pipeline de Inferência:
- Recuperação e Traversal: Dada uma proposição $P$ , o sistema calcula seu embedding e recupera os $k$ nós mais similares. Se a tentativa inicial de prova falhar, o sistema expande iterativamente o contexto atravessando o grafo até a profundidade $d$ , selecionando os $k$ vizinhos superiores dos nós visitados anteriormente.
- Geração de Prova Informal: O LLM gera uma prova informal em linguagem natural usando o contexto recuperado. Isso aproveita as capacidades de raciocínio emergentes do modelo e o amplo corpus de provas informais disponíveis no KG.
- Autoformalização: Um modelo separado (DeepSeek-Prover-V1.5) traduz a prova informal em código Lean 4.
- Verificação e Refinamento: O código Lean gerado é verificado usando o provador de teoremas Lean 4. Se a verificação falhar, mensagens de erro são enviadas de volta ao autoformalizador para refinamento. Se a prova ainda falhar, o sistema pode aumentar a profundidade de travessia do grafo ou empregar estratégias de busca.
Estratégias de Escalonamento (Computação em Tempo de Teste):
- Best-of-N: O sistema gera $n$ provas informais independentes, autoformaliza-as e usa um modelo "juiz" dedicado para pontuá-las com base na correção e clareza, selecionando o candidato de maior pontuação.
- Busca em Feixe (Beam Search): Os candidatos de prova são organizados em um feixe de largura $w$ . Em cada etapa, os candidatos são expandidos com base no feedback do verificador, pontuados e os $k$ superiores são retidos para a próxima iteração. Isso equilibra a exploração de caminhos de prova diversos com o refinamento orientado pela verificação.

Contribuições Principais

Framework KG-Prover: Um sistema que integra a geração de provas informais em linguagem natural com travessia iterativa baseada em grafo de conhecimento e um mecanismo de LLM-como-juiz, eliminando a necessidade de treinamento especializado ou iteração de especialistas.
KG Matemático em Grande Escala: A construção de um grafo de conhecimento a partir do ProofWiki com mais de 60.000 nós e mais de 300.000 arestas, modelando relações complexas entre conceitos matemáticos.
Sistema de Refinamento Iterativo: Um mecanismo de avaliação heurística e busca em feixe que melhora o desempenho em até 26,4% sobre baselines e 21,8% sobre configurações do KG-Prover sem escalonamento.
Demonstração de Escalonamento em Tempo de Teste: Evidências de que modular a profundidade de travessia do grafo e empregar estratégias de busca (Best-of-N, Busca em Feixe) aumenta significativamente o desempenho sem retreinar os modelos subjacentes.

Resultados Experimentais

O framework foi avaliado em três benchmarks: miniF2F-test, ProofNet e MUSTARDSAUCE.

Ganhos de Desempenho:
- O KG-Prover superou consistentemente os sistemas baseline e a Geração Aumentada por Recuperação (RAG) padrão em todos os conjuntos de dados.
- As melhorias variaram de 2% a 11% sobre as baselines em múltiplos modelos (Llama 3.1 8B, GPT-4o, o1-mini, etc.).
- No miniF2F-test, LLMs de propósito geral melhoraram em até 21% quando combinados com o KG-Prover.
- A configuração do KG-Prover com o4-mini alcançou uma taxa de aprovação de 50% no miniF2F-test.
- Na configuração de escalonamento mais alta, as melhorias atingiram 26,4% sobre as baselines.
Efeitos de Escalonamento:
- Profundidade de Travessia: A precisão aumentou com maior profundidade de travessia ( $r$ ), particularmente para modelos de parâmetros menores como o Llama 3.1 8B. Os primeiros aumentos de profundidade produziram os ganhos mais significativos.
- Estratégias de Busca: Combinar o KG com Busca em Feixe e amostragem Best-of-N melhorou ainda mais a precisão, alcançando até 10,75% no ProofNet e 50,40% no MUSTARDSAUCE.
- Modelos Ajustados (Finetuned): Mesmo quando aplicado a modelos já ajustados para Lean (por exemplo, TheoremLlama, DeepSeek-Prover-V1.5), o KG-Prover forneceu ganhos adicionais de desempenho (por exemplo, +1,85% sobre uma baseline ajustada no miniF2F).

Significado e Alegações

O artigo postula que o KG-Prover oferece uma abordagem promissora e escalável para a prova automatizada de teoremas que não requer ajuste fino adicional ou iteração intensiva de especialistas. Ao aproveitar as capacidades de raciocínio em linguagem natural embutidas em LLMs de propósito geral e aprimorá-los com informações estruturadas recuperadas por grafo, o framework efetivamente preenche a lacuna entre o raciocínio informal e a verificação formal.

Os autores enfatizam que este método permite que modelos de fundação existentes alcancem desempenho comparável ou superior ao de sistemas especializados e ajustados, simplesmente injetando conceitos relacionados durante a inferência. O trabalho destaca o potencial do escalonamento de computação em tempo de teste — modular a profundidade de travessia do grafo e empregar estratégias de busca — como uma alternativa viável ao escalonamento de parâmetros do modelo para tarefas de raciocínio complexo. Embora a abordagem introduza desafios na etapa de tradução de informal para formal, o sistema de dois agentes (geração + autoformalização) apoiado pela recuperação por grafo mitiga com sucesso essas questões, fornecendo traços de raciocínio interpretáveis e novas estratégias para geração de provas.