Pateikti „First Proof“ įrodymai
Dalijamės savo įrodymų bandymais, skirtais „First Proof“ – matematiniam iššūkiui, kuriuo tikrinama, ar dirbtinis intelektas gali pateikti patikrinamus įrodymus konkrečios srities problemoms spręsti.
Paleidome vidinį modelį visoms 10 „First Proof“(atsidaro naujame lange) užduotims – tai mokslinio lygio matematikos iššūkis, skirtas patikrinti, ar DI sistemos gali pateikti teisingus ir patikrinamus įrodymų bandymus. Skirtingai nei trumpo atsakymo ar konkursinio tipo matematika, šios užduotys reikalauja kurti visapusiškus argumentus specializuotose srityse, o teisingumą sunku nustatyti be ekspertų peržiūros. Pirmosios įrodymų problemų autoriai yra savo sričių pirmaujantys ekspertai, ir bent kelios problemos buvo atviros daugelį metų, kol autoriai rado sprendimus. Akademinis padalinys, kurio veiklos sritys iš esmės sutampa su nagrinėjamomis temomis, galėtų teoriškai per vieną savaitę išspręsti daugelį problemų.
Savo įrodymų bandymais pasidalijome(atsidaro naujame lange) 2026 m. vasario 14 d., šeštadienį, 00:00 val. Ramiojo vandenyno laiku. Remdamiesi ekspertų atsiliepimais, manome, kad bent penki modelio įrodymų bandymai (uždaviniai 4, 5, 6, 9 ir 10) turi didelę tikimybę būti teisingi, o keli kiti vis dar peržiūrimi. Iš pradžių manėme, kad mūsų bandymas spręsti 2 uždavinį greičiausiai buvo teisingas. Remdamiesi oficialiu „First Proof“ komentaru ir tolesne bendruomenės analize, dabar manome, kad tai yra neteisinga. Esame dėkingi už įsitraukimą ir tikimės toliau tęsti peržiūrą. Visą mūsų įrodymų bandymų rinkinį rasite čia(atsidaro naujame lange). Išankstinis leidinys apima visus dešimt įrodymo bandymų ir naujai pridėtą priedą su užklausų šablonais bei pavyzdžiais, kurie siekia imituoti mūsų rankines sąveikas su modeliais proceso metu.
Manome, kad nauji priešakiniai tyrimai yra bene svarbiausias būdas įvertinti naujos kartos dirbtinio intelekto modelių galimybes. Lyginamieji testai yra naudingi, tačiau jie gali praleisti kai kurias sudėtingiausias tyrimų dalis: ilgų protavimo grandinių palaikymą, tinkamų abstrakcijų pasirinkimą, dviprasmybių valdymą problemų formuluotėse ir argumentų, kurie atlaiko ekspertų patikrą, pateikimą. Tokie priešakiniai iššūkiai kaip „First Proof“ padeda mums išbandyti tas galimybes nepalankiomis sąlygomis, kai teisingumo patikrinimas nėra trivialus, o gedimų režimai yra informatyvūs.
„Šiuo metu apmokome naują modelį, kurio pagrindinis tikslas – didinti mąstymo tikslumą, siekiant, kad modelis galėtų nuolat mąstyti daugelį valandų ir išlikti labai užtikrintas savo išvadomis.“ Kai buvo paskelbtos „First Proof“ problemos, tai atrodė kaip tobula bandymų platforma, todėl savaitgalį ją išbandžiau. Jau pavyko išspręsti dvi problemas (Nr. 9 ir Nr. 10). Treniruodamasis jis tapo vis pajėgesnis ir galiausiai, mūsų vertinimu, išsprendė dar bent tris problemas. Ypač džiaugėmės, kai buvo išspręsta 6-oji problema, o po dviejų dienų – ir 4-oji, nes šios problemos buvo iš daugeliui iš mūsų pažįstamų sričių. „Smagu stebėti, kaip modelis kasdien tampa vis protingesnis.“
– James R. Lee (OpenAI tyrėjas, protavimo sritis)
Modelį vykdėme su ribota žmonių priežiūra. Mokymo metu siūlydami naudoti tam tikras modelio versijas, kartais siūlydavome iš naujo išbandyti strategijas, kurios ankstesniuose bandymuose pasirodė veiksmingos. Kai kurių bandymų metu, gavę ekspertų atsiliepimus, paprašėme modelio išplėsti arba patikslinti kai kurias įrodymo dalis, kad būtų lengviau patikrinti protavimą. Taip pat palengvinome šio modelio ir „ChatGPT“ tarpusavio sąveiką patvirtinimo, formatavimo ir stiliaus klausimais. Kai kuriems uždaviniams pateikiame geriausius iš kelių bandymų, atrinktų žmogaus sprendimu. Tai buvo greitas sprintas, ir mūsų procesas nebuvo toks tvarkingas, kaip norėtume tinkamai kontroliuojamame vertinime. Nekantriai laukiame diskusijų su „First Proof“ organizatoriais apie griežtesnę eksperimentų ir vertinimo sistemą būsimoms iteracijoms.
Šis darbas remiasi ankstesniais priešakinių protavimo modelių matematikos ir mokslo srityse rezultatais. 2025 m. liepą tarptautinėje matematikos olimpiadoje su bendrosios paskirties protavimo modeliu pasiekėme aukso medalio lygio pasiekimą(atsidaro naujame lange) (35/42 taškai). 2025 m. lapkritį pasidalinome atvejų analizėmis „Ankstyvieji mokslo spartinimo naudojant GPT‑5 eksperimentai“, kuriose GPT‑5 padėjo tyrėjams pasiekti konkrečios pažangos matematikos, fizikos, biologijos ir kitose srityse, kartu su pastebėtais apribojimais. O visai neseniai pranešėme apie fizikos bendradarbiavimą, kuriame GPT‑5.2 pasiūlė kandidatinę gliuono amplitudės formulės išraišką, kurią vėliau formaliai įrodė vidinis modelis ir patvirtino autoriai.
Laukiame glaudesnio bendradarbiavimo su bendruomene, kaip vertinti mokslinio lygio protavimus, įskaitant ekspertų atsiliepimus apie šiuos bandymus, ir džiaugiamės galėdami šias naujas galimybes pateikti būsimuose viešuosiuose modeliuose.
Autorius
Skaityti toliau
