Amikor az OpenAI ezen a héten több száz, állítólag nehéz matematikai problémát megoldó kéziratot tett közzé, a labor azt közölte, hogy egy neves matematikusokból álló tanácsadó testülettel konzultált, hogy elkerülje az előző, vitákat kiváltó esetekhez hasonló problémákat. A valóság azonban rávilágított hiányosságokra: a tanácsadók különösen hangsúlyozták, hogy matematikai eredmények esetén elengedhetetlen az emberi megértés, és ebben az értelemben az OpenAI közzétételei nem minden tekintetben feleltek meg az ajánlásoknak.
AGMAI ajánlásai és az OpenAI közzététele
Az Advisory Group on Mathematics and Artificial Intelligence (AGMAI), amelyet a Princeton University Institute for Advanced Study házigazdálkodik, kilenc elismert kutatóból áll különböző intézményekből. A szervezet szeptember végén publikált iránymutatásokat arra vonatkozóan, hogyan kellene a frontier laboroknak matematikai problémákat kezelniük. Az AGMAI közleményében a most közzétett bizonyításcsomagról azt állította, hogy „végső soron a matematikai közösség feladata megítélni, mennyire követték sikeresen az ajánlásainkat.”
Az AGMAI első kérése egyértelmű volt: „fejezzék be a fejlett matematikai problémák tesztelését zárt forrású (proprietary) modelleken.” Az OpenAI közzétételében azonban egyértelműen szerepel, hogy a labor zárt forrású modelljeit nyílt kutatási problémákon értékeli.
Mennyiségi adatok: 719 kézirat, kevés láncolt gondolat és részleges formalizáció
OpenAI összesen 719 kéziratot tett közzé. Bár a labor több AGMAI-elv érvényesítését is jelezte — például az eredmények mielőbbi publikálását és információk megosztását arról, hogyan jutottak a modellek a következtetésekhez — a gyakorlati teljesítés hiányos volt. Csak 10 a 719 kéziratból tartalmazott a modell „chain of thought” (láncolt gondolat) jellegű feljegyzéseket.
A matematikusok azt javasolták, hogy az ember számára nem egyértelmű bizonyításokat formalizálni kellene géppel ellenőrizhető formába. Az OpenAI által közzétett bizonyítások 42%-a azonban még nem esett át ezen a formalizációs folyamaton, azaz a kiadott anyagok közel felénél hiányzott a teljes, formális ellenőrzés.
„Elveszve a fordításban”: a formalizáció és a természetes nyelv közötti eltérések
A problémát jól illusztrálja egy ezen a héten megjelent tanulmány a University of Cambridge és a King’s College London kutatóitól, amely megkérdőjelezi, hogyan közelítik meg a frontier laborok ezeket a feladatokat. Amikor a modellek matematikai problémát oldanak meg, először természetes nyelvű (NL) magyarázatot hoznak létre, majd ezt próbálják Lean nevű formális nyelven kifejezni — amelyben elvileg kódra fordítással ellenőrizhető a bizonyítás.
A tanulmány dokumentált legalább két eltérést az OpenAI által adott NL-bizonyítás és a hozzá tartozó Lean-kód között egy, a Navier–Stokes-egyenletekből származtatott feladat megoldásánál. Ezek az eltérések önmagukban nem cáfolják egyik változatot sem, de komoly kétségeket vetnek fel azzal kapcsolatban, hogy a modellek megbízhatóan képesek-e autonóm módon lefordítani az NL-bizonyításokat formális, gép által ellenőrzött bizonyításokká emberi közreműködés nélkül.
Hiányzó géppel olvasható metaadatok és a felülvizsgálat szükségessége
Az AGMAI arra kérte az OpenAI-t, hogy „tartalmazzanak géppel olvasható metaadatokat, amelyek összekapcsolják a természetes nyelvű és a formális artefaktumokat”. Ezt a lépést az OpenAI nem valósította meg a most közzétett anyagokkal.
A Cambridge–King’s paper — amelyet a szerzők „lost in translation” címmel zártak — arra figyelmeztet, hogy az NL-bizonyítások és az automatikusan formalizált Lean-bizonyítások nem tekinthetők automatikusan megbízhatónak a hagyományos, emberi peer review és ellenőrzési folyamat nélkül.
Az emberi felelősség és a közösségi részvétel hiánya
A matematikusok hangsúlyozzák, hogy amikor új eredményeket emberek fedeznek fel, maguk vállalják a felelősséget azokért és kommunikálnak a szélesebb közösséggel – publikációk, előadások, szemináriumok révén. Ez a folyamat növeli az érthetőséget, lehetővé teszi az eredmények más problémák megoldására való alkalmazását, és gyakorlati területeken hasznosuló tudást hoz létre.
Terence Tao, aki korábban kritikát fogalmazott meg az OpenAI megközelítése kapcsán, közösségi médiában azt írta: „A problémákat olyan AI prompterek oldják meg autonóm módon, akiknek nincs érdekeltségük a szélesebb terület iránt, miután kezdeti céljuk teljesült, és nem értik elég jól az AI kimenetét ahhoz, hogy kérdésekre válaszoljanak, előadásokat tartsanak vagy interakciót folytassanak a többi kutatóval.”
Harvard University matematikaprofesszora, Melanie Wood a TechCrunchnak azt nyilatkozta, hogy amikor egy modellt kéri fel egy nehéz problémára és az „kiböki” a megoldást, akkor a közzététel pillanatában nincs emberi megértés a megoldás mögött — és innentől kezdődik a valódi munka, hogy az emberi szakértők megértsék és érvényesítsék az eredményeket.
Következmények és javaslatok
A jelen helyzet arra utal, hogy bár az AI modellek képesek összetett, előremutató javaslatok megfogalmazására matematikai problémákban, a közösség bizalma és a tudományos elfogadás szempontjából kulcsfontosságú a formalizáció, a transzparencia (például láncolt gondolatok és metaadatok közlése) és az, hogy emberi matematikusok vállaljanak felelősséget az eredmények megértéséért.
Az AGMAI javasolta, hogy az OpenAI finanszírozza azoknak a matematikusoknak a munkáját, akik szükségesek ahhoz, hogy a labor megoldásai valós, emberi megértést és hasznot eredményezzenek. A mostani közzététel azt mutatja, hogy a technológia ígérete és a gyakorlati követelmények között még jelentős szakadék van — különösen, ha a formális és informális bizonyítások között eltérések merülnek fel.
A további vita és értékelés a matematikai közösségre vár: az AGMAI és független kutatók feladata most, hogy a közzétett anyagokat átvilágítsák, és eldöntsék, mennyire szolgálják ezek a közzétételek a tudományos előrehaladást.
