OpenAI zverejnil desať matematických výsledkov vytvorených modelom Astra

OpenAI oznámil súbor desiatich nových výsledkov z matematiky a teoretickej informatiky, ktoré podľa firmy vytvorila interná verzia pripravovaného modelu Astra. Témy siahajú od geometrie vo vysokých dimenziách a teórie kódov cez grupy a operátorové algebry až po kvantovú zložitosť, mriežkovú kryptografiu a extrémnu kombinatoriku. Nejde teda o jeden efektný výpočet ani o riešenie školskej úlohy, ale o pokus ukázať AI ako aktívny nástroj pri výskume problémov, pri ktorých sa hlavný výsledok najmenej desať rokov neposunul. OpenAI zároveň zverejnil formálne certifikáty v dôkazovom asistente Lean, aby sa tvrdenia dali kontrolovať presnejšie než iba čítaním prirodzeného jazyka.

Najvýraznejšia časť oznámenia je rozsah výsledkov. OpenAI uvádza nové horné hranice pre hustotu ukladania gúľ vo vysokých dimenziách, exponenciálne lepšie hranice pre binárne a sférické kódy, konštrukciu nesofickej grupy a vyvrátenie Connesovej hypotézy o rigidite. Ďalšie výsledky sa týkajú dolných hraníc aritmetických obvodov pre výpočet permanentu, paralelného opakovania kvantových hier, náročnosti aproximácie problému najbližšieho vektora, Ehrhartovej hypotézy o objeme, viacfarebných Ramseyho čísel a dvoch hypotéz z extrémnej teórie grafov. Každá z týchto oblastí má vlastné kritériá významu, preto spoločný zoznam nemožno čítať ako jednoduchý rebríček desiatich rovnako veľkých objavov.

Podstatný je aj opísaný pracovný postup. Matematické argumenty mal vytvoriť model, ľudia ich následne s pomocou toho istého systému pripravili do podoby rukopisov a model potom formalizoval dôkazy v jazyku Lean. Firma odhaduje, že počet tokenov potrebných na hľadanie riešení by pri cenách rozhrania Sol API stál približne dvetisíc dolárov. Tento údaj nie je meraním celkových nákladov výskumu: nezahŕňa vývoj a trénovanie modelu, prácu výskumníkov ani nezávislé posudzovanie. Napriek tomu naznačuje, že po vybudovaní schopného systému môže byť samotné skúšanie veľkého množstva matematických ciest relatívne lacné.

Formálne certifikáty sú dôležité, pretože dôkazový asistent nekontroluje presvedčivosť štýlu, ale to, či jednotlivé kroky vyplývajú z presne zadaných pravidiel a predpokladov. Verejný repozitár openai/ten-proofs obsahuje súbory v jazyku Lean pre jednotlivé tvrdenia, napríklad pre balenie gúľ, nesofické grupy, Ramseyho čísla, permanent či kvantové paralelné opakovanie. To výrazne zvyšuje auditovateľnosť oproti situácii, keď firma zverejní iba zhrnutie odpovede modelu. Formálna kontrola však sama osebe nezaručuje, že formalizovaná veta presne zachytáva pôvodnú otvorenú otázku, že predpoklady sú matematicky prirodzené alebo že výsledok má deklarovaný dosah. Aj tieto väzby musia preveriť odborníci.

Z pohľadu vedeckej metódy preto treba oddeliť tri úrovne istoty. Overiteľným faktom je, že OpenAI zverejnil konkrétny zoznam tvrdení a zdrojový kód certifikátov. Tvrdenie firmy, že problémy vyriešila interná Astra, je prvotná správa autora systému a ešte nie všeobecne prijatý konsenzus matematickej komunity. A význam každého výsledku sa ukáže až po kontrole rukopisov, reprodukcii formalizácie, porovnaní s literatúrou a prípadných opravách. Pri desiatich náročných oblastiach bude tento proces trvať dlhšie než mediálne oznámenie a môže priniesť rozdielne verdikty pre jednotlivé práce.

Pre kryptografiu a teoretickú informatiku sú zaujímavé najmä výsledky o probléme najbližšieho vektora a o zložitosti obvodov. Problémy na mriežkach tvoria dôležitý základ postkvantovej kryptografie, ale nový teoretický výsledok automaticky neznamená prelomenie konkrétnych používaných schém. Je potrebné presne skúmať, aký model výpočtu, aproximačný faktor a redukciu výsledok používa. Podobne dolná hranica pre permanent môže byť zásadná v aritmetickej zložitosti bez toho, aby okamžite zmenila výkon bežného softvéru. Praktický dopad tu vedie cez lepšie pochopenie hraníc algoritmov, nie cez okamžitú aktualizáciu produktu.

Oznámenie tiež posúva diskusiu o tom, komu patrí vedecké autorstvo. OpenAI výslovne tvrdí, že označiť úplne strojovo vytvorený argument za ľudské dielo by skresľovalo spôsob jeho vzniku. Firma pripisuje ľuďom prípravu rukopisov, formalizáciu a zodpovednosť za správnosť, samotné matematické argumenty však pripisuje systému. Takéto rozdelenie bude musieť v praxi doplniť jasná dokumentácia verzií modelu, promptov, výberu pokusov, zásahov človeka a neúspešných ciest. Bez nej bude ťažké reprodukovať nielen finálny dôkaz, ale aj proces, ktorý k nemu viedol.

Verejné zverejnenie certifikátov je preto silnejší krok než ukážka uzavretého benchmarku, no stále nejde o úplne otvorený experiment. Astra nie je verejne dostupný model a externé tímy nemôžu zopakovať hľadanie riešení za rovnakých podmienok. Môžu však auditovať výstupy, spustiť Lean kód a hľadať chyby v preklade medzi neformálnou a formálnou vetou. Pre vedecké inštitúcie to vytvára nový typ recenznej práce: okrem matematického obsahu bude treba kontrolovať pôvod výstupu, kvalitu formalizácie a mieru ľudského výberu.

Ak výsledky prejdú nezávislou kontrolou, najväčší dopad nemusí byť v jedinom rekordnom dôkaze, ale v zmene ekonomiky teoretického výskumu. Model schopný paralelne skúšať veľa nápadov, prepájať vzdialené oblasti a následne vytvoriť strojovo kontrolovateľný certifikát by mohol urýchliť fázu hľadania hypotéz aj overovania detailov. Úlohou matematikov by zostalo formulovať plodné otázky, rozpoznávať zmysluplné argumenty, vysvetľovať ich kontext a rozhodovať, ktoré výsledky sú skutočne dôležité. Takýto nástroj by teda skôr menil rozdelenie práce než odstraňoval potrebu odborníkov.

Najbližšie týždne ukážu, či sa zverejnené rukopisy stanú potvrdenými príspevkami alebo súborom tvrdení, ktoré bude treba upraviť. Pozitívnym signálom je, že firma poskytla konkrétne artefakty na kontrolu namiesto samotných marketingových výsledkov. Rozhodujúci verdikt však nepatrí OpenAI ani modelu Astra, ale otvorenému procesu matematickej recenzie. Pre vývoj AI je už teraz podstatné, že latka sa posúva od odpovedí na známe úlohy k návrhu nových argumentov s formálnou stopou, ktorú možno technicky preverovať.