Matematika je pro AI zvláštně přitažlivé hřiště: odpověď buď drží pohromadě, nebo ne, a sebevědomě znějící odstavec to nezachrání. OpenAI teď zveřejnilo výsledky svého interního frontier modelu na otevřených matematických problémech a přidalo i materiály, které mě zaujaly možná ještě víc než samotný slibný výsledek.
Nejde jen o vyřešený příklad
OpenAI mluví o nových výsledcích na open problems, tedy problémech, které dosud nemají obecně známé vyřešení. Podklad ale neupřesňuje, které konkrétní problémy model řešil ani jaký přesně byl jeho přínos. Nechci tedy předstírat, že máme v ruce seznam matematických záhad odškrtnutých umělou inteligencí. Nemáme.
Samotný fakt, že firma výsledky sdílí jako výzkumnou práci a ne jen jako ukázku „model umí olympiádní úlohy“, je ale podstatný. Úspěch na známých testech může znamenat dobrou paměť, šikovné hledání vzorů i skutečné uvažování v různém poměru. U otevřeného problému je laťka přece jen nepříjemněji vysoko. A matematika umí být nepříjemná i bez asistence GPU.
Lean je zde důležitější než hezký příběh
Součástí zveřejnění jsou formalizace důkazů v systému Lean a další výzkumné podklady na GitHubu. Lean je nástroj pro formální ověřování matematiky: důkaz se zapisuje tak přesně, aby jeho jednotlivé kroky mohl zkontrolovat počítač.
To neznamená, že počítač automaticky posoudí význam celé matematické myšlenky. Kontroluje ale, zda formálně zapsaný důkaz opravdu navazuje krok za krokem. Mně osobně to přijde jako správný směr. U tvrzení o schopnostech jazykových modelů je snadné nechat se unést elegantním vysvětlením; zveřejněný artefakt, který lze spustit a kontrolovat, je mnohem méně romantický, ale o dost užitečnější.
Otevřené sdílení neznamená, že každý zájemce bude zítra číst Lean kód u snídaně. Já bych na to nejspíš potřebovala druhou snídani a několik tutoriálů. Umožňuje však matematikům a lidem z formálních metod ověřit práci vlastním postupem, místo aby se spoléhali jen na interpretaci firmy.
Interní frontier model nechává dost otazníků
Výsledky pocházejí z interního frontier modelu, tedy z modelu na špičce schopností OpenAI. Z podkladu ale neplyne jeho název, dostupnost ani to, zda se tyto matematické schopnosti objeví v nějakém veřejném produktu. Stejně tak nevíme, jak velkou část práce odvedl model samostatně, jakou roli měli lidští výzkumníci a kolik pokusů vedlo k použitelnému výsledku.
To nejsou drobné účetní detaily. Rozdíl mezi „model navrhl zajímavý směr, který lidé dopracovali“ a „model vytvořil a formalizoval důkaz s minimální pomocí“ je obrovský. Obě varianty mohou být vědecky cenné, jen říkají něco jiného o tom, co AI skutečně umí.
Proč mi to stojí za pozornost
Nejsilnější část celé zprávy pro mě není představa AI, která zavře všechny učebnice matematiky a jde domů. Je to spojení objevování a ověřování. Jazykové modely umějí generovat hypotézy, postupy i omyly rychlostí, ze které se mi trochu motá hlava. Formální důkazy dávají šanci oddělit nápad od tvrzení, jež se dá opravdu prověřit.
Teď bude zajímavé sledovat, co z materiálů vytěží odborná komunita. Pokud se ukáže, že výsledky obstojí a postup půjde opakovat, nepůjde jen o další tabulku benchmarků, ale o užitečný příklad spolupráce modelů, matematiků a ověřovacích nástrojů. A to je typ pokroku, který se mi věří lépe než samotnému velkému číslu v prezentaci.
OpenAI tentokrát alespoň nesdílí pouze závěr, ale i část cesty k němu. U matematiky je to přesně ta část, která rozhoduje.
