Towards Language Model Guided TLA+ Proof Automation

Titel: Towards Language Model Guided TLA+ Proof Automation

Auteurs: Yuhao Zhou en Stavros Tripakis (Noordoostelijke Universiteit, Boston)

---

1. Probleemstelling

Formele verificatie met TLA+ (Temporal Logic of Actions) biedt rigoureuze garanties voor systeemspecificaties, met name voor gedistribueerde systemen. Het bouwen van formele bewijzen in TLA+ is echter een grote bottleneck:

• Expertisevereiste: Het vereist aanzienlijke menselijke expertise en inspanning.
• Hiërarchische structuur: In tegenstelling tot tactic-based bewijssystemen (zoals Lean of Coq) die werken met een sequentiële reeks commando's (tactics), is de TLA+-bewijsstructuur hiërarchisch. Bewijzen worden opgebouwd als bomen van claims en sub-claims (lemmata).
• Uitdaging voor LLM's: Bestaande methoden die Large Language Models (LLM's) gebruiken om bewijzen te genereren, zijn vaak gericht op tactic-based systemen. Direct toepassen van deze methoden op TLA+ leidt tot twee grote problemen:
  1. Syntactische fouten: LLM's genereren vaak onjuiste TLA+-syntaxis, wat verhindert dat de bewijzen door backend-provers (zoals TLAPS) worden geverifieerd.
  2. Monolithische generatie: Het genereren van een volledig bewijs in één keer maakt het moeilijk om fouten op te vangen; een fout in een vroeg stadium kan het hele bewijs ongeldig maken zonder dat er tussentijdse verificatie plaatsvindt.
• Gebrek aan data: Er ontbreken grote datasets van TLA+-bewijzen om LLM's op te trainen, in tegenstelling tot systemen zoals Lean.

2. Methodologie: LMGPA

De auteurs presenteren LMGPA (Language Model Guided Proof Automation), een aanpak die de sterke punten van LLM's (redeneren en decompositie) combineert met symbolische provers (rigoureuze verificatie).

Kerninzicht:
In plaats van de LLM te vragen om een volledig bewijs te genereren, wordt de LLM beperkt tot het genereren van genormaliseerde claim-decomposities. De LLM breekt complexe bewijsverplichtingen op in eenvoudigere sub-claims, terwijl de symbolische prover (TLAPS) de verificatie uitvoert.

Het Algorithmische Proces (Rekursieve Decompositie):
Het systeem werkt recursief volgens het volgende algoritme (Algorithm 2 in het paper):

1. Auto-proof poging: Eerst wordt geprobeerd om een bewijs direct te genereren met TLA+-directives (zoals OBVIOUS of BY DEF), die door TLAPS direct kunnen worden geverifieerd.
2. Decompositie: Als een auto-proof faalt, vraagt het systeem de LLM om de huidige claim op te splitsen in een set van sub-claims.
   • Genormaliseerde Structuur: De LLM wordt verplicht om output te genereren in een strikt, genormaliseerd formaat (ASSUME-PROVE structuur met ASCII-symboolen). Dit minimaliseert syntactische fouten.
   • Validatie: Het systeem verifieert of de gegenereerde sub-claims collectief de ouderclaim aantonen. Als dit faalt, krijgt de LLM feedback en probeert het opnieuw.
3. Rekursie: Voor elke geldige sub-claim wordt het proces recursief herhaald totdat alle bladeren van de bewijst boom direct door TLAPS kunnen worden geverifieerd.
4. Samenstelling: De uiteindelijke output is een compleet TLA+-bewijs dat de hiërarchische structuur volgt.

Technische Implementatie:

• Tools: Python 3.12, Tree-sitter voor parsing, LangChain voor LLM-interactie, en TLAPS (met backends Z3, Zenon, Isabelle) voor verificatie.
• Prompt Engineering: De prompts bevatten strikte instructies voor de syntaxis (bijv. gebruik van \A voor forall, geen Unicode) en de structuur van de sub-claims. Er wordt geen fine-tuning van de modellen gebruikt; het systeem vertrouwt puur op prompting.

3. Belangrijkste Bijdragen

1. LMGPA Framework: Een nieuw systeem dat LLM's succesvol toepast op het hiërarchische bewijzen in TLA+ door de taak te beperken tot decompositie in plaats van volledige bewijsgeneratie.
2. Genormaliseerde Claim-decompositie: Een strategie die syntactische fouten drastisch reduceert door de LLM output te beperken tot een gestructureerd formaat dat door de machine kan worden omgezet in geldige TLA+-code.
3. Benchmarksuite: De creatie van een nieuwe benchmark bestaande uit 119 theorema's:
   • 93 wiskundige theorema's (gebaseerd op miniF2F en ProofNet, handmatig vertaald naar TLA+).
   • 26 inductieve bewijzen voor kandidaat-invarianten van gedistribueerde protocollen.
4. Empirische Validatie: Uitgebreide experimenten die aantonen dat de methode superieur is aan bestaande baselines.

4. Resultaten

De evaluatie toont aan dat LMGPA consistent beter presteert dan de baselines (naïeve symbolische methoden en directe LLM-generatie) op alle geteste modellen (o.a. Claude 3.7, GPT-5, o3-mini, DeepSeek).

• Succespercentages:
  • Wiskundige benchmarks: LMGPA bereikte een succespercentage van 53,8% - 59,1% (afhankelijk van het model), vergeleken met slechts 17,2% - 29,0% voor directe LLM-generatie (DLPG) en 44,1% - 49,5% voor de puur symbolische methode (SAPG).
  • Gedistribueerde protocollen: LMGPA behaalde 38,5% - 50,0% succes, terwijl directe LLM-generatie vaak faalde (0% - 15,4%) en de symbolische methode slechts 38,5% haalde.
• Syntactische Validiteit: Een cruciale bevinding is dat LMGPA een veel hogere syntactische validiteit heeft dan directe generatie.
  • Bij directe generatie (DLPG) varieerde de syntactische validiteit tussen 0,2% en 20,3%.
  • Bij LMGPA (generatie van decomposities) lag de validiteit tussen 63,9% en 85,9%.
  • Dit bevestigt dat het beperken van de LLM-taak de belangrijkste oorzaak van fouten (syntaxis) wegneemt.
• Efficiëntie: Hoewel LMGPA meer LLM-query's vereist dan een directe poging, is het totaal aantal queries lager dan bij mislukte pogingen van directe generatie die constant opnieuw moeten worden geprobeerd.

5. Betekenis en Toekomstperspectief

• Doorbraak in TLA+ Automatisering: Dit werk overbrugt de kloof tussen de kracht van LLM's en de specifieke eisen van het TLA+-bewijsstelsel. Het toont aan dat LLM's nuttig kunnen zijn voor formele verificatie zonder dat ze volledig op de syntaxis hoeven te vertrouwen.
• Praktische Toepassing: De methode maakt het mogelijk om complexe bewijzen voor gedistribueerde systemen (zoals die gebruikt door Amazon en Microsoft) te automatiseren, wat de drempel voor formele verificatie verlaagt.
• Toekomstig Werk: De auteurs wijzen op de noodzaak van:
  • Fine-tuning op TLA+-corpora om de kwaliteit van decomposities verder te verbeteren.
  • Het ontwikkelen van benchmarks zonder data-lekkage.
  • Het trainen van LLM's om de beperkingen van symbolische provers te begrijpen, zodat ze decomposities genereren die niet alleen wiskundig correct zijn, maar ook door de prover binnen de tijdslimiet kunnen worden geverifieerd.

Conclusie:
Het paper demonstreert dat een hybride aanpak, waarbij LLM's fungeren als "architecten" voor de bewijsstructuur (decompositie) en symbolische provers als "bouwers" (verificatie), een effectieve strategie is om de automatisering van TLA+-bewijzen te realiseren. Dit lost het probleem van syntactische fouten op en biedt een schaalbare weg naar meer toegankelijke formele verificatie.