Designing FSMs Specifications from Requirements with GPT 4.0

Probleemstelling

Het ontwerpen van formele specificaties voor reactieve systemen, zoals eindige toestandsmachines (FSM's of Mealy-machines), is cruciaal voor het automatiseren van testactiviteiten en het waarborgen van systeemkwaliteit in Model-Driven Engineering (MDE). Traditioneel worden deze specificaties afgeleid van tekstuele requirements in natuurlijke taal. Dit proces is echter tijdrovend, vatbaar voor menselijke fouten en moeilijk volledig te automatiseren omdat het vaak leidt tot onoplosbare problemen of benaderende specificaties.

De kern van het probleem is dat de kwaliteit van de gegenereerde FSM direct invloed heeft op de betrouwbaarheid van het systeem: slechte specificaties leiden tot fouten die de testfase overleven en potentiële catastrofale uitval in productie. Hoewel Large Language Models (LLM's) zoals GPT-4 veelbelovend zijn voor het genereren van code en specificaties, is er nog weinig onderzoek gedaan naar hun nauwkeurigheid bij het vertalen van natuurlijke taal naar FSM's, noch naar methoden voor het automatisch repareren van gegenereerde, defecte specificaties.

Methodologie

De auteurs stellen een framework voor dat LLM's (specifiek GPT-4o) gebruikt om deterministische eindige toestandsmachines (DFSM's) te genereren op basis van Engelse tekstuele beschrijvingen, gevolgd door een expert-gestuurde reparatiestap.

1. Generatie met Prompt Engineering:

   • Er wordt gebruikgemaakt van "prompt engineering" om GPT-4o instructies te geven voor het genereren van een CSV-gebaseerde representatie van een DFSM (toestand, input, output, volgende toestand).
   • De input bestaat uit synthetisch gegenereerde tekstuele beschrijvingen van DFSM's, die variëren in complexiteit (aantal toestanden en transities).

2. Validatie en Detectie van Fouten:

   • Om de nauwkeurigheid te evalueren, wordt een "oracle" gebruikt (in dit geval een correct gegenereerde DFSM die dient als referentie).
   • Twee methoden worden toegepast om fouten te detecteren:
     • Syntactische vergelijking: Controleert op verschillen in toestanden en transities (bijv. ontbrekende transities, extra transities, lokale outputfouten, transferfouten).
     • Semantische vergelijking: Vergelijkt de gedragspatronen (traces) van de gegenereerde machine met de oracle. Hierbij worden onderscheidende sequenties (distinguishing sequences) en controlesequenties (checking sequences) gebruikt om input-reeksen te vinden die verschillende output-reeksen produceren in de twee machines.

3. Reparatiestrategieën:
   Het paper presenteert vier benaderingen om fouten in de gegenereerde FSM's te repareren:

   • Benadering 1 (Syntactisch): Als de oracle bekend is, worden de exacte syntactische fouten (ontbrekende of verkeerde transities) geïdentificeerd en als instructie toegevoegd aan de prompt voor een nieuwe generatie.
   • Benadering 2 (Semantisch - Onderscheidende Sequenties): Er worden input-sequenties gegenereerd die de gegenereerde machine onderscheiden van de oracle. De verwachte output voor deze sequenties wordt aan de prompt toegevoegd om de LLM te corrigeren.
   • Benadering 3 (Semantisch - Controlesequenties): Een realistischer scenario waarbij een menselijke expert (in plaats van een volledige oracle) de output van één specifieke, lange controlesequentie bevestigt. De prompt wordt verrijkt met deze feedback.
   • Benadering 4 (Op Foutmodellen gebaseerd / Mutatie): Er wordt een "mutatiemachine" (een niet-deterministische FSM) opgebouwd die een domein van mogelijke correcties omvat, gebaseerd op de meest voorkomende fouten die LLM's maken (zoals outputfouten en ontbrekende transities). Een algoritme (SAT-based mining) selecteert de juiste DFSM uit dit domein door experts te vragen om output voor specifieke input-sequenties, zonder de LLM opnieuw te vragen om te genereren.

Belangrijkste Bijdragen

• Synthetische Dataset: Het creëren van een dataset met willekeurig gegenereerde DFSM's en bijbehorende natuurlijke taalbeschrijvingen voor evaluatiedoeleinden.
• Prompt Engineering voor FSM's: Het ontwikkelen van specifieke prompts om GPT-4o te laten converteren van tekst naar een gestructureerde FSM-representatie.
• Reparatiemethodologie: Het voorstellen en evalueren van vier verschillende methoden voor het repareren van gegenereerde specificaties, variërend van volledig geautomatiseerd (met oracle) tot semi-automatisch (met expert-feedback).
• Empirische Analyse: Een uitgebreide evaluatie van de prestaties van GPT-4o en de effectiviteit van de reparatiestrategieën.

Resultaten

De experimenten, uitgevoerd met DFSM's van 5, 10 en 25 toestanden, leverden de volgende inzichten op:

• Generatiekwaliteit: GPT-4o kan vaak correcte FSM's genereren, maar de foutkans neemt toe met de complexiteit van de machine. De meest voorkomende fouten zijn outputfouten (verkeerde output voor een transities) en ontbrekende transities.
• Syntactische Reparatie: Deze methode (waarbij de oracle bekend is) is zeer effectief en bereikt een 100% succesrate voor het repareren van fouten, zelfs bij complexere machines. Dit toont aan dat LLM's goed kunnen reageren op specifieke instructies over syntactische correcties.
• Semantische Reparatie (Onderscheidende Sequenties): Deze methode presteerde slechter (0% succesrate bij 10 toestanden in de test). De auteurs suggereren dat LLM's moeite hebben met het verwerken van grote hoeveelheden input-output data tegelijkertijd, wat leidt tot een verlies van focus (attention mechanism).
• Controlesequenties: Hoewel realistischer, is deze methode minder efficiënt omdat het berekenen van controlesequenties tijdrovend is en lange sequenties complexe informatie bevatten die de LLM moeilijk correct kan interpreteren.
• Foutmodel-benadering: Deze methode bleek het meest veelbelovend voor praktische toepassingen. Door een reparatiedomein te definiëren op basis van bekende LLM-fouten en experts te raadplegen voor specifieke output-queries, kon in 100% van de gevallen een correcte FSM worden gevonden (voor de geteste configuraties). Dit vereist geen herhaaldelijke generatie door de LLM, maar wel een slimme selectie uit een domein van kandidaten.

Betekenis en Conclusie

Het onderzoek toont aan dat LLM's potentieel hebben voor het genereren van formele specificaties uit natuurlijke taal, maar dat ze niet volledig betrouwbaar zijn zonder validatie en reparatie.

• Kritieke Inzichten: LLM's lijken moeite te hebben met het "intelligente" begrijpen van complexe connecties in grote hoeveelheden informatie. Ze missen precisie bij het hanteren van grote datasets.
• Toekomstperspectief: De meest effectieve aanpak is een hybride model waarbij LLM's de initiële specificatie genereren, maar waar formele methoden en expertkennis (via foutmodellen en mining-algoritmen) worden ingezet om de specificatie te valideren en te repareren.
• Impact: Dit framework biedt een nieuwe visie op het gebruik van Machine Learning in Model-Driven Engineering. Het stelt dat volledige automatisatie van het ontwerp nog niet haalbaar is, maar dat semi-automatische workflows met menselijke interventie op strategische punten (reparatie) zeer waardevol en haalbaar zijn voor industriële toepassingen.

Kortom, het paper bevestigt dat GPT-4 een krachtig hulpmiddel is, maar dat de kwaliteit van de output afhankelijk is van een robuust framework voor foutdetectie en -reparatie, waarbij menselijke expertise en formele methoden essentieel blijven.