Comparison of heuristics for branching in neural network verification

Seidel, Jonas; Brix, Christopher Jan-Steffen; Noll, Thomas; Katoen, Joost-Pieter

Comparison of heuristics for branching in neural network verification

Seidel, Jonas^RWTH*

2022

Verantwortlichkeitsangabeby Jonas Seidel

ImpressumAachen 2022

Umfang75 Seiten : Illustrationen

Bachelorarbeit, RWTH Aachen University, 2022

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Noll, Thomas (Thesis advisor)^RWTH* ; Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Brix, Christopher Jan-Steffen (Consultant)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2022-09-12

Online
URL: https://publications.rwth-aachen.de/record/985671/files/985671.pdf

Einrichtungen

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
When verifying neural networks using relaxation based approaches, the exact behavior of a network is overapproximated, often introducing an error which is too large to decide whether a safety property holds or not. To make those approaches complete, verification problems are branched into easier to solve subproblems, by choosing neurons and effectively removing their introduced overapproximation error in each branch. The purpose of this thesis is to explore and compare different heuristics for branching in neural network verification.A selection of hand designed heuristics was implemented in a verification toolkit called Debona, which is a relaxation based approach implementing symbolic interval propagation. Their performance was evaluated on different feed-forward classification models of handwritten digits that were trained on the MNIST database.The results showed that the choice of branching heuristic significantly influences how fast a safety property can be verified. Some of the implemented heuristics managed to improve upon the existing heuristics in the Debona toolkit while others performed significantly worse. Heuristics that considered branching on input neurons were consistently outperformed by hidden neuron splitting heuristics on all our experiments. However, their results improved on networks with smaller input dimensions. It suggests that input splits are a bad choice for verifying neural networks with high input dimensions such as image recognition models but still might be valuable to verifying neural networks with a low-dimensional domain.In conclusion, this work provides an overview of various approaches to branching in neural network verification and highlights the importance of the choice of the branching heuristic to the effectiveness of relaxation based approaches.

Restricted:
PDF