„Tūkstančius metų matematikai prisitaikė prie naujausių
logikos ir samprotavimų pasiekimų. Ar jie pasiruošę dirbtiniam intelektui?
Getty muziejaus Los Andžele kolekcijoje yra XVII amžiaus
senovės graikų matematiko Euklido portretas: išsišiepęs, iškėlęs „Elementų“
lapus, jo traktatą apie geometriją, nešvariomis rankomis.
Daugiau, nei 2000 metų Euklido tekstas buvo matematinio
argumentavimo ir samprotavimo paradigma. „Euklidas išgarsėjo, pradedamas
„apibrėžimais“, kurie yra beveik poetiški“, – elektroniniame laiške sakė
Carnegie Mellon universiteto logikas Jeremy Avigadas. „Tada jis sukūrė to meto
matematiką, įrodydamas dalykus taip, kad kiekvienas tolesnis žingsnis „aiškiai
išplauktų“ iš ankstesnių, naudodamas pagrindines sąvokas, apibrėžimus ir
ankstesnes teoremas. Buvo skundų, kad kai kurie „akivaizdūs“ Euklido žingsniai
buvo ne tokie akivaizdūs, sakė daktaras Avigadas, tačiau sistema veikė.
Tačiau XX amžiuje matematikai nebenorėjo grįsti matematikos
šiuo intuityviu geometriniu pagrindu. Vietoj to jie sukūrė formalias sistemas –
tikslius simbolinius vaizdus, mechanines taisykles. Galiausiai šis
formalizavimas leido matematiką paversti kompiuteriniu kodu. 1976 m. keturių
spalvų teorema, kuri teigia, kad keturių spalvų pakanka užpildyti žemėlapį, kad
nė karto du gretimi regionai nebūtų vienodos spalvos, tapo pirmąja pagrindine
teorema, įrodyta, skaičiuojant su grubia kompiuterio jėga.
Dabar matematikai grumiasi su naujausia transformuojančia
jėga – dirbtiniu intelektu.
2019 m. Christianas Szegedy, kompiuterių mokslininkas,
anksčiau dirbęs „Google“, o dabar Įlankoje startuojančioje įmonėje, numatė,
kad kompiuterinė sistema per dešimtmetį atitiks arba viršys geriausių žmonių
matematikų gebėjimus spręsti problemas. Praėjusiais metais jis patikslino
tikslinę datą iki 2026 m.
Prinstono Išplėstinių studijų instituto matematikas ir 2018
m. Fieldso medalio laureatas Akshay Venkatesh šiuo metu nėra suinteresuotas naudoti
A.I., tačiau jis nori apie tai kalbėti. „Noriu, kad mano mokiniai suprastų, jog
sritis, kurioje jie dirba, labai pasikeis“, – pernai interviu sakė jis.
Neseniai elektroniniu paštu jis pridūrė: „Aš neprieštarauju apgalvotam technologijų naudojimui mūsų žmogiškajam supratimui paremti. Tačiau
aš tvirtai tikiu, kad labai svarbu atkreipti dėmesį į tai, kaip mes jas
naudojame."
Vasario mėn. Dr. Avigad dalyvavo seminare apie „mašininius
įrodymus“ Grynos ir taikomosios matematikos institute, Kalifornijos
universiteto miestelyje Los Andžele. (Paskutinę seminaro dieną jis aplankė
Euklido portretą.) Susirinkime dalyvavo netipiškas matematikų ir kompiuterių
mokslininkų mišinys. „Jaučiasi, kad tai turi įtakos“, – sakė universiteto
matematikas, 2006 m. Fieldso medalio laimėtojas ir seminaro pagrindinis
organizatorius Terence'as Tao.
Daktaras Tao pažymėjo, kad tik pastaruosius kelerius metus
matematikai pradėjo nerimauti dėl galimų A.I. grėsmių matematinei estetikai ar
jiems patiems. Tie žinomi bendruomenės nariai dabar gvildena problemas ir tiria
galimą „tabu sulaužymą“, – sakė jis.
Vienas ryškus seminaro dalyvis sėdėjo pirmoje eilėje:
trapecijos formos dėžė, pavadinta „robotu su pakeliama ranka“, kuri skleidė
mechaninį ūžesį ir pakeldavo ranką, kai interneto dalyviui iškildavo klausimas.
„Tai padeda, jei robotai yra mieli ir nekelia grėsmės“, – sakė daktaras Tao.
Pritraukite „įrodymų verkšleninkus“
Šiais laikais netrūksta įtaisų, skirtų optimizuoti mūsų
gyvenimą – mitybą, miegą, mankštą. „Mums patinka prisirišti prie savęs daiktus,
kad būtų lengviau viską susitvarkyti“, – per seminaro pertrauką sakė
Viskonsino-Madisono universiteto matematikas Jordanas Ellenbergas. Jis
pridūrė, kad įtaisai gali padaryti tą patį matematikos srityje: „Labai aišku, kad
kyla klausimas, ką mašinos gali padaryti už mus, o ne tai, ką mašinos padarys
mums“.
Viena matematikos programėlė vadinama įrodymo padėjėju arba
interaktyviuoju teoremų tikrintoju. („Automatika“ buvo ankstyvas įsikūnijimas
septintajame dešimtmetyje.) Žingsnis po žingsnio matematikas įrodymą paverčia
kodu; tada programinė įranga patikrina, ar motyvai yra teisingi. Patikrinimai
kaupiasi bibliotekoje – dinaminėje kanoninėje nuorodoje, kurią gali peržiūrėti
kiti. Šio tipo formalizavimas suteikia pagrindą šiandieninei matematikai, sakė
daktaras Avigadas, Hoskinsono formaliosios matematikos centro (finansuojamas
kriptovaliutų verslininko Charleso Hoskinsono) direktorius, „lygiai taip pat,
kaip Euklidas bandė kodifikuoti ir sudaryti pagrindą to meto matematikai“.
Pastaruoju metu dėmesį patraukia atvirojo kodo patikrinimo
pagalbinė sistema Lean. „Microsoft“ kompanijoje sukurta Leonardo de Mouro, kompiuterių
mokslininko, šiuo metu dirbančio „Amazon“. „Lean“ naudoja automatizuotą
samprotavimą, kuris yra pagrįstas vadinamuoju senamadišku dirbtiniu intelektu
arba GOFAI – simboliniu A.I., įkvėptu logikos. Iki šiol Lean bendruomenė
patvirtino intriguojančią teoremą apie sferos išvertimą iš vidaus, taip pat
pagrindinę teoremą matematinių sferų suvienijimo schemoje, be kitų gambitų.
Tačiau įrodinėjimo asistentas turi ir trūkumų: jis dažnai
skundžiasi, kad nesupranta matematiko įvestų apibrėžimų, aksiomų ar
samprotavimo žingsnių, todėl jis buvo vadinamas „įrodinėjimo verkšleninku“.
Visas tas verkšlenimas gali apsunkinti tyrimus. Tačiau Heather Macbeth,
matematikė iš Fordhamo universiteto, teigė, kad ta pati funkcija – eilučių
grįžtamasis ryšys – taip pat daro sistemas naudingas mokymui.
Pavasarį dr. Macbeth sukūrė „dvikalbį“ kursą: kiekvieną
lentoje pateiktą problemą ji išvertė į Lean kodą paskaitų konspektuose, o
studentai pateikė namų darbų problemų sprendimus tiek Lean, tiek prozoje. „Tai
suteikė jiems pasitikėjimo“, – sakė daktaras Makbetas, nes jie iškart gavo
grįžtamąjį ryšį apie tai, kada buvo baigtas įrodymas ir ar kiekvienas žingsnis
buvo teisingas, ar neteisingas.
Nuo to laiko, kai dalyvavo seminare, Emily Riehl, matematikė
iš Johnso Hopkinso universiteto, naudojo eksperimentinę įrodinėjimo asistento
programą, kad įformintų įrodymus, kuriuos anksčiau paskelbė kartu su
bendraautoriu. Patikrinimo pabaigoje ji pasakė: „Aš tikrai labai giliai
suprantu įrodymą, daug giliau, nei kada nors supratau anksčiau. Aš mąstau taip
aiškiai, kad galiu tai paaiškinti tikrai kvailam kompiuteriui."
Grubi priežastis – bet ar tai matematika?
Kitas automatizuotas samprotavimo įrankis, kurį naudoja
Marijn Heule, kompiuterių mokslininkas iš Carnegie Mellon universiteto ir
„Amazon“ mokslininkas, yra tai, ką jis šnekamojoje kalboje vadina „žiauriu
samprotavimu“ (arba, techniškiau kalbant, Satisfiability arba SAT, sprendėju).
Pasak jo, tiesiog nurodant kruopščiai sukurtą kodavimą, kurį „egzotišką
objektą“ norite rasti, superkompiuterių tinklas slenka per paieškos erdvę ir
nustato, ar tas subjektas egzistuoja, ar ne.
Prieš pat seminarą daktaras Heule ir vienas iš jo aspirantų, Bernardo Subercaseaux, užbaigė savo ilgalaikės problemos
sprendimą, naudodami 50 terabaitų failą. Tačiau šis failas vargu ar lyginamas su
rezultatu, kurį daktaras Heule ir bendradarbiai pateikė 2016 m.: „Dviejų šimtų
terabaitų matematikos įrodymas yra didžiausias visų laikų“, – skelbiama
„Nature“ antraštėje. Toliau straipsnyje buvo klausiama, ar problemų sprendimas,
naudojant tokius įrankius tikrai laikomas matematika. Dr. Heule nuomone, šis
požiūris reikalingas „spręsti problemas, kurių žmonės negali padaryti“.
Kitas įrankių rinkinys naudoja mašininį mokymąsi, kuris
sintezuoja daugybę duomenų ir aptinka reguliarumus, tačiau nemoka loginio,
nuoseklaus samprotavimo. „Google“ „DeepMind“ kuria mašininio mokymosi
algoritmus, kad galėtų susidoroti su baltymų lankstymu (AlphaFold) ir laimėjimu
šachmatuose (AlphaZero). 2021 m. Nature straipsnyje komanda apibūdino savo
rezultatus, kaip „pažangą matematikoje, vadovaujant žmogaus intuicijai su A.I“.
Yuhuai „Tony“ Wu, kompiuterių mokslininkas, anksčiau dirbęs
„Google“, o dabar Įlankoje įsteigęs įmonę, išdėstė didesnį mašininio mokymosi
tikslą: „išspręsti matematiką“. „Google“ daktaras Wu ištyrė, kaip dideli kalbų
modeliai, įgalinantys pokalbių robotus, gali padėti matematikai. Komanda
naudojo modelį, kuris buvo apmokytas, naudojant interneto duomenis, o vėliau
tiksliai suderintas su dideliu matematikos duomenų rinkiniu, naudodamas,
pavyzdžiui, internetinį matematikos ir mokslo darbų archyvą. Kai kasdienine
anglų kalba buvo paprašyta išspręsti matematikos uždavinius, šis specializuotas
pokalbių robotas, pavadintas Minerva, „gana gerai mėgdžiojo žmones“, – seminare
sakė daktaras Wu. Modelis gavo geresnius balus, nei vidutinis 16 metų mokinys
vidurinės mokyklos matematikos egzaminų metu.
Galiausiai, daktaras Wu sakė, kad jis įsivaizdavo
„automatizuotą matematiką“, kuris „gali pati išspręsti matematinę teoremą“.
Matematika kaip lakmuso popierėlis
Matematikai į šiuos įprastinės tvarkos sutrikimus reagavo įvairiai.
Michaelas Harrisas iš Kolumbijos universiteto išreiškia
nepasitenkinimą savo „Silicon Reckoner“ substack. Jam nerimą kelia potencialiai
prieštaringi matematikos tyrimų ir technologijų bei gynybos pramonės tikslai ir
vertybės. Neseniai paskelbtame informaciniame biuletenyje jis pažymėjo, kad
vienas seminaro pranešėjas „A.I. to Assist Mathematical Reasoning“, kurį
organizavo Nacionalinės mokslų akademijos, buvo Booz Allen Hamilton,
vyriausybės rangovo žvalgybos agentūroms ir kariuomenei, atstovas.
Dr. Harrisas apgailestavo, kad trūksta diskusijų apie didesnes
A.I. sistemas ir matematinius tyrimus, ypač „kai priešingai vyksta labai gyvas
pokalbis“ apie technologijas „beveik visur, išskyrus matematiką“.
Geordie Williamsonas iš Sidnėjaus universiteto ir „DeepMind“
bendradarbis kalbėjo N.A.S. susirinko ir paskatino matematikus bei informatikus
labiau įsitraukti į tokius pokalbius. Seminare Los Andžele jis pradėjo savo
pokalbį eilute, pritaikyta iš „Tu ir atominė bomba“, 1945 m. George'o Orwello
esė. „Atsižvelgiant į tai, kaip tikėtina, kad per ateinančius penkerius metus
mes visi būsime labai paveikti, – sakė dr. Williamsonas, – gilus mokymasis nesukėlė
tiek diskusijų, kiek buvo galima tikėtis“.
Dr. Williamsonas mano, kad matematika yra lakmuso
popierėlis, parodantis, ką mašininis mokymasis gali ir ko negali. Samprotavimas
yra esminis matematinio proceso veiksnys, ir tai yra esminė neišspręsta
mašininio mokymosi problema.
Dr. Williamsono ir „DeepMind“ bendradarbiavimo pradžioje
komanda rado paprastą neuroninį tinklą, kuris numatė „matematikos dydį, kuris
man labai rūpėjo“, – sakė jis viename interviu, ir tai padarė „juokingai
tiksliai“. Daktaras Williamsonas sunkiai bandė suprasti, kodėl – tai būtų
teoremos esmė – bet negalėjo. Taip pat negalėjo niekas iš DeepMind. Kaip ir
senovės geometras Euklidas, neuroninis tinklas kažkaip intuityviai atskleidė
matematinę tiesą, tačiau loginis „kodėl“ toli gražu nebuvo akivaizdus.
Los Andželo dirbtuvėse iškili tema buvo, kaip suderinti
intuityvų ir logišką. Jei A.I. galėtų daryti abu tuo pačiu metu, visi statymai
būtų baigti.
Tačiau, pastebėjo daktaras Williamsonas, yra menka
motyvacija suprasti juodąją dėžę, kurią suteikia mašininis mokymasis. „Tai yra
įsilaužimo kultūra technologijų srityje, kur, jei juodoji dėžė veikia didžiąją laiko
dalį, tai puiku“, – sakė jis, "tačiau toks scenarijus palieka matematikus
nepatenkintus".
Jis pridūrė, kad, norint suprasti, kas vyksta neuroniniame
tinkle, kyla „įdomių matematinių klausimų“, o atsakymų radimas suteikia
matematikams galimybę „prasmingai prisidėti prie pasaulio“."
Komentarų nėra:
Rašyti komentarą