Nakon što je Google DeepMind pobijedio ljude u svemu, od Igrajte Go to strateške društvene igre,
sada tvrdi da je na rubu pobjede nad najboljim studentima svijeta u rješavanju matematičkih problema.
Sa sjedištem u Londonu Strojno učenje Tvrtka je 25. srpnja objavila da su njezini sustavi umjetne inteligencije (AI) riješili četiri od šest problema zadanih učenicima na Međunarodnoj matematičkoj olimpijadi (IMO) 2024. u Bathu, Ujedinjeno Kraljevstvo. AI je pružio rigorozne, korak-po-korak dokaze koje su procijenila dva vrhunska matematičara i postigao ocjenu 28/42 - samo jedan bod od teritorija zlatne medalje.
“To je očito vrlo značajan napredak,” kaže Joseph Myers, matematičar iz Cambridgea, UK, koji je, zajedno s dobitnikom Fieldsove medalje Timom Gowersom, pregledao rješenja i pomogao u odabiru izvornih problema za ovogodišnji IMO.
DeepMind i druge tvrtke su u utrci da strojevima konačno pruže dokaze koji su važni Riješite istraživačka pitanja iz matematike. Problemi predstavljeni na IMO-u, vodećem svjetskom natjecanju za mlade matematičare, postali su mjerilo za napredak prema tom cilju i smatraju se "velikim izazovom" za strojno učenje, priopćila je tvrtka.
"Ovo je prvi put da je sustav umjetne inteligencije postigao performanse na razini medalje", rekao je Pushmeet Kohli, potpredsjednik AI u znanosti u DeepMindu, na brifingu za novinare. "Ovo je važna prekretnica u izgradnji naprednih istražitelja dokaza", rekao je Kohli.
Proširenje
Prije samo nekoliko mjeseci, u siječnju, sustav DeepMind AlphaGeometry postignuća na razini medalje postignut u rješavanju jedne vrste IMO problema, naime onih u euklidskoj geometriji. Prvi AI koji postigne zlatnu medalju na cjelokupnom testu – uključujući pitanja iz algebre, kombinatorike i teorije brojeva, koja se općenito smatraju izazovnijima od geometrije – moći će dobiti nagradu od 5 milijuna dolara, nagradu AI Mathematics Olympiad Prize (AIMO). (Nagrada ima stroge kriterije kao što su otkrivanje izvornog koda i rad s ograničenom računalnom snagom, što znači da se DeepMindovi trenutni napori ne bi kvalificirali.)
U svom posljednjem pokušaju, istraživači su koristili AlphaGeometry2 za rješavanje geometrijskog problema za manje od 20 sekundi; AI je poboljšana i brža verzija njihovog sustava za snimanje, kaže računalni stručnjak DeepMinda Thang Luong.
Za druge vrste pitanja tim je razvio potpuno novi sustav pod nazivom AlphaProof. AlphaProof je rješavao dva zadatka iz algebre na natjecanju i jedan iz teorije brojeva, što je trajalo tri dana. (Sudionici stvarnog IMO-a imaju dvije sesije od po 4,5 sata.) Nije bilo moguće riješiti dva problema u kombinatorici, drugom području matematike.

Istraživači su imali različite rezultate kada su odgovarali na matematička pitanja koristeći jezične modele — vrstu sustava koji pokreću chatbotove poput ChatGPT-a. Ponekad modeli daju točan odgovor, ali ne mogu racionalno objasniti svoje razmišljanje, a ponekad lupaju gluposti.
Samo prošli tjedan, tim istraživača iz softverskih kompanija Numina i HuggingFace koristio je jezični model da osvoji srednju AMIO 'nagradu za napredak' temeljenu na pojednostavljenim verzijama IMO problema. Tvrtke su svoje cjelokupne sustave učinile otvorenim kodom i učinile ih dostupnima za preuzimanje drugim istraživačima. Ali pobjednici su rekliPriroda, da sami jezični modeli vjerojatno ne bi bili dovoljni za rješavanje težih problema.
Samo klasa
AlphaProof kombinira jezični model s tehnologijom učenja s pojačanjem koja koristi motor "AlphaZero" koji je tvrtka uspješno koristila za napadačke igre kao što su Go i neke specifične matematičke probleme koristi se. U učenju s potkrepljenjem, neuronska mreža uči putem pokušaja i pogrešaka. Ovo dobro funkcionira kada se njegovi odgovori mogu ocijeniti pomoću objektivnog standarda. U tu svrhu AlphaProof je obučen za čitanje i pisanje dokaza u formalnom jeziku koji se zove Lean, a koji se koristi u istoimenom softverskom paketu 'Proof Assistant' koji je popularan među matematičarima. Kako bi to učinio, AlphaProof je testirao jesu li njegovi rezultati ispravni tako što ih je pokrenuo u paketu Lean, što je pomoglo u ispunjavanju nekih koraka u kodu.
Uvježbavanje jezičnog modela zahtijeva goleme količine podataka, no malo je matematičkih dokaza bilo dostupno u Leanu. Kako bi prevladao ovaj problem, tim je razvio dodatnu mrežu koja je pokušala prevesti postojeći zapis od milijun problema napisanih prirodnim jezikom, ali bez rješenja koje je napisao čovjek, u Lean, kaže Thomas Hubert, DeepMindov istraživač strojnog učenja koji je suvodio razvoj AlphaProofa. "Naš je pristup bio, možemo li naučiti dokazivati čak i ako izvorno nismo trenirali na dokazima koje su napisali ljudi?" (Tvrtka je zauzela sličan pristup Gou, gdje je njegova umjetna inteligencija naučila igrati igru igrajući sama protiv sebe, a ne na način na koji to rade ljudi.)
Čarobni ključevi
Mnogi od Lean prijevoda nisu imali smisla, ali dovoljno je bilo dovoljno dobrih da AlphaProof dovede do točke u kojoj može započeti svoje cikluse učenja pojačanja. Rezultati su bili puno bolji od očekivanih, rekao je Gowers na brifingu za novinare. "Mnogi problemi u IMO-u imaju svojstvo čarobnog ključa. Problem isprva izgleda teško dok ne pronađete čarobni ključ koji ga otvara", rekao je Gowers, koji radi na Collège de France u Parizu.
U nekim se slučajevima činilo da AlphaProof može pružiti taj dodatni korak kreativnosti pružajući jedan točan korak iz beskrajno velikog mogućeg rješenja. Ali potrebna je daljnja analiza kako bi se utvrdilo jesu li odgovori manje iznenađujući nego što se činilo, dodao je Gowers. Sličan diskurs pojavio se nakon iznenađujućeg 'Vlak 37', DeepMinds AlphaGo bot kod njega poznata pobjeda iz 2016. nad najboljim svjetskim ljudskim Go igračem napravio – prekretnica za AI.
Ostaje za vidjeti mogu li se tehnike usavršiti za rad na razini istraživanja u matematici, rekao je Myers na konferenciji za novinare. "Može li se proširiti na druge vrste matematike koje možda nemaju milijune problema na kojima se vježba?"
"Nalazimo se na točki u kojoj mogu dokazati ne samo otvorene istraživačke probleme, već i probleme koji su veliki izazov za najbolje mlade matematičare na svijetu", rekao je DeepMind računalni stručnjak David Silver, koji je bio vodeći istraživač koji je razvijao AlphaGo sredinom 2010-ih.
 
             
				  