Suche
Mein Konto
Po to, kai „Google DeepMind“ nugalėjo žmones visame kame, nuo Žaisti Eikite į strateginius stalo žaidimus,
dabar ji teigia esanti ant slenksčio, sprendžiant matematikos uždavinius geriausius pasaulio mokinius.
Londone įsikūręs Mašininis mokymasis Bendrovė liepos 25 d. paskelbė, kad jos dirbtinio intelekto (AI) sistemos išsprendė keturias iš šešių problemų, kurios buvo pateiktos studentams 2024 m. Tarptautinėje matematikos olimpiadoje (IMO) Bath mieste, Jungtinėje Karalystėje. AI pateikė griežtus, žingsnis po žingsnio įrodymus, kuriuos įvertino du geriausi matematikai ir pasiekė 28/42 balą – tik vieną tašką iš aukso medalio teritorijos.
„Akivaizdu, kad tai labai reikšminga pažanga“, – sako Josephas Myersas, matematikas iš Kembridžo, JK, kuris kartu su Fields medalininku Timu Gowersu apžvelgė sprendimus ir padėjo pasirinkti pirmines šių metų TJO problemas.
DeepMind ir kitos bendrovės lenktyniauja, kad galiausiai pateiktų mašinoms svarbių įrodymų Spręskite matematikos tyrimo klausimus. TJO, pirmaujančiame pasaulyje jaunųjų matematikų konkurse, pateiktos problemos tapo pažangos etalonu siekiant šio tikslo ir yra laikomos „didžiuliu iššūkiu“ mašinų mokymuisi, teigė bendrovė.
„Tai pirmas kartas, kai dirbtinio intelekto sistema pasiekė medalio lygio našumą“, – spaudos konferencijoje sakė Pushmeetas Kohli, „DeepMind“ DI mokslo srityje viceprezidentas. „Tai svarbus žingsnis kuriant pažangius įrodymų tyrėjus“, – sakė Kohli.
Pratęsimas
Vos prieš kelis mėnesius, sausio mėnesį, DeepMind sistema AlphaGeometry medalio lygio pasiekimai pasiekti sprendžiant vieno tipo TJO problemas, būtent tas, kurios yra Euklido geometrijoje. Pirmasis dirbtinis intelektas, pasiekęs aukso medalį atliekant bendrą testą, įskaitant algebros, kombinatorikos ir skaičių teorijos klausimus, kurie paprastai laikomi sudėtingesniais nei geometrija, turės teisę gauti 5 milijonų dolerių prizą, AI matematikos olimpiados prizą (AIMO). (Apdovanojimui taikomi griežti kriterijai, tokie kaip šaltinio kodo atskleidimas ir darbas su ribota skaičiavimo galia, o tai reiškia, kad dabartinės „DeepMind“ pastangos nebūtų tinkamos.)
Paskutiniame bandyme mokslininkai panaudojo AlphaGeometry2 geometrijos problemą išspręsti per mažiau nei 20 sekundžių; AI yra patobulinta ir greitesnė jų įrašų sistemos versija, sako „DeepMind“ kompiuterių specialistas Thangas Luongas.
Dėl kitų tipų klausimų komanda sukūrė visiškai naują sistemą, pavadintą AlphaProof. AlphaProof išsprendė du algebros uždavinius varžybose ir vieną skaičių teorijoje, kuri užtruko tris dienas. (Tikros TJO dalyviai turi dvi sesijas po 4,5 valandos.) Ji negalėjo išspręsti dviejų kombinatorikos, kitos matematikos srities, uždavinių.
Tyrėjai gavo įvairių rezultatų atsakydami į matematinius klausimus naudodami kalbos modelius – tokias sistemas, kurios maitina pokalbių robotus, tokius kaip ChatGPT. Kartais modeliai pateikia teisingą atsakymą, bet negali racionaliai paaiškinti savo samprotavimų, o kartais jie spėlioja nesąmones.
Dar praėjusią savaitę programinės įrangos kompanijų „Numina“ ir „HuggingFace“ tyrėjų komanda naudojo kalbos modelį, kad laimėtų tarpinį AMIO „pažangos prizą“, pagrįstą supaprastintomis TJO problemų versijomis. Įmonės padarė visas savo sistemas atviro kodo ir leido jas atsisiųsti kitiems tyrėjams. Tačiau nugalėtojai sakėGamta, kad vien kalbos modelių, ko gero, nepakaktų sunkesnėms problemoms spręsti.
Tik klasė
AlphaProof sujungia kalbos modelį su sustiprinimo mokymosi technologija, kuri naudoja „AlphaZero“ variklį, kurį įmonė sėkmingai panaudojo atakos žaidimams, tokiems kaip „Go“ ir kai kurie. specifines matematines problemas naudotas. Stiprinant mokymąsi, neuroninis tinklas mokosi per bandymus ir klaidas. Tai gerai veikia, kai jo atsakymus galima įvertinti naudojant objektyvų standartą. Šiuo tikslu AlphaProof buvo išmokytas skaityti ir rašyti įrodymus formalia kalba, vadinama Lean, kuri naudojama matematikų populiariame to paties pavadinimo programinės įrangos pakete „Proof Assistant“. Norėdami tai padaryti, „AlphaProof“ patikrino, ar jo išėjimai yra teisingi, paleisdami juos „Lean“ pakete, kuris padėjo atlikti kai kuriuos kodo veiksmus.
Kalbos modelio mokymas reikalauja didžiulio duomenų kiekio, tačiau Lean programoje buvo mažai matematinių įrodymų. Siekdama įveikti šią problemą, komanda sukūrė papildomą tinklą, kuriame buvo bandoma išversti esamą milijono problemų, parašytų natūralia kalba, bet be žmogaus parašytų sprendimų, įrašą į Lean, sako Thomas Hubertas, „DeepMind“ mašininio mokymosi tyrinėtojas, vadovavęs AlphaProof kūrimui. „Mūsų požiūris buvo toks: ar galime išmokti įrodyti, net jei iš pradžių nesimokėme remdamiesi žmogaus rašytais įrodymais? (Bendrovė laikėsi panašaus požiūrio į Go, kur jos AI išmoko žaisti žaidimą žaisdamas prieš save, o ne iš to, kaip tai daro žmonės.)
Magiški raktai
Daugelis „Lean“ vertimų nebuvo prasmingi, tačiau buvo pakankamai geri, kad „AlphaProof“ pasiektų tokį tašką, kad galėtų pradėti sustiprinimo mokymosi ciklus. Rezultatai buvo daug geresni, nei tikėtasi, spaudos konferencijoje sakė Gowersas. "Daugelis problemų TJO turi šią magiškojo rakto savybę. Problema iš pradžių atrodo sudėtinga, kol randate stebuklingą raktą, kuris jį atidaro", - sakė Gowersas, dirbantis Paryžiaus koledže "Collège de France".
Kai kuriais atvejais atrodė, kad AlphaProof galėjo suteikti tą papildomą kūrybiškumo žingsnį, pateikdama vieną teisingą žingsnį iš be galo didelio galimo sprendimo. Tačiau norint nustatyti, ar atsakymai buvo mažiau stebinantys, nei atrodė, reikia atlikti tolesnę analizę, pridūrė Gowersas. Panašus diskursas atsirado po netikėto „Traukinys 37“, „DeepMinds AlphaGo“ robotas garsioji 2016 m. pergalė prieš geriausią pasaulyje žmogaus Go žaidėją padarė AI lūžio tašką.
Myersas per spaudos konferenciją sakė, ar galima tobulinti metodus, kad jie veiktų matematikos tyrimų lygmeniu. „Ar tai gali būti išplėsta į kitas matematikos rūšis, kuriose gali būti neišmokyta milijonų problemų?
„Esame toje vietoje, kur jie gali įrodyti ne tik atviras mokslinių tyrimų problemas, bet ir problemas, kurios yra labai sudėtingos patiems geriausiems jauniems pasaulio matematikams“, – sakė „DeepMind“ kompiuterių specialistas Davidas Silveris, kuris 2010-ųjų viduryje buvo pagrindinis AlphaGo kūrėjas.