Resumo Técnico: COMPOSE – Compondo Teoremas Futuros a partir de Citações e Estrutura Formal

Definição do Problema

O artigo aborda o desafio da geração futura fundamentada de matemática: a tarefa de prever uma afirmação matemática futura plausível (uma declaração semelhante a um teorema) para um artigo "âncora" dado. Os autores argumentam que uma previsão válida deve satisfazer duas restrições simultâneas:

1. Trajetória Científica: Deve estender a direção de pesquisa indicada pelo grafo de citações científicas e pela evolução das ideias na literatura.
2. Fundamentação Formal: Deve respeitar as dependências lógicas inerentes à matemática formal, garantindo que a afirmação seja derivável validamente de definições, lemas e teoremas existentes.

Abordagens existentes tipicamente modelam apenas uma dessas fontes. Modelos treinados exclusivamente em texto científico podem gerar afirmações fluentes, mas logicamente desfundamentadas, enquanto sistemas de prova de teoremas raciocinam sobre estruturas formais, mas carecem do contexto científico para identificar direções de pesquisa promissoras. O artigo postula que combinar essas fontes complementares é não trivial devido às diferenças fundamentais na forma como artigos científicos e bibliotecas formais (como Mathlib) organizam o conhecimento.

Metodologia: O Framework COMPOSE

Os autores propõem o COMPOSE, um framework de duplo grafo que condiciona um modelo de linguagem tanto ao contexto de citação científica quanto à estrutura de teorema formal. A abordagem consiste em três componentes principais:

1. Construção de Dados

Os autores construíram um conjunto de dados de 108.000 exemplos de grafos pareados científico-formal derivados de artigos de matemática do arXiv (2000–2023) e da biblioteca Lean Mathlib.

• Grafo Científico ($G_s$): Construído a partir de um artigo âncora e seu contexto de citação (até dois saltos). Inclui nós de resumo para artigos e nós de teorema extraídos do texto. As arestas representam links de citação e dependências internas do artigo.
• Grafo Formal ($G_f$): Construído alinhando teoremas informais extraídos aos teoremas correspondentes no Mathlib. Esse alinhamento utiliza o FrenzyMath (um corpus de descrições informais escritas por humanos para teoremas do Mathlib) para realizar recuperação informal-para-informal, evitando o ruído da autoformalização direta. O grafo formal expande-se a partir da raiz do teorema correspondente usando arestas de dependência extraídas via LeanDojo.
• Benchmark: Um conjunto de teste retido temporalmente de 47.000 artigos futuros do final de 2024 e 2025, usado para avaliar a capacidade do modelo de prever resultados publicados reais.

2. Arquitetura do Modelo

O COMPOSE emprega uma arquitetura de duplo codificador seguida por um decodificador condicionado ao grafo:

• Duplos Codificadores: Duas Redes Neurais de Grafos (GNNs) dedicadas processam $G_s$ e $G_f$ separadamente.
  • Os nós de $G_s$ são inicializados com embeddings E5 (texto científico).
  • Os nós de $G_f$ são inicializados com embeddings DeepSeek-Math (assinaturas formais).
  • Ambos utilizam passagem de mensagens direcionada e específica por tipo de aresta com conexões residuais com portão.
• Módulo de Fusão: As representações de ambos os grafos são projetadas em um espaço latente compartilhado e fundidas por meio de um mecanismo de atenção cruzada bidirecional. Isso permite que o modelo integre a direção científica com restrições formais.
• Decodificador: Um LLM especializado em matemática pré-treinado (DeepSeek-Math-7B ou Mistral-7B) adaptado com LoRA. Camadas de atenção cruzada são inseridas no decodificador para condicionar a geração aos embeddings de grafo fundidos, permitindo que o modelo atenda à estrutura completa do grafo durante a geração de tokens.

3. Treinamento em Duas Etapas

• Etapa 1 (Aprendizado de Representação): Os codificadores de grafo e o módulo de fusão são treinados sem o decodificador usando três objetivos:
  • Previsão de Link: Para garantir que os codificadores capturem a estrutura do grafo.
  • Alinhamento Contrastivo: Para alinhar a representação de grafo fundida com o resumo do artigo-alvo e a afirmação principal.
  • Alinhamento Cruzado: Para alinhar explicitamente nós de teorema informais com suas contrapartes formais correspondentes.
• Etapa 2 (Geração): O decodificador é adicionado e ajustado finamente usando:
  • Perda Autoregressiva: Previsão padrão do próximo token.
  • Perda de Margem de Grafo: Um termo de regularização que penaliza o modelo se ele gerar o mesmo texto para um par de grafos incompatível, forçando-o a depender do contexto específico do grafo.

Resultados Principais

Os experimentos foram conduzidos no benchmark de 47K artigos futuros, comparando o COMPOSE contra bases fortes (incluindo GIANTS, FutureGen, GoAI e várias variantes apenas de texto ou apenas de prompt).

• Desempenho de Recuperação: O COMPOSE alcançou o maior Gap (0,240), definido como a diferença na similaridade de cosseno entre o texto gerado e o artigo futuro verdadeiro versus artigos não relacionados. Superou significativamente as bases em H@10 (50,8%) e H@100 (80,8%), indicando que suas afirmações geradas têm muito mais probabilidade de recuperar o artigo futuro correto do conjunto.
• Previsão de Afirmação Matemática Nova (NMCP): O COMPOSE liderou em Precisão (0,560) e Correspondência (0,730), demonstrando que suas saídas se alinham com teoremas futuros em níveis tanto formais quanto informais, não apenas tematicamente.
• Avaliação por Juiz LLM: Um juiz LLM (GPT-4.0) avaliou as saídas quanto a Conteúdo, Profundidade, Novidade, Precisão e Especificidade. O COMPOSE alcançou a pontuação geral mais alta (3,36/5), particularmente em Profundidade Técnica (3,52) e Especificidade (3,52), produzindo saídas mais concretas e matematicamente ricas do que as bases, que frequentemente geravam resumos vagos.
• Estudos de Ablação: Remover qualquer um dos codificadores de grafo, científico ou formal, causou quedas significativas de desempenho, confirmando que ambas as modalidades fornecem sinais complementares. O grafo formal foi crucial para a fundamentação, enquanto o grafo científico foi essencial para identificar a direção de pesquisa correta.

Significado e Afirmações

O artigo afirma que a geração futura de matemática se beneficia da combinação de contexto científico com estrutura formal.

• Geração Fundamentada: Os autores demonstram que confiar apenas em texto científico leva a afirmações que são tematicamente relevantes, mas logicamente desfundamentadas, enquanto confiar apenas em estrutura formal limita o modelo a teoremas conhecidos sem antecipar novas direções. O COMPOSE supera com sucesso essa lacuna.
• Contribuição de Dados: A construção do conjunto de dados pareado de 108K e o benchmark de 47K artigos futuros fornecem um novo recurso para avaliar a geração matemática fundamentada, abordando a falta de benchmarks temporais neste campo.
• Avanço Metodológico: O framework de duplo grafo com fusão por atenção cruzada oferece uma abordagem inovadora para integrar fontes de conhecimento heterogêneas (literatura informal vs. lógica formal) para tarefas generativas.

Os autores notam limitações, especificamente que o método depende de um alinhamento aproximado informal-formal (o que pode introduzir ruído em áreas com cobertura esparsa do Mathlib) e que as afirmações geradas não são verificadas por um assistente de prova, dependendo em vez disso de recuperação e avaliação baseada em LLM como sinais proxy. Eles sugerem que trabalhos futuros poderiam incorporar verificação consciente de prova para verificar diretamente a correção formal das afirmações geradas.