DeepMind pasiekia matematinių problemų sprendimo etapą - kitas didelis iššūkis AI
DeepMind pasiekia matematinių problemų sprendimo etapą - kitas didelis iššūkis AI
Po to, kai „Google DeepMind“ nugalėjo žmones viskuo, iš Žaidimas Eikite į strateginius lentelės žaidimus ,
Dabar teigia, kad reikia įveikti geriausius pasaulio studentus, kai sprendžiant matematikos užduotis.
Londone įsikūręs Mašinų mokymasis Bendrovė liepos 25 d. Paskelbė, kad jo dirbtinio intelekto (KI) sistemos išsprendė keturias iš šešių užduočių, kurios buvo duotos tarptautinės matematikos olimpinių žaidynių (TJO) 2024 m., Bath, Didžiojoje Britanijoje. PG pateikė griežtus, laipsniškus įrodymus, kurie buvo įvertinti dviem geriausiomis matematikomis ir pasiekė tik 28/42 balą iš vieno taško iš aukso medalių srities.
"Tai akivaizdžiai labai svarbi pažanga", - sako Josephas Myersas, matematikas iš Kembridžo, Didžiosios Britanijos, kuris kartu su laukų medalininku Timu Gowersu patikrino sprendimus ir padėjo atrinkti pirmines problemas šiais metais.
„DeepMind“ ir kitos įmonės rengia lenktynes, kad galų gale pateiktų mašinų įrodymus, esminį Išspręskite tyrimo klausimus matematikoje . Problemos, susijusios su TJO, pirmaujančia pasaulyje jaunų matematikų varžybomis, tapo kriterijomis, skirtoms pažangai šio tikslo kryptimi, ir, pasak bendrovės, yra laikomos „dideliu iššūkiu“ mašinų mokymuisi.
"Tai yra pirmas kartas, kai AI sistema sugebėjo pasiekti paslaugas medalio lygiu", - sakė Pushmeet Kohli, „Deepmind“ mokslo viceprezidentas, konsultuodamasi spaudai. „Tai yra svarbus etapas pakeliui į progresyvių įrodymų kūrimą“, - sakė Kohli.
pratęsimas
Tik prieš keletą mėnesių, sausio mėn., „DeepMind“ sistema Alfageometrijos paslaugos medalių lygyje Sprendžiant tam tikros rūšies Imo problemas, būtent Euklidinės geometrijos tipą. Pirmasis AI, dirbantis aukso medalyje, siekiant bendro testo, įtraukiančio klausimus algebroje, kombinatorikoje ir skaičių teorijoje, kurie paprastai laikomi reiklesniais nei geometrija-turi teisę gauti 5 mln. USD kainą, AI matematikos olimpiados premiją (AIMO). )
Naujausiame bandyme tyrėjai panaudojo alfageometriją2, kad išspręstų geometrijos problemą per mažiau nei 20 sekundžių; AI yra patobulinta ir greitesnė jūsų įrašų sistemos versija, sako „Deepmind“ kompiuterių specialistas Thang Luong.
Dėl kitų tipų klausimų komanda sukūrė visiškai naują sistemą, vadinamą „Alphaproof“. Alfaproofas išsprendė dvi algebros problemas konkurencijoje ir vieną skaičių teorijoje, kuriai tai užtruko tris dienas. (Faktinio TJO dalyvių dviem sesijomis yra po 4,5 valandos.) Ji negalėjo išspręsti dviejų derinio problemų, kitos matematikos srities.
Tyrėjai pasiekė įvairių rezultatų, kai atsako į matematinius klausimus su balso modeliais - tokio tipo, kuris skatina pokalbių programas, tokias kaip „Chatt“. Kartais modeliai pateikia teisingą atsakymą, tačiau negali racionaliai paaiškinti savo samprotavimo, o kartais Specifinės matematinės problemos . Didėjant mokymui, neuroninis tinklas mokosi eksperimentų ir klaidų. Tai gerai veikia, jei jo atsakymus galima įvertinti naudojant objektyvią skalę. Šiuo tikslu „Alphaproof“ buvo išmokytas skaityti ir rašyti įrodymus oficialia kalba, vadinama Lean, kuri naudojama to paties pavadinimo programinės įrangos pakete „PROOR Assistant“, kuris yra populiarus tarp matematikų. Tam „Alphaproof“ patikrino, ar jo išlaidos buvo teisingos, darant jas į liesą paketą, kuris padėjo užpildyti kai kuriuos kodekso veiksmus.
Balso modelio mokymui reikalingas didžiulis duomenų kiekis, tačiau liesai buvo prieinami tik keli matematiniai įrodymai. Siekdama išspręsti šią problemą, komanda sukūrė papildomą tinklą, kuris bandė išversti esamą milijono problemų, kurios buvo parašytos natūralia kalba, įrašą, tačiau neišvertė sprendimų, parašytų Lean, sako Thomas Hubert, „Deepmind Machine“ besimokančiojo tyrėjas, kuris vykdė „Alphaproof“ plėtrą. "Mes galime išmokti įrodyti savo požiūrį, net jei mes iš pradžių neišmokėme pagal žmogaus rašytus įrodymus?" (Kompanija buvo panaši į kelio vietą, kur jo AI išmoko žaisti žaidimą žaisdamas prieš save, o ne tai, kaip žmonės tai daro.)
stebuklingas raktas
Daugelis liesų vertimų neturėjo prasmės, tačiau pakankamai buvo pakankamai geri, kad alfaproofas būtų toks, kad jis galėtų pradėti didėjančius mokymosi ciklus. Rezultatai buvo daug geresni nei tikėtasi, sakė „Gowers“ spaudos konsultacijoje. "Daugybė problemų, susijusių su TJO, turi šią stebuklingo rakto savybę. Problema pirmiausia atrodo sunku, kol rasite stebuklingą raktą, kuris jį atveria", - sakė Gowersas, dirbantis „Collège de France“ Paryžiuje.
Kai kuriais atvejais „Alphaproof“ atrodė, kad gali žengti šį papildomą kūrybiškumo žingsnį, suteikdamas teisingą žingsnį iš be galo didelio įmanomo sprendimo. Tačiau norint nustatyti, ar atsakymai buvo ne tokie stebinantys, nei atrodė, reikia atlikti papildomą analizę, pridūrė „Gowers“. Panašus diskursas atsirado po stebėtino Garsioji pergalė 2016 m. Apie geriausią pasaulyje „Human Go“ grotuvą -Ki posūkio taškas.
Belieka išsiaiškinti, ar metodai gali būti tobulinami, kad jie galėtų atlikti matematikos tyrimų lygį, sakė Myers spaudos apžvalgoje. "Ar tai gali išplėsti į kitų rūšių matematiką, kai negalima mokyti jokių milijonų problemų?"
"Mes pasiekėme tašką, kuriame jūs galite ne tik įrodyti atvirų tyrimų problemas, bet ir problemas, kurios yra labai sudėtingos geriausiems jauniems matematikams pasaulyje",-sakė „Deepmind“ kompiuterių specialistas Davidas Silveris, kuris buvo pagrindinis „Alphago“ plėtros tyrėjas 2010 m. Viduryje.