ELTE-projekt az európai kutatási élvonalban
Hatalmas támogatást nyert el a magyar kutató egy európai pályázaton.
Kaposi Ambrus típuselméleti kutatása 2024-ben Magyarországról egyedüliként részesült ERC Consolidator Grant támogatásban a legrangosabb európai tudományos kiválósági pályázaton. Kategóriájában (Élettelen természettudományok és műszaki tudományok) 928 benyújtott pályázat közül került a kiválasztott 131 közé.
Az Európai Kutatási Tanács (European Research Council - ERC) a Horizon Europe keretprogramban a felfedező kutatásoktól a hasznosítás kezdeti fázisáig díjazza a legígéretesebb kutatásokat. A Consolidator Grant pályázaton a már kutatócsoporttal és kiemelkedő eredményekkel rendelkező, tudományos áttörés ígéretét hordozó kutatásokat ismerik el. Kaposi Ambrus és csapata a Magasabb megfigyelés-alapú típuselmélet (Higher Observational Type Theory – HOTT) című kutatásával a számítógépes bizonyítórendszerek használatát forradalmasíthatja.
A számítógépes bizonyítórendszerek a típuselméletre (type theory) épülnek. A típuselmélet mind a matematikusok, mind pedig az informatikusok bizonyítási és helyesség-ellenőrzési problémáira megoldást kínál, hiszen olyan formális nyelvi eszközt ad a kezünkbe, amellyel egyszerre lehet programokat és matematikai bizonyításokat írni. Egy program típusa maga az állítás, a típusnak megfelelő program pedig az állítás bizonyítása.
A típuselmélet magasabb-dimenziós modelljeiben a típusok elemeit absztrakt terek pontjaival, az egyenlőség típust pedig a pontok közötti utakkal adják meg. Ilyen modellekre építve fejlesztették ki a homotópia-típuselméletet (homotopy type theory), amelyben teljesül az izomorf típusok egyenlőségének elve. Ezzel az elvvel a számítógépes bizonyítás közel kerül a mindennapos matematikusi gyakorlathoz, ahol az izomorf struktúrákat azonosnak tekintik.
A HOTT projekt célja a homotópia-típuselmélet egy új változatának kidolgozása, amelyben a magasabb-dimenziós geometria nem kézzel van beépítve, hanem emergens. Az alapötlet, hogy az egyenlőség típus nem geometriai módon, hanem számítással van megadva. A megoldás elmagyarázhatóvá teszi a homotópia-típuselméletet, és rövidíti a bizonyításokat, hiszen a bizonyítások egyes részei automatikus számításokká válnak. Az új típuselmélet hosszú távon hozzá fog járulni a matematikai bizonyítások számítógépes ellenőrzésének és a szoftverek helyességbizonyításának fejlődéséhez azáltal, hogy lehetővé teszi az absztrakt, újra felhasználható bizonyítások készítését.
Kaposi Ambrus az ELTE Programozási Nyelvek és Fordítóprogramok Tanszék egyetemi docense, PhD-fokozatait klinikai orvostudományokból és informatikából szerezte. Kutatási területei a típuselmélet, a funkcionális programozás, a matematikai logika, az orvosi statisztika. 2019-ben az MTA Bolyai-ösztöndíjában, 2020-ban az ELTE Ígéretes Kutatója kitüntetésben részesült. Típuselméleti kutatásait korai fázisukban az ELTE Informatikai Kar Tématerületi Kiválósági Pályázatai támogatták, az Ipar és Digitalizáció, majd a Nemzetvédelem, Nemzetbiztonság alprogramok keretében.
Összegezve
- Kaposi Ambrus 2024-ben egyedüliként kapott ERC Consolidator Grant támogatást Magyarországról.
- Kaposi Ambrus kutatása a számítógépes bizonyítórendszerek forradalmát ígéri a típuselmélet terén.
- Típuselmélet megoldást kínál matematikusok és informatikusok bizonyítási problémáira.
- Kaposi Ambrus az ELTE Programozási Nyelvek és Fordítóprogramok Tanszék egyetemi docense.
- Kaposi Ambrus kutatási területei közé tartozik a típuselmélet, a funkcionális programozás és az orvosi statisztika.
Kövesse az Egészségkalauz cikkeit a Google Hírek-ben, a Facebook-on, az Instagramon vagy a Twitter-en, Tiktok-on is!
