Grammar-Constrained Refinement of Safety Operational Rules Using Language in the Loop: What Could Go Wrong

Technische Samenvatting: Grammatica-beperkte verfijning van operationele veiligheidsregels

Het Probleem

In Cyber-Fysieke Systemen (CPS), zoals autonome voertuigen, worden veiligheidsspecificaties geoperationaliseerd via operationele regels. Deze regels definiëren de veilige grenzen (bijv. minimale afstand tot een voorligger) waarbinnen een systeem mag opereren. Wanneer de omgeving verandert of het systeem evolueert, kunnen deze regels inconsistent worden met de werkelijke geobserveerde systeemuitkomsten (bijv. een regel zegt "veilig", maar het systeem faalt toch).

Het verfijnen van deze regels is complex omdat:

1. Syntactische correctheid: De nieuwe regels moeten strikt voldoen aan een domeinspecifieke grammatica.
2. Semantische rechtvaardiging: Het gebruik van Large Language Models (LLMs) voor verfijning brengt risico's met zich mee, zoals het "overfitten" op geobserveerde data (het creëren van regels die te restrictief zijn zonder dat dit door de veiligheidseisen wordt ondersteund).

Methodologie

De auteurs introduceren een framework dat counterfactual reasoning (tegenfeitelijke redenering) combineert met een grammatica-beperkte LLM-verfijningslus. Het proces bestaat uit drie hoofdfasen:

1. Counterfactual Analysis (Tegenfeitelijke Analyse):
   Wanneer een regel inconsistent is, zoekt het systeem naar een "minimale perturbatie" (een kleine wijziging) in de input die de uitkomst van het systeem zou veranderen. Dit helpt om de beslissingsgrens van de regel nauwkeurig te lokaliseren. Dit resulteert in een evidence file met paren van inputs die de inconsistentie blootleggen.
2. Grammar-Constrained LLM Rule Synthesis:
   Een LLM fungeert als assistent om de regel te verfijnen. De LLM krijgt de grammatica, de inconsistente regel en de tegenfeitelijke bewijslast als input. De prompt dwingt de LLM om minimale wijzigingen voor te stellen (zoals het aanpassen van drempelwaarden of operatoren) die voldoen aan de syntactische regels van de grammatica.
3. Refinement Loop & Validatie:
   De voorgestelde regel wordt getoetst aan drie criteria:
   • Geen tegenstrijdigheden: De nieuwe regel mag niet conflicteren met bestaande veilige regels.
   • Behoud van consistentie: Regels die eerder correct waren, mogen niet onjuist worden door de wijziging.
   • Resolutie van inconsistentie: De nieuwe regel moet de foutieve uitkomsten daadwerkelijk corrigeren.

Belangrijkste Bijdragen

• Nieuw Framework: Een geïntegreerde aanpak die counterfactuals gebruikt om LLM's te sturen bij het herschrijven van formele veiligheidsregels.
• Grammatica-beperking: Een methode om de output van LLM's te dwingen binnen de strikte syntactische kaders van een domeinspecifieke taal te blijven.
• Empirische LLM-studie: Een diepgaande analyse van hoe verschillende LLM-varianten (zoals GPT-5, Claude, Gemini) presteren op het gebied van grammatica, semantiek, interpreteerbaarheid en minimaliteit.

Resultaten

De auteurs testten het framework op een autonoom rijdend controlesysteem (ADS).

• Effectiviteit: Het framework slaagde erin de inconsistenties van een conventionele baseline volledig op te lossen, wat leidde tot een verbetering in de decisiveness gain (van 0.86 naar 1.0).
• LLM-variatie: De studie toonde aan dat de kwaliteit sterk afhankelijk is van het model. Terwijl sommige modellen (zoals GPT-5 Thinking) uitstekende, minimale en semantisch correcte regels genereerden, vertoonden andere (zoals Claude of DeepSeek) problemen met ofwel de grammatica (syntactische fouten) ofwel met "over-constraining" (het onnodig te streng maken van regels).
• Gevonden lessen: De auteurs waarschuwden dat LLM's de neiging hebben om regels "veiliger" te laten lijken door drempelwaarden extreem te vernauwen, wat in de praktijk onterecht kan zijn (overfitting).

Significantie

Dit onderzoek is cruciaal voor de veiligheid van autonome systemen. Het laat zien dat LLM's krachtige instrumenten kunnen zijn voor het onderhoud van veiligheidsspecificaties, maar dat ze nooit autonoom mogen worden ingezet. Er is een noodzaak voor strikte, parser-gebaseerde grammatica-controle en semantische validatie (zoals simulatie-gebaseerde falsificatie) om te voorkomen dat een AI-model onbedoeld de operationele grenzen van een voertuig op een onjuiste manier wijzigt.