Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

1. O Problema

A verificação de programas depende fundamentalmente de invariantes de loop (condições que se mantêm verdadeiras antes e após cada iteração de um loop) para garantir formalmente que o software se comporta conforme o esperado. No entanto, a descoberta automática de invariantes fortes (aqueles que são não apenas corretos, mas suficientes para provar as asserções finais) é um desafio antigo e, em geral, indecidível.

Abordagens tradicionais (como resolução de restrições e análise dinâmica) muitas vezes falham em encontrar invariantes fortes o suficiente para acelerar a verificação. Trabalhos recentes tentaram usar Grandes Modelos de Linguagem (LLMs) para gerar esses invariantes, mas enfrentam duas limitações principais:

1. Avaliação Insuficiente: Trabalhos anteriores (como Pei et al., 2023) frequentemente avaliavam apenas a correção sintática ou comparavam com ferramentas de análise dinâmica (como o Daikon), o que não garante a correção formal nem a utilidade prática para acelerar o provador.
2. Complexidade Excessiva: Sistemas subsequentes tratam a saída dos LLMs como "material simbólico ruidoso", exigindo algoritmos complexos de pós-processamento (filtragem, recombinação, reparo, backtracking) para tentar transformar as saídas imperfeitas em invariantes válidos.

2. Metodologia: O Framework Quokka

O artigo introduz o Quokka, um framework orientado à avaliação para síntese de invariantes baseada em LLMs. A filosofia central é simplificar o processo: em vez de tentar "consertar" a saída do LLM, o Quokka avalia diretamente se um invariante candidato é útil.

Abordagem Baseada em Verificador

O método formaliza a tarefa usando lógica de Hoare. Para um programa $P$ e uma propriedade alvo $p^*$, o LLM propõe um invariante candidato $q$. O Quokka executa duas consultas de verificador em paralelo:

1. Validação do Invariante ($d_a$): Verifica se $q$ é um invariante correto para o programa (sem assumir nada).
2. Validação da Propriedade ($d_b$): Verifica se a propriedade alvo $p^*$ é provada assumindo que $q$ é verdadeiro.

O resultado é determinado por regras lógicas simples:

• Se $q$ é válido e $p^*$ é provada sob $q$, o sistema retorna Verdadeiro (aceleração bem-sucedida).
• Se $q$ é inválido ou $p^*$ não é provada, o sistema retorna Falso ou Inconclusivo.

Inovações de Implementação:

• Validação Direta: Elimina a necessidade de algoritmos complexos de "query-filter-reassemble" ou reparo simbólico.
• Consulta Paralela: As duas consultas de verificador são executadas simultaneamente, reduzindo a latência.
• Foco na Utilidade: O objetivo não é apenas encontrar invariantes corretos, mas invariantes que aceleram a prova da asserção final.

Geração de Dados e Ajuste Fino

• Dataset de Treino: Os autores criaram um conjunto de dados sintético de 3.589 instâncias, filtrando programas gerados por LLMs que foram validados pelo verificador UAutomizer.
• Fine-Tuning: Aplicaram Supervised Fine-Tuning (SFT) usando LoRA em modelos como o Qwen2.5-7B.
• Amostragem Best-of-N: Geram múltiplos candidatos de invariantes e selecionam aquele que resulta no menor tempo de verificação (maior aceleração).

3. Contribuições Principais

1. Framework Quokka: Um método de síntese de invariantes que fornece uma avaliação sound (correta formalmente) e atinge o estado da arte (SOTA) em desempenho, superando verificadores baseados em LLMs anteriores.
2. Novo Benchmark: Construção de um conjunto de dados com 866 instâncias derivadas do SV-COMP (competição de verificação de software), que é significativamente maior e mais complexo (com múltiplos loops, funções, arrays e ponteiros) do que os conjuntos de dados usados em trabalhos anteriores.
3. Avaliação Abrangente: Avaliação de 9 LLMs de ponta (incluindo famílias Llama, Qwen, Claude e GPT), demonstrando que o ajuste fino e a amostragem Best-of-N trazem melhorias mensuráveis.
4. Análise de Falhas: Identificação de que a maioria das falhas não é devido a invariantes incorretos, mas sim a timeouts do verificador ou invariantes triviais que não decomõem o problema.

4. Resultados Experimentais

Os experimentos foram conduzidos utilizando o verificador UAutomizer (estado da arte não baseado em LLM) como base.

• Desempenho Geral: O Quokka superou consistentemente todos os verificadores baseados em LLMs anteriores (como LaM4Inv, Clause2Inv, LEMUR e Loopy).
  • Com o modelo gpt-5.2 e amostragem Best-of-8, o Quokka resolveu significativamente mais instâncias e com tempos médios de solução muito menores do que os baselines.
  • Em um benchmark de 60 segundos, o Quokka resolveu 21 instâncias adicionais além da linha de base do UAutomizer, enquanto modelos menores resolveram menos.
• Impacto do Ajuste Fino: O fine-tuning do Qwen2.5-7B aumentou o número de invariantes corretos de 419 para 431 e melhorou o número de instâncias resolvidas adicionais.
• Amostragem Best-of-N: Aumentar o número de candidatos ($N$) de 1 para 8 resultou em ganhos contínuos de desempenho, com platô após $N=8$ devido a contenção de recursos.
• Comparação com Baselines: O Quokka demonstrou ser superior mesmo quando comparado a versões atualizadas dos baselines (ex: LEMUR e Clause2Inv rodando com o mesmo modelo gpt-5.2). A simplicidade do design do Quokka provou ser mais eficaz do que a complexidade algorítmica dos concorrentes.

5. Significado e Conclusão

O trabalho Quokka representa uma mudança de paradigma na verificação de programas assistida por LLMs. Ele demonstra que, à medida que os modelos de linguagem se tornam mais capazes, a necessidade de algoritmos complexos de "harness" para reparar saídas de LLMs diminui.

• Simplicidade e Eficácia: Um design focado na avaliação direta ("verificar se ajuda a provar") é mais robusto e eficiente do que tentar reescrever ou filtrar sintaticamente a saída do modelo.
• Validação Formal: Ao contrário de trabalhos anteriores que dependiam de análise dinâmica (potencialmente insone), o Quokka garante a correção formal através de verificadores dedutivos.
• Futuro da Pesquisa: O estudo estabelece uma nova base para a pesquisa em verificação, sugerindo que o foco deve ser na integração direta entre LLMs e verificadores formais de ponta, utilizando técnicas de amostragem e ajuste fino para maximizar a utilidade dos invariantes gerados.

Em resumo, o Quokka prova que LLMs podem acelerar significativamente a verificação de programas quando avaliados sob critérios rigorosos de utilidade prática, superando as abordagens complexas e menos eficazes do estado da arte anterior.