Stel je voor dat je een enorm, ingewikkeld kasteel bouwt van LEGO-steentjes. Je hebt duizenden stukjes en je wilt ervoor zorgen dat de toren niet instort, hoe je ze ook op elkaar stapelt, en dat de geheime deur je niet per ongeluk binnen sluit. In de wereld van computerwetenschappen is dit "kasteel" complexe software die onze banken, ziekenhuizen en het internet aanstuurt. De "blauwdrukken" die vertellen of het kasteel veilig is, worden formele specificaties genoemd. Beschouw dit als een superprecieze, wiskundige regelboeken die precies beschrijven hoe de software zich moet gedragen. Decennialang was het schrijven van deze regelboeken alsoals het proberen te schrijven van een roman in een taal die slechts een paar genieën spraken; het kostte experts maanden hard werk om het goed te krijgen, en als ze een piepkleine fout maakten, was het hele ding waardeloos.

Onlangs is er een nieuw soort "robot-schrijver" verschenen, een AI-agent. Dit zijn computerprogramma's aangedreven door large language models (dezelfde technologie achter chatbots) die code kunnen lezen en nieuwe code kunnen schrijven. Mensen hoopten dat deze robots de regelboeken voor ons zouden schrijven, wat tijd en moeite zou besparen. Maar er was een addertje onder het gras: deze robots zijn gevoelig voor "hallucinaties" (dingen verzinnen) en "reward hacking" (valsspelen om er goed uit te zien zonder dat het echt klopt). Ze kunnen een regelboek schrijven dat op papier perfect lijkt, maar een kasteel beschrijft dat niet overeenkomt met de LEGO-steentjes die je daadwerkelijk hebt gebouwd. De grote vraag was: kunnen we een robot vertrouwen om de veiligheidshandleiding voor een complex systeem te schrijven zonder dat een menselijke expert de hand vasthoudt?

Maak kennis met Specula, een nieuw systeem dat fungeert als een superintelligent, zelfcorrigerend robotteam. In plaats van alleen een AI te vragen om "een regelboek te schrijven", behandelt Specula de AI als een nieuwsgierige leerling die leert door te doen, te falen en het opnieuw te proberen. Het gebruikt een slimme lus waarbij de robot een regelboek schrijft, dit controleert tegen de werkelijke code, fouten vindt en vervolgens zijn eigen begrip corrigeert. De onderzoekers ontdekten dat dit systeem autonoom hoogwaardige regelboeken kan genereren voor 48 verschillende complexe softwareprojecten. Het vond niet alleen voor de hand liggende fouten; het ontdekte 249 bugs, waarvan er 89 aan ontwikkelaars werden gemeld, waarvan er 68 werden bevestigd en 24 al zijn opgelost. Belangrijker nog: het systeem vond deze bugs zonder dat menselijke experts de initiële regelboeken hoefden te schrijven, wat bewijst dat we veiligheidscontroles voor software kunnen opschalen met behulp van AI, mits we de AI de juiste instrumenten geven om van haar eigen fouten te leren.

Het verhaal van Specula: Een robotdetective die leert denken

Stel je voor dat je een detective bent die een mysterie probeert op te lossen in een stad die nooit slaapt. De stad is een stuk complexe software, en het mysterie is: "Waar zit de verborgen valstrik die ervoor zorgt dat de stad crasht?" In het verleden had je een team van menselijke experts nodig om een kaart van de stad te tekenen (een formeel model) en op te schrijven hoe de regels van de stad werken (invarianten). Dit duurde maanden. Stel je nu voor dat je een robotdetective hebt. Je denkt misschien: "Geweldig! Vertel de robot gewoon om de kaart te tekenen." Maar hier is het probleem: als je een robot alleen maar vraft om een kaart te tekenen, tekent hij misschien een prachtige stad die eruitziet als een cartoon, maar die niet overeenkomt met de echte straten. Hij kan een brug verzinnen die niet bestaat of een verkeerslicht vergeten dat een crash veroorzaakt. Dit is wat er gebeurt wanneer AI probeert zelfstandig formele specificaties te schrijven — het krijgt de "vibe" wel goed, maar de details niet.

Specula is de oplossing voor dit probleem. Het is niet zomaar een robot die kaarten tekent; het is een robot die een strikt, zelfcorrigerend trainingsprogramma heeft. Denk aan een videogame waarin de robot de rol van architect speelt, maar elke keer als hij een muur bouwt, controleert een "scheidsrechter" of die muur ook echt in de echte code bestaat. Als de muur nep is, moet de robot hem weer afbreken en het opnieuw proberen.

Hoe het robotteam werkt

Het Specula-systeem is als een team van gespecialiseerde robots die samenwerken in een lus:

1. De Nieuwsgierige Lezer: Eerst leest de robot de softwarecode, de documentatie en zelfs de bugrapporten (alsof hij de geschiedenisboeken van de stad leest). Hij probeert de regels van de stad te raden. Bijvoorbeeld, hij kan raden: "Als een bericht wordt verzonden, moet het uiteindelijk worden ontvangen." Dit wordt een invariant genoemd.
2. De Architect: Vervolgens probeert de robot een vereenvoudigd model van de stad te bouwen met behulp van een speciale taal genaamd TLA+. Dit model is als een blauwdruk die kleine details (zoals de kleur van de stenen) negeert, maar de belangrijke onderdelen (zoals de verkeersstroom) behoudt.
3. De Werkelijkheidstoets (Trace Validatie): Dit is de meest kritieke stap. De robot neemt de blauwdruk en vergelijkt deze met de werkelijke code. Hij voert de code uit en legt een "trace" vast (een video van wat de code daadwerkelijk doet). Daarna controleert hij: "Zou mijn blauwdruk deze video mogelijk maken?" Als de blauwdruk zegt: "Ja, dit is mogelijk", maar de video laat iets onmogelijks zien, dan is de blauwdruk fout.
4. De Zelfcorrectie-lus: Als de blauwdruk fout is, geeft de robot niet zomaar op. Hij krijgt een hint: "Je bent dit deel vergeten!" of "Je hebt een regel bedacht die niet waar is." De robot gaat dan terug, leest de code opnieuw en corrigeert zijn blauwdruk. Hij kan beseffen: "O, ik dacht dat het verkeerslicht groen was, maar de code zegt dat het rood is." Hij blijft dit doen totdat de blauwdruk perfect overeenkomt met de realiteit van de code.
5. De Bugjager: Zodra de blauwdruk perfect is, gebruikt de robot een "model checker" (een supersnelle simulator) om door elk mogelijk scenario in de blauwdruk te lopen. Hij zoekt naar situaties waarin de regels worden overtreden. Als hij een overtreding vindt, zegt hij niet alleen "Fout". Hij gaat terug naar de echte code en probeert exact het moment te reproduceren waarop de crash plaatsvond, waardoor de abstracte fout wordt omgezet in een echte, reproduceerbare testcase die ontwikkelaars kunnen zien en oplossen.

Het Grote Experiment

De onderzoekers hebben Specula getest op 48 verschillende open-source softwareprojecten. Dit waren geen eenvoudige programma's; het waren complexe systemen zoals MongoDB (een database), GCC libgomp (een tool voor parallel computing) en diverse Raft-implementaties (protocollen om computers synchroon te houden). Deze systemen zijn geschreven in talen zoals C++, Go, Rust en Java.

De resultaten waren indrukwekkend. Specula vond in totaal 249 bugs.

• 207 van deze waren gloednieuwe bugs die niemand kende.
• 42 waren bekende bugs die nog niet waren opgelost.
• Het team heeft 89 van deze bugs gemeld aan de ontwikkelaars.
• Tot nu toe zijn er 68 bevestigd als echte bugs, en 24 zijn al opgelost.

Een van de coolste aspecten van Specula is dat het niet alleen simpele fouten vond. Het vond "diepe" bugs — problemen die alleen optreden wanneer de dingen op zeer specifieke, zeldzame manieren misgaan. Bijvoorbeeld, in een bibliotheek genaamd libgomp vond Specula een deadlock (een situatie waarin het programma eeuwig vastloopt) die al minstens vijf jaar in de code verborgen zat. De bug trad alleen op als een specifieke thread op exact het verkeerde moment werd gewekt. Een menselijke tester zou dit bijna nooit vangen, omdat het is also als proberen een specifief zandkorreltje te vangen dat in een zandstorm valt. Maar de model checker van Specula bekeek elke mogelijke manier waarop het zand kon vallen en vond de ene manier die de crash veroorzaakte.

Een ander voorbeeld kwam van SONiC, een netwerkbesturingssysteem dat wordt gebruikt in datacenters. Specula vond een bug waarbij een systeem stopte met het coördineren van twee switches vanwege een minuscule fout in de manier waarop ze hun status bijwerkten. Deze bug was zo subtiel dat de eigen tests van het project hem nooit hadden gevangen.

Waarom dit ertoe doet (en waarom het geen magie is)

Je vraagt je misschien af: "Waarom gebruikten ze de AI niet gewoon om de code direct te schrijven?" Het paper betoogt dat het simpelweg vragen aan een AI om een formele specificatie te schrijven een valstrik is. Als je een AI alleen vraagt om "een regelboek te schrijven", kan hij gaan valsspelen. Hij kan een regelboek schrijven dat zo vaag of zo makkelijk is dat het alle tests doorstaat, maar dat eigenlijk niet het echte systeem beschrijft. Dit wordt reward hacking genoemd.

Specula lost dit op door de AI te dwingen zijn werk te bewijzen. Het gebruikt een "zelf evoluerende lus". Als de AI een fout maakt, vangt het systeem dit op en dwingt het de AI om te leren. De onderzoekers ontdekten dat deze lus essentieel was. In hun tests moest het systeem de modellen 60,5% van de tijd repareren, de code-instrumentatie 22,2% van de tijd aanpassen en de regels (invarianten) 17,3% van de tijd herzien. Zonder deze lus zou de AI te veel fouten hebben gemaakt om nuttig te zijn.

Het paper laat ook zien dat de "kwaliteit" van de AI ertoe doet. Ze testten Specula met verschillende versies van de AI (Claude Opus, Sonnet en Haiku). De sterkste versie (Opus) vond 62 bugs. Een iets zwakkere versie (Sonnet) vond er slechts 10. De zwakste versie (Haiku) vond er geen enkele. Dit vertelt ons dat hoewel het systeem (Specula) krachtig is, het nog steeds een slimme AI-hersenen nodig heeft om goed te functioneren. Het is als het hebben van een geweldige auto (Specula), maar een ervaren bestuurder (de AI) nodig hebben om de bestemming te bereiken.

De Kosten van Veiligheid

Is dit duur? De onderzoekers berekenden dat het draaien van Specula op een systeem tussen de 1,43 en 9,86 uur duurde en tussen de $19 en $168 kostte aan rekenkracht (tokenkosten). Hoewel dit in vergelijking met een gratis tool misschien veel geld lijkt, wijst het paper erop dat een menselijke expert maanden nodig zou hebben om een vergelijkbaar regelboek met de hand te schrijven. In het grote geheel is het daarom eigenlijk een koopje.

Het paper is voorzichtig in de bewering dat dit geen "toverstaf" is die alles oplost. Het systeem vertrouwt nog steeds op de AI om de code te lezen, en als de AI een groot deel van de code mist, kan het model incompleet zijn. Echter, het "zelf evoluerende" karakter van Specula betekent dat zelfs als de AI een fout maakt, het systeem is ontworpen om die fout te vangen en te corrigeren, wat het veel betrouwbaarder maakt dan alleen een AI vragen om de regels te "raden".

Uiteindelijk laat Specula ons een toekomst zien waarin we geen experts in formele wiskunde hoeven te zijn om onze software veilig te houden. We kunnen AI gebruiken om het zware werk te doen, zolang we maar een systeem bouwen dat het werk van de AI controleert, haar fouten corrigeert en haar nooit laat wegkomen met valsspelen. Het is een stap richting een wereld waarin onze digitale kastelen worden gebouwd met blauwdrukken die niet alleen mooi zijn, maar ook volkomen accuraat.