Kutatás
Gépi ellenőrzés és nyílt tárhely: az OpenAI közzéteszi matematikai eredményeit
Az OpenAI széles körű új matematikai eredményeket tesz közzé, amelyeket egy belső, még ki nem adott csúcsmodell állított elő. A cég egy független tanácsadó testület ajánlásai alapján döntött a közzététel módjáról, és sok bizonyítást gépileg ellenőrizhető formában is mellékel.
Az eredmények egy GitHub-tárolóba kerülnek, a cikkek revíziójára és a hivatkozásokra vonatkozó protokollal együtt. A cég közösségi üzemeltetésű alternatívákat is vizsgál. A tároló összefoglalja a modell gondolatmenetét, és statisztikát közöl arról, hány problémával próbálkozott, ami segíthet felmérni, hogy a sikeres eredmények mekkora részét teszik ki az összes kísérletnek.
Bizonyítások, amelyeket gép ellenőriz
Sok bizonyításhoz Lean-formalizálást is mellékelnek, és a tárolót további formalizálásokkal frissítik majd. A Lean egy programozási nyelv és bizonyításellenőrző rendszer, amelyben a matematikai levezetéseket a számítógép lépésről lépésre ellenőrzi. Ha egy bizonyítás átmegy ezen az ellenőrzésen, akkor logikailag hibátlan, így nem kell pusztán a modell vagy a cég szavára hagyatkozni.
Ez az AI által generált matematikánál különösen fontos. A nyelvi modellek hajlamosak meggyőzően hangzó, de hibás érveléseket előállítani, amelyeket egy gyors olvasás során nehéz észrevenni. A gépi ellenőrzés kiszűri az ilyen hibákat, és ezzel jelentősen növeli az eredmények hitelességét a matematikus közösség szemében.
A tároló a felhasznált számítási kapacitásra is becslést ad. Az OpenAI szerint egy átlagos eredmény nagyjából háromórányi ChatGPT Pro-„gondolkodásnak” megfelelő számítást igényelt. A számítási költség közlése azért lényeges, mert reálisabb képet ad arról, mennyi erőforrás kell egy-egy eredményhez, és így arról is, mennyire hatékony a módszer.
Ami még hiányzik a bejelentésből
A bejelentés nem részletezi, pontosan mely problémákról és hány eredményről van szó, és független matematikusi értékelés sem ismert még. Az sem derül ki, melyik belső modellről van szó, és mikor adják ki. A közzététel pontos dátuma és a GitHub-tároló linkje sem szerepelt a beszámolóban, ahogy az sem, a bizonyítások mekkora része kapott Lean-formalizálást.
Az OpenAI workshopokat, konferenciákat és speciális programokat finanszíroz az AI által elért nagy eredmények megértésére, és a modell felelős kiadásán dolgozik. A hír az AI-cégek matematikai kutatási versenyének része, amelyben az átláthatóság, a gépi ellenőrzés és a számítási költség közlése egyre fontosabb hitelességi szempont lesz.