Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

Probleemstelling

Programma-verificatie (program verification) is essentieel voor het garanderen van de correctheid van software, vooral in veiligheidskritieke domeinen. Een van de langdurigste uitdagingen op dit gebied is het automatisch ontdekken van loop-invarianten (lus-invarianten). Een loop-invariant is een logische voorwaarde die waar is voor en na elke iteratie van een lus. Om een verificatie te versnellen, moeten deze invarianten niet alleen correct zijn, maar ook sterk genoeg om de eindassertie te bewijzen.

Bestaande methoden hebben twee grote tekortkomingen:

1. Traditionele methoden (zoals constraint solving of abstracte interpretatie) zijn vaak complex en hebben moeite met complexe programma's.
2. Eerdere LLM-benaderingen (zoals Pei et al., 2023) hebben twee fundamentele beperkingen:
   • Ze testen vaak alleen de correctheid van de gegenereerde invariant, niet of deze daadwerkelijk de verificatie versnelt.
   • Ze gebruiken dynamische analyse-tools (zoals Daikon) voor validatie, wat onzeker (unsound) is omdat deze tools invariants afleiden uit testruns in plaats van formele verificatie.
   • Andere recente werken (zoals LaM4Inv, LEMUR, Loopy) behandelen de output van LLM's als "ruis" die complexe post-processing, filtering en herstel-algoritmen vereist voordat ze bruikbaar zijn. Dit maakt de systemen zwaar en complex.

Methodologie: Quokka

Het paper introduceert Quokka, een evaluatie-gericht framework dat LLM's gebruikt om loop-invarianten te synthetiseren met als doel de verificatie direct te versnellen.

Kernprincipes:

• Evaluatie-centric Design: In plaats van complexe algoritmen te gebruiken om LLM-outputs te repareren, valideert Quokka direct of een gegenereerde invariant helpt bij het bewijzen van de doelstelling.
• Sound Verificatie: Quokka gebruikt een formele verifier (UAutomizer) in plaats van dynamische analyse.
• Het Verificatieproces: Voor een programma $P$ en een doel-eigenschap $p^*$, stelt een LLM een kandidaat-invariant $q$ voor. Quokka voert twee parallelle verificatie-query's uit:
  1. Correctheid: Is $q$ een geldige invariant? (Verificatie van $P$ zonder extra aannames, maar met assertie $q$).
  2. Bruikbaarheid: Geldt de doel-eigenschap $p^*$ als we $q$ als aanname (assumption) toevoegen?
• Beslissingslogica:
  • Als de doel-eigenschap faalt zelfs met de aanname $q$, is het doel vals.
  • Als $q$ correct is én de doel-eigenschap wordt bewezen onder $q$, dan is het doel bewezen.
  • Anders is het resultaat inconclusief (bijv. door time-outs).
• Geen complexe post-processing: Er wordt geen "query-filter-reassemble" strategie gebruikt. De LLM moet direct een bruikbare invariant leveren.

Data en Training:

• Benchmark: Er is een dataset van 866 instances geconstrueerd, afgeleid van de SV-COMP (Software Verification Competition). Dit is de grootste dataset tot nu toe voor LLM-verificatie en bevat complexere programma's (meerdere lussen, functies, arrays, pointers) dan eerdere datasets.
• Training: Er is een synthetische dataset van 3589 instances gegenereerd door seed-programma's uit SV-COMP te gebruiken en deze te filteren via de solver.
• Technieken: Het paper onderzoekt Supervised Fine-Tuning (SFT) met LoRA en Best-of-N sampling (het genereren van meerdere kandidaten en het selecteren van de snelste).

Belangrijkste Resultaten

De auteurs hebben 9 state-of-the-art LLM's geëvalueerd (waaronder GPT-5, Claude 3.5/4, Qwen2.5, Llama 3.1).

1. Superieure Prestaties: Quokka presteert consequent beter dan alle eerdere LLM-gebaseerde verificatoren (zoals LEMUR, Clause2Inv, Loopy).
   • Op de benchmark lost Quokka met gpt-5.2 en Best-of-8 sampling het grootste aantal extra instances op vergeleken met de baseline solver (UAutomizer).
   • Het bereikt state-of-the-art resultaten in zowel het aantal opgeloste instances als de gemiddelde oplostijd.
2. Effectiviteit van Sampling: Best-of-N sampling bleek zeer effectief. De prestaties verbeterden tot $N=8$, waarbij de snelste verificatietijd werd gevonden. Boven $N=8$ namen de voordelen af door resource-contentie.
3. Fine-Tuning: Supervised fine-tuning op de gegenereerde dataset leverde bescheiden maar meetbare verbeteringen op in zowel correctheid als snelheid.
4. Analyse van Fouten: De meeste fouten waren geen incorrecte invarianten, maar time-outs. Vaak genereerden LLM's invarianten die te triviaal waren (geen decompositie van het probleem) of identiek aan de oorspronkelijke assertie, waardoor ze geen versnelling boden.
5. Vergelijking met Bestaande Werk: Eerdere methoden die complexe herstel-algoritmen gebruiken, presteerden slechter dan Quokka's simpele, directe validatie-aanpak. Dit suggereert dat LLM's tegenwoordig capabel genoeg zijn om direct bruikbare invarianten te genereren zonder zware symbolische reparatie.

Bijdragen

1. Quokka Framework: Een nieuw, sound en evaluatie-gericht framework voor LLM-based invariant synthesis dat direct meet of een invariant de verificatie versnelt.
2. Nieuwe Benchmark: Een uitgebreide dataset van 866 complexe instances, aanzienlijk uitdagender dan bestaande datasets.
3. Empirische Evaluatie: Een grondige evaluatie van 9 LLM's, waarbij wordt aangetoond dat grotere en nieuwere modellen significant beter presteren.
4. Technische Inzichten: Bewijs dat simpele, evaluatie-gerichte ontwerpen superieur zijn aan complexe, "harness-heavy" systemen voor LLM-verificatie, en dat Best-of-N sampling een effectieve strategie is.

Significantie

Dit werk markeert een verschuiving in hoe LLM's worden geïntegreerd in formele verificatie. Het toont aan dat we niet langer complexe symbolische "reddingsoperaties" nodig hebben om LLM-outputs bruikbaar te maken. In plaats daarvan kunnen we vertrouwen op de directe validatie van LLM-generaties door een formele solver. Quokka stelt een nieuwe standaard (state-of-the-art) voor LLM-based program verification en biedt een fundamenteel onderbouwde basis voor toekomstig onderzoek, waarbij de focus ligt op het vinden van invarianten die de verificatie daadwerkelijk versnellen in plaats van alleen correct zijn.