DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent

1. Declaração do Problema

A prova de teoremas automatizada (ATP) avançou significativamente com Modelos de Linguagem de Grande Escala (LLMs) e assistentes de prova formais como o Lean. No entanto, os sistemas atuais de última geração enfrentam duas limitações críticas:

• Falta de Generalização: A maioria das abordagens trata cada teorema isoladamente. Embora possam decompor problemas em etapas intermediárias, essas etapas são frequentemente altamente específicas para o problema individual e não se generalizam entre diferentes teoremas.
• Ineficiência: Os métodos existentes dependem de bibliotecas de lemas fixas e estáticas (limitando a adaptabilidade) ou sintetizam novos lemas intermediários para cada instância de problema. Isso leva a computação redundante, comprimentos de prova mais longos e maior uso de tokens, já que o sistema falha em acumular e reutilizar "habilidades" (lemas) aprendidas de provas anteriores.

O artigo argumenta que os sistemas atuais falham em mimetizar a prática matemática humana, onde matemáticos acumulam, abstraem e reutilizam sistematicamente um conjunto central de lemas transferíveis para resolver novos problemas com eficiência.

2. Metodologia: O Framework DreamProver

O DreamProver é um framework agencial projetado para aprender e evoluir uma biblioteca reutilizável de lemas através de um paradigma iterativo "Wake-Sleep" (Vigília-Sono), inspirado em teorias de aprendizado cognitivo e no algoritmo DreamCoder. O sistema opera em ciclos alternados:

A. Fase de Vigília (Descoberta e Decomposição de Teoremas)

Nesta fase, o agente tenta provar teoremas de um conjunto de treinamento usando a biblioteca de lemas atual.

• Identificação de Teoremas Aprendíveis: O sistema tenta provar teoremas diretamente usando a biblioteca. Se bem-sucedido, o teorema é marcado como "aprendível", implicando que a biblioteca é suficiente para aquele domínio.
• Descoberta de Teoremas Intermediários: Se um teorema não puder ser provado diretamente, o sistema o decompõe recursivamente em subproblemas mais simples (sub-teoremas).
  • Gera um esboço de prova formal.
  • Extrai objetivos intermediários não provados (marcados por sorry) como teoremas independentes.
  • Valida esses teoremas extraídos tentando remontar a prova completa usando o esboço e os novos candidatos.
• Resultado: O sistema acumula um conjunto de "teoremas aprendíveis" (resultados intermediários) derivados dos dados de treinamento.

B. Fase de Sono (Abstração de Lemas e Otimização da Biblioteca)

Nesta fase, o sistema processa as experiências acumuladas para evoluir a biblioteca de lemas.

• Agrupamento Semântico: O sistema anota os teoremas intermediários coletados com descrições em linguagem natural (subdomínio, dificuldade, conceitos relevantes). Em seguida, incorpora essas descrições e as agrupa usando K-Means com base na similaridade semântica.
• Abstração de Lemas: Para cada cluster, um LLM é solicitado a gerar um lema candidato que generaliza os teoremas específicos naquele cluster.
• Validação Estrutural: Para garantir que os lemas abstraídos sejam aplicáveis, o sistema calcula a similaridade estrutural (usando distância de edição de árvore em árvores de expressões de lógica de primeira ordem) entre o lema candidato e os teoremas no cluster. Lemas que excedem um limite de similaridade são mantidos.
• Atualização da Biblioteca (Esquecimento e Duplicação):
  • Deduplicação: Novos lemas são comparados com a biblioteca existente usando distância de edição de árvore; lemas altamente similares (duplicatas) são descartados.
  • Esquecimento: Para manter uma biblioteca compacta, o sistema emprega uma estratégia de "Menos Recente Usado" (LRU). Lemas que não foram usados frequentemente nas fases de vigília recentes são podados assim que a biblioteca atinge a capacidade.
  • Verificação: Os lemas candidatos restantes são formalmente verificados para garantir que são prováveis.

C. Inferência

Durante a inferência em problemas de teste não vistos, o DreamProver utiliza a biblioteca evoluída. Primeiro, tenta a geração direta de prova. Se isso falhar, emprega um fluxo de trabalho "Esboço-e-Prova" (Sketch-and-Prove), usando a biblioteca para orientar a geração de esboços de prova e a resolução de subobjetivos.

3. Contribuições Principais

1. Paradigma Wake-Sleep para ATP: A primeira aplicação de um ciclo contínuo e iterativo de vigília-sono especificamente para evoluir bibliotecas de lemas transferíveis em prova de teoremas formais.
2. Aprendizado de Lemas Transferíveis: Diferentemente de trabalhos anteriores (como LEGO-Prover) que lutaram para demonstrar reutilização eficaz, o DreamProver agrupa e abstrai explicitamente resultados intermediários em lemas gerais, criando uma base de conhecimento persistente e de alta qualidade.
3. Mecanismos de Eficiência: A introdução de um mecanismo de "esquecimento" (poda LRU) e deduplicação estrutural garante que a biblioteca permaneça compacta (<100 lemas), prevenindo o estouro da janela de contexto e mantendo alta relevância de recuperação.
4. Generalização de Domínio: O framework é projetado para funcionar em diversos domínios matemáticos, incluindo aqueles sub-representados nos dados de treinamento de LLMs.

4. Resultados Experimentais

Os autores avaliaram o DreamProver em cinco domínios matemáticos: Desigualdades, Teoria dos Números, Combinatória, Geometria Plana e Teoria do Aprendizado de Máquina.

• Ganhos de Desempenho:

  • O DreamProver melhorou as taxas de sucesso de prova em uma média de 61% em comparação com sistemas de última geração (SOTA) anteriores como Hilbert e Goedel-Prover-V2.
  • Em domínios específicos, as melhorias foram drásticas: 114% em Teoria dos Números e 50% em Combinatória.
  • Em domínios sub-representados (Geometria Plana, Teoria de ML), o DreamProver resolveu significativamente mais instâncias do que LLMs proprietários (por exemplo, resolvendo 14-16 problemas de geometria de nível olímpico onde LLMs de base resolveram 0-3).

• Eficiência e Qualidade:

  • Redução de Tokens: O DreamProver reduziu o uso de tokens de saída em 48% em média em comparação com sistemas agentes SOTA.
  • Concisão de Prova: As provas geradas foram 50% mais curtas em média, indicando maior qualidade e melhor estrutura.
  • Reutilização de Lemas: A análise mostrou que 58% dos lemas gerados durante o treinamento foram reutilizados em conjuntos de teste, contribuindo para 71% de todos os teoremas provados com sucesso.

• Estudos de Ablação:

  • Remover o refinamento iterativo de vigília-sono (evolução de passagem única) reduziu significativamente as taxas de sucesso (de 104 para 76 problemas resolvidos).
  • Remover o agrupamento semântico resultou em uma biblioteca sobredimensionada e ingovernável, reduzindo o desempenho até mesmo abaixo de uma base sem biblioteca.

5. Significado

O DreamProver representa uma mudança da prova de teoremas "one-shot" ou de "biblioteca estática" para aprendizado contínuo e de autoaperfeiçoamento.

• Ponte entre as Lacunas: Ele efetivamente preenche a lacuna entre o poder de raciocínio bruto dos LLMs e o conhecimento estruturado e reutilizável necessário para raciocínio matemático complexo.
• Escalabilidade: Ao aprender uma biblioteca compacta e transferível, o sistema reduz o custo computacional de provar novos teoremas, tornando a verificação formal de alto nível mais acessível.
• Aprendizado Semelhante ao Humano: O framework mimetiza processos cognitivos humanos (adquirir experiência, abstrair princípios e esquecer detalhes irrelevantes), sugerindo um caminho viável para sistemas de raciocínio de IA mais robustos e generalizáveis.

Em conclusão, o DreamProver demonstra que aprender e refinar explicitamente uma biblioteca de lemas reutilizáveis é um fator crítico para alcançar desempenho de última geração em prova de teoremas automatizada, particularmente em domínios matemáticos complexos e com escassez de dados.