Thesis Details

Formal Analysis of Neural Networks

Bachelor's Thesis Student: Hudák David Academic Year: 2021/2022 Supervisor: Češka Milan, doc. RNDr., Ph.D.
Czech title
Formální metody pro analýzu neuronových sítí
Language
English
Abstract

Today, the area where we can use deep learning is becoming broader. It includes safety-critical domains such as traffic or healthcare, and the need for its verification grows. However, sufficient verification toolkits for neural networks, the leading deep learning approach, are still in development. State-of-the-art algorithms now can not verify commonly used deep networks. In this paper, we focus on one of the state-of-the-art solutions, VeriNet. More generally, we focused on the symbolic approach of local robustness analysis. This approach usually relies on creating, processing, and refining the neural network representation, and we focused on the refinement phase. We primarily dealt with the branch and bound algorithm, which in this toolkit splits node inputs in a network to create smaller sub-problems. For this algorithm, we proposed and implemented new split node selection strategies. Specifically, we designed memory-based, alternating, and semi-hierarchical strategies. We achieved significant improvements in the scalability of the VeriNet toolkit. One of our approaches can solve more complex cases and significantly improve already solved cases' performance. Moreover, we discovered an anomaly in the behavior of the verification algorithm we named branch implosions, which led to extreme speed up for some cases. In addition, we extended the set of performed network benchmarks with models from the Marabou package. 

Keywords

Neural network, ReLU, VeriNet, ESIP, branch and bound, splitting strategies, branch implosions, semi-hierarchical strategy, formal verification

Department
Degree Programme
Files
Status
defended, grade B
Date
13 June 2022
Reviewer
Committee
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Martínek Tomáš, Ing., Ph.D. (DCSY FIT BUT), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT), člen
Citation
HUDÁK, David. Formal Analysis of Neural Networks. Brno, 2022. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2022-06-13. Supervised by Češka Milan. Available from: https://www.fit.vut.cz/study/thesis/24620/
BibTeX
@bachelorsthesis{FITBT24620,
    author = "David Hud\'{a}k",
    type = "Bachelor's thesis",
    title = "Formal Analysis of Neural Networks",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2022,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/24620/"
}
Back to top