Technisches Resümee: TLA-Prover

Problemstellung

TLA+ ist eine formale Spezifikationssprache, die zur Verifizierung verteilter Systeme und sicherheitskritischer Protokolle verwendet wird, gepaart mit dem TLC-Model-Checker für eine erschöpfende Zustandsraumexploration. Während Large Language Models (LLMs) vielversprechende Ergebnisse bei der Codegenerierung zeigen, haben sie mit TLA+ erhebliche Schwierigkeiten, da die Sprache im Pre-Training-Korpus nur spärlich repräsentiert ist und über eine idiosynkratische Syntax verfügt (z. B. temporale Operatoren, Mengenkomprehensionen).

Bestehende Baselines, wie die FormaLLM-Studie, zeigen, dass ungetunte Open-Weight-LLMs lediglich eine Erfolgsquote von 8,6 % beim Bestehen des TLC-Model-Checkers über 25 Modelle hinweg erreichen. Eine kritische Herausforderung beim Training von LLMs für die formale Verifizierung ist das Reward Hacking. Im Kontext von TLA+ und TLC kann ein Modell das binäre „Pass“-Signal optimieren, indem es triviale, tautologische Invarianten generiert (z. B. TypeOK == TRUE). Diese Spezifikationen bestehen TLC in jedem erreichbaren Zustand, vermitteln jedoch keine aussagekräftigen Eigenschaften über das Protokoll, was die Verifizierung unbrauchbar macht. Standardmäßige Reinforcement-Learning-Ansätze, die sich ausschließlich auf das TLC-Pass/Fail-Signal als Belohnung verlassen, sind anfällig für diesen Ausfallmodus.

Methodik

Die Autoren präsentieren TLA-Prover, ein 20-Milliarden-Parameter-Modell (basierend auf gpt-oss-20b), das für die Synthese von TLA+-Spezifikationen entwickelt wurde. Der Ansatz kombisch Supervised Fine-Tuning (SFT) mit einer neuartigen Trainingspipeline, die reparaturbasierte Group Relative Policy Optimization (GRPO) und eine vierstufige Validierungshierarchie integriert.

1. Vierstufige Validierungshierarchie

Um Reward Hacking zu verhindern und die semantische Gültigkeit sicherzustellen, wird jedes Modellergebnis durch eine deterministische externe Pipeline in eines von vier Stufen eingestuft:

• Bronze: Die Ausgabe schlägt den SANY-Parser (syntaktisch ungültig).
• Silver: Die Ausgabe parst korrekt, kann aber nicht in TLC geladen oder ausgeführt werden (z. B. Timeouts, Typfehler).
• Gold: Die Ausgabe besteht sowohl SANY als auch TLC; der Model Checker erschöpft den Zustandsraum und alle Invarianten halten.
• Diamond: Die Ausgabe besteht Gold und die Invariante ist mutationssensitiv.
  • Mechanismus: Eine automatisierte AST-basierte Mutation wird auf das Invarianten-Prädikat angewendet (z. B. Negierung eines Konjunkts, Umkehrung relationaler Operatoren oder Vertauschen von Konstanten). Die mutierte Spezifikation wird erneut durch TLC ausgeführt.
  • Kriterium: Wenn die Mutation bewirkt, dass TLC ein Gegenbeispiel findet, gilt die ursprüngliche Invariante als nicht-trivial (Diamond). Wenn TLC weiterhin besteht (z. B. weil die Invariante TRUE war), fällt die Ausgabe durch den Diamond-Check. Dieser Schritt blockiert explizit tautologische Invarianten.

2. Trainingspipeline

Der Trainingsprozess besteht aus zwei primären Phasen, mit einer DPO-Ablation zum Vergleich:

• Phase 1: Supervised Fine-Tuning (SFT)

  • Korpus: Ein kuratierter Datensatz von 1.053 Spezifikationen, der strikt auf die Diamond-Stufe gefiltert wurde. Die Daten stammen aus der TLA+ Foundation Distribution und dem tlaplus/examples-Repository, ergänzt durch einen Ollama-Generator und gefiltert durch einen LLM-Judge sowie die vierstufige Pipeline.
  • Architektur: Ein LoRA-Adapter (Rank 8, Alpha 16) wird auf die Attention-Projektionen des 20B-Parameter-Basemodells angewendet.
  • Ziel: Dem Modell die strukturelle Vokabel und Syntax von TLA+ beizubringen.

• Phase 2: Reparaturbasierte Group Relative Policy Optimization (GRPO)

  • Motivation: Standard-GRPO versagt, wenn alle Proben in einer Gruppe den Verifizierer verfehlen (Sparse Rewards), was zu einem Null-Vorteil und keinem Gradientenfluss führt.
  • Mechanismus: Das Modell wird mit einer „kaputten“ Spezifikation konfrontiert (gewonnen aus vorherigen Fehlversuchen) und hat die Aufgabe, diese zu reparieren.
  • Belohnungssignal: Ein kontinuierlicher Verbesserungsscore basierend auf Stufenübergängen (Bronze→Silver: 0,1, Silver→Gold: 0,3, Gold→Diamond: 0,6). Dies liefert dichte Gradienten selbst dann, wenn das Endergebnis nicht perfekt ist, solange sich die Stufe verbessert.
  • Prozess: Das Modell korrigiert seine eigenen Ausgaben iterativ unter Verwendung von TLC-Fehlermeldungen als Feedback.

• Ablationsstudie (DPO): Eine Variante der Direct Preference Optimization wurde aus demselben SFT-Checkpoint unter Verwendung statischer Präferenzpaare (Diamond > Gold > Silver > Bronze) trainiert. Dies diente als Baseline zum Vergleich gegen den dynamischen, reparaturbasierten GRPO-Ansatz.

Kernergebnisse

Das Modell wurde auf einem Held-out-Benchmark mit 30 Problemen mittels Single-Shot Greedy Decoding evaluiert.

• Leistung: TLA-Prover (finaler Repair-GRPO-Checkpoint) erreichte eine Pass-Rate von 30 % (9/30) sowohl auf Gold- als auch auf Diamond-Ebene.
• Baseline-Vergleich: Dies stellt eine 3,5-fache Verbesserung gegenüber der ungetunten FormaLLM-Baseline von 8,6 % dar.
• Ablationsvergleich: Die DPO-Variante erreichte eine Diamond-Pass-Rate von 20 % und wurde vom Repair-GRPO-Ansatz (30 %) übertroffen.
• Anti-Reward-Hacking-Validierung: Entscheidend ist, dass die Gold- und Diamond-Passraten bei jedem Checkpoint in der Produktionspipeline identisch waren (Differenz von 0). Dies zeigt, dass das Modell nicht gelernt hat, tautologische Invarianten zu generieren, die zwar TLC bestehen, aber den Mutationstest nicht bestehen. Die einzige Ausnahme war ein einzelner Fall in der DPO-Ablation, den die Diamond-Stufe erfolgreich abgefangen hat.
• Inferenzstrategien:
  • Best-of-8 Sampling steigerte die Diamond-Pass-Rate auf 37 % (11/30).
  • Die Greedy ∪ Best-of-8 Union deutet auf eine Obergrenze von 43 % (13/30) hin, was zeigt, dass das Modell die Fähigkeit besitzt, mehr Probleme zu lösen, wenn mehrere Versuche möglich sind.
  • Selbstkorrektur (3-Shot TLC-Feedback) brachte keine Verbesserung, was darauf hindeutet, dass die Fehler auf Wissenslücken und nicht auf zufälligen Sampling-Fehlern beruhen.

Bedeutung und Beiträge

Das Paper beansprucht drei primäre Beiträge:

1. TLA-Prover mit einer vierstufigen Hierarchie: Die Einführung einer Validierungshierarchie, bei der die oberste Stufe (Diamond) Mutationstests nutzt, um tautologische Invarianten auszuschließen. Dies adressiert das spezifische Risiko des Reward Hackings, das mit der Nutzung von TLC als Belohnungssignal einhergeht, und stellt sicher, dass „Bestanden“ eine nicht-triviale Spezifikation impliziert.
2. Reparaturbasierte GRPO-Pipeline: Eine zweistufige Trainingspipeline, die SFT auf einem Diamond-Tier-Korpus mit reparaturbasierter GRPO kombiniert. Dieser Ansatz nutzt das Online-Feedback des Verifizierers, um dichte Belohnungssignale bereitzustellen, was die statische DPO-Ablation übertrifft.
3. Empirische Anti-Reward-Hacking-Analyse: Die Beobachtung, dass die Gold- und Diamond-Passraten über alle Checkpoints hinweg übereinstimmen, liefert den empirischen Beweis, dass die Pipeline den Ausfallmodus der „immer wahren Invariante“ erfolgreich verhindert.

Die Autoren positionieren diese Arbeit als die erste TLA+-spezifische Trainingsstudie, die die FormaLLM-Baselines substanziell übertrifft. Sie betonen, dass das Modell zwar die Synthese von Spezifikationen signifikant verbessert, derzeit aber auf Invarianten-ähnliche Spezifikationen mit kleinen Zustandsräumen spezialisiert ist und Schwierigkeiten mit komplexen Protokollen hat, die Fallunterscheidungen oder Quantorenmanipulation erfordern. Die Arbeit unterstreicht, dass verifizier-gesteuertes Training ohne Anti-Reward-Hacking-Validierung (wie die Diamond-Stufe) unzureichend ist, um aussagekräftige formale Spezifikationen zu erzeugen.