Verification of a DPLL Transition System in Rocq

Stel je een wereld voor waarin computers constant een spannend spel van "Waar of Onwaar" spelen. In dit spel krijgt de computer een enorme, verwarde knoop van logische stellingen aangereikt—zoals een recept dat zegt: "Als je suiker toevoegt, moet je ook bloem toevoegen, maar als je bloem toevoegt, mag je geen zout toevoegen." Het doel is om een manier te vinden om het recept te volgen zonder de regels te breken. Dit is het Satisfiability (SAT) probleem. Het is het digitale equivalent van proberen een miljoen verschillende puzzelstukjes in een doos te passen waarbij sommige stukjes rood zijn, sommige blauw, en de instructies zeggen: "Geen rood naast blauw."

Waarom geven we erom? Omdat dit niet zomaar een logische puzzel is; het is de motor achter bijna alles wat complex is in de computerwetenschap. Van het ontwerpen van microchips tot het bewijzen dat een wiskundig theorema waar is, computers gebruiken SAT-solvers om door deze enorme logische labyrinten te navigeren. Maar hier is de crux: deze solvers zijn ongelooflijk complex. Als er een piepkleine bug in de code verstopt zit, kan de computer je met vol vertrouwen vertellen dat een bewijs geldig is, terwijl het eigenlijk onzin is. Daarom zijn wiskundigen en informatici geobsedeerd door formele verificatie. Zie het als het bouwen van een superstrak, onbreekbaar veiligheidsnet. In plaats van er alleen maar op te hopen dat de computer werkt, gebruiken ze een speciaal soort "wiskundige microscoop" (een proof assistant) om elke stap van de logica te controleren, om ervoor te zorgen dat de machine nooit kan liegen over het antwoord.

Het Grote Avontuur van het Papier: Het Bouwen van een Betrouwbare Logische Machine

In dit artikel nemen Julia Dijkstra en Benedikt Ahrens een enorme stap richting het betrouwbaar maken van deze logische machines. Ze hebben niet alleen een programma geschreven; ze hebben een wiskundig bewezen skelet gebouwd van een beroemde logische oplosmethode genaamd DPLL (Davis-Putnam-Logemann-Loveland) binnen een tool genaamd Rocq.

Beschouw de DPLL-methode niet als een star robot die een script volgt, maar als een spel van "Toestandswisseling". Stel je een detective voor die een mysterie probeert op te lossen. De detective begint met een leeg notitieblok (geen aanwijzingen). Ze hebben een reeks regels voor hoe ze hun notitieblok bijwerken:

1. De "Oh, ik zie het!" Regel (Unit Propagate): Als een aanwijzing zegt "De butler heeft het gedaan OF de dienstmeid heeft het gedaan," en de detective weet al dat de dienstmeid onschuldig is, dan moet het notitieblok worden bijgewerkt naar "De butler heeft het gedaan." De detective heeft geen keuze; de logica dwingt de zet af.
2. De "Zuivere Gokh" Regel (Pure Literal): Als de detective een aanwijzing ziet over "de tuinman," maar nooit een aanwijzing ziet over "de tuinman niet heeft gedaan," kan de detective veilig gokken dat de tuinman betrokken is zonder angst voor een tegenstrijdigheid.
3. De "Uitwaaier" Regel (Decide): Als de detective vastloopt, kiest hij een willekeurige aanwijzing (zo zoals "De butler heeft het gedaan") en schrijft hij dit op als een beslissing. Dit is een splitsing in de weg.
4. De "Oeps, Foute Afslag" Regel (Backtrack): Als de detective een beslissing opschrijft en later een tegenstrijdigheid vindt (een aanwijzing die zegt "De butler heeft het niet gedaan"), moet hij alles wat er na die beslissing gebeurde wissen, de beslissing omdraaien (nu de butler het niet deed) en opnieuw proberen.
5. De "Game Over" Regel (Fail): Als ze alles wissen, de laatste beslissing omdraaien en nog steeds op een tegenstrijdigheid stuiten, is het spel voorbij. Het mysterie is onoplosbaar.

De belangrijkste prestatie van de auteurs is het nemen van dit hele spel en het opschrijven in een taal die de Rocq proof assistant kan lezen en verifiëren. Ze zeiden niet alleen: "Dit lijkt goed." Ze bewozen drie enorme zaken:

• Correctheid: Als het spel eindigt met een oplossing, is die oplossing zeker echt. De computer zal geen modellen hallucineren.
• Volledigheid: Als er een oplossing bestaat, zal het spel deze vinden. De computer zal niet vastlopen of opgeven wanneer dat niet nodig is.
• Terminatie: Het spel zal nooit eeuwig doorgaan. Het is wiskundig gegarandeerd dat het stopt, ofwel met een oplossing, ofwel met een "Game Over."

Een Nieuwe Twist Toevoegen: De "Zuivere" Regel

Een van de coole bijdragen van het papier is dat ze een specifieke regel aan hun spel hebben toegevoegd die sommige eerdere versies van deze theorie achterlieten: de Pure Literal Regel. In de detective-analogie is dit het moment dat de detective beseft: "Hé, ik heb nooit bewijs gezien tegen de tuinman, dus ik neem gewoon aan dat de tuinman de dader is." De auteurs bewezen dat het toevoegen van deze regel het spel sneller maakt zonder de veiligheidsgaranties te breken. Ze lieten zien dat zelfs met deze extra kortere weg, de logica luchtdicht blijft.

Van Theorie naar een Echte (Maar Simpele) Robot

Nadat ze bewezen hadden dat de regels van het spel in theorie perfect werken, vroegen de auteurs: "Kunnen we daadwerkelijk een robot bouwen die dit spel speelt?" Ze creëerden een strategie—een set instructies voor de detective over welke regel hij als volgende moet kiezen. Ze bouwden een concrete versie van deze strategie in Rocq en gebruikten vervolgens een magische tool genaamd extractie om hun wiskundige bewijs om te zetten in een echt computerprogramma geschreven in OCaml.

Ze testten deze nieuwe robot op enkele eenvoudige puzzels. Het werkte! Het loste problemen correct op, inclusief een puzzel genaamd zebra.cnf met 155 variabelen en 1.135 clausules. De auteurs zijn echter zeer eerlijk over de beperkingen van de robot. Het is als een bewijs-van-concept speelgoedauto: hij rijdt perfect en bewijst dat de motor werkt, maar het is nog geen Formule 1-raceauto. Hij is traag omdat hij eenvoudige lijsten gebruikt om aanwijzingen te onthouden, terwijl echte raceauto's hoogwaardig geheugen gebruiken. De auteurs geven toe dat deze versie niet klaar is om de industriële reuzen te verslaan die vandaag de dag door bedrijven worden gebruikt, maar het is een geverifieerde kern. Het is een kleine, onbreekbare fundering waarop toekomstige, snellere en intelligentere solvers kunnen worden gebouwd.

Wat Dit Betekent voor de Toekomst

Het artikel beweert niet de oplossing te hebben gevonden voor het maken van de snelste SAT-solver ter wereld. In plaats daarvan beweert het een veiligst mogelijke blauwdruk te hebben gebouwd. Door de abstracte regels in Rocq te bewijzen, hebben ze een "vertrouwde kern" gecreëerd. Toekomstige onderzoekers kunnen nu dit blauwdruk nemen en de fancy functies van moderne solvers toevoegen—zoals "leren van fouten" (clause learning) of "meerdere stappen terugspringen" (non-chronological backtracking)—met de zekerheid dat de onderliggende logica nog steeds deugdelijk is.

Kortom, Dijkstra en Ahrens hebben niet alleen een betere auto gebouwd; ze hebben de blauwdruk gebouwd voor een auto die nooit kan crashen, waarbij ze bewezen dat de logica achter de wielen wiskundig perfect is. Het is een kleine, geverifieerde stap die de weg vrijmaakt voor veel grotere, complexere en betrouwbaardere logische machines in de toekomst.