Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

1. Il Problema

La verifica formale dei programmi si basa sulla capacità di dimostrare che un software si comporta come previsto, specialmente in domini critici per la sicurezza. Una sfida fondamentale e irrisolta da decenni è la scoperta automatica degli invarianti di ciclo.

• Invariante di ciclo: Una condizione logica che rimane vera prima, durante e dopo ogni iterazione di un ciclo.
• La difficoltà: Per accelerare la verifica, gli invarianti non devono essere solo corretti, ma anche forti (sufficienti a provare l'asserzione finale). Invarianti deboli ma corretti non riducono lo sforzo del verificatore.
• Limiti degli approcci precedenti: I metodi tradizionali (risoluzione di vincoli, analisi dinamica) hanno limiti di scalabilità. Le ricerche recenti che utilizzano i Large Language Models (LLM) per generare invarianti hanno mostrato due difetti principali:
  1. Valutano solo la correttezza sintattica o confrontano con strumenti di analisi dinamica (come Daikon), che non sono sound (sicuri) per la verifica formale.
  2. Trattano l'output degli LLM come "materiale simbolico rumoroso", richiedendo complessi algoritmi di post-elaborazione (filtraggio, ricomposizione, riparazione) per renderli utilizzabili, aumentando la complessità del sistema.

2. Metodologia: Il Framework Quokka

Gli autori introducono Quokka, un framework orientato alla valutazione che semplifica drasticamente l'uso degli LLM nella sintesi di invarianti.

Approccio "Evaluation-Centric"

A differenza dei lavori precedenti che tentano di "aggiustare" l'output dell'LLM, Quokka valuta direttamente se un invariante candidato è utile. Il processo si basa su due query parallele a un verificatore formale (UAutomizer):

1. Verifica della correttezza ($d_a$): Si verifica se la proposizione proposta dall'LLM è effettivamente un invariante valido per il programma.
2. Verifica dell'utilità ($d_b$): Si verifica se, assumendo che l'invariante sia vero, l'asserzione target del programma viene provata.

Se entrambe le condizioni sono soddisfatte, l'invariante è considerato utile e accelera la verifica. Questo approccio elimina la necessità di algoritmi complessi di riparazione o ricomposizione, spostando il carico di lavoro sulla capacità dell'LLM di generare direttamente candidati validi.

Dataset e Benchmark

• Quokka-Bench: È stato costruito un benchmark di 866 istanze derivate da SV-COMP (Software Verification Competition).
• Complessità: Rispetto ai dataset precedenti, questo include programmi più lunghi, con cicli multipli, funzioni, array e puntatori, rendendo il benchmark più sfidante e rappresentativo della realtà.
• Dati di Addestramento: Per il fine-tuning, sono stati generati 3.589 programmi sintetici filtrati dal verificatore per garantire la qualità dei dati.

Tecniche di Ottimizzazione

• Supervised Fine-Tuning (SFT): Addestramento di modelli (es. Qwen2.5-7B) su invarianti corretti estratti da UAutomizer.
• Best-of-N Sampling: Generazione di $N$ candidati invarianti e selezione di quello che porta al tempo di verifica più rapido.

3. Risultati Sperimentali

Gli autori hanno valutato 9 LLM all'avanguardia (tra cui GPT-5, Claude 4, Qwen2.5, Llama 3) e confrontato Quokka con i migliori verificatori basati su LLM esistenti (LaM4Inv, Clause2Inv, LOOPY, LEMUR).

• Prestazioni Superiori: Quokka supera costantemente i metodi precedenti. Utilizzando gpt-5.2 con Best-of-8 sampling, il sistema risolve il maggior numero di istanze aggiuntive rispetto al verificatore base (UAutomizer) e riduce drasticamente il tempo medio di risoluzione.
  • Esempio: A un timeout di 60 secondi, Quokka risolve 21 istanze in più rispetto alla baseline con gpt-5.2, mentre i metodi precedenti ne risolvono molte meno o nessuna.
• Impatto del Fine-Tuning e Best-of-N:
  • Il Fine-tuning porta a miglioramenti misurabili ma moderati nella correttezza e nella velocità.
  • Il Best-of-N mostra guadagni significativi fino a $N=8$, dopo di che i benefici si stabilizzano a causa dei vincoli di risorse.
• Analisi dei Fallimenti: La maggior parte dei fallimenti non è dovuta a invarianti errati generati dall'LLM, ma a timeout del verificatore o a invarianti generati che sono troppo banali (es. identici all'asserzione originale) o non sufficientemente forti.

4. Contributi Chiave

1. Framework Quokka: Un nuovo paradigma per la verifica basata su LLM che abbandona la complessa post-elaborazione simbolica a favore di una valutazione diretta e sound tramite verificatori formali.
2. Nuovo Benchmark: Il dataset di 866 istanze, il più grande e complesso finora utilizzato per valutare i verificatori basati su LLM, che distingue chiaramente le capacità dei diversi modelli.
3. Nuovo Stato dell'Arte (SOTA): Dimostrazione che un approccio semplice e focalizzato sulla valutazione supera metodi complessi basati su algoritmi di riparazione.
4. Analisi delle Tecniche: Evidenzia che tecniche come il Fine-tuning e il Best-of-N sampling sono efficaci per migliorare le prestazioni, fornendo linee guida pratiche per la ricerca futura.

5. Significato e Impatto

Questo lavoro segna un cambio di paradigma nella verifica assistita da LLM. Dimostra che, man mano che i modelli linguistici diventano più capaci, non è necessario costruire sistemi ibridi complessi per "correggere" i loro errori. Al contrario, un design semplice che tratta l'output dell'LLM come un candidato da validare direttamente (e non da riparare) è più efficiente e performante.

Quokka stabilisce un nuovo standard per la verifica dei programmi, offrendo una fondazione solida per futuri ricerche che mirano a integrare l'intelligenza artificiale nella verifica formale di sistemi software critici, riducendo i tempi di verifica e aumentando l'affidabilità del software.