Víme, jestli je Navier-Stokes správně?

včera 22:57 | Přečteno: 114× | matematika | | poslední úprava: dnes 00:25

Před dvěma týdny světem otřásla zpráva, že OpenAI vyřešila problém Milénia. Doprovodila jej důkazem v Leanu. Coby někdo, kdo se v oblasti formální matematiky & AI pohybuje, bych rád vysvětlil, jak jsme sebevědomí, že je výsledek matematicky správně, a co by se ještě mohlo zvrtnout.

Řeč je o tomhle repositáři, které obsahuje důkaz v Leanu. Mezi laiky jsem zaregistroval zhruba takovéhle dvě reakce:

• Je to v Leanu, tak to musí být správně.
• No a co? Proč bych měl věřit nějakému obřímu AI-slopu? Určitě tam bude nějaký bug.

A ani jedna není moc přesná, tak si zkusíme rozdělit, v čem se doopravdy mohl skrývat zádrhel, a proč si jsou lidi už celkem jistí.

• Softwarový bug v kernelu Leanu / toolingu.
• Bug ve formální formulaci oné věty -- dokázalo se něco jiného, než se chtělo.
• Chyba ve filozofických základech matematiky.

Tak si je pojďme po jednom projít.

Softwarový bug v Leanu.

Lean je poměrně komplexní software, ale jako správný logický systém odděluje svoje jádro, od automatizace, a uživatelského rozhraní. Jádro je zodpovědné za to, že každý krok následuje pravidla teorie závislých typů, na které Lean stojí. Při běžném použítí Leanu s ním uživatel moc neinteraguje, a běží pouze na pozadí jako sanity-check.

Pokud ale chceme ověřit cizí (a možná škodlivý) důkaz, je situace jiná. Ještě před pár lety na takovou situaci nebyl Lean připravený, teď je. Oficiální nástroj se jmenuje Comparator. Comparator spustí veškerý kód, který není ryzí jádro uvnitř sandboxu, a exportuje pouze low-level kroky v logice. Celé se to jmenuje "comparator" proto, že srovnává dva kódy napsané v Leanu -- důkaz (ke kterému jsme co nejvíc nedůvěřiví), a specifikaci -- větu, kterou chceme dokázat, a stojí stranou od všeho toho dokazování.

Bug v Comparatoru mi přijde dost nepravděpodobný -- jeho autor, Henrik Böving, si hodně dával záležet ne tom, aby byl pokud možná možná minimalistický, a bezpečný z pohledu IT security (nám ostatním přišel jeho přístup přehnaně paranoidní, ale asi ho teď chápu).

Bug v kernelu se objevit může. Po nějakou dobu Lean odolával útokům AI agentů (narozdíl od Rocqu & Isabelle), ale zrovna před dvěma měsíci nechal jeden AI researcher, Ramana Kumar, AI agenty, ať v Leanu dokáže Colatzovu domněnku. Výsledek byl pozitivní: důkaz byl schválen oficiálním jádrem Leanu, i alternativním populárním kernelem nanoda. Ukázalo se ale, že za výsledkem stojí softwarová chyba. Vlastně dvě chyby, jedna v oficiálním kernelu, a jiná chyba v nanodě, ale AI byla tak šikovná, že dokázala obejít obě dvě.

Proč by teď mělo být jinak? Tak v první řadě pak lidi vyvinuli určité úsilí, aby nechali agenty pochytat další bugy v jádru Leanu & nanodě. Ale za mne je poměrně důležitý i fakt, že vzniklo ještě další jádro Leanu: con-leche. Tohle jádro je na jednu stranu na-vibe-kóděné Claudem, ale na druhou stranu samo o sobě obsahuje důkaz v Leanu o svojí matematické správnosti (za předpokladu teorie množin s nekonečně nedosažitelnými kardinály, vysvětlím později). Takovýhle důkaz by měl běžné softwarové chyby odchytit, leda že by

• (a) Claude sám důkaz správnosti con-leche postavil na exploitu (z mojí zkušenosti to AI běžně nedělá, obzvlášť, když je pod dohledem).
• (b) Byla chyba je v interpretaci onho SW, například v knihovně GMP na velká čísla, o kterou se opírá jak oficiáľní kernel, tak jakýkoli program napsaný v Leanu.

Jak o tom teď přemýšlím, tak mi chyba ve všech použitých knihovnách na velká čísla příjde jako asi nejslabší článek... na druhou stranu, existují Kernely pro lean, které mají knihovnu pro velká čisla softwarově verifikovanou, a vůbec bych se nedivil, kdyby je někdo zkoušel pustit na Navier-Stokese. Poptám se a dám pak vědět.

Chyba ve formulaci dokázané věty

Okolo posledního Silvestra bylo pozdvižení, když jeden researcher, co odešel z DeepMindu, aby si založil vlastní startup tvrdil, že jeho AI vyřešila Navier-Stokesovy rovnice. Tou dobou se můj kamarád (Tomáš Skřivan) podíval, jestli existuje oficiální formulace Navier-Stokesových rovnic v Leanu, a zjistil, že jediná existující formulace měla řadu chyb. Od té doby ale napsal Tomáš vlastní formulaci, která prošla recenzí několika matematiků. To je verze, kterou OpenAI použíla pro svůj důkaz. Krom toho se po výsledku OpenAI na to znění podívali i další matematici, a prakticky všichni se shodují, že nevidí, co by na tom mohlo být špatně.

Další varianta chyby by mohla být schovaná v definicích z knihovny Mathlib. To je standardní matematická knihovna, odkud Lean zná pojmy jako "reálná čísla" nebo "parciální derivace". Takovou chybu ale považuji za dost nepravděpodobnou. Chyby v definicích většinou dlouho nevydrží, protože když máte definice špatně, tak na ně narazíte v okamžiku, kdy se snažíte dokázat nějaké věty. A protože jak reálná čisla, tak parciální derivace jsou dost elementární koncepty, tak jsem si prakticky jistý, že jsou napsané správně.

Takže ano, jsem si dost jistý, že skutečně jde o ten problém, za který se nabízelo $1M. Jestli to je skutečně ta formulace, o kterou se fyzici zajímají je jiná otázka... Cena $1M byla totiž vypsána za cokoli z následujícího (laicky řečeno):

• (a) & (b) Dokažte, že čaj samovolně neexploduje.
• (c) & (d) Dokažte, že čaj může explodovat, když ho šikovně mícháte lžičkou.

Rozdíl mezi variantami a / b (analogicky mezi c / d) jsou převážně formální (jestli jsme na toru nebo v nekonečném prostoru). Nicméně je rozdíl, zda se povolí externí síla, a nebo ne. OpenAI vyřešila (c) & (d). Když byla totiž cena vypsána, tak si lidi mysleli, že ani když "čaj mícháte lžičkou, tak explodovat nemá šanci", a tak vůbec nečekali, že by to vlastně šlo udělat, i když s naprosto uměle kalkulovanými silami. Postupem času lidi ale začali singularity nacházet v podobných diferenciálních rovnicích, případně numerickými metodami, hezky to vysvětlují na téhle přednášce (ale je to zase delší).

Chyba v matematice

Logici jsou posedlí velkými čísly & zejména velkými množínami. Množínami, které nejsou jenom nekonečné, ale i ta jejich nekonečnost je tak nepředstavitelně enormní, že se to laikovi vůbec nedá vysvětlit, natož aby to mělo jakoukoly souvislost s miniaturním fyzickým světem... Představte si vysoce inteligentního matematika, který stráví roky přemýšlením o tom, jak chytře vymyslet popis co možná největší množiny -- o takhle velkých množinách tu je řeč.

Proč? Co je na velkých množinách tak ukrutně zajímavého? Inu, logici nekonečné množíny nemají pro sebe, ale pro to, aby vás do nich mohli zavřít. Posláním logiků je poskytnout ostatním matematikům svět, ve kterém na jednu stranu budou omezení, aby nemohli odvodit nesmysly skrz triky jako "Množína všech množin, které neobsahují sama sebe" nebo "Nejmenší číslo, které se nedá definovat méně než dvaceti českými slovy." Na druhou stranu je třeba, aby se matematici necítili stísněně -- aby měli dost prostoru na to "dělat matiku".

Dá se to trochu přirovnat k softwarovému sandboxu. Dáte uživatelům příliš mnoho restrikcí, a příliš málo nástrojů, a budou reptat. Dáte jim příliš mnoho svobody, a hacknou vás.

Hodně omezená logická klec je Peanova aritmetika. V praxi Peanova aritmetika matematikům umožní postavit jakékoli konečné objekty -- celá čísla, racionální čísla, matice, grafy, ... ale ne nekonečné objekty jako reálná čísla, nekonečné posloupnosti, atp. Běžně se proto v matematice používá teorie množin od Zermelo a Frankela. Formální systémy často jdou ještě kousek dál, a třeba Lean je ekvivalentní teorii množin s libovolným konečným počtem nedosažitelných kardinálů. To zhruba řečeno znamená, že to je konečně mnoho standardních teorií množin zanořených v sobě.

Když tohle řeknete matematikovi, často se zděsí. "Můžu tomu věřit? Celou svojí kariéru jsem si myslel, že existuje jenom jedna úroveň teorie množin. Co když se s těmihle nedosažitelnými kardinály dá odvodit spor?" Na druhou stranu, já považuji takovou možnost za ne moc pravděpodobnou. I když se jedná o teorii vyžadující / poskytující víc místa než běžná teorie množin, a proto je trochu víc riskantní, je to pořád hodně na začátku seznamu velkých kardinálů. Logici se na velké kardinály dívali už dost dlouho, a krom Reinhardtova kardinálu (navržený 1967, vyvrácený 1971) zatím nenašli spor v žádném dalším velkém kardinálu. Takže ty nedosažitelné kardinály, které jsou v seznamu na Wikipedii na druhém místě, jsou dost v bezpečí.

       

Anketa

Komentáře

[Max]

Chybí mi v anketě, že o tom nevím ani tušku ¯\_(ツ)_/¯.
Zdar Max

[vencour]

🐧 +1

[vencour]

Pro zvědavce co na to říká AI ... Jak moc je to ok a bez chyb?

[mirefek]

Dobrý no , jestli to pomůže k pochopení... Jenom mi přijde, že AI moc nepochopila, že naprosto centrální téma mého zápisku bylo "můžeme věřit Leanu?" (ne jenom druhá půlka), a místo toho se fakt hodně rozpovídal o těch rovnicích samotných. Já se zaměřil na otázku Leanu proto, že o rovnicích samotných, a kdejakých kontroverzích se mluvilo fakt hodně, a moc se neví, na čem je založená současná jistota matematické správnosti.