AI op de Internationale Wiskunde Olympiade: Hoe AlphaProof en AlphaGeometry 2 het zilveren medaille niveau bereikten

Wiskundige redenering is een essentieel onderdeel van de menselijke cognitieve vaardigheden, waardoor vooruitgang in wetenschappelijke ontdekkingen en technologische ontwikkelingen mogelijk wordt gemaakt. Terwijl we streven naar het ontwikkelen van kunstmatige algemene intelligentie die gelijkwaardig is aan de menselijke cognitie, is het essentieel om AI te voorzien van geavanceerde wiskundige redeneringsvaardigheden. Hoewel huidige AI-systemen basiswiskunde kunnen hanteren, worstelen ze met de complexe redenering die nodig is voor geavanceerde wiskundige disciplines zoals algebra en meetkunde. Echter, dit kan veranderen, aangezien Google DeepMind significante vooruitgang heeft geboekt in het verbeteren van de wiskundige redeneringsvaardigheden van een AI-systeem. Deze doorbraak is gemaakt op de Internationale Wiskunde Olympiade (IMO) 2024. Opgericht in 1959, is de IMO de oudste en meest prestigieuze wiskundewedstrijd, waarbij scholieren wereldwijd worden uitgedaagd om problemen op te lossen in algebra, combinatoriek, meetkunde en getaltheorie. Elk jaar strijden teams van jonge wiskundigen om zes zeer moeilijke problemen op te lossen. Dit jaar introduceerde Google DeepMind twee AI-systemen: AlphaProof, dat zich richt op formele wiskundige redenering, en AlphaGeometry 2, dat zich specialiseert in het oplossen van meetkundige problemen. Deze AI-systemen wisten vier van de zes problemen op te lossen, waarmee ze presteerden op het niveau van een zilveren medaille. In dit artikel zullen we onderzoeken hoe deze systemen werken om wiskundige problemen op te lossen.

AlphaProof: Het combineren van AI en formele taal voor wiskundig bewijzen

AlphaProof is een AI-systeem dat is ontworpen om wiskundige uitspraken te bewijzen met behulp van de formele taal Lean. Het integreert Gemini, een vooraf getraind taalmodel, met AlphaZero, een versterkingsleeralgoritme dat bekend staat om het behalen van meesterschap in schaken, shogi en Go.

Het Gemini-model vertaalt natuurlijke taalprobleemverklaringen in formele verklaringen, waardoor een bibliotheek van problemen met verschillende moeilijkheidsniveaus ontstaat. Dit dient twee doelen: het omzetten van onnauwkeurige natuurlijke taal in nauwkeurige formele taal voor het verifiëren van wiskundige bewijzen en het gebruik van de voorspellende capaciteiten van Gemini om een lijst van mogelijke oplossingen met formele taalprecisie te genereren.

Wanneer AlphaProof een probleem tegenkomt, genereert het potentiële oplossingen en zoekt het naar bewijsstappen in Lean om deze te verifiëren of te weerleggen. Dit is in wezen een neuro-symbolische aanpak, waarbij het neurale netwerk, Gemini, natuurlijke taalinstructies vertaalt in symbolische formele taal om de uitspraak te bewijzen of te weerleggen. Vergelijkbaar met AlphaZero’s self-play-mechanisme, waarbij het systeem leert door tegen zichzelf te spelen, traint AlphaProof zichzelf door te proberen wiskundige uitspraken te bewijzen. Elke bewijspoging verfijnt AlphaProof’s taalmodel, waarbij succesvolle bewijzen het model versterken om moeilijkere problemen aan te pakken.

Voor de Internationale Wiskunde Olympiade (IMO) werd AlphaProof getraind door het bewijzen of weerleggen van miljoenen problemen die verschillende moeilijkheidsniveaus en wiskundige onderwerpen bestreken. Deze training werd voortgezet tijdens de wedstrijd, waarbij AlphaProof zijn oplossingen verfijnde totdat het complete antwoorden op de problemen vond.

AlphaGeometry 2: Het integreren van LLM’s en symbolische AI voor het oplossen van meetkundige problemen

AlphaGeometry 2 is de nieuwste iteratie van de AlphaGeometry-serie, die is ontworpen om meetkundige problemen aan te pakken met verhoogde precisie en efficiëntie. Gebouwd op de basis van zijn voorganger, maakt AlphaGeometry 2 gebruik van een neuro-symbolische aanpak die neurale grote taalmodellen (LLM’s) combineert met symbolische AI. Deze integratie combineert regelgebaseerde logica met de voorspellende capaciteit van neurale netwerken om hulpconstructies te identificeren, die essentieel zijn voor het oplossen van meetkundige problemen. Het LLM in AlphaGeometry voorspelt nieuwe meetkundige constructies, terwijl de symbolische AI formele logica toepast om bewijzen te genereren.

Wanneer AlphaGeometry een meetkundig probleem tegenkomt, evalueert het LLM talloze mogelijkheden, waarbij het voorspelt constructies die cruciaal zijn voor het oplossen van problemen. Deze voorspellingen dienen als waardevolle aanwijzingen, die de symbolische motor leiden naar accurate deducties en het dichter brengen bij een oplossing. Deze innovatieve aanpak stelt AlphaGeometry in staat om complexe meetkundige uitdagingen aan te pakken die verder gaan dan conventionele scenario’s.

Een van de belangrijkste verbeteringen in AlphaGeometry 2 is de integratie van het Gemini LLM. Dit model is getraind vanaf scratch op aanzienlijk meer synthetische gegevens dan zijn voorganger. Deze uitgebreide training stelt het in staat om moeilijkere meetkundige problemen aan te pakken, waaronder problemen die objectbewegingen en vergelijkingen van hoeken, verhoudingen of afstanden betreffen. Bovendien beschikt AlphaGeometry 2 over een symbolische motor die twee ordes van grootte sneller werkt, waardoor het in staat is om alternatieve oplossingen met ongekende snelheid te onderzoeken. Deze vooruitgang maakt AlphaGeometry 2 een krachtig instrument voor het oplossen van complexe meetkundige problemen, waarmee het een nieuwe standaard in het veld zet.

AlphaProof en AlphaGeometry 2 op de IMO

Dit jaar op de Internationale Wiskunde Olympiade (IMO) werden de deelnemers getest met zes diverse problemen: twee in algebra, één in getaltheorie, één in meetkunde en twee in combinatoriek. Google-onderzoekers vertaalden deze problemen in formele wiskundige taal voor AlphaProof en AlphaGeometry 2. AlphaProof loste twee algebra-problemen en één getaltheorie-probleem op, waaronder het moeilijkste probleem van de wedstrijd, dat slechts door vijf menselijke deelnemers dit jaar werd opgelost. Ondertussen loste AlphaGeometry 2 het meetkundige probleem succesvol op, hoewel het de twee combinatorische uitdagingen niet aanging

Elk probleem op de IMO is waard zeven punten, wat opgeteld wordt tot een maximum van 42. AlphaProof en AlphaGeometry 2 behaalden 28 punten, waarmee ze perfecte scores behaalden op de problemen die ze oplosten. Dit plaatste hen aan de bovenkant van de zilveren medaille categorie. De drempel voor een gouden medaille lag dit jaar op 29 punten, bereikt door 58 van de 609 deelnemers.

Volgende stap: Natuurlijke taal voor wiskundige uitdagingen

AlphaProof en AlphaGeometry 2 hebben indrukwekkende vooruitgang getoond in de wiskundige probleemoplossende capaciteiten van AI. Echter, deze systemen zijn nog steeds afhankelijk van menselijke experts om wiskundige problemen in formele taal te vertalen voor verwerking. Bovendien is het onduidelijk hoe deze gespecialiseerde wiskundige vaardigheden kunnen worden geïntegreerd in andere AI-systemen, zoals voor het onderzoeken van hypothesen, het testen van innovatieve oplossingen voor langdurige problemen en het efficiënt beheren van tijdrovende aspecten van bewijzen.

Om deze beperkingen te overwinnen, ontwikkelen Google-onderzoekers een natuurlijke taalredeneringssysteem op basis van Gemini en hun laatste onderzoek. Dit nieuwe systeem heeft tot doel de probleemoplossende capaciteiten te verbeteren zonder dat formele taalvertaling nodig is en is ontworpen om naadloos te integreren met andere AI-systemen.

De bottom line

De prestaties van AlphaProof en AlphaGeometry 2 op de Internationale Wiskunde Olympiade zijn een opmerkelijke stap voorwaarts in de capaciteit van AI om complexe wiskundige redenering aan te pakken. Beide systemen toonden prestaties op zilveren medaille-niveau door vier van de zes moeilijke problemen op te lossen, waarmee ze aanzienlijke vooruitgang toonden in formele bewijzen en meetkundige probleemoplossing. Ondanks hun prestaties zijn deze AI-systemen nog steeds afhankelijk van menselijke input voor het vertalen van problemen in formele taal en stellen ze zichzelf voor uitdagingen bij de integratie met andere AI-systemen. Toekomstig onderzoek is gericht op het verder verbeteren van deze systemen, mogelijk door het integreren van natuurlijke taalredenering om hun capaciteiten uit te breiden over een bredere reeks wiskundige uitdagingen.