Egy nyitott kriptográfiai probléma bizonyításában ért el fontos eredményt Prof. Dr. Nagy Gábor Péter, az SZTE Bolyai Intézet vezetője, matematikus, egyetemi tanár, valamint hallgatója, Vajda Attila. A problémát Claude Carlet francia professzor, a modern matematikai kriptográfia meghatározó alakja vetette fel 2018-ban. Carlet a cikkében megjegyezte, hogy az esetek felére vonatkozóan a megoldása "még nem teljes", a másik felére viszont új módszerek lesznek szükségesek. Egy évvel később a feladatot kitűzték az NSUCrypto nemzetközi kriptográfiai versenyen is, de mostanáig senkinek sem sikerült megoldania.
A Bolyai Intézet professzora és diákja a bizonyítás megtalálásához új kutatási módszert alkalmazott, amely összehangolva használta a mesterséges intelligenciát és az emberi intuíciót. A bizonyítandó sejtés az úgynevezett Kasami-polinomokra vonatkozott, amelyeket különböző k és n relatív prím egész számokból lehet konstruálni; a kiírás szerint meg kellett mutatni, hogy egy bizonyos feltétel teljesül minden k és n relatív prímszám esetén.
Dr. Nagy Gábor Péter kérdésünkre elmondta, hogy a Kasami-polinomok azért érdekesek, mert csaknem teljesen nemlineáris tulajdonsággal bírnak. Ez azt jelenti, hogy maximális ellenállást tanúsítanak a differenciális kriptoanalízissel szemben, vagyis alkalmasak az információ titkosítására.
– A magyarázatot kezdjük onnan, hogy mi a szimmetrikus kulcsú kriptográfiával foglalkozunk, amelyben egyazon kulccsal történik a titkosítás és a feloldás. Ehhez szükség van egy függvényre, amely úgynevezett nagyon nemlineáris tulajdonsággal bír. A lineáris függvények ugyanis matematikailag túl könnyen kezelhetők, ezért minden kriptorendszerben lennie kell legalább egy résznek, amely nagyon nemlineáris – mondta az SZTE Bolyai Intézetének új vezetője.
Prof. Dr. Nagy Gábor Péter elmondta, hogy a nemlinearitás mérésére az 1990-es években Kaisa Nyberg finn matematikusnő javasolt új módszert, amit először idegenkedve fogadott a szakma; azóta azonban kiderült, hogy a függvények, amelyek ezzel a mérőszámmal mérve erős nemlinearitást mutatnak, tényleg ellenállnak a különböző támadási lehetőségeknek.
– Egyszóval, a titkosításhoz minél egyszerűbb nemlineáris függvényeket keresünk, és annál nincs egyszerűbb, mint hogy egy számnak veszem a hatványát. Ezt egy adott fokú polinomnak mondjuk, de még azok között is egyszerű, mert csak egyetlen tagból áll. A Kasami-függvény egy olyan polinomosztály, amelyben x a d-ediken található, d pedig kifejezhető egy k függvény segítségével; a kettő n-ed rendű véges test lesz, vagyis egy bizonyos számolási környezeten belül ez egy nemlineáris leképezés. A konstrukció nagyon egyszerű, jó tulajdonságai vannak, csakhogy ezeket nagyon nehéz matematikailag bebizonyítani. A Kasami-függvénynek ezt az adottságát a publikációk kész tényként kezelik, egyik cikk a másikra hivatkozik. Tudtuk tehát, hogy teljesülnek jó tulajdonságai, a bizonyításuk azonban nem volt fellelhető, ezért írta ki feladatként a verseny – fejtette ki az SZTE matematikusa.
 |
| Prof. Dr. Nagy Gábor Péter matematikus, egyetemi tanár, az SZTE Bolyai Intézet vezetője. Fotó: Bartha Karina |
Dr. Nagy Gábor Péter szerint régi célja az elméleti informatikával és az alkalmazott matematikával foglalkozó szakembereknek, hogy egy matematikai bizonyítás helyességét a számítógép is le tudja ellenőrizni. Az utóbbi években az úgynevezett típuselmélet, a matematika logika egy új ága szolgáltatott ehhez eszközöket, amelyek lehetővé teszik, hogy számítógépes program létre tudjon hozni matematikai állításokat, és a bizonyítás helyességét is ellenőrizni tudja. A bizonyítás ötlete onnan származik, hogy a nagy nyelvi modellek jól ismerik a típuselméleten alapuló tételbizonyító rendszereket. A legelterjedtebb ezek közül a LEAN nevű rendszer, amely mögé napjaink egyik legnagyobb matematikusa, az ausztrál-amerikai Terence Tao is beállt.
– Arra voltam kíváncsi, hogy használhatjuk-e ezeket az eszközöket kutatási asszisztensként – folytatta Dr. Nagy Gábor Péter. – Egy kutatási projektnek számos munkaigényes lépése van: ha van egy ötletünk, amelyhez számításokat szeretnénk kidolgozni, akkor az egészet kézzel kell elvégeznünk. A projektünk első részében összegyűjtöttük a természetes nyelven leírt matematikai bizonyításokat, és a különböző mesterséges intelligenciák segítségével átfordítottuk a LEAN formalizált nyelvére. Így számítógépesen le lehetett ellenőrizni, hogy helyes-e a bizonyítás. Ez egy teljesen új kutatási módszertan. A területen heti szinten jelennek meg újdonságok, legutóbb Terence Tao kaliforniai csoportja számítógépes repozitóriumot indított a LEAN rendszerre formalizált matematikai eredmények összegyűjtésére. Nincs még talán két hete sem, hogy elindult a projekt, és már azon dolgozunk, hogy az eredményeink bekerüljenek abba a repozitóriumba.
A feladat bizonyítása közben az is kiderült, hogy az erősebb mesterségesintelligencia-előfizetés már a matematikában is kutatási előnyt jelent:
– Mi Attilával nem a teljes állítást bizonyítottuk, hanem a k=2 esetet. A megoldásunkat augusztus 19-én közzétettük, 30-án kaptam egy üzenetet Douglas McNeil kanadai hobbimatematikustól, hogy további AI-segédlettel sikerült megoldania a problémát teljes általánossággal. Így az eredménynek három társszerzője van. A formális bizonyításunk már online van, és hamarosan közöljük a bizonyítást hagyományos, matematikai nyelvezeten leírva. Kiderült, hogy szerzőtársunknak drágább, nagyobb teljesítményű AI-előfizetés állt rendelkezésére. A piacon hozzáférhető modellek közül a legerősebbek elérése néhány száz dollárba kerül, ezt akár egy kutatási pályázatból is ki lehet gazdálkodni, de egyelőre nem könnyű ennek a megszervezése az egyetemen. Kollegáimat is bátorítom, hogy mindenkinek legyen pár ezer forintos saját AI-előfizetése, és próbáljuk megszervezni, hogy kutatási projektekből finanszírozott erősebb előfizetéseink is legyenek. Egyelőre az jellemző, hogy a k-2-re úgy értük el a bizonyítást, hogy hazajött Budapestről a nagyfiam, aki egy startupnál dolgozik, és a havi AI-előfizetésükön még volt pár száz dollár. Éppen elő volt már készítve a kutatásunk, és ellenőrizni tudtuk a bizonyítás helyességét – fűzte hozzá az SZTE matematikusa.
A kutatás előzményeiről Dr. Nagy Gábor Péter elmondta, hogy az elmúlt években rendszeresen jöttek hírek, miszerint a nagy nyelvi modellek összetett matematikai problémákkal is megbirkóznak.
– Matematikusként véges geometriával, diszkrét matematikával, véges algebrai struktúrákkal foglalkozom, és ezekkel kapcsolatban rendszeresen elhangzik, hogy mennyi kriptográfiai alkalmazásuk van. De itt véget is ér a sztori, a konkrét kriptográfiai kapcsolat általában nincs tisztázva. 2016-tól volt nálam egy marokkói doktorandusz, ő hívta fel a figyelmem az NSUCrypto kriptográfiai versenyre, amelyet már akkor is egy nemzetközi szervezőbizottság felügyelt. Sokáig csak szemeztünk a versennyel, és végül 2020-ban két másik kollegámmal, Aradi Miklóssal és Nagy Gáborral alkottunk egy 3 fős csapatot, és elindultunk rajta. A verseny sajátossága, hogy megoldásra váró nyitott problémákat is kitűznek, ezeket néha 1-2 évvel később oldja meg valaki, néha sok éven keresztül nyitottak maradnak. A Kasami-polinomok feladatát időnként megpróbáltam elsütni egy-egy hallgatói beszélgetésben, de rendszerint nem jött rá igazi válasz. Mígnem a tavasz folyamán Vajda Attila alapszakos hallgatóm is bekapcsolódott, és nagy kitartással elkezdte kipróbálni a különböző mesterséges intelligencia rendszereket. Az egyiknek föltette a kérdést, majd a választ ellenőriztette a másikkal, és érdekes eredmények kezdtek jönni. Látszott, hogy ezzel érdemes jobban foglalkozni. Mindegyik megoldásról kiderült ugyan 1-2 hét után, hogy hibásak, a nagy nyelvi modell hallucinációit tartalmazzák, de érdemesnek látszott folytatni. A nagy nyelvi modellek már vannak annyira erősek, hogy a nyilvánvaló hibákat észreveszik, a nehezen észrevehető hibák azonban rejtve maradtak, és egy kicsit mindig megváltoztatták a kérdés matematikai jelentését. Ezután újra kellett néhány hét, amíg rájöttünk, hogy még nincs megoldva a probléma. Megint matematikailag kellett utánanézni a kérdésnek, és lépésről lépésre betanítani a nyelvi modellt, hogy az egész problémakörben valamennyire tájékozott legyen, vagyis meglegyen az alapkontextusa. Fél éven keresztül készítettük elő a terepet részfeladatokkal, mire már fel lehetett tenni neki a kérdést a konkrét problémáról.
 |
| Fotó: Bartha Karina |
Dr. Nagy Gábor Péter úgy gondolja, a matematikai kutatásban elfogadható módszer az emberi intuíció kombinálása a mesterséges intelligenciával:
– Van, akiknek látom a szemében a rosszallást, de mindenki számára nyilvánvaló, hogy ezt nem lehet megállítani. Sok kollegáról tudom, hogy kísérletezik vele. Egyesek jobban aggódnak, hogy a kutatási területükön 1-2 éven belül minden lényeges problémát meg lehet oldani az AI-al. Mások úgy érzik, hogy eléggé elvont a területük ahhoz, hogy még néhány évig teremjen nekik babér. Az én prognózisom az, hogy a matematika és az összes tudomány vidáman túl fogja élni az AI-t, viszont az eddigi publikációs rendszert újra kell majd gondolni.
A kutatás a "Kombinatorikus struktúrák csoportokban és geometriákban" című projekten belül hozott eredményt, "SNN 152582" azonosítószámon.
Panek Sándor
A borítóképen: Dr. Nagy Gábor Péter matematikus, egyetemi tanár, a Szegedi Tudományegyetem Bolyai Intézetének új vezetője. Fotó: Bartha Karina
