Suche
Mein Konto
Efter att Google DeepMind besegrade människor i allt, från Spela Gå till strategibrädspel,
den säger sig nu vara på gränsen till att slå världens bästa elever på att lösa matteproblem.
Den Londonbaserade Maskininlärning Företaget meddelade den 25 juli att dess system för artificiell intelligens (AI) löste fyra av de sex problem som gavs till studenter vid 2024 International Mathematical Olympiad (IMO) i Bath, Storbritannien. AI:n gav rigorösa, steg-för-steg-bevis utvärderade av två främsta matematiker och uppnådde en poäng på 28/42 - bara en poäng från guldmedaljområdet.
"Det är uppenbarligen ett mycket betydande framsteg", säger Joseph Myers, en matematiker från Cambridge, Storbritannien, som tillsammans med Fields-medaljören Tim Gowers granskade lösningarna och hjälpte till att välja de ursprungliga problemen för årets IMO.
DeepMind och andra företag är i kapplöpningen för att i slutändan förse maskiner med bevis som är viktiga Lös forskningsfrågor i matematik. De problem som presenterades vid IMO, världens ledande tävling för unga matematiker, har blivit ett riktmärke för framsteg mot det målet och anses vara en "stor utmaning" för maskininlärning, sa företaget.
"Det här är första gången ett AI-system har uppnått prestanda på medaljnivå", sa Pushmeet Kohli, vicepresident för AI i vetenskap på DeepMind, i en pressträff. "Detta är en viktig milstolpe för att bygga avancerade bevisutredare," sa Kohli.
Förlängning
För bara några månader sedan, i januari, kom DeepMind-systemet Prestationer på AlphaGeometry-medaljnivå uppnåtts för att lösa en typ av IMO-problem, nämligen de i euklidisk geometri. Den första AI som presterar på guldmedaljnivå på det övergripande testet – inklusive frågor i algebra, kombinatorik och talteori, som allmänt anses vara mer utmanande än geometri – kommer att vara berättigad till ett pris på $5 miljoner, AI Mathematics Olympiad Prize (AIMO). (Utmärkelsen har strikta kriterier som att avslöja källkod och arbeta med begränsad datorkraft, vilket innebär att DeepMinds nuvarande ansträngningar inte skulle kvalificera sig.)
I sitt senaste försök använde forskarna AlphaGeometry2 för att lösa geometriproblemet på under 20 sekunder; AI är en förbättrad och snabbare version av deras skivsystem, säger DeepMind-datorspecialisten Thang Luong.
För de andra typerna av frågor utvecklade teamet ett helt nytt system som heter AlphaProof. AlphaProof löste två algebraproblem i tävlingen och ett i talteori, vilket tog tre dagar. (Deltagare i själva IMO har två sessioner på 4,5 timmar vardera.) Det gick inte att lösa de två problemen i kombinatorik, ett annat område av matematik.
Forskare har haft blandade resultat när de besvarar matematiska frågor med hjälp av språkmodeller - den typ av system som driver chatbots som ChatGPT. Ibland ger modellerna rätt svar men kan inte förklara sina resonemang rationellt, och ibland de sprutar nonsens.
Bara förra veckan använde ett team av forskare från mjukvaruföretagen Numina och HuggingFace en språkmodell för att vinna ett mellanliggande AMIO "framstegspris" baserat på förenklade versioner av IMO-problem. Företagen har gjort hela sina system öppen källkod och gjort dem tillgängliga för andra forskare att ladda ner. Men vinnarna saNatur, att enbart språkmodeller förmodligen inte skulle räcka för att lösa svårare problem.
Endast klass
AlphaProof kombinerar en språkmodell med förstärkningsinlärningsteknologi som använder "AlphaZero"-motorn som företaget framgångsrikt har använt för attackspel som Go och några specifika matematiska problem begagnad. I förstärkningsinlärning lär sig ett neuralt nätverk genom försök och misstag. Detta fungerar bra när hans svar kan utvärderas med hjälp av en objektiv standard. För detta ändamål utbildades AlphaProof i att läsa och skriva korrektur på ett formellt språk som heter Lean, som används i mjukvarupaketet 'Proof Assistant' med samma namn som är populärt bland matematiker. För att göra detta testade AlphaProof om dess utdata var korrekta genom att köra dem i Lean-paketet, vilket hjälpte till att fylla i några av stegen i koden.
Att träna en språkmodell kräver enorma mängder data, men ändå fanns det få matematiska bevis tillgängliga i Lean. För att övervinna detta problem utvecklade teamet ytterligare ett nätverk som försökte översätta ett befintligt register med en miljon problem skrivna på naturligt språk men utan mänskliga skrivna lösningar till Lean, säger Thomas Hubert, en DeepMind-maskininlärningsforskare som var med och ledde utvecklingen av AlphaProof. "Vårt tillvägagångssätt var, kan vi lära oss att bevisa även om vi ursprungligen inte tränade på mänskligt skrivna bevis?" (Företaget tog ett liknande tillvägagångssätt som Go, där dess AI lärde sig att spela spelet genom att spela mot sig själv snarare än från hur människor gör det.)
Magiska nycklar
Många av Lean-översättningarna var inte vettiga, men tillräckligt många var tillräckligt bra för att få AlphaProof till den punkt där den kunde starta sina förstärkningsinlärningscykler. Resultaten var mycket bättre än väntat, sa Gowers vid pressträffen. "Många problem på IMO har den här magiska nyckelegenskapen. Problemet ser svårt ut tills du hittar en magisk nyckel som öppnar den", säger Gowers, som arbetar på Collège de France i Paris.
I vissa fall verkade AlphaProof kunna ge det där extra steget av kreativitet genom att tillhandahålla ett korrekt steg från en oändligt stor möjlig lösning. Men ytterligare analys behövs för att avgöra om svaren var mindre överraskande än de verkade, tillade Gowers. En liknande diskurs dök upp efter den överraskande "Tåg 37", DeepMinds AlphaGo-boten hos honom berömd seger 2016 över världens bästa mänskliga Go-spelare gjort – en vändpunkt för AI.
Huruvida teknikerna kan fulländas för att fungera på forskningsnivå i matematik återstår att se, sa Myers vid pressträffen. "Kan det expandera till andra typer av matematik som kanske inte har miljontals problem tränade på?"
"Vi är vid den punkt där de kan bevisa inte bara öppna forskningsproblem, utan också problem som är mycket utmanande för de allra bästa unga matematikerna i världen", säger DeepMind-datorspecialisten David Silver, som var den ledande forskaren som utvecklade AlphaGo i mitten av 2010-talet.