New York Times: Ak by umelá inteligencia dokázala spojiť intuíciu a logiku, nemala by hranice

V zbierke Gettyho múzea v Los Angeles sa nachádza portrét starogréckeho matematika Euklida zo 17. storočia: rozcuchaný, so špinavými rukami, v ktorých drží listy „elementov", svojho traktátu o geometrii.

Viac ako 2 000 rokov bol Euklidov text paradigmou matematickej argumentácie a uvažovania. „Euklides je známy tým, že začína ‚definíciami', ktoré sú takmer poetické," uviedol v e-maile Jeremy Avigad, logik z Carnegie Mellon University. „Na nich potom vybudoval vtedajšiu matematiku a dokazoval veci takým spôsobom, že každý nasledujúci krok ‚jasne vyplýval' z predchádzajúcich, pričom používal základné pojmy, definície a predchádzajúce tvrdenia." Dr. Avigad uviedol, že sa vyskytli sťažnosti, že niektoré Euklidove „jasné" kroky boli menej ako jasné, napriek tomu však systém fungoval.

V 20. storočí však matematici už neboli ochotní zakladať matematiku na tomto intuitívnom geometrickom základe. Namiesto toho vytvorili formálne systémy – presné symbolické reprezentácie, mechanické pravidlá. Táto formalizácia nakoniec umožnila preložiť matematiku do počítačového kódu. V roku 1976 sa veta o štyroch farbách, ktorá hovorí, že štyri farby stačia na vyplnenie mapy tak, aby žiadne dve susedné oblasti nemali rovnakú farbu, stala prvou významnou vetou dokázanou pomocou počítačovej hrubej sily.

Matematici teraz zápasia s najnovšou transformačnou silou: umelou inteligenciou.

V roku 2019 Christian Szegedy, počítačový vedec, ktorý predtým pracoval v spoločnosti Google a teraz pôsobí v jednom zo start-upov v Bay Area, predpovedal, že počítačový systém sa do desiatich rokov vyrovná alebo prekoná schopnosť riešiť problémy najlepších ľudských matematikov. Minulý rok tento cieľový dátum upravil na rok 2026.

Akshay Venkatesh, matematik z Institute for Advanced Study v Princetone a držiteľ Fieldsovej medaily za rok 2018, sa v súčasnosti nezaujíma o používanie umelej inteligencie, ale rád o nej hovorí. „Chcem, aby si moji študenti uvedomili, že oblasť, v ktorej pôsobia, sa veľmi zmení," povedal v jednom z minuloročných rozhovorov. Nedávno dodal prostredníctvom e-mailu: „Nie som proti premyslenému a zámernému využívaniu technológií na podporu nášho ľudského chápania. Som však pevne presvedčený, že je podstatná uvedomelosť ohľadom spôsobu, akým ju používame."

Vo februári sa Dr. Avigad zúčastnil na seminári o „strojovo asistovaných dôkazoch" na Inštitúte pre čistú a aplikovanú matematiku na pôde Kalifornskej univerzity v Los Angeles. (V posledný deň seminára navštívil Euklidov portrét.) Na stretnutí sa zišla netypická zmes matematikov a informatikov. „Cítim, že to má význam," povedal Terence Tao, matematik z univerzity, nositeľ Fieldsovej medaily z roku 2006 a hlavný organizátor seminára.

Dr. Tao poznamenal, že len v posledných rokoch sa matematici začali obávať potenciálnych hrozieb umelej inteligencie, či už pre matematickú estetiku alebo pre nich samotných. Podľa jeho slov to, že významní členovia komunity teraz rozoberajú túto problematiku a skúmajú jej možnosti, „trochu narúša tabu".

V prvom rade sedel jeden nápadný účastník seminára: lichobežníková škatuľa s názvom „robot na zdvihnutie ruky", ktorá vydávala mechanický šum a zdvihla ruku vždy, keď mal online účastník otázku. „Pomáha, ak sú roboti roztomilí a neohrozujúci," povedal doktor Tao.

Pripravte sa na „dôkazových nariekačov"

V dnešnej dobe nie je núdza o pomôcky na optimalizáciu nášho života – strava, spánok, cvičenie. „Radi na seba pripájame prístroje, aby sme si uľahčili prácu," povedal Jordan Ellenberg, matematik z Wisconsinskej univerzity v Madisone, počas prestávky na seminári. Dodal, že to isté by mohli urobiť aj prístroje umelej inteligencie pre matematiku: „Je úplne jasné, že otázka znie: Čo môžu stroje urobiť pre nás, a nie čo stroje urobia s nami."

Jeden z matematických nástrojov sa nazýva asistent dôkazov alebo interaktívny overovač tvrdení. („Automath" bol jeho prvou inkarnáciou v 60. rokoch 20. storočia.) Matematik krok za krokom preloží dôkaz do kódu; potom softvérový program skontroluje, či je úvaha správna. Verifikácie sa zhromažďujú v knižnici, dynamickom kánonickom odkaze, do ktorého môžu nahliadnuť ostatní. Dr. Avigad, ktorý je riaditeľom Hoskinsonovho centra pre formálnu matematiku (financovaného kryptopodnikateľom Charlesom Hoskinsonom), povedal, že tento typ formalizácie poskytuje základ pre dnešnú matematiku „presne tak, ako sa Euklides snažil kodifikovať a poskytnúť základ pre matematiku svojej doby".

V poslednom čase priťahuje pozornosť open-source asistenčný systém Lean. Systém Lean, ktorý v spoločnosti Microsoft vyvinul Leonardo de Moura, počítačový vedec, ktorý teraz pracuje v spoločnosti Amazon, využíva automatizované uvažovanie, ktoré je poháňané tzv. starou dobrou umelou inteligenciou alebo GOFAI – symbolickou umelou inteligenciou inšpirovanou logikou. Komunita Lean doteraz okrem iných pokusov overila zaujímavú vetu o obrátení gule naruby, ako aj kľúčovú vetu v schéme na zjednotenie matematických oblastí.

Dôkazový asistent má však aj nevýhody: Často sa sťažuje, že nerozumie definíciám, axiómam alebo úvahovým krokom, ktoré zadáva matematik, a preto sa mu hovorí „dôkazový nariekač". Všetko toto nariekanie môže spôsobiť, že výskum bude ťažkopádny. Heather Macbethová, matematička z Fordhamskej univerzity, však tvrdí, že tá istá vlastnosť – poskytovanie spätnej väzby riadok po riadku – robí tieto systémy užitočné aj na vyučovanie.

Na jar Dr. Macbethová navrhla „bilingválny" kurz: V poznámkach k prednáškam preložila každý problém prezentovaný na tabuli do kódu Lean a študenti predkladali riešenia domácich úloh v Lean aj klasicky. „Dodalo im to sebavedomie," povedala Dr. Macbethová, pretože dostávali okamžitú spätnú väzbu o tom, kedy bol dôkaz hotový a či bol každý krok správny, alebo nie.

Emily Riehlová, matematička z Univerzity Johnsa Hopkinsa, od účasti na seminári použila experimentálny program na formalizáciu dôkazov, ktoré predtým publikovala so spoluautorom. Na konci verifikácie povedala: „Dôkazu som naozaj, ale naozaj hlboko porozumela, oveľa hlbšie, ako som ho kedy predtým chápala. Myslím tak hlboko, že to dokážem vysvetliť aj naozaj hlúpemu počítaču."

Hrubý rozum – ale je to matematika?

Ďalším nástrojom na automatické odôvodňovanie, ktorý používa Marijn Heule, počítačový vedec na Carnegie Mellon University a odborník spoločnosti Amazon, je to, čo hovorovo nazýva „hrubé odôvodňovanie" (alebo, odbornejšie, riešiteľ splniteľnosti alebo SAT). Podľa jeho slov stačí, aby ste pomocou starostlivo vytvoreného kódovania uviedli, aký „exotický objekt" chcete nájsť, a sieť superpočítača prechádza vyhľadávacím priestorom a určuje, či táto entita existuje alebo nie.

Krátko pred seminárom Dr. Heule a jeden z jeho doktorandov Bernardo Subercaseaux dokončili riešenie dlhodobého problému so súborom s veľkosťou 50 terabajtov. Tento súbor sa však sotva dal porovnať s výsledkom, ktorý Dr. Heule a jeho spolupracovníci dosiahli v roku 2016: „Dvestoterabajtový matematický dôkaz je najväčší v histórii," hlásal titulok v časopise Nature. Článok sa ďalej pýtal, či sa riešenie problémov s takýmito nástrojmi skutočne počíta za matematiku. Podľa názoru doktora Heuleho je tento prístup potrebný „na riešenie problémov, ktoré presahujú možnosti ľudí".

Ďalšia skupina nástrojov využíva strojové učenie, ktoré syntetizuje množstvo údajov a zisťuje vzory, ale nie je dobré na logické, postupné uvažovanie. Spoločnosť DeepMind od Googlu navrhuje algoritmy strojového učenia na riešenie takých úloh, ako sú skladanie bielkovín (AlphaFold) a vyhrávanie v šachu (AlphaZero). V článku v časopise Nature z roku 2021 tím opísal svoje výsledky ako „pokrok v matematike prostredníctvom riadenia ľudskej intuície pomocou umelej inteligencie".

Yuhuai „Tony" Wu, počítačový vedec, ktorý predtým pracoval v spoločnosti Google a teraz pôsobí v jednej zo začínajúcich firiem v Bay Area, si stanovil vyšší cieľ strojového učenia: „vyriešiť matematiku". V spoločnosti Google Dr. Wu skúmal, ako by veľké jazykové modely, ktoré umožňujú chatboty, mohli pomôcť v matematike. Tím použil model, ktorý bol vycvičený na internetových údajoch a potom doladený na veľkom súbore údajov bohatých na matematiku, napríklad pomocou online archívu matematických a vedeckých článkov. Keď tento špecializovaný chatbot s názvom Minerva požiadali v bežnej angličtine o riešenie matematických úloh, „celkom dobre napodobňoval ľudí", povedal Dr. Wu na seminári. Model dosiahol výsledky, ktoré boli lepšie, ako má priemerný 16-ročný študent na stredoškolských skúškach z matematiky.

Dr. Wu nakoniec povedal, že si predstavuje „automatizovaného matematika", ktorý „dokáže sám vyriešiť matematickú vetu".

Matematika ako lakmusový test

Matematici reagovali na tieto narušenia s rôznou mierou znepokojenia.

Michael Harris z Kolumbijskej univerzity vyjadruje výhrady na svojej stránke „Silikónový Počtár". Znepokojujú ho potenciálne protichodné ciele a hodnoty výskumnej matematiky a technologického a obranného priemyslu. V nedávnom bulletine si všimol, že jedným z rečníkov na seminári „Umelá inteligencia na pomoc matematickému uvažovaniu", ktorý organizovala Národná akadémia vied, bol zástupca spoločnosti Booz Allen Hamilton, vládneho dodávateľa pre spravodajské agentúry a armádu.

Dr. Harris vyjadril ľútosť nad nedostatkom diskusií o širších dôsledkoch umelej inteligencie na matematický výskum, najmä „v kontraste s veľmi živou diskusiou" o tejto technológii „takmer všade okrem matematiky".

Geordie Williamson z Univerzity v Sydney a spolupracovník spoločnosti DeepMind vystúpil na stretnutí N.A.S. a vyzval matematikov a informatikov, aby sa viac zapájali do takýchto diskusií. Na seminári v Los Angeles otvoril svoju prednášku vetou upravenou z eseje Georgea Orwella Vy a atómová bomba z roku 1945. „Vzhľadom na to, aké je pravdepodobné, že nás všetkých v najbližších piatich rokoch hlboko ovplyvní," povedal Dr. Williamson, „hlboké učenie nevzbudilo toľko diskusií, ako by sa dalo očakávať."

Dr. Williamson považuje matematiku za lakmusový test toho, čo strojové učenie dokáže alebo nedokáže. Uvažovanie je kvintesenciou matematického procesu a je kľúčovým nevyriešeným problémom strojového učenia.

Na začiatku spolupráce Dr. Williamsona s DeepMind tím našiel jednoduchú neurónovú sieť, ktorá predpovedala „veličinu v matematike, na ktorej mi veľmi záležalo", povedal v rozhovore, a to až „smiešne presne". Dr. Williamson sa veľmi snažil pochopiť prečo – čo by bol základ tvrdenia – ale nedokázal to. Nedokázal to ani nikto v DeepMind. Podobne ako staroveký geometer Euklides, aj neurónová sieť nejako intuitívne rozoznala matematickú pravdu, ale logické „prečo" ani zďaleka nebolo zrejmé.

Na seminári v Los Angeles bolo hlavnou témou, ako spojiť intuíciu a logiku. Ak by umelá inteligencia dokázala robiť oboje naraz, nemala by žiadne limity.

Dr. Williamson však poznamenal, že motivácia pochopiť čiernu skrinku, ktorú predstavuje strojové učenie, je mizivá. „Je to typická kultúra v technike, kde, ak to väčšinu času funguje, je to skvelé," povedal – ale s týmto scenárom sú matematici nespokojní.

Dodal, že snaha pochopiť  čo sa deje vo vnútri neurónovej siete, vyvoláva „fascinujúce matematické otázky" a hľadanie odpovedí predstavujú pre matematikov príležitosť „zmysluplne prispieť svetu".

Článok pôvodne vyšiel v denníku New York Times. Všetky práva vyhradené.