Evaluating LLM-Generated ACSL Annotations for Formal Verification

Titel: Evaluatie van door LLM gegenereerde ACSL-annotaties voor formele verificatie

Auteurs: Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan (Maynooth University, Ierland)

---

1. Het Probleem

Formele specificaties zijn essentieel voor het bouwen van verifieerbare en betrouwbare softwaresystemen, maar het genereren van accurate specificaties voor real-world C-programma's blijft een grote uitdaging. Hoewel kunstmatige intelligentie (AI) en grote taalmodellen (LLM's) indrukwekkende resultaten boeken in taalbegrip, ontbreekt er vaak garantie voor veiligheid en correctheid. Het handmatig schrijven en onderhouden van formele specificaties (zoals ACSL - ANSI/ISO C Specification Language) is kostbaar, tijdrovend en schaalt slecht.

De kernvraag van dit onderzoek is: In welke mate kunnen formele analyse-tools automatisch ACSL-specificaties genereren en verifiëren voor C-programma's zonder menselijke of leer-gebaseerde hulp? Er is behoefte aan empirisch bewijs dat de prestaties van geautomatiseerde methoden (zoals regelgebaseerde scripts) vergelijkt met die van moderne LLM's.

2. Methodologie

De auteurs hebben een gecontroleerde empirische studie uitgevoerd met de volgende opzet:

• Dataset: Gebruik werd gemaakt van de CASP-dataset (gepubliceerd in november 2025), bestaande uit 506 C-programma's met formeel verifieerde ACSL-specificaties. Uit deze dataset werden 355 schone C-bestanden geselecteerd voor analyse.
• Generatiestrategieën: Vijf systemen werden vergeleken op hun vermogen om ACSL-annotaties te genereren:
  1. Een regelgebaseerd Python-script.
  2. De RTE-plugin van Frama-C (Runtime Error Detection).
  3. Drie Large Language Models (LLM's): DeepSeek-V3.2, GPT-5.2 en OLMo 3.1 32B Instruct.
• Verificatie-omgeving: Alle gegenereerde specificaties werden verwerkt in het Frama-C platform (Linux omgeving).
  • Statische analyse: Uitgevoerd met de EVA-tool.
  • Verificatie: Uitgevoerd met de WP-plugin (Weakest Precondition) van Frama-C.
  • Oplossers (SMT Solvers): Vier verschillende solvers werden gebruikt om de bewijsplichten te controleren: Alt-Ergo, CVC4, CVC5 en Z3.
• Metingen: De studie evalueerde bewijssuccespercentages, het aantal time-outs (tijdslimieten), en de stabiliteit van de oplossers (gemeten via "Qed-tijd" en variantie).

3. Belangrijkste Bijdragen

• Empirische Vergelijking: Dit paper biedt een van de eerste directe, gecontroleerde vergelijkingen tussen traditionele tool-gebaseerde generatie (regels/RTE) en state-of-the-art LLM's voor ACSL-generatie.
• Nieuwe Dataset: Het repurposed de recente CASP-dataset voor een volledig geautomatiseerde evaluatie, in plaats van de gebruikelijke interactieve, mens-in-de-loop workflows.
• Nuance in Evaluatie: De auteurs tonen aan dat bewijssucces alleen niet voldoende is; de stabiliteit van de solver (tijdslimieten en consistentie) is een kritieke factor bij het beoordelen van de kwaliteit van gegenereerde specificaties.
• Benchmark voor Toekomstig Onderzoek: Het biedt een baseline voor onderzoek naar hybride workflows die LLM's combineren met formele methoden.

4. Resultaten

De resultaten tonen duidelijke trade-offs tussen expressiviteit en verificatiestabiliteit:

A. Prestaties per Generatiemethode

• Tool-gegenereerde specificaties (Python-script & RTE):
  • Bereikten de hoogste bewijssuccespercentages (RTE bereikte bijna 100% succes).
  • Toonden de laagste tijdslimieten (time-outs) en zeer lage variantie in "Qed-tijd" (tijd om een bewijs te voltooien).
  • Conclusie: Ze zijn betrouwbaar, voorspelbaar en solver-vriendelijk, maar minder expressief.
• LLM-gegenereerde specificaties:
  • DeepSeek: Toonde de beste prestaties onder de LLM's, met bewijssucces dat dicht bij de RTE-plugin lag, maar met iets meer tijdslimieten.
  • GPT-5: Had een lager succespercentage en aanzienlijk meer time-outs, vooral met de Alt-Ergo solver. De specificaties waren vaak te zwak of dubbelzinnig.
  • OLMo3: Bevond zich in het midden; het behield een redelijke stabiliteit maar introduceerde meer complexiteit dan de tools.
  • Algemeen: LLM's konden vaak syntactisch correcte ACSL genereren, maar de semantische sterkte en volledigheid varieerden sterk, wat leidde tot onvoorspelbare bewijsresultaten.

B. Prestaties per Solver

• CVC4 en CVC5: Toonden over het algemeen de meest stabiele gedrag met de laagste tijdslimieten en consistente prestaties over alle generatiemethoden heen.
• Z3: Bereikte lagere centrale variantie (sneller in gemiddelde tijd) maar vertoonde bredere fluctuaties bij complexe, door LLM gegenereerde specificaties.
• Alt-Ergo: Had over het algemeen de hoogste tijdslimieten, vooral bij de door LLM's gegenereerde annotaties, wat wijst op gevoeligheid voor ambiguïteit in de specificaties.

C. Trade-off: Expressiviteit vs. Stabiliteit

Er is een duidelijke inverse relatie gevonden:

• Hogere expressiviteit (vaak geproduceerd door LLM's) leidt tot hogere variantie in bewijstijden en meer time-outs.
• Strakke, gestructureerde methoden (regels/RTE) leveren snelle, voorspelbare en betrouwbare verificatie op, maar met minder complexiteit.

5. Betekenis en Conclusie

Dit onderzoek concludeert dat hoewel LLM's veelbelovend zijn voor het genereren van formele specificaties, ze nog niet klaar zijn voor volledig geautomatiseerde, schaalbare verificatie zonder menselijke tussenkomst of aanvullende validatiestappen.

• Betrouwbaarheid: Tool-gegenereerde specificaties (zoals RTE) vormen een degelijke basis voor automatische verificatie.
• Potentieel LLM's: LLM's kunnen expressie toevoegen, maar introduceren onzekerheid die de prestaties van SMT-solvers negatief beïnvloedt.
• Toekomstige Richting: Effectieve hybride workflows moeten een balans vinden tussen de expressiviteit van LLM's en de stabiliteit van regelgebaseerde systemen. De studie benadrukt dat "bewijssucces" niet alleen moet worden gemeten aan het aantal geslaagde bewijzen, maar ook aan de stabiliteit en efficiëntie van de onderliggende solvers.

De paper biedt een waardevol empirisch fundament voor onderzoekers die werken aan het integreren van AI in formele verificatiepipelines voor kritieke softwaresystemen.