Resumo Técnico: Nazrin: Uma Tática de Automação de Provas Neurais Atômicas em Lean 4

Declaração do Problema

A prova de teoremas assistida por máquina em sistemas como o Lean 4 enfrenta desafios significativos ao treinar agentes automatizados em provas escritas por humanos. Os principais obstáculos incluem:

1. Espaços de Ação Ilimitados: Provas humanas utilizam uma variedade infinita de táticas com parâmetros arbitrários (por exemplo, simp com listas longas de argumentos, use com testemunhas arbitrárias), criando um espaço de busca ruidoso e difícil de aprender.
2. Visões de Apresentação vs. Busca: Provas escritas por humanos frequentemente priorizam concisão e legibilidade (Visão de Apresentação), obscurecendo os passos incrementais de raciocínio reverso (Visão de Busca) realmente necessários para descobrir a prova. Isso inclui "saltos misteriosos" e a elisão de passos intermediários.
3. Acoplamento de Metavariáveis: No Lean, os objetivos (goals) muitas vezes dependem uns dos outros (metavariáveis acopladas). Uma busca em árvore ingênua falha ao não considerar o fato de que resolver um objetivo pode resolver instantaneamente outro ou tornar um caminho impossível, complicando a busca em um Grafo Acíclico Dirigido (DAG) em vez de uma simples árvore.
4. Restrições de Hardware: Os provadores de teoremas neurais existentes frequentemente exigem recursos computacionais significativos, limitando sua acessibilidade e a escala de dados de treinamento que podem processar.

Metodologia

O artigo introduz o Nazrin (Neural Atomizer for Inhabitation Problems), um agente de prova de teoremas baseado em redes neurais de grafos (GNN). A metodologia baseia-se em três pilares fundamentais:

1. Táticas Atômicas

Os autores definem um conjunto pequeno e finito de "táticas atômicas" capazes de provar qualquer afirmação provável em Lean. Estas táticas são projetadas para ter um espaço de parâmetros limitado, garantindo que o espaço de ação para o agente seja finito.

• Completude: O conjunto cobre todos os construtores de expressões de alto nível no Lean (por exemplo, intro para abstração lambda, exact/apply para constantes, cases para tipos indutivos).
• Propriedades: As táticas são invariantes (não alteram metavariáveis atribuídas sem retrocesso), completas, progressivas (sempre fazem progresso) e determinísticas.
• Minimização de Seção Transversal: O conjunto é escolhido para minimizar "seções transversais" (o número de objetivos acoplados), reduzindo a dificuldade do problema de geração de orientação.

2. Transposição de Atomização

Para treinar o agente, os autores desenvolveram um novo algoritmo para converter provas existentes escritas por humanos (Visão de Apresentação) em sequências de táticas atômicas (Visão de Busca).

• Atomização: O algoritmo traduz termos de prova arbitrários em uma série de passos atômicos. Ele utiliza o termo de prova de verdade fundamental (ground-truth) para guiar a construção de uma nova prova usando apenas táticas atômicas.
• Transposição: O algoritmo reordena a execução das táticas para corresponder à "Visão de Busca". Ele prioriza objetivos "sucessores" (objetivos cujas soluções informam os predecessores) sobre objetivos "predecessores". Isso mimetiza o raciocínio reverso usado na descoberta (por exemplo, provas $\epsilon$-$\delta$) em vez da apresentação direta.
• Transposição de Nível de Estado e de Objetivo: O sistema reordena a disposição de táticas para evitar becos sem saída. Por exemplo, permite que táticas "semigraduais" não conflitantes (que atuam em partes de um alvo ou variável livre) sejam despachadas em ordem arbitrária, mesmo que os objetivos acoplados ainda não estejam instanciados.

3. ExprGraph e Arquitetura Neural

O agente utiliza uma Rede Neural de Grafos (GNN) para processar expressões Lean, representadas como ExprGraphs.

• Essencialização: As expressões são convertidas em grafos onde distinções técnicas irrelevantes (por exemplo, nomes de variáveis específicos, metadados) são apagadas. O grafo preserva simetrias fundamentais (por exemplo, $\alpha$-equivalência) e garante que subexpressões correspondam a subgrafos.
• Autômato Probabilístico Neural (NPA): Em vez de um modelo generativo padrão, o Nazrin usa um NPA. A GNN condiciona as probabilidades de transição de um autômato de estados finitos.
  • Estado de Tipo (Kind State): Seleciona o tipo de tática (por exemplo, intro, apply).
  • Estados Descendentes: Cabeças de GNN especializadas geram argumentos (por exemplo, selecionar uma constante para apply ou uma variável livre).
• Eficiência: O modelo é pequeno (1,5M de parâmetros para a biblioteca padrão, 11M para o Mathlib) e roda em hardware de CPU de consumo, gerando milhares de táticas por minuto.

Principais Contribuições

1. Táticas Atômicas: Um conjunto finito e completo de táticas que reduz o espaço de ação de prova de teoremas para um tamanho gerenciável, permitindo aprendizado por reforço e treinamento supervisionado eficientes.
2. Algoritmo de Transposição de Atomização: Um método para gerar dados de treinamento em larga escala convertendo matemática formalizada existente em provas de visão de busca atômica, efetivamente ensinando o agente como encontrar provas, em vez de como apresentar provas.
3. ExprGraph: Uma representação baseada em grafos reduzida de expressões Lean que explora simetrias estruturais e referências de variáveis, mimetizando explicitamente mecanismos de atenção encontrados em modelos de linguagem.
4. Provador Nazrin: Um agente baseado em GNN de baixo recurso que consegue treinar em dados atomizados e generalizar para novos teoremas.
5. Estrutura de Avaliação: Uma avaliação rigorosa que mimetiza o desenvolvimento de novas teorias, onde o agente é treinado em uma fatia da biblioteca e testado na próxima para garantir que não haja vazamento de informação.

Resultados

Os autores avaliaram o Nazrin na biblioteca padrão do Lean e no Mathlib:

• Sucesso de Atomização: Aproximadamente 58% dos 170.180 teoremas foram atomizados com sucesso.
• Generalização:
  • Treinado na Fatia 1 da Biblioteca Padrão, o Nazrin alcançou 57% de precisão na Fatia 2.
  • Treinado na Fatia 3 do Mathlib, alcançou 34% de conclusão na Fatia 4.
• Comparação: O Nazrin demonstrou a capacidade de provar teoremas que as táticas de automação existentes (Aesop e Grind) não conseguiram resolver dentro de um limite de 15 segundos.
• Desempenho: O sistema opera eficientemente em hardware de consumo, contrastando com os requisitos pesados de recursos de muitos provadores baseados em LLM.

Significância e Alegações

O artigo afirma que o Nazrin aborda o descompasso fundamental entre a estrutura das provas escritas por humanos e os requisitos da busca automatizada. Ao impor um espaço de ação finito através de táticas atômicas e gerar dados de treinamento via transposição de atomização, os autores demonstram que:

• Agentes de aprendizado de máquina podem ser treinados para descobrir provas incrementalmente sem a necessidade de gerar parâmetros complexos e arbitrários do zero.
• Representações baseadas em grafos são eficazes para capturar as simetrias estruturais de provas matemáticas.
• A prova de teoremas de alto desempenho é alcançável em hardware modesto, tornando a tecnologia mais acessível.

Os autores observam que, embora o sistema seja promissor, ele atualmente não cobre todos os teoremas (a atomização falha para algumas provas de alta seção transversal) e a arquitetura não foi totalmente ajustada. Eles sugerem que trabalhos futuros poderiam focar em melhorar a cobertura de atomização, reduzir as seções transversais e refinar a arquitetura neural para lidar de forma mais robusta com condicionamento de múltiplos parâmetros e dados não simbólicos (números/strings).