Een kunstmatig intelligent systeem heeft van vijf wiskundige vermoedens bewezen dat ze niet waar zijn. Dat deed het systeem zonder enige aanvullende informatie over de problemen.
De kunstmatige intelligentie (AI) is ontwikkeld door wiskundige Adam Zsolt Wagner van de Tel Aviv Universiteit in Israël. Het systeem zocht naar tegenvoorbeelden voor een reeks langdurig openstaande vermoedens in grafentheorie – een tak van de wiskunde waarin objecten worden bestudeerd die bestaan uit knooppunten en verbindingen. Wiskundigen dachten altijd dat die vermoedens juist waren, maar konden dat niet bewijzen.
Voor elk vermoeden ontwikkelde Wagner een maatstaf voor hoe dicht een bepaald voorbeeld het ontkrachten ervan benadert. Neem bijvoorbeeld een vermoeden dat stelt dat een bepaald probleem niet in minder dan vijf stappen kan worden opgelost. Een oplossing met zes stappen komt dan dichter bij ontkrachting dan een oplossing met zeven stappen. En een oplossing met vier stappen is een weerlegging van het vermoeden.
Simpel
Wagner programmeerde een neuraal netwerk zodanig dat het steeds een aantal willekeurige voorbeelden genereerde. Via de maatstaven beoordeelde het systeem telkens van elk daarvan hoe geschikt het was als weerlegging. Vervolgens gooide de AI de slechtst scorende voorbeelden weg, om daar nieuwe willekeurige voorbeelden voor in de plaats te brengen. Daarna begon de beoordeling opnieuw.
‘We gooien gewoon telkens de slechte voorbeelden weg en leren van de beste’, zegt Wagner. ‘De computerarchitectuur is echt zo simpel als maar kan. Er gebeurt niks bijzonders.’
Bij enkele tientallen vermoedens kon de AI geen voorbeeld vinden dat de theorie ontkrachtte. Maar in vijf gevallen kwam die wel bij een oplossing terecht die uitwees dat het vermoeden niet klopte.
Wagner liet het systeem draaien op zijn vijf jaar oude laptop. Het ontkrachten van elk van de vijf vermoedens duurde enkele uren tot enkele dagen. Vaak was het resultaat contra-intuïtief. ‘Al gaf je me honderd jaar; ik was nooit uit mezelf op deze constructies gekomen’, zegt Wagner.
Creatief werk
‘Het is absoluut indrukwekkend’, zegt wiskundige Leslie Hogben van de Iowa State Universiteit in de VS. Zij zag een van haar vermoedens door de AI worden ontkracht. ‘We zien hier een enorm voordeel van kunstmatige intelligentie, en vanuit wiskundig oogpunt zit daar geen keerzijde aan. Het systeem vindt simpelweg dingen voor ons, alsof het iemand met geweldig inzicht is. De tegenvoorbeelden zijn echt spelden in hooibergen.’
Waar de AI erin is geslaagd om vermoedens te ontkrachten, is het bewijzen ervan veel moeilijker. Het ontkrachten van een idee vergt namelijk alleen het opstellen en testen van een enorme hoeveelheid mogelijke oplossingen, om te zien of één daarvan het vermoeden weerspreekt. Dat klusje kan simpel geautomatiseerd worden.
Een bewijs vinden is daarentegen creatief werk. Dat vereist scherpzinnige sprongen en omvat het verbinden van vele logische gevolgtrekkingen.
Gouden standaard
De eerste theorie die met behulp van een computer is bewezen, is de vierkleurenstelling. Die stelt dat met vier kleuren elke landkaart zodanig kan worden ingekleurd, dat er geen twee landen van dezelfde kleur elkaar raken. In 1976 werd deze stelling bewezen met behulp van een computer die een onuitputtelijke lijst voorbeelden naging. Destijds vonden sommigen dat niet zo elegant, maar tegenwoordig is het gebruik van computers bij wiskundige problemen volkomen geaccepteerd.
Toch is het volgens Hogben van belang dat menselijke wiskundigen te allen tijde een bewijs kunnen volgen. ‘Persoonlijk zou ik nooit een probleem hebben met een verifieerbare weerlegging. Maar een computerbewijs dat niet met de hand is na te rekenen, daar zou ik me wel zorgen om maken. Dat gaat voor mij in tegen de gouden standaard van de wiskunde’, zegt ze.
Wiskundige Timothy Gowers van de Collège de France in Parijs noemde de benadering op Twitter een interessant proof of concept. ‘Het is moeilijk voorstelbaar dat dit het einde van het verhaal is. Misschien kan dit worden omgevormd tot een eenvoudige ‘controleer je vermoedens-tool’. Dat zou wiskundigen enorm helpen’, zegt hij.
