A neurális hálózatok ma már képesek kifinomult matematikai levezetéseket, releváns premisszákat, sőt hasznos sejtéseket is megjósolni. Christian Szegedy, a Google Research mesterséges intelligenciával foglalkozó magyar kutatója viszont csapatával egy olyan rendszert épít, ami tíz éven belül túlszárnyalhatja a matematikusok legvadabb álmait is: az automatizált matematikus olyan szinten képes lesz a tudósok „munkatársává” válni, hogy rutinból ellenőrzi majd azokat a bizonyításokat, amelyeket csak néhány ember képes megérteni a Földön, levezetésük pedig éveket vehet igénybe, és képes lehet olyan új matematikai dimenziók megnyitására, amelyekről ma még fogalmunk sincs.

Habár 2018-ban a vezető AI-szakértők 2060-ra tették annak valószínűségét, hogy a gépek rutinból, autonóm módon a legnevesebb matematikai szakfolyóiratokban publikálható bizonyításokat állítsanak elő úgy, hogy a bizonyítandó tételek is a neurális hálók gépagyából pattannak ki, Szegedy a SZTAKI és a Rényi MILAB Mesterséges Intelligencia Alapkutatás Szeminárium keretében megtartott, szerdai előadásában már a következő évtizedre jósolja ennek megvalósulását. Kérdés, észrevenné-e bárki, ha valaki egy szaklaphoz megpróbálna benyújtani egy AI által írt bizonyítást, vagy inkább az történne, ami az OpenAI GPT-3 nevű, mélytanulást használó, autoregresszív nyelvi modellje által írt blogposzttal – a legtöbb kommentelő nem vette észre, hogy nem ember írta a cikket. Ez persze egyelőre hipotetikus felvetés, viszont az, hogy mire képes jelenleg a rendszer, hová tart és mik a kihívásai, már kevésbé.

Qubit: A kutatócsoport célja egy olyan rendszer létrehozása, amely képes értelmezni és formalizálni a természetes nyelvi matematikát. Ezt hogy kell elképzelni?

Christian Szegedy: Igazából a hosszú távú cél kicsit más. Ezzel sokan egyetértenek, mások pedig nem, de én úgy vélem, így vezet az út az én hosszú távú vízióm felé: olyan rendszert szeretnék létrehozni, amellyel úgy lehet programozni, mintha egy emberrel lépnénk interakcióba. Vagyis az AI valójában egy embert szimulál, amivel ugyanúgy lehet kommunikálni, mint egy másik emberrel, és lényegében a programozás összes feladatát elvégzi automatikusan. Csak szerintem ehhez a matematika formalizálásán keresztül vezet az út, mert létre kell hozni egy gépet, ami gyakorlatilag ugyanolyan mélységben és ugyanolyan képességekkel tud érvelni meg bebizonyítani azt, hogy például egy program korrekt, mint egy ember.

Ez egy viszonylag nehéz feladat, és akkor már egyszerűbb megoldani előtte a matematikát. Viszont ezt nem lehet csak úgy, vákuumban megtenni, mert a matematika nagyon szerteágazó témakör, és ha azt mondom, hogy szeretnék egy rendszert, ami fölfedezi a matematikát, ez nem egy jól definiált kérdés. Igazából a matematika olyan nagy, hogy fontos feladat eldönteni, melyik részét fedezze fel és értse meg a mesterséges intelligencia.

Úgyhogy szerintem a legbiztonságosabb és legészszerűbb eljárás azt megértetni vele, amit az emberek érdekesnek találnak, ezért végül is kifejlesztettünk valamit annak mentén, hogy mi az érdekes matematika, bár az érdekesség fogalmát szintén nem lehet formalizálni. Nem tudjuk azt mondani a gépnek, hogy fedezzen fel érdekes matematikát.

Az első lépés tehát az, hogy a gépek megértsék, mit tart az ember érdekesnek. De ahhoz a számítógépnek el kell olvasnia, meg kell értenie az emberi matematikát. És mivel a legtöbb matematika nem formális, a gépek számára értelmezhető, hanem informális formában van – tehát olyan cikkek formájában, amelyeket az emberek olvasnak –, nagyon nehéz feladat, hogy a gép a természetes nyelvből megértse a matematikát. Hiába néz ki egy laikus számára egy matematikai cikk nagyon formálisnak, a valóságban nem az. Tele van hatalmas logikai ugrásokkal, slampos megoldásokkal, ami néha azok számára sem nyilvánvalóan dekódolható, akik évekig tanultak matematikát. Egy matematikai cikkből néha egy óra gondolkodás megérteni két mondatot, úgyhogy ezek az írások ebből a szempontból néha informálisabbak, mint sok informálisnak gondolt tartalom.

Szerintem mégis ezen keresztül vezet az út, és ennek megvan az a mellékhatása is, hogy akkor formálisan le tudjuk ellenőrizni az összes létező matematikai korpuszt, mert a gép tudná formalizálni és ellenőrizni, hogy a bizonyítások tényleg jók-e. Ezekben mindenféle apró dolgokon el lehet csúszni, és lehetnek bennük szubsztanciális hibák is, ami gyakran ténylegesen elő is fordul.

Qubit: Hol tart most a folyamat? Milyen időtávlatokban lehet gondolkozni a mesterségesen intelligens matematikus létrehozásakor?

Christian Szegedy: Én nagyon optimista vagyok, de igazából az egész még nagyon gyerekcipőben jár. Viszont ezek mind exponenciális folyamatok, szóval amikor valamit megoldunk, akkor hirtelen lehetőségek tárháza nyílik meg, és hirtelen ugrásokkal fejlődik a terület. A legelején mindig úgy néz ki, mintha apró lépésekkel haladnánk, aztán egyszerre csak elérik azt a szintet, amikor már olyanok a képességek, hogy hirtelen érdekessé válik az ember számára. Ez úgy néz ki, mintha a semmiből előjött volna, pedig ha megnézi az ember az exponenciális görbe elejét, ott is ugyanolyan impresszív dolgok zajlanak, és szerintem most ugyanez történik.

Például vannak az újfajta neuronháló-architektúrát jelentő transzformereket használó nagy nyelvi modellek, mint amilyen a Google fordítóprogramja, és ezekkel már olyan fantasztikus képességeket lehet felmutatni, amelyek három évvel ezelőtt még nagyon meglepőnek tűntek volna, manapság viszont már mindenki elfogadja őket. Ezekkel olyanokat lehet csinálni, mint amit az egyik cikkünkben csináltunk: kitöröl az ember mindenféléket egy matematikai állításból, és az algoritmus viszonylag jó pontossággal kitalálja a hiányzó részeket. Ez ugyanaz az eljárás, mint amit az OpenAI használ arra, hogy cikkeket generáljon vagy végigfuttasson a szövegen egy érzelemelemzést (sentiment analysis). Ha ezeket megfelelően tréningelik, akkor ezek már kezdik megközelíteni azt a szintet, ahogyan az ember bánik a nyelvvel.

Qubit: És mit szólnak a matematikusok ahhoz, hogy épül egy ilyen rendszer? Elég nagy az ellenállás az MI-vel szemben, és bár lehet, hogy főleg a laikusok körében, de sokakban él a félelem, hogy jön az algoritmus, és elveszi a munkájukat.

Christian Szegedy: A matematikusok azért viszonylag nyitott, racionálisan gondolkozó emberek, de ennek kapcsán mindenesetre kétféle álláspontot látok. A matematikusok 95 százaléka úgy gondolja, hogy ez az ő életükben már nem valósul meg, őket ez nem érinti, rövid távon, egy évtizeden belül meg pláne nem fog megtörténni - miközben tíz éven belül ez szerintem realitás lesz. A maradék 5 százalék pedig érdekesnek tartja az elképzelést. A matematikának ugye nemcsak az a lényege, hogy magas szinten tudjunk megoldani feladatokat, hanem egyszerűen az, hogy az ember kíváncsi, és problémákat akar megoldani, amik a valóságban előfordulnak.

Itt gyakorlatilag a gép úgy működik majd, mint egy mikroszkóp, ami nélkül nem látnánk a részecskéket. Vagyis ez is betekintést nyújt majd olyan struktúrák viselkedésébe, amelyek megértésére az emberi agy képtelen. Ez olyan lesz, mintha lenne az embernek egy iszonyatosan zseniális matematikus barátja, és bárrmit kérdezhetne tőle.

Qubit: Vásárhelyi Orsi adattudós egyebek mellett azt kutatja, hogy ha egy csapatba botok kerülnek be, akkor hogyan változik meg köztük a viszony. Ő azt találta, hogy elkezdenek gyengülni az emberi kapcsolatok. Lát hasonló veszélyt az automatizált matematikus esetén?

Christian Szegedy: Nyilván van ilyen veszély, igen. De egyébként az is lehet, hogy bizonyos szempontból az emberek csak hátráltatják a dolgokat. Például a Go játékban korábban kipróbáltak olyan csapatokat, amelyekben számítógép és ember is volt, és ők egyszerűen rosszabbul játszottak, mint azok a csapatok, amelyekben csak gépek kaptak helyet. A legelején, mikor még a sakkgépek majdnem olyan jók vagy csak kicsit jobban voltak, mint az ember, még segített az emberi intuíció, de egy idő után, amikor a sakkgépek sokkal jobban lettek, az ember már hátráltató tényezővé vált.

Szóval bizonyos dolgokban ahhoz, hogy megoldjanak egy problémát, a gépek annyira jók lesznek, hogy nem fog szerepet játszani az ember. Viszont abban, hogy milyen problémát oldjanak meg, vagy hogy azt hogy alkalmazzák a valóságra, ott továbbra is kikerülhetetlen marad az ember.

Qubit: Hogyan lehet egy ilyen rendszert ellenőrizni? Ha annyival jobb lesz, mint az ember, honnan fogjuk tudni, hogy mit művel?

Christian Szegedy: Éppen ez az előnye annak az útnak, amit én javaslok, ami formalizálja a matematikát, és így az embernek ismerős nyelven formába önti az algoritmikus gondolkodást. Mert az is lehetséges út lett volna, hogy egyszerűen csak megengedjük a gépnek, hogy tanulja meg a maga nyelvén a matematikát, és mondjon mindenfélét. Akkor azt az emberek kénytelenek lennének elhinni neki, de ez az eljárás, amit én javaslok, azon alapul, hogy használunk olyan formális bizonyító rendszereket, amik teljesen gépiesen leellenőrizhetők. Tehát emberek egy nagyon pici, ezer soros kis programmal utánamehetnek, mit csinált az AI. Ezt a programot megírhatják tíz különböző példányban, tíz különböző módon, és működik. Végeredményben pedig ott lesz az összes formális bizonyítás, még akkor is, ha sok milliárd vagy trillió lépéses bizonyításokról lesz szó, és egy gyors számítógéppel, mechanikus lépésekkel ellenőrizhető marad.

Qubit: Tehát ha jól értem, egy másik algoritmus fogja ellenőrizni a matematikus algoritmust.

Christian Szegedy: Igen, ez egy sztenderd eljárás, már most is ezt csináljuk. Van egy nagyon egyszerű ellenőrző mag, ami pár száz vagy pár ezer soros kód. Az ember oda elküldi a matematikai bizonyítást, ami le van bontva apró, pici lépésekre, ahol minden kis lépést triviális leellenőrizni, és ez a nagyon egyszerű ellenőrző mag nézi át a bizonyításokat. De nagyon nehéz is lenne a bizonyításokra megerősítéses tanulási (reinforcement learning) rendszert létrehozni, ha nem lenne ellenőrző rendszer, ami megnézi, helyesek-e a bizonyítások. És az nem egy gépi tanuló rendszer, hanem egy teljesen mechanisztikus ellenőrző mag.

Qubit: A kérdés csak amiatt vetődik fel, mert vannak olyan algoritmusok, amelyeknél a logikai lépések, amik mentén döntést hoz, nem visszafejthetők, vagyis fekete doboz modellek, ahol a kimeneti-bemeneti értékeket ismerjük kívülről, a logikát viszont nem.

Christian Szegedy: Igen, ez létezik, de a kettő nem zárja ki egymást. Az, hogy az algoritmus létrehoz matematikai bizonyításokat, az más, mint megérteni, hogyan jött létre az a bizonyítás. Tehát le lehet ellenőrizni, hogy tényleg azt csinálja-e, amit akart az ember, de maguk a bizonyítást létrehozó gépi tanuló rendszerek tényleg úgy működnek, mint a fekete dobozok, vagyis sosem fogjuk teljesen megérteni őket. Minél szofisztikáltabb, annál kevésbé fogjuk tudni, hogy működött. Mégis létre fog hozni matematikai bizonyításokat, néha jót, néha rosszat, és az ellenőrző rendszer utána majd visszadobja, hogy ezt elrontotta. Ugyanúgy, ahogy az embernél is, néha hibázunk. Az AI is el fog rontani dolgokat, de tanul majd belőle.

Qubit: Nem félelmetes, hogy itt egy rendszer, és nem tudjuk, minek alapján lép? Ez Douglas Adams Bölcs Elme nevű szuperszámítógépét idézi, ami ugyan megmondta, hogy a válasz az élet végső kérdésére meg mindenre 42, de hogy mi a végső kérdés, azt már nem lehet pontosan tudni.

Christian Szegedy: Van egy ilyen irány, igen, de szerintem ez szükségszerű irány. Ezek a rendszerek valahol a káosz és a mechanisztikus rend határán helyezkednek el. A dolog erejét az adja, hogy ezeket nem lehet annyira megérteni. Lényegében sztochasztikus alapon működnek, amiben az emberek nem túl jók. Rengeteg különböző esemény valószínűségét össze tudják hasonlítani belül, és akkor az ember nem tudja igazán megérteni, milyen komponensek játszottak szerepet egy döntés megszületésében, mert annyi különböző tulajdonságnak a súlyát és valószínűségét kellene összehasonlítani, amire az ember nem képes, ezek a rendszerek viszont annál inkább.

Mindez azért érdekes, mert az emberi intuíció is így működik, és ezért nem tudták sokáig mechanizálni, de lényegében a gépek kezdik az embert felülmúlni az intuíció terén – pont ott, ahol úgy tűnt, hogy az emberek jobbak. Ez öt-hat évvel ezelőtt hirtelen eltűnt: a gépek most már jobbak az intuitív dolgok kifejlesztésében, mint az ember.

Kapcsolódó cikkek a Qubiten: