Resumo Técnico: ProofWala

Declaração do Problema

A prova de teoremas automatizada usando métodos neurais requer uma infraestrutura robusta para interagir com Provadores de Teoremas Interativos (ITPs), extrair dados estruturados de provas e executar a busca de provas em escala. As ferramentas existentes são frequentemente fragmentadas, específicas de cada assistente e orientadas para a execução interativa em nível de arquivo via interfaces REPL (Read-Eval-Print Loop). Esta arquitetura apresenta limitações significativas:

• Escalabilidade: Dificulta a análise em escala de repositórios e a experimentação paralela.
• Extração de Dados: Oferece acesso limitado a metadados de nível de declaração (ex: definições indutivas, constantes, namespaces) e torna a construção de grafos de dependência de todo o repositório difícil ou inviável.
• Lacunas entre Assistentes: A falta de ferramentas unificadas torna desafiadora a exploração de potenciais ganhos cross-linguais e cross-domínio provenientes do treinamento em corpora formais multilíngues (ex: Lean e Rocq).

Metodologia

Os autores apresentam o ProofWala, um framework de engenharia de provas multilíngue projetado para unificar interação, extração de dados, treinamento e busca entre diferentes ITPs. O framework é construído em torno de três componentes principais:

1. O Módulo de Interface (itp-interface)

Este é um módulo reutilizável para interação programática com ITPs, fornecendo uma abstração unificada para Lean 4 e Rocq (múltiplas versões).

• Backend Lean 4: Em vez de depender de uma arquitetura baseada em REPL, os autores implementaram metaprogramas que executam diretamente dentro do elaborador do Lean. Isso permite:
  • Rastreamento de nível de tática semanticamente fiel.
  • Extração de metadados de nível de declaração e construção de grafos de dependência de todo o repositório.
  • Melhor manipulação de construtos de táticas aninhadas (ex: blocos have).
  • Clonagem de Ambiente: A capacidade de clonar ambientes de prova para execução paralela, o que é difícil com fluxos de trabalho REPL padrão.
  • Robustez de Versão: Uma camada de compatibilidade tênue garante a compatibilidade futura entre versões do Lean 4 a partir da 4.15.0.
• Backend Rocq: Construído sobre o coq_serapy, estendendo-o para suportar a extração sistemática de estados de prova e rastros de táticas, mapeando-os para o mesmo formato unificado usado para o Lean.
• Modelo de Estado Unificado: Ambos os assistentes são mapeados para um sistema de transição de estado padronizado onde um estado de prova é um conjunto de obrigações (objetivos e hipóteses), e as táticas transitam esses estados.

2. Módulo de Dados e Modelo

• Extração de Dados: O framework extrai pares de estado de prova–tática de grandes repositórios (CompCert, MathComp, GeoCoq, Mathlib, CategoryTheory) ao reexecutar scripts de tática dentro do kernel do assistente.
• Formato Unificado: Os dados extraídos são armazenados em um formato JSON unificado que abstrai detalhes específicos do assistente enquanto preserva informações semânticas. O formato de prompt para treinamento é idêntico para Lean e Rocq, omitindo tokens específicos do assistente para facilitar o treinamento cross-assistente.
• Treinamento: Os autores realizaram o ajuste fino (fine-tuning) de um modelo CodeT5-Base (220M de parâmetros) em três configurações:
  1. ProofWala-Rocq: Treinado em repositórios Rocq.
  2. ProofWala-Lean: Treinado em repositórios Lean.
  3. ProofWala-Multilingual: Treinado conjuntamente em ambos os assistentes.

3. Módulo de Busca de Prova Paralela

• Pool de Ambientes: Uma inovação chave é o pool de ambientes, que mantém múltiplos ambientes de prova clonados inicializados em estados de fronteira idênticos.
• Execução Paralela: Candidatos a táticas são executados concorrentemente nessas instâncias clonadas. Este pool integra-se com o Ray para execução distribuída, permitindo busca de prova escalável e anotação em larga escala.
• Algoritmos de Busca: O módulo suporta busca de melhor primeiro (best-first) e beam search paralelizadas. Ele mantém uma árvore de prova anotada registrando apenas transições de estado válidas e compiláveis, permitindo uma análise granular da dinâmica de busca.

Principais Contribuições

1. Framework Padronizado e Biblioteca de Engenharia: O ProofWala fornece um framework unificado para extrair e organizar dados de nível de tática e apoiar o desenvolvimento de ferramentas. Ele introduz um pipeline de instrumentação via metaprogramação para o Lean que suporta travessia de repositório consciente de dependências e clonagem de ambiente, capacidades anteriormente difíceis de alcançar via REPL.
2. Suporte para Conclusão de Prova Paralela: O framework é o primeiro sistema de código aberto a fornecer busca de prova paralela ao suportar explicitamente ambientes de prova clonados e avaliação de táticas concorrentes dentro de uma interface multi-ITP unificada.
3. Datasets e Modelos Multilíngues: Os autores liberam um dataset multilíngue (~450K pontos de dados, 270M de tokens) e modelos treinados (Lean, Rocq e Multilingual) que facilitam a busca de prova de ponta a ponta.

Resultados

Os autores avaliaram os modelos nos splits de teste do CompCert, MathComp, GeoCoq, CategoryTheory e Lean/Mathlib, bem como no benchmark MiniF2F.

• Transferência Cross-Lingual: O modelo ProofWala-Multilingual geralmente iguala ou melhora os baselines monolíngues.
  • Melhorias Estatisticamente Significativas: Observadas no maior benchmark (Lean/Mathlib) e no cenário de adaptação de domínio CategoryTheory (onde o modelo multilingual foi ajustado nos dados de CategoryTheory).
  • Tendências: Outros datasets mostraram tendências consistentes, mas não estatisticamente significativas, favorecendo o treinamento multilíngue.
• Adaptação de Domínio: No domínio de CategoryTheory, o modelo multilingual alcançou scores pass-at-k substancialmente mais altos após o fine-tuning em comparação com o baseline apenas de Rocq, sugerindo que o pré-treinamento em dados de linguagens mistas auxilia na adaptação, mesmo quando o domínio alvo é representado em apenas um assistente.
• Dinâmica de Busca: A análise das árvores de prova revelou que modelos multilíngues frequentemente produzem árvores maiores com fatores de ramificação (branching factors) mais altos, indicando que eles propõem um número maior de táticas válidas por estado.
• Escalabilidade: A execução paralela via pools de ambiente melhorou significativamente o throughput. O aumento de 8 para 20 workers de CPU melhorou o pass@5 no MiniF2F de 22.54% para 26.23%, reduzindo simultaneamente o tempo médio de prova.

Significância e Alegações

O artigo afirma que o ProofWala representa uma mudança de ferramentas fragmentadas e específicas de assistentes para uma infraestrutura unificada e escalável para prova de teoremas neural.

• Unificação Arquitetural: Ao unificar execução, coleta de dados, análise de dependência e busca, o framework permite uma análise sistemática, reproduzível e granular da busca de prova neural em múltiplos ITPs.
• Evidência de Transferência: O trabalho fornece evidência empírica de que o treinamento multilíngue gera transferência cross-lingual e cross-domínio positiva em raciocínio formal, particularmente em regimes de alta densidade de dados e cenários de adaptação de domínio.
• Fundação de Pesquisa: Os autores posicionam o ProofWala não apenas como um sistema de busca de prova, mas como um framework de pesquisa que transforma a busca de prova de uma avaliação de "caixa-preta" em um pipeline analisável. Isso permite que pesquisadores estudem transferência estrutural, tamanho de árvore, fatores de ramificação e latência de execução de maneiras anteriormente difíceis de obter.

Os autores observam que, embora modelos maiores e infraestrutura adicional (ex: retrieval, verifiers) sejam provavelmente necessários para o desempenho de estado da arte em benchmarks, sua principal contribuição é o framework em si, que isola os efeitos do treinamento multilíngue e das estratégias de busca paralela. Eles veem a extensão para assistentes orientados a documentos (como o Isabelle) como um desafio de engenharia, e não uma limitação conceitual, deixando isso para trabalhos futuros.