Az OpenAI Astra modellje tíz évtizedes matematikai problémát oldott meg

Az OpenAI nem a megszokott termékbemutatóval jelentette be a következő nagy modelljét. Ehelyett augusztus 1-jén tíz megoldott matematikai problémát tett közzé, és ezekkel adott nevet az új modellcsaládjának: Astra. A cég szerint a modell egy belső verziója tíz olyan eredményt ért el a matematika és az elméleti számítástudomány területén, amelyek mindegyike legalább egy évtizede nyitott kérdés volt.

A bejelentéshez egy 249 oldalas kéziratgyűjtemény és – ami ennél is fontosabb – minden egyes eredményhez egy géppel ellenőrizhető Lean 4 bizonyítási tanúsítvány tartozik, amely nyilvánosan elérhető a GitHubon, Apache 2.0 licenc alatt.

A kódtár „sorry” számlálója nullán áll, ami azt jelenti, hogy mind a tíz formalizált bizonyítás minden egyes lépését hiánytalanul ellenőrizte a rendszer.

Mit oldott meg pontosan az Astra?

A legnagyobb visszhangot kiváltó eredmény egy nem szofikus csoport első explicit megszerkesztése. Ez a kérdés a csoportelmélet egyik központi nyitott problémája volt azóta, hogy Mihail Gromov 1999-ben bevezette a szoficitás fogalmát – 27 éven át egyetlen matematikusnak sem sikerült bizonyítania vagy cáfolnia a létezését.

A többi eredmény több területet is lefed. Az Astra:

• cáfolta Connes merevségi sejtését a Neumann-algebrákra vonatkozóan,
• bizonyította Ehrhart térfogatsejtését,
• megoldott három problémát Paul Erdős híres listájáról – köztük a 183. számút a többszínű Ramsey-számokról,
• 1978 óta először javította a magas dimenziójú gömbpakolási sűrűség általános felső korlátját,
• bizonyított egy párhuzamos ismétlési tételt kétszemélyes kvantumjátékokra,
• új alsó korlátokat állapított meg a permanens kiszámításának áramkör-komplexitására.

Az OpenAI matematikai kutatásokért felelős vezetője, Sébastien Bubeck az X-en erősítette meg az eredményeket. A teljes számítási költség mind a tíz megoldásra nagyjából 2000 dollár volt a cég Sol API-jának árai alapján.

„Gyönyörűnek nevezte azokat.”

Miért más ez, mint a korábbi bejelentések?

A Lean-tanúsítványok egy olyan kifogásra válaszolnak, amelyet a matematikai közösség régóta hangoztat a mesterséges intelligencia által generált bizonyításokkal kapcsolatban: hogy nehéz azokat függetlenül ellenőrizni. A géppel ellenőrizhető bizonyítást bárki érvényesítheti, akinek van Lean-fordítója – anélkül, hogy meg kellene bíznia a modellben vagy annak üzemeltetőjében. A hagyományos, hónapokig tartó szakértői lektorálás így a letöltés idejére zsugorodik: a verifikáció és a publikálás ugyanazon a napon megtörténik.

Fontos árnyalat ugyanakkor, hogy a Clay Matematikai Intézet hét, egyenként egymillió dolláros Millenniumi díjas problémája közül egyik sem dőlt meg. A megoldott feladatok valódi nyitott problémák, de nem a legnehezebbek közül valók. A modell által adott matematikai tartalmat emberi kutatók dolgozták fel publikálható kéziratokká.

Az Anthropic gyors ellenpontja

A bejelentés után 24 órán belül érkezett a hidegzuhany: az Anthropic egyik kutatója, Levent Alpoge azt állította, hogy a Fable modell segítségével – egy általános prompttal és internet-hozzáférés nélkül – a tíz bizonyításból ötöt reprodukálni tudott. Ez felveti a kérdést, hogy a publikált eredmények mennyire válogatottak, illetve hogy az OpenAI vajon hány sikertelen próbálkozást hagyott ki a 2000 dolláros költségszámításból (amely csak a sikeres futásokat fedi le).

Feszültség a matematikai közösséggel

A bejelentés az AI-cégek és a matematikai közösség közötti fokozódó feszültség árnyékában érkezett. Júniusban a matematikusok kiadták a Leideni Nyilatkozatot, amelyet a Nemzetközi Matematikai Unió is támogatott, és amely arra figyelmeztet, hogy az AI-cégek beleegyezés nélkül használnak publikált kutatásokat, megkerülik a szakértői lektorálást, és veszélyeztetik a bizonyítás és a hivatkozás integritását. A nyilatkozat kifejezetten megnevezte azokat a cégeket, amelyek sajtóközleményeken keresztül – nem pedig lektorált folyóiratokban – jelentik be eredményeiket.

Mi várható az Astra körül?

Az OpenAI nem közölte, mikor adja ki nyilvánosan az Astrát, csak a „következő nagy modelljeként” hivatkozik rá. Egyes megfigyelők, köztük Mark Kretschmann befektető, azt találgatják, hogy az Astra valójában a GPT-6 sorozat része. A cég emellett 100 000 akadémiai kutatónak ad ingyenes hozzáférést az élvonalbeli (frontier) modelljeihez 2027-ig – ez a lépés mélyíti a tudományos közösséggel való kapcsolatát, ugyanakkor a saját platformjára koncentrálja a kutatási infrastruktúrát.

Az, hogy a tágabb matematikai közösség elfogadja-e a blogbejegyzésben, nem pedig lektorált folyóiratban bejelentett eredményeket, egyelőre nyitott kérdés marad – pontosan az a kérdés, amelynek megválaszolására a Leideni Nyilatkozat született.