témavezető: Kovásznai Gergely
helyszín (magyar oldal): Debreceni Egyetem Informatikai Kar helyszín rövidítés: DE IK
A kutatási téma leírása:
Napjaink mesterséges intelligencia fejlesztéseinek legfontosabb és legszélesebb körben alkalmazott eszközei a neurális hálózatok, elsősorban a deep learning területén. Számtalan alkalmazási területet lehetne sorolni az orvosi képfeldolgozástól kezdve az adatbányászaton keresztül a számítógépes játékok mesterséges intelligenciájáig. Kijelenthetjük, hogy manapság ez az informatikai alap- és alkalmazott kutatások egyik leginkább forrongó területe, mely rengeteg még megoldatlan kérdés kutatásával kecsegtet.
A neurális hálózatokat alkalmazó rendszerek olyan mértékben váltak komplexekké az utóbbi években, hogy elengedhetetlenek a rendszerekkel kapcsolatos biztonsági vizsgálatok, úgy mint a globális/lokális biztonság vagy a robusztusság kérdése. Az utóbbi 1-2 évben ezen a területen fontos szakcikkek jelentek meg, ám még nagyon az elején tart a szakma a még nyitott kérdések megválaszolásának. Egy nagy potenciállal rendelkező irány a SAT és SMT szolverek alkalmazása, melyeket manapság már széles körben használnak az iparban olyan komplex rendszerek (pl. hardver, szoftver, szenzorhálózatok, repülésirányító rendszerek stb.) formális verifikációjára, melyek esetén a kimerítő tesztelés nem megvalósítható és/vagy nem nyújt megfelelő garanciát. A szakirodalomban neurális hálózatok formális verifikációjának területén általában binarizált neurális hálózatokra fókuszálnak, melyek bizonyítottan képesek biztosítani a hagyományos neurális hálózatok hatékonyságát, viszont sokkal alkalmasabbak a logikai alapokon nyugvó formális módszerek alkalmazására.
Egy különösen érdekes és nagy figyelmet ígérő kutatási és fejlesztési irány a binarizált neurális hálózatok összehasonlító analízise formális módszerek segítségével, elsősorban #SAT szolverek alkalmazásával. Ez arra adna lehetőséget a szakembereknek, hogy „meg tudják mérni” két neurális hálózat „hasonlóságát”, azaz azon modellek (inputok) arányát, melyekre a két hálózat ugyanazt az outputot szolgáltatja. Természetesen ez a kérdés nem vizsgálható kimerítő teszteléssel, a formális módszerek viszont épp megfelelő eszközöket adnak a kezünkbe. A kutatás eredménye nem csupán publikációkban nyilvánul majd meg, hanem egy saját fejlesztésű szoftverben, mely a megfelelő formában kódolja a vizsgált neurális hálózatokat, futtatja az alkalmazott #SAT szolvert, majd a formális analízis eredményét megfelelően interpretálja.
Irodalom
• N. Narodytska, S. Kasiviswanathan, L. Ryzhyk, M. Sagiv, T. Walsh. Verifying Properties of Binarized Deep Neural Networks. 32nd AAAI Conference on Artificial Intelligence (AAAI-18), pp. 6615-6624, 2018.
• I. Hubara, M. Courbariaux, D. Soudry, R. El-Yaniv, Y. Bengio. Quantized Neural Networks: Training Neural Networks with Low Precision Weights and Activations. Journal of Machine Learning Research, vol. 18(187), pp. 1-30, 2018.
• B. McDanel, S. Teerapittayanon, H. T. Kung. Embedded Binarized Neural Networks. 2017 International Conference on Embedded Wireless Systems and Networks, pp. 168-173, 2017.
• L. Pulina, A. Tacchella. Challenging SMT Solvers to Verify Neural Networks. AI Communications, vol. 25(2), pp. 117-135, 2012.
Bejelentkezés
