Google DeepMind har utvecklat AlphaProof, ett AI-system som matchade silvermedaljprestationen vid den internationella matematikolympiaden 2024 och fick 28 av 42 poäng. Systemet saknade bara en poäng till guld i världens mest prestigefyllda matematiktävling för undergraduates. Detta genombrott visar framsteg i AI:s förmåga att hantera komplexa matematiska bevis.
Datorer har länge excellerat i beräkningar men kämpat med det logiska resonemang som krävs för avancerad matematik. Google DeepMinds nya AI, AlphaProof, adresserar detta genom att uppnå silvermedaljprestation vid den internationella matematikolympiaden 2024 (IMO), den främsta gymnasienivåmatematiktävlingen. IMO bestod av sex problem värda sju poäng vardera, totalt 42 poäng. Guldmedaljer krävde 29 poäng eller mer, uppnådda av 58 av 609 deltagare, medan silver gick till de med 22–28 poäng, med 123 mottagare. AlphaProof fick 28 poäng, löste fyra problem självständigt för 21 poäng och använde den specialiserade AlphaGeometry 2 för geometriproblemet för att nå silvernivå.
AlphaProofs utveckling började med att övervinna begränsad träningsdata för formella matematiska bevis. Teamet använde Lean-programvaran, ett verktyg för precisa matematiska definitioner och verifieringar. För att utöka datamängden tränade de en stor språkmodell Gemini för att översätta naturliga språkmatematiska påståenden till Lean, och genererade cirka 80 miljoner formaliserade påståenden. Som Thomas Hubert, DeepMind-forskare och huvudförfattare, förklarade: «Den stora svårigheten med att arbeta med formella språk är att det finns väldigt lite data.» Trots brister: «Det finns många sätt att dra nytta av approximativa översättningar,» tillade han.
Systemets arkitektur hämtar från DeepMinds AlphaZero och kombinerar ett neuralt nätverk tränat genom trial and error med en trädssökningsalgoritm för att utforska bevisvägar. Det belönar korrekta bevis och straffar ineffektiva steg, vilket främjar eleganta lösningar. En ny tillägg, Test-Time Reinforcement Learning (TTRL), låter AlphaProof generera variationer av svåra problem för träning i realtid, vilket efterliknar mänsklig problemlösning. «Vi försökte lära oss det här spelet genom trial and error,» sa Hubert.
AlphaProof krävde dock mänsklig hjälp för att formalisera problem i Lean och tog flera dagar per utmanande problem, och förbrukade hundratals TPU-dagar – långt bortom mänskliga tidsgränser på 4,5 timmar per session. Endast sex människor löste det svåraste problemet; AlphaProof var den sjunde. DeepMind erkänner de höga beräkningskostnaderna men siktar på att optimera för bredare användning. «Vi vill inte stanna vid matematiktävlingar. Vi vill bygga ett AI-system som verkligen kan bidra till forskningsnivåmatematik,» uppgav Hubert. Teamet planerar ett betrodd testare-program för att dela ett AlphaProof-verktyg med matematiker.
Arbetet beskrivs i detalj i en Nature-artikel från 2025 (DOI: 10.1038/s41586-025-09833-y).