Technische Samenvatting: Een Empirische Studie naar door LLM's gegenereerde Specificaties voor VeriFast

Probleemstelling

Statische verificatietools, met name die gebaseerd op Separation Logic (SL) zoals VeriFast, zijn in staat om industriële schaal software te verifiëren op functionele correctheid en geheugenveiligheid. De adoptie ervan wordt echter gehinderd door de aanzienlijke menselijke arbeid die nodig is om specificaties te schrijven. In tegenstelling tot niet-SL verifiers, vereisen SL verifiers complexe hulp-specificaties — inclusief loop-invarianten, inductieve lemma's en expliciete "folds" en "unfolds" (openen en sluiten) van predicaten — om over heap-structuren en eigendom (ownership) te redeneren. Terwijl recent onderzoek succesvol LLM's heeft toegepast voor het genereren van specificaties voor niet-SL verifiers (bijv. Dafny, Frama-C), is er een gebrek aan empirische evaluatie met betrekking tot hun vermogen om specificaties te genereren voor SL-gebaseerde verifiers, die unieke redeneerpatronen vereisen met betrekking tot heap-disjointheid en eigendom.

Methodologie

De auteurs voerden een twee-fasen empirische studie uit om de prestaties van LLM's te evalueren bij het genereren van specificaties voor de SL verifier VeriFast.

Dataset Constructie:
De studie maakte gebruik van een dataset van 303 functies uit 60 C-programma's. Voor elke functie werden vier versies gemaakt:

1. Ground Truth: Volledig gespecificeerd en geverifieerd met VeriFast.
2. Natural Language (NL): Broncode met informele natuurlijke taalbeschrijvingen van het gedrag.
3. Functional Behavior (FB): Broncode met formele pre- en postcondities in de specificatietaal van VeriFast.
4. Functional Behavior Plus (FBP): Broncode met formele pre/postcondities plus aanvullende constructen die vereist zijn voor verificatie (bijv. status van geheugenallocatie, integer-grenzen).

Experimenteel Ontwerp:
De studie verliep in twee fasen:

1. Pilot Studies: Uitgevoerd op een subset van 45 functies (uit 10 door de auteurs ontwikkelde programma's) om de optimale configuratie te selecteren.

   • Prompting Benaderingen: Acht benaderingen werden getest, waaronder Basic, Chain-of-Thought (CoT), RAG-sparse en RAG-dense, met variaties in input-granulariteit (gehele programma versus enkele functie).
   • LLM Selectie: Tien LLM's werden geëvalueerd. Op basis van verificatiesuccesratio's, foutenservereit en behoud van functioneel gedrag, werden drie modellen geselecteerd voor de volledige studie: Claude 3.7 Sonnet, Gemini 2.5 Pro, en GPT-4o.
   • Selectieresultaat: De RAG-sparse benadering met input splitting (het verwerken van één functie tegelijk) werd gekozen als de meest effectieve prompting-strategie.

2. Volledige Studie: De geselecteerde prompt en drie LLM's werden toegepast op de volledige dataset van 303 functies over alle drie de inputtypen (NL, FB, FBP), wat resulteerde in 2.727 output-functies.

Analyse Metrieken:

• RQ1 (Functioneel Gedrag): Kwalitatieve analyse van of de LLM de broncode heeft gewijzigd of de pre/postcondities heeft verzwakt/versterkt ten opzichte van de input.
• RQ2 (Verifieerbaarheid): Kwantitatieve meting van het percentage gegenereerde specificaties dat succesvol is geverifieerd met VeriFast.
• RQ3 (Fouten): Een diepgaande analyse van 354 falende functies (gesampled om de distributie van taalfuncties te vertegenwoordigen), waarbij fouten handmatig zijn gerepareerd om ze te categoriseren naar ernst (Compile, Praktisch, Theoretisch) en locatie (bijv. predicaten, loop-invarianten, open/close statements).

Belangrijkste Bijdragen

1. Eerste Empirische Studie op SL Verifiers: Dit is de eerste grondige evaluatie van LLM's die specificaties genereren voor een SL verifier (VeriFast), waarbij 8 prompting-benaderingen, 10 LLM's en 3 inputtypen worden behandeld.
2. Uitgebreide Dataset: Een publiekelijk beschikbare dataset van 60 C-programma's (303 functies) met vier varianten van specificaties (inclusief ground truth) om toekomstig onderzoek te faciliteren.
3. Granulaire Foutanalyse: Een gedetailleerde taxonomie van verificatiefouten, waarbij onderscheid wordt gemaakt tussen compilerfouten, praktische redeneerfouten (bijv. ontbrekende heap-chunks) en theoretische logische inconsistenties, inclusioneel met door mensen gecodeerde fixes.
4. Actiegerichte Inzichten: Specifieke richtlijnen voor het optimaliseren van LLM-gebaseerde verificatie-omgevingen, inclusclusief de voordelen van formele input-specificaties en het nut van de auto-features van VeriFast.

Resultaten

Behoud van Functioneel Gedrag (RQ1):

• LLM's behielden grotendeels het beoogde functionele gedrag.
• Broncode: 91,0% van de outputs bleef ongewijzigd; 9,0% bevatte wijzigingen (voornamelijk kleine semantische edities of gehallucineerde headers).
• Specificaties: 92% van de pre- en postcondities behield het functionele gedrag (equivalent of versterkt).
• Impact van Input: Formele inputs (FB/FBP) resulteerden in hogere behoudpercentages dan Natural Language (NL) inputs. Gemini 2.5 Pro vertoonde de hoogste robuustheid tegen ambiguïteit.

Verifieerbaarheid (RQ2):

• De algehele verificatiesuccesratio was 31,4% (ongeveer 1 op de 3 functies).
• Inputtype: Succesratio's correleerden met de volledigheid van de input: FBP (39,9%) > FB (29,5%) > NL (24,6%).
• Modelprestaties: Gemini 2.5 Pro presteerde beter dan de anderen (39,7% gemiddelde succes) vergeleken met Claude 3.7 (29,8%) en GPT-4o (24,5%).
• Complexiteit: Succesratio's daalden significant voor complexe functies: Normale SL (51,2%) > Recursieve Predicaten (30,9%) > Concurrency (12,3%) en Loops (11,4%).

Foutanalyse (RQ3):

• Foutenverdeling: Van de 1.652 geanalyseerde fouten waren 71% Praktisch (onvoldoende voor geautomatiseerd redeneren, bijv. ontbrekende open/close statements), 23% waren Compile fouten, en slechts 6% waren Theoretisch (logische inconsistenties).
• Oorzaken: De overgrote meerderheid van de fouten (94%) kwam voort uit een gebrek aan domeinspecifieke kennis over de mechanica van de SL verifier (syntax, heap-redenering, eigendom-tracking) in plaats van algemene logische redeneerfouten.
• Specifieke Falen: Veelvoorkomende problemen omvatten ontbrekende malloc_block annotaties, onjuiste plaatsing van pre/postcondities, en het niet leveren van noodzakelijke loop-invarianten of lemma's voor de transitiviteit van heap-segmenten.
• Verschillen tussen Modellen: Gemini 2.5 produceerde de minste fouten in alle categorieën, met name in theoretisch en praktisch redeneren.

Betekenis en Claims

Het artikel claimt dat hoewel LLM's in staat zijn om het functionele gedrag van broncode en specificaties te behouden, ze momenteel slechts bescheiden succes boeken bij het genereren van volledig verifieerbare specificaties voor separation logic tools. De primaire bottleneck is niet algemeen redeneren, maar een gebrek aan specifieke kennis over de hulp-specificatiepatronen die uniek zijn voor SL verifiers (bijv. het beheren van heap-eigendom via open/close en lemma's).

De auteurs concluderen dat:

1. Formele Inputs Belangrijk Zijn: Het verstrekken van formele contracten (FB/FBP) verbetert de succesratio's aanzienlijk vergeleken met natuurlijke taal.
2. Modelselectie Cruciaal Is: Gemini 2.5 Pro is momenteel het superieure model voor deze taak, vooral voor complexe functies zoals concurrency en loops, ondanks een hogere kostenpost.
3. Verbetering van Tooling: Om de prestaties van LLM's te verbeteren, zouden SL verifiers betere debugging-informatie (bijv. symbolische heap-states) moeten blootstellen aan LLM's tijdens repair-loops, en hybride benaderingen moeten gebruiken waarbij symbolische tools (zoals de auto-feature van VeriFast) eenvoudige open/close generatie afhandelen terwijl LLM's complexe redenering uitvoeren.

De studie claimt niet dat LLM's momenteel menselijke experts kunnen vervangen voor SL verificatie, maar biedt een baseline en specifieke richtlijnen voor het bouwen van toekomstige AI-ondersteunde verificatie-omgevingen.