AI vid den internationella matematiska olympiaden: 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 resonemangs fö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 väsentliga framsteg i att främja en AI-systems matematiska resonemangs förmågor. Genombrottet skedde vid den internationella matematiska olympiaden (IMO) 2024. Grundad 1959, är IMO den äldsta och mest prestigefyllda matematik tävlingen, som utmanar gymnasieelever världen över med problem i 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: Kombination av AI och formell språk för matematisk 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 naturliga språkproblem till formella, och skapar en samling av problem med varierande svårighetsgrader. Detta tjänar två syften: att omvandla oexakta naturliga språk till exakta formella språk för att verifiera matematiska bevis, och att använda Gemini’s prediktiva förmågor för att generera en lista av möjliga lösningar med formell 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, Gemini, översätter naturliga språkinstruktioner till det symboliska formella språket Lean för att bevisa eller motbevisa påståendet. Liknande 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 försök att bevisa 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 matematiska olympiaden (IMO) tränades AlphaProof genom att bevisa eller motbevisa miljontals problem som täcker olika svårighetsgrader och matematiska ämnen. Denna träning fortsatte under tävlingen, där AlphaProof förfinade sina lösningar tills det hittade kompletta svar på problemen.

AlphaGeometry 2: Integrering av 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å grunden av sin föregångare, använder AlphaGeometry 2 en neuro-symbolisk approach som kombinerar neuronnätverk med symbolisk AI. Denna integration kombinerar regelbaserad logik med den prediktiva förmågan hos neuronnätverk för att identifiera auxiliära 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 många möjligheter, och förutsäger konstruktioner som är avgörande för problem-lösning. Dessa förutsägelser tjänar som värdefulla ledtrådar, som guidar den symboliska motorn mot exakta deduktioner och främjar lösningen. 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 är tränad från scratch på betydligt mer syntetisk data än sin föregångare. Denna omfattande träning utrustar den för 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 aldrig tidigare skådad hastighet. Dessa framsteg gör AlphaGeometry 2 till ett kraftfullt verktyg för att lösa intrikata geometriska problem, och sätter en ny standard inom området.

AlphaProof och AlphaGeometry 2 vid IMO

I år vid den internationella matematiska olympiaden (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å algebraproblem och ett talteoriproblem, 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 kunde inte knäcka de två kombinatoriska utmaningarna.

Varje problem vid IMO är värt sju poäng, vilket ger en maximal poäng på 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 i år 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 av AlphaProof och AlphaGeometry 2 vid den internationella matematiska olympiaden är ett anmärkningsvärt steg framåt i AI:s förmåga att hantera komplex matematisk resonemang. Båda systemen visade silvermedalj-prestanda 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 med integration 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 serie matematiska utmaningar.