DeepMind når milstolpen i lösningen av matematiska problem - nästa stora utmaning för AI

Efter att Google DeepMind besegrade människor i allt, från GAG TO STRATEGY BOARD GAMES ,
Nu påstår sig vara på väg att slå världens bästa studenter när de löser matematiska uppgifter.

den Londonbaserade Maskininlärning Företaget tillkännagav den 25 juli att hans konstgjorda intelligens (KI) -system har löst fyra av de sex uppgifterna som gavs till studenterna vid International Mathematics Olympics (IMO) 2024 i Bath, Storbritannien. AI tillhandahöll rigorösa, gradvisa bevis, som utvärderades med två topp matematik och uppnådde en poäng på 28/42 endast en poäng från området med guldmedaljer.

"Det är uppenbarligen en mycket viktig framsteg," säger Joseph Myers, en matematiker från Cambridge, Storbritannien, som tillsammans med fältmedaljist Tim Gowers kontrollerade lösningarna och hjälpte till att välja de ursprungliga problemen för detta år.

DeepMind och andra företag är i loppet för att i slutändan ge bevis på maskiner, det väsentliga Lös forskningsfrågor i matematik . Problemen med IMO, världens ledande konkurrens för unga matematiker, har blivit en måttstock för framsteg i riktning mot detta mål och ses som en "stor utmaning" för maskininlärning, enligt företaget.

"Detta är första gången som ett AI -system kunde uppnå tjänster på medaljnivå," sade Pushmeet Kohli, vice president för AI i Science på DeepMind, i en presskonsult. "Detta är en viktig milstolpe på väg att bygga upp progressiva bevis," sade Kohli.

förlängning

För bara några månader sedan, i januari, DeepMind System Alfageometri-tjänster på medaljer nivå När man löser en typ av IMO-problem, nämligen de i den euklidiska geometri. Den första AI som arbetar på en guldmedaljnivå för de övergripande test inklusive frågor i algebra, kombinatorik och antal teori, som i allmänhet anses vara mer krävande än geometri-är rätt att få ett pris på 5 miljoner dollar, AI Math Olympiad Prize (AIMO). (Priset har strikta kriterier som avslöjande av källkoden och arbetet med begränsad datorkraft, vilket innebär att de aktuella ansträngningarna inte skulle kvalificera sig.)

I sitt senaste försök använde forskare alfageometri2 för att lösa geometriproblemet på mindre än 20 sekunder; AI är en förbättrad och snabbare version av ditt 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å algebra -problem i tävlingen och en i siffror, för vilken det tog tre dagar. (Deltagarna i den faktiska IMO har två sessioner på 4,5 timmar vardera.) Det kunde inte lösa de två problemen i kombinationen, ett annat matematikområde.

Forskare har uppnått blandade resultat när de svarar på matematiska frågor med röstmodeller - den typ av system som driver chatbots som Chatt. Ibland ger modellerna rätt svar, men kan inte förklara deras resonemang rationellt, och ibland

Först förra veckan använde ett team av mjukvaruföretag Numina och Huggingface en röstmodell för att vinna ett mellanliggande Amios framstegspris "baserat på förenklade versioner av IMO -problem. Företagen gjorde hela systemet öppna källor och gjorde det tillgängligt för att ladda ner andra forskare. Men vinnarna sa Nature att språkmodeller ensamma förmodligen inte skulle räcka för att lösa svåra problem.

alphaproof kombinerar en röstmodell med tekniken för att förstärka lärande, som "alphazero" -motorn för attackspel som GO såväl som några Specifika matematiska problem . Med ökande lärande lär sig ett neuralt nätverk genom experiment och fel. Detta fungerar bra om dess svar kan utvärderas med en objektiv skala. För detta ändamål utbildades alphaproof för att läsa och skriva bevis på ett formellt språk som heter Lean, som används i programvarupaketet "Proof Assistant" med samma namn som är populärt bland matematiker. För detta testade alphaproof om hans utgifter var korrekta genom att göra dem i Lean -paketet, vilket hjälpte till att fylla i några av stegen i koden.

Utbildningen av en röstmodell kräver enorma mängder data, men endast ett fåtal matematiska bevis fanns tillgängliga i Lean. För att övervinna detta problem utvecklade teamet ett ytterligare nätverk som försökte översätta en befintlig inspelning av en miljon problem som skrevs på naturligt språk, men utan att översätta lösningar skrivna i Lean, säger Thomas Hubert, en djupmaskinforskare som genomförde utvecklingen av alphaproof med. "Vi kan lära oss att bevisa vår strategi, även om vi ursprungligen inte har utbildat på mänskliga skrivna bevis?" (Företaget liknade Go, där hans AI lärde sig spela spelet genom att spela mot sig själv, istället för hur människor gör.)

magisk nyckel

Många av de magra översättningarna gav ingen mening, men tillräckligt bra var tillräckligt bra för att få alphaproof till den punkt där den kunde starta sina ökande inlärningscykler. Resultaten var mycket bättre än väntat, säger Gowers vid presskonsultationen. "Många problem med IMO har den här egenskapen till den magiska nyckeln. Problemet ser först svårt ut tills du hittar en magisk nyckel som öppnar den," sade Gowers, som arbetar på Collège de France i Paris.

I vissa fall verkade alphaproof kunna ta detta ytterligare kreativitetssteg genom att ge det ett korrekt steg från en oändligt stor möjlig lösning. Men ytterligare analys krävs för att avgöra om svaren var mindre överraskande än de såg ut, tilllade gowers. En liknande diskurs uppstod efter den överraskande 'Zug 37' , The DeepMinds AlphaGo-bot at his Berömd seger 2016 om världens bästa Human Go-spelare -A vändpunkt för KI.

Det återstår att se om teknikerna kan perfekteras för att arbeta på en nivå av forskning i matematik, sade Myers vid pressöversynen. "Kan det expandera till andra typer av matematik där inga miljoner problem kan utbildas?"

"Vi har nått den punkt där du inte bara kan bevisa öppna forskningsproblem, utan också problem som är mycket utmanande för de allra bästa unga matematikerna i världen," sa DeepMind-datorspecialisten David Silver, som var den ledande forskaren i utvecklingen av AlphaGo i mitten av 2010.