VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications

Resumo Técnico: VeriAct

1. O Problema

A especificação formal (ex: em Java Modeling Language - JML) é fundamental para garantir a confiabilidade e correção de software. No entanto, a síntese automática de especificações de alta qualidade permanece um desafio, exigindo expertise de domínio.
O problema central identificado pelos autores é a lacuna entre "verificabilidade" e "qualidade real":

• Falsa Segurança: Métodos atuais baseados em Grandes Modelos de Linguagem (LLMs) focam em fazer com que a especificação passe no verificador (ex: OpenJML).
• Limitação Crítica: Uma especificação pode passar na verificação formal sem ser correta ou completa. Por exemplo, um pós-condição trivial como ensures true passa em qualquer verificador, mas não descreve o comportamento real do código.
• Falhas Comuns: Especificações geradas por LLMs frequentemente são muito fracas (não capturam todos os casos) ou muito fortes (rejeitam entradas válidas), erros que os verificadores tradicionais não detectam porque apenas conferem a consistência lógica, não a semântica completa.
• Dependência Humana: A distinção entre especificações substantivas e triviais ainda depende de avaliação manual, o que não escala para grandes conjuntos de dados.

2. Metodologia

Os autores conduziram um estudo empírico estruturado em quatro etapas (Respostas a Questões de Pesquisa - RQs) para investigar e resolver esse problema:

• RQ1: Avaliação Empírica (Classical vs. Prompt-Based):

  • Compararam ferramentas clássicas (Houdini, Daikon) com abordagens baseadas em LLMs (SpecGen, AutoSpec, FormalBench).
  • Utilizaram dois benchmarks: SpecGenBench (120 tarefas) e FormalBench (662 tarefas).
  • Testaram 6 modelos de LLM (proprietários e open-weight) com diversas configurações de prompt (zero-shot, few-shot, CoT, etc.).
  • Métrica principal: Taxa de Verificação (VR) – fração de especificações que passam no verificador.

• RQ2: Otimização de Prompt (GEPA):

  • Investigaram se a otimização de prompts poderia melhorar a qualidade.
  • Utilizaram GEPA (Genetic-Pareto), uma técnica de evolução de prompts que usa feedback estruturado (erros de sintaxe vs. violações de verificação) para refinar iterativamente as instruções do LLM.
  • Objetivo: Empurrar a taxa de aprovação do verificador ao limite.

• RQ3: Avaliação de Qualidade Real (Spec-Harness):

  • Introduziram o Spec-Harness, um novo framework de avaliação que vai além do "passou/falhou" do verificador.
  • Métricas Propostas: Baseadas em Triplos de Hoare e testes de mutação:
    1. PostCorr (Correção do Pós-condição): A especificação aceita todas as execuções corretas?
    2. PostComp (Completude do Pós-condição): A especificação rejeita saídas incorretas (mutantes)?
    3. PreCorr (Correção do Pré-condição): A especificação aceita todas as entradas válidas?
    4. PreComp (Completude do Pré-condição): A especificação rejeita entradas inválidas?
  • Objetivo: Medir a "Taxa de Verificação Significativa" (MVR).

• RQ4: Síntese Agente-Guiada (VeriAct):

  • Propuseram o VeriAct, um framework agente que utiliza um loop fechado para síntese e reparo.
  • Funcionamento: O agente (baseado no paradigma CodeAct) gera uma especificação, executa a verificação, analisa erros e, crucialmente, roda o Spec-Harness. Se as métricas de qualidade não forem atingidas, o agente usa esse feedback estruturado para refinar a especificação iterativamente até que ela seja verificável, correta e completa.

3. Principais Contribuições

1. Evidência Empírica da Lacuna: Demonstraram que altas taxas de aprovação de verificadores não refletem a qualidade real da especificação. Especificações triviais ou incompletas passam facilmente.
2. Limites da Otimização de Prompt: Mostraram que, embora a otimização de prompts (GEPA) aumente a taxa de aprovação do verificador, ela atinge um teto e não resolve problemas de correção e completude semântica.
3. Spec-Harness: Desenvolvimento de um framework de avaliação automatizado que quantifica a correção e completude de especificações formais usando mutação de entrada/saída e verificação simbólica, expondo falhas invisíveis aos verificadores tradicionais.
4. VeriAct: Criação de um sistema agente guiado por verificação que supera as abordagens estáticas, sintetizando especificações que são não apenas verificáveis, mas semanticamente robustas.

4. Resultados

• RQ1 (Benchmarks): O Houdini (clássico) teve a maior taxa de verificação (86,7% no SpecGenBench), seguido por abordagens baseadas em LLMs. No entanto, a diferença entre a melhor configuração e a média foi grande, indicando sensibilidade excessiva ao design do prompt.
• RQ2 (Otimização): A otimização GEPA melhorou as taxas de verificação para prompts fracos, mas não para os já fortes, confirmando um teto de desempenho.
• RQ3 (Qualidade Real - O Choque): Ao aplicar o Spec-Harness, a Taxa de Verificação Significativa (MVR) colapsou.
  • O Houdini caiu de 86% de VR para apenas 2% de MVR (especificações triviais).
  • Abordagens baseadas em LLMs também sofreram quedas drásticas (ex: de ~54% VR para ~24% MVR no SpecGenBench).
  • Isso provou que a maioria das especificações "aceitas" pelos verificadores eram semânticamente vazias ou incorretas.
• RQ4 (VeriAct): O VeriAct superou todas as bases (clássicas e otimizadas).
  • No SpecGenBench, houve um ganho de +5% na MVR em relação às melhores bases.
  • No FormalBench (mais complexo), o ganho foi de +12%.
  • O agente conseguiu identificar e corrigir especificações "muito fracas" (que passavam no verificador mas falhavam no Spec-Harness) através de iterações de refinamento.

5. Significado e Impacto

Este trabalho representa uma mudança de paradigma na síntese de especificações formais:

• Mudança de Métrica: Argumenta que a métrica de sucesso não deve ser apenas "passar no verificador", mas sim a correção e completude semântica da especificação.
• Superação do Teto: Demonstra que a otimização de prompts sozinha é insuficiente; é necessário um ciclo de feedback ativo que avalia a qualidade da especificação, não apenas sua validade sintática/lógica superficial.
• Agência na Engenharia de Software: O VeriAct valida a eficácia de agentes autônomos que combinam execução de código, verificação formal e avaliação de qualidade para realizar tarefas complexas de engenharia de software que modelos estáticos não conseguem resolver sozinhos.

Em suma, o paper propõe que para garantir software confiável, devemos ir além da verificabilidade e adotar frameworks como o VeriAct e Spec-Harness para garantir que as especificações geradas realmente descrevam o comportamento desejado do sistema.