DeepMind AI wint een zilveren medaille op de Internationale Wiskundeolympiade

De AI van Google DeepMind won dit jaar een zilveren medaille op de Internationale Wiskunde Olympiade (IMO), wat de eerste keer is dat kunstmatige intelligentie het podium bereikt.

IMO wordt beschouwd als de meest prestigieuze wereldcompetitie voor jonge wiskundigen. Het correct beantwoorden van testvragen vereist wiskundige vaardigheden die systemen voor kunstmatige intelligentie doorgaans missen.

In januari demonstreerde Google DeepMind AlphaGeometry, een kunstmatig intelligentiesysteem dat zowel een aantal IMO-geometrievragen als mensen kon beantwoorden. Deze kwam echter niet uit een live competitie en kon geen antwoord geven op vragen uit andere wiskundige disciplines, zoals getaltheorie, algebra en combinatoriek, wat nodig is om een ​​IMO-medaille te winnen.

Google DeepMind heeft nu een nieuwe AI uitgebracht, AlphaProof genaamd, die een breder scala aan wiskundige problemen kan oplossen, en een verbeterde versie van AlphaGeometry, die meer geometrievragen kan oplossen.

Toen het team beide systemen samen testte op de IMO-vragen van dit jaar, beantwoordden ze vier van de zes vragen correct, wat hen een score opleverde van 28 van de mogelijke 42 punten. Dit was genoeg om de zilveren medaille te winnen en slechts één punt minder te halen dan de gouden medailledrempel van dit jaar.

Tijdens de wedstrijd in Bath, Groot-Brittannië, wonnen vorige week 58 deelnemers gouden medailles en 123 zilveren medailles.

“We zijn ons er allemaal zeer van bewust dat AI uiteindelijk beter zal zijn dan mensen in het oplossen van de meeste wiskundige problemen, maar de snelheid waarmee AI verbetert is adembenemend”, zegt Gregor Dolinar, voorzitter van de IMO. “Om een ​​paar dagen geleden op de IMO 2024 een gouden medaille met slechts één punt mis te lopen, is echt indrukwekkend.”

Op een persconferentie zei Timothy Gowers van de Universiteit van Cambridge, die hielp bij het markeren van de antwoorden van AlphaProof, dat de prestaties van de AI verrassend waren en dat het ‘magische sleutels’ leek te hebben gevonden om problemen op een vergelijkbare manier als mensen te beantwoorden. “Ik dacht dat deze magische sleutels waarschijnlijk iets verder zouden gaan dan wat het kon doen, dus het was nogal een verrassing in de een of twee gevallen waarin het programma deze sleutels daadwerkelijk vond,” zei Gowers.

AlphaProof werkt op dezelfde manier als de eerdere Google DeepMind AI, die de beste mensen kan verslaan bij schaken en Go. Al deze AI’s zijn gebaseerd op een ‘trial-and-error’-aanpak, genaamd versterkend leren, waarbij het systeem na vele pogingen zijn eigen manier vindt om een ​​probleem op te lossen. Deze methode vereist echter een groot aantal problemen die zijn geschreven in een taal die AI kan begrijpen en verifiëren, terwijl de meeste IMO-achtige problemen in het Engels zijn geschreven.

Om dit te omzeilen, gebruikten Thomas Hubert van DeepMind en zijn collega’s Google’s Gemini AI, een taalmodel zoals het model dat ChatGPT aanstuurt, om deze problemen te vertalen naar een programmeertaal genaamd Lean, zodat de AI kan leren hoe ze deze kunnen oplossen.

“In het begin zal hij misschien wel de eenvoudigste problemen kunnen oplossen en van het oplossen van die eenvoudigere problemen leren om steeds moeilijkere problemen aan te pakken”, zei Hubert op een persconferentie. Het produceert zijn antwoorden ook in Lean, zodat deze direct als juist kunnen worden geverifieerd.

Hoewel de prestaties van AlphaProof indrukwekkend zijn, verloopt het langzaam en duurt het tot drie dagen om enkele oplossingen te vinden in plaats van de 4,5 uur voor drie vragen die concurrenten mogen. Hij slaagde er ook niet in om beide vragen over combinatoriek, de studie van het tellen en rangschikken van getallen, te beantwoorden. “We werken er nog steeds aan om te begrijpen waarom dit zo is, wat ons hopelijk zal leiden om het systeem te verbeteren”, zegt Alex Davies van Google DeepMind.

Het is ook niet duidelijk hoe AlphaProof tot zijn antwoorden komt en of het dezelfde soort wiskundige intuïtie gebruikt als mensen, zei Gowers, maar het vermogen om bewijzen van Lean naar het Engels te vertalen maakt het gemakkelijker om te verifiëren dat ze correct zijn.

Het resultaat is indrukwekkend en een belangrijke mijlpaal, zegt Geordie Williamson van de Universiteit van Sydney, Australië. “Er zijn veel eerdere pogingen geweest om leren te leren op basis van formeel bewijsmateriaal, maar geen enkele heeft veel succes gehad.”

Hoewel een systeem als AlphaProof nuttig zou kunnen zijn voor werkende wiskundigen bij het ontwikkelen van bewijzen, kan het duidelijk niet helpen bij het identificeren van problemen die moeten worden opgelost en eraan te werken, wat een groot deel van de tijd van de onderzoekers in beslag neemt, zegt Yang-Hui He van het London Institute for wiskundige wetenschappen.

Hubert zei dat zijn team hoopt dat AlphaProof de grote taalmodellen van Google, zoals Gemini, kan helpen verbeteren door het aantal onjuiste antwoorden te verminderen.

Handelsbedrijf XTX Markets heeft een prijs van $5 miljoen aangeboden – de AI Wiskundeolympiade genoemd – voor een AI die in staat is een gouden medaille te behalen bij de IMO, maar AlphaProof komt niet in aanmerking omdat deze niet openbaar beschikbaar is. “We hopen dat de vooruitgang van DeepMind meer teams zal inspireren om mee te doen aan de AIMO-prijs, en natuurlijk zouden we een publieke inzending van DeepMind zelf verwelkomen”, zegt Alex Gerko van XTX Markets.