🤖 machine learning

SMT-Based Active Learning of Weighted Automata

Dieser Beitrag stellt einen parametrischen, auf SMT basierenden aktiven Lernalgorithmus für nichtdeterministische gewichtete Automaten vor, der minimale Ergebnisse garantiert, die Terminierung für endliche Semiringe sicherstellt und in umfangreichen Experimenten eine überlegene Effizienz und Kompaktheit im Vergleich zu bestehenden Methoden demonstriert.

Ursprüngliche Autoren: Tiago Ferreira, Kevin Batz, Alexandra Silva

Veröffentlicht 2026-05-11

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Tiago Ferreira, Kevin Batz, Alexandra Silva

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 versuchen einem Roboter beizubringen, ein Labyrinth zu navigieren, ohne dass Sie den Grundriss des Labyrinths kennen. Sie können dem Roboter zwei Arten von Fragen stellen:

"Was passiert, wenn ich diesen Weg nehme?" (Der Roboter teilt Ihnen das Ergebnis mit, etwa: "Ich stecke fest" oder "Ich finde einen Schatz im Wert von 5 Goldmünzen.")
"Ist diese von Ihnen gezeichnete Karte korrekt?" (Der Roboter prüft Ihre Karte gegen das echte Labyrinth und sagt "Ja" oder "Nein, Sie haben hier eine Abzweigung übersehen".)

Dies ist die Kernidee des Aktiven Lernens: Ein Algorithmus, der ein Modell lernt, indem er einem "Lehrer" (dem realen System) intelligente Fragen stellt.

Lange Zeit funktionierten diese Lernalgorithmen hervorragend für einfache "Ja/Nein"-Labyrinthe (wie: Ist diese Tür offen oder geschlossen?). Doch reale Systeme sind oft komplexer. Sie beinhalten Gewichte: Kosten, Wahrscheinlichkeiten oder Zeit. Zum Beispiel: "Was ist der günstigste Weg zum Ausgang?" oder "Wie hoch ist die Wahrscheinlichkeit eines Absturzes?"

Dieser Artikel stellt eine neue, leistungsfähige Methode vor, um Computern beizubringen, diese gewichteten Automaten (Labyrinthe mit Zahlen, die den Pfaden zugeordnet sind) zu lernen.

Der alte Weg: Die "Tabelle"-Methode

Früher nutzten Forscher eine Methode, die auf riesigen Tabellen (sogenannten Hankel-Matrizen) basierte. Stellen Sie sich vor, Sie versuchen ein Puzzle zu lösen, indem Sie eine massive Tabellenkalkulation ausfüllen, bei der jede Zelle von komplexen algebraischen Regeln abhängt.

Das Problem: Diese Tabellenmethode wird sehr unübersichtlich und schwer zu lösen, wenn die Zahlen nicht nur einfache ganze Zahlen sind. Oft gelingt es ihr nicht, die einfachste mögliche Karte zu finden, oder sie bleibt stecken, wenn sie versucht zu beweisen, dass sie die Aufgabe abschließen kann. Es ist wie der Versuch, einen Rubik's Cube zu lösen, indem man jeden möglichen Zug auf ein Blatt Papier schreibt; das funktioniert für kleine Würfel, wird aber für große unmöglich.

Der neue Weg: Die "SMT"-Methode

Die Autoren schlagen einen anderen Ansatz vor: Constraint Solving (Einschränkungslösung). Anstatt eine Tabellenkalkulation auszufüllen, verwandeln sie das Lernproblem in ein riesiges Logikpuzzle.

Die Analogie: Der Detektiv und der SMT-Löser
Stellen Sie sich vor, Sie sind ein Detektiv, der versucht, einen Tatort (das Labyrinth) basierend auf Zeugenaussagen (den Antworten des Lehrers) zu rekonstruieren.

Die Hypothese: Sie raten einen Verdächtigen und einen Zeitplan (eine kleine Karte mit wenigen Zuständen).
Die Einschränkungen: Sie schreiben eine Liste von Regeln auf: "Wenn der Verdächtige in der Bank war, muss er um 17 Uhr gegangen sein" oder "Das gesamte gestohlene Geld muss 100 $ betragen."
Der SMT-Löser: Dies ist ein superschlau Computerprogramm (wie eine Logik-Engine), das prüft, ob Ihre Regeln Sinn ergeben. Es fragt: "Gibt es irgendeinen Weg, die Bewegungen des Verdächtigen so zu arrangieren, dass alle diese Regeln wahr sind?"
- Wenn Ja: Der Löser liefert Ihnen eine gültige Karte.
- Wenn Nein: Er teilt Ihnen mit, dass Ihre Karte unmöglich ist.

Der Algorithmus des Artikels funktioniert wie folgt:

Er beginnt mit einer winzigen, einfachen Karte.
Er fragt den Lehrer nach Antworten zu bestimmten Pfaden.
Er speist diese Antworten als eine Reihe mathematischer Regeln in den SMT-Löser ein.
Der Löser versucht, eine Karte zu finden, die zu allen Regeln passt.
Wenn der Lehrer sagt: "Nein, diese Karte ist falsch, weil sie bei diesem spezifischen Pfad versagt", fügt der Algorithmus diesen Pfad zu den Regeln hinzu und bittet den Löser, es erneut zu versuchen.

Warum ist das besser?

Der Artikel behauptet drei Hauptvorteile, einfach erklärt:

1. Es findet immer die kleinste Karte (Minimalität)
Die alten Methoden gaben Ihnen manchmal eine Karte mit 10 Räumen, wenn eine 3-Raum-Karte funktioniert hätte. Die neue SMT-Methode ist darauf ausgelegt, die kleinstmögliche Karte zu finden, die zu den Regeln passt. Es ist wie das Finden der effizientesten Route anstatt nur einer Route.

2. Es funktioniert mit "seltsamer" Mathematik
Die alten Methoden hatten Schwierigkeiten mit komplexen Zahlensystemen (wie "Tropischer" Mathematik, bei der man Zahlen addiert, aber das Minimum nimmt, oder "Bottleneck"-Mathematik). Die neue Methode kann diese "seltsamen" Mathematiksysteme handhaben, indem sie sie in Logikpuzzles übersetzt, die der Computermaschine verständlich sind. Es ist wie ein universeller Dolmetscher, der komplexe Mathematik in einfache "Wahr/Falsch"-Fragen verwandeln kann.

3. Es ist schneller und benötigt weniger Fragen
In ihren Experimenten lernte die neue Methode komplexe Karten viel schneller als die alte "Tabellen"-Methode. Außerdem musste sie dem Lehrer weniger Fragen stellen, um die richtige Antwort zu erhalten.

Der "naive" Basisvergleich: Sie verglichen ihre Methode mit einer "dummen" Version, die einfach zufällig rät. Die neue Methode war weitaus überlegen.
Der "State-of-the-Art"-Konkurrent: Sie verglichen sie mit der besten bestehenden Methode. Die neue Methode erzeugte Karten, die deutlich kleiner waren (manchmal 10-mal kleiner!) und dennoch in angemessener Zeit fertig wurden.

Der "magische" Bestandteil: SMT-Löser

Das Geheimnis ist SMT-Lösung (Satisfiability Modulo Theories). Stellen Sie sich einen SMT-Löser als einen übermächtigen Logikprüfer vor. Er prüft nicht nur, ob ein Satz wahr ist; er prüft, ob eine komplexe Reihe mathematischer Regeln gleichzeitig wahr sein können.

Die Autoren bewiesen, dass für viele Arten von Mathematiksystemen (einschließlich endlicher und einiger unendlicher) dieses Logikpuzzle lösbar ist.
Sie zeigten, dass, wenn das Mathematiksystem endlich ist (wie eine begrenzte Menge von Zahlen), der Algorithmus garantiert abschließt.

Zusammenfassung

Der Artikel stellt eine neue Methode vor, um Computern beizubringen, komplexe, gewichtete Systeme zu verstehen. Anstatt veralteter, sperriger Tabellenmethoden zu verwenden, verwandelten sie das Problem in ein Logikpuzzle, das ein moderner Computermaschine knacken kann.

Ergebnis: Es findet das einfachstmögliche Modell.
Ergebnis: Es funktioniert mit einer breiteren Vielfalt von Mathematiksystemen als zuvor.
Ergebnis: Es ist schneller und stellt weniger Fragen als frühere Methoden.

Die Autoren testeten dies an Tausenden von Beispielen und stellten fest, dass es ein robustes, praktisches Werkzeug zum Erlernen dieser komplexen Systeme ist und eine starke Alternative zu den Methoden der letzten zehn Jahre bietet.

Technischer Überblick: SMT-basiertes aktives Lernen gewichteter Automaten

Problemstellung

Das aktive Lernen von Automaten, das mit Angluins $L^\star$ -Algorithmus eingeführt wurde, hat sich zu einer Standardtechnik für die Inferenz von Modellen unbekannter Komponenten in der formalen Verifikation entwickelt. Während $L^\star$ -artige Methoden für boolesche Automaten (deterministisch und nichtdeterministisch) gut etabliert sind, hat sich ihre Erweiterung auf gewichtete endliche Automaten (WFAs) als erheblich schwieriger erwiesen. WFAs verallgemeinern boolesche Automaten, indem sie Übergängen Gewichte aus einem Halbring zuordnen, was die Modellierung quantitativer Eigenschaften wie Kosten, Wahrscheinlichkeit und Ressourcenverbrauch ermöglicht.

Bestehende Ansätze zum Lernen von WFAs basieren auf Verallgemeinerungen der Hankel-Matrix oder der Beobachtungstabelle (z. B. $WL^\star$ ). Diese Methoden erfordern eine Analyse der algebraischen Struktur des zugrunde liegenden Halbrings. Folglich ist der Nachweis der Terminierung und Minimalität subtil und oft auf spezifische algebraische Klassen beschränkt (z. B. Körper, Hauptidealringe). Für viele praktisch relevante Halbringe, wie den tropischen Halbring oder den Bottleneck-Halbring, sind Terminierungsgarantien entweder unbekannt oder gewährleisten keine minimalen Automaten. Darüber hinaus erzeugen bestehende Algorithmen häufig nicht-minimale Modelle oder skalieren bei unendlichen Halbringen nicht effektiv.

Methodik

Die Autoren schlagen einen neuartigen, constraints-basierten aktiven Lernalgorithmus vor, der das Lernproblem direkt als Erfüllbarkeitsproblem formuliert, das durch SMT-Solver (Satisfiability Modulo Theories) gelöst werden kann.

Kernansatz

Anstatt eine Beobachtungstabelle zu verfeinern, konstruiert der Algorithmus inkrementell ein Gleichungssystem über dem gegebenen Halbring $S$ . Die Lösungen dieses Systems entsprechen exakt nichtdeterministischen WFAs, die mit dem „Lehrer" (der Zielsprache) bei allen beobachteten Abfragen übereinstimmen.

Der Lernprozess folgt einer Standard-Schleife des aktiven Lernens (Algorithmus 1):

Hypothesengenerierung: Der Algorithmus versucht, einen $n$ -zuständigen WFA zu finden, der mit der aktuellen Beobachtungsmenge $O$ konsistent ist. Dies wird an eine Unterfunktion getAutomaton delegiert.
Äquivalenzabfrage: Wenn eine konsistente Hypothese $H$ gefunden wird, wird der Lehrer abgefragt, um zu überprüfen, ob $H$ die Zielsprache $L$ erkennt.
Umgang mit Gegenbeispielen: Falls der Lehrer ein Gegenbeispiel $w$ liefert (wobei $H(w) \neq L(w)$ ), wird $w$ zu $O$ hinzugefügt, und die Schleife wird mit den verstärkten Constraints wiederholt.

Die Unterfunktion `getAutomaton`

Der Artikel stellt zwei Implementierungen für getAutomaton vor:

Naiver Baseline: Kodiert direkt die Semantik des WFA. Er behandelt Anfangsgewichte, Übergangsmatrizen und Endgewichte als unbekannte Variablen und löst die Gleichung $out(w) = \text{semantics}(w)$ für alle $w \in O$ .
Optimiert (SWAL): Nutzt eine koalgebraische Perspektive und das Konzept der Zustandssprachen. Anstatt direkt die globale Sprache zu lösen, werden Zwischenvariablen eingeführt, die die von jedem Zustand akzeptierte Sprache repräsentieren. Dies führt zu einem Gleichungssystem, bei dem:
- Stabilisierungs-Constraints sicherstellen, dass Zustandssprachen konsistent mit den Übergangsgewichten sind.
- Spannungs-Constraints sicherstellen, dass die Anfangsgewichte die Zustandssprachen korrekt kombinieren, um die Zielausgabe zu erreichen.
- Schlüsselerkenntnis: Obwohl diese Kodierung mehr Variablen und Gleichungen einführt, macht sie gemeinsame Teilstrukturen (Suffixe) zwischen Beobachtungen sichtbar. Dies ermöglicht es SMT-Solvern, Zwischenergebnisse wiederzuverwenden und verbessert die Skalierbarkeit im Vergleich zum naiven Ansatz erheblich.

Entscheidbarkeit und Halbringe

Der Algorithmus ist parametrisch bezüglich des Halbrings. Die Autoren identifizieren, dass für entscheidbare Halbringe (bei denen die Erfüllbarkeit endlicher Gleichungssysteme entscheidbar ist) die Unterfunktion getAutomaton korrekt und vollständig implementiert werden kann.

Endliche Halbringe: Trivial entscheidbar durch Brute-Force oder SMT.
Unendliche Halbringe: Der Artikel liefert Kodierungen für den tropischen Halbring ( $\min, +$ ), beschränkte tropische Halbringe und den Bottleneck-Halbring ( $\max, \min$ ) in entscheidbare Theorien wie quantorenfreie lineare ganzzahlige Arithmetik (QF-LIA) und quantorenfreie Bitvektoren (QF-BV).

Hauptbeiträge

Neuer Algorithmus: Ein neuer SMT-basierter aktiver Lernalgorithmus für nichtdeterministische WFAs, der parametrisch bezüglich des Halbrings ist.
Minimalitätsgarantie: Im Gegensatz zu $L^\star$ -artigen Methoden, die oft außerhalb spezifischer algebraischer Strukturen keine Minimalitätsgarantien bieten, garantiert dieser Algorithmus bei Terminierung die Erzeugung minimaler WFAs, unabhängig vom Halbring.
Terminierungsbedingungen: Die Autoren beweisen die partielle Korrektheit und liefern hinreichende Bedingungen für die Terminierung. Insbesondere beweisen sie, dass der Algorithmus für alle endlichen Halbringe terminiert. Für unendliche Halbringe ist die Terminierung zwar nicht durch dieselben Kardinalitätsargumente theoretisch garantiert, doch die Implementierung zeigt praktischen Erfolg.
Constraints-basierte Synthese: Der Artikel stellt den ersten constraints-basierten Generierungsalgorithmus für WFAs vor, der eine SMT-basierte Synthese ermöglicht. Er identifiziert spezifische Halbringe, bei denen die resultierenden Constraint-Systeme entscheidbar sind.
Experimentelle Evaluation: Eine umfassende Evaluierung, die die vorgeschlagene Methode (SWAL) mit einem naiven Baseline-Ansatz und dem state-of-the-art $WL^\star$ -Algorithmus vergleicht.

Experimentelle Ergebnisse

Die Autoren implementierten den Algorithmus (SWAL) in OCaml unter Verwendung des Z3-Solvers und evaluierten ihn an über 5.000 zufällig generierten Benchmarks für boolesche, tropische, beschränkt tropische und Bottleneck-Halbringe.

Vs. Naiver Baseline: SWAL übertrifft die naive Kodierung sowohl in der Laufzeit als auch in der Skalierbarkeit erheblich. Während der naive Ansatz Schwierigkeiten hat, Automaten mit mehr als 2–6 Zuständen zu lernen (abhängig vom Halbring), lernt SWAL erfolgreich minimale Automaten mit bis zu 8 Zuständen. Die optimierte Kodierung (Zustandssprachen) reduziert die Anzahl der Timeouts/Out-of-Memory-Fehler um Größenordnungen.
Vs. $WL^\star$ : Im Vergleich zu $WL^\star$ $W L^{⋆}$ (ein state-of-the-art Algorithmus für Hauptidealringe):
- Minimalität: SWAL erzeugt konsistent minimale Automaten, während $WL^\star$ häufig Automaten erzeugt, die bis zu 10-mal größer sind.
- Effizienz: SWAL benötigt weniger Ausgabeabfragen (Interaktionen mit dem Lehrer) als $WL^\star$ .
- Laufzeit: SWAL ist in der Laufzeit konkurrenzfähig, terminiert oft schneller und weist weniger Ressourcenfehler (TO/OOM) auf als $WL^\star$ .
Inkrementalität: Die Aktivierung der inkrementellen SMT-Lösung reduziert die Lernzeit und den Ressourcenverbrauch drastisch und bestätigt die Eignung des constraints-basierten Ansatzes für inkrementelles Lernen.

Bedeutung und Behauptungen

Der Artikel positioniert das constraints-basierte Lernen als praktische und robuste Alternative zu traditionellen Hankel/ $L^\star$ -artigen Methoden für gewichtete Automaten, insbesondere in verifikationsorientierten Szenarien.

Robustheit: Der Ansatz bewältigt ein breiteres Spektrum an Halbringen (einschließlich unendlicher wie des tropischen), für die algebraische Terminierungsbeweise für $L^\star$ -artige Methoden schwierig oder nicht existent sind.
Minimalität: Die Garantie der Minimalität ist ein entscheidender Vorteil, da minimale Modelle für eine effiziente Verifikation und Abstraktion unerlässlich sind.
Skalierbarkeit: Die experimentellen Ergebnisse zeigen, dass die SMT-basierte Synthese skalieren kann, um komplexe, minimale gewichtete Automaten zu lernen, die für bestehende Algorithmen derzeit unerreichbar sind.

Die Autoren schließen, dass sie zwar keinen allgemeinen Terminierungsbeweis für alle unendlichen Halbringe liefern (ein bekanntes offenes Problem), ihre Methode jedoch eine praktische Lösung bietet, die erfolgreich minimale WFAs in Szenarien lernt, in denen frühere Methoden versagen oder suboptimale Modelle erzeugen. Zukünftige Arbeiten umfassen die Erforschung weiterer inkrementeller Hypothesen-Updates und die Erweiterung des Ansatzes auf probabilistische Automaten.