Thesis supervisor: Gergely Kovásznai
Location of studies (in Hungarian): University of Debrecen Faculty of Informatics Abbreviation of location of studies: DE IK
Description of the research topic:
Nowadays, neural networks can be considered to be the most important and most widely applied tools in artificial intelligence development, especially in deep learning. There exist numerous application areas such as medical image processing, data mining or the AI in computer games. This is recently one of the “hot spots” of basic and applied research in computer science, that provides numerous unsolved questions.
Systems that employ neural networks became very complex in the past years and, therefore, they require security checks such as global/local safety or robustness. In the past couple of years, although a few important papers have been published in this topic, there are still several unsolved questions. One of the most promising direction is to apply SAT and SMT solvers, that are already widely applied in industry to formally verify complex system (e.g., hardware, software, sensor networks, air traffic control systems, etc.), where exhaustive testing is infeasible and/or does not provide sufficient guarantees. In the topic of the formal verification of neural networks, literature usually focuses on binarized neural networks, since they can achieve the efficiency of traditional neural networks and are much more suitable for applying formal methods based on logic.
The comparative formal analysis of binarized neural networks is an especially interesting and noteworthy direction in research and development, in particular with #SAT solvers. This could help specialists to “measure” how “similar” two neural networks are, i.e., to calculate the ratio of those models (inputs) for which the networks provide the same output. Of course, this problem cannot be solved by exhaustive testing, this is why formal methods are the suitable tools here. The expected results of this research are not only papers, but a software which encodes neural networks, executes an underlying #SAT solver and interprets the result of the formal analysis.
Bibliography
• 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.
Deadline for application: 2019-11-15
2024. IV. 17. ODT ülés Az ODT következő ülésére 2024. június 14-én, pénteken 10.00 órakor kerül sor a Semmelweis Egyetem Szenátusi termében (Bp. Üllői út 26. I. emelet).
Login
