Can Large Language Models Model Programs Formally?

Probleemstelling

In het digitale tijdperk is het garanderen van de correctheid, veiligheid en betrouwbaarheid van software via formele verificatie van cruciaal belang, vooral omdat software de ruggengraat vormt van kritieke infrastructuur. Formele verificatie bestaat voornamelijk uit twee benaderingen: theorema-bewijzen (theorem proving) en model checking.

Hoewel er aanzienlijke vooruitgang is geboekt bij het gebruik van Large Language Models (LLM's) voor het ondersteunen van theorema-bewijzen (bijvoorbeeld via autoformalisatie), blijft model checking achter. De belangrijkste bottleneck is de moeilijkheid om automatisch nauwkeurige en hanteerbare gedragsmodellen af te leiden uit bestaande code. Vooral bij dynamische talen zoals Python, met complexe runtime-gedragingen (zoals mutabele aliassen, hogere-orde functies en asynchrone operaties), is het lastig om een eindige maar trouwe toestandsruimte te abstraheren. Er is een gebrek aan benchmarks en methoden om LLM's te evalueren op hun vermogen om broncode direct om te zetten in verificatie-klare specificaties voor model checking.

Methodologie: Model-Bench

Om deze kloof te dichten, stellen de auteurs Model-Bench voor. Dit is een benchmark en een bijbehorende pipeline voor het evalueren en verbeteren van het vermogen van LLM's om Python-programma's te modelleren naar verificatie-klare TLA+ (Temporal Logic of Actions) specificaties, die kunnen worden gecontroleerd door de model checker TLC.

De aanpak omvat de volgende stappen:

1. Data Collectie en Verwerking:

   • De dataset bestaat uit 400 Python-programma's afgeleid van drie bekende benchmarks: HumanEval, MBPP en LiveCodeBench.
   • Een strikt filteringsproces is toegepast om de data geschikt te maken voor TLA+:
     • Bibliotheken: Alleen typing en math zijn toegestaan; andere imports zijn verwijderd.
     • Taalfeatures: Complexe features (zoals recursie, list comprehensions, classes) zijn herschreven of vereenvoudigd.
     • Typen: Variabelen met complexe typen zijn geëlimineerd; alleen basis typen (None, Number, String, List, Tuple, Dict, Iter) worden behouden.
     • Validatie: Alle geselecteerde programma's worden uitgevoerd om de functionaliteit te verifiëren.
   • De dataset bevat in totaal 1.639 testgevallen om de correctheid van de gegenereerde modellen te valideren.

2. Code-transformatie (Code Transformation):

   • Omdat Python en TLA+ fundamenteel verschillende uitvoeringsmodellen hebben, introduceren de auteurs een transformatiestap.
   • Python-code wordt omgezet naar een Control-Flow Graph (CFG) en vervolgens herschreven naar een toestandsmachinepatroon.
   • In deze getransformeerde code worden alle variabelen expliciet gedeclareerd en wordt een pc (program counter) variabele gebruikt om de huidige staat te volgen. De logica wordt uitgedrukt als een reeks if-statements binnen een while-lus, wat de structuur van TLA+ acties nabootst.
   • Dit proces is deterministisch en behoudt de semantiek van het oorspronkelijke programma.

3. Experimenteel Ontwerp:

   • Verschillende LLM's (waaronder DeepSeek-V3, Qwen3, Gemma, Llama) worden getest onder drie prompt-configuraties:
     1. Originele code (Zero-shot).
     2. Originele code met voorbeelden (Few-shot).
     3. Getransformeerde code met voorbeelden (Few-shot).
   • De modellen ondergaan iteratieve zelfcorrectie via foutfeedback.

4. Evaluatiemetrics:

   • Runnable@k: Het percentage gegenereerde modellen dat ten minste één keer succesvol wordt geverifieerd door TLC binnen $k$ pogingen.
   • State Similarity: Een maatstaf voor de overeenkomst tussen de toestandsruimte van het gegenereerde model en het "oracle" (handmatig geverifieerd) model. Dit wordt berekend als de overlap van waargenomen toestanden, waarbij een drempelwaarde ($\theta = 1.0$) wordt gebruikt om te garanderen dat alle variabele-waardeparen in het gegenereerde model ook in het oracle-model voorkomen.

Belangrijkste Resultaten

De uitgebreide experimenten leiden tot de volgende bevindingen:

• Algemene Prestaties (RQ1):

  • De prestaties zijn beperkt. Zelfs de beste modellen (DeepSeek-V3) bereiken slechts een Runnable@1 van 51,75% (bij Few-shot prompting).
  • De gemiddelde State Similarity voor de beste modellen ligt rond de 49,55%.
  • Few-shot learning heeft een aanzienlijk positief effect: modellen presteren veel beter met voorbeelden dan zonder (bijv. een stijging van ~9% naar ~27% in Runnable@1 voor de gemiddelde prestatie). Zonder voorbeelden (Zero-shot) zakken veel modellen naar bijna 0% succes.

• Effectiviteit van Code-transformatie (RQ2):

  • Het gebruik van getransformeerde code leidt tot een daling in het percentage runnable modellen (vanwege de langere context en complexere structuur), maar een significante stijging in de State Similarity (bijv. +18,99% voor DeepSeek-V3).
  • Dit suggereert dat transformatie de LLM's helpt om de semantiek beter te begrijpen, zelfs als de syntaxis minder direct "runnable" is. Een ensemble van originele en getransformeerde prompts levert het beste totaalresultaat op.

• Invloed van Complexiteit (RQ3):

  • Er is een sterke negatieve correlatie tussen de syntactische complexiteit van de broncode (gemeten via cyclomatische complexiteit, maximale lusdiepte en aantal variabelen) en het succes van de modellering.
  • Interessant genoeg is de moeilijkheidsgraad van het algoritme (zoals aangegeven in de oorspronkelijke benchmarks) niet betrouwbaar gecorreleerd met de modelleringssucces; het zijn de nestende lussen en datastructuurcomplexiteit die de grootste uitdaging vormen.

• Foutanalyse (RQ4):

  • Compileerfouten: Vaak veroorzaakt door het gebruik van Python-builtin functies die niet bestaan in TLA+ (bijv. sort).
  • Runtime-fouten: Voornamelijk gerelateerd aan indexering (Python is 0-gebaseerd, TLA+ is 1-gebaseerd), wat LLM's vaak vergeten ondanks expliciete instructies.
  • Assertiefouten: Soms zijn de fouten het gevolg van "te grote trouw" aan de broncode, waarbij LLM's essentiële logica (zoals functieaanroepen) weglaten of constante waarden verkeerd interpreteren.

Bijdragen en Significantie

1. Model-Bench: De eerste uitgebreide benchmark en pipeline die specifiek is ontworpen om het vermogen van LLM's te evalueren om Python-code direct om te zetten in formele TLA+ specificaties voor model checking.
2. Code-transformatie methode: Een innovatieve aanpak die Python-code herschrijft naar een toestandsmachine-achtige vorm om de kloof tussen dynamische programmeertalen en formele specificatietalen te overbruggen.
3. Empirische inzichten: Het paper levert cruciale bewijzen dat LLM's significant beperkt zijn in het automatisch modelleren van programma's, vooral bij complexe code, en identificeert specifieke foutpatronen (zoals indexering en bibliotheekverschillen) die toekomstig onderzoek moeten adresseren.

Conclusie:
Hoewel LLM's veelbelovend zijn voor formele verificatie, tonen de resultaten aan dat er nog een grote kloof bestaat tussen het genereren van syntactisch correcte code en het creëren van semantisch trouwe, verificatie-klare modellen. Model-Bench biedt een fundament om deze beperkingen aan te pakken en richt de aandacht op de noodzaak van geavanceerdere redeneercapaciteiten in toekomstige LLM's voor het domein van model checking.