DeepMind når milepæl i løsningen av matematiske problemer - den neste store utfordringen for AI

Etter at Google DeepMind beseiret folk i alt, fra Game Go to Strategy Board Games ,
Hevder nå å være på grensen til å slå verdens beste studenter når de løser matematikkoppgaver.

Den London-baserte Machine-Learning Company kunngjorde 25. juli at hans kunstige intelligens (KI) -systemer har løst fire av de seks oppgavene som ble gitt til studentene ved International Mathematics Olympics (IMO) 2024 i Bath, Storbritannia. AI ga strenge, gradvis bevis, som ble evaluert av to toppmatematikk og oppnådde en poengsum på 28/42-bare ett punkt fra området med gullmedaljer.

"Det er åpenbart en veldig viktig fremgang," sier Joseph Myers, en matematiker fra Cambridge, Storbritannia, som sammen med Fields -medaljen Tim Gowers sjekket løsningene og bidro til å velge de opprinnelige problemene for dette året.

DeepMind og andre selskaper er i løpet av til slutt å fremlegge bevis for maskiner, det essensielle Løs forskningsspørsmål i matematikk . Problemene med IMO, verdens ledende konkurranse om unge matematikere, har blitt en målestokk for fremgang i retning av dette målet og blir sett på som en "stor utfordring" for maskinlæring, ifølge selskapet.

"Dette er første gang at et AI -system var i stand til å oppnå tjenester på medaljivå," sa Pushmeet Kohli, visepresident for AI i Science at DeepMind, i en pressekonsultasjon. "Dette er en viktig milepæl på vei til å bygge opp progressive bevis," sa Kohli.

utvidelse

Bare for noen måneder siden, i januar, DeepMind-systemet Alphageometry Services på medaljernivå Når du løser en type IMO-problemer, nemlig de i Euclidean Geomety-geomety. Den første AI som fungerer på et gullmedalje-nivå for de samlede test-inkludert spørsmålene i algebra, kombinatorikk og tallteori, som generelt anses som mer krevende enn geometri-har rett til å få en pris på $ 5 millioner, AI Math Olympiad-prisen (AIMO). (Prisen har strenge kriterier som avsløring av kildekoden og arbeidet med begrenset datakraft, noe som betyr at den nåværende innsatsen til DeepMind ikke ville kvalifisere seg.)

I sitt siste forsøk brukte forskere AlphageOmetry2 for å løse geometri -problemet på mindre enn 20 sekunder; AI er en forbedret og raskere versjon av platesystemet ditt, sier DeepMind Computer Specialist Thang Luong.

For de andre typene spørsmål utviklet teamet et helt nytt system kalt Alphaproof. Alphaproof løste to algebraproblemer i konkurransen og en i antall teori, som det tok tre dager. (Deltakerne i den faktiske IMO har to økter på 4,5 timer hver.) Det klarte ikke å løse de to problemene i kombinasjonen, et annet matematikkområde.

Forskere har oppnådd blandede resultater når de svarer på matematiske spørsmål med stemmemodeller - typen system som driver chatbots som Chatt. Noen ganger gir modellene riktig svar, men kan ikke forklare resonnementet rasjonelt, og noen ganger >

Bare forrige uke brukte et team av programvareselskaper Numina og Huggingface en stemmemodell for å vinne en mellomliggende Amio 'Progress Price' basert på forenklede versjoner av IMO -problemer. Selskapene gjorde hele systemene åpen kildekode og gjorde det tilgjengelig for nedlasting av andre forskere. Men vinnerne sa natur at språkmodeller alene sannsynligvis ikke ville være nok til å løse vanskelige problemer.

Bare klasse

Alphaproof kombinerer en stemmemodell med teknologien for å forsterke læring, som "Alphazero" -motoren for angrepsspill som Go, så vel som noen Spesifikke matematiske problemer . Med økende læring lærer et nevralt nettverk gjennom eksperimenter og feil. Dette fungerer bra hvis svarene kan evalueres ved hjelp av en objektiv skala. For dette formålet ble Alphaproof opplært til å lese og skrive bevis på et formelt språk kalt Lean, som brukes i programvarepakken 'Proof Assistant' med samme navn som er populær blant matematikere. For dette testet Alphaproof om utgiftene hans var riktige ved å gjøre dem i Lean -pakken, noe som bidro til å fylle ut noen av trinnene i koden.

Opplæringen av en stemmemodell krever enorme datamengder, men bare noen få matematiske bevis var tilgjengelige i Lean. For å overvinne dette problemet utviklet teamet et ekstra nettverk som prøvde å oversette et eksisterende innspilling av en million problemer som ble skrevet på naturlig språk, men uten å oversette løsninger skrevet i Lean, sier Thomas Hubert, en forsker fra DeepMind Machine som gjennomførte utviklingen av Alphaproof med. "Vi kan lære å bevise vår tilnærming, selv om vi ikke opprinnelig har trent på menneskelige skrevne bevis?" (Selskapet var likt farten, der hans AI lærte å spille spillet ved å spille mot seg selv, i stedet for slik folk gjør.)

magisk nøkkel

Mange av de magre oversettelsene ga ingen mening, men nok var gode nok til å bringe alfapoof til det punktet hvor det kunne starte sine økende læringssykluser. Resultatene var mye bedre enn forventet, sa Gowers på pressekonsultasjonen. "Mange problemer med IMO har denne egenskapen til den magiske nøkkelen. Problemet ser først vanskelig ut til du finner en magisk nøkkel som åpner den," sa Gowers, som jobber på Collège de France i Paris.

I noen tilfeller så Alphaproof ut til å kunne ta dette ekstra kreativitetstrinnet ved å gi det et riktig skritt fra en uendelig stor mulig løsning. Men det kreves ytterligere analyse for å avgjøre om svarene var mindre overraskende enn de så ut, la Gowers til. En lignende diskurs oppsto etter den overraskende 'Zug 37' , The DeepMinds AlphaGo-Bot på hans Famous Victory i 2016 om verdens beste menneskelige Go Player Et vendepunkt for KI.

Det gjenstår å se om teknikkene kan perfeksjoneres for å fungere på et forskningsnivå i matematikk, sa Myers ved Press Review. "Kan den utvide til andre typer matematikk der ingen millioner av problemer kan bli opplært?"

"Vi har nådd det punktet hvor du ikke bare kan bevise åpne forskningsproblemer, men også problemer som er veldig utfordrende for de aller beste unge matematikerne i verden," sa DeepMind Computer Specialist David Silver, som var den ledende forskeren i utviklingen av AlphaGo i midten av 2010.