Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

Resumo Técnico: Prova de Teoremas Neural para Condições de Verificação (NTP4VC)

Definição do Problema
A verificação de programas é um pilar da confiabilidade de software, mas sua adoção permanece limitada a domínios de segurança crítica. Um gargalo primário é o esforço manual necessário para provar Condições de Verificação (VCs) — proposições lógicas que codificam a corretude de programas. Embora os Provadores Automáticos de Teoremas (ATPs) se destaquem em domínios específicos, eles frequentemente falham em VCs do mundo real, exigindo extensas anotações e provas manuais. Embora a Prova de Teoremas Neural (NTP) tenha mostrado promessa em competições matemáticas, sua aplicação ao domínio específico e de alto risco da prova automatizada de VCs na verificação de programas permanece amplamente inexplorada. Além disso, os benchmarks existentes para prova de teoremas costem focar em lemas auxiliares ou enigmas matemáticos, em vez das VCs diretas geradas por pipelines de verificação industrial, e carecem de suporte para múltiplas linguagens formais.

Metodologia
Os autores introduzem o NTP4VC, uma tarefa e um benchmark projetados para avaliar a capacidade de Grandes Modelos de Linguagem (LLMs) de automatizar a prova de VCs. A metodologia envolve três componentes principais:

1. Extração e Tradução de Corpus:

   • O benchmark utiliza projetos de verificação industrial existentes (ex: escalonador do kernel do Linux, alocador de memória do Contiki-OS) processados através de pipelines estabelecidos: Frama-C (para código C) e Why3 (como backend de verificação).
   • Como as VCs nativas em linguagens de NTP convencionais como Lean são escassas para projetos industriais, os autores desenvolveram um pipeline de tradução baseado em regras. Este sistema extrai VCs do Why3 e as traduz para Isabelle, Lean e Rocq (anteriormente Coq).
   • A tradução baseia-se em aproximadamente 2.400 regras de mapeamento e reescrita escritas por especialistas (por linguagem) para garantir a preservação semântica e a expressão idiomática nas linguagens alvo, evitando a falta de confiabilidade da tradução baseada em LLMs.

2. Processo de Complicação:

   • As VCs extraídas diretamente de projetos verificados são frequentemente "fáceis demais" porque desenvolvedores humanos já forneceram anotações suficientes (ex: assert, lemma e anotações de aplicação de lemas) para guiar os ATPs.
   • Para criar casos de benchmark desafiadores, os autores implementaram um processo de complicação que remove sistematicamente essas anotações auxiliares. Isso restaura as VCs a um estado mais próximo da verificação totalmente automatizada, aumentando significativamente a dificuldade enquanto mantém a provabilidade (assumindo um provador suficientemente forte).

3. Construção do Benchmark:

   • O benchmark final consiste em 600 VCs cuidadosamente selecionadas extraídas de mais de 7.500 candidatas.
   • O conjunto é equilibrado entre duas categorias:
     • Pearls of Programs (5s Pérolas de Programas) (50%): Programas funcionais mínimos que capturam pontos de dor da verificação (algoritmos, estruturas de dados, problemas de competição como o VerifyThis).
     • Real C Verification (Verificação de C Real) (50%): VCs derivadas de projetos C industriais (ex: Contiki-OS, kernel do Linux, parsers X.509).
   • A dificuldade é calibrada de modo que o ATP predefinido mais forte no Why3 (Auto_Level_3) alcance uma taxa de sucesso entre 20% e 25%, garantindo uma mistura de problemas solucionáveis e abertos.

Principais Contribuições

• Definição de NTP4VC: O artigo define formalmente a tarefa de aplicar a geração de provas baseada em aprendizado de máquina para automatizar a prova de VCs, identificando-a como um gargalo crítico na verificação de programas.
• Método de Extração Confiável: Um método inovador e de código aberto para extrair e traduzir VCs de pipelines de verificação industrial para múltiplas linguagens de ITP usando regras escritas por especialistas em vez de LLMs, garantindo fidelidade semântica.
• Primeiro Benchmark Multilingue do Mundo Real: A introdução do NTP4VC, o primeiro benchmark que visa especificamente a prova automatizada de VCs através de Isabelle, Lean e Rocq, apresentando uma mistura diversificada de casos algorítmicos e industriais.
• Avaliação Abrangente: Uma avaliação extensa de sete modelos, incluindo LLMs de propósito geral (ex: GPT-4o-mini, Qwen3) e provadores de teoremas especializados (ex: DeepSeek-Prover-V2, Goedel-Prover), além de provadores "hammer" clássicos (Sledgehammer, CoqHammer).

Resultados
A avaliação revela desafios significativos para os atuais modelos de NTP na verificação de programas:

• Baixas Taxas de Sucesso: Mesmo os melhores modelos com fine-tuning por linguagem alcançam taxas de sucesso muito baixas. O melhor modelo especializado (Minilang) atinge apenas 2,08% de pass@1 no Isabelle. Modelos de propósito geral performam ainda pior (ex: GPT-o4-mini-high com 1,19% de pass@1).
• Comparação com Hammers: Provadores baseados em hammers clássicos superam significativamente os modelos neurais. O Sledgehammer alcança 18,00% de pass@1 no Isabelle, e o CoqHammer alcança 5,67% no Rocq.
• Análise de Erros: Os modos de falha diferem dos benchmarks matemáticos. Modelos de NTP lutam com:
  • Erros Sintáticos: ~24% das provas no Isabelle falham devido a parênteses mal fechados ou problemas de sintaxe em fórmulas profundamente aninhadas.
  • Confusão Semântica: Modelos frequentemente produzem código pragmaticamente incorreto (ex: atribuições imperativas em Lean em vez de táticas declarativas) ou aplicações de táticas repetitivas e sem sentido.
  • Alucinação: Modelos frequentemente invocam táticas inexistentes (ex: why3 no Rocq) ou constantes não definidas.
• Especificidade de Domínio: Os hammers performam notavelmente melhor em tarefas de "Real C Verification" do que em "Pearls of Programs", sugerindo que técnicas de raciocínio clássico (solvers SMT) são altamente otimizadas para cenários de verificação industrial, enquanto os modelos de NTP lutam em ambos os domínios.

Significância e Alegações
O artigo afirma que o NTP4VC estabelece um benchmark fundamental para o avanço das abordagens neurais para a verificação de programas. Os resultados destacam uma lacuna substancial entre as capacidades atuais de NTP e os requisitos da verificação de programas do mundo real, indicando que a verificação de programas exige capacidades de raciocínio fundamentalmente diferentes dos problemas de competição matemática. Os autores afirmam que, embora os LLMs mostrem promessa, é necessário progresso significativo para lidar com a natureza longa, profundamente aninhada e sintaticamente rígida das VCs. O trabalho fornece uma infraestrutura necessária (benchmark e pipeline de extração) para impulsionar pesquisas futuras rumo ao fechamento dessa lacuna, potencialmente levando a avanços na verificação automatizada de programas. Os autores mantêm-se modestos, observando que os casos do benchmark derivam de projetos formalmente verificados, mas reconhecendo que bugs de implementação no pipeline de tradução poderiam, teoricamente, tornar alguns casos impossíveis de provar, embora tenham tomado extensas medidas para mitigar isso.