# Improving Knowledge Distillation for BERT Models: Loss Functions, Mapping
Methods, and Weight Tuning

Adeem Jassani
MSc in Applied Computing
<EMAIL_ADDRESS>
Apoorv Dankar
MSc in Applied Computing
<EMAIL_ADDRESS>
Kartikaeya Kumar
MSc in Applied Computing
<EMAIL_ADDRESS>

###### Abstract

The use of large transformer-based models such as BERT, GPT, and T5 has led to
significant advancements in natural language processing. However, these models
are computationally expensive, necessitating model compression techniques that
reduce their size and complexity while maintaining accuracy. This project
investigates and applies knowledge distillation for BERT model compression,
specifically focusing on the TinyBERT student model. We explore various
techniques to improve knowledge distillation, including experimentation with
loss functions, transformer layer mapping methods, and tuning the weights of
attention and representation loss and evaluate our proposed techniques on a
selection of downstream tasks from the GLUE benchmark. The goal of this work
is to improve the efficiency and effectiveness of knowledge distillation,
enabling the development of more efficient and accurate models for a range of
natural language processing tasks.

##  1 Introduction

Large transformer-based models have significantly advanced the field of NLP.
However, these models are computationally expensive, posing challenges in
deployment on resource-constrained devices. Model compression techniques, like
knowledge distillation, aim to reduce model size and complexity while
maintaining performance.

This project focuses on improving knowledge distillation for BERT (Devlin et
al. (2018)) model compression, specifically using the TinyBERT (Jiao et al.
(2019)) student model. We explore various techniques to enhance the efficiency
and effectiveness of knowledge distillation, including experimentation with
alternative loss functions, transformer layer mapping methods, and tuning the
weights of attention and representation loss. We evaluate the performance of
our proposed techniques on a selection of downstream tasks from the GLUE
benchmark (Wang et al. (2018)). Our objective is to contribute to the
development of more efficient and accurate models for a range of natural
language processing tasks.

Our experiments (GitHub link in the reproducibility section of Appendix A.2)
show that certain alternative loss functions, such as KL divergence (Kullback
and Leibler (1951)), can lead to improved performance in some scenarios,
particularly when training with limited data for challenging tasks like CoLA
Warstadt et al. (2018). Additionally, we demonstrate the importance of the
mapping function between student and teacher layers. Our novel LearnableMap
offers a slight improvement over the baseline. Our work highlights the
potential benefits of these techniques and provides insights that can inform
future research on model compression and knowledge distillation.

##  2 Related Works

Transformer-based models like BERT are commonly compressed using a combination
of knowledge distillation, pruning, and quantization techniques. BERT (Devlin
et al. (2018)), is one of the most widely used pre-trained language models.
Knowledge distillation, introduced by (Hinton et al. (2015)), is a popular
technique for model compression that involves training a smaller, simpler
model to mimic the behavior of a larger, more complex model. DistilBERT (Sanh
et al. (2019)), a compressed version of BERT, is the first BERT model
compressed using knowledge distillation.

To further improve knowledge distillation, researchers have proposed several
extensions to the technique. For example, Patient Knowledge Distillation (Sun
et al. (2019)), uses loss calculated at multiple intermediate layers of the
teacher model for incremental knowledge extraction, resulting in better
accuracy. Another notable example is TinyBERT (Jiao et al. (2019)), which
refines previous methods by, first, incorporating an attention loss between
intermediate layers, and second, utilizing a two-stage distillation process to
boost the efficiency and effectiveness of the technique.

##  3 Methodology

In this section, we outline our methodology, detailing the TinyBERT
distillation process and the three exploration techniques we employed:
alternative loss functions, mapping functions, and tuning the weights of
representation and attention loss.

The total loss function for TinyBERT distillation consists of three
components: 1) Embedding loss ($\mathcal{L}_{\mathrm{embd}}$) for the input
layer ($m=0$), the 2) Transformer layer loss which is a sum of hidden
representation loss ($\mathcal{L}_{\mathrm{hidn}}$) and attention loss
($\mathcal{L}_{\mathrm{attn}}$) for the transformer layers ($0<m\leq M$), and
3) Prediction loss ($\mathcal{L}_{\mathrm{pred}}$) for the output layer
($m=M+1$). Here, $m$ represents the index of the student layer, and $M$
denotes the total number of transformer layers in the student model.

For the embedding and prediction layers, the loss is computed between the
corresponding student and teacher layers. Since there are 12 transformer
layers in BERT and 4 transformer layers in TinyBERT, a mapping function
$n=g(m)$ (explained in more detail in 3.2) is used to determine the mapped
teacher layer for the $m^{th}$ student layer. Thus, for the intermediate
layers, the loss is computed between the student layer and the mapped teacher
layer. The mapping function and its detailed explanation can be found in
Section 3.2.

The TinyBERT distillation process has two stages: 1) General Distillation,
which distils the general BERT model into the general TinyBERT model, and 2)
Task Distillation, which distils the task-specific BERT model into the task-
specific TinyBERT model, initialized from the general TinyBERT model. Task
Distillation has two substages: a) Transformer Layer Distillation, using only
transformer layer loss, and b) Prediction Layer Distillation, using only
prediction layer loss.

###  3.1 Exploring KL Divergence as Attention Loss

Attention loss, denoted as $\mathcal{L}_{\mathrm{attn}}$, measures the
difference between the attention distributions of the teacher and student
models. The original TinyBERT approach uses mean squared error (MSE) over
unnormalized attention matrices. In our experiments, we use Kullback-Leibler
(KL) divergence (Kullback and Leibler (1951)) over normalized attention
matrices as shown in the following equation.

$\frac{1}{h}\sum_{i=1}^{h}MSE\left(A_{i}^{S},A_{i}^{T}\right)\rightarrow\frac{1}{h}\sum_{i=1}^{h}KL\left(\sigma\left(A_{i}^{S}\right),\sigma\left(A_{i}^{T}\right)\right)$
(1)

where $h$ is the number of attention heads, ${A}_{i}$ refers to the attention
matrix corresponding to the $i$-th head of teacher or student and $\sigma$
represents softmax. We explore KL Divergence since it measures the difference
between two probability distributions making it a natural fit for comparing
attention distributions.

###  3.2 Exploring different Mapping Functions

As described previously, the mapping functions determine which teacher layers
a student layer learns from. In the base paper, a uniform mapping function
$g(m)=3m$ is used. For example, in the uniform mapping, student layer 1 is
mapped to teacher layer 3, and student layer 2 is mapped to teacher layer 6,
and so on.

Inspired by uniform mapping, we divide the teacher layers into blocks equal to
the number of student layers. For example, teacher layers (1, 2, 3) form block
1, (4, 5, 6) form block 2, and so on. We explore various novel mapping
functions that combine different teacher layers to create an aggregated
representation for the student to learn from. In our framework, we represent
the mapping function as the normalized vector ${v}(m)\in\mathbb{R}^{3}$, as
there are three layers in one block. 111We use the value 3 for ease of
understanding, but the framework is extensible to any distillation where the
number of layers of the teacher is divisible by the number of layers of the
student. The aggregated teacher representation is computed as a linear
combination of the representations from the corresponding block with weights
${v}(m)$. The base uniform mapping fits into our framework with
${v}(m)=(0,0,1)$. We experiment with the following mapping functions:

  1. 1.

Random map: ${v}_{k}(m)=\mathrm{OneHot}(\mathrm{RandInt}(3))\forall m$. One
layer from the corresponding block is randomly selected to be the teacher
representation for the student layer during each iteration. Here, $k$
represents the iteration number during the training process.

  2. 2.

Mean map: ${v}(m)=\left(\frac{1}{3},\frac{1}{3},\frac{1}{3}\right)\forall m$.
This (fixed) mapping equally combines all three layers in the corresponding
block to form the aggregate teacher representation for the student layer to
learn from.

  3. 3.

Learnable map: ${v}_{k}(m)=\mathrm{softmax}({\theta}_{k}[m])\forall m$. This
mapping learns the optimal combination of layers in the corresponding block to
form the aggregate teacher representation. Here,
$\theta\in\mathbb{R}^{(M,N/M)}$ where $M$ and $N$ are numbers of layers in
student and teacher respectively.

###  3.3 Tuning the Weights of Representation and Attention Loss

In the base paper, the authors employ an equal weighting of hidden
representation loss and attention loss for transformer layer distillation. In
our experiments, we explore adjusting the relative weights of these two losses
to examine their impact. We modify the loss function by introducing a tunable
parameter $\alpha$ ranging from 0 to 1 (with $\alpha=0.5$ giving the baseline)
, as shown in the modified combined loss equation:

$\mathcal{L}_{\mathrm{hidn}}+\mathcal{L}_{\mathrm{attn}}\rightarrow
2\alpha\cdot\mathcal{L}_{\mathrm{hidn}}+2(1-\alpha)\cdot\mathcal{L}_{\mathrm{attn}}$
(2)

##  4 Experiments

In our research project, we focused on the task-specific distillation stage
due to the high computational cost associated with general distillation. Thus,
we conducted multiple experiments using two datasets from the GLUE benchmark
(Wang et al. (2018)) - CoLA and STS-B (Cer et al. (2017)) - as they exhibited
a significant performance gap between the Teacher and base Student models. The
standard metrics for the respective tasks were employed to evaluate the
models. The Teacher models used in our experiments were fine-tuned BERT
models, which were obtained from the TextAttack Model Hub (Morris et al.
(2020)) on Hugging Face. We utilized the General TinyBERT model provided by
the TinyBERT authors on Hugging Face as our Student model.

Since all our experiments are modifications of the transformer layer loss, we
have implemented our experiments only in the transformer distillation sub
stage of task distillation stage. We adhered to hyperparameters recommended in
the TinyBERT paper (details in A.2). To keep track of all experiments, we used
wandb (Biewald (2020)) as our experiment management tool. The experiments were
conducted using the NVIDIA GeForce RTX 2060 Rev, which has 6 GB of GDDR6,
available from the Department of computer science GPU cluster.

###  4.1 Loss Function Experiments

We conducted experiments to evaluate the performance of the KL divergence loss
and compared it with the baseline loss function using full and half training
data.

Our experimental results demonstrated that the KL divergence loss outperformed
the baseline loss function in the CoLA task. Specifically, we observed a 5.7%
improvement over the baseline when using the full training data and a 12.0%
improvement over the baseline when using half of the training data. However,
we did not observe any significant improvement over the baseline for the STS-B
task when using the KL divergence loss. The detailed results can be found in
the left panels of Figures 1 and 2.

These findings highlight the potential benefits of using the KL divergence
loss function in specific scenarios, such as when training with limited data
and for challenging tasks like CoLA.

###  4.2 Mapping Functions

For the mapping function we experimented with the RandomMap, MeanMap and
LearnableMap functions as explained in Section 3.2. Additionally in the
LearnableMap method, we tried two different initializations of the parameters
- ${v}_{0}(m)=\left(\frac{1}{3},\frac{1}{3},\frac{1}{3}\right)$ which is
equivalent to MeanMap and ${v}_{0}(m)=(0.11,0.11,0.78)$
222${v}_{0}(m)=(0.11,0.11,0.78)$ is obtained by applying softmax(-1, -1, 1).
To obtain the weight vector $(0,0,1)$ we will need to set the $\theta_{0}$ set
to (0, 0, +inf). However, setting a component of $\theta_{0}$ to +inf makes
the optimization difficult which is close to the Base map. We also tuned the
independent learning rate of these params among [1e-3, 1e-4, 5e-5, 1e-6]. We
found that the baseline was performing significantly better than RandomMap in
CoLA which shows the importance of the mapping function. LearnableMap performs
comparably to the baseline for CoLA and does not show any major improvement.
However, for the STS-B task all mappings, including random performed almost
equally. The detailed results are in the center panels of Figures 1 and 2.

While the learnable mapping doesn’t yield significant improvements, an
intriguing observation is that the weight vectors ${v}_{k}(m)$ converge to the
same values regardless of initialization (A.1). This may indicate convergence
to a global minimum and the existence of a mapping that minimizes transformer
loss, presenting a potentially interesting area for further exploration.

###  4.3 Weighting Attention and Representation Loss

In our experiments, we investigated the impact of different values of $\alpha$
on task-specific distillation performance. We observed that for the CoLA task,
setting $\alpha=1$ resulted in significantly worse performance compared to
other values, while other values performed comparably. This finding suggests
that attention loss plays a crucial role in the CoLA task. On the other hand,
for the STS-B task, we found that all tested $\alpha$ values returned similar
results (A.3). The detailed results can be found in the right panels of
Figures 1 and 2.

(a) Loss Function

(b) Mapping Function

(c) Weights of Rep Loss

Figure 1: Various experiments for CoLA

(a) Loss Function

(b) Mapping Function

(c) Weights of Rep Loss

Figure 2: Various experiments for STS-B

##  5 Conclusion

In this study, we investigated various factors influencing the performance of
the TinyBERT model during task-specific distillation. Our findings indicate
that the KL divergence loss function can offer performance improvements for
challenging tasks like CoLA, especially when training with limited data. For
mapping functions, while the learnable mapping didn’t yield significant
improvements, we observed that weight vectors converged to the same values
regardless of initialization, hinting at a potentially interesting area for
future exploration. Our experiments on weighting attention and representation
loss revealed that attention loss plays a crucial role in the CoLA task, while
having less impact on the STS-B task.

In the case of the STS-B task, the performance did not change significantly in
any experiment, indicating that the model may not be learning much from
transformer loss and that most learning is happening through prediction loss
distillation. We later confirmed this by skipping the transformer loss
distillation and achieving similar results as when it was included (A.3).

It is important to note that since we experimented only with the task-specific
distillation stage, the performance improvements observed may be further
enhanced if we apply the same modifications in the general distillation stage
as well. Overall, our research provides valuable insights for future work on
improving transformer-based model distillation methods.

## References

  * Biewald [2020] Lukas Biewald.  Experiment tracking with weights and biases, 2020.  _Software available from wandb. com_ , 2(5), 2020.
  * Cer et al. [2017] Daniel Cer, Mona Diab, Eneko Agirre, Inigo Lopez-Gazpio, and Lucia Specia.  Semeval-2017 task 1: Semantic textual similarity-multilingual and cross-lingual focused evaluation.  _arXiv preprint arXiv:1708.00055_ , 2017.
  * Devlin et al. [2018] Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova.  Bert: Pre-training of deep bidirectional transformers for language understanding, 2018.  URL http://arxiv.org/abs/1810.04805.  cite arxiv:1810.04805Comment: 13 pages.
  * Hinton et al. [2015] Geoffrey Hinton, Oriol Vinyals, and Jeff Dean.  Distilling the knowledge in a neural network, 2015.  URL http://arxiv.org/abs/1503.02531.  cite arxiv:1503.02531Comment: NIPS 2014 Deep Learning Workshop.
  * Jiao et al. [2019] Xiaoqi Jiao, Yichun Yin, Lifeng Shang, Xin Jiang, Xiao Chen, Linlin Li, Fang Wang, and Qun Liu.  Tinybert: Distilling bert for natural language understanding.  _arXiv preprint arXiv:1909.10351_ , 2019.
  * Kullback and Leibler [1951] Solomon Kullback and Richard A Leibler.  On information and sufficiency.  _The annals of mathematical statistics_ , 22(1):79–86, 1951.
  * Morris et al. [2020] John X. Morris, Eli Lifland, Jin Yong Yoo, Jake Grigsby, Di Jin, and Yanjun Qi.  Textattack: A framework for adversarial attacks, data augmentation, and adversarial training in nlp, 2020.
  * Sanh et al. [2019] Victor Sanh, Lysandre Debut, Julien Chaumond, and Thomas Wolf.  Distilbert, a distilled version of bert: smaller, faster, cheaper and lighter.  _ArXiv_ , abs/1910.01108, 2019.
  * Sun et al. [2019] S. Sun, Yu Cheng, Zhe Gan, and Jingjing Liu.  Patient knowledge distillation for bert model compression.  In _Conference on Empirical Methods in Natural Language Processing_ , 2019.
  * Wang et al. [2018] Alex Wang, Amanpreet Singh, Julian Michael, Felix Hill, Omer Levy, and Samuel Bowman.  GLUE: A multi-task benchmark and analysis platform for natural language understanding.  In _Proceedings of the 2018 EMNLP Workshop BlackboxNLP: Analyzing and Interpreting Neural Networks for NLP_ , pages 353–355, Brussels, Belgium, November 2018. Association for Computational Linguistics.  doi: 10.18653/v1/W18-5446.  URL https://aclanthology.org/W18-5446.
  * Warstadt et al. [2018] Alex Warstadt, Amanpreet Singh, and Samuel R Bowman.  Neural network acceptability judgments.  _arXiv preprint arXiv:1805.12471_ , 2018.

## Team Contribution

Authors are listed in alphabetical order. All members contributed equally
throughout the duration of the project. All decisions related to the different
parts of the project (like problem formulation, literature review,
experimental design, and inferences) were taken collectively after discussion.
Some specific contributions are as follows: Adeem took the initiative to
implement the loss functions and run experiments. Apoorv did the same with
various Mapping functions. Kartikaeya was responsible for implementing and
experimenting with weight tuning.

##  Appendix A Appendix

###  A.1 Converging weights from LearnableMap

One of the very interesting things that we observed was that while using
LearnableMap, with the correct learning rate and number of epochs we converge
on the same final weights of the learnable parameter $\theta$. This finding
indicates that there exists an optimal ${v}(m)$ that minimizes the transformer
loss. However, we gathered this insight late in the project and could not
experiment with it enough to get the best results from this. The following
plot shows the convergence and optimal value of weights. Here $v(m)[j]$
denotes the value of the learned weight for $j^{th}$ layer in the respective
block for the $m^{th}$ student layer.

Figure 3: Converging weights from LearnableMap

###  A.2 Details for reproducibility

In the following tables, we have reported what hyperparameter combinations
gave us the best performance metrics for the experiments. The learning rates
and batch size are given for the prediction distillation substage.

For the KL loss, we experimented with different weights relative to the
representation loss. We observed that a weight of 1 resulted in good
performance, and increasing the weight beyond that led to only marginal
improvements.

GitHub Links:

  * •

Loss Function Experiment

  * •

Mapping Function Experiment

  * •

Weight Tuning Experiment

Other hyperparameters values:

  * •

Random Seed is set at 42.

  * •

Learning rate for the transformer layer stage is 5e-05

  * •

Stage 1 epochs for CoLA is 30

  * •

Stage 1 epochs for STS-B is 20

  * •

Stage 2 epochs for both is 3

  * •

Stage 1 batch size is 32

  * •

For Mapping Function experiments the run_name args should be one of the
following (or contain these strings in the name) : [ RandomMap, MeanMap,
LearnableMap ]

  * •

To specify an initialization of the Learnable map, these run_name should be
used : [ LearnableMapUniformStart, LearnableMap001Start ]

Loss Function | MCC | Learning Rate | Batch Size
---|---|---|---
KL | 0.362875 | 1e-05 | 16
MSE | 0.343187 | 1e-05 | 16
KL (50%) | 0.311703 | 2e-05 | 32
MSE (50%) | 0.278384 | 2e-05 | 16
Table 1: Best hyperparameters for Loss function experiments on CoLA Loss Function | Corr | Learning Rate | Batch Size
---|---|---|---
KL | 0.873543 | 3e-05 | 16
MSE | 0.868203 | e-05 | 32
KL (50%) | 0.861659 | 3e-05 | 16
MSE (50%) | 0.859205 | 3e-05 | 16
Table 2: Best hyperparameters for Loss function experiments on STS-B Mapping Function | MCC | Learning Rate (LearnableMap lr) | Batch Size
---|---|---|---
Learnable | 0.344937 | 1e-05 (5e-05) | 32
Base | 0.344144 | 2e-05 | 16
Mean | 0.318876 | 1e-05 | 32
Random | 0.266996 | 1e-05 | 32
Table 3: Best hyperparameters for Mapping Function experiments on CoLA Mapping Function | Corr | Learning Rate (LearnableMap lr) | Batch Size
---|---|---|---
Base | 0.871267 | 3e-05 | 16
Learnable | 0.870572 | 3e-05 (5e-05) | 32
Random | 0.867048 | 3e-05 | 16
Mean | 0.863824 | 3e-05 | 16
Table 4: Best hyperparameters for Mapping Function experiments on STS-B Weight of Rep Loss | MCC | Learning Rate | Batch Size
---|---|---|---
$\alpha=0.75$ | 0.353044 | 2e-05 | 32
$\alpha=0.5$ (Base) | 0.348409 | 2e-05 | 32
$\alpha=0.25$ | 0.347475 | 1e-05 | 32
$\alpha=0$ | 0.343706 | 3e-05 | 32
$\alpha=1$ | 0.250387 | 3e-05 | 32
Table 5: Best hyperparameters for $\alpha$ tuning experiments on CoLA Weight of Rep Loss | Corr | Learning Rate | Batch Size
---|---|---|---
$\alpha=0.25$ | 0.872409 | 3e-05 | 32
$\alpha=0$ | 0.871626 | 3e-05 | 16
$\alpha=1$ | 0.870140 | 2e-05 | 16
$\alpha=0.75$ | 0.869641 | 3e-05 | 32
$\alpha=0.5$ (Base) | 0.869064 | 2e-05 | 32
Table 6: Best hyperparameters for $\alpha$ tuning experiments on STS-B

###  A.3 Confirmation of the Irrelevance of Transformer Layer Loss
Distillation for STS-B Task

In our previous experiments, we observed no significant change in the results
of the STS-B task, leading us to hypothesize that transformer layer
distillation might not be crucial for this task. To test this hypothesis, we
conducted an experiment in which we skipped the transformer layer loss
distillation step.

Instead of fine-tuning the TinyBERT model using the transformer layer loss, we
directly trained the model on the prediction loss distillation task, using the
general TinyBERT model as the initialization. Interestingly, we found that
skipping the transformer layer loss distillation stage yielded almost the same
result (corr = 0.8717) as the baseline (corr = 0.8682). In fact, the
performance was slightly better when skipping the transformer layer loss
distillation.

This observation suggests that the transformer layer loss distillation might
not be essential for the STS-B task, and a more efficient alternative could
involve directly training on the prediction loss distillation task.
Additionally, this experiment highlights the possibility that the relevance of
transformer layer loss distillation may depend on the specific task, and it
might not be equally important for all tasks.


# Benchmarking Local Robustness of High-Accuracy Binary Neural Networks for
Enhanced Traffic Sign Recognition

Andreea Postovan Mădălina Eraşcu Faculty of Mathematics and Informatics, West
University of Timisoara
4 blvd. V. Parvan, 300223, Romania {andreea.postovan99,
<EMAIL_ADDRESS>
###### Abstract

Traffic signs play a critical role in road safety and traffic management for
autonomous driving systems. Accurate traffic sign classification is essential
but challenging due to real-world complexities like adversarial examples and
occlusions. To address these issues, binary neural networks offer promise in
constructing classifiers suitable for resource-constrained devices.

In our previous work, we proposed high-accuracy BNN models for traffic sign
recognition, focusing on compact size for limited computation and energy
resources. To evaluate their local robustness, this paper introduces a set of
benchmark problems featuring layers that challenge state-of-the-art
verification tools. These layers include binarized convolutions, max pooling,
batch normalization, fully connected. The difficulty of the verification
problem is given by the high number of network parameters (905k - 1.7 M), of
the input dimension (2.7k-12k), and of the number of regions (43) as well by
the fact that the neural networks are not sparse.

The proposed BNN models and local robustness properties can be checked at
https://github.com/ChristopherBrix/vnncomp2023_benchmarks/tree/main/benchmarks/traffic_signs_recognition.

The results of the 4th International Verification of Neural Networks
Competition (VNN-COMP’23) revealed the fact that 4, out of 7, solvers can
handle many of our benchmarks randomly selected (minimum is 6, maximum is 36,
out of 45). Surprisingly, tools output also wrong results or missing
counterexample (ranging from 1 to 4). Currently, our focus lies in exploring
the possibility of achieving a greater count of solved instances by extending
the allotted time (previously set at 8 minutes). Furthermore, we are intrigued
by the reasons behind the erroneous outcomes provided by the tools for certain
benchmarks.

##  1 Introduction

Traffic signs play a crucial role in ensuring road safety and managing traffic
flow, both in urban and highway driving. For autonomous driving systems, the
accurate recognition and classification of traffic signs, known as _traffic
sign classification (recognition)_ , are essential components. This process
involves two main tasks: firstly, isolating the traffic sign within a bounding
box, and secondly, classifying the sign into a specific traffic category. The
focus of this work lies on the latter task.

Creating a robust traffic sign classifier is challenging due to the complexity
of real-world traffic scenes. Common issues faced by classifiers include a
lack of _robustness_ against _adversarial examples_ [20] and occlusions [22].
_Adversarial examples_ are inputs that cause classifiers to produce erroneous
outputs, and _occlusions_ occur naturally due to various factors like weather
conditions, lighting, and aging, which make traffic scenes unique and diverse.

To address the lack of robustness, one approach is to formally verify that the
trained classifier can handle both adversarial and occluded examples. Binary
neural networks (BNNs) have shown promise in constructing traffic sign
classifiers, even in devices with limited computational resources and energy
constraints, often encountered in autonomous driving systems. BNNs are neural
networks (NNs) with binarized weights and/or activations constrained to $\pm
1$, reducing model size and simplifying image recognition tasks.

The long-term goal of this work is to provide formal guarantees of specific
properties, like robustness, that hold for a trained classifier. This
objective leads to the formulation of the _verification problem_ : given a
trained model and a property to be verified, does the model satisfy that
property? The verification problem is translated into a constrained
satisfaction problem, and existing verification tools can be employed to solve
it. However, due to its NP-complete nature [15], this problem is
experimentally challenging for state-of-the-art tools.

In our previous work [17], we proposed high-accuracy BNN models explicitly for
traffic sign recognition, with a thorough exploration of accuracy, model size,
and parameter variations for the produced architectures. The focus was on BNNs
with high accuracy and compact model size, making them suitable for devices
with limited computation and energy resources, while also reducing the number
of parameters to facilitate the verification task. The German Traffic Sign
Recognition Benchmark (GTSRB) [6] was used for training, and testing involved
similar images from GTSRB, as well as Belgian [2] and Chinese [5] datasets.
This paper builds upon the models with the best accuracy from the previous
study [17] and presents a set of benchmark problems to verify local robustness
properties of these models.

The novelty of the proposed benchmarks lies in the fact that traffic signs
recognition is done using binarized neural networks. To the best of our
knowledge this was not done before [9, 19]. Compared to existing benchmarks.
The types of layers used determine a complex verification problem and include
_binarized convolution layers_ to capture advanced features from the image
dataset, _max pooling layers_ for model size reduction while retaining
relevant features, _batch normalization layers_ for scaling, and _fully
connected (dense) layers_. The difficulty of the verification problem is given
by the high number of network parameters (905k - 1.7 M), of the input
dimension (2.7k-12k), and of the number of regions (42) as well by the fact
that the neural networks are not sparse. Discussions with organizers and
competitors in the Verification of Neural Network Competition (VNN-
COMP)111https://github.com/stanleybak/vnncomp2023/issues/2 revealed that no
tool competing in 2022 could handle the proposed benchmark. Additionally, in
VNN-COMP 2023 [4], the benchmark was considered fairly complex by the main
developer of the winning solver
$\alpha,\beta$-CROWN222https://github.com/Verified-Intelligence/alpha-beta-
CROWN.

We publicly released our bechmark in May 2023. In the VNN-COMP 2023, which
took place in July 2023, our benchmark was used in scoring, being nominated by
at least 2 competing tools. 4, out of 7, tools were able to find an answer for
the randomly generated instances. Most instances were solved by
$\alpha,\beta$-CROWN (39 out of 45) but it received penalties for 3 results
due to either incorrect answer or missing counterexample. Most correct answers
were given by Marabou333https://github.com/NeuralNetworkVerification/Marabou
(18) with only 1 incorrect answer.

Currently, we are investigating the reasons why the tools were not able to
solve all instances and why incorrect answers were given. Additionally, more
tests will be performed on randomly generated answers and we will examine the
particularities of the input images and of the trained networks which can not
be handled by solvers due to timeout or incorrect answer.

The rest of the paper is organized as follows. In Section 2 we present related
work focusing on comparing the proposed benchmark with others competing in
VNN-COMP. Section 3 briefly describes deep neural networks, binarized neural
networks and formulates the robustness property. In Section 4 we describe the
anatomy of the trained neural networks whose local robustness is checked. In
Section 5.1 we introduce the verification problem and its canonical
representation (VNN-LIB and ONNX formats). Section 6 presents the methodology
for benchmarks generation and the results of the VNN-COMP 2023.

##  2 Related Work

There exist many approaches for the verification of neural networks, see [21]
for a survey, however few are tackling the verification of binarized neural
networks.

Verifying properties using boolean encoding [16] is an alternative approach to
validate characteristics of a specific category of neural networks, known as
binarized neural networks. These networks possess binary weights and
activations. The proposed technique involves reducing the verification problem
from a mixed integer linear programming problem to a Boolean satisfiability.
By encoding the problem in Boolean logic, they exploit the capabilities of
modern SAT solvers, combined with a counterexample-guided search method, to
verify various properties of these networks. A primary focus of their research
is assessing the networks’ resilience against adversarial perturbations. The
experimental outcomes demonstrate the scalability of this approach when
applied to medium-sized deep neural networks employed in image classification
tasks. However their neural networks do not have convolution layers and can
handle only a simple dataset like MNIST where images are black and white and
there are just $10$ classes to classify. Also, no tool implementing the
approach was realeased to be tested.

Paper [7] focuses on verification of binarized neural network, extended the
Marabou [15] tool to support _Sign Constrains_ and verified a network that
uses both binarized and non-binarized layers. For testing they used Fashion-
MNIST dataset which was trained using XNOR-Net architecture and obtained the
accuracy of only 70.97%. This extension could not be used in our case due to
the fact that we have binarized convolution layers which the tool can not
handle.

In the verification of neural networks competition (VNN-COMP), in 2022, there
are various benchmarks subject to verification [3], however, there is none
involving traffic signs. To the best of our knowledge there is only one paper
which deals with traffic signs datasets [12] that is GTSRB. However, they
considered only subsets of the dataset and their trained models consist of
only fully connected (FC) layers with ReLU activation functions, not
convolutions, ranging from 70 to 1300 neurons. Furthermore they do not mention
the accuracy of their trained models to be able to compare it with ours.
Moreover, the benchmarks from VNN-COMP 2022 [müller2023international] used for
image classification tasks have are in Table 1. As one could observe, no
benchmarks use binarized convolutions and batch normalization layers.
Discussions with competition organizers revealed the fact that no tool from
2022 competition could handle our benchmark444See
https://github.com/stanleybak/vnncomp2023/issues/2 intervention from user
stanleybak on May 17, 2023.

Table 1: Benchmarks proposed in the VNN-COMP 2022 for image classification tasks Category | Benchmark | Network Types | #Neurons | Input Dimension
---|---|---|---|---
5*CNN & ResNet | Cifar Bias Field | Conv. + ReLU | 45k | 16
| Large ResNets | ResNet (Conv. + ReLU) | 55k - 286k | 3.1k - 12k
| Oval21 | Conv. + ReLU | 3.1k - 6.2k | 3.1k
| SRI ResNet A/B | ResNet (Conv. + ReLU) | 11k | 3.1k
| VGGNet16 | Conv. + ReLU + MaxPool | 13.6M | 1 - 95k
Fully-Connected | MNIST FC | FC. + ReLU | 512 - 1.5k | 784

The report of this year neural networks verification competition (VNN-COMP
2023) is in the draft version, but we present here the differences between our
benchmark and the others. Table 2 taken from the draft report presents all the
scored benchmarks, i.e. benchmarks which were nominated by at least 2
competing tools and are used in their ranking. The column Network Type
presents the types of layers of the trained neural network, the column # of
Params represent the number of parameters of the trained neural network, the
column Input Dimension represents the dimension of the input (for example, for
an image with dimension 30x30 pixels and RGB channel the dimension is 30x30x3
which means that the verification problem contains 30x30x3 variables), the
Sparsity column represents the degree of sparsity of the trained neural
network and, finally, the column # of Regions represents the number of regions
determined by the verification problem (for example, for our German Traffic
Sign Recognition Benchmark there are 43 traffic signs classes). Our proposed
benchmark, Traffic Signs Recognition, is more complex as the others as it
involves cumulatively a high number of parameters, input dimension, number of
regious and no sparsity.

Table 2: Benchmarks proposed in the VNN-COMP 2023 Name | Network Type | # of Params |  | Input
---
Dimension
Sparsity | # of Regions
nn4sys | Conv, FC, Residual + ReLU, Sigmoid | 33k - 37M | 1-308 | 0-66% | 1 - 11k
VGGNet16 | Conv + ReLU + MaxPool | 138M | 150k | 0-99% | 1
Collins Rul CNN | Conv + ReLU, Dropout | 60k - 262k | 400-800 | 50-99% | 2
TLL Verify Bench | FC + ReLU | 17k - 67M | 2 | 0% | 1
Acas XU | FC + ReLU | 13k | 5 | 0-20% | 1-4
cGAN |  | FC, Conv, ConvTranspose,
---
Residual + ReLU, BatchNorm, AvgPool
500k-68M | 5 | 0-40% | 2
Dist Shift | FC + ReLU, Sigmoid | 342k-855k | 792 | 98.9% | 1
ml4acopf | FC, Residual + ReLU, Sigmoid | 4k-680k | 22-402 | 0-7% | 1-600
blueTraffic Signs Recogn |  blueConv+Sign+MaxPool+BatchNorm, FC, |  blue905k-1.7M |  blue2.7k-12k |  blue0% |  blue43
ViT | Conv, FC, Residual + ReLU, Softmax, BatchNorm | 68k-76k | 3072 | 0% | 9

##  3 Theoretical Background

###  3.1 Deep Neural Networks

_Neural networks_ , inspired by the human brain, are computational models
composed of interconnected nodes called artificial neurons. These networks
have gained attention for their ability to learn and perform complex tasks.
The nodes compute outputs using _activation functions_ , and synaptic
_weights_ determine the strength of connections between nodes. Training is
achieved through optimization algorithms, such as _backpropagation_ , which
adjust the weights iteratively to minimize the network’s error.

A _deep neural network (DNN)_ [7] can be conceptualized as a directed graph,
where the nodes, also known as neurons, are organized in _layers_. The input
layer is responsible for receiving initial values, such as pixel intensities
in the case of image inputs, while the output layer generates the final
predictions or results. Hidden layers, positioned between the input and output
layers, play a crucial role in extracting and transforming information.

Figure 1: A fully connected DNN with 4 input nodes, 3 output nodes and 3
hidden layers

During the evaluation or inference process, the input values propagate through
the network, layer by layer, using connections between neurons. Each neuron
applies a specific mathematical operation to the inputs it receives, followed
by the _activation function_ that introduces _non-linearity_ to the network.
The activation function determines the neuron’s output based on the weighted
sum of its inputs and an optional bias term.

Different layer types are employed in neural networks to compute the values of
neurons based on the preceding layer’s neuron values. Those relevant for our
work are introduced in Section 3.2.

###  3.2 Binarized Neural Networks

A BNN [13] is a feedforward network where weights and activations are mainly
binary. [16] describes BNNs as sequential composition of blocks, each block
consisting of linear and non-linear transformations. One could distinguish
between _internal_ and _output blocks_.

There are typically several _internal blocks_. The layers of the blocks are
chosen in such a way that the resulting architecture fulfills the requirements
of accuracy, model size, number of parameters, for example. Typical layers in
an internal block are: [1)]

linear transformation (LIN)

binarization (BIN)

max pooling (MP)

batch normalization (BN). A linear transformation of the input vector can be
based on a fully connected layer or a convolutional layer. In our case is a
convolution layer since our experiments have shown that a fully connected
layer can not synthesize well the features of traffic signs, therefore, the
accuracy is low. The linear transformation is followed either by a
binarization or a max pooling operation. Max pooling helps in reducing the
number of parameters. One can swap binarization with max pooling, the result
would be the same. We use this sequence as Larq [10], the library we used in
our experiments, implements convolution and binarization in the same function.
Finally, scaling is performed with a batch normalization operation [14].

There is _one output block_ which produces the predictions for a given image.
It consists of a dense layer that maps its input to a vector of integers, one
for each output label class. It is followed by function which outputs the
index of the largest entry in this vector as the predicted label.

We make the observation that, if the MP and BN layers are omitted, then the
input and output of the internal blocks are binary, in which case, also the
input to the output block. The input of the first block is never binarized as
it drops down drastically the accuracy.

###  3.3 Properties of (Binarized) Neural Networks: Robustness

_Robustness_ is a fundamental property of neural networks that refers to their
ability to maintain stable and accurate outputs in the presence of
perturbations or adversarial inputs. Adversarial inputs are intentionally
crafted inputs designed to deceive or mislead the network’s predictions.

As defined by [16], _local robustness_ ensures that for a given input $x$ from
a set $\chi$, the neural network $F$ remains unchanged within a specified
perturbation radius $\epsilon$, implying that small variations in the input
space do not result in different outputs. The output for the input $x$ is
represented by its label $l_{x}$. We consider $L_{\infty}$ norm defined as
$||x||_{\infty}=\sup\limits_{n}|x_{n}|$, but also other norms can be used,
e.g. $L_{0}$ [18].

######  Definition 1 (Local robustness.).

A feedforward neural network $F$ is locally $\epsilon$-robust for an input
$x,x\in\chi$, if there does not exist $\tau,||\tau||_{\infty}\leq\epsilon$,
such that $F(x+\tau)\neq l_{x}$.

_Global robustness_ [16] is an extension of the local robustness and it is
defined as the expected maximum safe radius over a given test dataset,
representing a collection of inputs.

######  Definition 2 (Global robustness.).

A feed-forward neural network $F$ is globally $\epsilon$-robust if for any
$x,x\in\chi$, and $\tau,||\tau||_{\infty}\leq\epsilon$, we have that
$F(x+\tau)=l_{x}$.

The definitions above can not be used in a computational setting. Hence, [15]
proposes Definition 3 for local robustness which is equivalent to Definition
1.

######  Definition 3 (Local robustness.).

A network is $\epsilon$-locally robust in the input $x$ if for every
$x^{\prime}$, such that $||x-x^{\prime}||_{\infty}\leq\epsilon$, the network
assigns the same label to $x$ and $x^{\prime}$.

For our setting, the input is an image represented as a vector with values
represented by the pixels. Hence, the inputs are the vector $x$ and the
perturbation $\epsilon$.

This formula can also be applied to all inputs simultaneously (all images from
test set of the dataset), in that case _global robustness_ is addressed.
However, the number of parameters involved in checking _global robustness_
property increases enormously. Hence, in this paper, the benchmarks propose
verification of local robustness only.

##  4 Anatomy of the Binarized Neural Networks

For benchmarking, we propose the two BNNs architectures for which we obtained
the best accuracy [17], as well an additional one. More precisely, the best
accuracy for GTSRB and Belgium datasets is $96,45\%$ and $88,17\%$,
respectively, and was obtained for the architecture from Figure 2, with input
size 64$\times$64 (see Table 3). The number of parameters is almost $2$M and
the model size $225,67$ KiB (for the binary model) compared to $6932,48$ KiB
(for the Float-32 equivalent).

Figure 2: Accuracy Efficient Architecture for GTSRB and Belgium dataset Table 3: Best results for the architecture from Figure 2. Dataset for train: GTSRB. 2*Input size |  2*#Neur | Accuracy | #Params | Model Size (in KiB)
---|---|---|---|---
|  | German | China | Belgium | Binary | Real | Total | Binary | Float-32
64px $\times$ 64px | 1024 | 96.45 | 81.50 | 88.17 | 1772896 | 2368 | 1775264 | 225.67 | 6932.48

The best accuracy for Chinese dataset ($83,9\%$) is obtained by another
architecture, namely from Figure 3, with input size 48$\times$48 (see Table
4). This architecture is more efficient from the point of view of
computationally limited devices and formal verification having $900$k
parameters and $113,64$ KiB (for the binary model) and $3532,8$ KiB (for the
Float-32 equivalent). Also, the second architecture gave the best average
accuracy and the decrease in accuracy for GTSRB and Belgium is small, namely
$1,17\%$ and $0,39\%$, respectively.

Figure 3: Accuracy Efficient Architecture for Chinese dataset Table 4: Best results for the architecture from Figure 3. Dataset for train: GTSRB. 2*Input size |  2*#Neur | Accuracy | #Params | Model Size (in KiB)
---|---|---|---|---
|  | German | China | Belgium | Binary | Real | Total | Binary | Float-32
48px $\times$ 48px | 256 | 95.28 | 83.90 | 87.78 | 904288 | 832 | 905120 | 113.64 | 3532.80

One could observe that the best architectures were obtained for input size
images 48x48 and 64x64 pixels with max pooling and batch normalization layers
which reduce the number of neurons, namely perform scaling which leads to good
accuracy. We also propose for benchmarking an XNOR architecture, i.e.
containing only binary parameters, (Figure 4) for which we obtained the best
results for input size images 30x30 pixels and GTSRB (see Table 5).

Figure 4: XNOR(QConv) architecture Table 5: XNOR(QConv) architecture. Image size: 30px $\times$ 30px. Dataset for train and test: GTSRB. 2*Model description |  2*Acc |  2* | #Binary
---
Params
Model Size (in KiB)
|  |  | Binary | Float-32
|  QConv(16, 3$\times$3), QConv(32, 2$\times$2), D(43)
---
81.54 | 1005584 | 122.75 | 3932.16

##  5 Model and Property Specification: VNN-LIB and ONNX Formats

The VNN-LIB (Verified Neural Network Library) format [11] is a widely used
representation for encoding and exchanging information related to the
verification of neural networks. It serves as a standardized format that
facilitates the communication and interoperability of different tools and
frameworks employed in the verification of neural networks.

The VNN-LIB format typically consists of two files that provide a detailed
specification of the neural network model (see Section 5.1), along with
relevant properties and constraints (see Section 5.2). These files encapsulate
important information, including the network architecture, weights and biases,
input and output ranges, and properties to be verified.

###  5.1 Model Representation

In machine learning, the representation of models plays a vital role in
facilitating their deployment and interoperability across various frameworks
and platforms. One commonly used format is the H5 format, which is an
abbreviation for _Hierarchical Data Format version 5_. The H5 format provides
a structured and efficient means of storing and organizing large amounts of
data, including the parameters and architecture of machine learning models. It
is widely supported by popular deep learning frameworks, such as TensorFlow
and Keras, allowing models to be saved, loaded, and shared in a standardized
manner.

However, while the H5 format serves as a convenient model representation for
specific frameworks, it may lack compatibility when transferring models
between different frameworks or performing model verification. This is where
the _Open Neural Network Exchange_ (ONNX) format comes into play. ONNX offers
a vendor-neutral, open-source alternative that allows models to be represented
in a standardized format, enabling seamless exchange and collaboration across
multiple deep learning frameworks.

The VNN-LIB format, which is used for the formal verification of neural
network models, leverages ONNX as its underlying model representation.

###  5.2 Property specification

For property specification, VNN-LIB standard uses the SMT-LIB format. The SMT-
LIB (Satisfiability Modulo Theories-LIBrary) language [8] is a widely
recognized formal language utilized for the formalization of Satisfiability
Modulo Theories (SMT) problems.

A VNN-LIB file is structured as follows555See, e.g.
https://github.com/apostovan21/vnncomp2023/blob/master/vnnlib/model_30_idx_1678_eps_1.00000.vnnlib
and the elements involved have the following semantics for the considered
image classification task:

  1. 1.

definition of input variables representing the values of the pixels $X_{i}$
($i=\overline{1,P}$, where $P$ is the dimension of the input image: $N\times
M\times 3$ pixels). For the file above, there are $2700$ variables as the
image has dimension $30\times 30$ and the channel used is RGB.

  2. 2.

definition of the output variables representing the values $Y_{j}$
($j=\overline{1,L}$, where $L$ is the number of classes of the images in the
dataset). For the file above, there are $43$ variables as the GTSRB
categorises the traffic signs images into $43$ classes.

  3. 3.

bounding constraints for the variables input variables. Definition 5.1 is used
for generating the property taking into account that vector $x$ (its elements
are the values of the pixels of the image) and $\varepsilon$ (perturbation)
are known. For example, if $\varepsilon=10$ and the value of the pixel
$X_{2699}^{\prime}$ of the image with index $1678$ from GTSRB is $24$, the
generated constraints for finding the values of the perturbed by $\varepsilon$
pixel $X_{2699}$ for which the predicted label still holds is:

            (assert (<= X_2699 34.00000000))
        (assert (>= X_2699 14.00000000))

  4. 4.

constraints involving the output variables assessing the value of the output
label. For example, if the verification problem is formulated as: _Given the
image with index $1678$, the perturbation $\varepsilon~{}=~{}10$ and the
trained model, find if the perturbed images are in class $38$_, the generated
constraints are as follows which actually represents the negation of the
property to be checked:

            (assert (or (>= Y_0 Y_38)
                    ...
                    (>= Y_37 Y_38)
                    (>= Y_39 Y_38)
                    ...
                    (>= Y_42 Y_38)))

##  6 Benchmarks Proposal and Experimental Results of the VNN-COMP 2023

To meet the requirements of the VNN-COMP 2023, the benchmark datasets must
conform to the ONNX format for defining the neural networks, while the problem
specifications are expected to adhere to the VNN-LIB format. Therefore, we
have prepared a benchmark set comprising the BNNs introduced in Section 4 that
have been encoded in the ONNX format. In order to assess the adversarial
robustness of these networks, the problem specifications encompassed
perturbations within the infinity norm around zero, with radius denoted as
$\epsilon=\\{1,3,5,10,15\\}$. To achieve this, we randomly selected three
distinct images from the test set of the GTSRB dataset for each model and have
generated the VNNLIB files for each epsilon in the set, in the way we ended up
having 45 VNNLIB files in total. We were constrained to generate the small
benchmark which includes just 45 VNNLIB files because of the total timeout
which should not exceed 6 hour, this is the maximum timeout for a solver to
address all instances, consequently a timeout of 480 seconds was allocated for
each instance. For checking the generated VNNLIB specification files for
submitted in the VNNCOMP 2023 as specified above as well as to generate new
ones you can check https://github.com/apostovan21/vnncomp2023.

Our benchmark was used for scoring the competing tools. The results for our
benchmark, as presented by the VNN-COMP 2023 organizers, are presented in
Table 6.

Table 6: VNN-COMP 2023 Results for Traffic Signs Recognition Benchmark # | Tool | Verified | Falsified | Fastest | Penalty | Score | Percent
---|---|---|---|---|---|---|---
1 | Marabou | 0 | 18 | 0 | 1 | 30 | 100%
2 | PyRAT | 0 | 7 | 0 | 1 | -80 | 0%
3 | NeuralSAT | 0 | 31 | 0 | 4 | -290 | 0%
4 | alpha-beta-CROWN | 0 | 39 | 0 | 3 | -60 | 0%

The meaning of the columns is as follows. Verified is number of instances that
were UNSAT (no counterexample) and proven by the tool. Falsifieid is number
that were SAT (counterexample was found) and reported by the tool. Fastest is
the number where the tool was fastest (this did not impact the scoring in this
year competition). Penalty is the number where the tool gave the incorrect
result or did not produce a valid counterexample. Score is the sum of scores
($10$ points for each correct answer and $-150$ for incorrect ones). Percent
is the score of the tool divided by the best score for the benchmark (so the
tool with the highest score for each benchmark gets $100$) and was used to
determine final scores across all benchmarks.

Currently, we are investigating if the number of solved instances could be
higher if the time is increased (the deadline used was 8 minutes). Also, it is
interesting why the tools gave incorrect results for some benchmarks.

##  7 Conclusions

Building upon our prior study that introduced precise binarized neural network
models for traffic sign recognition, this study presents standardized
challenges to gauge the resilience of these networks to local variations.
These challenges were entered into the VNN-COMP 2023 evaluation, where 4 out
of 7 tools produced results. Our current emphasis is on investigating the
potential for solving more instances by extending the time limit (formerly set
at 8 minutes). Additionally, we are keen to comprehend the factors
contributing to incorrect outputs from the tools on specific benchmark tasks.

## Acknowledgements

This work was supported by a grant of the Romanian National Authority for
Scientific Research and Innovation, CNCS/CCCDI - UEFISCDI, project number PN-
III-P1-1.1-TE-2021-0676, within PNCDI III.

## References

  * [1]
  * [2] _Belgian Traffic Sign Database_.  https://www.kaggle.com/datasets/shazaelmorsh/trafficsigns.  Accessed: March 25th, 2023.
  * [3] _Benchmarks of the 3rd International Verification of Neural Networks Competition (VNN-COMP’22)_.  https://github.com/ChristopherBrix/vnncomp2022_benchmarks.  Accessed: February 22nd, 2023.
  * [4] _Benchmarks of the 4th International Verification of Neural Networks Competition (VNN-COMP’23)_.  https://github.com/ChristopherBrix/vnncomp2023_benchmarks.  Accessed: July 26th, 2023.
  * [5] _Chinese Traffic Sign Database_.  https://www.kaggle.com/datasets/dmitryyemelyanov/chinese-traffic-signs.  Accessed: March 25th, 2023.
  * [6] _German Traffic Sign Recognition Benchmark_.  https://www.kaggle.com/datasets/meowmeowmeowmeowmeow/gtsrb-german-traffic-sign?datasetId=82373&language=Python.  Accessed: March 25th, 2023.
  * [7] Guy Amir, Haoze Wu, Clark Barrett & Guy Katz (2021): _An SMT-Based Approach for Verifying Binarized Neural Networks_.  In Jan Friso Groote & Kim Guldstrand Larsen, editors: Tools and Algorithms for the Construction and Analysis of Systems, Springer International Publishing, Cham, pp. 203–222, 10.1007/978-3-030-72013-1_11.
  * [8] Clark Barrett, Aaron Stump, Cesare Tinelli et al. (2010): _The SMT-LIB Standard: Version 2.0_.  In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), 13, p. 14.
  * [9] Dan Ciregan, Ueli Meier & Jürgen Schmidhuber (2012): _Multi-Column Deep Neural Networks for Image Classification_.  In: 2012 IEEE Conference on Computer Vision and Pattern Recognition, IEEE, pp. 3642–3649, 10.1109/CVPR.2012.6248110.
  * [10] Lukas Geiger & Plumerai Team (2020): _Larq: An Open-Source Library for Training Binarized Neural Networks_.  Journal of Open Source Software 5(45), p. 1746, 10.21105/joss.01746.
  * [11] Dario Guidotti, Stefano Demarchi, Armando Tacchella & Luca Pulina (2023): _The Verification of Neural Networks Library (VNN-LIB)_.  Available at https://www.vnnlib.org.
  * [12] Xingwu Guo, Ziwei Zhou, Yueling Zhang, Guy Katz & Min Zhang (2023): _OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks_.  In Sriram Sankaranarayanan & Natasha Sharygina, editors: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature Switzerland, Cham, pp. 208–226, 10.1007/978-3-031-30823-9_11.
  * [13] Itay Hubara, Matthieu Courbariaux, Daniel Soudry, Ran El-Yaniv & Yoshua Bengio (2016): _Binarized Neural Networks_.  Advances in Neural Information Processing Systems 29\.
  * [14] Sergey Ioffe & Christian Szegedy (2015): _Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift_.  In: International conference on machine learning, PMLR, pp. 448–456, 10.48550/arXiv.1502.03167.
  * [15] Guy Katz, Clark Barrett, David L Dill, Kyle Julian & Mykel J Kochenderfer (2022): _Reluplex: A Calculus for Reasoning about Deep Neural Networks_.  Formal Methods in System Design 60(1), pp. 87–116, 10.1007/s10703-021-00363-7.
  * [16] Nina Narodytska, Shiva Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv & Toby Walsh (2018): _Verifying properties of binarized deep neural networks_.  In: Proceedings of the AAAI Conference on Artificial Intelligence, 32, 10.1609/aaai.v32i1.12206.
  * [17] Andreea Postovan & Mădălina Eraşcu (2023): _Architecturing Binarized Neural Networks for Traffic Sign Recognition_.  arXiv preprint arXiv:2303.15005, 10.48550/arXiv.2303.15005.
  * [18] Wenjie Ruan, Min Wu, Youcheng Sun, Xiaowei Huang, Daniel Kroening & Marta Kwiatkowska (2019): _Global robustness evaluation of deep neural networks with provable guarantees for the hamming distance_.  IJCAI-19, 10.24963/ijcai.2019/824.
  * [19] Johannes Stallkamp, Marc Schlipsing, Jan Salmen & Christian Igel (2012): _Man vs. Computer: Benchmarking Machine Learning Algorithms for Traffic Sign Recognition_.  Neural networks 32, pp. 323–332, 10.1016/j.neunet.2012.02.016.
  * [20] Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow & Rob Fergus (2013): _Intriguing Properties of Neural Networks_.  arXiv preprint arXiv:1312.6199, 10.48550/arXiv.1312.6199.
  * [21] Huan Zhang, Kaidi Xu, Shiqi Wang & Cho-Jui Hsieh (2022): _Formal Verification of Deep Neural Networks: Theory and Practice_.  https://neural-network-verification.com/.  Tutorial at AAAI 2022.
  * [22] Jianming Zhang, Wei Wang, Chaoquan Lu, Jin Wang & Arun Kumar Sangaiah (2020): _Lightweight Deep Network for Traffic Sign Classification_.  Annals of Telecommunications 75, pp. 369–379, 10.1007/s12243-019-00731-9.