Resumo Técnico: Diversificar para Verificar

Declaração do Problema

Embora os Grandes Modelos de Linguagem (LLMs) tenham se tornado eficazes na síntese de código executável a partir de linguagem natural, a geração de software formalmente verificado permanece um desafio significativo. Em frameworks de verificação dedutiva como o Why3, a correção não é estabelecida meramente pela passagem de casos de teste; ela requer uma especificação semântica formal (contratos, pré-condições, pós-condições) e orientação de prova suficiente (invariantes, variantes, lemas) para satisfazer um provador de teoremas automatizado.

O problema central abordado é que a estrutura de implementação de um programa — especificamente sua representação de dados (ex: arrays vs. listas) e fluxo de controle (ex: recursivo vs. imperativo) — pode afetar drasticamente sua verificabilidade automatizada. Uma única semântica de nível de tarefa pode ser satisfeita por múltiplas implementações, contudo, algumas estruturas podem gerar condições de verificação intratáveis para os solvers SMT atuais, enquanto outras são facilmente prováveis. Abordagens existentes frequentemente tratam a geração de código como uma tarefa de etapa única, falhando em aproveitar o potencial da diversidade de implementação para encontrar artefatos "amigáveis à verificação".

Metodologia: Diversify2Verify

Os autores introduzem o Diversify2Verify, um pipeline baseado em LLM em estágios, projetado para gerar e verificar artefatos Why3. O pipeline decompõe o processo de geração em três estágios distintos, impondo fronteiras estritas para garantir que o sucesso da verificação não seja alcançado pelo enfraquecimento da especificação ou alteração da semântica fundamental da tarefa.

1. Arquitetura do Pipeline

• Estágio 1: Geração de Contrato.
  • Entrada: Tarefa em linguagem natural, assinatura alvo, exemplos concretos e uma representação alvo (array ou lista).
  • Processo: O LLM infere um contrato formal específico da representação (pré-condições, pós-condições, predicados auxiliares).
  • Validação: O contrato é verificado quanto ao tipo em Why3, e "lemas de teste" derivados de exemplos concretos são tentados para serem provados.
  • Política: Uma vez que um contrato passa na validação, ele é congelado. Ele serve como o alvo semântico imutável para os estágios subsequentes. O reparo é permitido apenas antes do congelamento para corrigir sintaxe, tipos ou inconsistências semânticas com os exemplos.
• Estágio 2: Geração de Implementação.
  • Processo: O pipeline gera candidatos WhyML executáveis para o mesmo contrato congelado.
  • Estratégia de Diversidade: Para cada tarefa, quatro famílias distintas de implementação são geradas:
    1. Array-Recursivo
    2. Array-Imperativo
    3. Lista-Recursivo
    4. Lista-Imperativo
  • Validação: Candidatos são filtrados por verificação de tipo e passagem em um subconjunto de testes executáveis.
  • Política: O reparo é limitado (5 tentativas) e restrito à mesma representação e família de estrutura de controle (ex: um candidato array-imperativo não pode ser reparado em um lista-recursivo).
• Estágio 3: Verificação Completa e Reparo.
  • Processo: O contrato congelado e uma implementação testada são combinados. O LLM adiciona as anotações de prova necessárias (invariantes de loop, variantes, código fantasma, asserções) para conectar o estado local do programa ao contrato global.
  • Verificação: O Why3 (com solvers SMT Z3, Alt-Ergo, CVC4) tenta descarregar todas as condições de verificação.
  • Política de Reparo: Se a verificação falhar, um reparo limitado (2 tentativas) é realizado. Os reparos são estritamente orientados à prova (fortalecimento de invariantes, adição de lemas) e devem preservar o contrato congelado e a família de implementação.

2. Construção do Benchmark

Os autores construíram um benchmark orientado à verificação derivado do LeetCodeDataset:

• Escopo: 73 tarefas envolvendo inteiros, arrays e listas.
• Critérios de Seleção: As tarefas foram filtradas para garantir que admitam contratos formais, suportem múltiplas implementações plausíveis e sejam adequadas para o raciocínio baseado em SMT.
• Escala: O benchmark produz 292 variantes de implementação (4 por tarefa).
• Nota: O benchmark é intencionalmente enviesado para tipos de dados amigáveis ao SMT para isolar o efeito da representação e da estrutura de controle na verificabilidade.

Contribuições Principais

1. Pipeline Diversify2Verify: Um pipeline de LLM em estágios que separa a inferência de contrato, a geração de implementação e a anotação de prova, impondo uma disciplina de "contrato congelado" para evitar o desvio da especificação durante o reparo.
2. Geração de Implementação Diversificada: Uma abordagem sistemática para gerar variantes recursivas e imperativas sobre ambas as representações de array e lista, permitindo a comparação direta de programas estruturalmente diferentes contra um mesmo alvo semântico.
3. Benchmark de Verificação: Um conjunto curado de 73 tarefas com 292 artefatos gerados, incluindo contratos aceitos, implementações WhyML e logs de verificação, disponibilizados publicamente.
4. Estudo Empírico de Verificabilidade: Uma análise quantificando como o sucesso da verificação varia por representação e estilo de implementação, e medindo os ganhos da geração de múltiplas variantes.

Resultados

A avaliação demonstra que a diversidade de implementação melhora significativamente a taxa de sucesso da verificação automatizada:

• Verificação ao Nível de Artefato:
  • Inicial: 96 de 292 artefatos (32,9%) verificados sem reparo.
  • Após o Reparo: 154 de 292 artefatos (52,7%) verificados após duas passagens de reparo.
  • Impacto do Reparo: O reparo foi responsável por verificar 58 artefatos adicionais, com a primeira passagem gerando o maior ganho.
• Verificação ao Nível de Tarefa:
  • Pelo menos uma variante verificou para 49 das 73 tarefas, alcançando uma taxa de sucesso de 67,1% ao nível da tarefa.
  • A família individual mais forte (Array-Recursivo) verificou 44 tarefas.
  • Isso indica que a diversidade fornece um aumento mensurável na cobertura de tarefas; confiar em um único estilo de implementação perderia muitas tarefas solucionáveis.
• Diferenças Estruturais:
  • Recursivo vs. Imperativo: Variantes recursivas verificaram com mais frequência (60,3% para arrays, 54,8% para listas) do que variantes imperativas (47,9% para ambos). Isso é atribuído ao fato de implementações recursivas frequentemente se alinharem melhor com especificações recursivas, enquanto implementações imperativas exigem invariantes de loop complexos para resumir o estado mutável.
  • Array vs. Lista: As taxas de verificação agregadas para arrays e listas foram semelhantes, sugerindo que a escolha da estrutura de controle (recursivo vs. imperativo) tem um efeito mais pronunciado do que a escolha da representação de dados neste contexto.
• Análise de Falha:
  • A maioria dos artefatos não verificados (138 restantes) possuía pouquíssimas obrigações de prova restantes (média de 2,5 metas raiz), sugerindo que as falhas foram causadas por falta de andaimes de prova (ex: invariantes específicos) e não por implementações fundamentalmente incorretas.
  • Uma auditoria manual confirmou que o pipeline preservou com sucesso os contratos congelados em 291 de 292 casos, ocorrendo apenas uma instância onde o LLM adicionou pré-condições não presentes no contrato original.

Significância e Alegações

O artigo afirma que implementações equivalentes em nível de tarefa podem diferir substancialmente em verificabilidade. A hipótese central é apoiada: gerar variantes diversas aumenta a probabilidade de encontrar uma implementação cuja estrutura seja propícia à verificação dedutiva automatizada.

Os autores enfatizam que esta abordagem não depende de uma única geração "perfeita", mas sim da diversidade como uma ferramenta prática para navegar no espaço de condições de verificação. Ao desacoplar a geração de especificação da geração de implementação e impor fronteiras estritas durante o reparo, o sistema garante que o sucesso da verificação não seja alcançado pelo enfraquecimento da especificação ou pela mudança da semântica da tarefa.

O trabalho sugere que, para a programação verificada assistida por LLM, a diversidade de implementação é um mecanismo poderoso para melhorar a cobertura de tarefas, particularmente quando combinada com reparo orientado pelo verificador e limitado. Os autores observam que estas descobertas são específicas ao contexto de tarefas de inteiros e sequências usando Why3 e sugerem que trabalhos futuros explorem estruturas de dados mais ricas e outros frameworks de verificação.