Van zilver naar goud: hoe DeepMinds AI de wiskundeolympiade veroverde

DeepMinds AI heeft in één jaar tijd opmerkelijke vooruitgang geboekt in wiskundige redenering. Na een zilveren medaille te hebben behaald op de Internationale Wiskundeolympiade (IMO) in 2024, behaalde hun AI-systeem een gouden medaille in 2025. Deze snelle vooruitgang benadrukt de groeiende capaciteiten van kunstmatige intelligentie om complexe, abstracte problemen aan te pakken die menselijke creativiteit en inzicht vereisen. Dit artikel zal uitleggen hoe DeepMind deze transformatie bereikte, de technische en strategische keuzes die daarachter liggen, en de bredere implicaties van deze vooruitgang.

Het belang van de IMO

De Internationale Wiskundeolympiade, opgericht in 1959, wordt wereldwijd erkend als de belangrijkste wiskundewedstrijd voor middelbare scholieren. Elk jaar moeten de beste studenten van over de hele wereld zes moeilijke problemen oplossen uit algebra, meetkunde, getaltheorie en combinatoriek. Het oplossen van deze problemen vereist meer dan alleen berekening; deelnemers moeten echte wiskundige creativiteit, strikte logische denken en de mogelijkheid om elegante bewijzen te construeren laten zien.

Voor kunstmatige intelligentie is de IMO een unieke uitdaging. Terwijl AI patronenherkenning, gegevensanalyse en zelfs complexe spellen als Go en schaken heeft geperfectioneerd, vereist olympische wiskunde creatieve, abstracte redenering en de synthese van nieuwe ideeën, vaardigheden die traditioneel worden beschouwd als kenmerken van menselijke intelligentie. Als gevolg daarvan is de IMO een natuurlijke testomgeving geworden voor het evalueren van hoe dichtbij AI komt bij het bereiken van echt menselijke redenering.

De doorbraak van zilver in 2024

In 2024 introduceerde DeepMind twee AI-systemen om IMO-niveau-problemen aan te pakken: AlphaProof en AlphaGeometry 2. Beide systemen zijn voorbeelden van “neuro-symbolische” AI, die de kracht van grote taalmodellen (LLM’s) combineert met de striktheid van symbolische logica.

AlphaProof was ontworpen om wiskundige beweringen te bewijzen met behulp van Lean, een formele wiskundige taal. Het combineerde Gemini, DeepMinds grote taalmodel, met AlphaZero, dat een versterkingsleerengine is die bekend staat om zijn succes in bordspellen. In deze setting was de rol van Gemini om natuurlijke taalproblemen te vertalen naar Lean en pogingen te doen om bewijzen te genereren door logische stappen te produceren. AlphaProof was getraind op miljoenen voorbeeldproblemen uit verschillende wiskundige disciplines en moeilijkheidsgraden. Het systeem verbeterde zichzelf door steeds complexere beweringen te proberen te bewijzen, net zoals AlphaZero leerde door tegen zichzelf te spelen.

AlphaGeometry 2 was ontworpen om meetkundige problemen op te lossen. Hierbij maakte Gemini’s taalbegrip het mogelijk voor de AI om nuttige hulpconstructies te voorspellen, terwijl een symbolische redeneerengine de logische deducties beheerde. Deze hybride aanpak stelde AlphaGeometry in staat om meetkundige problemen aan te pakken die verder gingen dan het bereik van traditionele machine-redenering.

Samen losten deze systemen vier van de zes IMO-problemen op: twee in algebra, één in getaltheorie en één in meetkunde, met een score van 28 van de 42. Deze prestatie was een belangrijke mijlpaal, omdat het de eerste keer was dat een AI het zilveren medaille-niveau had bereikt op de IMO. Echter, deze succes afhankelijk was van menselijke experts om problemen te vertalen naar formele wiskundige talen. Ze vereisten ook enorme computationele middelen, die dagen van verwerkingstijd per probleem in beslag namen.

Technische innovaties achter de gouden medaille

DeepMinds overgang van zilver naar gouden medaille prestatie werd aangedreven door verschillende significante technische verbeteringen.

1. Natuurlijke taal als medium voor bewijzen

De meest significante verandering was het verschuiven van systemen die expertvertalingen naar formele talen vereisten naar het behandelen van natuurlijke taal als medium voor bewijzen. Deze verschuiving wordt bereikt door een verbeterde versie van Gemini uitgerust met Deep Think-mogelijkheden. In plaats van problemen om te zetten in Lean, verwerkt het model de tekst rechtstreeks, genereert informele schetsen, formaliseert intern kritische stappen en produceert een verfijnd Engels bewijs. Versterkingsleer van menselijke feedback (RLHF) werd gebruikt om oplossingen te belonen die logisch consistent, bondig en gepresenteerd waren.

Gemini Deep Think verschilt van de openbare versie van Gemini op twee belangrijke manieren. Ten eerste wijdt het langere contextvensters en meer berekenings tokens per query toe, waardoor het model meerdere pagina’s lange ketens van gedachten kan onderhouden. Ten tweede gebruikt het parallelle redenering, waarbij honderden speculatieve draden worden gegenereerd voor verschillende potentiële oplossingen. Een lichtgewicht supervisor rangschikt en bevordert vervolgens de meest veelbelovende paden, concepten lenend van Monte Carlo boomzoekingen maar toegepast op tekst. Deze aanpak imiteert hoe menselijke teams brainstormen, onproductieve ideeën verwijderen en convergeren naar elegante oplossingen.

2. Training en versterkingsleer

Het trainen van Gemini Deep Think omvatte het fijn afstemmen van het model om volgende stappen te voorspellen in plaats van eindantwoorden. Voor dit doel werd een corpus van 100.000 kwalitatief hoogwaardige Olympische en undergraduate contestoplossingen samengesteld. Het corpus werd voornamelijk verzameld uit openbare wiskunde-fora, arXiv-preprints en collegeprobleemsets. Menselijke mentoren beoordeelden trainingsvoorbeelden om illogische of onvolledige bewijzen te filteren. Versterkingsleer hielp het model te verfijnen, waarbij het werd gestuurd naar het produceren van bondige en precieze bewijzen. Vroege versies produceerden overbodige bewijzen, maar straffen op redundante zinnen hielpen de output te snoeien.

In tegenstelling tot conventionele fijnafstelling, die vaak worstelt met schaarse beloningen waarbij feedback binair is, of het bewijs correct is of niet. DeepMind implementeerde een stapsgewijze beloningsysteem, waarbij elke geverifieerde sublemma bijdroeg aan de algehele score. Dit beloningsmechanisme leidt Gemini zelfs wanneer een compleet bewijs zeldzaam is. Het trainingsproces duurde drie maanden en maakte gebruik van ongeveer 25 miljoen TPU-uren.

3. Massale parallelisatie

Parallelisatie speelde ook een cruciale rol in DeepMinds vooruitgang van zilver naar goud. Elk probleem genereerde meerdere redeneerbranches in parallel, met middelen die dynamisch verschoven naar meer veelbelovende wegen wanneer anderen stagneerden. Deze dynamische planning was vooral gunstig voor combinatorische problemen, die grote oplossingsruimtes hebben. De aanpak is vergelijkbaar met hoe mensen hulp-ongelijkheden testen voordat ze zich committeren aan een volledige inductie. Hoewel deze techniek computationeel duur was, was het beheersbaar met DeepMinds TPU v5-clusters.

DeepMind op de IMO 2025

Om de integriteit van de wedstrijd te behouden, bevroor DeepMind de gewichten van het model drie weken voor de IMO om te voorkomen dat officiële problemen in de trainingsset terechtkwamen.

Tijdens de wedstrijd kreeg Gemini Deep Think de zes officiële problemen in platte tekst zonder toegang tot het internet. Het systeem werkte op een cluster dat was geconfigureerd om de computationele kracht van een standaard laptop per proces te simuleren. Het hele probleemoplossingsproces werd voltooid in minder dan drie uur, ruim binnen de tijdslimiet. De gegenereerde bewijzen werden zonder wijzigingen ingediend bij de IMO-coördinatoren.

Gemini Deep Think behaalde perfecte scores op de eerste vijf problemen. Het laatste probleem, dat een moeilijke combinatorische puzzel was, stelde echter zowel de AI als 94% van de menselijke deelnemers voor een uitdaging. Ondanks dit eindigde de AI met een totale score van 35/42 en behaalde het een gouden medaille. Deze score was zeven punten hoger dan de prestatie van het voorgaande jaar. Waarnemers beschreven de bewijzen van de AI later als ‘zorgvuldig’ en ‘volledig’, waarbij werd opgemerkt dat ze de strikte rechtvaardigingen volgden die van menselijke deelnemers werden verwacht.

Implicaties voor AI en wiskunde

DeepMinds prestatie is een belangrijke mijlpaal voor zowel AI als wiskunde. Voor AI is het behalen van de IMO een stap naar kunstmatige algemene intelligentie (AGI), waarbij systemen elke intellectuele taak kunnen uitvoeren die een mens kan. Het oplossen van complexe wiskundige problemen vereist redenering en begrip, die fundamentele componenten zijn van algemene intelligentie. Deze succes aangeeft dat AI stappen zet naar meer menselijke cognitieve vaardigheden.

Voor wiskunde kunnen AI-systemen zoals Gemini Deep Think onmisbare hulpmiddelen worden voor wiskundigen. Ze kunnen helpen bij het verkennen van nieuwe gebieden, het verifiëren van vermoedens en zelfs het ontdekken van nieuwe stellingen. Door de meer saaie aspecten van bewijsconstructie te automatiseren, bevrijdt AI menselijke wiskundigen om zich te concentreren op hogere conceptuele werk. Bovendien kunnen de technieken die zijn ontwikkeld voor deze AI-systemen nieuwe methoden in wiskundig onderzoek inspireren die mogelijk niet alleen door menselijke inspanning kunnen worden bereikt.

Echter, de vooruitgang van AI in wiskunde roept ook vragen op over de rol van AI in onderwijsinstellingen en -wedstrijden. Naarmate de capaciteiten van AI blijven groeien, zullen er discussies zijn over hoe de betrokkenheid van AI de aard van wiskundeonderwijs en -wedstrijden kan veranderen.

Terugblik

Het winnen van een gouden medaille op de IMO is een belangrijke mijlpaal, maar er zijn nog veel wiskundige uitdagingen die voor de huidige AI-systemen buiten bereik liggen. Echter, de snelle vooruitgang van zilver naar goud in slechts één jaar benadrukt het versnellende tempo van AI-innovaties en -ontwikkelingen. Als deze trend zich voortzet, kunnen AI-systemen binnenkort enkele van de meest beroemde onopgeloste problemen in de wiskunde aanpakken. Terwijl de vraag of AI menselijke creativiteit zal vervangen of versterken onopgelost blijft, is de IMO van 2025 een duidelijke indicatie dat kunstmatige intelligentie significante stappen heeft gezet in logische redenering.