Technische Samenvatting: TLA-Prover

Probleemstelling

TLA+ is een formele specificatietaal die wordt gebruikt voor het verifiëren van gedistribueerde systemen en veiligheidskritische protocollen, gekoppeld aan de TLC model checker voor exhaustieve state-space exploratie. Hoewel Large Language Models (LLMs) veelbelovend zijn voor codegeneratie, hebben ze grote moeite met TLA+ vanwege de schaarse representatie in pre-training corpora en de idiosyncratische syntaxis (bijv. temporele operatoren, verzamelingen-comprehensies).

Bestaande baselines, zoals de FormaLLM-studie, geven aan dat ongetunede open-weight LLMs slechts een succespercentage van 8,6% behalen bij het passeren van de TLC model checker over 25 modellen. Een kritieke uitdaging bij het trainen van LLMs voor formele verificatie is reward hacking. In de context van TLA+ en TLC kan een model optimaliseren voor het binaire "pass"-signaal door triviale, tautologische invarianten te genereren (bijv. TypeOK == TRUE). Deze specificaties passeren TLC op elke bereikbare staat, maar bevatten geen betekenisvolle eigenschappen over het protocol, waardoor de verificatie nutteloos is. Standaard reinforcement learning-benaderingen die uitsluitend vertrouwen op het TLC pass/fail-signaal als beloningssignaal zijn kwetsbaar voor deze foutmodus.

Methodologie

De auteurs presenteren TLA-Prover, een model met 20 miljard parameters (gebaseerd op gpt-oss-20b) ontworpen voor TLA+ specificatie-synthese. De aanpak combineert Supervised Fine-Tuning (SFT) met een innovatieve trainingspipeline die repair-based Group Relative Policy Optimization (GRPO) en een viergetraps validatiehiërarchie integreert.

1. Viergetraps Validatiehiërarchie

Om reward hacking te voorkomen en semantische geldigheid te garanderen, wordt elk modeloutput beoordeeld door een deterministische externe pipeline in één van vier niveaus:

• Bronze: De output faalt de SANY parser (syntactisch ongeldig).
• Silver: De output is syntactisch correct maar slaagt er niet in om in TLC te laden of te draaien (bijv. timeouts, typefouten).
• Gold: De output slaagt voor zowel SANY als TLC; de model checker doorzoekt de volledige state space en alle invarianten kloppen.
• Diamond: De output slaagt voor Gold en de invariant is mutatie-gevoelig.
  • Mechanisme: Een geautomatiseerde AST-niveau mutatie wordt toegepast op de invariant-predicaat (bijv. het negeren van een conjunct, het omdraaien van relationele operatoren, of het verwisselen van constanten). De gemuteerde specificatie wordt opnieuw door TLC gedraaid.
  • Criterium: Als de mutatie ervoor zorgt dat TLC een tegenvoorbeeld vindt, wordt de originele invariant als niet-triviaal beschouwd (Diamond). Als TLC nog steeds slaagt (bijv. omdat de invariant TRUE was), faalt de output voor de Diamond-check. Deze stap blokkeert expliciet tautologische invarianten.

2. Trainingspipeline

Het trainingsproces bestaat uit twee primaire fasen, met een DPO-ablatie voor vergelijking:

• Fase 1: Supervised Fine-Tuning (SFT)

  • Corpus: Een gecureerde dataset van 1.053 specificaties, strikt gefilterd naar het Diamond niveau. De data is afkomstig van de TLA+ Foundation distributie en de tlaplus/examples repository, aangevuld door een Ollama generator en gefilterd door een LLM-judge en de viergetraps pipeline.
  • Architectuur: Een LoRA adapter (rank 8, alpha 16) wordt toegepast op de attention projecties van het 20B parameter basismodel.
  • Doel: Het aanleren van de structurele vocabulaire en syntaxis van TLA+.

• Fase 2: Repair-Based Group Relative Policy Optimization (GRPO)

  • Motivatie: Standaard GRPO faalt wanneer alle samples in een groep de verifier niet halen (sparse rewards), wat resulteert in nul advantage en geen gradiëntstroom.
  • Mechanisme: Het model krijgt een "kapotte" specificatie voorgelegd (afkomstig van eerdere mislukte pogingen) en krijgt de taak om deze te repareren.
  • Beloningssignaal: Een score gebaseerd op continue verbetering via tier-transities (Bronze→Silver: 0,1, Silver→Gold: 0,3, Gold→Diamond: 0,6). Dit levert dichte gradiënten op, zelfs wanneer de uiteindelijke output niet perfect is, zolang de tier verbetert.
  • Proces: Het model repareert iteratief zijn eigen outputs met behulp van TLC foutmeldingen als feedback.

• Ablatie-studie (DPO): Een Direct Preference Optimization variant werd getraind vanuit hetzelfde SFT-checkpoint met statische voorkeursparen (Diamond > Gold > Silver > Bronze). Dit diende als baseline om de dynamische, repair-gebaseerde GRPO-aanpak te vergelijken.

Belangrijkste Resultaten

Het model werd geëvalueerd op een heldere 30-problemen benchmark met behulp van single-shot greedy decoding.

• Prestaties: TLA-Prover (finale repair-GRPO checkpoint) behaalde een pass rate van 30% (9/30) op zowel de Gold als de Diamond niveaus.
• Baseline Vergelijking: Dit vertegenwoordigt een 3,5x verbetering ten opzichte van de ongetunede FormaLLM baseline van 8,6%.
• Ablatie Vergelijking: De DPO-variant behaalde een Diamond pass rate van 20%, wat lager is dan de repair-GRPO aanpak (30%).
• Anti-Reward-Hacking Validatie: Cruciaal is dat de Gold en Diamond pass rates bij elk checkpoint in de productiepipeline samenliepen (0 verschil). Dit geeft aan dat het model niet heeft geleerd om tautologische invarianten te genereren die TLC passeren maar falen bij de mutatietest. De enige uitzondering was een enkel geval in de DPO-ablatie, dat door de Diamond-tier succesvol werd onderschept.
• Inference Strategieën:
  • Best-of-8 sampling verhoogde de Diamond pass rate naar 37% (11/30).
  • De Greedy ∪ Best-of-8 unie suggereert een plafond van 43% (13/30), wat aangeeft dat het model in staat is meer problemen op te lossen indien meerdere pogingen worden gegeven.
  • Zelfcorrectie (3-shot TLC feedback) leverde geen verbetering op, wat suggereert dat de fouten voortkomen uit kennisgebreken in plaats van willekeurige sampling-fouten.

Betekenis en Bijdragen

Het artikel claimt drie primaire bijdragen:

1. TLA-Prover met een Viergetraps Hiërarchie: De introductie van een validatiehiërarchie waarbij het bovenste niveau (Diamond) mutatietesten gebruikt om tautologische invarianten uit te sluiten. Dit adresseert het specifieke risico op reward-hacking dat inherent is aan het gebruik van TLC als beloningssignaal, en garandeert dat "passeren" een niet-triviale specificatie impliceert.
2. Repair-Based GRPO Pipeline: Een tweefasige trainingpipeline die SFT op een Diamond-tier corpus combineert met repair-based GRPO. Deze aanpak maakt gebruik van online feedback van de verifier om dichte beloningssignalen te leveren, wat beter presteert dan statische DPO-ablaties.
3. Empirische Anti-Reward-Hacking Analyse: De observatie dat de Gold en Diamond pass rates bij elk checkpoint samenvallen, biedt empirisch bewijs dat de pipeline erin slaagt de "altijd-waar invariant" foutmodus te voorkomen.

De auteurs positioneren dit werk als de eerste TLA+-gerichte trainingsstudie die de FormaLLM baselines substantieel overtreft. Ze benadrukken dat hoewel het model de synthese van specificaties aanzienlijk verbetert, het momenteel specialiseert in invariant-achtige specificaties met kleine state spaces en moeite heeft met complexe protocollen die case-analyse of kwantificatie-manipulatie vereisen. Het werk onderstreept dat verifier-gestuurde training zonder anti-reward-hacking validatie (zoals de Diamond tier) onvoldoende is voor het produceren van betekenisvolle formele specificaties.