AI på den internationella matematikolympiaden: Hur AlphaProof och AlphaGeometry 2 uppnådde silvermedaljstandard

Matematiskt resonemang är en livsviktig aspekt av mänskliga kognitiva förmågor, som driver framåt vetenskapliga upptäckter och teknologiska utvecklingar. När vi strävar efter att utveckla artificiell allmän intelligens som matchar mänsklig kognition, är det avgörande att utrusta AI med avancerade matematiska resonemangsförmågor. Medan nuvarande AI-system kan hantera grundläggande matematikproblem, kämpar de med den komplexa resonemang som behövs för avancerade matematiska discipliner som algebra och geometri. Men detta kan vara på väg att förändras, eftersom Google DeepMind har gjort betydande framsteg i att förbättra ett AI-systems matematiska resonemangsförmågor. Genombrottet skedde vid den internationella matematikolympiaden (IMO) 2024. Grundad 1959 är IMO den äldsta och mest prestigefyllda matematiktävlingen, som utmanar gymnasieelever världen över med problem inom algebra, kombinatorik, geometri och talteori. Varje år tävlar lag av unga matematiker för att lösa sex mycket utmanande problem. I år introducerade Google DeepMind två AI-system: AlphaProof, som fokuserar på formellt matematiskt resonemang, och AlphaGeometry 2, som specialiserar sig på att lösa geometriska problem. Dessa AI-system lyckades lösa fyra av sex problem, och presterade på samma nivå som en silvermedaljör. I den här artikeln kommer vi att utforska hur dessa system fungerar för att lösa matematiska problem.

AlphaProof: Kombinerar AI och formell språk för matematiskt bevis

AlphaProof är ett AI-system som är utformat för att bevisa matematiska påståenden med hjälp av det formella språket Lean. Det integrerar Gemini, en förtränad språkmodell, med AlphaZero, en förstärkt inlärningsalgoritm som är känd för att ha bemästrat schack, shogi och Go.

Gemini-modellen översätter naturligt språk till formellt språk, och skapar en bibliotek av problem med varierande svårighetsgrad. Detta tjänar två syften: att omvandla oexakta naturligt språk till exakt formellt språk för att verifiera matematiska bevis, och att använda de prediktiva förmågorna hos Gemini för att generera en lista av möjliga lösningar med formellt språkprecision.

När AlphaProof möter ett problem, genererar det potentiella lösningar och söker efter bevissteg i Lean för att verifiera eller motbevisa dem. Detta är i princip en neuro-symbolisk approach, där det neuronnätverk som Gemini använder, översätter naturligt språk till det symboliska formella språket Lean för att bevisa eller motbevisa påståendet. Liksom AlphaZeros självspel-mekanism, där systemet lär sig genom att spela spel mot sig själv, tränar AlphaProof sig själv genom att försöka bevisa matematiska påståenden. Varje bevisförsök förfinar AlphaProofs språkmodell, med framgångsrika bevis som förstärker modellens förmåga att hantera mer utmanande problem.

För den internationella matematikolympiaden (IMO) tränades AlphaProof genom att bevisa eller motbevisa miljontals problem som täckte olika svårighetsgrader och matematiska ämnen. Denna träning fortsatte under tävlingen, där AlphaProof förfinade sina lösningar tills den hittade kompletta svar på problemen.

AlphaGeometry 2: Integrerar LLM och symbolisk AI för att lösa geometriska problem

AlphaGeometry 2 är den senaste versionen av AlphaGeometry-serien, som är utformad för att hantera geometriska problem med förbättrad precision och effektivitet. Byggande på grunderna av sin föregångare, använder AlphaGeometry 2 en neuro-symbolisk approach som kombinerar stora språkmodeller (LLM) med symbolisk AI. Denna integration kombinerar regelbaserad logik med den prediktiva förmågan hos neuronnätverk för att identifiera hjälp-punkter, som är avgörande för att lösa geometriska problem. LLM i AlphaGeometry förutsäger nya geometriska konstruktioner, medan den symboliska AI:n tillämpar formell logik för att generera bevis.

När AlphaGeometry möter ett geometriskt problem, utvärderar LLM ett stort antal möjligheter, och förutsäger konstruktioner som är avgörande för problem-lösning. Dessa förutsägelser fungerar som värdefulla ledtrådar, som vägleder den symboliska motorn mot exakta deduktioner och förbättrar möjligheten att hitta en lösning. Denna innovativa approach möjliggör för AlphaGeometry att hantera komplexa geometriska utmaningar som sträcker sig bortom konventionella scenarier.

En viktig förbättring i AlphaGeometry 2 är integrationen av Gemini LLM. Denna modell tränas från scratch på betydligt mer syntetisk data än sin föregångare. Denna omfattande träning utrustar den med förmågan att hantera mer svåra geometriska problem, inklusive de som involverar objektrörelser och ekvationer för vinklar, förhållanden eller avstånd. Dessutom har AlphaGeometry 2 en symbolisk motor som fungerar två storleksordningar snabbare, vilket möjliggör för den att utforska alternativa lösningar med en tidigare aldrig skådad hastighet. Dessa framsteg gör AlphaGeometry 2 till ett kraftfullt verktyg för att lösa invecklade geometriska problem, och sätter en ny standard inom området.

AlphaProof och AlphaGeometry 2 på IMO

I år på den internationella matematikolympiaden (IMO) testades deltagarna med sex olika problem: två i algebra, ett i talteori, ett i geometri och två i kombinatorik. Google-forskare översatte dessa problem till formellt matematiskt språk för AlphaProof och AlphaGeometry 2. AlphaProof hanterade två algebra-problem och ett talteori-problem, inklusive det svåraste problemet i tävlingen, som endast fem mänskliga deltagare löste i år. Samtidigt löste AlphaGeometry 2 det geometriska problemet, men lyckades inte med de två kombinatoriska utmaningarna.

Varje problem på IMO är värt sju poäng, och maximala poängen är 42. AlphaProof och AlphaGeometry 2 fick 28 poäng, och uppnådde perfekta poäng på de problem de löste. Detta placerade dem i den övre delen av silvermedalj-kategorin. Gränsen för guldmedalj var 29 poäng, som uppnåddes av 58 av de 609 deltagarna.

Nästa steg: Naturligt språk för matematiska utmaningar

AlphaProof och AlphaGeometry 2 har visat imponerande framsteg i AI:s matematiska problem-lösningsförmåga. Men dessa system är fortfarande beroende av mänskliga experter för att översätta matematiska problem till formellt språk för bearbetning. Dessutom är det oklart hur dessa specialiserade matematiska färdigheter kan integreras i andra AI-system, såsom för att utforska hypoteser, testa innovativa lösningar på långvariga problem och effektivt hantera tidskrävande aspekter av bevis.

För att övervinna dessa begränsningar utvecklar Google-forskare ett naturligt språk-resonemangssystem baserat på Gemini och deras senaste forskning. Detta nya system syftar till att förbättra problem-lösningsförmågan utan att kräva formellt språk-översättning, och är utformat för att integreras smidigt med andra AI-system.

Sammanfattning

Prestationen hos AlphaProof och AlphaGeometry 2 på den internationella matematikolympiaden är ett betydande steg framåt i AI:s förmåga att hantera komplex matematisk resonemang. Båda systemen visade silvermedalj-nivå-prestation genom att lösa fyra av sex utmanande problem, och visade betydande framsteg i formellt bevis och geometrisk problem-lösning. Trots deras prestationer är dessa AI-system fortfarande beroende av mänsklig inmatning för att översätta problem till formellt språk, och står inför utmaningar i integrationen med andra AI-system. Framtida forskning syftar till att förbättra dessa system ytterligare, och potentiellt integrera naturligt språk-resonemang för att utöka deras förmågor över en bredare range av matematiska utmaningar.