Technische Samenvatting: Neuro-Symbolische Synthese van Formeel Geverifieerde Markov Gebruiksmodellen

1. Probleemstelling

De primaire flessenhals die de brede adoptie van Model-Based Statistical Testing (MBST) buiten veiligheidskritische niches verhindert, is de handmatige constructie van Markov-keten gebruiksmodellen. Deze modellen zijn essentieel voor het verschuiven van testdoelstellingen van absolute code-dekking naar statistische inferentie met betrekking tot de verwachte kwaliteit in het veld. Echter, het vertalen van ambigue, ongestructureerde natuurlijke taalvereisten naar formeel geverifieerde toestands-overgangstopologieën en wiskundig consistente waarschijnlijkheidsmatrices vereist aanzienlijke expertise in formele methoden.

Hoewel Large Language Models (LLMs) wel syntactische extractiecapaciteiten hebben getoond, lijden puur neurale benaderingen onder vier kritieke beperkingen wanneer ze worden toegepast op MBST:

1. Stochastische Volatiliteit & Hallucinatie: LLMs kunnen kritieke randgevallen weglaten, onmogelijke overgangen construeren of systeeminvarianten schenden, wat leidt tot ongeldige testgevallen.
2. Kalibratiefalen: LLMs worstelen met precieze numerieke redenering en falen vaak in het voldoen aan de strikte rij-stochastische beperkingen ($\sum_j p_{ij} = 1$) en complexe multivariabele beperkingen die vereist zijn voor geldige Markov-ketens.
3. Toestandsruimte-explosie: LLMs die binnen eindige contextvensters opereren, kunnen niet effectief zeer gelijktijdige, multi-stream overgangsmodellen bijhouden of genereren zonder de structurele coherentie te verliezen.
4. Semantische-Haalbaarheid Divergentie: LLMs blinken uit in semantische progressie, maar schenden frequent fysieke en logische haalbaarheidsbeperkingen (bijv. een afrekenovergang uitvoeren met een lege winkelwagen), waardoor paden worden gegenereerd die semantisch logisch zijn maar fysiek onuitvoerbaar.

Bestaande literatuur mist een end-to-end evaluatie van de vraag of geautomatiseerde modelconstructie de structurele en probabilistische eigenschappen kan behouden die nodig zijn voor de foutdetectiegaranties van MBST.

2. Methodologie: Het NeSy-MBST Framework

Het artikel introduceert Neuro-Symbolic Model-Based Statistical Testing (NeSy-MBST), een hybride framework dat semantische parsing ontkoppelt van wiskundige beperkingsresolutie. De architectuur integreert vijf nauw gekoppelde stadia:

A. Progressie-Haalbaarheid Dual-Memory Architectuur

Het systeem verdeelt de modelconstructie in twee complementaire geheugensystemen:

• Neuraal Progressiegeheugen: Een gefinetuned LLM parseert natuurlijke taalvereisten om een semantische flow-graaf te ontwerpen (het "wat"), waarbij de beoogde gedragstopologieën worden vastgelegd.
• Symbolisch Haalbaarheidgeheugen: Een regelgebaseerde engine handhaaft strikte logische invarianten, precondities en overgangsbeveiligingen (het "hoe"), en valideert elke kandidaat-overgang voordat deze wordt toegelaten.

B. Actief Automata Leren via $L^*$ met LLM Oracles

Het framework maakt gebruik van een gespecialiseerde variant van het $L^*$-algoritme voor actief automata leren om de toestandsruimte te ontdekken.

• Lidmaatschapsvragen (Membership Queries): Het algoritme bevraagt een grammatica-beperkt LLM oracle (beperkt tot de outputs: Ja, Nee, Onzeker) om te bepalen of een kandidaat-inputsequentie wordt geaccepteerd.
• Equivalentievragen (Equivalence Queries): Het huidige hypothese-automata wordt getest tegen het werkelijke Systeem Onder Test (SUT). Divergenties leveren tegenvoorbeelden op die worden gebruikt om de hypothese te verfijnen.
• Escalatie: Als de LLM "Onzeker" teruggeeft, wordt de query geëscaleerd naar menselijke experts of SUT runtime-executie, waardoor wordt voorkomen dat de leerloop nooit ongeverifieerde informatie incorporeert.

C. Pad-Afhankelijke Hiërarchische Modellering

Om pad-afhankelijkheid zonder combinatorische explosie aan te pakken, gebruikt NeSy-MBST een tweelaagse hiërarchie:

1. Bovenliggende Boomstructuur: Veelvuldige, pad-afhankelijke sequenties worden gemodelleerd als een hogere-orde Markov-keten ingebed in een boom.
2. Onderliggend Markov-model: Zeldzame of uitzonderingspaden worden gemodelleerd met standaard eerste-orde Markov-ketens.

D. Wiskundige Beperkingsoptimalisatie

In plaats van de LLM direct de numerieke waarschijnlijkheden te laten genereren, besteedt het framework dit uit aan een symbolische solver:

1. Extractie van Beperkingen: De LLM extraheert vergelijkende relaties (bijv. $P(\text{afrekenen}|\text{winkelwagen}) > P(\text{browsen}|\text{winkelwagen})$) uit de vereisten.
2. Convexe Optimalisatie: Een convexe programmeermachine (SLSQP) lost voor de overgangswaarschijnlijkheidsmatrix $P$ op die aan alle geëxtraheerde beperkingen, rij-stochasticiteit en domeinspecifieke grenzen voldoet, terwijl de entropie wordt gemaximaliseerd om ongegronde bias te vermijden.

E. Closed-Loop Model Adaptatie

Het framework behandelt het gebruiksmodel als een levend artefact. Runtime-telemetrie (executie-logs, dekking-metrieken, foutgegevens) wordt teruggevoerd naar de modelleringsengine. De LLM analyseert divergenties tussen voorspeld en geobserveerd gedrag, en de symbolische solver herkalibreert de waarschijnlijkheden, waardoor het model convergeert naar real-world gebruikspatronen.

3. Belangrijkste Bijdragen

• NeSy-MBST Framework: Een nieuwe architectuur die $L^*$-actief leren, grammatica-beperkte LLM oracles, symbolische solvers en closed-loop feedback combineert om de synthese van gebruiksmodellen te automatiseren.
• Formele Verificatie van LLM Output: De introductie van een symbolische verificatieloop die structurele schendingen detecteert (onbereikbare toestanden, ontbrekende zelf-lussen) en gerichte her-prompting triggert, waardoor een door recall beperkt generatieprobleem wordt omgezet in een verificatie-gestuurd completion-probleem.
• Orthogonale Decompositie van Fouten: Het artikel stelt vast dat structurele volledigheid (topologie) en probabilistische kalibratie (gewichten) orthogonale eigenschappen zijn, die respectievelijk door de symbolische loop en de convexe optimizer worden aangepakt.
• Empirische Validatie: Een uitgebreide evaluatie op een Autonomous Vehicle (AV) CPS-benchmark en twee e-commerce specificaties, waarbij NeSy-MBST wordt vergeleken met pure neurale baselines en traditionele handmatige benaderingen.

4. Experimentele Resultaten

Geëvalueerd op een AV CPS-benchmark (9 toestanden, 13 overgangen) en e-commerce modellen (tot 42 toestanden, 218 overgangen, bereikte NeSy-MBST het volgende:

• Extractie-nauwkeurigheid (RQ1): Behaalde een systeem-niveau F1-score van 0,9125, waarmee de veiligheidskritische drempel van 0,90 werd overschreden. Dit is een verbetering van 39,1% ten opzichte van de beste GPT-4o baseline (Hybrid SMF) en een verbetering van 14,8% ten opzichte van de sterkste enkele-model baseline (Claude 3.5 Sonnet).
• Foutdetectie-dekking (RQ2): Behaalde 85,7% overgangsdekking, een winst van 35,7 procentpunt ten opzichte van de pure neurale baseline (50%). Dit suggereert een significante toename in de diversiteit van fout-onthullende paden.
• Probabilistische Kalibratie (RQ3): Behaalde een Jensen–Shannon Divergentie (JSD) van 0,012 (vs. 0,157 voor de pure neurale baseline), wat bevestigt dat de convexe optimizer de getrouwheid van de operationele testallocatie behoudt. De genormaliseerde Frobenius-afstand was 0,0654, wat wijst op een hoge structurele gelijkenis met de referentieverdeling.
• Efficiëntie: Genereerde volledige model-dekking testsuites in minder dan zes minuten voor modellen met tot 42 toestanden.
• Ablatie-studie (RQ4):
  • De Symbolische Loop werd geïdentificeerd als de primaire drijfveer voor structurele volledigheid (verhoging van de overgangs-F1 van 0,78 naar 0,96).
  • De Convexe Optimizer bleek de probabilistische kalibratie te regeren zonder de structurele metrieken te wijzigen.
  • Closed-loop feedback leverde marginale verbeteringen in distributionele getrouwheid, wat vooral waardevol is voor langetermijn testcampagnes.

5. Betekenis en Claims

Het artikel claimt dat NeSy-MBST de handmatige modelleringsbottleneck elimineert zonder de statistische strengheid die vereist is voor veiligheidskritische Cyber-Physical Systems (CPS) in gevaar te brengen.

• De Kloof Overbruggen: De resultaten demonstreren dat neuro-symbolische integratie de structurele getrouwheid (F1 $\ge$ 0,90) en probabilistische kalibratie kan bereiken die vereist zijn voor MBST, waar pure neurale benaderingen hierin falen.
• Proxy voor Foutdetectie: Hoewel de studie geen directe defectdetectie-ratio's tegen een seeded foutencorpus heeft gemeten, voert het artikel aan dat de geobserveerde toename van 35,7% in overgangsdekking een sterke proxy is voor foutdetectie, consistent met de 25–40% verbeteringen die in industriële MBT-implementatieliteratuur worden gerapporteerd.
• Engineering Standaard: De auteurs stellen voor dat de augmentatie van formele test-modelgeneratie door LLM's moet transformeren van een onderzoekscuriositeit naar een standaard engineeringpraktijk, mits aan twee voorwaarden wordt voldaan: (1) LLM's moeten opereren onder structurele beperkingen (grammatica-beperkte output, symbolische verificatie) om hallucinatie te voorkomen, en (2) numerieke parameters moeten worden toegewezen door gecertificeerde solvers, niet door de LLM direct.

Het artikel concludeert dat deze aanpak rigoureuze statistische testen toegankelijk maakt voor bredere softwareontwikkelingspraktijken, waardoor het verder komt dan specialistische veiligheidskritische teams, terwijl het erkent dat toekomstig werk nodig is om deze bevindingen te valideren op grotere industriële systemen en met diverse vereistensstijlen.