Novosť deviatich dôkazov DeepMind preveria matematici

Matematický dôkaz môže pôsobiť presvedčivo, a predsa v ňom môže zostať medzera, ktorú roky nikto neodhalí. Agent AlphaProof Nexus od Google DeepMind vytvoril dôkazy k deviatim úlohám, ktoré zadal Paul Erdős, a softvér skontroloval každý krok. Výsledky sa najprv objavili v májovom preprintе (arXiv) a po recenznom konaní vyšli 8. októbra v časopise Science (Science). Softvér mohol potvrdiť správnosť logiky, no posúdiť, či dôkazy prinášajú niečo nové, museli matematici.

Rozhodca, ktorého nemožno obmäkčiť

Chatboty vedia napísať matematický text, ktorý znie správne. Sebavedomý výklad môže zakryť chýbajúci krok a odhalí ho len pozorné čítanie. AlphaProof Nexus sa tomuto riziku vyhýba tým, že pracuje v jazyku Lean. V ňom sa definície, tvrdenia aj dôkazy zapisujú natoľko presne, že ich počítač dokáže skontrolovať.

Lean si možno predstaviť ako rozhodcu, ktorý prečíta každý riadok hotového dôkazu a overí ho podľa pevných pravidiel. Na štýle nezáleží. Ak čo i len jeden krok nevyplýva z predchádzajúcich, dôkaz neprejde, nech je zvyšok akokoľvek elegantný.

Výskumný tím opisuje agenta ako systém, ktorý hľadá dôkazy zapísané v jazyku Lean. Vedci mu sprístupnili aj AlphaProof, starší systém DeepMind vytvorený špeciálne na dokazovanie. V testoch tímu prinieslo rovnaký výsledok aj jednoduchšie riešenie: jazykový model spojený s Leanom bez AlphaProofu vytvoril dôkazy ku všetkým deviatim Erdősovým úlohám (The Decoder). Pri týchto úlohách sa špecializovaná súčasť ukázala ako zbytočná.

Článok uvádza dôkazy pre deväť Erdősových tvrdení a 44 domnienok z Online Encyclopedia of Integer Sequences, rozsiahleho katalógu číselných vzorov (Science). Domnienky sú tvrdenia, ktoré sa považujú za pravdivé, no nikto ich ešte nedokázal. Medzi výsledkami je aj dvojdielny problém o celých číslach, ktorý Erdős a András Sárközy predložili v roku 1970. Viac než polstoročie zostával otvorený (ABC).

Čo rozhodca nevidí

Záruka, ktorú dáva Lean, má jasné hranice. Potvrdzuje, že dôkaz preukazuje tvrdenie presne tak, ako je zapísané v kóde. Neodpovedá však na tri otázky: či kód vystihuje, čo mal Erdős na mysli, či na otázku niekto neodpovedal už dávno a či riešenie prináša nové poznanie.

Problém z roku 1970 ukazuje, prečo záleží na posledných dvoch otázkach. Jeho druhá časť vyplýva z prvej, takže jeden dôkaz vyrieši obe. Keď sa dôkazy agenta začali šíriť, ukázalo sa, že obe časti rieši aj pomerne malá úprava konštrukcie z pôvodného článku z roku 1970 (arXiv). Dôkazy agenta boli správne. Problém bol jednoducho bližšie k vyriešeniu, než naznačovalo označenie „otvorený“.

Odhalenie takýchto súvislostí si vyžaduje ľudí, ktorí poznajú danú oblasť. Gergely Bérczi, matematik z dánskej Aarhus University a jeden z autorov článku, pomáhal vyberať vhodné otázky a overovať riešenia (Aarhus University). Pomáhal aj písať verzie dôkazov, ktorým porozumejú ľudskí čitatelia. Lean potvrdil správnosť každého kroku, zatiaľ čo Bérczi a jeho kolegovia posudzovali, čo dôkazy prinášajú.

Toto rozdelenie práce odlišuje štúdiu od výsledku, ktorý prišiel minulý mesiac. Vtedy Claude od Anthropic prepísal do jazyka Lean už známy dôkaz Veľkej Fermatovej vety (To Brief). Pri prepise známeho dôkazu nevznikajú pochybnosti o jeho novosti. Keď systém hľadá riešenia medzi tvrdeniami považovanými za otvorené, treba zistiť, či na ne už niekto neodpovedal. Práve toto preverenie sa stáva hlavnou úlohou.

Tím zverejnil súbory s dôkazmi, takže ich ostatní môžu skontrolovať tým istým spôsobom (GitHub). Štúdia ukazuje konkrétny posun: agent umelej inteligencie vytvoril strojovo overiteľné dôkazy pre niektoré tvrdenia, ktoré matematici považovali za otvorené. Záruka sa vzťahuje na tieto tvrdenia tak, ako sú zapísané v jazyku Lean. Čo jednotlivé dôkazy pridali k matematike, posudzovali matematici, ktorí ich čítali.