Semantic Search over 9 Million Mathematical Theorems

Este trabalho apresenta e avalia um sistema de busca semântica em escala para 9,2 milhões de teoremas matemáticos extraídos de fontes como o arXiv, demonstrando que a recuperação específica de teoremas, e não apenas de artigos inteiros, é viável e eficaz ao utilizar descrições em linguagem natural e modelos de linguagem avançados.

O essencial

Imagine que o conhecimento matemático é uma biblioteca gigante e infinita, cheia de milhões de livros (artigos científicos) escritos por gênios ao redor do mundo.

O problema é que, até hoje, se você quisesse encontrar uma fórmula específica, um teorema ou uma prova dentro dessa biblioteca, você teria que pegar um livro inteiro, ler capa a capa e tentar adivinhar em qual página a informação estava escondida. Era como tentar encontrar uma agulha num palheiro, mas o palheiro era do tamanho de um planeta.

Os pesquisadores deste trabalho decidiram construir um super-índice para essa biblioteca. Eles criaram uma ferramenta que permite procurar diretamente pela "agulha" (o teorema), sem precisar ler o "palheiro" inteiro (o artigo).

Aqui está como eles fizeram isso, explicado de forma simples:

1. O Grande Desafio: A "Barreira da Linguagem"

Os matemáticos escrevem suas descobertas usando uma linguagem muito técnica, cheia de símbolos estranhos (como $\sum$, $\int$, $\forall$) e códigos de computador (LaTeX).

• O Problema: Se você perguntar a um buscador comum: "Existe uma prova de que todo número primo par é 2?", o computador não entende bem essa pergunta porque ele está acostumado a procurar por palavras-chave exatas nos códigos, não pelo significado da frase.
• A Solução Criativa: Os autores usaram Inteligência Artificial (IA) para ler cada um dos 9,2 milhões de teoremas e reescrevê-los como se fossem manchetes de jornal ou resumos curtos em português (ou inglês, no caso original). Eles chamam isso de "slogans".
  • Em vez de: "Teorema 3.4: $\forall x \in \mathbb{R}, x^2 \geq 0$."
  • A IA criou: "O quadrado de qualquer número real é sempre positivo ou zero."

2. A Biblioteca de 9 Milhões de Livros

Eles não pararam em apenas alguns livros. Eles vasculharam o arXiv (o maior repositório de pré-publicações científicas do mundo) e mais 7 outras fontes, como a ProofWiki e o Stacks Project.

• Eles conseguiram extrair e organizar 9,2 milhões de afirmações matemáticas. É a maior coleção já feita de "fatos matemáticos" prontos para busca.

3. Como a Busca Funciona (A Analogia do Tradutor)

Quando um matemático (ou um robô) faz uma pergunta, o sistema faz o seguinte:

1. Traduz a Pergunta: Transforma a pergunta do usuário em um "slogan" (uma frase simples).
2. Traduz a Resposta: Como todos os 9 milhões de teoremas já foram transformados em "slogans" pela IA, o sistema compara a pergunta com os slogans.
3. Encontra o Par: Como ambos agora estão na mesma "língua" (frases naturais), a IA consegue entender que "número primo par é 2" é a mesma coisa que "o único primo par é 2", mesmo que as palavras sejam ligeiramente diferentes.

4. O Resultado: Um "Google" para Teoremas

Eles testaram essa ferramenta com perguntas de matemáticos reais.

• O Antigo Jeito: Se você usasse o Google ou o ChatGPT comum, eles provavelmente te dariam o título de um artigo que pode conter a resposta, ou então inventariam uma resposta errada com confiança.
• O Novo Jeito: A ferramenta deles encontrou o teorema exato, na página exata, dentro do artigo exato, com muito mais precisão.
  • Eles conseguiram achar o teorema certo em 45% das tentativas (enquanto o Google e o ChatGPT conseguiam em menos de 20-30%).

5. Por que isso é importante?

• Para Humanos: Um matemático pode economizar horas de leitura procurando se uma ideia já foi descoberta antes.
• Para Robôs (IA): Se um robô estiver tentando provar um teorema novo, ele precisa de "peças" (teoremas antigos) para montar o quebra-cabeça. Essa ferramenta dá ao robô acesso imediato às peças certas, evitando que ele tente reinventar a roda ou cometa erros.

Resumo da Ópera

Pense nisso como a diferença entre tentar encontrar uma música específica em um toca-discos gigante, girando os discos aleatoriamente, versus usar um Spotify onde você digita a letra da música e ele toca exatamente o que você quer.

Os autores criaram o "Spotify dos Teoremas Matemáticos", transformando milhões de códigos complexos em frases simples que qualquer pessoa (ou máquina) pode entender e buscar. E o melhor: eles deixaram a ferramenta gratuita para todos usarem!

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "Semantic Search over 9 Million Mathematical Theorems", apresentado em português:

Visão Geral

O artigo apresenta um sistema de busca semântica em escala para teoremas matemáticos, abordando a lacuna entre ferramentas de pesquisa atuais (que operam no nível de documentos inteiros) e a necessidade real de matemáticos e agentes de IA de localizar resultados específicos (teoremas, lemas, proposições) dentro de grandes corpora técnicos. O trabalho introduz o maior corpus unificado de teoremas de pesquisa escritos por humanos já disponibilizado publicamente, contendo 9,2 milhões de declarações de teoremas.

---

1. O Problema

• Limitação das Ferramentas Atuais: Motores de busca acadêmicos (Google Scholar, arXiv) e LLMs com acesso à web operam no nível de documentos. Quando um pesquisador busca um resultado específico, é forçado a ler manualmente artigos inteiros para encontrar a afirmação correta.
• Risco de Redundância e Erros: A falta de busca no nível do teorema leva a retratações de artigos (2,5% dos pré-prints retirados no arXiv devem-se a resultados já existentes) e a agentes de IA que "resolvem" problemas que já foram estabelecidos décadas atrás.
• Desafio Técnico: A linguagem matemática é altamente simbólica e estruturada (LaTeX), o que dificulta a aplicação direta de modelos de busca semântica padrão, projetados para linguagem natural.

2. Metodologia

O sistema proposto segue um pipeline de processamento e recuperação em várias etapas:

A. Coleta e Parsing de Dados

• Corpus: Coletado de 99,5% do arXiv (tags de matemática, estatística, ciência da computação, física, etc.) e 0,5% de outras fontes estruturadas (Stacks Project, ProofWiki, Open Logic Project, etc.).
• Parsing: Utiliza três estratégias para extrair teoremas do código LaTeX:
  1. Node Search (plasTeX): Converte LaTeX em uma árvore de nós estruturada (sucesso em 6,9 milhões de teoremas).
  2. TeX Logging: Um pacote LaTeX personalizado que registra dados de teoremas durante a compilação (1,8 milhões).
  3. Regex-based Parsing: Expressões regulares para delimitadores básicos (542 mil).
• Limpeza: Filtragem de corpos de teoremas truncados ou malformados.

B. Representação (O "Slogan")

• Geração de Descrição Natural: Em vez de embutir diretamente o LaTeX (que é difícil para modelos de linguagem entenderem semanticamente), o sistema usa um LLM (DeepSeek V3) para gerar um "slogan" — uma descrição curta e declarativa em inglês natural do resultado principal do teorema.
• Estratégias de Contexto: O estudo avaliou três abordagens de prompt para o LLM:
  1. Apenas o corpo do teorema.
  2. Corpo + Resumo (Abstract) do artigo.
  3. Corpo + Introdução do artigo.
  • Resultado: O uso da Introdução forneceu o melhor desempenho, pois contextualiza o teorema dentro do fluxo do artigo.

C. Embedding e Recuperação

• Modelo de Embedding: Utiliza o Qwen3-Embedding-8B para mapear os slogans e as consultas do usuário em um espaço vetorial compartilhado.
• Indexação: Os vetores são armazenados em um banco de dados PostgreSQL com a extensão pgvector, utilizando um índice HNSW (Hierarchical Navigable Small World) combinado com quantização binária para busca aproximada de vizinhos mais próximos (ANN) rápida.
• Pipeline de Recuperação:
  1. Busca inicial baseada em distância de Hamming (rápida).
  2. Re-classificação (Reranking) baseada em similaridade de cosseno.
  3. Opcionalmente, um re-ranker cruzado (Cross-Encoder) para refinamento final.

---

3. Contribuições Principais

1. Corpus de Grande Escala: Disponibilização de 9,2 milhões de teoremas com metadados ricos, o maior conjunto de dados desse tipo até a data.
2. Análise Sistemática de Representação: Demonstração de que embutir slogans em linguagem natural supera significativamente a embutir fórmulas LaTeX brutas.
3. Sistema de Recuperação State-of-the-Art: Um motor de busca que supera as ferramentas existentes tanto no nível do teorema quanto no nível do artigo.
4. Ferramentas Públicas: Lançamento de uma interface de busca, API REST, servidor MCP (Model Context Protocol) para agentes de IA e o dataset no Hugging Face.

---

4. Resultados Experimentais

O sistema foi avaliado em um conjunto de 111 consultas escritas por matemáticos profissionais, comparado a baselines como Google Search, arXiv Search, ChatGPT 5.2 e Gemini 3 Pro.

• Desempenho no Nível de Teorema (Hit@20):
  • Método Proposto (Qwen3 8B): 45,0%
  • ChatGPT 5.2 com busca: 19,8%
  • Gemini 3 Pro: 27,0%
  • Observação: O modelo proposto encontra o teorema correto em 45% das vezes dentro dos 20 primeiros resultados, quase o dobro do desempenho dos LLMs gerais.
• Desempenho no Nível de Artigo (Hit@20):
  • Método Proposto: 56,8%
  • Google Search: 37,8%
• Análise de Ablação:
  • Contexto: Fornecer a introdução do artigo ao LLM gerador de slogans melhorou o desempenho em comparação com apenas o corpo ou o resumo.
  • Modelo de Embedding: O Qwen3 8B superou consistentemente modelos menores (Gemma 0.3B) e outros embedders especializados.
  • Reranking: A aplicação de um re-ranker cruzado aumentou o Hit@1 de 17,1% para 18,9%.
• Validação com RAG (Retrieval-Augmented Generation):
  • Em um experimento com o modelo Claude, a adição do banco de dados de teoremas corrigiu um raciocínio matemático incorreto sobre compactificações KSBA, permitindo que o modelo encontrasse a resposta correta citando teoremas específicos, algo que falhou sem a recuperação.

---

5. Significado e Impacto

• Viabilidade em Escala Web: O trabalho prova que a busca semântica em teoremas matemáticos é viável e eficaz em escala web, superando a barreira da notação simbólica através da "informalização" (slogans).
• Apoio à Pesquisa Humana e IA:
  • Para matemáticos: Permite localizar resultados específicos sem ler artigos inteiros, acelerando revisões de literatura.
  • Para Agentes de IA e Provas Formais: Fornece uma ferramenta crucial para seleção de premissas em sistemas de prova automática (como Lean), reduzindo a alucinação e melhorando a eficiência na busca de lemas relevantes.
• Acesso Democratizado: Ao tornar o corpus e a ferramenta de busca públicos, o projeto facilita o acesso ao conhecimento matemático de ponta, potencialmente reduzindo retratações e duplicação de esforços na pesquisa.

O projeto está disponível em theoremsearch.com, incluindo a ferramenta de busca, API e o dataset.