AI ponuja dokaz za Navier-Stokes. Kaj ostane matematikom?

Odpri sliko v polni velikosti

Vir slike: OpenAI.

Ko v kavo vlijemo mleko, nastanejo vrtinci. Podobno zapleteno gibanje vidimo v oblakih, rekah in zraku za letalom. Navier-Stokesove enačbe opisujejo gibanje tekočin in plinov, a njihova uporaba še ne pomeni, da razumemo vse, kar matematično dopuščajo.[4]

OpenAI je 8. septembra objavil dokaz, za katerega trdi, da rešuje znameniti problem obstoja in gladkosti teh enačb.[1] Če rezultat prestane neodvisno preverjanje, bo pomemben dosežek matematike. Hkrati odpira vprašanje, ki sega precej dlje od tekočin: kaj se zgodi s strokovnim znanjem, ko stroj pride do odgovora hitreje, kot ga ljudje uspemo razumeti?

Kaj je bilo pravzaprav rešeno?

Zelo poenostavljeno: ali lahko gibanje v matematičnem modelu, ki se začne povsem gladko, v končnem času postane tako skrajno, da gladek opis odpove? Takšni točki pravimo singularnost. Viskoznost, torej notranje trenje tekočine, gibanje sicer blaži; vprašanje je, ali to vedno zadošča.[1]

OpenAI trdi, da je izdelal primer, v katerem nastane singularnost kljub viskoznosti. Pomembna podrobnost je, da gre za tekočino z gladko zunanjo silo, ne za trditev, da se bo vsak običajen vrtinec sam od sebe spremenil v nekaj neskončnega.[1] To tudi ni napoved, da bo resnična voda dosegla neskončno hitrost. Gre za mejo idealiziranega matematičnega opisa, ne za odpravo fizikalnih omejitev.[1]

Prav tako tega ne gre pripisati običajnemu pogovoru s ChatGPT. Po navedbah OpenAI je rezultat ustvaril interni model, zmogljivejši od Astre, v sistemu z okoli 10.000 sočasnimi agenti. Astra je nato sodelovala pri formalizaciji in preverjanju dokaza v sistemu Lean.[1]

Objavljena rešitev ni isto kot zaključen strokovni pregled. Ob pripravi tega članka Clay Mathematics Institute problem na svoji strani še označuje kot aktiven.[4] Tukaj zato poročamo o objavljenem dokazu in trditvah avtorjev, ne o dokončno zaključenem postopku priznanja rešitve.

Kaj je podpisalo 25 Fieldsovih medalistov?

Petindvajset prejemnikov Fieldsove medalje, med njimi Terence Tao, Peter Scholze in Maryna Viazovska, je podpisalo deklaracijo A Severe Misalignment of AI in Mathematics. Njeno sporočilo: cilji podjetij, ki rešene probleme uporabljajo kot merilo zmogljivosti AI, se lahko močno razidejo s cilji matematike.[2]

Podpisniki ne trdijo, da AI nima mesta v raziskovanju. Izrecno priznavajo njegov potencial za pospeševanje resničnega matematičnega razumevanja.[2] Opozarjajo pa, da množično proizvajanje odgovorov »drži« ali »ne drži« ni enakovredno razvoju novih idej.[2]

Slavni problem je lahko svetilnik: raziskovalcem daje smer. Med iskanjem rešitve nastajajo metode, povezave in nova vprašanja. Nato sledijo razlage, razprave in poenostavitve, dokler lahko nekdaj nedostopen rezultat postane snov, iz katere se učijo študenti. Prav ta pot je osrednja tema deklaracije.[2]

Če ohranimo samo končni dokaz, smo morda dosegli cilj tekmovanja, ne pa nujno vsega, zaradi česar smo problem sploh raziskovali.

Tao: odgovor ni ves dosežek

Tao je za IBM Think opozoril na nevarnost, da bi hitrost reševanja prehitela počasnejše delo razvijanja metod in razumevanja, zakaj delujejo.[3] Njegova skrb ni samo, ali je posamezen dokaz pravilen, temveč tudi, kaj lahko spregledamo med hitenjem do naslednjega rezultata.[3]

Tu pomaga ločiti dve vprašanji. Ali zaključek sledi iz predpostavk? In: katera ideja pojasni, zakaj je tako, ter kje jo lahko uporabimo še drugje?

Formalni preverjevalnik, kot je Lean, je namenjen preverjanju formalno zapisanih dokaznih korakov. OpenAI je objavil tudi takšno formalizacijo.[1] Toda potrditev formalnega zapisa sama po sebi še ni razlaga, ki jo raziskovalec razume in zna prenesti na nov problem. Tudi preveriti je treba, ali formalno zapisana trditev ustreza vprašanju, ki smo ga želeli rešiti.

Kje je potem meja AI?

Ta dosežek, če bo potrjen, ne dokazuje, da AI lahko reši vse matematične probleme. Ne pove pa nam niti, da obstaja varna meja, za katero bodo nove ideje vedno izključno človeške.

Preveč udobno bi bilo reči: stroji bodo dokazovali, ljudje pa bomo za vedno edini, ki razumemo. AI lahko pomaga tudi pri razlagah, poenostavitvah in iskanju povezav. Deklaracija takšnega razvoja ne izključuje; vprašanje je, ali ga bomo spodbujali tako zavzeto kot lov na naslednji slavni problem.[2]

Zato se lahko pomembna omejitev preseli. Ne samo »ali znamo dobiti odgovor«, ampak »ali ga znamo preveriti, razložiti, povezati z drugim znanjem in naučiti naslednjo generacijo«.

Za matematike to ne pomeni nujno konca raziskovanja. Lahko pomeni več prostora za vprašanja, ki so bila doslej nedosegljiva. Toda če se spremeni način nastajanja dokazov, bo treba premisliti tudi način učenja: kako vzgojiti nekoga, ki zna presojati rezultat, če vse zahtevne vmesne korake vedno opravi orodje?

Isto vprašanje čaka druge stroke

Deklaracija izrecno povezuje položaj matematikov z drugimi znanstvenimi in ustvarjalnimi poklici: leta dela niso služila le izdelavi končnega rezultata, temveč tudi razvoju presoje in novih vprašanj.[2]

Primerjava je uporabna, čeprav meja preverjanja ni povsod enaka. V matematiki lahko formalno preverjamo sklepanje iz predpostavk. V medicini mora hipoteza prestati stik z bolniki in raziskavami. Pri inženirstvu mora rešitev delovati v resničnih razmerah. Lep dokument ali pravilen izračun še ne zagotavlja dobrega izida.

To ni razlog, da bi počasnost razglasili za vrednoto. Če lahko AI odstrani mesece rutinskega dela, je to priložnost. Pomembno pa je ločiti delo, ki ga lahko pogrešamo, od dela, skozi katero nastaja sposobnost samostojnega mišljenja.

Najzanimivejše vprašanje ob Navier-Stokesu zato ni, ali so matematiki postali odveč. Je, ali bomo z AI samo hitreje zapirali stara vprašanja ali pa bomo zaradi njega sposobni postavljati boljša nova.