Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis

De Gids van de Detective voor het Matchen van Dingen

Stel je voor dat je een detective bent die een mysterie probeert op te lossen waarbij twee verschillende beschrijvingen van een plaats delict eigenlijk hetzelfde evenement moeten zijn. De ene getuige zegt: "De verdachte droeg een rode hoed en een blauwe jas," terwijl de andere getuige zegt: "De verdachte droeg een rode hoed en een blauwe jas." Makkelijk, toch? Maar wat als de tweede getuige zegt: "De verdachte droeg een rode hoede en een blauwe jas, maar de hoed was eigenlijk een vermomming voor een blauwe jas"? Nu moet je uitzoeken of deze twee verhalen bij elkaar kunnen passen door de "variabelen" (zoals de specifieke kleuren of voorwerpen) te vervangen door de juiste waarden. In de wereld van de informatica wordt dit puzzelstukje unificatie genoemd. Het is de motor die alles aandrijft, van de kunstmatige intelligentie die schaak speelt tot de software die controleert of je code correct is geschreven.

Decennialang hebben informatici geprobeerd machines te leren om deze puzzel automatisch op te lossen. Het doel is niet alleen om de computer "ja, ze komen overeen" te laten zeggen, maar om de computer het stappenplan (het algoritme) te laten verzinnen voor hoe ze overeenkomen. Dit is een veld genaamd deductieve programmasynthese. Denk eraan als het vragen aan een superintelligente robot om een wiskundig bewijs te leveren, maar in plaats van alleen "Q.E.D." aan het einde te schrijven, moet de robot je een werkend stuk software overhandigen dat het probleem oplost. Het addertje? De robot moet er absoluut zeker van zijn dat de software correct is, want het bewijs is de garantie. Als het bewijs standhoudt, werkt het programma. Als het bewijs faalt, is het programma waardeloos.

De Grote Ontdekking van het Papier: Een Robot Leren Zijn Eigen Puzzeloplosser te Bouwen

Dit artikel, geschreven door Richard Waldinger, is een verhaal over een robot genaamd Snark die werd gevraagd om vanaf nul een unificatie-algoritme te bouwen, met alleen de regels van de logica. De auteur gaf Snark niet simpelweg het antwoord; hij gaf het een set logische regels (een "axiomatische theorie") en een doel: "Vind een substitutie die deze twee expressies identiek maakt."

De belangrijkste bevinding van het papier is dat Snark er succesvol in slaagde om automatisch een werkend unificatie-algoritme af te leiden. Het kopieerde niet zomaar een oud algoritme; het ontdekte een nieuwe versie die daadwerkelijk efficiënter en begrijpelijker is dan sommige eerdere handmatige pogingen. De robot deed dit door de creatie van het programma te behandelen als een gigantische logische puzzel. Het begon met een vaag doel en bouwde, door het proces op te splitsen in kleinere gevallen (zoals "Wat als het eerste item een constante is?" of "Wat als het een variabele is?"), een complex "als-dan-anders"-beslissingsboom. Deze boom is het uiteindelijke programma.

Het papier sluit expliciet uit dat dit een eenvoudige, eenstaps truc was. De auteur geeft toe dat het proces veel "menselijke hulp" vereiste in de vorm van het opzetten van de juiste logische regels en het kiezen van de juiste "wel-gegronde relaties" (een chique manier om te zeggen: "regels die garanderen dat de robot niet in een oneindige lus terechtkomt"). Het papier argumenteert ook tegen de opvatting dat unificatie een eenvoudige, rechttoeخواstaande zaak is. Zoals een citaat in het papier opmerkt: "wanneer een grondige presentatie wordt geprobeerd, wordt er gerealiseerd dat de zaak vrij subtiel en verraderlijk is." Het papier beweert niet dat dit alle problemen van programmasynthese oplost of dat het een wondermiddel is voor alle software engineering. In plaats daarvan presenteert het dit als een succesvolle casestudy die bewijst dat de volledige automatische afleiding van complexe algoritmen mogelijk is, zelfs als dat voor veel andere soorten programma's nog steeds een onderzoeksdoel is.

Hoe de Robot "Dacht"

Om te begrijpen hoe Snark dit deed, stel je voor dat je een kind probeert te leren om een rommelige stapel speelgoed te sorteren. Je zegt niet alleen "sorteer ze." Je geeft ze een set regels: "Als het een blok is, doe het in de rode bak. Als het een auto is, doe het in de blauwe bak." Maar wat als het speelgoed zowel een blok als een auto is? Dan heb je ook een regel nodig voor dat geval.

Snark gebruikte een methode genaamd deductieve tableaux. Stel je een whiteboard voor met twee kolommen: "Wat we weten" (Asserties) en "Wat we moeten vinden" (Doelen).

1. Het Doel: "Vind een manier om Expressie A en Expressie B hetzelfde te laten lijken."
2. Het Proces: Snark kijkt naar het doel en vraagt: "Wat als A een variabele is? Wat als het een constante is?" Het splitst het probleem op in deze verschillende "gevallen".
3. Het "Aha!"-moment: Wanneer Snark beseft dat het om een groot probleem op te lossen, eerst een kleinere versie van hetzelfde probleem moet oplossen, introduceert het recursie. Het is alsof je zegt: "Om deze grote stapel te sorteren, sorteer ik eerst de linkerhelft, dan de rechterhelft, en dan combineer ik ze." Het papier legt uit dat Snark hierbij zeer voorzichtig moest zijn om te voorkomen dat het eeuwig zou blijven sorteren. Het gebruikte een "wel-gegronde relatie" (een wiskundige garantie dat elke stap het probleem strikt kleiner maakt, zoals aftellen van 100 naar 0) om te bewijzen dat het proces uiteindelijk zou stoppen.

De "Environment"-truc

Een van de slimste zetten van het papier was het licht aanpassen van het probleem om het voor de robot makkelijker te maken. In plaats van alleen te vragen "Hoe match je A en B?", kreeg Snark de vraag: "Hoe match je A en B gegeven dat je al een lijst met matches van eerder hebt?" Deze lijst wordt een environment (omgeving) genoemd.

Denk hierbij aan een spelletje "Simon zegt". Als Simon zegt "Raak je neus aan", dan doe je dat. Maar als Simon zegt "Draag een hoed" en daarna zegt "Raak je neus aan", dan moet je de hoed onthouden én je neus aanraken. Door de "environment" (de hoed) bij te houden, kon de robot een efficiënter algoritme bouwen. Het papier suggereert dat deze versie met drie argumenten (Expressie A, Expressie B en de Environment) daadwerkelijk makkelijker voor een computer te synthetiseren is dan de simpelere versie met twee argumenten die mensen gewoonlijk gebruiken.

Het Eindresultaat: Een Nieuw Recept

Het papier concludeert door de eigenlijke code te tonen die Snark heeft geproduceerd. Het ziet eruit als een lange lijst met "als dit, dan dat"-instructies.

• Als de environment defect is, geef dan een "failure"-signaal terug.
• Als de twee expressies al hetzelfde zijn, geef dan de huidige lijst met matches terug.
• Als de één een variabele is en de ander een constante, maak dan een nieuwe regel om ze te verwisselen.
• Als beide complexe structuren zijn (zoals een lijst met items), breek ze dan op in hun linker- en rechterdelen, los eerst het linkerdeel op, en gebruik dat resultaat om het rechterdeel op te lossen.

Het papier benadrukt dat dit programma bewijsbaar correct is. Omdat het programma rechtstreeks uit een logisch bewijs is geëxtraheerd, weten we dat het werkt. Als het bewijs zegt "deze stap is geldig", dan is de codestap geldig. De auteur merkt op dat hoewel het bewijs ongeveer 10 seconden duurde voor het Snark-systeem om te vinden, de echte waarde in de methode zit: het laat zien dat we software kunnen bouwen door stellingen te bewijzen, in plaats van simpelweg te gissen en te controleren.

Waarom Dit Belangrijk Is (En Waarom Het Nog Geen Magie Is)

Het papier eindigt met een speelse knipoog naar de toekomst. Er wordt vermeld dat hoewel moderne AI (zoals Large Language Models) code kan schrijven, ze soms "hallucineren" of feiten verzinnen. Ze kunnen een programma schrijven dat er juist uitziet, maar een verborgen bug bevat. Deductieve synthese is daarente daarentegen als een wiskundig bewijs: als de stappen kloppen, dan moet het resultaat kloppen.

De auteur suggereert een toekomst waarin we deze twee werelden kunnen combineren: een slimme AI gebruiken om te helpen bij het opzetten van de logische regels en de "gissingen" voor het bewijs, en vervolgens een rigoureuze theorem prover gebruiken om het eindresultaat te verifiëren. Maar voor nu staat dit papier als een testament voor de kracht van de logica: een machine was in staat om naar een complex, lastig probleem te kijken en, stap voor stap, zijn eigen oplossing uit te vinden, waarmee bewezen wordt dat de weg naar perfecte software misschien wel een pad van pure wiskunde is.