My thesis for the fulfillment of the Master of Science (MS) Computer Science at the University of Colorado, Boulder. “Knowledge Distillation before Formal Verification of Deep Neural Networks” (Perr-Sauer, 2022). This work was advised by Professor Ashutosh Trivedi and was defended successfully to obtain my masters degree with thesis option.

In this work, we explore a technique called knowledge distillation (Hinton, 2015) to compress a fully connected neural network (also known as a multi-layer perceptron) before verifying safety properties of the compressed network with a formal verification technique called nnenum (Bak, 2021).

Formal verification proceeds by iterating safety regions through the network structure, which scales inefficiently with the number of so-called “split” neurons in the network. This means it is computationally infeasible to use formal verification on large networks. Although much work has been done to speed up verification algorithms, fundamentally they are limited by an exponential time complexity in the size of the target neural network.

Knowledge Distillation is a type of compression algorithm used to generate smaller, so-called “student” networks using a larger “teacher” network to assist in training them. There are theoretical as well as practical reasons why using such a teacher network might be superior to training the smaller student network from scratch.

In my thesis, both knowledge distillation and the nnenum algorithm are defined, and some background is provided. We apply a novel experimental procedure to a reference neural network called Acas-XU (Julian, 2016). Through computational experiments, we find that compressing the network does indeed speed up the formal verification as expected. However, the fidelity of the student network was not high enough to be useful, and not all safety properties required of the Acas-XU network were preserved.