Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

Stellen Sie sich vor, Sie versuchen, einem sehr intelligenten, belesenen Roboter beizubringen, ein strenges, mathematisches Rezept für eine komplexe Maschine zu schreiben. Diese Maschine ist ein „verteiltes System“ (wie die Cloud-Server, auf denen Amazon oder Microsoft laufen), und das Rezept wird in einer speziellen Sprache namens TLA+ geschrieben.

Diese Sprache ist wie ein hochriskantes Puzzle. Wenn man auch nur ein winziges Symbol verpasst oder die Logik auch nur leicht falsch darstellt, könnte die Maschine im Rezept zwar funktionieren, aber in der Realität abstürzen. Das Problem ist, dass das Schreiben dieser Rezepte von Hand schwer und langsam ist. Daher fragten Forscher: Können wir einfach eine moderne KI (ein Large Language Model, oder LLM) bitten, diese Rezepte für uns zu schreiben?

Dieser Bericht ist der erste große Bewertungsbericht zu dieser Frage. Hier ist, was sie herausgefunden haben, einfach erklärt:

1. Die Lücke zwischen „Grammatik vs. Bedeutung“

Die Forscher baten 30 verschiedene KIs, diese TLA+-Rezepte basierend auf Beschreibungen in natürlicher englischer Sprache zu schreiben.

• Die gute Nachricht (Grammatik): In etwa 26 % der Fälle schrieb die KI ein Rezept, das oberflächlich betrachtet korrekt aussah. Die „Rechtschreibprüfung“ (genannt SANY) sagte: „Okay, die Wörter und Symbole sind in der richtigen Reihenfolge.“
• Die schlechte Nachricht (Bedeutung): Wenn sie das Rezept jedoch tatsächlich durch einen „Logik-Tester“ (genannt TLC) laufen ließen, um zu sehen, ob es wirklich funktionierte, bestand es nur in 8,6 % der Fälle.

Die Analogie: Stellen Sie sich vor, Sie bitten einen Studenten, einen juristischen Vertrag zu schreiben. Der Student verwendet perfekte Rechtschreibung und Grammatik (26 % Erfolg), aber der Vertrag, den er geschrieben hat, besagt eigentlich das Gegenteil dessen, was beabsichtigt war, oder lässt eine entscheidende Klausel aus, was ihn rechtlich wertlos macht (nur 8,6 % Erfolg). Die KI ist gut darin, das Aussehen der Sprache nachzuahmen, scheitert aber oft daran, die dahinterstehende Logik zu verstehen.

2. Größer ist nicht immer besser

Normalerweise nehmen wir an, dass ein größeres, leistungsfähigeres KI-Modell eine bessere Arbeit leistet. Aber in dieser Studie war das nicht der Fall.

• Die Überraschung: Ein kleineres KI-Modell (DeepSeek r1:8b) machte einen viel besseren Job als sein massiver „großer Bruder“ (DeepSeek r1:70b).
• Warum? Das kleinere Modell wurde speziell darauf trainiert, „Schritt für Schritt zu denken“ (wie ein Mathematikkunstschüler, der seinen Rechenweg zeigt), während das größere Modell auf so vielen allgemeinen Internetdaten trainiert wurde, dass es durch die strengen Regeln von TLA+ verwirrt wurde. Es ist wie ein spezialisierter Koch, der genau weiß, wie man ein Soufflé backt, im Gegensatz zu einem Generalisten, der zwar alles kochen kann, aber bei dem spezifischen Rezept vielleicht zu viel nachdenkt.

3. „Code-Experten“ scheiterten

Die Forscher testeten KIs, die berühmt dafür sind, Computercode (wie Python oder Java) zu schreiben. Überraschenderweise schnitten diese „Code-Experten“ schlechter ab als die allgemeinen KIs.

• Der Grund: Diese Modelle sind so sehr daran gewöhnt, Code mit Semikolons (;) und geschweiften Klammern ({}) zu schreiben, dass sie versehentlich diese Symbole in das TLA+-Rezept einfügten. Da TLA+ diese Symbole nicht verwendet, war das Rezept sofort defekt. Es ist, als würde ein Zimmermann versuchen, eine Uhr zu reparieren, aber stattdessen versehentlich einen Hammer benutzen, weil das das Werkzeug ist, das er für alles andere verwendet.

4. Der „Schritt-für-Schritt“-Trick funktionierte am besten

Die Forscher probierten vier verschiedene Wege aus, um die KI um Hilfe zu bitten. Die erfolgreichste Methode war die sogenannte „Progressive Prompting“.

• Wie es funktionierte: Anstatt die KI zu bitten, das ganze Rezept auf einmal zu schreiben, baten sie sie, es Stück für Stück aufzubauen: „Schreibe zuerst den Titel. Jetzt schreibe die Variablen. Jetzt schreilen die Regeln.“
• Das Ergebnis: Dies war die einzige Methode, die überhaupt voll funktionsfähige Rezepte produzierte (die 8,6 % Erfolgsquote). Es ist wie beim Hausbau: Wenn man versucht, das Dach, die Wände und das Fundament in einem einzigen riesigen Sprung zu bauen, wird man wahrscheinlich scheitern. Aber wenn man Zimmer für Zimmer baut, hat man eine größere Chance auf Erfolg.

5. Die „Halluzinationen“ der KI

Die Forscher fanden fünf spezifische Arten, wie die KI immer wieder dieselben Fehler machte, was sie als „Halluzinationen“ bezeichnen:

1. Falsche Symbole: Verwendung von fancy mathematischen Symbolen (wie ∧) anstelle der einfachen Textsymbole, die TLA+ erfordert (wie /\).
2. Sprachmischung: Versehentliches Hinzufügen von Semikolons oder Backticks aus anderen Programmiersprachen.
3. Laut Denken: Die KI fügte manchmal ihren eigenen „Denkprozess“ (wie ...) direkt in das fertige Rezept ein, was dieses unbrauchbar machte.
4. Falsche Länge: Manchmal schrieb die KI ein Rezept, das 9 Mal zu lang war, oder sie schrieb fast gar nichts.
5. Defekte Struktur: Fehlende „End“-Markierungen des Rezepts, wodurch das Dokument unvollständig blieb.

Das Fazament

Der Bericht kommt zu dem Schluss, dass aktuelle KIs noch nicht in der Lage sind, zuverlässige TLA+-Spezifikationen eigenständig zu schreiben. Während sie das Aussehen der Sprache imitieren können, machen sie immer noch zu viele logische Fehler, um ohne die Überprüfung jeder einzelnen Zeile durch einen menschlichen Experten vertraut werden zu können.

Die Forscher schlagen vor, um dies zu beheben:

• Die „Schritt-für-Schritt“-Prompting-Methode anzuwenden.
• Kleinere, auf logisches Denken spezialisierte Modelle anstelle von massiven, allgemeinen Modellen zu verwenden.
• Werkzeuge zu entwickeln, die häufige Fehler automatisch korrigieren (wie das Entfernen der falschen Symbole), bevor die KI überhaupt versucht, das Rezept auszuführen.

Bis dahin bleibt das Schreiben dieser kritischen Systemrezepte eine Aufgabe für menschliche Experten, wobei die KI als hilfreiche, aber fehleranfällige Assistentin fungiert.