AI vid International Mathematical Olympiad: How AlphaProof and AlphaGeometry 2 Achieved Silver-Medal Standard

Matematiskt resonemang är en viktig aspekt av människans kognitiva förmågor, som driver framsteg i vetenskapliga upptäckter och teknisk utveckling. När vi strävar efter att utveckla artificiell allmän intelligens som matchar mänsklig kognition är det viktigt att utrusta AI med avancerade matematiska resonemangsmöjligheter. Medan nuvarande AI-system kan hantera grundläggande matematiska problem, kämpar de med de komplexa resonemang som behövs för avancerade matematiska discipliner som algebra och geometri. Detta kan dock komma att förändras, som Google DeepMind har gjort betydande framsteg i att utveckla ett AI-systems matematiska resonemangsförmåga. Detta genombrott görs vid Internationell matematikolympiad (IMO) 2024. IMO grundades 1959 och är 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 om att lösa sex mycket utmanande problem. I år introducerade Google DeepMind två AI-system: AlphaProof, som fokuserar på formella matematiska resonemang, och AlphaGeometry 2, som specialiserat 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: Kombinera AI och formellt språk för att bevisa matematiska teorem

AlphaProof är ett AI-system designat för att bevisa matematiska påståenden med det formella språket Lean. Det integrerar tvillingarna, en förutbildad språkmodell, med Alpha Zero, en förstärkningsinlärningsalgoritm känd för att behärska schack, shogi och Go.

Gemini-modellen översätter naturliga problemformuleringar till formella, vilket skapar ett bibliotek med problem med olika svårighetsnivåer. Detta tjänar två syften: att konvertera oprecisa naturligt språk till exakt formellt språk för att verifiera matematiska bevis och använda prediktiva förmågor hos Tvillingarna för att generera en lista över möjliga lösningar med formell språkprecision.

När AlphaProof stöter på ett problem genererar det potentiella lösningar och söker efter bevissteg i Lean för att verifiera eller motbevisa dem. Detta är i huvudsak ett neurosymboliskt tillvägagångssätt, där det neurala nätverket, Gemini, översätter naturliga språkinstruktioner till det symboliska formspråket Lean för att bevisa eller motbevisa påståendet. I likhet med AlphaZeros självspelsmekanism, där systemet lär sig genom att spela spel mot sig självt, tränar AlphaProof sig själv genom att försöka bevisa matematiska påståenden. Varje provfö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 International Mathematical Olympiad (IMO) tränades AlphaProof genom att bevisa eller motbevisa miljontals problem som täcker olika svårighetsnivåer och matematiska ämnen. Denna utbildning fortsatte under tävlingen, där AlphaProof förfinade sina lösningar tills den hittade fullständiga svar på problemen.

AlphaGeometry 2: Integrering av LLM och symbolisk AI för att lösa geometriproblem

AlphaGeometry 2 är den senaste iterationen av Alfageometri serie, designad för att hantera geometriska problem med ökad precision och effektivitet. AlphaGeometry 2 bygger på grunden för sin föregångare och använder ett neurosymboliskt tillvägagångssätt som kombinerar neurala stora språkmodeller (LLM) med symbolisk AI. Denna integrering kombinerar regelbaserad logik med neurala nätverks prediktiva förmåga att identifiera hjälppunkter, väsentliga för att lösa geometriproblem. LLM i AlphaGeometry förutsäger nya geometriska konstruktioner, medan den symboliska AI använder formell logik för att generera bevis.

När AlphaGeometry ställs inför ett geometriskt problem utvärderar kandidatexamen i juridik ett flertal möjligheter och förutsäger konstruktioner som är avgörande för problemlösning. Dessa förutsägelser fungerar som värdefulla ledtrådar och vägleder den symboliska motorn mot korrekta deduktioner och avancerar närmare en lösning. Denna innovativa metod gör det möjligt för AlphaGeometry att ta itu med 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 grunden på betydligt mer syntetisk data än sin föregångare. Denna omfattande utbildning utrustar den för att hantera svårare geometriproblem, inklusive de som involverar objektrörelser och ekvationer av vinklar, förhållanden eller avstånd. Dessutom har AlphaGeometry 2 en symbolisk motor som arbetar två storleksordningar snabbare, vilket gör att den kan utforska alternativa lösningar med oöverträffad hastighet. Dessa framsteg gör AlphaGeometry 2 till ett kraftfullt verktyg för att lösa intrikata geometriska problem, vilket sätter en ny standard på området.

AlphaProof och AlphaGeometry 2 på IMO

I år vid International Mathematical Olympiad (IMO) testades deltagarna med sex olika problem: två i algebra, ett i talteori, ett i geometri och två i kombinatorik. Google-forskare översatt dessa problem till formellt matematiskt språk för AlphaProof och AlphaGeometry 2. AlphaProof tog itu med två algebraproblem och ett nummerteoretiskt problem, inklusive det svåraste problemet i tävlingen, löst av endast fem mänskliga tävlande i år. Under tiden löste AlphaGeometry 2 framgångsrikt geometriproblemet, även om det inte knäckte de två kombinatoriska utmaningarna

Varje problem vid IMO är värt sju poäng, vilket ger maximalt 42 poäng. AlphaProof och AlphaGeometry 2 fick 28 poäng och fick perfekta poäng på de problem de löste. Detta placerade dem i den övre änden av silvermedaljkategorin. Tröskeln för guldmedalj i år var 29 poäng, nådd av 58 av de 609 tävlande.

Nästa språng: Naturligt språk för matematikutmaningar

AlphaProof och AlphaGeometry 2 har visat imponerande framsteg inom AI:s matematiska problemlösningsförmåga. Dessa system är dock 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 införlivas i andra AI-system, till exempel 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 Googles forskare ett naturligt språkresonemangssystem baserat på Gemini och deras senaste forskning. Detta nya system syftar till att förbättra problemlösningsförmåga utan att kräva formell språköversättning och är utformat för att smidigt integreras med andra AI-system.

The Bottom Line

Prestandan för AlphaProof och AlphaGeometry 2 vid den internationella matematikolympiaden är ett anmärkningsvärt steg framåt i AI:s förmåga att hantera komplext matematiskt resonemang. Båda systemen visade silvermedaljprestanda genom att lösa fyra av sex utmanande problem, vilket visar betydande framsteg inom formellt bevis och geometrisk problemlösning. Trots sina framgångar är dessa AI-system fortfarande beroende av mänsklig input 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, potentiellt genom att integrera naturligt språkresonemang för att utöka deras kapacitet över ett bredare spektrum av matematiska utmaningar.