Matematici prověřují novost důkazů DeepMind

Matematický důkaz může být elegantní, a přesto v něm může zůstat mezera, kterou nikdo léta neodhalí. Agent AlphaProof Nexus od Google DeepMind vytvořil důkazy k devíti problémům Paula Erdőse a software ověřilo každý jejich krok. Výsledky se nejprve objevily v květnovém preprintu (arXiv) a po odborném recenzním řízení vyšly 8. října v časopise Science (Science). Počítač mohl potvrdit správnost postupu; zda důkazy přinesly něco nového, museli posoudit matematici.

Rozhodčí, na kterého styl neplatí

Chatboti dokážou formulovat matematická řešení, která znějí správně. Sebevědomý text může zakrýt chybějící krok a odhalí ho jen pozorný čtenář. AlphaProof Nexus se této pasti vyhýbá tím, že pracuje v jazyce Lean. Ten umožňuje zapisovat definice, tvrzení a důkazy tak přesně, aby každý krok mohl zkontrolovat počítač.

Lean funguje jako rozhodčí, který čte hotový důkaz řádek po řádku a řídí se pevnými pravidly. Na stylu nezáleží. Pokud některý krok nevyplývá z předchozích, důkaz neprojde, ať zbytek působí jakkoli elegantně.

Autoři popisují agenta jako systém, který hledá důkazy zapsané v jazyce Lean. Výzkumníci mu zpřístupnili také AlphaProof, starší systém DeepMind vyvinutý přímo pro dokazování. V jejich testech přineslo stejné výsledky i jednodušší řešení: jazykový model spojený s Leanem, bez AlphaProof, dokázal všech devět Erdősových problémů (The Decoder). U těchto úloh se tak specializovaný systém ukázal jako zbytečný.

Studie uvádí formálně ověřené důkazy k devíti Erdősovým tvrzením a ke 44 domněnkám z Online Encyclopedia of Integer Sequences, rozsáhlého katalogu číselných posloupností. Domněnky jsou tvrzení považovaná za pravdivá, která však dosud nikdo nedokázal (Science). Mezi Erdősovými úlohami je dvoudílná otázka o celých číslech, kterou Erdős a András Sárközy položili v roce 1970. Více než půl století zůstávala nevyřešená (ABC).

Co rozhodčí nevidí

Záruka Lean má přesně vymezený dosah: potvrzuje, že důkaz dokládá tvrzení tak, jak je zapsáno v kódu. Neodpovídá ale na tři otázky: zda zápis vystihuje, co Erdős zamýšlel, zda už někdo problém dávno vyřešil a zda řešení přináší nový poznatek.

Na problému z roku 1970 je vidět, proč záleží na posledních dvou otázkách. Druhá část úlohy implikuje první, takže jediný důkaz řeší obě. Když se důkazy agenta rozšířily, ukázalo se, že na obě části odpovídá také drobná úprava konstrukce z původního článku z roku 1970 (arXiv). Důkazy agenta byly správné. Úloha jen byla blíž vyřešení, než napovídalo její označení za otevřenou.

Podobné souvislosti dokážou zachytit lidé, kteří obor dobře znají. Gergely Bérczi, matematik z Aarhus University v Dánsku a jeden z autorů studie, pomáhal vybírat vhodné otázky a ověřovat řešení (Aarhus University). Pomáhal také sepsat verze důkazů, kterým porozumí lidský čtenář. Lean ručil za každý krok, zatímco Bérczi a jeho kolegové posuzovali, co z těchto kroků plyne.

Toto rozdělení práce odlišuje studii od vývoje z minulého měsíce. Tehdy Claude od Anthropic převedl do Leanu už známý důkaz Fermatovy poslední věty (To Brief). Převod slavného důkazu nevyvolává pochybnosti o novosti. U hledání mezi tvrzeními považovanými za nevyřešená už ano — a ověření novosti se tak stává hlavní částí práce.

Výzkumný tým zveřejnil soubory s důkazy, takže je ostatní mohou prověřit stejným způsobem (GitHub). Studie ukazuje konkrétní schopnost: agent s umělou inteligencí vytvořil strojově ověřitelné důkazy k některým tvrzením, která matematici považovali za nevyřešená. Záruka se vztahuje na jejich zápis v Leanu. Co jednotlivé důkazy přinesly matematice, dál posuzovali matematici, kteří je četli.