Is 21.269 een priemgetal, dus alleen deelbaar door 1 en zichzelf? Als er één ding is waar computers goed in zijn, is het rekenen. Volgens ChatGPT is 21.269 geen priemgetal, „omdat het deelbaar is door 13”. In werkelijkheid is 21.269 wél priem, iets wat elk computeralgebrasysteem je binnen een fractie van een seconde kan vertellen.
Zulke flaters maakt de chatbot veel. „Chat-GPT gokt gewoon”, zegt wiskundige Johan Commelin van de Universiteit Utrecht in een videogesprek. ChatGPT is dan ook geen rekenaar, maar een taalmodel dat getraind is op een grote database met teksten. Het ontbeert hem aan formele logica. Commelin: „Alle kennis die ChatGPT heeft over rekenen, is gebaseerd op voorbeeldsommen die in zijn training zaten. Daaruit extrapoleert hij hoe hij verwacht dat een rekensom verder gaat. Als ik een chatbox was, zou ik ook gokken dat 21.269 niet priem is. Er zijn immers minder vijfcijferige priemgetallen dan vijfcijferige niet-priemgetallen.”
Of er oneindig veel priemgetallen bestaan (ja), is een vraag waarmee ChatGPT beter overweg kan. Hij is die vraag kennelijk in zijn training tegengekomen en kan keurig het aloude bewijs dat teruggaat tot Euclides, driehonderd jaar voor Christus, leveren. Veel moeilijker is de vraag: zijn er oneindig veel priemtweelingen? ChatGPT blijft het antwoord schuldig. Niet verwonderlijk, want het probleem van de priem-tweelingen is nog altijd onopgelost. ChatGPT komt niet verder dan te vertellen wat priem-tweelingen zijn (paren van priemgetallen met verschil 2, zoals 3 en 5, of 11 en 13) en wat de ontwikkelingen in de voorbije decennia zijn richting een bewijs.
ChatGPT komt niet verder dan te vertellen wat priemtweelingen zijn
Wat gebeurt er als je ChatGPT vraagt of hij zélf het probleem van de priemtweelingen kan oplossen? „Het zou geweldig zijn als ik dat zou kunnen! Helaas is het vinden van een bewijs voor een probleem zoals de priemtweelingconjectuur bijzonder complex. Het vereist niet alleen een diepgaande kennis van getaltheorie, maar vaak ook nieuwe wiskundige inzichten en technieken die nog ontdekt moeten worden. (…) Als kunstmatige intelligentie kan ik wiskundige concepten en technieken analyseren en uitleggen, maar het daadwerkelijk ontwikkelen van nieuwe wiskundige ideeën en inzichten valt nog buiten mijn mogelijkheden.”
Saillant detail is het woordje ‘nog’ in deze laatste zin. Komt er ooit een moment dat een kunstmatige intelligentie de creativiteit van een menselijke intelligentie bezit? ChatGPT zelf houdt die mogelijkheid in elk geval open.
Miljoenen meetkundeproblemen
Dit jaar is een forse stap gezet. Het bedrijf DeepMind, bekend van onder meer AlphaGo, AlphaZero en AlphaFold, lanceerde twee AI-systemen die zijn ontwikkeld om complexe wiskundige vraagstukken te kunnen oplossen: AlphaProof en AlphaGeometry. Het gebruik van computers bij wiskundig onderzoek is niet nieuw (zie inzet). Wat wél nieuw is, is dat de nieuwe tools van DeepMind geen ‘assistenten’ zijn, maar wiskundige problemen van begin tot eind helemaal zélf oplossen. Ze combineren de taalvaardigheid die we kennen van ChatGPT met een ‘formeel redeneersysteem’.
AlphaGeometry is op maat gemaakt voor euclidische meetkunde – dat is de klassieke, tweedimensionale meetkunde. Deze kunstmatige intelligentie werd getraind aan de hand van miljoenen meetkundeproblemen, die automatisch werden gegenereerd. Bleek een oplossingsstrategie niet te werken, dan zocht het systeem naar een andere strategie, zoals: ‘voeg daar een hulplijn toe’, of: ‘halveer die hoek’. AlphaGeometry werd zo steeds beter en sneller in het voorspellen van constructies die tot een correcte oplossing leiden. De nieuwe versie, AlphaGeometry 2, is nóg beter dan zijn voorganger.
AlphaProof is algemener en niet, zoals AlphaGeometry, voor een speciaal deelgebied ontwikkeld. Momenteel blijkt AlphaProof vooral overweg te kunnen met algebra en getaltheorie. Commelin: „ChatGPT gaat dingen verzinnen en heeft zelf geen idee wanneer hij bluft. Alpha-Proof kan logisch redeneren.” Dat AlphaProof daartoe in staat is, komt doordat het gebruikmaakt van de programmeertaal Lean. Lean kan stellingen schrijven en bewijzen. Ook kan het bewijzen verifiëren, zonder tussenkomst van mensen. „Er zit een wisselwerking tussen de AI, die probeert creatief te zijn, en Lean, die niet creatief is, maar wel heel strikt de regels van de wiskunde kent”, zegt Commelin, die zelf deel uitmaakt van de Lean-gemeenschap.
Als je AlphaProof een opgave geeft, gaat hij op zoek naar een oplossing of een bewijs. Het antwoord, of een aanzet daartoe, wordt in de taal van Lean gegeven. Lean evalueert dit en stelt vast welke stappen in het bewijs legaal zijn. Dat voorkomt dat de kunstmatige intelligentie gaat bluffen. Als er een illegale zet is gedaan, of een weg blijkt dood te lopen, dan koppelt Lean dat terug. Vervolgens probeert AlphaProof iets anders. Bij moeilijke problemen gebeurt het maar zelden dat direct de goede weg wordt bewandeld. Dat zie je goed als je een oplossing, geschreven in Lean, terugvertaalt naar normale taal. Commelin: „Je ziet dan vaak allerlei zijsporen die niet relevant zijn. Die worden er niet uitgefilterd. Je krijgt het gevoel dat AlphaProof zijn kladblaadje inlevert.”
Afgelopen zomer vond de vuurproef plaats voor AlphaProof en Alpha-Geometry 2. Zonder tijdslimiet kregen ze de zes opgaven van de International Mathematical Olympiad (IMO) voorgelegd. Deze olympiade is de meest prestigieuze wiskundewedstrijd voor middelbare scholieren en vindt elk jaar in juli plaats. In twee keer vierenhalf uur krijgen de deelnemers, die zich na diverse voorrondes hebben gekwalificeerd, zes hondsmoeilijke vragen voorgelegd uit de getaltheorie, algebra, meetkunde en combinatoriek.
De meetkunde-opgave wist AlphaGeometry 2 in slechts negentien seconden op te lossen. Een mens heeft die tijd alleen al nodig om de opgave te lezen: ‘Zij Δ ABC een driehoek met |AB| < |AC| < |BC|. Zij ω de ingeschreven cirkel van driehoek ABC, en zij I het middelpunt van ω. Zij X het punt, verschillend van C, op de lijn BC zodat de lijn door X die evenwijdig is met AC, raakt aan ω. Analoog, zij Y het punt, verschillend van B, op de lijn BC zodat de lijn door Y die evenwijdig is met AB, raakt aan ω. De lijn AI snijdt de omgeschreven cirkel van driehoek ABC nogmaals in P ≠ A. De middens van de lijnstukken AC en AB noemen we respectievelijk K en L. Bewijs dat ∠KIL + ∠YPX = 180°.’
AlphaProof was succesvol bij drie opgaven over algebra en getaltheorie. Met name de laatste opgave van het toernooi, over zogeheten ‘aquazule functies’ (geen bestaand begrip in de wiskunde; het werd speciaal voor de IMO bedacht) was complex: van de in totaal 609 olympiadedeelnemers waren er slechts vijf die dat probleem konden oplossen. Geen geringe prestatie dus van AlphaProof.
Maar perfect is AlphaProof allerminst. De twee opgaven over combinatoriek – het vakgebied dat zich bezighoudt met het slim tellen van mogelijkheden – kon AlphaProof niet oplossen, en de oplossing van het getaltheorieprobleem was pas rond na drie hele dagen kunstmatig zweten.
Hallucinerende onzin
In september kwam ook het bedrijf OpenAI, eigenaar van ChatGPT, met een nieuwe kunstmatige intelligentie, o1 geheten. Net als de twee systemen van DeepMind, claimt o1 te kunnen ‘denken’ en ‘redeneren’. Het splitst lastige stappen op in eenvoudigere stappen, en het probeert een andere aanpak als de huidige niet werkt.
Terence Tao – een van ’s werelds beste wiskundigen, van de universiteit van Californië – nam de proef op de som. Bij een bepaald probleem, dat kan worden opgelost door de ‘stelling van Cramer’ toe te passen, kon ChatGPT slechts enkele relevante concepten noemen. „Maar de details waren hallucinerende onzin”, schrijft Tao op Mastodon. Daarentegen gaf o1 „een volkomen bevredigend antwoord”.
Minder succesvol was o1 toen Tao hem een probleem van de Hongaarse wiskundige Paul Erdös voorlegde. Het betreffende probleem was tot voor kort onopgelost. Tao wist het probleem recent te kraken; op 2 september postte hij zijn oplossing op de preprintserver arXiv. Tao gaf o1 een deel van de oplossing en vroeg om het ontbrekende ingrediënt. De topwiskundige noemt diens antwoord „licht teleurstellend”, want o1 kwam niet verder dan een voorstel voor een al bestaande strategie; creatieve varianten bleven achterwege.
Intuïtie, creativiteit en vindingrijkheid – typisch menselijke eigenschappen – zijn onontbeerlijk om tot nieuwe wiskundige inzichten te komen. Zullen systemen als AlphaProof en o1 ooit een open probleem, zoals dat over de priemtweelingen, oplossen? Veel wiskundigen zijn voorzichtig met het voorspellen van de toekomst. Vooralsnog noemt Tao het creëren van creatieve strategieën door AI „vrij zwak”.
Optimisten zijn er ook. Zeer uitgesproken is Christian Szegedy, een wiskundige en informaticus die werkzaam is bij xAI van Elon Musk. Szegedy heeft voorspeld dat AI nog vóór 2030 een groot open probleem, waar wiskundigen geen raad mee weten, oplost. Zo ver durft Commelin, net als de meeste wiskundigen, niet te gaan. „Maar ik ga ook niet beweren dat dat nooit zal gebeuren. De grens is vast nog niet bereikt.”
