Jeremy Avigad, një logjikist në Universitetin Carnegie Mellon, në blu, me studentët gjatë një shkolle verore “Formalizimi i Matematikës” në Institutin e Shkencave Matematikore Simons Laufer në Berkeley, Kaliforni
Në koleksionin e muzeut ‘Getty’ në Los Anxhelos është një portret nga shekulli i 17-të i matematikanit të lashtë grek Euklid: i çrregullt, duke mbajtur lart fletët e ‘Elementeve’, traktatin e tij mbi gjeometrinë, me duar të papastra.
Për më shumë se 2000 vjet, teksti i Euklidit ishte paradigma e argumentimit dhe arsyetimit matematik. “Euklidi fillon me ‘përkufizime’ që janë pothuajse poetike,” tha Jeremy Avigad, një logjikist në Universitetin Carnegie Mellon, në një email.
“Ai më pas ndërtoi matematikën e kohës mbi të, duke i vërtetuar gjërat në një mënyrë të tillë që çdo hap i njëpasnjëshëm ‘të ndjekë qartë’ hapat e mëparshëm, duke përdorur nocionet bazë, përkufizimet dhe teoremat e mëparshme.”
Kishte ankesa se disa nga hapat ‘e qartë’ të Euklidit ishin më pak se të dukshme, tha Dr. Avigad, megjithatë sistemi funksionoi.
Por nga shekulli i 20-të, matematikanët nuk ishin më të gatshëm ta bazonin matematikën në këtë bazë gjeometrike intuitive. Në vend të kësaj ata zhvilluan sisteme formale – paraqitje të sakta simbolike, rregulla mekanike.
Përfundimisht, ky zyrtarizim lejoi që matematika të përkthehej në kod kompjuterik. Në vitin 1976, teorema me katër ngjyra – e cila thotë se katër ngjyra janë të mjaftueshme për të mbushur një hartë në mënyrë që të mos ketë dy rajone ngjitur me të njëjtën ngjyrë – u bë teorema e parë kryesore e provuar me ndihmën e forcës brutale llogaritëse.
Tani matematikanët po përballen me forcën më të fundit shndërruese: inteligjencën artificiale.
Në vitin 2019, Christian Szegedy, një shkencëtar kompjuteri dikur në Google dhe tani në një start-up në Zonën e Gjirit, parashikoi se një sistem kompjuterik do përputhej ose tejkalonte aftësinë për zgjidhjen e problemeve të matematikanëve më të mirë njerëzorë brenda një dekade. Vitin e kaluar ai rishikoi kohën e synuar brenda vitit 2026.
Akshay Venkatesh, një matematikan në Institutin për Studime të Përparuara në Princeton dhe një fitues i Medaljes Fields në vitin 2018, aktualisht nuk është i interesuar të përdorë A.I. (Artificial Intelligence), por ai është i etur të flasë për të.
“Dua që studentët e mi të kuptojnë se fusha në të cilën ata janë do ndryshojë shumë,” tha ai në një intervistë vitin e kaluar. Ai së fundmi shtoi me email: “Unë nuk jam kundër përdorimit të studiuar dhe të qëllimshëm të teknologjisë për të mbështetur mirëkuptimin tonë njerëzor. Por unë besoj fuqimisht se vetëdija për mënyrën se si e përdorim është thelbësore.”
Në shkurt, Dr. Avigad ndoqi një seminar rreth ‘provave të ndihmuara nga makineritë’ në Institutin për Matematikën e Pastër dhe të Aplikuar, në kampusin e Universitetit të Kalifornisë, Los Anxhelos. (Ai vizitoi portretin e Euklidit në ditën e fundit të seminarit.) Mbledhja tërhoqi një përzierje atipike matematikanësh dhe shkencëtarësh kompjuterikë.
“Ka një ndjesi që ndihet logjikisht,” tha Terence Tao, një matematikan në universitet, fitues i një Medalje Fields në 2006 dhe organizatori kryesor i seminarit.
Organizatorët e shkollës verore, nga e majta: Dr. Avigad, Patrick Massot nga Universiteti Paris-Saclay dhe Heather Macbeth nga Universiteti Fordham
Dr. Tao vuri në dukje se vetëm në dy vitet e fundit matematikanët kanë filluar të shqetësohen për kërcënimet e mundshme të A.I., qoftë për estetikën matematikore apo për veten e tyre. Ai tha se anëtarët e shquar të komunitetit tani po shqyrtojnë çështjet dhe po eksplorojnë potencialin ‘që mund të thyejë tabutë’.Një pjesëmarrës i dukshëm i seminarit u ul në rreshtin e parë: një kuti trapezoidale e quajtur ‘roboti me dorë’ që lëshonte një zhurmë mekanike dhe e ngrinte dorën sa herë që një pjesëmarrës në internet kishte një pyetje.
“Kjo ndihmon nëse robotët janë të lezetshëm dhe jo kërcënues,” tha Dr. Tao.
‘Nxirrni ‘ankuesit e provave’
Këto ditë nuk ka mungesë të pajisjeve për optimizimin e jetës sonë – dietë, gjumë, stërvitje.
“Ne na pëlqen t’i bashkojmë gjëra vetes për ta bërë pak më të lehtë t’i rregullojmë gjërat,” tha Jordan Ellenberg, një matematikan në Universitetin e Wisconsin-Madison, gjatë një pushimi seminari. A.I. Gadgetry mund të bëjë të njëjtën gjë për matematikën, shtoi ai: “Është shumë e qartë se pyetja është, çfarë mund të bëjnë makinat për ne, jo çfarë do të bëjnë makinat me ne.”
Një pajisje matematikore quhet një asistent provash, ose provë e teoremës interaktive. (“Automath” ishte një mishërim i hershëm në vitet 1960.) Hap pas hapi, një matematikan përkthen një provë në kod; atëherë një program softuer kontrollon nëse arsyetimi është i saktë. Verifikimet grumbullohen në një bibliotekë, një referencë kanonike dinamike me të cilën të tjerët mund të këshillohen.
Ky lloj formalizimi ofron një bazë për matematikën sot, tha Dr. Avigad, i cili është drejtor i Qendrës Hoskinson për Matematikën Formale (financuar nga sipërmarrësi i kriptove Charles Hoskinson), ‘në të njëjtën mënyrë që Euklidi po përpiqej të kodifikonte dhe siguron një bazë për matematikën e kohës së tij’.
Kohët e fundit, sistemi i asistencës me burim të hapur Lean po tërheq vëmendjen. Zhvilluar në Microsoft nga Leonardo de Moura, një shkencëtar kompjuteri tani te Amazon, Lean përdor arsyetimin e automatizuar, i cili mundësohet nga ajo që njihet si inteligjenca artificiale e mirë e modës së vjetër, ose GOFAI – A.I. simbolike, e frymëzuar nga logjika.
Deri tani, komuniteti Lean ka verifikuar një teoremë intriguese në lidhje me kthimin e një sfere nga brenda jashtë, si dhe një teoremë kryesore në një skemë për unifikimin e sferave matematikore, midis gambiteve të tjera.
Emily Riehl, një matematikane në Universitetin Johns Hopkins, ka përdorur një program eksperimental të ndihmës provash
Por një asistent provash ka edhe të meta: ai shpesh ankohet se nuk i kupton përkufizimet, aksiomat ose hapat e arsyetimit të futura nga matematikani, dhe për këtë është quajtur një ‘ankues provash’. I gjithë ky rënkim mund ta bëjë kërkimin të vështirë. Por Heather Macbeth, një matematikane në Universitetin Fordham, tha se e njëjta veçori – duke ofruar reagime rresht pas rreshti – gjithashtu i bën sistemet të dobishme për mësimdhënie.
Në pranverë, Dr. Makbeth krijoi një kurs ‘dygjuhësh’: Ajo përktheu çdo problem të paraqitur në dërrasën e zezë në kodin Lean në shënimet e leksionit dhe studentët paraqitën zgjidhje për problemet e detyrave të shtëpisë si në Lean ashtu edhe në prozë.
“Kjo u dha atyre besim,” tha Dr. Macbeth, sepse ata morën reagime të menjëhershme se kur mbaroi prova dhe nëse çdo hap gjatë rrugës ishte i drejtë apo i gabuar.
Që nga ndjekja e seminarit, Emily Riehl, një matematikane në Universitetin Johns Hopkins, përdori një program eksperimental ‘asistent provash’ për të zyrtarizuar provat që ajo kishte botuar më parë me një bashkëautor. Në fund të një verifikimi, ajo tha: “Unë jam vërtet, shumë e thellë në të kuptuarit e provës, shumë më thellë se sa kam kuptuar ndonjëherë më parë. Unë jam duke menduar aq qartë sa mund t’ia shpjegoj atë edhe një kompjuteri vërtet memec’.
Arsyeja brutale – por a është matematikë?
Një tjetër mjet i automatizuar i arsyetimit, i përdorur nga Marijn Heule, një shkencëtar kompjuteri në Universitetin Carnegie Mellon dhe një studiues i Amazon, është ajo që ai e quan në mënyrë bisedore ‘arsyetimi brutal’ (ose, më teknikisht, një Satisfiability, ose SAT). Thjesht duke deklaruar, me një kodim të krijuar me kujdes, cilin ‘objekt ekzotik’ dëshironi të gjeni, tha ai, një rrjet superkompjuterësh kalon nëpër një hapësirë kërkimi dhe përcakton nëse ai entitet ekziston apo jo.
Pak përpara seminarit, Dr. Heule dhe një nga doktorantët e tij, studenti Bernardo Subercaseaux, finalizuan zgjidhjen e tyre për një problem të gjatë me një skedar me madhësi 50 terabajt. Megjithatë, ai skedar vështirë se krahasohet me një rezultat që Dr. Heule dhe bashkëpunëtorët e prodhuan në vitin 2016: “Dëshmia e matematikës me dyqind terabajt është më e madhja ndonjëherë”, njoftoi një titull në revistën Nature.
Shkrimi vazhdoi të pyeste nëse zgjidhja e problemeve me mjete të tilla llogaritet vërtet si matematikë. Sipas mendimit të Dr. Heule, kjo qasje është e nevojshme ‘për të zgjidhur problemet që janë përtej asaj që njerëzit mund të bëjnë’.
Marijn Heule dhe një student kohët e fundit përdorën një mjet të automatizuar të arsyetimit për të zgjidhur problemin e “ngjyrosjes së paketimit”, disi si problemi i hartës me katër ngjyra, por shumë më i ndërlikuar
Një grup tjetër mjetesh përdor mësimin e makinerive, i cili sintetizon shumë të dhëna dhe zbulon modele, por nuk është i mirë në arsyetimin logjik hap pas hapi. DeepMind i Google harton algoritme të mësimit të makinerive për të trajtuar gjëra të tilla si palosja e proteinave (AlphaFold) dhe fitorja në shah (AlphaZero). Në një punim të vitit 2021 në Nature, një ekip i përshkroi rezultatet e tyre si ‘përparimi i matematikës duke udhëhequr intuitën njerëzore me A.I’.
Yuhuai ‘Tony’ Wu, një shkencëtar kompjuteri dikur në Google dhe tani me një start-up në Zonën e Gjirit, ka përshkruar një qëllim më madhështor të të mësuarit të makinerive: ‘të zgjidhë matematikën’.
Në Google, Dr. Wu eksploroi se si modelet e mëdha të gjuhës që fuqizojnë chatbots mund të ndihmojnë me matematikën. Ekipi përdori një model që u stërvit mbi të dhënat e internetit dhe më pas u rregullua në një grup të madh të dhënash të pasura me matematikë, duke përdorur, për shembull, një arkiv në internet të letrave matematikore dhe shkencore.
Kur u pyet në anglishten e përditshme për të zgjidhur probleme matematikore, ky chatbot i specializuar, i quajtur Minerva, ishte ‘shumë i mirë në imitimin e njerëzve’, tha Dr. Wu në seminar. Modeli mori rezultate që ishin më të mira se një student mesatar 16-vjeçar në provimet e matematikës në shkollë të mesme.
Në fund të fundit, tha Dr. Wu, ai parashikoi një ‘matematikan të automatizuar’ që ka ‘aftësinë për të zgjidhur një teoremë matematikore vetë’.
Matematika si test lakmus
Matematikanët i janë përgjigjur këtyre ndërprerjeve me nivele të ndryshme shqetësimi. Michael Harris, në Universitetin e Kolumbias, shpreh shqetësime në nënstivat e tij “Silicon Reckoner”. Ai është i shqetësuar nga qëllimet dhe vlerat potencialisht konfliktuale të matematikës kërkimore dhe industrisë së teknologjisë dhe mbrojtjes.
Në një buletin të fundit, ai vuri në dukje se një folës në një seminar, “A.I. për të ndihmuar arsyetimin matematikor”, organizuar nga Akademitë Kombëtare të Shkencave, ishte një përfaqësues nga Booz Allen Hamilton, një kontraktor qeveritar për agjencitë e inteligjencës dhe ushtrinë.
Dr. Harris u ankua për mungesën e diskutimit rreth implikimeve më të mëdha të A.I. në kërkimin matematikor, veçanërisht ‘kur është në kontrast me bisedën shumë të gjallë që po ndodh’ për teknologjinë ‘pohuajse kudo përveç matematikës’.
Geordie Williamson, nga Universiteti i Sidneit dhe një bashkëpunëtor i DeepMind, foli në N.A.S. duke mbledhur dhe nxitur matematikanët dhe shkencëtarët e kompjuterave që të përfshihen më shumë në biseda të tilla. Në seminarin në Los Anxhelos, ai e hapi fjalimin e tij me një rresht të përshtatur nga “Ti dhe bomba atomike”, një ese e vitit 1945 nga George Orwell.
“Duke pasur parasysh sa gjasa kemi të gjithë ne që të ndikojmë thellësisht brenda pesë viteve të ardhshme,” tha Dr. Williamson, ‘të mësuarit e thellë nuk ka ngjallur aq shumë diskutime sa mund të pritej’.
Yuhuai “Tony” Wu, një shkencëtar kompjuteri në Zonën e Gjirit, parashikon një “matematicien të automatizuar” – një asistent kërkimor me qëllim të përgjithshëm që ka “aftësinë për të zgjidhur një teoremë matematikore vetë”
Dr. Williamson e konsideron matematikën një provë lakmusi të asaj që mësimi i makinerive mund ose nuk mund të bëjë. Arsyetimi është thelbësor për procesin matematikor dhe është problemi thelbësor i pazgjidhur i mësimit të makinerive.
Në fillim të bashkëpunimit të Dr. Williamson me DeepMind, ekipi gjeti një rrjet të thjeshtë nervor që parashikonte ‘një sasi në matematikë për të cilën më interesonte shumë’, tha ai në një intervistë, dhe e bëri këtë ‘me saktësi të frikshme’.
Dr. Williamson u përpoq shumë të kuptonte pse – kjo do ishte krijimi i një teoreme – por nuk mundi. Askush nuk mundi në DeepMind. Ashtu si gjeometri i lashtë Euklidi, rrjeti nervor kishte dalluar disi intuitivisht një të vërtetë matematikore, por ‘pse-ja’ logjike e saj nuk ishte aspak e qartë.
Në seminarin e Los Anxhelosit, një temë e spikatur ishte se si të kombinohen intuitivja dhe logjika. Nëse A.I. mund t’i bënte të dyja në të njëjtën kohë, të gjitha bastet do anuloheshin.
Por sipas Dr. Williamson, ka pak motivim për të kuptuar ‘kutinë e zezë’ që paraqet mësimi i makinerive. “Është kultura e hakerëve në teknologji, ku nëse funksionon shumicën e kohës, kjo është e mrekullueshme,” tha ai – por ky skenar i lë matematikanët të pakënaqur.
Ai shtoi se përpjekja për të kuptuar se çfarë ndodh brenda një rrjeti nervor ngre ‘pyetje magjepsëse matematikore’ dhe se gjetja e përgjigjeve paraqet një mundësi për matematikanët ‘që të kontribuojnë në mënyrë kuptimplotë për botën’.
VINI RE: Ky material është pronësi intelektuale e New York Times
Përgatiti për Hashtag.al, K.Manjani
