Technischer Zusammenfassung: Synthese und Verifikation von Transformer-Programmen

Problemstellung

Transformer, die grundlegende Architektur von Large Language Models (LLMs), sind berüchtigt schwer formal zu analysieren. Zwar sind sie ausdrucksstark und parallelisierbar, doch die Verifikation ihrer Eigenschaften ist unentscheidbar, und ihre Erweiterung um Chain-of-Thought-Mechanismen macht sie Turing-vollständig. Um dies zu adressieren, haben Forscher deklarative Sprachen wie RASP (Restricted Access Sequence Processing Language) und ihre Variante C-RASP (Counting RASP) entwickelt, um das Verhalten von Transformern mit präziser Semantik zu erfassen.

Trotz des theoretischen Zusammenhangs zwischen C-RASP und Transformern verbleiben jedoch zwei kritische Lücken:

1. Verifikation: Es gibt keine automatische Methode zur Verifikation von C-RASP-Programmen. Die Prüfung, ob ein C-RASP eine triviale Sprache erkennt, ist im allgemeinen Fall unentscheidbar, und es existiert kein praktisches Werkzeug zur Analyse von Eigenschaften wie Sprachequivalenz oder -inklusion.
2. Synthese: Es ist keine Methode bekannt, um automatisch ein C-RASP-Programm aus Beispielen zu lernen oder zu synthetisieren. Bestehende Ansätze verlassen sich auf das Training neuronaler Netze und das Extrahieren von Regeln, was häufig scheitert, implementierbare Übersetzungen zu erzeugen, oder idealisierte Annahmen erfordert.

Dieser Beitrag adressiert diese Herausforderungen durch die Entwicklung der ersten automatischen Techniken sowohl für die Verifikation als auch für die Synthese von C-RASP-Programmen.

Methodik

1. Verifikation durch Reduktion auf Lustre

Die Autoren stellen eine formale Verbindung zwischen C-RASP und Lustre her, einer synchronen Datenfluss-Sprache, die für eingebettete Systeme verwendet wird.

• Übersetzung: Ein C-RASP-Programm wird in einen Lustre-Knoten übersetzt. Die Übersetzung bildet C-RASP-Regeln auf Lustre-Variablen (Boolesche und ganzzahlige Ströme) ab.
  • Zähl-Operatoren: Der C-RASP-Zähloperator #φ (Zählen der Positionen, an denen φ gilt) wird in Lustre mittels Hilfs-Ganzzahlvariablen simuliert, die Werte über einen unendlichen Strom akkumulieren.
  • Endlich vs. Unendlich: Da C-RASP auf endlichen Wörtern und Lustre auf unendlichen Strömen operiert, wird die Eingabe als unendlicher Strom mit einem spezifischen End-of-Stream-Marker (#) und einem Ewigkeits-Marker (Ω) kodiert.
• Modellprüfung: Nach der Übersetzung werden Eigenschaften wie Sprachequivalenz, -inklusion und -leerheit mit state-of-the-art Modellprüfern (insbesondere Kind2) in Kombination mit optimierten SMT-Lösern (CVC5, Z3) verifiziert.
• Komplexität: Die Übersetzung ist polynomiell in der Größe, sofern die Bereichsparameter im Operator #rs,re unär kodiert sind.

2. Synthese durch Simulated Annealing

Der Beitrag schlägt einen lokalen Suchalgorithmus basierend auf Simulated Annealing vor, um C-RASP-Programme aus positiven und negativen Beispielen zu synthetisieren.

• Zustandsraum: Die Suche ist auf eine feste „Programmform" beschränkt, definiert durch die Anzahl der Booleschen Regeln ($N_b$), Zählregeln ($N_c$) und eine Schranke für numerische Konstanten ($K$).
• Mutationsoperatoren: Der Algorithmus erkundet den Zustandsraum durch Anwendung syntaktischer Mutationen auf das aktuelle Programm. Dazu gehören:
  • Resampling: Ersetzen der rechten Seite einer Regel vollständig.
  • Mikro-Mutationen: Lokale Änderungen wie das Vertauschen logischer Konnektoren, das Umschalten der Negation oder das Ändern der Strenge von Vergleichen.
  • Einschränkungen: Mutationen sind auf flache Syntaxfragmente beschränkt (z. B. Tiefe 2 für Zähl-Ausdrücke), um die Suche hin zu einfachen, interpretierbaren Modellen zu lenken.
• Zielfunktion: Die Bewertungsfunktion $E(P)$ priorisiert die Minimierung von Fehlklassifikationen ($\lambda_{mis}$), gefolgt von der Bestrafung unerreichter Regeln ($\lambda_U$) und der Gesamtgröße des abstrakten Syntaxbaums ($\lambda_S$).
• Annealing-Dynamik: Der Algorithmus akzeptiert schlechtere Lösungen mit einer Wahrscheinlichkeit, die von einem Kühl-Temperaturplan abhängt, was ihm ermöglicht, lokale Optima zu verlassen.

3. Integrierte Anwendungen

Die Autoren integrieren diese beiden Komponenten in ein einheitliches Framework, das zwei Anwendungen unterstützt:

1. Minimierung von Transformer-Programmen: Gegeben ein C-RASP-Programm synthetisiert das System ein strukturell kleineres, äquivalentes Programm. Es wechselt zwischen lokaler Suche und Äquivalenzprüfung ab; Gegenbeispiele aus dem Verifizierer leiten die Suche.
2. Eingeschränktes Lernen: Gegeben eine partielle Spezifikation (ein C-RASP-Programm $P_{spec}$) und gelabelte Beispiele synthetisiert das System ein Programm, das zu den Beispielen passt und in die Sprache von $P_{spec}$ inkludiert ist ($L(P) \subseteq L(P_{spec})$).

Hauptbeiträge

1. Erste automatische Verifikationsmethode: Der Beitrag stellt die erste Technik vor, um C-RASP-Programme automatisch zu verifizieren, indem sie auf Lustre reduziert und Modellprüfung eingesetzt wird. Dies ermöglicht die Verifikation von Sprachequivalenz, -inklusion und -leerheit.
2. Erste automatische Synthesemethode: Die Autoren führen einen lokalen Suchalgorithmus (Simulated Annealing) ein, der in der Lage ist, C-RASP-Programme direkt aus Beispielen zu synthetisieren und dabei die Notwendigkeit eines intermediären Trainings neuronaler Netze zu umgehen.
3. Implementierung und Benchmarking: Eine einheitliche Scala-Werkzeugkette wurde implementiert und gegen eine Suite von Benchmarks aus der Literatur evaluiert, einschließlich regulärer, zählabhängiger und kontextfreier Sprachen.

Experimentelle Ergebnisse

Die Autoren bewerteten ihr Werkzeug an einer Benchmark-Suite, die Sprachen wie Dyck-1, Majority und verschiedene Tomita-Automaten umfasst.

• Effizienz: Das Werkzeug synthetisierte erfolgreich korrekte C-RASP-Programme für die meisten Benchmarks innerhalb eines 300-Sekunden-Timeouts. Beispielsweise dauerte die Synthese eines Programms für Dyck-1 etwa 3,92 Sekunden, während AnBnCn 80,05 Sekunden benötigte.
• Genauigkeit: Die Synthese erreichte eine hohe Trainings- und Evaluierungsgenauigkeit (oft 100 %) bei Sprachen innerhalb der Ausdruckskraft von C-RASP.
• Vergleich mit Transformern: Der Beitrag stellt fest, dass für bestimmte Benchmarks das Training eines Transformers (z. B. GPT-2 via HuggingFace), um die korrekte Sprache zu erreichen, mehrere Stunden dauern konnte, wohingegen das C-RASP-Synthese-Werkzeug die Aufgabe in Sekunden abschloss.
• Grenzen: Wie aus der Ausdruckstheorie zu erwarten, konnten Sprachen jenseits der Leistungsfähigkeit von C-RASP (z. B. Parity, Tomita 3, Tomita 5) nicht mit hoher Genauigkeit gelernt werden; die besten Trainingsgenauigkeiten blieben unter 80 %.

Bedeutung und Behauptungen

Der Beitrag positioniert C-RASP nicht nur als theoretisches Werkzeug zum Verständnis der Ausdruckskraft von Transformern, sondern als interpretierbares Surrogatmodell. Durch die Bereitstellung automatischer Methoden für Verifikation und Synthese argumentieren die Autoren, dass C-RASP mit formalen Methoden (FXAI) analysiert werden kann, wodurch die Lücke zwischen der „Black-Box"-Natur neuronaler Netze und dem Bedarf an Erklärbarkeit geschlossen wird.

Die Bedeutung liegt in:

• Praktische Entscheidbarkeit: Während die allgemeine Verifikation unentscheidbar ist, bietet die Reduktion auf Lustre einen praktischen, automatisierten Pfad zur Verifikation spezifischer, realer Transformer-Verhalten.
• Direkte Synthese: Die Synthesemethode bietet einen direkten Weg zur Generierung interpretierbarer Programme ohne die Instabilität oder Undurchsichtigkeit des Trainings tiefer neuronaler Netze.
• Optimierung: Die Fähigkeit, bestehende Transformer-Programme zu minimieren und sie unter Einschränkungen zu lernen, demonstriert die Nützlichkeit von C-RASP für Programmsverfeinerung und sicherheitskritische Anwendungen.

Die Autoren schließen, dass ihre Arbeit das Fundament für die formale Analyse von Transformern legt, wobei zukünftige Richtungen die Verifikation der Robustheit und die Integration von Chain-of-Thought (CoT)-Mechanismen umfassen.