⚡ electrical engineering

NeuroSymbolic Robustness Analysis for Discrete Systems with Respect to Transition Deviations

Dieses Paper schlägt ein neurosymbolisches Framework vor, das Large Language Models zur Ableitung zulässiger Übergangsabweichungen mit symbolischer Analyse kombiniert, um Robustheitsgarantien für ereignisgesteuerte Systeme zu berechnen, wodurch die Skalierbarkeit und Konservativität bestehender Methoden effektiv adressiert werden.

Ursprüngliche Autoren: Shih-Jie Shih, Jonghan Lim, Ilya Kovalenko, Rômulo Meira-Góes

Veröffentlicht 2026-06-03

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Shih-Jie Shih, Jonghan Lim, Ilya Kovalenko, Rômulo Meira-Góes

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie bauen eine sehr strenge Verkehrsregelung für eine belebte Kreuzung. Sie schreiben ein perfektes Regelwerk (den „Supervisor“), das den Autos genau sagt, wann sie anhalten und fahren sollen, um sicherzustellen, dass keine Unfälle passieren. Dieses Regelwerk funktioniert perfekt, wenn sich die Autos und die Straße exakt so verhalten, wie Sie es in Ihrem Entwurf gezeichnet haben.

Aber in der realen Welt läuft nicht immer alles nach Plan. Ein Auto könnte liegen bleiben, ein Sensor könnte eine Fehlfunktion haben oder ein Fahrer könnte einen Fehler machen. In der Ingenieurwissenschaft sind dies „Abweichungen“. Wenn Ihr Regelwerk diese realen Störungen nicht berücksichtigt, könnte Ihre Verkehrsregelung versagen und Unfälle könnten passieren.

Das Problem: Zu viele „Was-wäre-wenn“-Szenarien

Ingenieure haben versucht, dies zu lösen, indem sie fragten: „Was wäre, wenn das Auto IRGENDETWAS anderes macht als im Entwurf vorgesehen?“

Das Problem ist, dass die Anzahl der „irgendwelche anderen“ Szenarien astronomisch groß ist. Es ist, als würde man versuchen, jede einzelne Möglichkeit zu prüfen, auf die Weise, wie ein Auto Fehlfunktionen aufweisen könnte, im gesamten Universum.

Es ist zu langsam: Das Prüfen jeder einzelnen Möglichkeit verbraucht so viel Rechenleistung, dass es für alles außer den einfachsten Systemen unmöglich ist.
Es ist zu albern: Viele dieser „Was-wäre-wenn“-Szenarien sind physikalisch unmöglich. Zum Beispiel könnte ein Entwurf besagen, dass ein Auto plötzlich auf die andere Straßenseite teleportiert. Während dies in einem Computermodell mathematisch möglich ist, ist es im realen Leben physikalisch unmöglich. Das Prüfen dieser albernen Szenarien verschwendet Zeit und verwirrt die Ergebnisse.

Die Lösung: Ein „Neurosymbolisches“ Teamwork

Dieses Paper schlägt ein kluges Zusammenspiel zwischen zwei Arten von Künstlicher Intelligenz vor, um diese Probleme zu lösen. Stellen Sie sich das wie die Einstellung eines Kreativen Detektivs und eines Strengen Buchhalters vor, die zusammenarbeiten.

1. Der Kreative Detektiv (Der „Neurale“ Teil)

Zuerst nutzt das Team ein Large Language Model (LLM) – die gleiche Art von KI, die Geschichten schreibt oder Fragen beantwortet.

Was es tut: Die KI liest die technischen Entwürfe und die Beschreibungen in natürlicher Sprache darüber, wie das System funktionieren sollte (z. B. „Autos können nicht teleportieren“, „Maschinen können keine Teile verarbeiten, bevor sie ankommen“).
Die Analogie: Stellen Sie sich vor, die KI ist ein Detektiv, der den Entwurf liest und sagt: „Okay, ich kenne diese Maschine. Sie kann nicht einfach spontan Teile aus dem Nichts herausschießen. Das verstößt gegen die Gesetze der Physik. Also werde ich dieses unmögliche Szenario ignorieren.“
Das Ergebnis: Anstatt Millionen von unmöglichen Fehlfunktionen zu prüfen, filtert die KI diese heraus und liefert dem Team eine kurze, realistische Liste von Dingen, die tatsächlich schiefgehen könnten.

2. Der Strenge Buchhalter (Der „Symbolische“ Teil)

Sobald der Kreative Detektiv die kurze, realistische Liste der Störungen bereitgestellt hat, übernimmt der Strenge Buchhalter.

Was er tut: Dieser Teil nutzt traditionelle, mathematisch schwere Logik (symbolische Argumentation), um das System rigoros gegen genau diese kurze Liste zu testen.
Die Analogie: Der Buchhalter rät nicht; er rechnet. Er prüft: „Wenn die Maschine auf diese Weise klemmt, hält die Verkehrsregelung dann immer noch alle sicher?“
Das Ergebnis: Da die Liste klein und realistisch ist, kann der Buchhalter die Aufgabe schnell erledigen und eine mathematisch perfekte Sicherheitsgarantie geben.

Wie es in der Praxis funktioniert

Die Forscher haben dieses „Detektiv + Buchhalter“-Team in drei realen Szenarien getestet:

Eine Fabrikmaschine: Überprüfung, ob eine Maschine einen Lagerbehälter überlaufen lassen könnte, wenn Teile zu schnell ankommen oder stecken bleiben.
Der Therac-25 (Eine medizinische Maschine): Ein berühmter historischer Fall, bei dem eine Strahlungsmaschine aufgrund eines Designfehlers Unfälle verursachte. Sie prüften, ob die Sicherheitsregeln damit umgehen können, wenn ein Bediener Tasten zu schnell drückt oder den falschen Modus wählt.
Ein Kommunikationsprotokoll: Überprüfung, ob ein Nachrichtensystem mit verlorenen oder duplizierten Datenpaketen umgehen kann, ohne abzustürzen.

Die Ergebnisse

Das Paper stellte fest, dass diese neue Methode eine enorme Verbesserung darstellt:

Es reduziert das Rauschen: Die KI hat in einigen Fällen über 90 % der „albernen, unmöglichen“ Szenarien erfolgreich herausgefiltert.
Es bewahrt die Sicherheit: Obwohl sie weniger Szenarien geprüft haben, waren die gefundenen Sicherheitsgarantien genauso stark, als hätten sie jedes mögliche Szenario geprüft.
Es ist schneller: Indem die unmöglichen Fehlfunktionen ignoriert wurden, musste der Computer nicht so hart arbeiten, um die Antwort zu finden.

Zusammenfassend

Dieses Paper führt einen Weg ein, um Sicherheitsprüfungen für Maschinen intelligenter zu machen. Anstatt vorherzusagen, was alles möglich wäre (einschließlich unmöglicher Zaubertricks), nutzt es KI, um herauszufinden, was im realen Leben tatsächlich schiefgehen könnte, und verwendet dann strikte Mathematik, um zu beweisen, dass das System gegen diese spezifischen, realistischen Risiken sicher ist. Es ist, als würde man eine Brücke auf Rost und Risse prüfen, anstatt sich Sorgen zu machen, dass sie von einem Meteoriten getroffen wird.

Technisches Resümee: Neurosymbolische Robustheitsanalyse für diskrete Systeme hinsichtlich Transitionsabweichungen

Problemstellung

In der Überwachungssteuerung von ereignisgesteuerten diskreten Systemen (Discrete-Event Systems, DES) werden Regler synthetisiert, um Spezifikationen auf ein Prozessmodell durchzusetzen. Während klassische Methoden „korrekt-durch-Konstruktion“-Garantien bieten, sind diese Garantien strikt von der Genauigkeit des Prozessmodells abhängig. In der Praxis führen Abweichungen durch unmodellierte Dynamiken, Sensorauschen oder Abstraktionsfehler dazu, dass das reale System vom nominalen Modell abweicht, was potenziell die Sicherheit gefährdet.

Neuere Arbeiten haben dies adressiert, indem sie diskrete Robustheit als die Menge aller möglichen Transitionsabweichungen (zusätzliche Übergänge, die zum nominalen Prozess hinzugefügt werden) definiert haben, gegen welche ein Überwacher die Sicherheit aufrechterhält. Dieser transitionsbasierte Ansatz steht jedoch vor zwei kritischen Einschränkungen:

Skalierbarkeit: Der Raum der möglichen Abweichungen wächst exponentiell mit den Zustands- und Aktionsräumen, was eine erschöpfende Enumeration für alle außer den kleinsten Systemen rechnerisch untragbar macht.
Konservatismus: Die überwiegende Mehrheit der mathematisch möglichen Abweichungen ist physisch nicht realisierbar (z. B. eine Maschine, die spontan ein Teil ausgibt, ohne dass ein Eingang erfolgt ist). Die Einbeziehung dieser nicht realisierbaren Abweichungen bläht den Suchraum auf und liefert Robustheitsergebnisse, die das reale Systemverhalten nicht akkurat widerspiegeln.

Bestehende Versuche, nicht realisierbare Abweichungen mithilfe formaler Systembeschränkungen ( $P_{sys}$ ) zu filtern, erfordern, dass Domänenexperten physikalische Gesetze manuell in formale Spezifikationen kodieren, was eine erhebliche Belastung darstellt und den Overhead für die Analyse-Pipeline erhöht.

Methodik

Das Paper schlägt einen neurosymbolischen Rechenrahmen vor, um diese Herausforderungen hinsichtlich Skalierbarkeit und Realisierbarkeit anzugehen. Der Ansatz entkoppelt die Argumentation über die physische Realisierbarkeit von der formalen Berechnung der Robustheitsgarantien durch einen zweistufigen Prozess:

1. Neuronale Realisierbarkeitsfilterung (LLM-Schicht)

Die erste Stufe nutzt Large Language Models (LLMs), um eine Teilmenge physisch realisierbarer Abweichungstransitionen ( $D$ ) abzuleiten.

Input: Das Framework nimmt formale LTS-Modelle des Prozesses und des Überwachers, natürliche Sprachbeschreibungen von Systemzuständen und Ereignissen, Sicherheitsspezifikationen sowie Domänenwissen über physikalische Gesetze (z. B. „ein Teil kann nicht an zwei Orten gleichzeitig sein“) auf.
Prozess: Ein strukturierter Prompt-Template leitet das LLM an, diese Eingaben zu verarbeiten. Das LLM hat die Aufgabe, Transitionen zu identifizieren, die realistische Fehler oder Abweichungen darstellen, welche konsistent mit der Semantik und den physikalischen Beschränkungen des Systems sind.
Output: Eine reduzierte Menge realisierbarer Abweichungen $D \subseteq (Q_E \times Act_E \times Q_E) \setminus R_E$ , die signifikant kleiner ist als der vollständige Transitionsraum.

2. Symbolische Robustheitsverifikation (Symbolische Schicht)

Die zweite Stufe führt eine formale Verifikation auf der reduzierten Menge $D$ durch.

Prozess: Ein Brute-Force-Algorithmus (Algorithmus 1) iteriert durch alle Teilmengen der realisierbaren Abweichungen $D$ . Für jede Kandidaten-Abweichungsmenge $d$ verwendet er Standard-Model-Checking, um zu verifizieren, ob das abweichende System $E_d$ , gesteuert durch den Überwacher $S$ , die Sicherheitseigenschaft $P$ erfüllt (d. h. $E_d/S \models P$ ).
Verfeinerung: Der Algorithmus extrahiert nur die maximalen robusten Abweichungen (jene, die nicht in anderen robusten Abweichungen enthalten sind), um die endgültige Robustheitsmenge $\Delta_f$ zu bilden.
Garantie: Da die Verifikation symbolisch auf einem formal definierten Transitionssystem durchgeführt wird, bleiben die resultierenden Robustheitsgarantien in Bezug auf die abgeleitete Menge $D$ mathematisch korrekt.

Zentrale Beiträge

Das Paper skizziert zwei primäre Beiträge:

Ein neurosymbolischer Rahmen: Eine neuartige Architektur, die LLMs zur Ableitung physisch realisierbarer Abweichungsmodelle mit symbolischen Methoden zur Berechnung von Robustheitsgarantien kombiniert. Dieser Ansatz automatisiert die Extraktion physikalischer Beschränkungen aus natürlicher Sprache und Domänenwissen, wodurch die manuelle formale Kodierung von $P_{sys}$ entfällt.
Prototyp und Evaluierung: Die Implementierung eines Prototyp-Tools und dessen experimentelle Evaluierung anhand von drei unterschiedlichen Fallstudien: ein Fertigungssystem, die Therac-25 Strahlentherapie-Schnittstelle und das Alternate Bit Protocol (ABP).

Experimentelle Ergebnisse

Das Framework wurde auf drei Fallstudien unter Verwendung von LLMs (GPT-5.2 und Claude 3.5 Sonnet) für die Realisierbarkeitsfilterung und einem Python-basierten symbolischen Verifizierer evaluiert.

Fertigungssystem: Das LLM identifizierte 18 realisierbare Abweichungen (aus einem theoretischen Raum von 108). Die symbolische Schicht fand eine maximale robuste Abweichungsmenge und bestätigte, dass das System gegen 15 spezifische Transitionen robust, aber gegenüber spezifischen Pufferentleerungsfehlern anfällig ist.
Therac-25: Die Analyse identifizierte 9 realisierbare Abweichungen. Es wurde festgestellt, dass das System gegen wiederholte „Enter“-Tastendrücke des Bedieners robust ist, aber anfällig für die spezifische Race Condition im Zusammenhang mit der Auswahl der Elektronen-Therapie, wodurch der historische Designfehler präzise erfasst wurde.
ABP-Protokoll: Das LLM identifizierte 16 realisierbare Abweichungen. Die Analyse bestätigte die Robustheit gegenüber Nachrichtenverlust, Duplikation und Korruption, was mit der Designabsicht des Protokolls übereinstimmt.

Quantitative Befunde:

Reduktion der Realisierbarkeit: Die LLMs reduzierten den Suchraum erheblich. Die Reduktion reichte von 67 % (Therac-25) bis 99 % (ABP) im Vergleich zum vollständigen Transitionsraum.
Genauigkeit der Realisierbarkeit: Im Fertigungsbeispiel waren 89 % der von GPT generierten Transitionen physisch realisierbar, verglichen mit 54 % für Claude. Bei komplexeren Systemen wie ABP sank die Realisierbarkeitsrate für beide Modelle (63 % und 36 %), was auf die Notwendigkeit verbesserten Prompt-Engineerings oder Domänen-Ontologien hindeutet.
Robustheitsäquivalenz: Trotz der Arbeit auf einer reduzierten Menge von Abweichungen lieferte das Framework Robustheitsgarantien, die mit der Analyse des vollständigen Transitionsbasierten Ansatzes vergleichbar sind.

Bedeutung und Behauptungen

Das Paper behauptet, dass dieser neurosymbolische Ansatz erfolgreich den Trade-off zwischen Skalierbarkeit und dem Einschluss nicht realisierbarer Abweichungen in der diskreten Robustheitsanalyse adressiert. Durch die Nutzung von LLMs zur Filterung des Lösungsraums basierend auf semantischem und physischem Verständnis macht die Methode die Robustheitsanalyse für Systeme handhabbar, in denen eine erschöpfende Enumeration unmöglich ist.

Die Autoren betonen, dass das LLM-Komponente zwar ein probabilistisches Element bei der Identifizierung realisierbarer Abweichungen einführt, die anschließende symbolische Verifikation jedoch sicherstellt, dass die endgültigen Robustheitsgarantien in Bezug auf die abgeleitete Menge $D$ formal korrekt sind. Die Arbeit zeigt, dass es möglich ist, Robustheitsanalysen zurückzugewinnen, die mit Methoden des vollen Raums vergleichbar sind, während man auf einer drastisch kleineren, physisch bedeutsamen Teilmenge von Abweichungen operiert.

Das Paper schließt bescheiden mit dem Hinweis, dass die aktuelle Implementierung des Brute-Force-Algorithmus eine Optimierung für größere Systeme erfordert und dass zukünftige Arbeiten sich auf die Verbesserung des Prompt-Engineerings, die Integration von Domänen-Ontologien zur Steigerung der LLM-Genauigkeit und die Untersuchung interaktiver Verfeinerungsschleifen konzentrieren werden, bei denen symbolische Ergebnisse die LLM-Abfragen leiten.