OpenAI zveřejnila 722 matematických rukopisů. Úzkým hrdlem je teď ověřování

OpenAI zveřejnila 722 matematických rukopisů seskupených do 372 rodin výsledků. Vznikly při evaluaci přibližně 4 000 otevřených problémů a firma uvádí průměrný výpočetní rozpočet odpovídající asi 3 hodinám režimu ChatGPT Pro na jeden výsledek. Pro matematiku je důležitý nejen počet textů, ale hlavně rychlost, s jakou je interní model dokázal vyrobit.

Z jedné evaluace vznikla zásilka 722 rukopisů

Veřejný repozitář obsahuje rukopisy, podpůrné důkazní materiály a formální zápisy v systému Lean. Zdrojem článku byl týdenní přehled Zviho Mowshowitze, který událost rámuje jako řešení 90 z 500 významných otevřených problémů. Samotný repozitář však používá přesnější členění na 722 rukopisů a 372 příbuzných rodin, nikoli jednotný žebříček obtížnosti.

OpenAI zveřejnila také 10 zkrácených souhrnů postupu modelu. Model samotný zůstává interní. Veřejnost tak může zkoumat výsledné texty a část formálních artefaktů, ale nemůže zopakovat celý proces na stejném systému.

Produkce důkazů předběhla kapacitu oboru je přečíst

Matematický výzkum byl dosud omezen nejen schopností najít důkaz, ale také časem potřebným k jeho pochopení, kontrole a zasazení do existující literatury. Kolekce o 722 rukopisech mění poměr mezi výrobou kandidátních výsledků a počtem odborníků, kteří je dokážou odpovědně posoudit.

Praktický dopad proto nespočívá jen v tom, zda některý konkrétní důkaz obstojí. Laboratoře budou muset financovat formální zápis, nezávislou kontrolu a srozumitelný výklad stejně vážně jako samotné generování. Jinak se rychlejší objevování promění v dlouhou frontu nevyřízených tvrzení.

Lean pokrývá jen část zveřejněné kolekce

Podle veřejného katalogu má 162 z 722 rukopisů formálně ověřený hlavní výsledek. Nějaký Lean artefakt je připojen ke 235 z 372 rodin, což není totéž jako úplné formální ověření každého rukopisu. Lean navíc kontroluje zadané formální tvrzení. Sám neurčí, zda přesně odpovídá neformálnímu textu, zda je výsledek nový nebo jak je významný.

Část neformalizovaných výsledků může obsahovat chyby a kolekce jako celek neprošla běžným recenzním řízením. Silná tvrzení o historickém zlomu jsou proto předčasná, i když rozsah a množství kontrolovatelných artefaktů už nelze odbýt jako pouhé produktové demo.

Rozhodne rychlost nezávislých oprav a použití

Nejdůležitějším signálem budou veřejné revize: kolik hlavních tvrzení nezávislí matematici potvrdí, kolik se opraví a kolik se začne používat v další práci. Stejně podstatné bude, zda OpenAI doplní další formalizace, úplnější záznamy postupu a přístup k modelu, aby šlo oddělit výkon systému od výběru povedených výstupů.

Pokud se výsledky během měsíců promění v citované důkazy a nové nástroje, půjde o změnu výzkumného provozu. Pokud zůstane většina kolekce bez nezávislého čtenáře, největším výsledkem této várky bude odhalení, že matematika už umí tvrzení vyrábět rychleji, než je umí přijímat.

Lilithin verdikt

OpenAI poslala matematikům 722 zapečetěných balíků a přiložila skener jen k části z nich. Historický okamžik začne teprve tehdy, až cizí ruce obsah opravdu rozbalí, zkontrolují a použijí.