Resumo Técnico: Manter o Estado da Prova Ativo

Declaração do Problema

Sistemas de prova automática de teoremas que utilizam Modelos de Linguagem de Grande Escala (LLMs) e o pipeline Draft–Sketch–Prove (DSP) dependem cada vez mais de busca baseada em portfólio. Essa abordagem envolve fixar um conjunto de táticas candidatas e tentar aplicá-las em paralelo em cada "furo de prova" (representado por tokens sorry) em uma prova parcialmente especificada.

No ecossistema atual do Lean 4 com Mathlib, essa busca paralela é severamente limitada pela sobrecarga de inicialização de ramificações. Cada ramo de busca reconstrói atualmente o estado da prova do zero, incorrendo em dois custos massivos:

1. Carregamento de Imports: Desserialização de bibliotecas .olean pré-compiladas (Mathlib), levando aproximadamente 60 segundos por ramo.
2. Elaboração do Corpo do Teorema: Re-verificação de tipos do cabeçalho do teorema e de todas as etapas intermediárias até o objetivo final. Isso escala com a complexidade da prova, variando de 18 a 735 segundos por ramo.

Juntos, esses componentes consomem >99% do tempo de parede por ramo. Para um portfólio padrão de 7 táticas aplicadas a 4 furos (28 ramos), a sobrecarga pode exceder 17 minutos em uma única máquina, tornando a busca baseada em portfólio inviável na escala dos pipelines DSP (que podem propor 100+ candidatos de rascunho por teorema). A causa raiz é uma incompatibilidade entre o gerenciamento de estado interno do Lean (que armazena em cache estados elaborados para diagnósticos do IDE) e o acesso externo (que força uma reconstrução completa para cada novo ramo).

Metodologia

Os autores introduzem o Snapshotting do Estado da Prova, um mecanismo que captura o estado da prova elaborado uma única vez e o reutiliza em múltiplos ramos paralelos, em vez de reconstruí-lo para cada tentativa.

Arquitetura do Sistema

A solução envolve uma extensão mínima ao Language Server (LSP) do Lean 4 e uma camada de orquestração em Python:

1. Extensões do Servidor Lean: Três novos métodos JSON-RPC são adicionados ao Lean.Server.FileWorker:

   • dspSnapshotPing: Um handshake para verificar o suporte a snapshots.
   • dspSnapshotCapture: Dado um URI de arquivo e uma posição sorry, bloqueia até que a elaboração alcance esse ponto, registra uma referência de snapshot e retorna um snapshotId estável.
   • dspSnapshotBranch: Aceita um snapshotId e um array de configurações de táticas. Ele gera tarefas paralelas (IO.asTask) para cada tática, substituindo a tática pelo sorry e executando-a contra o estado de objetivo capturado.

2. Mecanismo de Forking Eficiente:

   • Ambiente Compartilhado: O Environment (contendo todas as constantes do Mathlib, instâncias de classes de tipos e conjuntos simp, aproximadamente 2–4 GB) é imutável. É compartilhado entre todos os ramos por referência e nunca copiado.
   • Contexto Copiado: Apenas o MetavarContext (obrigações de prova abertas, tipicamente alguns kilobytes) é copiado por ramo.
   • Resultado: Forkar um ramo custa apenas o tempo para copiar alguns kilobytes de memória, reduzindo a sobrecarga de memória por ramo de O(GB) para O(KB) e eliminando a RAM como um gargalo de paralelismo.

3. Integração com DSP:

   • O orquestrador em Python detecta posições sorry em um esboço gerado por LLM.
   • Captura um snapshot para cada furo.
   • Despacha todo o portfólio de táticas (por exemplo, aesop, norm_num, omega, ring, linarith, decide, simp) em uma única chamada RPC em lote.
   • O servidor distribui esses ramos em paralelo usando o escalonador de roubo de trabalho do Lean.

Posicionamento

Este trabalho define a otimização de Nível 2 na hierarquia de aceleração de busca de provas:

• Nível 0 (DSP Padrão): Reconstrução completa por ramo.
• Nível 1 (ex.: Kimina): Armazena em cache o Environment pós-importação entre teoremas, mas ainda re-elabora o corpo do teorema por ramo.
• Nível 2 (Snapshot-DSP): Armazena em cache o estado pós-elaboração (incluindo o corpo do teorema) e o fork para ramos dentro do mesmo teorema.
• Nota: Isso é ortogonal a mecanismos de backtracking intra-ramo como SavedState usado pelo Aesop.

Principais Contribuições

1. Implementação do Sistema: Um sistema de snapshotting do estado da prova compreendendo extensões LSP do Lean 4 e uma camada de orquestração em Python que permite forking leve de estados de prova para execução paralela de táticas.
2. Avaliação: Medições abrangentes de aceleração em 48 problemas miniF2F-v2, demonstrando que >99% do tempo de parede por ramo é sobrecarga eliminada por essa abordagem.
3. Lançamento de Código Aberto: O binário do Lean corrigido, o pipeline Snapshot-DSP e a suíte de avaliação são lançados como código aberto.

Resultados

Experimentos foram conduzidos em 48 problemas miniF2F-v2 (45 benchmarks feitos à mão e 3 execuções completas de ponta a ponta) em um MacBook Pro (8 GB de RAM).

• Aceleração de Tempo de Parede: A abordagem alcança uma aceleração de 5,6–50× sobre o fallback padrão (lake build por ramo).
  • Média: 14× de aceleração.
  • Mediana: 9,7× de aceleração (em 45 benchmarks feitos à mão).
• Comportamento de Escala: A aceleração escala monotonicamente com o número de ramos de prova (furos × táticas).
  • 1 furo (7 ramos): ~7,9× de aceleração.
  • 5 furos (35 ramos): ~29,8× de aceleração.
• Decomposição de Custos:
  • Execução da Tática: Representa apenas alguns milissegundos a 500 ms por ramo (percentil 95: 289 ms).
  • Sobrecarga: Os >99% restantes do tempo de execução no fallback são sobrecarga de elaboração, que o snapshotting elimina completamente.
  • Custo Nativo: A abordagem nativa de snapshot adiciona apenas 4–13 segundos de sobrecarga combinada do LSP e execução de táticas sobre o custo de captura única.

Significado e Alegações

O artigo afirma que o snapshotting do estado da prova é uma arquitetura de aceleração pura que não altera a precisão da prova ou as estratégias de busca, mas remove a barreira de escalabilidade que impede o uso de grandes portfólios de táticas em máquinas únicas.

• Viabilidade: Transforma cenários de busca inviáveis (por exemplo, 2.800 ramos levando 29 horas) em tratáveis (3,5 horas) em hardware padrão.
• Mudança Arquitetural: O trabalho serve como uma "prova de existência" de que a fronteira entre o gerenciamento de estado interno do Lean e sistemas externos de IA pode ser redesenhada. Ao expor snapshot-and-fork como uma operação de servidor de primeira classe, demonstra que a reutilização de estado no nível de elaboração é alcançável com um patch mínimo em ferramentas de produção.
• Complementaridade: O mecanismo é ortogonal ao cache no nível de importação (Nível 1). Enquanto o Nível 1 evita reinicializações do servidor entre teoremas, o Nível 2 elimina a re-elaboração do corpo do teorema entre ramos. Uma futura variante de servidor persistente combinando ambos poderia gerar ganhos adicionais, mas a implementação atual foca no gargalo de despacho de ramos.

Os autores enfatizam que isso é uma intervenção direcionada para expor a cadeia de snapshot de elaboração para reutilização externa, motivada pela observação de que o servidor Lean já computa e armazena em cache esse estado para diagnósticos do IDE, mas falha em expô-lo a orquestradores externos de busca de provas.