Donderdag maakte Google DeepMind bekend dat AI-systemen genaamd AlphaProof en AlphaGeometry 2 naar verluidt vier van de zes problemen van de Internationale Wiskunde Olympiade (IMO) van dit jaar hebben opgelost en een zilveren medaille-waardige score hebben behaald. De technologiegigant beweert dat dit de eerste keer is dat AI dit prestatieniveau bereikt in de prestigieuze wiskundecompetitie – maar zoals gebruikelijk bij AI zijn de beweringen niet zo duidelijk als ze lijken.
Google zegt dat AlphaProof versterkend leren gebruikt om wiskundige uitspraken te bewijzen in een formele taal genaamd Lean. Het systeem is getraind door het genereren en controleren van miljoenen proefdrukken, waardoor steeds moeilijkere problemen geleidelijk worden opgelost. Ondertussen wordt AlphaGeometry 2 beschreven als een verbeterde versie van Google’s vorige geometrie-oplossende AI Mod I, nu aangedreven door een op Gemini gebaseerd taalmodel dat is getraind op aanzienlijk meer gegevens.
Volgens Google hebben vooraanstaande wiskundigen Sir Timothy Gowers et al. Joseph Myers evalueerde de AI-modeloplossingen aan de hand van de officiële IMO-regels. Het bedrijf meldt dat het gecombineerde systeem 28 van de mogelijke 42 punten heeft verdiend, net onder de gouden medailledrempel van 29 punten. Dit omvatte een perfecte score voor het moeilijkste probleem van de concurrentie, dat volgens Google dit jaar slechts door vijf menselijke deelnemers is opgelost.
Een wiskundewedstrijd als geen ander
De IMO, die sinds 1959 jaarlijks wordt gehouden, daagt elite wiskundigen uit voor uiterst moeilijke problemen op het gebied van algebra, combinatoriek, meetkunde en getaltheorie. Prestaties bij IMO-problemen zijn een erkende maatstaf geworden voor het evalueren van het wiskundig redeneervermogen van een AI-systeem.
Google stelt dat AlphaProof twee algebraproblemen en één getaltheorieprobleem heeft opgelost, terwijl AlphaGeometry 2 een meetkundeprobleem heeft opgelost. Het AI-model slaagde er naar verluidt niet in om twee combinatorische problemen op te lossen. Het bedrijf beweert dat zijn systemen één probleem binnen enkele minuten hebben opgelost, terwijl andere er wel drie dagen over deden.
Google zegt dat het eerst IMO-problemen heeft vertaald naar een formele wiskundige taal die door een AI-model moet worden verwerkt. Deze stap verschilt van de officiële competitie, waarbij menselijke deelnemers tijdens twee sessies van 4,5 uur rechtstreeks met probleemstellingen werken.
Google meldt dat AlphaGeometry 2 vóór de competitie van dit jaar 83 procent van de historische IMO-geometrieproblemen van de afgelopen 25 jaar kon oplossen, vergeleken met het succespercentage van zijn voorganger van 53 procent. Het bedrijf beweert dat het nieuwe systeem het geometrieprobleem van dit jaar in 19 seconden heeft opgelost nadat het een geformaliseerde versie had ontvangen.
Beperkingen
Ondanks de beweringen van Google bood Sir Timothy Gowers een genuanceerder perspectief op de DeepMind-modellen van Google in een draad op X. Hoewel hij erkende dat de prestatie “verder gaat dan wat automatische stellingbewijzers eerder hebben kunnen doen”, benadrukte Gowers verschillende belangrijke kwalificaties.
“De belangrijkste kwalificatie is dat het programma veel langer duurde dan de menselijke concurrenten – meer dan 60 uur voor sommige problemen – en natuurlijk een veel hogere verwerkingssnelheid dan het arme oude menselijke brein”, schreef Gowers. “Als menselijke concurrenten zoveel tijd per probleem hadden gekregen, hadden ze ongetwijfeld hoger gescoord.”
Gowers merkte ook op dat mensen problemen handmatig vertaalden naar de formele taal van Lean voordat het AI-model live ging. Hij benadrukte dat hoewel AI de fundamentele wiskundige redeneringen uitvoerde, deze stap van “autoformalisering” door mensen werd uitgevoerd.
Wat de bredere implicaties voor wiskundig onderzoek betreft, uitte Gowers zijn onzekerheid. “Zijn we dicht bij het punt waarop wiskundigen overbodig zijn? Dat is moeilijk te zeggen. Ik denk dat we nog steeds een paar doorbraken missen”, schreef hij. Hij suggereerde dat de lange verwerkingstijd van het systeem aangaf dat het “de wiskunde niet had uitgewerkt”, maar gaf toe dat “er duidelijk iets interessants aan de hand is als het werkt”.
Zelfs met deze beperkingen speculeerde Gowers dat dergelijke AI-systemen waardevolle onderzoeksinstrumenten zouden kunnen worden. ‘Dus we zijn misschien dichtbij een programma waarmee wiskundigen antwoorden kunnen krijgen op een breed scala aan vragen, zolang die vragen niet te moeilijk zijn – iets dat binnen een paar uur kan worden gedaan. Het zou enorm nuttig zijn als een onderzoeksinstrument, zelfs als hij zelf niet in staat was de openstaande problemen op te lossen.”