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

Stel je voor dat je een zeer intelligente, goed onderlegde robot probeert te leren hoe hij een strikt, wiskundig recept moet schrijven voor een complexe machine. Deze machine is een "gedistribueerd systeem" (zoals de cloudservers die Amazon of Microsoft draaien), en het recept wordt geschreven in een speciale taal genaamd TLA+.

Deze taal is als een hoogwaardige puzzel. Als je één klein symbool mist of de logica net iets verkeerd krijgt, kan de machine wel werken volgens het recept, maar in de echte wereld crashen. Het probleem is dat het handmatig schrijven van deze recepten moeilijk en traag is. Daarom vroegen onderzoekers: Kunnen we een moderne AI (een Large Language Model, of LLM) gewoon vragen om deze recepten voor ons te schrijven?

Dit papier is het eerste grote rapportcijfer over die vraag. Dit is wat ze vonden, eenvoudig uitgelegd:

1. De kloof tussen "Grammatica vs. Betekenis"

De onderzoekers vroegen 30 verschillende AI's om deze TLA+-recepten te schrijven op basis van beschrijvingen in gewone mensentaal.

• Het goede nieuws (Grammatica): In ongeveer 26% van de gevallen schreef de AI een recept dat er aan de oppervlakte correct uitzag. De "spellingscontrole" (genaamd SANY) zei: "Oké, de woorden en symbolen staan in de juiste volgorde."
• Het slechte nieuws (Betekenis): Echter, wanneer ze het recept daadwerkelijk door een "logische tester" (genaamd TLC) haalden om te zien of het echt werkte, slaagde het slechts in 8,6% van de gevallen.

De Analogie: Stel je voor dat je een student vraagt om een juridisch contract te schrijven. De student gebruikt perfecte spelling en grammatica (26% succes), maar het contract dat hij schreef zegt eigenlijk het tegenovergestelde van wat bedoeld werd, of laat een cruciale clausule weg, waardoor het juridisch waardeloos is (slechts 8,6% succes). De AI is geweldig in het nabootsen van het uiterlijk van de taal, maar faalt vaak in het begrijpen van de logica erachter.

2. Groter is niet altijd beter

Normaal gesproken nemen we aan dat een grotere, krachtigere AI het beter zal doen. Maar in deze studie was dat niet het geval.

• De verrassing: Een kleiner AI-model (DeepSeek r1:8b) deed het veel beter dan zijn enorme "grote broer" (DeepSeek r1:70b).
• Waarom? Het kleinere model was specifiek getraind om "stap voor stap te denken" (zoals een wiskundestudent die zijn berekeningen laat zien), terwijl het grotere model getraind was op zoveel algemene internetdata dat het in de war raakte door de strikte regels van TLA+. Het is als een gespecialiseerde chef die precies weet hoe hij een soufflé moet bakken, versus een generalist die alles kan koken maar misschien te veel nadenkt over het specifieke recept.

3. "Code-experts" faalden

De onderzoekers testten AI's die beroemd zijn om het schrijven van computercode (zoals Python of Java). Verrassend genoeg deden deze "code-experts" het slechter dan de algemene AI's.

• De reden: Deze modellen zijn zo gewend aan het schrijven van code met puntkomma's (;) of accolades ({}) dat ze deze per ongeluk in het TLA+-recept bleven plaatsen. Omdat TLA+ deze symbolen niet gebruikt, ging het recept direct kapot. Het is alsof een timmerman een horloge probeert te repareren, maar per ongeluk een hamer probeert te gebruiken omdat dat is wat hij voor alles gebruikt.

4. De "Stap-voor-stap" truc werkte het best

De onderzoekers probeerden vier verschillende manieren om de AI om hulp te vragen. De meest succesvolle methode werd "Progressive Prompting" genoemd.

• Hoe het werkte: In plaats van de AI te vragen om het hele recept in één keer te schrijven, vroegen ze het om het stukje bij beetje op te bouwen: "Schrijf eerst de titel. Nu schrijf je de variabelen. Nu de regels."
• Het resultaat: Dit was de enige methode die volledig werkende recepten opleverde (de succesratio van 8,6%). Het is als het bouwen van een huis: als je probeert het dak, de muren en het fundament in één enorme sprong te bouwen, zul je waarschijnlijk falen. Maar als je kamer voor kamer bouwt, heb je een grotere kans op succes.

5. De "Hallucinaties" van de AI

Het papier vond vijf specifieke manieren waarop de AI steeds dezelfde fouten maakte, wat ze "hallucinaties" noemen:

1. Verkeerde symbolen: Het gebruik van fancy wiskundige symbolen (zoals ∧) in plaats van de gewone tekstsymbolen die TLA+ vereist (zoals /\).
2. Taalmixen: Per ongeluk puntkomma's of backticks van andere programmeertalen toevoegen.
3. Hardop denken: De AI plakte soms zijn eigen "denkproces" (zoals ...) direct in het uiteindelijke recept, wat het verpestte.
4. Verkeerde lengte: Soms schreef de AI een recept dat 9 keer te lang was, of schreef de AI bijna niets.
5. Gebroken structuur: Het missen van de "einde"-markeringen van het recept, waardoor het document onvoltooid bleef.

De Kern van het Verhaal

Het papier concludeert dat huidige AI nog niet in staat is om betrouwbare TLA+-specificaties zelfstandig te schrijven. Hoewel het de vorm van de taal kan nabootsen, maakt het nog steeds te veel logische fouten om zonder menselijke controle van een expert elke regel te kunnen vertrouwen.

De onderzoekers suggereren dat we, om dit op te lossen, het volgende moeten doen:

• Gebruik de "stap-voor-stap" prompting methode.
• Gebruik kleinere, op redeneren gerichte modellen in plaats van enorme algemene modellen.
• Bouw tools die de veelvoorkomende fouten automatisch corrigeren (zoals het verwijderen van de verkeerde symbolen) voordat de AI zelfs maar probeert het recept uit te voeren.

Tot die tijd blijft het schrijven van deze cruciale systeemrecepten een taak voor menselijke experts, waarbij AI fungeert als een behulpzame maar foutgevoelige assistent.