Technische Samenvatting: Event-B Agent

Probleemstelling

De ontwikkeling van software die "correct by construction" is, steunt op formele methoden, waarbij systeembeweging en vereisten wiskundig worden uitgedrukt en geverifieerd via theorema-bewijzen en modelcontrole. De steile leercurve en de vraag naar wiskundige expertise hebben echter de wijdverbreide adoptie van deze methoden belemmerd. Hoewel Large Language Models (LLM's) veelbelovend zijn gebleken in autoformalisatie, zijn bestaande benaderingen grotendeels beperkt tot geïsoleerde taken, zoals het bewijzen van stellingen zonder formalisatie of het synthetiseren van modellen die uitsluitend worden geverifieerd door middel van bounded model checking.

Cruciaal is dat huidige op LLM's gebaseerde methoden geen ondersteuning bieden voor de iteratieve, gezamenlijke evolutie van formele modellen en de bijbehorende bewijzen. In de praktijk vereist formele ontwikkeling dat wanneer een theorema-bewijzer faalt om een bewijsverplichting (PO) te ontlasten, het systeem wijzigingen toestaat in zowel het formele model als de bewijsartefacten. Bestaande tools gaan ofwel uit van een vast model en zoeken naar bewijzen (LLM-bewijshulpmiddelen), of construeren modellen zonder strikte bewijsgebaseerde verificatie (autoformalisatie). Er ontbreekt een kader dat formele ontwikkeling formuleert als een gecoördineerd proces over een gezamenlijke toestandsruimte van modellen en bewijzen, waardoor iteratieve verfijning en reparatie mogelijk worden.

Methodologie: Event-B Agent

Om deze hiaten aan te vullen, stellen de auteurs Event-B Agent voor, een nieuw neurosymbolisch kader voor end-to-end synthese en reparatie van formele modellen. Het kader is ontworpen om natuurlijke taalvereisten te accepteren en via een iteratief proces dat verfijning, synthese en reparatie integreert, een formeel Event-B-model te construeren.

De methodologie bestaat uit drie hoofdfasen:

1. Planning van de Verfijningstrategie

Omdat redeneren over complexe systemen uitdagend is door de snelle groei van de zoekruimte, zet Event-B Agent LLM's in om een verfijningstrategie te plannen.

• Decompositie: De agent partitioneert de set natuurlijke taalvereisten in disjuncte subsets en verdeelt deze over meerdere verfijningsstappen.
• Kleef-invarianten: Voor elke overgang tussen verfijningsstappen stelt de LLM "kleef-invarianten" voor – predicaten die abstracte en concrete variabelen relateren om consistentie te waarborgen.
• Validatie: Deze invarianten worden gevalideerd via tegenvoorbeeldcontrole (met een modelchecker) en bewijspogingen voordat ze worden geaccepteerd, zodat eigenschappen die in eerdere stappen zijn bewezen, behouden blijven.

2. Modelsynthese

Voor elke verfijningsstap synthetiseert de agent een formeel model op basis van de toegewezen vereisten en kleef-invarianten.

• Schema-gestuurde generatie: Om syntaxisfouten die veel voorkomen bij LLM-generatie te beperken, gebruikt het systeem een JSON-schema dat de Event-B-grammatica codeert. Dit zorgt voor structurele correctheid (bijv. verplichte gebeurtenissen, variabele declaraties).
• Well-Formedness-lus: Het gegenereerde model wordt gecompileerd. Fouten bij het compileren (bijv. type-mismatches, niet gedeclareerde variabelen) worden teruggekoppeld aan de LLM voor iteratieve reparatie totdat het model syntactisch geldig en type-correct is.

3. Model- en Bewijsreparatie

Dit is de kernbijdrage van het kader, ontworpen om de gezamenlijke evolutie van modellen en bewijzen te hanteren.

• Verificatielus: Gesynthetiseerde modellen worden eerst gecontroleerd door een modelchecker (ProB) op invariantenschendingen binnen gebonden toestanden. Als er tegenvoorbeelden worden gevonden, wordt het model gerepareerd.
• Theorema-bewijzen: Het model wordt vervolgens onderworpen aan ongebonden theorema-bewijzen. Als bewijzen falen, analyseert het systeem de bewijstoestand om de oorzaak te diagnosticeren.
• Aanbeveling van reparatieregels: Het systeem maakt gebruik van een nieuw component dat bewijstoestanden koppelt aan specifieke reparatieregels (bijv. "Contradictory Goal", "Existential Goal", "Quantified Invariant Preservation"). Deze regels zijn empirisch afgeleid uit ervaringen met handmatig ontlasten van bewijzen.
• Uitvoering van atomische reparatie: Een "fix strategy decision"-LLM kiest uit een bibliotheek van atomische reparatiefuncties (bijv. StrengthenGuard, AddInvariant, InstantiateHypothesis) en voert deze uit. Dit beperkt de wijzigingen van de LLM tot sounde, verifieerbare operaties.
• Soundheid: Het systeem waarborgt soundheid door alle bewijzen opnieuw af te spelen na elke modelwijziging. Een reparatie wordt alleen geaccepteerd als het gecombineerde effect de doel-PO ontlast, geverifieerd door SMT-oplossers en theorema-bewijzers.

Belangrijkste Bijdragen

Het artikel schetst drie hoofdbijdragen:

1. Kader: Event-B Agent is het eerste end-to-end kader voor synthese en reparatie van formele modellen dat verfijning-gebaseerde ontwikkeling ondersteunt met gecoördineerde modelconstructie en bewijsherleiding, en het principe van correctness by construction belichaamt.
2. Hulpmiddel: Een proof-of-concept hulpmiddel geïntegreerd in de Rodin IDE (de standaardomgeving voor Event-B), waarbij gebruik wordt gemaakt van ProB voor modelcontrole en standaard Rodin-bewijzers voor theorema-bewijzen.
3. Evaluatie: Een uitgebreide evaluatie op 27 formele systemen (variërend van eenvoudig tot complex) waarbij Event-B Agent wordt vergeleken met baselines, inclusief ablatiestudies en efficiëntie-analyse.

Experimentele Resultaten

Het kader werd geëvalueerd op 27 formele systemen met gemiddeld 182,41 bewijsverplichtingen per systeem. De resultaten tonen aanzienlijke verbeteringen ten opzichte van baselines (LLM + auto-provers, Cursor en PAT-Agent):

• Consistentie (Rate van Ontlasting van Bewijsverplichtingen - PDR): Event-B Agent behaalde een PDR van 97,86%, wat significant beter is dan baselines (89,20% tot 95,56%). Het behield een PDR boven de 97,0% over alle complexiteitsniveaus, terwijl baselines een hogere variantie vertoonden en prestatiedegradatie met complexiteit.
• Correctheid (Vereistendekking - RC en Voldoening - RF):
  • RC: Event-B Agent behaalde 97,13%, wat de op één na beste methode met 4,63% overtreft.
  • RF: Event-B Agent behaalde 93,79%, wat de op één na beste methode met 18,01% overtreft.
  • De verhouding RF/RC (0,97) geeft aan dat zodra een vereiste is vastgelegd, de agent de bijbehorende bewijzen succesvol ontlast, in tegenstelling tot baselines waar vastgelegde vereisten vaak onbewezen bleven.
• Efficiëntie: De gemiddelde tijd om een systeem te synthetiseren en te repareren was 74,45 minuten. De gemiddelde tijd om een enkele PO te proberen te ontlasten was 0,24 minuten, wat suggereert dat de reparatie-overhead lineair schaalt met het aantal PO's in plaats van te exploderen met systeemcomplexiteit.
• Ablatiestudies: Het verwijderen van ofwel de verfijningstrategie of het component voor reparatiegeleiding leidde tot prestatiedalingen, wat bevestigt dat deze twee componenten elkaar versterken. Verfijning vermindert de bewijscomplexiteit, terwijl reparatiegeleiding de correctheid van de verfijningsstappen waarborgt.

Betekenis en Claims

De auteurs beweren dat Event-B Agent een veelbelovende stap is naar praktische, sounde, door LLM's ondersteunde formele ontwikkeling. Door formele ontwikkeling te behandelen als een gezamenlijke toestandsruimte van modellen en bewijzen, overwint het kader de beperkingen van geïsoleerde autoformalisatie of theorema-bewijzen.

Het artikel benadrukt dat:

• Verfijning essentieel is voor het beheersen van complexiteit, waardoor de agent moeilijke problemen kan ontleden in hanteerbare stappen terwijl correctheid behouden blijft.
• Bewijsgeleide reparatie noodzakelijk is omdat modelcontrole alleen (gebonden) onvoldoende is voor algemene correctheid; theorema-bewijzen (ongebonden) zijn vereist, maar dit vereist een mechanisme om zowel het model als het bewijs te repareren wanneer automatisch redeneren faalt.
• De neurosymbolische aanpak succesvol de semantische flexibiliteit van LLM's combineert met de strikte soundheid van symbolische verificatietools.

De auteurs blijven bescheiden wat betreft de huidige reikwijdte, en merken op dat de bibliotheek van reparatieregels empirisch is afgeleid en niet exhaustief is, en dat het hanteren van inconsistente natuurlijke taalvereisten een uitdaging blijft voor toekomstig werk. De resultaten suggereren echter dat het voorgestelde kader effectief de kloof overbrugt tussen natuurlijke taalvereisten en correct-by-construction formele modellen.