Benchmarking Local Robustness of High-Accuracy Binary Neural Networks
  for Enhanced Traffic Sign Recognition
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.
Andreea Postovan, Mădălina Eraşcu
Benchmarking Local Robustness of High-Accuracy Binary Neural Networks for Enhanced Traffic Sign Recognition

###### 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](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)1 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\)-CROWN2.

Footnote 1: [https://github.com/stanleybak/vnncomp2023/issues/2](https://github.com/stanleybak/vnncomp2023/issues/2)

Footnote 2: [https://github.com/Verified-Intelligence/alpha-beta-CROWN](https://github.com/Verified-Intelligence/alpha-beta-CROWN)

We publicly released our benchmark 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 Marabou3 (19) with only 1 incorrect answer.

Footnote 3: [https://github.com/NeuralNetworkVerification/Marabou](https://github.com/NeuralNetworkVerification/Marabou)

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 [10] 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 benchmark4.

Footnote 4: See [https://github.com/stanleybak/vnncomp2023/issues/2](https://github.com/stanleybak/vnncomp2023/issues/2) intervention from user stanleybak on May 17, 2023

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

\begin{table}
\begin{tabular}{c c c c c}
**Category** & **Benchmark** & **Network Types** & **\#Neurons** & **Input Dimension** \\ \hline \multirow{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 \\ \hline Fully-Connected & MNIST FC & FC. + ReLU & 512 - 1.5k & 784 \\ \end{tabular}
\end{table}
Table 1: Benchmarks proposed in the VNN-COMP 2022 for image classification tasks
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 regions and no sparsity.

## 3 Theoretical Background

### 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. 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 _nonlinearity_ 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.

\begin{table}
\begin{tabular}{c c c c c c}
**Name** & **Network Type** & **\# of Params** & 
\begin{tabular}{c} **Input** \\ **Dimension** \\ \end{tabular} & **Sparsity** & **\# of Regions** \\ \hline nn4sys & Conv, FC, Residual + ReLU, Sigmoid & 33k - 37M & 1-308 & 0-66\% & 1 - 11k \\ \hline VGGNet16 & Conv + ReLU + MaxPool & 138M & 150k & 0-99\% & 1 \\ \hline Collins Rul CNN & Conv + ReLU, Dropout & 60k - 262k & 400-800 & 50-99\% & 2 \\ \hline TLL Verify Bench & FC + ReLU & 17k - 67M & 2 & 0\% & 1 \\ \hline Acas XU & FC + ReLU & 13k & 5 & 0-20\% & 1-4 \\ \hline \multirow{2}{*}{cGAN} & FC, Conv, Conv/Transpose, & \multirow{2}{*}{500k-68M} & \multirow{2}{*}{5} & \multirow{2}{*}{0-40\%} & \multirow{2}{*}{2} \\  & Residual + ReLU, BatchNorm, AvgPool & & & & \\ \hline Dist Shift & FC + ReLU, Sigmoid & 342k-855k & 792 & 98.9\% & 1 \\ \hline ml4acopf & FC, Residual + ReLU, Sigmoid & 4k-680k & 22-402 & 0-7\% & 1-600 \\ \hline Traffic Signs Recogn & Conv+Sign+MaxPool+BatchNorm, FC, & 905k-1.7M & 2.7k-12k & 0\% & 43 \\ \hline ViT & Conv, FC, Residual + ReLU, Softmax, BatchNorm & 68k-76k & 3072 & 0\% & 9 \\ \hline \end{tabular}
\end{table}
Table 2: Benchmarks proposed in the VNN-COMP 2023
### Binarized Neural Networks

A BNN [12] is a feedforward network where weights and activations are mainly binary. [15] 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) _2)_ binarization (BIN) _3)_ max pooling (MP) _4)_ 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 [9], the library we used in our experiments, implements convolution and binarization in the same function. Finally, scaling is performed with a batch normalization operation [13].

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.

### 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 [15], _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}\)[17].

**Definition 3.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}\).

Figure 1: A fully connected DNN with 4 input nodes, 3 output nodes and 3 hidden layers
_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 3.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.3 for local robustness which is equivalent to Definition 3.1.

**Definition 3.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).

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.

One could observe that the best architectures were obtained for input size images \(48\times\)\(48\) and \(64\times\)\(64\) 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 \(30\)x\(30\) pixels and GTSRB (see Table 5).

\begin{table}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|} \hline \multirow{2}{*}{**Input size**} & \multirow{2}{*}{**\#Neur**} & \multicolumn{3}{c|}{**Accuracy**} & \multicolumn{3}{c|}{**\#Params**} & \multicolumn{1}{c|}{**Model Size (in KiB)**} \\ \cline{3-9}  & & **German** & **China** & **Belgium** & **Binary** & **Real** & **Total** & **Binary** & **Float-32** \\ \hline
64px \(\times\) 64px & \(1024\) & **96.45** & **81.50** & **88.17** & 1772896 & 2368 & 1775264 & 225.67 & 6932.48 \\ \hline \end{tabular}
\end{table}
Table 3: Best results for the architecture from Figure 2. Dataset for train: GTSRB.

Figure 2: Accuracy Efficient Architecture for GTSRB and Belgium dataset
## 5 Model and Property Specification: VNN-LIB and ONNX Formats

The VNN-LIB (Verified Neural Network Library) format [10] 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.

### 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.

### Property specification

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

A VNN-LIB file is structured as follows5 and the elements involved have the following semantics for

\begin{table}
\begin{tabular}{|l|c|c|c|c|c|c|c|c|c|} \hline \multirow{2}{*}{**Input size**} & \multirow{2}{*}{**\#Neur**} & \multicolumn{3}{c|}{**Accuracy**} & \multicolumn{3}{c|}{**\#Params**} & \multicolumn{1}{c|}{**Model Size (in KiB)**} \\ \cline{3-10}  & & **German** & **China** & **Belgium** & **Binary** & **Real** & **Total** & **Binary** & **Float-32** \\ \hline
48px \(\times\) 48px & 256 & **95.28** & **83.90** & **87.78** & 904288 & 832 & 905120 & 113.64 & 3532.80 \\ \hline \end{tabular}
\end{table}
Table 4: Best results for the architecture from Figure 3. Dataset for train: GTSRB.

Figure 3: Accuracy Efficient Architecture for Chinese dataset
the considered image classification task:

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. 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. 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 \(\epsilon\) (perturbation) are known. For example, if \(\epsilon=10\) and the value of the pixel \(X^{\prime}_{2699}\) of the image with index 1678 from GTSRB is 24, the generated constraints for finding the values of the perturbed by \(\epsilon\) pixel \(X_{2699}\) for which the predicted label still holds is: (assert (<= X_2699 34.0000000)) (assert (>= X_2699 14.0000000))
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 \(\epsilon~{}=~{}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

Figure 4: XNOR(QConv) architecture

\begin{table}
\begin{tabular}{|l|c|c|c|c|} \hline
**Model description** & **Acc** & \begin{tabular}{c} **\#Binary** \\ **Params** \\ \end{tabular} & 
\begin{tabular}{c} **Model Size (in KiB)** \\ **Binary** \\ \end{tabular} \\ \hline QConv(16, 3\(\times\)3), QConv(32, 2\(\times\)2), D(43) & 81.54 & 1005584 & 122.75 & 3932.16 \\ \hline \end{tabular}
\end{table}
Table 5: XNOR(QConv) architecture. Image size: 30px \(\times\) 30px. Dataset for train and test: GTSRB.
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](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.

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.

\begin{table}
\begin{tabular}{l c c c c c c} \# & **Tool** & **Verified** & **Falsified** & **Fastest** & **Penalty** & **Score** & **Percent** \\ \hline
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\% \\ \end{tabular}
\end{table}
Table 6: VNN-COMP 2023 Results for Traffic Signs Recognition Benchmark