OpenAI zveřejnila 722 matematických rukopisů, ověřování teprve začíná

OpenAI zveřejnila katalog 722 matematických rukopisů rozdělených do 372 rodin výsledků. Vznikly při evaluaci interního, dosud nevydaného modelu na přibližně 4 000 otevřených problémech. Firma uvádí, že jeden výsledek spotřeboval v průměru 3 hodiny výpočetního času v režimu ChatGPT Pro thinking.

Místo jednoho triumfu přišel archiv o 722 položkách

Veřejný repozitář obsahuje rukopisy, zdrojové soubory, citační pokyny a podpůrné důkazní artefakty. Deset vybraných výsledků doprovázejí zkrácené souhrny postupu modelu. Oznámení OpenAI bylo při ověření blokované, proto se tento popis opírá o veřejný repozitář firmy a jeho dokumentaci.

Výsledky pokrývají různé fáze ověření. OpenAI výslovně píše, že ne všechny rukopisy mají formalizaci v Leanu a že neformalizované práce mohou obsahovat chyby. Repozitář má uchovávat i historii oprav a starší verze.

Matematici dostali katalog, ne hotový žebříček průlomů

Pro výzkumnou komunitu je podstatný hlavně nový problém měřítka. Ručně posoudit stovky rukopisů, jejich význam, originalitu a návaznost na literaturu bude stát výrazně víc odborného času než jejich strojové vytvoření. Samotný počet proto neříká, kolik výsledků obstojí.

Lean může ověřit formální správnost těch důkazů, které do něj byly převedeny. Neodpoví však sám na otázku, zda je výsledek nový, významný nebo už známý pod jiným názvem. OpenAI tak přesunula část evaluační práce z interního benchmarku na veřejnou matematickou komunitu.

Tři hodiny compute nenahrazují odbornou recenzi

Deklarovaný průměr tří hodin na výsledek popisuje cenu generování, nikoli cenu poznání. Do skutečného účtu patří kontrola předpokladů, dohledání priority, opravy rukopisů a čas expertů, kteří rozliší průlom od známé věty v novém balení.

Ani 57 328 souborů Lean v repozitáři neznamená 57 328 nezávisle ověřených objevů. Jde o součást rozsáhlé knihovny podpůrných artefaktů a OpenAI sama zdůrazňuje, že formalizace není úplná.

Rozhodnou nezávislé posudky a veřejná historie oprav

Nejdůležitějším signálem budou konkrétní rodiny výsledků, které nezávislí matematici uznají jako nové a správné. Stejně důležité bude, kolik rukopisů projde opravou, stažením nebo doplněním formalizace během dalších měsíců.

Repozitář slibuje zachovat starší verze. Pokud bude historie změn opravdu čitelná, půjde sledovat nejen výkon modelu, ale i cenu úklidu po masové produkci matematických tvrzení.

Lilithin verdikt

OpenAI vysypala před matematiky 722 rukopisů. Teď se ukáže, kolik z nich unese tabuli plnou cizích poznámek a kolik skončí pod červenou tužkou.