Resumo Técnico: Descoberta de Teoremas Autossupervisionada em um Sistema Axiomático Formal

Declaração do Problema

Embora sistemas de IA recentes, particularmente Grandes Modelos de Linguagem (LLMs), tenham demonstrado progresso significativo no raciocínio matemático, eles dependem amplamente de priors fornecidos por humanos, como textos matemáticos, código e bibliotecas de teoremas existentes. Uma questão aberta crítica permanece: Pode um agente descobrir autonomamente teoremas úteis partindo puramente das regras primitivas de um sistema axiomático formal, sem acesso a conhecimento prévio humano, bibliotecas de teoremas existentes ou conjuntos de problemas de treinamento?

Métodos atuais frequentemente dependem de conhecimento construído por humanos para iniciar o raciocínio (bootstrap). Mesmo agentes de autoaperfeiçoamento em domínios axiomáticos frequentemente dependem de juízes externos para avaliar a utilidade dos teoremas descobertos. Este artigo investiga se um agente pode não apenas descobrir teoremas, mas também identificar e utilizar aqueles que são "úteis" para melhorar sua própria busca de provas e o desempenho de sistemas de raciocínio externos, baseando-se exclusivamente em axiomas e regras de inferência.

Metodologia

1. Configuração Formal: Sistema de Hilbert como uma Máquina de Pilha

Os autores instanciam o problema dentro de um sistema axiomático de Hilbert para lógica proposicional. O sistema é deliberadamente minimalista, consistindo em:

• Três Axiomas:
  • $Ax1: A \to (B \to A)$ (Enfraquecimento)
  • $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ (Distribuição)
  • $Ax3: (\neg A \to \neg B) \to (B \to A)$ (Contraposição)
• Uma Regra de Inferência: Modus Ponens (MP), derivando $Y$ de $X$ e $X \to Y$.

Para facilitar o aprendizado, os autores formulam a prova de teoremas como um processo de decisão de máquina de pilha determinística e condicionada ao objetivo $(S, A, s_0, P)$:

• Estado ($S$): Uma pilha finita de fórmulas.
• Ações ($A$): Empilhar instâncias de $Ax1, Ax2, Ax3$ na pilha, ou aplicar Modus Ponens (MP).
• Mecanismo: A ação MP utiliza unificação de Hindley–Milner. Se o elemento no topo da pilha se unificar com $X \to Y$ e o elemento abaixo se unificar com $X$, ambos são removidos da pilha (popped) e $Y$ é empilhado.
• Sucesso: Uma prova é bem-sucedida se a pilha contiver uma única fórmula que corresponda ao objetivo alvo.

2. Algoritmo de Descoberta de Teoremas Autossupervisionado

A contribção central é um algoritmo que alterna entre busca de prova e extração de teoremas úteis, construindo uma biblioteca de teoremas que servem como lemas para buscas futuras.

A. Aprendizado de Política Condicionada ao Objetivo

O agente aprende uma política $\pi_\theta(A|S, g)$ para prever a próxima ação dado o estado atual da pilha $S$ e um objetivo $g$.

• Aprendizado de Perspectiva (Hindsight Learning): Durante um episódio de busca, qualquer estado onde a pilha contém uma única fórmula $f_t$ é tratado como um "teorema alcançado", independentemente de ser o objetivo original.
• Sinal de Treinamento: O prefixo de ações que leva a $f_t$ é tratado como uma prova de $f_t$. Esses prefixos são adicionados a um conjunto de treinamento $D_{train}$ para atualizar a política via perda de entropia cruzada.
• Buffer de Objetivos ($G$): Um buffer mantém os teoremas descobertos. O agente amostra objetivos uniformemente de $G$ para episódios de busca subsequentes, efetivamente realizando o bootstrapping de seu próprio currículo.

B. Extração de Teoremas Úteis

Para evitar que a biblioteca se torne inflada com teoremas triviais ou redundantes, o algoritmo filtra os teoremas descobertos com base em dois critérios:

1. Generalidade: Os teoremas são filtrados para remover aqueles que são meras especializações de outros candidatos. O sistema retém apenas os elementos "mínimos" sob uma ordem parcial definida por substituição de fórmulas (ou seja, mantendo as formas mais gerais).
2. Reprovabilidade: O sistema estima a probabilidade de que a política atual possa provar novamente um teorema. Usando uma média posterior Bayesiana (Beta(1,1)), ele prioriza teoremas que foram descobertos, mas que são difíceis de provar novamente de forma confiável. Esses teoremas "difíceis de reprovar" são valiosos porque adicionar o conhecimento deles como lemas comprime caminhos de prova difíceis.

C. Expansão da Biblioteca de Múltiplas Gerações

O processo opera em gerações:

1. Aprendizado de Política: Treinar a política no espaço de ações atual (inicialmente apenas axiomas e MP).
2. Extração: Identificar teoremas úteis do buffer de objetivos $G$ baseando-se em generalidade e reprovabilidade.
3. Expansão do Espaço de Ações: Adicionar os teoremas extraídos como novas ações de biblioteca (ex: $Thm_1, Thm_2$). Quando selecionadas, essas ações empilham o teorema correspondente na pilha, atuando como um lema pré-verificado.
4. Iteração: Repetir o processo, permitindo que o agente use teoremas descobertos anteriormente para encontrar novos teoremas mais complexos.

Principais Contribuições

1. Formulação: A prova de teoremas proposicionais é formulada como um processo de decisão de máquina de pilha baseado diretamente em axiomas de Hilbert e regras de inferência, evitando a dependência de corpora de provas externos.
2. Algoritmo: É proposto um algoritmo de descoberta de teoremas autossupervisionado que expande uma biblioteca de teoremas a partir de regras primitivas puras. Ele reutiliza os teoremas extraídos como lemas para buscas de prova subsequentes.
3. Descoberta Autônoma: O agente descobre dezenas de milhares de teoremas e encontra provas para problemas de referência escritos por humanos sem usar priors humanos para treinamento.
4. Transferibilidade: Os teoremas extraídos servem como conhecimento externo eficaz, melhorando o desempenho de raciocínio de LLMs externos quando fornecidos como lemas no prompt.

Resultados Experimentais

1. Descoberta de Teoremas e Cobertura

• Crescimento: O número de teoremas descobertos aumenta ao longo de seis gerações, demonstrando a capacidade do agente de expandir sua base de conhecimento autonomamente.
• Desempenho em Benchmarks: O agente encontra com sucesso provas do sistema de Hilbert para 30% de um conjunto de referência escrito por humanos (derivado do livro de Kleene).
• Comparação: Enquanto o GPT-5-high (o baseline mais forte) atinge apenas cerca de 23% de precisão nesses benchmarks sem assistência, a capacidade do agente de encontrar provas para 30% sugere que ele descobre provas não triviais que são significativas do ponto de vista matemático humano.

2. Impacto no Raciocínio de LLMs

• Lemas de Prompt: Quando os teoremas extraídos são fornecidos como lemas de prompt para variantes do GPT-4o e GPT-5, suas taxas de sucesso de prova nos problemas de referência melhoram significativamente.
• Análise Qualitativa:
  • Alguns teoremas descobertos correspondem a princípios bem conhecidos (ex: o princípio da explosão, $\neg A \to (A \to B)$), que são facilmente interpretáveis.
  • Outros (ex: levantamento complexo de implicação) não são imediatamente óbvios para humanos, mas funcionam efetivamente como conhecimento de suporte em provas de LLMs.
  • Isso indica que o agente pode trazer à tona lemas úteis que humanos não forneceram explicitamente, e que esses lemas são transferíveis entre diferentes arquiteturas de raciocínio (do agente para os LLMs).

Significância e Alegações

O artigo afirma fornecer evidências de que úteis teoremas podem emergir da busca de prova sem depender de bibliotecas de teoremas fornecidas por humanos.

• IA Autoevoluível: O trabalho sugere um caminho para sistemas de IA autoevoluíveis para matemática que podem expandir autonomamente seu conhecimento formal através da busca de provas, garantindo que cada descoberta permaneça formalmente verificável.
• Verificabilidade Formal: Ao contrário dos LLMs que podem alucinar afirmações plausíveis mas incorretas, as descobertas do agente são estritamente fundamentadas nos axiomas e regras de inferência do sistema de Hilbert.
• Modéstia: Os autores não alegam ter superado o estado da arte dos LLMs em raciocínio geral. Em vez disso, demonstram que, em um ambiente controlado e formal, um agente pode aprender a descobrir e utilizar seu próprio conhecimento para resolver problemas que são difíceis até para LLMs avançados, e que esse conhecimento autodescoberto pode aumentar sistemas externos.

O estudo é limitado a um único sistema axiomático (lógica proposicional de Hilbert), mas os autores postulam que o framework é generalizável para sistemas mais ricos, como lógica de primeira ordem ou teoria dos conjuntos, o que permanece como uma direção para trabalhos futuros.