400 OpenAI rezultatų matematikams gali reikšti kelerius tikrinimo metus
The Verge kalbinti matematikai sako, kad OpenAI paskelbti šimtai DI sukurtų rezultatų gali užtrukti metus, kol bus suprasti ir patikrinti.
OpenAI paskelbti šimtai DI sukurtų matematikos rezultatų gali reikalauti metų darbo, kol akademinė bendruomenė supras, kas juose iš tiesų įrodyta.
The Verge spalio 9 dieną rašo, kad kalbėjosi su daugiau kaip trimis dešimtimis matematikų, bandančių įvertinti staigų rezultatų srautą. Leidinio teigimu, OpenAI išleido beveik 400 DI sugeneruotų rezultatų, paskirstytų per daugiau kaip 700 rankraščių.
Šis mastas svarbus, nes matematikoje rezultatas tampa vertingas tik tada, kai kiti žmonės gali suprasti įrodymą ir patikrinti teiginio ribas. The Verge nurodo, kad darbai apima kombinatoriką, geometriją, skaičių teoriją, teorinį informatikos mokslą, algebrą, topologiją, tikimybes ir matematinę fiziką.
Pasak leidinio, net pirminis medžiagos peržiūrėjimas yra sunkus. Keli matematikai The Verge sakė, kad vien apie 40 puslapių turinio lentelės ir santraukų peržiūra užtruko didžiąją valandos dalį.
Imperial College London profesorius Kevin Buzzard leidiniui sakė savo srityje, algebrinėje skaičių teorijoje, radęs kelis teiginius, kurie iškart išsiskyrė. Tačiau jis pabrėžė, kad jeigu jie nėra formalizuoti, matematikams teks skaityti galimai neteisingą medžiagą arba laukti kitų patikros.
The Verge rašo, kad dalis rankraščių turi formalizacijas Lean kalba, kuri leidžia kompiuteriu tikrinti matematinius įrodymus. Tačiau OpenAI savo GitHub saugykloje pripažino, kad rezultatai yra skirtinguose patikros etapuose, o formalizuota ne visa medžiaga.
Leidinio duomenimis, formalizuota apie 300 pagrindinių rezultatų iš 719 rankraščių, tai yra maždaug 42 procentai. Net tada tyrėjai turi patikrinti, ar formalizacija tikrai atitinka rankraštyje teigiamą rezultatą.
Ši naujiena rodo, kad DI moksle gali sukurti ne tik greitį, bet ir naują darbo eilę žmonėms. Jei rezultatų daug daugiau nei gebančių juos tikrinti specialistų, akademinė vertė priklausys nuo atrankos, formalizavimo ir aiškaus dokumentavimo.
The Verge cituoja matematikų vertinimus, kad net kompiuteriu patikrinamas Lean kodas nepašalina žmogaus darbo. Reikia suprasti, ar formali formuluotė atitinka matematinį teiginį, kurį rankraštis žada išspręsti.
Toliau bus matyti, kurie OpenAI rezultatai taps pripažintais matematikos indėliais, o kurie liks nepatikrintų tekstų mase. Kol kas pagrindinis pokytis aiškus: DI gali pagaminti pakankamai daug teorinės medžiagos, kad pats tikrinimas tampa atskiru moksliniu iššūkiu.
Rašome apie dirbtinį intelektą lietuviškai. Kiekvienas straipsnis parengtas pagal nurodytą šaltinį, o nuorodą į originalą rasite kortelėje „Šaltinis“.
