PROMISE: Proof Automation as Structural Imitation of Human Reasoning

1. O Problema

A verificação formal de software, embora ofereça garantias matemáticas de correção para sistemas críticos (como o microkernel seL4), enfrenta um gargalo de escalabilidade. A construção de provas formais é extremamente trabalhosa, exigindo anos de esforço de especialistas e resultando em artefatos de prova que frequentemente superam o tamanho do próprio código.

Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham mostrado sucesso em outras áreas, sua aplicação na geração automática de provas formais ainda é limitada. As abordagens atuais sofrem com:

• Visão de "Shot Único" ou Busca Superficial: A maioria dos métodos trata a geração de prova como uma tarefa de geração de texto única ou uma busca rasa baseada em recuperação de informações (RAG) por similaridade textual superficial (palavras-chave).
• Falta de Escalabilidade Estrutural: Em grandes projetos de verificação (como sistemas operacionais), as provas possuem dependências profundas e interconectadas. Métodos que recuperam apenas premissas ou provas inteiras falham em capturar os padrões de evolução do estado da prova (como o raciocínio humano avança passo a passo).
• Ineficiência em Contextos Complexos: A similaridade lexical não garante que uma prova recuperada seja estruturalmente aplicável ao estado atual da prova, levando a tentativas falhas repetidas e incapacidade de escalar para sistemas grandes.

2. Metodologia: PROMISE

O PROMISE (PROof MIning via Structural Embeddings) propõe uma mudança de paradigma: em vez de gerar provas como texto estático, ele as trata como um processo de busca iterativo e estado-consciente, guiado pela similaridade estrutural de transições de estado de prova.

Arquitetura Principal

O sistema opera através de uma busca em feixe (beam search) sobre estados de prova no assistente de prova Isabelle/HOL. O processo é dividido em etapas:

1. Modelagem de Transição de Estado:

   • Uma prova é vista como uma sequência de estados ($s_0 \xrightarrow{t_1} s_1 \xrightarrow{t_2} \dots \xrightarrow{t_n} s_n$), onde cada passo aplica uma tática que transforma o estado atual (objetivos e hipóteses).
   • O PROMISE não recupera apenas "provas", mas sim trilhas de transição de estado que capturam como objetivos e suposições evoluem em provas bem-sucedidas.

2. Recuperação Híbrida (Estrutural + Nome):

   • Recuperação Estrutural (Core): O sistema constrói um banco de dados de representações estruturais de lemas. Para cada lema, ele executa a prova original, registrando os estados intermediários. Na inferência, ele recupera lemas cujos padrões de transição de estado (como a evolução do objetivo) são estruturalmente semelhantes ao estado atual. Isso é feito via embeddings e reclassificação semântica.
   • Recuperação de Nomes: Identifica quais lemas e definições concretas estão disponíveis no contexto atual (via PIDE/Isabelle) para garantir que as sugestões de táticas sejam semanticamente válidas.

3. Geração de Candidatos e Validação:

   • O LLM recebe um prompt "fundamentado" (grounded) contendo o estado atual, as premissas, e templates de táticas extraídos das provas estruturalmente similares (sem revelar os nomes dos lemas para evitar vazamento).
   • O modelo gera múltiplos candidatos de próximos passos (1-2 comandos).
   • Filtragem Estática e Verificação de Máquina: Os candidatos são normalizados, filtrados por sintaxe e, crucialmente, executados no Isabelle via uma ponte Scala-Isabelle. Apenas passos que produzem um novo estado de prova válido (reduzindo subobjetivos) são mantidos.

4. Busca em Feixe Adaptativa:

   • O sistema mantém um feixe de estados de prova promissores.
   • Uma função de pontuação (beam scoring) prioriza candidatos que reduzem o número de subobjetivos, mantêm o tamanho da prova conciso e exploram famílias de táticas diversas.
   • O processo é iterativo até que a prova seja fechada ou os limites de profundidade/budget sejam atingidos.

3. Contribuições Principais

• Nova Perspectiva de Geração de Prova: Introduz a visão de que a geração automática de provas deve ser modelada como um problema de raciocínio de processo sobre transições de estado de prova, e não apenas como recuperação de artefatos estáticos ou previsão de táticas.
• Framework PROMISE: Desenvolve um framework independente de modelo que opera sem treinamento adicional (zero-shot/few-shot), utilizando mineração estrutural para guiar a busca.
• Recuperação Baseada em Padrões de Evolução: Demonstra que recuperar padrões de como as provas evoluem (estrutura) é mais eficaz do que recuperar apenas o conteúdo textual (palavras-chave).
• Avaliação Abrangente: Realiza uma avaliação empírica extensa no benchmark seL4/l4v, comparando com sistemas de ponta como Selene e Rango.

4. Resultados Experimentais

O PROMISE foi avaliado em 223 teoremas do projeto de verificação seL4, utilizando diferentes backends de LLM (Qwen2.5-Coder-7B-Instruct, GPT-3.5-Turbo, GPT-4.1).

• Desempenho Superior: O PROMISE superou consistentemente as abordagens anteriores.
  • No modelo Qwen2.5-Coder-7B-Instruct, alcançou 77% de sucesso em tarefas P1 (fáceis) e 36% em P2 (médias), comparado a 30% e 2% do Selene ACC5, respectivamente.
  • Em média, obteve uma taxa de sucesso global de 55.7%, superando significativamente o Rango (34.0%) e o Selene (26.8%).
  • Melhorias relativas de até 186% foram observadas em certos cenários.
• Robustez entre Modelos: Diferente de outros métodos que variam drasticamente dependendo da capacidade do LLM, o PROMISE manteve desempenho estável entre modelos abertos (Qwen) e proprietários (GPT), sugerindo que a estratégia de recuperação estrutural compensa limitações do modelo.
• Caso de Uso em P3 (Difícil): No nível mais difícil (P3), o PROMISE provou 7 lemas, mais que o dobro do melhor baseline (Rango com 3).
• Exceção: O único cenário onde o PROMISE não superou o Rango foi no GPT-4.1 em tarefas P2 (diferença de 2%), possivelmente devido à rigidez excessiva do prompt de few-shot em um modelo que já possui forte capacidade de raciocínio zero-shot.

5. Significado e Impacto

O trabalho demonstra que a limitação atual da automação de provas com LLMs não é a falta de capacidade de raciocínio dos modelos, mas sim a incapacidade das abordagens atuais de gerenciar estruturas de dependência profundas e reutilizar conhecimento de prova além de provas individuais.

Ao imitar o raciocínio humano focando na evolução estrutural do estado da prova em vez da similaridade textual, o PROMISE oferece um caminho viável para escalar a verificação formal para sistemas de software do mundo real (como kernels de SO e compiladores). Isso reduz a barreira de entrada para a verificação formal, tornando-a mais acessível e menos dependente de esforço manual massivo, um passo crucial para a adoção generalizada de software com garantias de segurança e confiabilidade.