Op vleugels van vervulbaarheid

Steeds vaker worden wiskundige bewijzen – deels – door de computer geleverd, met software die uitgaat van ‘vervulbaarheid’. Twee logici wisten er een deel van een tachtig jaar oud probleem mee op te lossen.

illustratie Roland Blokhuizen

Ooit, in 1976, werd voor het eerst een wiskundige stelling bewezen met een computer. En vol van verontwaardiging spraken puristen schande van de onbetrouwbaarheid, omdat geen mens de talloze computerberekeningen kon controleren. Begrijpelijk was dat wel: in die tijd was de beschikbare software een janboel. Het ging om het bewijs van de vierkleurenstelling, in 1852 geformuleerd door Francis Guthrie, die zegt dat elke landkaart met hooguit vier kleuren gekleurd kan worden op zo’n manier, dat twee naastgelegen gebieden nooit dezelfde kleur hebben. Een computer had 1200 uur rekentijd nodig om 1482 mogelijke landkaartconfiguraties met soms honderdduizenden individuele gevallen door te rekenen en te controleren of er een toegestane kleuring bestond.

Nu is het vertrouwen in computerbewijzen veel groter. Het ‘menselijk begrip’ wordt door de meeste wiskundigen niet meer als betrouwbaarder gezien dan een computerprogramma. Freek Wiedijk is wiskundige aan de Radboud Universiteit Nijmegen en hij zegt het zo: „Het is alsof biologie die met het blote oog kan worden gedaan een andere status zou hebben dan biologie die een microscoop nodig heeft. Ik zie het probleem niet, en bij wiskunde met of zonder computer net zo min.” En ook bij zo’n computerprogramma komt het aan op menselijk begrip, want programmeren is mensenwerk.

Bij moderne computerbewijzen draait alles om ‘vervulbaarheid’, oftewel: om SAT-software. ‘SAT’ staat voor satisfiability, een begrip uit de mathematische logica. Met logische operaties als ‘of’, ‘en’ en ‘niet’ en een stel zogeheten Boolese variabelen (vernoemd naar George Boole, de vader van de symbolische logica), die alle de waarde ‘waar’ of ‘onwaar’ kunnen aannemen, kun je formules maken. Zo’n formule heet ‘vervulbaar’ als je waarden (waar of onwaar) aan de variabelen kunt toekennen op zo’n manier dat de formule zélf waar is. Twee banale voorbeelden: de formule ‘x en y’ is vervulbaar omdat de toekenning ‘x is waar en y is waar’ voldoet, en de formule ‘x of y’ is vervulbaar omdat de toekenning ‘x is waar en y is waar’ voldoet, net als de toekenningen ‘x is waar en y is onwaar’ en ‘x is onwaar en y is waar’, overigens.

Een SAT-solver is een programma dat zo’n formule inleest en vaststelt of hij vervulbaar is, en zo ja ook een vervulling aangeeft: de waarden voor de variabelen waarvoor de formule waar is. Een formule-oplosser, als het ware. De computer construeert zo een bewijs met behulp van technieken die aanvankelijk erg gevoelig waren voor fouten, maar die de laatste jaren revolutionair zijn verbeterd. Ze worden daarom steeds vaker ingezet om stellingen te bewijzen die mensen niet voor elkaar krijgen. „Iedereen, werkelijk iedereen, codeert zijn problemen tegenwoordig zó, dat een SAT-solver het kan verwerken,” aldus Wiedijk.

Een recente SAT-doorbraak is een bewijs van een speciaal geval van het discrepantievermoeden, dat in 1932 werd geformuleerd door de Hongaar Paul Erdös, en ruim twintig jaar later – onafhankelijk daarvan – door de Rus Nikolai Cudakov. Dat vermoeden gaat over patronen in ‘±1-rijen’, willekeurige rijen die uit niets anders bestaan dan de getallen +1 en –1. De ‘discrepantie’ van zo’n rij is de grootst mogelijke afwijking – ten opzichte van nul – van de som van de termen in een deelrijtje waarvan de termen op gelijke afstand van elkaar liggen (zie inzet).

Het algemene probleem is nog altijd niet opgelost, maar een computerondersteund bewijs van een speciaal geval, geleverd door Boris Konev en Alexei Lisitsa (University of Liverpool), is deze zomer gepubliceerd door het tijdschrift Artificial Intelligence. Voor hun bewijs moest worden aangetoond dat de discrepantie van élke ±1 1-rij van lengte 1.161 ten minste 3 is. Van zulke rijen bestaan er 21161, ongeveer 3 × 10349. Met de hand een onmogelijke taak, en zonder slim programmeerwerk ook voor een computer niet te doen. Zou een computer een miljard rijtjes per seconde kunnen checken, dan zou hij hier bijna 10333 jaar mee bezig zijn, veel langer dan de leeftijd van het heelal.

Verificatie

Konev en Lisitsa vertaalden het probleem in Boolese algebra zodat een SAT-solver het probleem wél te lijf kon gaan. Voor het bewijs hoefde de SAT-solver ‘slechts’ 70 miljoen gevallen te onderzoeken; daarmee waren álle 21161 rijen van lengte 1161 afgedekt. De solver kon voor die 70 miljoen reeksen in korte tijd nagaan of hun discrepantie ten minste 3 is. Daartoe schreven de onderzoekers formules uit die horen bij rijen van lengte 1160 en 1161. Het resultaat van de SAT-solver was dat er bij 1160 een toekenning is waarvoor alle formules vervulbaar zijn; dat betekent dat er een ±1-rij van lengte 1160 bestaat waarvan de discrepantie onder de 3 blijft. Bij 1161 bleek zo’n toekenning niet te bestaan, hetgeen impliceert dat de discrepantie van elke rij van die lengte ten minste 3 is.

In een modern computerbewijs zit ook een tweede stap: verificatie. Vaak kan het computerresultaat worden geverifieerd door een ‘bewijschecker’ of ‘bewijsassistent’: een onafhankelijk computerprogramma gaat dan de juistheid van een door een SAT-solver geleverd bewijs na. Als de checker het in orde vindt, kun je er vanuit gaan dat de SAT-solver zijn werk zonder fouten heeft gedaan.

In theorie kan zo’n checker óók fouten maken, maar de kans daarop is zeer klein. Jan Friso Groote, hoogleraar informatica aan de Technische Universiteit Eindhoven, noemt de betrouwbaarheid van checkers ‘extreem hoog’. „Ik heb enkele grote bewijzen door Coq [een van de bekendste bewijsassistenten] gehaald. De extreem subtiele fouten die daarmee boven water kwamen, hebben mij zeer overtuigd van de kracht van dergelijke tools. Interactieve bewijsassistenten zijn vele malen preciezer in het controleren van een bewijs dan de beste wiskundige. De Laatste Stelling van Fermat [in 1994 bewezen door Andrew Wiles, zonder computer] is in mijn ogen ook pas bewezen wanneer een interactieve bewijsassistent er zijn zegen aan heeft gegeven,” zegt Groote.

Marijn Heule, die als postdoc-onderzoeker aan de Technische Universiteit Delft werkte aan SAT-solvers en sinds 2012 verbonden is aan het Department of Computer Sciences van de University of Texas (Austin), verwacht dat er niet veel wiskundigen zijn die zullen twijfelen aan de juistheid van het bewijs van het speciale geval van het discrepantievermoeden. Dat komt met name door de validatie van het bewijs door diverse bewijscheckers. Een van die checkers is drup-trim, ontwikkeld door Heule zelf.

Heules checker kon niet alleen het bewijs valideren, maar kon het ook optimaliseren. Toen Konev en Lisitsa hun bewijs presenteerden, vorige zomer tijdens een conferentie in Wenen, was de output van de SAT-solver een file van 13 gigabyte. Ter vergelijking: alle tekst op de Engelse Wikipedia, met bijna vijf miljoen lemma’s, is zo’n 10 gigabyte. Heules checker produceerde een veel compacter bewijs: slechts zes procent van het oorspronkelijke.

Slim mensenwerk

Hoewel er met een computerbewijs duidelijkheid is dát een stelling waar is (al helemaal als het ook de zegen van een checker heeft), blijft voor sommige wiskundigen een nadeel dat het onduidelijk blijft waaróm die waar is. „Omdat miljoenen gevallen zijn gecontroleerd en allemaal OK bleken te zijn” is dan geen bevredigend antwoord.

Aan de andere kant: het is ook fout om een bewijs volledig toe te schrijven aan de computer. Meestal doet de computer ‘slechts’ het omvangrijke rekenwerk, waar geen conceptvorming aan te pas komt. Bij zowel het bewijs van het vierkleurenprobleem uit 1976 als het recente bewijs van het discrepantievermoeden ging de computer systematisch een groot aantal gevallen af, maar er kwam slim mensenwerk aan te pas om de computer te laten doen wat hij moest doen: daarbij gaat het wel degelijk om begrip.