Špičkový matematik se v noci rozplakal. AI smetla za pár dní to, na čem dřel celé roky

Když francouzský matematik a držitel prestižní Fieldsovy medaile Hugo Duminil-Copin otevřel jednoho večera balík více než 700 předběžných vědeckých prací, které začátkem října zveřejnila společnost OpenAI, neudržel emoce. Rozplakal se tak, že probudil svou dceru. Během okamžiku smetla umělá inteligence (AI) ze stolu 16 matematických problémů, na nichž pracoval celé roky.

Zatímco akademici zažívají z bleskového pokroku matematických schopností AI existenciální šok, rozlousknutí abstraktních rovnic je ve skutečnosti předehrou k největší komerční transformaci v oboru. Technologičtí giganti a investoři vidí v propojení jazykových modelů s matematikou svatý grál: první AI, která si nevymýšlí. Garance, že se čip nebo software v letadle, jaderné elektrárně či při řízení cloudu bude chovat podle zadání, by nespolehlivé chatboty změnila v kritickou infrastrukturu, za niž budou firmy v mnoha oborech ochotny platit miliardy dolarů.

Že se AI firmy vrhly právě na matematiku, není náhoda. Běžné jazykové modely halucinují – vymýšlejí si. Jejich texty proto vyžadují pomalou a drahou lidskou kontrolu. V matematice je ale pravda binární: důkaz buď správný je, nebo není. Vývojáři proto jazykové modely spojili s programem Lean, který funguje jako neúprosný dozorce. Vznikl neúnavný tandem: zatímco AI chrlí varianty řešení a přichází s důkazem v podobě kódu, Lean každý krok ověří. Pokud AI zalže nebo udělá nelogický skok, Lean ji zastaví. Jestliže však systém najde řešení, jež tímto sítem projde, vzniká nezpochybnitelný výsledek.

Rychlost, s jakou AI v řešení matematických rébusů postupuje, šokuje. Dnes ale ohledně tempa rozhoduje hlavně hrubá výpočetní síla. Už v září OpenAI prohlásila, že vyřešila problém Navierových–Stokesových rovnic. Ty patří mezi takzvaných sedm problémů tisíciletí, za jejichž vyřešení je vypsána odměna jeden milion dolarů (21,8 milionu korun). OpenAI v tomto případě nasadila zhruba deset tisíc spolupracujících AI agentů, kteří k důkazu došli ani ne za čtyři dny.

To je pro technologické firmy zároveň cesta k vyřešení hrozby „modelového kolapsu“: docházejí totiž kvalitní lidské texty a trénování na podkladech od jiných AI, obsahujících chyby, vede k degeneraci modelů. Ověřené matematické důkazy naopak představují syntetická data nejvyšší kvality, která slouží jako dokonalé palivo pro novou generaci algoritmů.

Rychlost pokroku díky tomuto tandemu je brutální. Ještě v roce 2023 dokázal ChatGPT ve středoškolské olympiádě získat sotva pětinu bodů; dnes řeší mezinárodní soutěže na plný počet.

Přichází kentaur

Přesto má tento triumf pro řadu vědců stinnou stránku. AI sice předloží důkaz, že věta platí, ale často už neobjasní proč. Pro vědce však v matematice nikdy nešlo jen o konečný výsledek, ale také o hluboké pochopení a budování nových teorií. Tento odpor k „černým skříňkám“ z dílny AI se projevil například veřejným odsudkem skupinou držitelů Fieldsovy medaile. Asociace pro lidskou matematiku pak masové zveřejnění předběžných řešení stovek matematických problémů OpenAI označila za „demonstraci moci“ a matematiky vyzvala, aby se společností přestali spolupracovat a „vrátili se k vizi vědy, která se zaměřuje na lidské chápání“.

Kooperativnější cestou než OpenAI šel Google DeepMind, divize společnosti Alphabet zaměřená na AI a strojové učení. Tato přední výzkumná laboratoř sází namísto hrubé síly na spolupráci člověka a stroje. Koncept známý jako „kentaur“ podle šachu, kdy spolu hrají člověk a stroj, prosazuje nejvlivnější žijící matematik Terence Tao. (Ten přitom ještě před dvěma lety přirovnal AI v matematice k průměrnému postgraduálnímu studentovi.)

V praxi „kentaura“ aplikuje systém AI Co-Mathematician právě od Google DeepMind, který v nejtěžší části referenčního testu FrontierMath vyřešil rekordních 48 procent úloh. Ve spolupráci s člověkem funguje jako virtuální asistent: hledá v literatuře, počítá úmorné mezikroky, a když narazí na slepou uličku, požádá o radu člověka.

Svou zkušenost z takové spolupráce popsal i oxfordský matematik Marc Lackenby, který řešil otevřený matematický problém v teorii grup. AI mu sice důkaz dodala, avšak s mezerou, již sama objevila. Lackenby si s ní poradil a důkaz dotáhl k úspěšnému konci. Stroj tak odvedl mechanickou dřinu, zatímco člověk dodal intuici. A problém padl.

Firmy a investoři chápou zapojení AI do vysoké matematiky ještě pragmatičtěji: jestliže systém dokáže bezchybně zkontrolovat matematický důkaz, stejnou metodou je schopen prověřit i software či hardware v reálném světě.

Verifikace jako zlatý důl

Tato metoda – takzvaná formální verifikace – není nová. Intel ji začal využívat už po slavné chybě v procesorech Pentium z roku 1994, která ho stála půl miliardy dolarů. Dnes ověřují řídicí systémy letadel Airbus nebo bezpečnostní platformy jaderných elektráren včetně Dukovan. Až dosud však šlo o extrémně drahý a pomalý proces, na nějž byly potřeba celé týmy špičkových matematiků.

AI v tandemu s Leanem tuto bariéru boří. Startupy jako Axiom (oceněný na 1,6 miliardy dolarů) či jeho konkurent Harmonic (oceněný na 1,45 miliardy dolarů) už stavějí byznys právě na tom, že automatizované matematické ověřování nasadí na finanční transakce nebo návrhy čipů. Amazon Web Services už touto metodou jistí i své cloudové služby, a dokonce ji nabízí koncovým klientům právě jako ochranu před chybujícími AI agenty.

Přestože jde vývoj v aplikování AI na matematiku neuvěřitelnou rychlostí kupředu, i zde nadále platí zásadní omezení: stroj ověří jen to, co mu člověk zadá. Pokud inženýr chybně nadefinuje samotné zadání, AI mu sice vygeneruje bezchybný důkaz, avšak pro nefunkční systém.

OpenAI se za vyřešení Navierových–Stokesových rovnic k nároku na milionovou odměnu nepřihlásila. Pro ni i ostatní firmy pracující s umělou inteligencí je cílem něco jiného: předložení důkazu, že současné AI modely již umějí poskytnout jistotu, za niž budou zákazníci ochotni platit mnohonásobně vyšší částky.