Az OpenAI most nem egy új benchmarkpontszámmal próbálja megmutatni, mire képes a következő modellje. Az augusztus 1-jén közzétett anyagban tíz, régóta nyitott matematikai és elméleti informatikai problémára mutat be új eredményt. A munkát az Astra nevű belső rendszer végezte, amelyet a cég a következő nagy modelljeként említ.
A bejelentés első olvasásra olyan, mintha valaki tíz tudományos áttörést tett volna le egyetlen reggel az asztalra. Ezzel azért érdemes óvatosan bánni. A 249 oldalas tanulmány és a formális bizonyítások nyilvánosak, de a matematikai közösség független ellenőrzése most kezdődhet el. Az OpenAI állítása komoly, az elfogadása nem automatikus.
Tíz probléma, amelyek legalább egy évtizede nem mozdultak
Az OpenAI olyan feladatokat válogatott össze, amelyek fő eredményében legalább tíz éve nem történt előrelépés, több esetben pedig sokkal régebb óta állt a kérdés. A lista a nagy dimenziós gömbpakolástól a kódoláselméleten és csoportelméleten át a kvantumos komplexitásig ér. Kriptográfiai szempontból is érdekes eredmény született a legközelebbi vektor problémájának közelítési nehézségéről.
A látványosabb állítások közé tartozik egy nem-szofikus csoport explicit megadása, a Connes-féle merevségi sejtés cáfolata, valamint három Erdős-problémához kapcsolódó eredmény. A gömbpakolási fejezet a tanulmány szerint 1978 óta az első javulást adja az általános, nagy dimenziós felső korlátra. Ezek külön-külön is teljes kutatási cikket érnének, itt viszont egyetlen csomagban jelentek meg.
Astra még nincs a felhasználóknál
Az Astra nem egy ma kipróbálható ChatGPT-modell. Az OpenAI belső változatként ír róla, megjelenési dátumot, API-hozzáférést és részletes képességtáblázatot nem közölt. A matematikai eredmények ezért egyszerre kutatási bemutatók és előzetesek: azt mutatják, milyen feladatokra szánja a cég a következő modellcsaládot.
A megoldások megtalálása után emberek dolgozták fel az érveket a modell segítségével, majd az Astra minden bizonyításhoz Lean-tanúsítványt készített. A nyilvános GitHub-tárolóban külön fájlok és ellenőrzési beállítások tartoznak a tételekhez. A cég emellett minden eredményhez kiadott egy, a modell által készített gondolatmenet-narrációt is.
A Lean sok hibát kiszűr, de nem helyettesíti a szakmai vitát
A Lean egy formális bizonyításellenőrző rendszer. Ha a tételt és a szükséges feltételeket helyesen fogalmazták meg, a gép lépésről lépésre ellenőrzi, hogy a következtetés valóban levezethető-e. Ez sokkal erősebb biztosíték annál, mintha egy nyelvi modell egyszerűen leírná, hogy szerinte kész a bizonyítás.
A tanúsítvány mégsem pecsételi le egy csapásra a teljes tudományos állítást. A matematikusoknak ellenőrizniük kell, hogy a formalizált tétel pontosan ugyanazt mondja-e, mint az eredeti nyitott probléma, nincsenek-e túl erős feltételezések, és valóban új-e az alkalmazott módszer. A 249 oldalnyi anyag értékelése nem fog egy hétvége alatt lezajlani.
Az OpenAI maga is szokatlanul egyenesen fogalmaz a szerzőségről. A matematikai érveket a rendszer hozta létre, ezért a cég szerint félrevezető lenne ezeket hagyományos emberi szerzőségként feltüntetni. Az emberek a kéziratok elkészítésében, a formalizálásban és az ellenőrzésben vettek részt, az eredmények helyességéért pedig az OpenAI vállal felelősséget.
A kétezer dolláros számból nem derül ki minden
A vállalat becslése szerint a megoldások megtalálásához szükséges tokenmennyiség nagyjából 2000 dollárba kerülne a Sol API árazásával. Ez meghökkentően alacsonynak hangzik tíz kutatási eredményért. A szám azonban nem tartalmaz világos bontást arról, hány sikertelen próbálkozás, emberi probléma-előkészítés és utólagos ellenőrzés állt a kiválasztott eredmények mögött.
A kiválasztás módja legalább ennyire fontos. Tíz sikerből nem tudjuk meg, hány olyan nyitott problémát kapott az Astra, amelynél nem jutott használható eredményre. Egy kutatási eszköznél a találati arány számít: ha száz próbából tízszer működik, az már hasznos lehet, de egészen más képet ad, mint ha minden második feladatot megold. Ezt a nevezőt az OpenAI most nem közölte.
Az sem látszik még, mennyire függött a teljesítmény a gondosan megírt utasításoktól és a feladatokhoz adott szakirodalomtól. Egy matematikus kezében a modell lehet kiváló ötletgenerátor akkor is, ha önállóan nem tudna végigvinni egy kutatási programot. A mostani bemutató ezt a különbséget nem méri, mert kész eredményeket mutat, nem dokumentált vaktesztet.
Astra valódi erejét ezért nem az dönti el, hogy az OpenAI hány problémát sorolt fel a bemutatóban. Az lesz érdekes, hogy független matematikusok mit találnak a bizonyításokban, más kutatócsoportok meg tudják-e ismételni a munkát, és a modell képes-e hasonló eredményt elérni olyan feladaton is, amelyet nem a saját fejlesztői választottak ki. Most először viszont van mit ellenőrizni: a tanulmány, a formalizált kód és a tíz konkrét állítás egyaránt nyilvános.
