Technische Samenvatting: SYSMOBENCH

Probleemstelling

Formele modellen zijn cruciaal voor het specificeren en verifiëren van de correctheid van grote, complexe computersystemen, met name in de domeinen van gedistribueerde en concurrente computing. Het creëren van deze modellen is echter berucht duur, omdat het een aanzienlijke inspanning van experts vereist om laag-niveau systeemcode te abstraheren naar rigoureuze wiskundige specificaties. Hoewel recente vooruitgang in generatieve AI (LLM's en agentische technieken) veelbelovend is gebleken voor het genereren van functie-niveau specificaties (bijv. pre- en postcondities), blijft het onduidelijk of AI effectief volledige, real-world systemen kan modelleren. Bestaande benchmarks richten zich voornamelijk op kleine codefragmenten of logische puzzels, en falen in het adresseren van de complexiteit van het abstraheren van systeemontwerp, het redeneren over veiligheid en liveness onder fouten, en het omgaan met de schaal van productie-waardige artefacten.

Methodologie

De auteurs presenteren SYSMOBENCH, een benchmark die ontworpen is om het vermogen van generatieve AI te evalueren om complexe real-world systemen formeel te modelleren. Het framework richt zich op concurrente en gedistribueerde systemen, die de basis vormen voor kritieke infrastructuur zoals besturingssystemen en clouddiensten.

Kerncomponenten

1. Taakformulering: De benchmark taakt AI-agenten om formele systeemmodellen te genereren (specifiek in TLA+, de de facto specificatietaal voor dergelijke systemen) vanuit real-world systeemartefacten. De input bestaat uit broncode, documentatie en runtime traces. De output moet essentiële gedragseigenschappen en statusovergangen vastleggen, terwijl irrelevante implementatiedetails worden uitgesloten.
2. Systeemartefacten: De benchmark bevat momenteel elf diverse artefacten, variërend van eenvoudige synchronisatieprimitieven (Spinlock, Mutex, Ringbuffer in de Asterinas OS) tot complexe gedistribueerde protocollen (Etcd Raft, Redis Raft, ZooKeeper FLE, Xline CURP) en compiler-gegenereerde systemen (PGo).
3. Geautomatiseerde Evaluatiemetrieken: Een belangrijke bijdrage is de ontwikkeling van geautomatiseerde, kwantitatieve metrieken om de modelkwaliteit te beoordelen zonder te vertrouwen op broze menselijke vergelijkingen of "LLM-as-a-judge"-benaderingen. De metrieken omvatten:
   • Syntactische Correctheid: Gevalideerd met de SANY Syntactic Analyzer. Het maakt gebruik van een gewogen scoringsschema (full-model versus per-action) om partiële correctheid te behandelen.
   • Runtime Correctheid: Gemeten door het deel van de modelacties dat zonder fouten kan worden uitgevoerd met behulp van de TLC model checker, wat dient als een proxy voor logische zelfconsistentie.
   • Conformiteit: Beoordeeld via trace-validatie, waarbij uitvoeringstraces van de geïnstrumenteerde systeemcode worden gecontroleerd tegen de state space van het gegenereerde model. Dit omvat het gebruik van een LLM om model-elementen aan code-elementen te koppelen om naamgevingsverschillen af te handelen.
   • Invariant Correctheid: Evalueert of het model voldoet aan systeem-specifieke safety en liveness eigenschappen. Invariant-templates worden via LLM's geconcretiseerd in model-specifieke TLA+ formules en vervolgens geverifieerd via model checking.

Evaluatie-agenten

De studie evalueert drie verschillende agent-ontwerpen aangedreven door vier state-of-the-art LLM's (Claude-Sonnet-4, GPT-5, Gemini-2.5-Pro, DeepSeek-R1):

• Basic Modeling Agent: Prompt de LLM direct met broncode en taakeisen.
• Code Translation Agent: Vertaalt systeemcode regel voor regel naar TLA+ voordat de control flows worden georganiseerd.
• Trace Learning Agent: Concludeert het systeemmodel uitsluitend op basis van runtime traces zonder code-input.

Belangrijkste Resultaten

De evaluatie onthult significante beperkingen in de huidige AI-capaciteiten met betrekking tot complexe systeemmodellering:

• Schaalbaarheidsgat: AI-agenten presteren goed op kleine, eenvoudige artefacten (bijv. Asterinas Spinlock), waarbij ze vaak hoge scores behalen op syntaxis, runtime en conformiteit. Echter, de prestaties nemen scherp af bij grotere, complexe systemen zoals Etcd Raft. Zo behaalde zelfs de best presterende agent op Etcd Raft (Claude-Sonnet-4 met code translation) slechts 15,38% conformiteit en 92,31% invariant correctheid, terwijl andere agenten volledig faalden op syntaxis- of runtime-checks.
• Abstractie-uitdagingen: De primaire faalmodi voor complexe systemen zijn de moeilijkheid bij het omgaan met code-verborigheid, het begrijpen van complexe protocol-logica (bijv. Raft ordering), en het correct abstraheren van geneste datastructuren (bijv. gedistribueerde logs).
• Agent Prestaties: De Code Translation Agent presteerde over het algemeen beter dan de Basic Modeling Agent op complexe systemen, wat suggereert dat het benutten van de code-vertalingscapaciteiten van LLM's hels helpt om hallucinaties van logica te voorkomen. De Trace Learning Agent presteerde over de hele linie slecht, waarbij vaak faalde op compilatie- en runtime-checks, wat aangeeft dat het afleiden van systeemmodellen uit traces momenteel moeilijker is voor LLM's dan het verwerken van broncode.
• Foutanalyse: Syntaxisfouten komen veel voor, met name bij wiskundige symbolen en misbruik van operatoren. Runtime-fouten komen vaak voort uit inconsistente configuraties of misverstanden over TLA+ datastructuren. Opvallend genoeg hebben LLM's aanzienlijk moeite met liveness properties, waarbij 41,9% van de invariant-schendingen gerelateerd is aan liveness vergeleken met slechts 8,3% voor safety properties, wat wijst op een zwakte in temporele redenering.
• Kwalitatieve Bruikbaarheid: Ondanks kwantitatieve beperkingen slaagden AI-gegenereerde modellen erin bekende bugs in vijf verschillende systemen te reproduceren, wat de praktische bruikbaarheid voor partiële correctheidscontrole aantoont.

Betekenis en Claims

De auteurs positioneren SYSMOBENCH als een fundamentele stap naar het bevorderen van AI van "code intelligence" naar "system intelligence".

• Benchmarking van de Realiteit: Het paper claimt dat hoewel AI veelbelovend is bij programmeertaken, het momenteel de capaciteit mist om grote, complexe systemen te begrijpen, te abstraheren en te specificeren die nodig zijn voor formele verificatie.
• Geautomatiseerde Evaluatie: Door geautomatiseerde metrieken vast te stellen voor syntaxis, runtime, conformiteit en invarianten, biedt SYSMOBENCH een schaalbare en objectieve manier om vooruitgang in dit domein te meten, voorbij de beperkingen van bestaande benchmarks die zich richten op kleine programma's of logische puzzels.
• Toekomstige Richting: De auteurs zien SYSMOBENCH als een voertuig om innovatieve AI-benaderingen te stimuleren. Ze merken op dat de benchmark uitbreidbaar is (ondersteuning voor Alloy en PAT) en actief de collectie artefacten uitbreidt. Ze benadrukken dat het doel niet enkel het genereren van code is, maar het mogelijk maken voor AI om bij te dragen aan de formele verificatie van veiligheidskritische real-world systemen, vergelijkbaar met de rol die SWE-bench speelt in software engineering.

Het paper concludeert dat huidige LLM's beperkt zijn in het modelleren van complexe systemen, maar dat het framework de noodzakelijke instrumenten biedt om verbeteringen te volgen en de ontwikkeling van meer capabele AI-agenten voor formele systeemmodellering te sturen.