Is er met AI een nieuwe rekenmachine geboren?

Waar in 2023 geen enkel AI-systeem kon scoren op de Internationale Wiskunde Olympiade (IMO), behaalde Google DeepMind in 2024 een zilveren medaille. Het systeem sprokkelde zelfs 28 van de 42 punten, wat net onder de goudgrens valt. Ter vergelijking: 67 van de 630 deelnemers kregen toen een gouden medaille. Dit jaar speldden meerdere AI-systemen, waaronder alweer Google DeepMind, maar ook OpenAI, zich een gouden medaille op door vijf van de zes problemen correct op te lossen. In dus amper twee jaar klom AI van onwetend naar het hoogste schavot op het podium.

Het succes achter deze systemen ligt in de combinatie van twee mechanismen. Enerzijds is er een neuraal netwerk voor patroonherkenning dat lijkt op een Transformer, de motor achter Large Language Models (LLMs) zoals ChatGPT. In 2024 werd het interne taalmodel van DeepMind getraind op miljoenen uitgeschreven meetkundige bewijzen. Hierdoor kan het model zelf potentiële constructieve stappen voorstellen, zoals ‘teken een lijn van punt A naar punt B’ of ‘voeg een middelpunt toe’. Het suggereert dus een meetkundige constructie analoog aan wat het eerder zag in soortgelijke contexten, niet als gevolg van het echt analyseren van het probleem. Het voorstel zit er dan ook vaak naast. Het baanbrekende is om het voorstel vervolgens te voeden aan een redeneermachine. De meetkundige constructies kunnen namelijk omgezet worden in een symbolische voorstelling waarop logische redeneringen kunnen worden toegepast, steunend op bekende stellingen. Zo kunnen de voorstellen dus leiden tot een bewijs of een dood spoor. In het laatste geval vraagt het systeem een nieuw voorstel aan het neuraal netwerk net zolang tot het lukt of tot de tijd om is. Het resultaat is dan niet louter een tekstueel en mogelijk onzinnig betoog, maar een logisch geverifieerd bewijs. Daarenboven kan er door de koppeling met taal zelfs een voor mensen leesbaar bewijs voorgelegd worden.

DeepMinds laatste systeem met deze ‘genereer-en-verifieer’-aanpak maakt gebruik van zogeheten reinforcement learning waarbij geen voorbeeldbewijzen meer nodig zijn. Dit is het principe achter AlphaGoZero, het systeem dat ieder mens op aarde verslaat in het spelletje Go en hierbij zetten uitvoert die nog geen mens ooit heeft gedaan. Tijdens de training wordt er enkel gebruikgemaakt van de ‘spelregels’ en een beloningssysteem. Dankzij enorme rekenkracht kan het systeem veel uitproberen om zo als het ware vanzelf tot succesvolle strategieën te komen. Dit idee kan dus ook op bewijsconstructies worden toegepast. Alleen is de wiskunde geen afgebakend domein zoals een Go-spel met slechts een eindig aantal regels. De wiskunde groeit dagelijks, niet alleen met kennis over bestaande structuren, maar er komen er ook nieuwe bij. Men moet het systeem daarom alvast voeden met wiskundige axioma’s en bestaande definities, waarmee dan via logische afleidingen bestaande resultaten worden geformaliseerd (en tegelijk geverifieerd). Daarnaast is niet elk bewijs een ‘daaruit volgt’-constructie, maar wordt er vaak ook gebruikgemaakt van slimme constructieve stappen. Deze worden momenteel voornamelijk handmatig in de bibliotheek ingevoerd waarbij mensen deze stappen in een geschikte formulering omzetten. Een werk van lange adem dus. Hoe rijker de bibliotheek wordt op het gebied van begrippen én redeneringen, hoe rijker voorgestelde bewijsstappen kunnen worden (zoals gevolgtrekkingen, lemma-toepassingen, tactiekaanroepen, …) wanneer een neuraal netwerk hierop getraind is. Het zijn zulke systemen die nu het goud grijpen.

Momenteel vereist het systeem ook nog menselijke hulp bij het omzetten van IMO-vragen in formele taal. Daarnaast gebeurt het oplossen in een niet-gecontroleerde omgeving waarbij de jury geen zicht heeft op gebruikte hulpmiddelen (rekenmachines, wiskundige software, het internet, …). Een vergelijking met menselijke prestaties gaat dus niet eerlijk op. De systemen werken razendsnel, maar maken onderweg zinloze voorstellen. De menselijke deelnemers hebben echt wel een beter beeld van het probleem, waardoor ze veel doeltreffender werken.

Is zo een systeem op weg om een goede wiskundige te worden? Wel, de systemen die IMO-goud halen, blijken quasi volledig te falen bij volstrekt nieuwe problemen. Waarom deze kloof? Een IMO-probleem, hoe moeilijk ook, past binnen bekende structuren waaruit AI kan putten, maar bij werkelijk nieuwe problemen die een andere denkrichting vereisen, mist de machine de menselijke creativiteit die nodig is om de wiskunde te bedrijven.

De komende jaren zal blijken hoe AI de wiskunde hervormt. Het doel is geen autonome AI-wiskundige, maar een partnerschap: de mens stelt baanbrekende vragen en voegt creativiteit toe, de AI levert rekenkracht en geheugen om die te bewijzen. De nieuwe rekenmachine is geboren.