„Įrodymas kode“
Autorius: Kevin Hartnett
„Quanta“, 288 puslapiai, 30 JAV dolerių
Praėjusį mėnesį matematikos pasaulį sukrėtė žinia: „OpenAI“ paskelbė išsprendusi vieną garsiausių šios srities uždavinių. Navjė-Stokso (Navier-Stokes) uždavinys, susijęs su sudėtinga skysčių dinamika, beveik du šimtmečius atlaikė matematikų bandymus jį įveikti. Siekdama jį išspręsti, „OpenAI“ pasitelkė 10 000 dirbtinio intelekto agentų būrį; jiems prireikė 88 valandų rezultatui gauti ir dar 17 valandų jam patvirtinti naudojant kompiuterinę tikrinimo programą „Lean“. Šiame procese bendrovė aplenkė Niujorko universiteto matematiką Tristaną Buckmasterį ir jo kolegas, kurie jau buvo arti sprendimo. Šis pranešimas daugeliui matematikų tapo šoku ir paskatino gilius apmąstymus. Tačiau Alano Turingo tai galbūt nebūtų nustebinę.
1936-aisiais, kai A. Turingui buvo vos 24-eri, jis sugalvojo paprastą, bet radikalų mintinį eksperimentą. Jis pasiūlė įsivaizduoti mechanizmą, sudarytą iš begalinės juostos, padalytos į langelius su juose įrašytais ženklais, bei „galvutės“ (taip jis vadino šią dalį), galinčios skaityti ir rašyti ženklus. Galvutė perskaitytų ženklą langelyje, reaguodama įrašytų kitą ženklą, tada pereitų prie kito langelio ir atliktų tą patį veiksmą – ir visa tai darytų vadovaudamasi iš anksto nustatytomis taisyklėmis. Šis pasiūlymas atrodė ir trivialus, ir beprasmis: juk mechanizmas nieko „nedaro“, tik keičia beprasmius ženklus kitais beprasmiais ženklais. Vis dėlto „Turingo mašina“ (taip šis mechanizmas vėliau buvo pavadintas) sukūrė teorinį pagrindą visiems iki šiol naudojamiems kompiuteriams.
A. Turingas nebuvo informatikas, nors ir sukūrė šią sritį. Jis buvo matematikas, o jo mašina – „formalizmo“ įsikūnijimas. Ši idėja tuo metu keitė matematiką: teigta, kad matematika – tai ne universalių tiesų tyrimas, o tiesiog manipuliavimas beprasmiais ženklais pagal iš anksto nustatytas taisykles. Tad kas galėtų būti tinkamiau už mechanizmą, kuris daro būtent tai? Vadinasi, Turingo mašina galėtų sukurti visą įmanomą matematiką ir tai daryti kur kas geriau nei klaidoms imlus žmogus.
Kaip straipsnyje „The Proof in the Code“ („Įrodymas kode“) pasakoja Kevinas Hartnettas, netrukus po to, kai atsirado skaitmeniniai kompiuteriai, jų kūrėjai pabandė praktiškai išbandyti A. Tiuringo pasiūlytą idėją. Šeštajame ir septintajame dešimtmečiuose tyrėjai sukūrė automatines teoremų įrodymo sistemas (angl. *Automated Theorem Provers* – ATP), gebančias analizuoti sudėtingas matematines formules ir nustatyti, ar tam tikromis sąlygomis jos yra teisingos. Šios sistemos pasirodė esančios galingos ir veiksmingos – bent jau sprendžiant tam tikras matematines problemas.
Vis dėlto paaiškėjo, kad daugumos matematikus dominančių klausimų neįmanoma taip paprastai pateikti kompiuteriui. Todėl, atsisakę visiško įrodymų automatizavimo idealo, tyrėjai sukūrė interaktyviąsias teoremų įrodymo sistemas (angl. *Interactive Theorem Provers* – ITP): matematikas pateikia formalų argumentavimą, o programa patikrina, ar jis teisingas ir kokiomis sąlygomis. Naudodamiesi šiuo lankstesniu įrankiu, 1976 m. Kennethas Appelis ir Wolfgangas Hakenas įrodė daugiau nei šimtmetį neišspręstą keturių spalvų teoremą, o Thomasas Halesas įrodė dar reikšmingesnę, keturis šimtmečius gyvavusią Keplerio hipotezę.
Nepaisant to, interaktyviosios sistemos (ITP) tarp praktikuojančių matematikų nepopuliarėjo. Jie greitai suprato, kad norint paversti matematinį argumentavimą kompiuterinei programai suprantama kalba, reikia įdėti milžiniškas pastangas. Argumentavimą tekdavo išskaidyti į varginančiai smulkų, žingsnis po žingsnio dėstomą formalų procesą; to paties reikėjo ir visai matematinei bazei, kuria tas argumentavimas rėmėsi. Įprastai bendraudami matematikai remiasi plačiu žinių bagažu, kurį, jų manymu, puikiai išmano ir kolegos. Norint pateikti argumentavimą ITP sistemai, visas šias papildomas žinias būtina suvesti aiškiai ir formaliai – pradedant nuo pačių paprasčiausių skaičių apibrėžimų. Paradoksalu, tačiau bandymas spręsti matematinę problemą pasitelkus kompiuterius dažnai pareikalaudavo kur kas daugiau darbo nei tradicinis sprendimo būdas.
Straipsnyje „The Proof in the Code“ pasakojama apie „Lean“ – interaktyviąją teoremų įrodymo sistemą, kuri galiausiai pavertė kompiuterinį įrodymą svarbia pagrindinės matematikos dalimi. „Lean“ sukūrė Leonardo de Moura – informatikas, dirbęs „Microsoft Research“ padalinyje 2000-ųjų pradžioje. Iš pradžių L. de Mouros tikslas buvo gana kasdieniškas: sukurti kompiuterinę programą, kuri „Microsoft“ produktuose aptiktų paslėptas klaidas. Jo „Z3“ programa pasirodė esanti itin veiksminga tikrinant „Windows 7“ prieš šios sistemos išleidimą 2009 m., tačiau „Lean“ buvo sukurta siekiant dar geresnių rezultatų: jei „Z3“ galėjo patikrinti tik konkrečias programos vykdymo sekas su tam tikromis reikšmėmis, tai „Lean“ buvo skirta klaidoms ieškoti visoje programoje.
Nors „Lean“ kūrėjas p. de Moura galbūt tikėjosi, kad ši programa prisidės prie „Microsoft“ finansinės sėkmės, netrukus paaiškėjo, kad didžiausią susidomėjimą ja rodo matematikai. Pasirodo, kompiuterinės programos tikrinimas ieškant klaidų beveik nesiskiria nuo formalaus matematinio įrodymo tikrinimo – o būtent tai ir atlieka interaktyviosios teoremų tikrinimo sistemos (ITP). Tad p. de Moura pradėjo glaudžiai bendradarbiauti su matematikų grupe, siekiančia, kad kompiuteriai taptų įprastu jų srities įrankiu. Hartnettas geriausiai atsiskleidžia aprašydamas įvairias šios nedidelės bendruomenės narių asmenybes ir tarpusavio santykių dinamiką. De Moura – genialus, tačiau kuklus žmogus – savo atkaklumu užtikrina sklandžią projekto eigą. Artimiausias jo bendražygis Jeremy Avigadas yra klasikinis akademinis mentorius, įtraukiantis savo studentus į šią veiklą. Jaunesnės kartos atstovas Mario Carneiro, kartais nesutariantis su de Moura, dega aistra formalizuoti matematinius įrodymus. O ryškus britų skaičių teoretikas Kevinas Buzzardas tiki, kad „Lean“ išvaduos matematiką nuo pernelyg didelio aplaidumo.
Norėdami išvengti Sizifo darbo – kiekvieną kartą iš naujo formalizuoti visą reikiamą matematiką, – „Lean“ entuziastai nusprendė sukurti „Mathlib“: formalizuotos matematikos biblioteką. Tai buvo ilgas ir neturintis aiškios pabaigos procesas, kėlęs trintį komandos viduje. Ypač daug sunkumų patyrė de Moura: siekdamas tobulinti pagrindines „Lean“ funkcijas, jis kasdien valandų valandas taisydavo kitų bendradarbių įrašus „Mathlib“ bibliotekoje, o patys bendradarbiai jam atrodė reiklūs ir nepagarbūs. Visgi bibliotekai augant ir žiniai apie ją sklindant plačiau, vis daugiau matematikų panoro prisidėti prie projekto ir tapti „Lean“ bendruomenės dalimi.
Lūžis įvyko 2020 m. pabaigoje. Peteris Scholze’ė, Fildso medalio (dar vadinamo matematikos Nobelio premija) laureatas, kreipėsi į K. Buzzardą prašydamas pagalbos: ar „Lean“ galėtų patikrinti naujausią ir sudėtingiausią jo įrodymą srityje, vadinamoje „skystaisiais tenzoriais“ (angl. *liquid tensors*)? Kadangi šis įrodymas rėmėsi daugybe ankstesnių rezultatų, norint jį patikrinti naudojant „Lean“, reikėjo formalizuoti visas tas matematines žinias ir įtraukti jas į „Mathlib“. Projektas pareikalavo 28 matematikų darbo ir truko 18 mėnesių, tačiau 2022 m. liepą P. Scholze’ė paskelbė, kad „Lean“ patvirtino jo įrodymą. Po metų Terence’as Tao iš Kalifornijos universiteto Los Andžele – dar vienas Fildso medalio laureatas ir, ko gero, įtakingiausias matematikas pasaulyje – subūrė dar didesnę grupę, kad pasitelkę „Lean“ patikrintų jo įrodytą polinominę Freimano-Ruzsos hipotezę. Abejonių nebeliko: „Lean“ tapo svarbiu šiuolaikinės matematikos ramsčiu.
Tačiau tuo metu, kai „Lean“ įrodinėjo savo vertę, už akademinių sluoksnių ribų vyko kita revoliucija. Pirmiausia „OpenAI“, o vėliau ir daugybė kitų įmonių pradėjo siūlyti didelius kalbos modelius, kurie galėjo rašyti prozą, versti kalbą, kurti vaizdo įrašus pagal komandas ir dar daugiau. Apmokyti dirbti su milžinišku kiekiu žmonių sukurtų šaltinių, šie teisės magistro (LLM) specialistai naudoja statistinius algoritmus, kad gautų rezultatus, kurie beveik nesiskiria nuo žmonių kūrinių.
Iš pradžių teisės magistro (LLM) specialistai buvo prasti matematikos srityje. Paprašyti sugeneruoti įrodymą, jie pateikdavo tekstą, kuris atrodė kaip įrodymas, bet buvo logiškai nerišlus. Tada Thomas Hubert iš „Google“ „DeepMind“ sugalvojo būdą, kaip pagerinti jų našumą: užuot tenkinęsi blogu „įrodymu“, teisės magistro (LLM) specialistai įvesdavo savo pradinį darbo produktą į „Lean“, kuris teikdavo grįžtamąjį ryšį. Teisės magistro (LLM) specialistai naudodavo šį grįžtamąjį ryšį, kad sukurtų geresnę versiją, kurią vėl įvestų į „Lean“. Po daugelio iteracijų DI variklis galėjo pateikti tinkamą įrodymą. Šis ciklas, daug kartų padaugintas naudojant autonominius DI agentus, buvo esminis „OpenAI“ rezultatui gauti.
Ar pagaliau pasiekėme tikrą Tiuringo mašiną, kuri gali generuoti sudėtingus matematikos uždavinius be žmogaus indėlio? Galima pateikti gerą argumentą, kad turime. Vis dėlto skaitydamas „Įrodymą kode“, kuris skaitytoją nukelia tiesiai prie dabartinių proveržių slenksčio, mane sužavėjo tiek mašininės matematikos ribotumas, tiek jos galia. „Lean“ gali patikrinti bet kokią dedukcijų seką, tačiau vis tiek remiasi „Mathlib“ – žmogaus sukurtu matematikos agregatu, kurį žmonės laikė svarbiu ir prasmingu.
Panašiai ir „OpenAI“ Navjė-Stokso įrodymas neabejotinai buvo fantastiškai sudėtingas ženklų manipuliavimo pratimas. Tačiau būtent žmonės nusprendė, kad svarbu išleisti milijonus dolerių dirbtinio intelekto agentams, kad šie atliktų šį konkretų ženklų manipuliavimo pratimą. Taigi turime paklausti: ar įrodymo metodas, kuris atmeta žmogaus įžvalgą ir turi būti priimtas tikėjimu, gali būti laikomas matematika? Neseniai paskelbtame laiške daugiau nei 25 Fieldso medalio laimėtojai (įskaitant ponus Scholze ir Tao) atsakė: „ne“. „OpenAI“ įrodymas beveik neabejotinai teisingas. Tačiau rezultatas, kuris nieko nepadeda skatinti žmonių supratimo, jų teigimu, vargu ar gali būti vadinamas matematika.
Ši sritis yra lūžio taške. Dėl „Lean“ sistemos išpopuliarėjimo ir didėjančios didžiųjų kalbos modelių (LLM) įtakos matematikai pirmą kartą per daugiau nei šimtmetį buvo priversti iš naujo įvertinti savo srities pagrindus. Kas laikoma matematika? Kas laikoma įrodymu? Ir kam – žmogui ar mašinai – turėtų atitekti nuopelnai? Kevino Hartnetto straipsnis „Įrodymas kode“ („The Proof in the Code“) – tai gyvas ir labai žmogiškas pasakojimas apie tai, kaip atsidūrėme šioje situacijoje.
---
A. Alexanderis dėsto mokslo ir matematikos istoriją Kalifornijos universitete Los Andžele. Naujausia jo knyga – „Liberty's Grid: A Founding Father, a Mathematical Dreamland, and the Shaping of America“" [1].
1. REVIEW --- Books: A Lean, Mean Math Machine. Alexander, Amir. Wall Street Journal, Eastern edition; New York, N.Y.. 03 Oct 2026: C7.
Komentarų nėra:
Rašyti komentarą