Technische Samenvatting: Neuro-symbolische Softwareverificatie met VerIbmc

Probleemstelling

De synthese van loopinvarianten blijft een centrale flessenhals in formele softwareverificatie. Hoewel symbolische technieken (bijv. abstracte interpretatie, constraint solving) en data-gestuurde "guess-and-check"-methoden bestaan, worstelen deze vaak met schaalbaarheid, expressiviteit of de diversiteit van echte code. Recentelijk hebben Large Language Models (LLM's) veelbelovend gebleken bij het genereren van kandidaat-invarianten door gebruik te maken van geleerde patronen uit code-corpora. Echter, bestaande neuro-symbolische benaderingen vertrouwen doorgaans op propriëtaire, gesloten modellen die via externe cloud-API's worden ontsloten. Deze afhankelijkheid introduceert aanzienlijke hindernissen voor industriële implementatie:

1. Privacy en Compliance: Broncode moet naar derde partijen worden verzonden, wat zorgen oproept over vertrouwelijkheid.
2. Reproduceerbaarheid: Afhankelijkheid van externe leveranciers bemoeilijkt integratie in gecontroleerde verificatiepipelines.
3. Kosten en Duurzaamheid: Grote modellen zijn computationeel duur en energie-intensief, wat hun praktische bruikbaarheid voor continue verificatieworkflows beperkt.

De auteurs stellen dat deze uitdagingen een verschuiving noodzakelijk maken naar lokaal inzetbare, open-weight taalmodellen die volledig binnen de infrastructuur van een organisatie kunnen opereren zonder propriëtaire code bloot te leggen.

Methodologie: De VerIbmc Pipeline

Het artikel presenteert VerIbmc, een neuro-symbolische pipeline ontworpen voor de synthese van loopinvarianten voor C-programma's door symbolisch redeneren te koppelen aan lokaal gehoste open-weight LLM's. Het systeem gebruikt ESBMC (Efficient SMT-Based Context-Bounded Model Checker) als de verificatie-oracle. De pipeline is ontworpen volgens het principe "escaleer alleen wanneer nodig", waarbij prioriteit wordt gegeven aan goedkope, deterministische symbolische redenering voordat de LLM wordt aangeroepen.

Kernarchitectuur

De pipeline werkt in drie afzonderlijke fasen:

1. Fase 0 (Baseline Verificatie): ESBMC verifieert het niet-geannoteerde programma. Als het programma triviaal veilig of bewezen onveilig is, stopt het proces onmiddellijk, waardoor onnodige synthese-inspanning wordt vermeden.
2. Fase 1 (Symbolische Kandidaatgeneratie): Als Fase 0 "Unknown" teruggeeft, enumereert het systeem symbolisch atomaire kandidaat-invarianten door middel van paarwijze vergelijking van loop-entry variabelen en constanten. Deze atomen worden op inductiviteit geverifieerd met ESBMC. Het systeem onderhoudt drie opslagplaatsen: Bewijsbaar ($P$), Weerlegbaar ($D$) en Onbekend ($U$). Als de conjunctie van alle bewijsbare atomen volstaat om de postconditie te bewijzen, wordt de pipeline succesvol afgerond zonder een LLM-aanroep.
3. Fase 2 (LLM Verfijningslus): Indien de symbolische fase onvoldoende is, gaat de pipeline een iteratieve lus binnen waarbij een LLM wordt geprompt om nieuwe invarianten te genereren.
   • Feedbackmechanisme: De LLM ontvangt het huidige programma, de inhoud van de $P$, $D$, en $U$ opslagplaatsen als gestructureerde feedback, en few-shot voorbeelden.
   • Decompositie en Recombinatie: Wanneer een door een LLM gegenereerde kandidaat de verificatie faalt, wordt deze gedecomposeerd in subformules (atomen). Atomen worden individueel geverifieerd en toegevoegd aan de juiste opslagplaatsen. De conjunctie van alle momenteel bewijsbare atomen wordt vervolgens opnieuw geverifieerd. Dit maakt het systeem in staat om nuttige componenten van mislukte LLM-voorstellen te behouden.
   • Terminatie: De lus gaat door totdat een geldige invariant wordt gevonden, het iteratiebudget is uitgeput, of een timeout optreedt.

Inferentiestrategieën

De auteurs evalueren vier inferentiestrategieën gebaseerd op twee ontwerpaspecten:

1. Verifier Feedback (Symbolische Prior):
   • Basic: Voert de volledige driefasige pipeline uit, gebruikmakend van de symbolische prior van Fase 1 en atomaire filtering.
   • LLM-Only: Slaat Fase 1 en atomaire decompositie over, en vertrouwt uitsluitend op de LLM om als geheel inductieve invarianten te genereren. Dit dient als een ablatiestandaard.
2. Redeneerstructuur:
   • Chain-of-Thought (CoT): Gebruikt standaard prompting met stapsgewijze redeneer-voorbeelden (Inductief, Hoare Logica, Horn Clause, of directe afleiding).
   • Tree-of-Thoughts (ToT): Verkent parallel meerdere afleidingsstijlen tijdens een "scouting"-fase, scoort ze op basis van het aantal gegenereerde bewijsbare atomen, en concentreert het resterende iteratiebudget op de top-twee presterende stijlen.

Belangrijkste Bijdragen

1. Neuro-symbolische Pipeline: Een compleet systeem dat lokaal geserveerde open-weight LLM's integreert met ESBMC voor geautomatiseerde loop-invariant synthese, volledig werkend op interne infrastructuur.
2. Systematische Evaluatie van Strategieën: Een uitgebreide vergelijking van pure LLM, symbolisch-gestuurde, en Tree-of-Thoughts (ToT) varianten, die de impact van symbolische feedback en redeneerstructuren aantoont.
3. Winst door Symbolische Feedback: Demonstratie dat het verstrekken van bewijsbare invariant-atomen als context aan de LLM consistente winsten oplevert, met name voor zwakkere modellen (bijv. Llama-3.1-8B wint +35 opgeloste benchmarks ten opzien van een pure-LLM baseline).
4. Prompt Engineering Analyse: Evaluatie van verschillende prompting-stijlen (CoT vs. ToT) en redeneertemplates (Inductief, Hoare Logica, Horn Clause) op invariant-synthese.
5. Grootschalige Benchmarking: Een uitgebreide evaluatie over vijf open-weight modellen (7B tot 120B parameters), vier inferentiestrategieën en vijf benchmarkfamilies (520 problemen, waarvan 499 effectief), wat neerkomt op 10.400 per-probleem uitkomsten.

Experimentele Resultaten

De evaluatie werd uitgevoerd op een server met vier NVIDIA RTX A6000 GPU's met behulp van vijf open-weight modellen: GPT-OSS-120B, GPT-OSS-20B, Qwen2.5-32B, Qwen2.5-7B, en Llama-3.1-8B.

• Algemene Prestaties: De beste enkele configuratie (GPT-OSS-120B met de Basic strategie) loste 431 van de 499 problemen op (86,4%).
• Vergelijking met State-of-the-Art (SOTA):
  • VerIbmc presteert aanzienlijk beter dan traditionele symbolische tools (CPA-Checker, 2ls, ESBMC-Kind) en neurale-only tools (Code2Inv) wanneer deze op dezelfde lokale hardware worden gedraaid.
  • Op gedeelde benchmark-suites is VerIbmc competitief met of ligt het iets onder de sterkste LLM-geaugmenteerde tools (Clause2Inv, LaM4Inv, LORIS) die dure externe API's (bijv. GPT-4) gebruiken. Opvallend genoeg bereikt VerIbmc deze resultaten zonder code naar de cloud te verzenden.
  • VerIbmc schaalt uniek naar de volledige SV-COMP benchmark set (154 problemen), inclusief programma's met arrays, geneste loops en pointers, waar veel concurrerende tools vanwege frontend-beperkingen niet toe in staat zijn.
• Impact van de Symbolische Fase: De symbolische Fase 1 loste 75 problemen op zonder enige LLM-aanroep. Voor zwakkere modellen zorgde de symbolische augmentatie voor significante verbeteringen (tot wel +35 extra opgeloste problemen voor Llama-3.1-8B).
• ToT vs. CoT: ToT-prompting toonde een diversiteit-accuratesse trade-off. Hoewel het unieke probleem-model paren bereikte die ontoegankelijk waren voor CoT, bracht het vaak een wall-clock overhead met zich mee en resulteerde het bij zwakkere modellen in een netto afname van opgelde problemen door uitputting van het iteratiebudget. Voor de sterkste modellen (GPT-OSS-120B) was het verschil in prestatie tussen CoT en ToT verwaarloosbaar.
• Modelcapaciteit: De resultaten geven aan dat modelcapaciteit de primaire drijfveer is voor accuratesse. De kloof tussen de sterkste en zwakste modellen was aanzienlijk groter dan de prestatievariantie geïntroduceerd door het wijzigen van strategieën binnen hetzelfde model.

Betekenis en Claims

Het artikel claimt dat VerIbmc aantoont dat een neuro-symbolische benadering gebaseerd op LLM's effectief kan worden toegepast op invariant-synthese op een privacy-bewuste en energie-efficiënte wijze. Door volledig op lokale infrastructuur te werken met open-weight modellen, elimineert de aanpak de noodzaak voor dure propriëtaire frontier modellen die achter API's vergrendeld zitten.

De auteurs benadrukken dat hun methode sound by construction is: elke kandidaat-invariant wordt door een formele verifieerder (ESBE) gecontroleerd voordat deze wordt geaccepteerd. Hoewel het systeem incompleet is vanwege de onbeslisbaarheid van het probleem, biedt het een praktisch, schaalbaar en reproduceerbaar pad voor AI-ondersteunde formele verificatie van productie-software. Het werk zet een stap richting industrie-klare verificatiepipelines waar gegevensprivacy en resource-efficiëntie kritieke vereisten zijn.