A mesterséges intelligencia már nemcsak számol
Ezzel a fejleménnyel óriási fordulat érkezett el. Eddig az emberi kreativitás és intuíció párosult a számítástechnika gyorsaságával, de az MI most egy lépéssel továbbment: logikai érvelést is képes támogatni, nemcsak számításokat végez. Matematikusok hosszú évtizedek óta dolgoznak egyre nagyobb apparátussal, hiszen a modern bizonyítások már hatalmas koncepcionális kereteket, összetett logikai láncolatokat és óriási eredménytárakat foglalnak magukba, amit egyetlen ember képtelen átlátni.
Korábban is előfordult, hogy számítógép segített: ilyen volt a négy szín tétele vagy a Kepler-sejtés. Most viszont az MI már nemcsak egy mechanikus segéd, hanem autonóm résztvevő a bizonyításban, különösen a formális bizonyításellenőrző programok – például a Lean – használatával.
Formális nyelvek és bizonyítási könyvtárak
A Lean és a hozzá hasonló formalizáló nyelvek lépésről lépésre vizsgálják, hogy minden definíció és következtetés precízen, logikailag megalapozottan halad-e. Ezekben a rendszerekben nincs semmiféle „ugrás” vagy kimondatlan feltevés: amit a rendszer elfogad, az ténylegesen igaznak tekinthető. Az utóbbi években elképesztő méretű bizonyítási könyvtárak jöttek létre, amelyekben rengeteg definíció és tétel található már előre igazolt formában, lehetővé téve, hogy új problémákat is beemeljenek a rendszerbe.
Egészen mostanáig azonban egy áttörő eredmény formális leírása és ellenőrzése hónapokat vagy éveket vett igénybe, rendkívüli szakértelmet megkövetelve.
A gömbpakolás áttörése
Ebben a kontextusban kell értelmezni a mostani szenzációs előrelépést, amikor az MI képes volt formálisan igazolni Viazovska legendás nyolc- és huszonnégy dimenziós gömbpakolási bizonyítását. Ez a matematikai probléma arra kérdez rá, hogy hány azonos gömb fér el hézag nélkül a különböző dimenziójú terekben. A háromdimenziós változaton túl, egészen 2022-ig szinte semmit nem tudtunk a magasabb dimenziós esetekről – Viazovska áttörő bizonyítása tette lehetővé, hogy erre választ kapjunk.
Most először sikerült az MI-nek és az embereknek közösen Lean-kódba átültetni ezt a nagyszabású bizonyítást, lépésről lépésre géppel igazolva annak helyességét. A Xena nevű startup Gauss nevű logikai MI-je kulcsszereplő volt ebben: bár az emberi kutatóknak kellett felállítani az alapstruktúrát, onnantól a rendszer villámgyorsan töltötte ki a hiányzó részeket. Először a nyolc-, majd a huszonnégy dimenziós esetet ellenőrizték le.
Új munkamódszerek és határok
Idővel ez a gyakorlat egészen új munkamódszereket vezethet be a matematika világába. Terence Tao Fields-érmes matematikus szerint az MI elsőre nem feltétlenül a legbonyolultabb problémákat oldja meg, hanem az időigényes, monoton részleteket veszi le a vállunkról. Ez felszabadítja a szakembereket, hogy inkább kreatív stratégiákon dolgozzanak, miközben az MI gondoskodik a logikai alaposságról.
Kevin Buzzard, a témában jártas kutató szerint nem mindegy, milyen MI-típusokkal dolgozunk. Fontos, hogy formális ellenőrzést is alkalmazzunk, ne csak olyan nagy nyelvi modelleket, amelyekben nincs garancia a helyességre. A Leanhoz hasonló rendszerek azért hasznosak, mert zárt módon, minden hézagot kizárva igazolnak.
Úgy tűnik, hogy bár a matematika nem lesz könnyebb, az MI-vel egyre biztosabban és gyorsabban tudjuk majd ellenőrizni az eddig elképzelhetetlenül összetett bizonyításokat. Ugyan a matematikusok szerepe nem tűnik el, de a hangsúly átrendeződik: egyre inkább eszközépítőként és MI-specialistaként dolgozunk majd együtt az új logikai „társainkkal”.
Ember és MI: kéz a kézben a tudás új határáig
A matematika mindig is támaszkodott olyan eszközökre, amelyek kitolták a megismerés határait. Az MI most nem megszünteti ezt a hagyományt, hanem olyan szintre emeli, ahol az emberi kreativitás és a gépi alaposság együtt teremt soha nem látott bizonyosságot. A fogalmak és érvelések nem lesznek egyszerűbbek, de az ellenőrzési és építési lehetőségek ugrásszerűen nőnek.
