A mesterséges intelligenciával foglalkozó startup Resolution (korábbi nevén Sequent) bejelentette, hogy automatikusan formalizálták Hironaka "resolution of singularities" (a szingularitások felbontása) tételét a Lean bizonyítás-asszisztensben. A formalizációs munka egy nagy, géppel előállított Lean-könyvtárat eredményezett, amelyet a csapat a statisztikai tanulás elméletéhez kötődő kérdések vizsgálatára használ: elsősorban a veszteségfelszín (loss landscape) geometriája és a generalizáció közti kapcsolatra vonatkozó kutatások elősegítésére.
Hogyan végezték el a formalizációt
A Resolution leírása szerint a folyamatot egy többlépcsős, ügynökalapú munkafolyamattal valósították meg. Egy kutató először két tervet dolgoztatott ki ügynökökkel: egy magas szintű, ember által értelmezhető verziót és egy részletes, 112 oldalas tervet, amely apró, atomikus lépésekre bontva követte a meglévő irodalmat. Ezután egy „orchestrator” ügynököt bízott meg a terv végrehajtásával; az orchestrator más ügynököket hozott létre, amelyek papíron végzett matematikai munkát végeztek, Lean-kódot írtak, és támogató feladatokat láttak el, például ellenőrizték, hogy a munkamenet a kitűzött célok felé halad-e.
A csapat beszámolója szerint a végrehajtási fázis viszonylag kevés manuális beavatkozást igényelt a kezdeti terven és az előző belső autoformalizációs munkákból leszűrt ügynök-képességeken túl. Ez mutatja, hogy a jól felépített, automatizált ügynökrendszerek képesek önállóan végrehajtani összetettebb formalizációs feladatokat.
Erőforrás-használat és kimenet
A projekt hozzávetőlegesen egy hétig tartott. A csapat adatai szerint a munkához nagyjából 100 milliárd bemeneti tokenre volt szükség (ennek mintegy 90%-a cache-olásból olvasás volt), illetve mintegy 300 millió kimeneti token keletkezett. A tokenek becsült költsége körülbelül 135 000 dollár volt. A formalizáció eredményeként mintegy 600 000 sor Lean-kód jött létre.
Milyen előnyöket hozott a formalizáció
Resolution szerint a létrehozott formalizált könyvtár lehetővé tette a csapat számára, hogy felgyorsítsa más, hozzá kapcsolódó kutatási irányok fejlesztését. Konkrétan a formalizált felbontás lehetővé teszi az elmélet további automatizálását, ami jobb megértést adhat a mintavétel (sampling) viselkedéséről; ez pedig közvetlenül kapcsolódik ahhoz, hogyan formálódnak a modellek tanulási folyamatai — amit a csapat „patterning”-nek nevez.
Miért számít ez a mesterséges intelligencia biztonsága szempontjából
Bár a csúcsmatematika sokszor távolinak tűnik a gyakorlati alkalmazásoktól, a Resolution beszámolója rávilágít arra, hogy az automatizált formalizációs technikák összekapcsolhatják az elméleti munkát az AI-fejlesztés gyakorlati szükségleteivel. A kulcs az, hogy a mesterséges intelligencia segítségével olyan korábban rendkívül költséges és embermunka-igényes feladatok válnak megvalósíthatóvá és ismételhetővé, amelyeket korábban kevesen végeztek el, és amelyek nehezen illeszthetők be egy startup kutatási ütemtervébe.
Resolution ezt az irányt azzal a jóslattal kommentálja, hogy a matematika „iparosodása” új, szigorú tudományt tehet lehetővé a kutatásautomatizálás területén — ami hosszabb távon hozzájárulhat az AI rendszerek viselkedésének pontosabb megértéséhez és biztonságosabb alakításához.
Következtetések
A Resolution esete szemlélteti, hogyan lehet a modern nagy nyelvi modelleket és ügynökrendszereket arra használni, hogy mély matematikai eredményeket formalizáljanak és integráljanak kutatási munkafolyamatokba. A bemutatott adatok — a nagyságrendekben mért tokenfelhasználás, a jelentős Lean-kód-mennyiség és az egyhetes végrehajtás — azt sugallják, hogy ez a megközelítés gazdaságilag és technikailag is életképes. Ha a folyamatok tovább fejlődnek, az automatizált matematika valóban új lehetőségeket teremthet az AI-biztonság és az alignment kutatásában.
