Technische Samenvatting: Geverifieerde LLM-gestuurde Synthese voor Conceptontwerp

Probleemstelling

Moderne softwaresystemen worden steeds vaker samengesteld door het combineren van herbruikbare gedragseenheden (bijv. authenticatie, labeling, toegangscontrole). Hoewel het definiëren van het gedrag van individuele eenheden vaak eenvoudig is, is het specificeren van de coördinatielogica die ervoor zorgt dat deze eenheden veilig met elkaar interageren moeilijk. De Concept Design-methodologie [Jac21] pakt dit aan door applicaties te organiseren rond "concepten" (zelfstandige, gebruikersgerichte functionele eenheden) die verbonden zijn door "reacties" (synchronisatieregels).

Echter, Concept Design mist momenteel een formele semantiek voor reacties. Dit gebrek maakt het moeilijk om:

1. Precies te definiëren wat een ontwerp betekent.
2. Automatisch te verifiëren of een ontwerp veiligheidsinvarianten bewaart (bijv. "gevoelige gegevens mogen niet achterblijven in een dead-letter queue").
3. Veilige coördinatielogica automatisch te synthetiseren.

Bovendien, zelfs als een ontwerp een veiligheidsinvariant voldoet, kan het niet overeenkomen met de intentie van de gebruiker. Veel verschillende reactie-ontwerpen kunnen dezelfde invariant voldoen, inclus�ndien deze onwaarschijnlijk zijn (bijv. het declassificeren van gevoelige gegevens om een invariant te voldoen in plaats van de gegevens te verplaatsen). Het artikel identificeert de noodzaak van een mechanisme om synthese te sturen naar het beoogde ontwerp van de gebruiker, zonder dat de gebruiker zijn intentie volledig hoeft te formaliseren in complexe logische beperkingen.

Methodologie

Het artikel introduceert foundry, een prototype-tool die een Counterexample-Guided Inductive Synthesis (CEGIS)-lus implementeert die wordt aangestuurd door Large Language Models (LLMs). De methodologie bestaat uit drie kerncomponenten:

1. Formele Semantiek

De auteurs definiëren een automata-gebaseerde semantiek voor concepten en reacties:

• Concepten worden gemodelleerd als geïnitialiseerde partiële semiautomata (deterministische toestandsmachines met inputs maar zonder outputs).
• Reacties worden gemodelleerd als een partiële monitor-semiautomaton die de samengestelde concept-automaton observeert. Reacties worden afgevuurd op basis van triggers (when), toestandscondities (where) en effecten (then).
• Compositie: De applicatie is een synchrone compositie van de concept-automata en de reactie-monitor.
• Verificatietarget: Veiligheid wordt geverifieerd door te controleren of de applicatie "settled" is (geen openstaande verplichtingen heeft) op het exacte moment dat de veiligheidsinvariant standhoudt. Dit wordt gecodeerd in Alloy 6 en gecontroleerd met behulp van bounded model checking.

2. LLM-gestuurde Syntheselus

Het syntheseproces werkt als volgt:

1. Voorstel: Een LLM stelt kandidaat-reacties voor (of herziet bestaande reacties) om een gegeven invariant te voldoen.
2. Translatie: Een tweede agent vertaalt de conceptbeschrijvingen, reacties en invarianten (momenteel geschreven in natuurlijke taal) naar Alloy 6.
3. Verificatie: De Alloy model checker verifieert het kandidaat-ontwerp tegen de invariant en eventuele verstrekte scenario's.
4. Feedback: Als verificatie faalt, wordt het tegenvoorbeeld (een spoor dat de invariant of een scenario schendt) teruggekoppeld aan de LLM om het ontwerp te verfijnen.

3. Sturingsmechanismen

Om de "ondergespecificeerde" aard van invariant-alleen synthese aan te pakken, stelt het artikel twee sturingsmechanismen voor:

• Natuurlijke taal-prompts: Het verstrekken van tekstuele beschrijvingen van het beoogde gedrag naast de invariant.
• Scenario-gestuurde synthese: Het verstrekken van positieve (toegestane) en negatieve (verboden) scenario's. In tegen tegenstelling tot prompts hebben scenario's een formele semantiek en kunnen ze automatisch worden gecontroleerd tegen kandidaat-ontwerpen.
• Scenario-elicitatie: Een LLM-gestuurde procedure waarbij het model korte actie-prefixes voorstelt die de invariant schenden, en de gebruiker deze classificeert als wenselijk of onwenselijk. Het model stelt vervolgens reparaties voor (suffixes) voor wenselijke prefixes. Dit verschuift de taak van de gebruiker van het schrijven van scenario's naar het classificeren ervan.

Belangrijkste Bijdragen

1. Formele Semantiek: Een automata-gebaseerde semantiek voor Concept Design-concepten en reacties, wat de bounded verificatie van invarianten en scenario's mogelijk maakt.
2. Geverifieerde Syntheselus: Een CEGIS-achtige, LLM-gestuurde syntheseprocedure voor het genereren van reactie-ontwerpen, geïntegreerd met een scenario-gestuurd mechanisme om synthese te sturen naar de beoogde ontwerpen.
3. Scenario-elicitatie: Een LLM-gestuurde techniek om vroege ontwerpverkenning te ondersteunen door gebruikers scenario's te laten classificeren die de invariant schenden, in plaats van ze vanaf nul te laten schrijven.
4. Empirische Evaluatie: Een uitgebreide evaluatie op drie applicaties (Dead-Letter Queue met gevoelige gegevens, Course Management System, One-Time Evidence Links) en twaalf ontwerpvarianten met behulp van de GPT-5.5 LLM.

Resultaten

De evaluatie, uitgevoerd op een benchmark van 12 ontwerpvarianten, leverde de volgende bevindingen op:

• Invariant-alleen Synthese:

  • LLM's bereiken vaak snel een geverifieerd ontwerp (vaak bij de eerste poging).
  • Ontwerpen zijn echter zelden stabiel over verschillende runs heen.
  • Synthese met alleen de invariant produceert frequent onwaarschijnlijke ontwerpen (bijv. het verbieden van geldige acties of het declassificeren van gegevens) omdat invarianten alleen de ontwerpplek ondergespecificeerd laten.

• Scenario vs. Prompt Guidance:

  • Scenario-gestuurde synthese herstelde beoogde ontwerpen consistenter dan natuurlijke taal-prompting (10/12 varianten vs. 8/12 varianten met initiële inputs).
  • Scenario's zijn gemakkelijker mechanisch te herzien (puur additief) vergeleken met prompts, die fragiel en ambigu kunnen zijn.
  • Overfitting: Minimale sets scenario's kunnen leiden tot overfitting, waarbij het model niet generaliseert (bijv. alleen specifieke aantallen berichten afhandelt). Het toevoegen van scenario's met variërende cardinaliteiten verzachtte dit probleem.

• Scenario-elicitatie:

  • Het eliciteren van 20 scenario's herstelde het beoogde ontwerp in 9/12 varianten, vergeleken met 5/12 met 10 scenario's.
  • Niet-determinisme: De voorstelprocedure van de LLM voor scenario's is niet-deterministisch; verschillende runs eliciteren verschillende sets scenario's, wat leidt tot niet-monotone resultaten (meer scenario's garanderen niet altijd betere dekking).
  • Gemiste gedragingen: Als het elicitatieproces een kritiek scenario mist (bijv. een specifiek inschrijvingspad), kan de synthese convergeren naar een ontwerp dat dat gedrag verbiedt, wat niet de intentie was.

• Foutmodi:

  • De primaire foutmodi waren het missen van kritieke scenario's (gebrek aan dekking) en overfitting (gebrek aan generalisatie).
  • Kwaliteitsproblemen omvatten redundante reacties en condities, hoewel dit de correctheid ten opzichte van de invariant niet beïnvloedde.

Betekenis en Claims

Het artikel claimt dat formele verificatie essentieel is bij het gebruik van LLM's voor hoogwaardige ontwerp-synthese. Hoewel LLM's vaak ontwerpen kunnen generen die eenvoudige invarianten voldoen, kunnen ze niet worden vertrouwd om het beoogde ontwerp te produceren zonder aanvullende sturing.

De betekenis van het werk ligt in het aantonen dat scenario's effectieve, controleerbare sturende artefacten zijn. Zij overbruggen de kloof tussen de formele veiligheidseisen (invarianten) en de informele intentie van de gebruiker. Het artikel stelt dat terwijl invarianten veiligheid garanderen, scenario's zorgen voor plausibiliteit en intentie-alignement.

De auteurs blijven bescheiden over de huidige staat van de prototype:

• De translatie van natuurlijke taal naar Alloy vertrouwt op een LLM, wat een potentiële bron van fouten introduceert (hoewel handmatige inspectie geen problemen vond in de uiteindelijke geverifieerde ontwerpen).
• Verificatie is bounded; de afwezigheid van tegenvoorbeelden garandeert geen onbegrensde correctheid.
• De evaluatie is beperkt tot één LLM-configuratie (GPT-5.5) en een specifieke set benchmarks, hoewel een kruiscontrole met Claude Fable 5 vergelijkbaar succes liet zien, wat suggereert dat de aanpak niet model-specifiek is.
• Toekomstig werk is vereist om de LLM-gebaseerde translatie te vervangen door een formele bron-taal, de verificatie te schalen naar grotere applicaties en de scenario-elicitatie robuuster te maken voor niet-determinisme en dekkingstekorten.