# CowStallNumbers: A Small Dataset for Stall Number Detection
of Cow Teats Images

Youshan Zhang
Yeshiva University, NYC, NY
<EMAIL_ADDRESS>
###### Abstract

In this paper, we present a small cow stall number dataset named
CowStallNumbers, which is extracted from cow teat videos with the goal of
advancing cow stall number detection. This dataset contains 1042 training
images and 261 test images with the stall number ranging from 0 to 60. In
addition, we fine-tuned a ResNet34 model and augmented the dataset with the
random crop, center crop, and random rotation. The experimental result
achieves a 92% accuracy in stall number recognition and a 40.1% IoU score in
stall number position prediction.

##  1 Introduction

In recent years, the dairy industry has expanded rapidly as the demand for
milk and milk products grow. One of the critical aspects of dairy farming is
the management of the herd’s health and productivity. To maximize milk
production and maintain the cows’ health, it is necessary to ensure that the
cows have a comfortable environment, appropriate feed, and regular health
checks. We previously studied how to classify different categories of teats
[25, 26]. However, these teat images were taken by phone and manually cropped.
To save time, we set up a camera toward the teat-end areas [27]; we proposed
to extract the key teat frames from the video images, which leads to another
problem that we cannot recognize the cows’ ID unless we can recognize the
stall number in the videos. Therefore, we need to develop a model to recognize
the stall numbers.

Figure 1: Timeline of You Only Look Once (YOLO) variants.

In this paper, we fine-tune the ResNet34 model for cow stall detection. We
evaluate our method using a small dataset of cow images with ground truth
annotations for cow stall locations. Our results show that our method achieves
high accuracy in cow stall detection, and can provide a valuable tool for
dairy farmers to optimize their operations. By enabling accurate and efficient
cow stall detection, we can improve the health and productivity of cows and,
in turn, increase the sustainability and profitability of the dairy industry.
Our contributions are two-fold:

  * •

We present a small cow stall number dataset named CowStallNumber with the goal
of advancing the field of cow stall number detection.

  * •

We fine-tuned the pre-trained ResNet34 model to get the position of the stall
number and recognize different stall numbers. We achieved a 95% accuracy in
stall number recognition and a 40.1% IoU score in box position prediction.

##  2 Related Work

The faster Region-based Convolutional Neural Network (R-CNN) algorithm has
been applied for cow tail detection, achieving higher accuracy and faster
detection times than the R-CNN algorithm [11]. However, one limitation of
these object detection algorithms is that they struggle with detecting objects
in certain environmental conditions, such as poor lighting or low contrast.
This is a concern in cow detection since cows blend in with their surroundings
or have their identifying features obscured by shadows or other visual
obstructions.

To address this issue, thermal imaging cow detection has been explored [2].
Thermal imaging uses infrared technology to detect the heat signature of an
object, which allows for more accurate detection in low-light or low-contrast
environments. In addition, thermal imaging can detect cows even in situations
where they are partially hidden, such as behind bushes or in tall grass.
Despite the advances in cow detection technology, there are still challenges
to be overcome. For example, detecting cows in large herds can be difficult,
as cows can tightly pack together and partially obstruct each other from view.
Furthermore, different breeds of cows may have unique physical characteristics
that require specific detection algorithms. We will review the related work of
object detection in the following paragraphs.

Figure 2: Example of three stall images (44, 13, and 0). Figure 3: Example
contents in the CSV file. ImageFilename is the cow stall number image.
[Box_position_1, Box_position_2, Box_position_3, Box_position_4] means that
[x, y, height, width] of the bounding box location. Class_name is the stall
number class. Empty space means we cannot detect the stall number in the
image.

Girshick et al. proposed the R-CNN model, which applied a region proposal
algorithm to generate candidate object regions. Then, it is passed to a
convolutional neural network (CNN) for classification [8]. Later, Girshick
proposed a Fast R-CNN model, which is an improved version of R-CNN that uses a
shared feature map for region proposal and classification, resulting in faster
and more accurate detection [7]. Ren et al. developed a Faster R-CNN model,
which is another extension of R-CNN that introduces a Region Proposal Network
(RPN) to generate region proposals more efficiently, making it the first real-
time object detection method [22]. You Only Look Once (YOLO) is a real-time
object detection method that generates predictions directly from the whole
image, which is based on a single CNN that simultaneously predicts the class
and position of each object. Redmon et al. [18] presented a Single Shot
MultiBox Detector (SSD) model, which generates object proposals and predicts
their class and location using a single neural network. SSD is faster compared
to Faster R-CNN and achieves higher accuracy than YOLO. Lin et al. proposed a
RetinaNet [17], which introduces a novel focal loss function that down-weights
easy examples and up-weights hard examples. Mask R-CNN [9] is an extension of
Faster R-CNN, which adds a branch to predict segmentation masks for each
object, and it can segment the detected objects in addition to their bounding
boxes. Cascade R-CNN [4] model is a variant of Faster R-CNN that utilizes a
cascade of detectors to improve the detection quality. Lin et al. proposed a
Feature Pyramid Network (FPN) model [16] that generates a pyramid of feature
maps that are used for object detection at different scales and improves the
performance of object detectors. FPN. DetNet [15] incorporates deformation-
aware convolutional layers that can handle object deformations and viewpoint
changes. DenseBox [10] applies dense regression to predict the coordinates of
object bounding boxes. CoupleNet [28] can predict the position and size of
objects in a coupled manner, leading to improved performance compared to other
real-time detection methods. Kong et al. proposed a Reverse Connection with
Objectness Prior Networks (RON) model [13] that uses a reverse connection to
capture context information for object proposal generation. RefineDet [24] is
a multi-stage object detection method that progressively refines the location
and size of object proposals. Edge Sampling Decoder (ESD) [5] incorporates
edge sampling into deep neural networks to detect edges and boundaries of
objects. Neural Architecture Search with Feature Pyramid Network (NAS-FPN) [6]
uses neural architecture search to design a feature pyramid network that
improves object detection performance.

There are also different variants of YOLO methods as shown in Fig. 1. YOLOv1
[19] was introduced in 2016. YOLOv2 (YOLO9000) [20] was released in 2017 and
used a Darknet-19 network architecture and incorporated batch normalization
and anchor boxes. It also introduced multi-scale predictions, enabling the
detection of objects at different scales. YOLOv3 [21] was released in 2018 and
used a Darknet-53 network architecture, introduced feature pyramid networks
(FPNs), and used residual connections. It also used anchor boxes with dynamic
scaling, leading to better detection at different scales. YOLOv4 [3] was
released in 2020, which used a CSPDarknet-53 network architecture, added
various improvements such as spatial pyramid pooling, and used a complex data
augmentation pipeline. YOLOv4 also included efficient training approaches such
as mosaic data augmentation and focal loss. YOLOv5 [12] was a PyTorch
implementation rather than a fork from the original Darknet, which has a CSP
backbone and PA-NET neck. The major improvement includes auto-learning
bounding box anchors. YOLOv6 [14] was released in 2022 and was a single-stage
object detection framework dedicated to industrial applications, with
hardware-friendly efficient design and high performance. YOLOv7 [23] was
released in 2022 and reduced the number of parameters by 75%, requires 36%
less computation, and achieves 1.5% higher AP (average precision) compared
with YOLOv4. YOLOv7-X achieves a 21 FPS faster inference speed than YOLOv5-X.
The YOLOv8 [1] model is fast, accurate, and easy to use, which can be applied
to a wide range of object detection and image segmentation tasks. It can be
trained on large datasets and run on various hardware platforms, from CPUs to
GPUs.

##  3 Data collection

The stall number images are retrieved from cow teat videos, which are recorded
to inspect the cow teats’ health status. More details of video recording
settings can be found in [27]. We first applied the unsupervised few-shot key
frame extraction (UFSKEF) model in [27] to extract the coarse stall number key
frames. We then manually checked these key frames and removed the wrong key
frame images. Fig. 2 shows three example stall numbers, where 0 means that we
cannot detect the stall numbers. Tab. LABEL:tab:stas lists the statistics of
our CowStallNumber dataset. Fig. 3 represents the content of training and test
CSV files.

Figure 4: The architecture of our stall number detection model. We fine-tune a ResNet34 model and add two output layers (for stall number box $[88,268,108,292]$ and stall number $50$, respectively). Figure 5: Three example outputs of our model. True box: true bounding box location; Pred box: predicted bounding box location. Table 1: Statistics of our CowStallNumber dataset | Training | Test | Total
---|---|---|---
Numbers | 1042 | 261 | 1303

##  4 Methods

Since stall number detection is an object detection problem, we evaluate the
performance of the stall number box using the IoU score in Eq.(1) and report
the recognition accuracy of stall number using accuracy in Eq.(2).

$IoU=\frac{|A\cap B|}{|A\cup B|},$ (1)

where $A$ is the ground truth stall bounding box, and $B$ is the predicted
stall bounding box.

$\text{Accuracy}=\frac{1}{n}\sum_{i=1}^{n}(Y_{i}==\hat{Y_{i}})\times 100,$ (2)

where $Y_{i}$ is ground truth stall number, and $\hat{Y_{i}}=f(X_{i})$ is the
predicted stall number ($X_{i}$ is the input stall image and $f$ is our fine-
tune ResNet34 model).

We apply L1 loss to optimize the bounding box and cross-entropy loss to
optimize the stall number recognition. The overall architecture of our model
is shown in Fig. 4, and the objective function is shown in the following
equation.

$\mathcal{L}=\frac{1}{n}\sum_{i=1}^{n}\\{\alpha|A_{i}-B_{i}|_{1}+\mathcal{L}_{ce}(f(X_{i}),Y_{i})\\},$
(3)

where $|\cdot|$ is the L1 loss, $\mathcal{L}_{ce}$ is the typical cross-
entropy loss and $\alpha$ is the balance factor between L1 loss and cross-
entropy loss.

##  5 Implementation details

During the training of our model, we set batch size = 64, training iteration
$I=300$, and learning rate = 0.06, $\alpha=1/1000$ with an Adam optimizer on a
48G RTX A6000 GPU using PyTorch. The input image size is $270\times 480$. We
also perform the random crop, center crop, and random rotation to augment more
images. The dataset is available at
https://github.com/YoushanZhang/Cow_stall_number.

##  6 Results

Tab. 2 shows the results of our model. We can find that the stall number
recognition accuracy is high, while the IoU score is low. This implies that
our model can successfully recognize the stall numbers. However, the low IoU
score means that the bounding box of the stall number is not correctly
predicted, which can lead to a low $\alpha$ value during the training. Another
reason is that there are significant differences between different stall
images (e.g., light, location, etc.). Fig. 5 shows three output images of our
model. All stall numbers are correctly predicted, while the stall number
positions differ slightly from the ground truth positions.

Table 2: Stall number detection results (% means $\times 100$) Method | IoU (%) | Accuracy (%)
---|---|---
ResNet34 | 40.1 | 95.0

##  7 Conclusion

In this paper, we create a small cow stall number dataset named
CowStallNumbers with the goal of advancing cow stall number detection. We
fine-tuned a ResNet34 model and augmented the datasets with the random crop,
center crop, and random rotation. The experimental result achieves a 92%
accuracy in stall number recognition and a 40.1% IoU score in stall number
position prediction. For future work, exploring a better object detection
model (e.g., YOLOV8) could further improve the performance of stall number
detection.

## References

  * [1] Yolov8 docs.  https://docs.ultralytics.com/.  Accessed: 2023-03-15.
  * [2] A Anagnostopoulos, M Barden, J Tulloch, K Williams, B Griffiths, C Bedford, M Rudd, Androniki Psifidi, G Banos, and Georgios Oikonomou.  A study on the use of thermal imaging as a diagnostic tool for the detection of digital dermatitis in dairy cattle.  Journal of dairy science, 104(9):10194–10202, 2021.
  * [3] Alexey Bochkovskiy, Chien-Yao Wang, and Hong-Yuan Mark Liao.  Yolov4: Optimal speed and accuracy of object detection.  arXiv preprint arXiv:2004.10934, 2020.
  * [4] Zhaowei Cai and Nuno Vasconcelos.  Cascade r-cnn: Delving into high quality object detection.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 6154–6162, 2018.
  * [5] Kean Chen, Jianguo Li, Weiyao Lin, John See, Ji Wang, Lingyu Duan, Zhibo Chen, Changwei He, and Junni Zou.  Towards accurate one-stage object detection with ap-loss.  In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pages 5119–5127, 2019.
  * [6] Golnaz Ghiasi, Tsung-Yi Lin, and Quoc V Le.  Nas-fpn: Learning scalable feature pyramid architecture for object detection.  In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, pages 7036–7045, 2019.
  * [7] Ross Girshick.  Fast r-cnn.  In Proceedings of the IEEE international conference on computer vision, pages 1440–1448, 2015.
  * [8] Ross Girshick, Jeff Donahue, Trevor Darrell, and Jitendra Malik.  Region-based convolutional networks for accurate object detection and segmentation.  IEEE transactions on pattern analysis and machine intelligence, 38(1):142–158, 2015.
  * [9] Kaiming He, Georgia Gkioxari, Piotr Dollár, and Ross Girshick.  Mask r-cnn.  In Proceedings of the IEEE international conference on computer vision, pages 2961–2969, 2017.
  * [10] Lichao Huang, Yi Yang, Yafeng Deng, and Yinan Yu.  Densebox: Unifying landmark localization with end to end object detection.  arXiv preprint arXiv:1509.04874, 2015.
  * [11] Xiaoping Huang, Xinru Li, and Zelin Hu.  Cow tail detection method for body condition score using faster r-cnn.  In 2019 IEEE International Conference on Unmanned Systems and Artificial Intelligence (ICUSAI), pages 347–351. IEEE, 2019.
  * [12] Nelson Joseph and Solawetz Jacob.  Yolov5 is here: State-of-the-art object detection at 140 fps.  https://blog.roboflow.com/yolov5-is-here/.  Accessed: 2023-03-15.
  * [13] Tao Kong, Fuchun Sun, Anbang Yao, Huaping Liu, Ming Lu, and Yurong Chen.  Ron: Reverse connection with objectness prior networks for object detection.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 5936–5944, 2017.
  * [14] Chuyi Li, Lulu Li, Hongliang Jiang, Kaiheng Weng, Yifei Geng, Liang Li, Zaidan Ke, Qingyuan Li, Meng Cheng, Weiqiang Nie, et al.  Yolov6: A single-stage object detection framework for industrial applications.  arXiv preprint arXiv:2209.02976, 2022.
  * [15] Zeming Li, Chao Peng, Gang Yu, Xiangyu Zhang, Yangdong Deng, and Jian Sun.  Detnet: A backbone network for object detection.  arXiv preprint arXiv:1804.06215, 2018.
  * [16] Tsung-Yi Lin, Piotr Dollár, Ross Girshick, Kaiming He, Bharath Hariharan, and Serge Belongie.  Feature pyramid networks for object detection.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 2117–2125, 2017.
  * [17] Tsung-Yi Lin, Priya Goyal, Ross Girshick, Kaiming He, and Piotr Dollár.  Focal loss for dense object detection.  In Proceedings of the IEEE international conference on computer vision, pages 2980–2988, 2017.
  * [18] Wei Liu, Dragomir Anguelov, Dumitru Erhan, Christian Szegedy, Scott Reed, Cheng-Yang Fu, and Alexander C Berg.  Ssd: Single shot multibox detector.  In Computer Vision–ECCV 2016: 14th European Conference, Amsterdam, The Netherlands, October 11–14, 2016, Proceedings, Part I 14, pages 21–37. Springer, 2016.
  * [19] Joseph Redmon, Santosh Divvala, Ross Girshick, and Ali Farhadi.  You only look once: Unified, real-time object detection.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 779–788, 2016.
  * [20] Joseph Redmon and Ali Farhadi.  Yolo9000: better, faster, stronger.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 7263–7271, 2017.
  * [21] Joseph Redmon and Ali Farhadi.  Yolov3: An incremental improvement.  arXiv preprint arXiv:1804.02767, 2018.
  * [22] Shaoqing Ren, Kaiming He, Ross Girshick, and Jian Sun.  Faster r-cnn: Towards real-time object detection with region proposal networks.  Advances in neural information processing systems, 28, 2015.
  * [23] Chien-Yao Wang, Alexey Bochkovskiy, and Hong-Yuan Mark Liao.  Yolov7: Trainable bag-of-freebies sets new state-of-the-art for real-time object detectors.  arXiv preprint arXiv:2207.02696, 2022.
  * [24] Shifeng Zhang, Longyin Wen, Xiao Bian, Zhen Lei, and Stan Z Li.  Single-shot refinement neural network for object detection.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 4203–4212, 2018.
  * [25] Youshan Zhang, Parminder S Basran, Ian R Porter, and Matthias Wieland.  Dairy cows teat-end condition classification using separable transductive learning.  In 61st National Mastitis Council (NMC) Annual Meeting, 2022.
  * [26] Youshan Zhang, Ian R Porter, Matthias Wieland, and Parminder S Basran.  Separable confident transductive learning for dairy cows teat-end condition classification.  Animals, 12(7):886, 2022.
  * [27] Youshan Zhang, Matthias Wieland, and Parminder S Basran.  Unsupervised few shot key frame extraction for cow teat videos.  Data, 7(5):68, 2022.
  * [28] Yousong Zhu, Chaoyang Zhao, Jinqiao Wang, Xu Zhao, Yi Wu, and Hanqing Lu.  Couplenet: Coupling global structure with local parts for object detection.  In Proceedings of the IEEE international conference on computer vision, pages 4126–4134, 2017.


11institutetext:  TU Wien, Austria 22institutetext: AIT Austrian Institute of
Technology, Austria

# Verifying Global Two-Safety Properties in Neural Networks with Confidence

Anagha Athavale1,2 Ezio Bartocci1 Maria Christakis1 Matteo Maffei 1 Dejan
Nickovic2 and Georg Weissenbacher1

###### Abstract

We present the first automated verification technique for confidence-based
2-safety properties, such as global robustness and global fairness, in deep
neural networks (DNNs). Our approach combines self-composition to leverage
existing reachability analysis techniques and a novel abstraction of the
softmax function, which is amenable to automated verification. We characterize
and prove the soundness of our static analysis technique. Furthermore, we
implement it on top of Marabou, a safety analysis tool for neural networks,
conducting a performance evaluation on several publicly available benchmarks
for DNN verification.

††footnotetext: Accepted at the 36th International Conference on Computer
Aided Verification, 2024.

##  1 Introduction

Deep neural networks (DNNs) [1, 2] encountered tremendous success in the
recent past due to their ability to infer highly nonlinear relations from
data, learn accurate predictive models, and make smart decisions with little
or no human intervention. Despite their success, the correctness of neural
networks remains a major concern due to their complexity and lack of
transparency. This is especially the case for safety- and security-critical
applications where errors and biases can have serious undesired consequences,
such as in medical diagnosis [3], self-driving cars [4], or financial systems
[5]. New techniques that can prove mathematical guarantees concerning the
behavior of neural networks are the need of the hour[6]. An effective approach
to address this issue is the use of automatic verification techniques, which
can either formally prove that the network adheres to a specified property or
return a concrete input (witness) demonstrating a violation of the
property[7].

_Robustness_ and _fairness_ are two important properties of neural networks.
Robustness refers to the neural network’s ability to make accurate predictions
even in the presence of input perturbations. In particular, a robust neural
network is able to produce accurate results without being overly sensitive to
small changes in the input. Fairness, on the other hand, refers to a neural
network’s ability to make unbiased and equitable predictions, particularly in
cases where the input data may contain sensitive attributes such as gender,
race, or age. A neural network that is not fair may produce biased results
that discriminate against certain groups, which can have serious ethical and
social implications.

##### Local robustness and fairness

provide the dominant perspective in verification and adversarial testing of
DNNs. Local robustness [8, 9, 10, 11] intuitively requires the DNN to have the
following property with respect to a given input $x$ – it has to make the same
prediction for the input $x$ as for all the points in the vicinity of $x$.
Local fairness [12, 13, 8] is defined in a similar way, with the distance
metric used for the inputs being the main difference. Both properties can be
formalized as safety properties. This has led to the design of a variety of
SMT-based techniques [14, 10, 15], which encode the neural networks and the
property to be verified as an SMT solving problem in order to enable automated
verification. Other works approach the verification problem using static
analysis [16, 17, 18, 19] which over-approximates DNN executions, thereby
compromising precision for higher scalability. Alternative verification
techniques include mixed-integer programming [20, 21, 22] and modified simplex
algorithms [9, 23].

Figure 1 (a) illustrates the properties of local robustness. It shows the
classification of an input $\vec{x}$ that includes two (continuous) features
$x_{1}$ and $x_{2}$. The pair of purple points is not a counterexample to
robustness, as both inputs lie within the same class. The green and blue
points, however, represent counterexamples to local robustness, as they fall
on different sides of the decision boundaries.

The above example shows two major limitations of local properties. First,
there are always inputs arbitrarily close to the decision boundary, which then
constitute counterexamples to local robustness. Second, local robustness is
defined only for a specific input. Consequently, it does not provide any
guarantees for any other input. It follows that the robustness of the entire
neural network cannot be assessed with local robustness only.

Figure 1: (a) Local, (b) partitioned-global and (c) our confidence-based
robustness. $x_{1}$ and $x_{2}$ denote continuous input points, while $x_{3}$
denotes a categorical input in the partitioned-global approach (b). The shades
of gray in (c) depict the level of confidence of the neural network with
respect to the given inputs – dark gray denotes high while white denotes low
confidence level. The neural network is robust to the pair of purple points in
all three cases (a), (b) and (c). The neural network is not robust for the
pair of blue points in the case of local and partitioned-global (b)
robustness, but is robust according to our definition (c). Finally, the neural
network is not robust for the pair of green points according to both the local
and our confidence-based global robustness (a) and (c), but is robust with
respect to the partitioned-global robustness (b). The global partitioning
method does not catch the counterexample, because the two green points are in
separate partitions.

##### Global robustness and fairness

The limitation of the local definition for robustness and fairness indicates
the need for a global property that evaluates the expected input/output
relation over _all pairs of inputs_.

We first observe that global robustness and fairness of DNNs are
_hyperproperties_ , i.e. properties that relate multiple executions of the
model. Khedr et al. [24] and Biswas et al. [25] recently introduced the first
verification techniques for hyperproperties in DNNs. These works assume that
the inputs contain categorical variables. Based on this strong assumption,
these two approaches partition the input space based on categorical features
to avoid comparing inputs close to decision boundaries, which would lead to a
non-satisfiable property. This is illustrated in Figure 1 (b). Here, we assume
that $\vec{x}$ includes a categorical feature $x_{3}$ in addition to the
continuous features $x_{1}$ and $x_{2}$. The left (right) part of Figure 1 (b)
depicts classes and inputs in the partition based on the categorical feature
$x_{3}$ with value $v$ ($v^{\prime}$). Consequently, only pairs of inputs
belonging to the _same_ partition are compared. Inputs belonging to two
different partitions (e.g. green points in Figure 1 (b)) deviate in at least
one categorical feature and can hence be assumed to violate the premise that
these inputs are “close”. According to this approach, a classification in a
secure network can only change with different categorical values. Any two
points that lie in the same partition but belong to different classes (e.g.
the pair of blue points in Figure 1 (b)) are considered counterexamples to the
global property. This leads to a strong limitation that does not admit two
classes to result from continuous inputs only, as typically required for
robustness. As a result, the two approaches [24, 25] address only verification
of global fairness.

##### Our contributions

Inspired by the work of Chen et al. [26] on properties of rule-based security
classifiers, we adopt a _confidence-based_ view on global robustness and
fairness for DNN. The idea is to compare all input pairs which are (1)
sufficiently close and (2) for which at least one of them yields a high
confidence classification. This intuitive definition expects robust and fair
DNNs to generate outputs with low confidence near the decision boundary.

We therefore propose _confidence-based 2-safety property_ , the first
definition that unifies global robustness and fairness for DNNs. Our
definition highlights the hyperproperty nature of global properties and uses
the confidence in the DNN as a first class citizen.

We briefly illustrate the intuition behind our confidence-based 2-safety
property definition with focus on robustness in Figure 1 (c), in which the
input space is colored into shades of gray and where every gray value
corresponds to a confidence of the network. Darker shades of gray represent
higher levels of confidence for the given classification. Our definition
captures two reasonable assumptions: (1) continuous inputs can also trigger
changes in classification, and (2) the confidence of the neural network at a
decision boundary must be relatively low. In essence, our definition requires
that for any input with high-confidence, all its $\epsilon$-neighbour inputs
yield the same class (e.g. the two purple points in Figure 1 (c)). This notion
discards inputs near the decision boundaries as counterexamples, as long as
they result in outputs with low confidence (e.g. the two blue points in Figure
1 (c)). Systems satisfying the 2-safety properties hence guarantee that input
points classified with a high confidence are immune to adversarial
perturbation attacks. In Figure 1 (c), the pair of green inputs witness the
violation of the confidence-based 2-safety property – the two points lie in
different classes and one of them has an output with high confidence.

This confidence-based view makes a conceptual change to the definition of
global properties, as it requires relating not only inputs, but also
confidence values to the outputs. This conceptual change poses a significant
challenge to the verification problem because checking a confidence-based
property on a DNN requires reasoning about its _softmax_ layer, which is not
supported by the state-of-the-art DNN verification tools [27, 28, 23, 29, 30,
31]. To solve this problem, we develop the first verification method that
supports DNNs with softmax, in which we use a linearized over-approximation of
the softmax function. We then combine it with self-composition [32] in order
to verify confidence-based 2-safety properties. We formally prove the
soundness of our analysis technique, characterizing, in particular, the error
bounds of our softmax over-approximation.

We demonstrate our approach 111
https://github.com/anaghaathavale/Global_2Safety_with_Confidence.gitin Marabou
[23], a state-of-the-art analysis tool for local robustness based on a
modified simplex algorithm, which we extend to support global robustness and
global fairness. We show that by combining our method with binary search, we
can go beyond verification and synthesize the minimum confidence for which the
DNN is globally robust or fair. We finally conduct a performance evaluation on
four neural networks trained with publicly available datasets to demonstrate
the effectiveness of our approach in identifying counterexamples and proving
global robustness and fairness properties.

##  2 Background

###  2.1 Feed-Forward Neural Networks

In feed-forward neural networks data flows uni-directionally, which means
there are no back edges. An input layer receives the inputs that move via one
or multiple hidden layers to the output layer [33]. A layer has multiple
neurons, each connected to the neurons in the next layer using a set of
weights. Each layer also has an associated bias. Weight and bias selection is
crucial to the performance of a neural network and is performed during the
training phase. Outputs are calculated by processing the inputs using weights
and biases, followed by applying the activation functions and then propagating
the processed inputs through the network[34].

Formally, a feed-forward neural network $f:\mathbb{R}^{m}\to\mathbb{R}^{n}$ is
modeled as a directed acyclic graph $G=(V,E)$ that consists of a set (finite)
of nodes $V$ and a set of edges $E\subseteq V\times V$.222We follow the
formalization of [35] and omit the biases for simplicity.The nodes $V$ are
partitioned into $l$ layers $V^{i}$ with $1\leq i\leq l$, where $V^{1}$ and
$V^{l}$ represent the input and output layers, and $V^{2},\ldots,V^{l-1}$
represent the hidden layers, respectively. We use $v_{i,j}$ to denote node $j$
in layer $i$. The edges $E$ connect nodes in $V^{i-1}$ with their successor
nodes in $V^{i}$ (for $1<i\leq l$).

Each node $v_{i,j}$ has an input and an output, where the latter is derived
from the former by means of an activation function. We use
$\operatorname{in}(v_{i,j})$ and $\operatorname{out}(v_{i,j})$ to denote the
input and output value of node $v_{i,j}$, respectively. The output is
determined by

$\operatorname{out}(v_{i,j})=a_{i,j}(\operatorname{in}(v_{i,j})))\,,$ (1)

where $a_{i,j}$ is the activation function. The input to node $v_{i,j}$ in
layer $V^{i}$ is determined by the outputs of its predecessors
$v_{i-1,1},\ldots,v_{i-1,k}$ in $V^{i-1}$ and weights associated with the
edges $(v_{i-1,k},v_{i,j})\in E$ for $1\leq k\leq|V^{i-1}|$:

$\operatorname{in}(v_{i,j})=\sum_{k=1}^{|V^{i-1}|}\operatorname{weight}((v_{i-1,k},v_{i,j}))\cdot\operatorname{out}(v_{i-1,k})$

The values of the nodes in the input layer $V^{1}$ are determined by the input
$\vec{x}$ to $f(\vec{x})$, i.e.,

$(\operatorname{in}(v_{1,1}),\ldots,\operatorname{in}(v_{1,m}))=\vec{x}\,.$

The output of the final layer $V^{l}$ is then computed by propagating the
inputs according to the activation functions (see Equation 1 above).
Consequently, a graph $G$ with $|V^{1}|=m$ input and $|V^{l}|=n$ output nodes
induces a function $f:\mathbb{R}^{m}\to\mathbb{R}^{n}$ whose semantics is
determined by the activation functions.

In this paper, we concentrate on the Rectified Linear Unit
($\operatorname{ReLU}$) activation function, which is frequently applied to
the hidden layers of deep neural networks. For a (scalar) input value $x$,
$\operatorname{ReLU}$ returns the maximum of 0 and $x$, i.e.

$\operatorname{ReLU}(x)=\max(0,x)\,.$

In neural networks that are used as classifiers and map an input $\vec{x}$ to
one of $m$ labels in a set of classes $C$, the final layer typically employs a
$\operatorname{softmax}$ function to ensure that the output represents
normalized probabilities corresponding to each of the $n$ classes.
Mathematically,

$\operatorname{softmax}(\vec{z})_{i}=\frac{e^{z\textsubscript{i}}}{\sum_{j=1}^{n}e^{z\textsubscript{j}}}$
(2)

where $\vec{z}$ represents the values $\operatorname{out}(v_{l-1,i})$ for
$1\leq i\leq n$ and $n=|V^{l-1}|$, and $z_{i}$ is the $i^{\text{th}}$ element
in $\vec{z}$. This induces a function $y:\mathbb{R}^{n}\to[0,1]^{n}$ mapping
every output of $V^{l-1}$ to a confidence score in the range $[0,1]$.
Consequently, $f(\vec{x})$ outputs a probability distribution over the
possible labels in $C$, where each component of the output vector represents
the probability of input $\vec{x}$ belonging to the corresponding class. We
use $\operatorname{conf}(f(\vec{x}))$ to refer to the highest probability
value in the $\operatorname{softmax}$ layer of $f(\vec{x})$ and call it the
confidence, i.e.,

$\operatorname{conf}(f(\vec{x}))=\max(\operatorname{out}(v_{l,1}),\ldots,\operatorname{out}(v_{l,n}))$
(3)

Finally, a function $\operatorname{class}:\mathbb{R}^{m}\to C$ then maps the
output of $f$ to the class $C$ corresponding to the highest probability in
$f(\vec{x})$:

$\operatorname{class}(f(\vec{x}))=\operatorname*{arg\,max}_{1\leq i\leq
n}(\operatorname{out}(v_{l,i}))$ (4)

###  2.2 Hyperproperties

Hyperproperties [36] are a class of properties that capture relationships
between multiple execution traces. This is in contrast to traditional
properties, which are evaluated over individual traces.

To define traces in the context of feed-forward neural networks, we extend our
notation $\operatorname{out}$ to layers as follows:

$\operatorname{out}(V^{i})=(\operatorname{out}(v_{i,1}),\ldots,\operatorname{out}(v_{i,k}))$

where $k=|V^{i}|$. Let $\operatorname{in}(V^{i})$ be defined similarly. The
corresponding trace $\pi$ for $f(\vec{x})$ is then formally defined as

$\pi=\operatorname{in}(V^{1}),\operatorname{out}(V^{1}),\ldots,\operatorname{in}(V^{l}),\operatorname{out}(V^{l})$

where $\operatorname{in}(V^{1})=\vec{x}$.

Note that each execution is entirely determined by the input value $\vec{x}$
(assuming that the function $f$ implemented by the network is deterministic).
Quantifying over traces $\pi$ of $f(\vec{x})$ hence corresponds to quantifying
over the corresponding inputs $\vec{x}$. A traditional safety property would
then quantify over the inputs $\vec{x}$, e.g.

$\forall\vec{x}\,.\,\operatorname{conf}(f(\vec{x}))\geq\kappa\,,$

stating that the confidence of each classification of the network should be
larger than a threshold $\kappa$. Another example of a traditional safety
property is local robustness, given in Definition 1 in subsection 2.4.

A hyperproperty, on the other hand, refers to, and quantifies over, more than
one trace. An example would be

$\forall\vec{x},\vec{x}^{\prime}\,.\,\frac{|f(\vec{x})_{i}-f(\vec{x}^{\prime})_{i}|}{||\vec{x}-\vec{x}^{\prime}||}\leq
K_{i}\,,1\leq i\leq n$ (5)

where $f(\vec{x})_{i}$ denotes $\operatorname{out}(v_{l,i})$. Equation 5
states that $K_{i}$ sets the maximum limit of the Lipschitz constant for
$f(\vec{x})_{i}$. A hyperproperty central to this paper is global robustness,
defined in Definition 2 subsection 2.4.

Hyperproperties are used to capture important properties that involve multiple
inputs, such as robustness and fairness. By verifying hyperproperties of
neural networks, we can ensure that they behave correctly across all possible
input traces.

###  2.3 Relational Verification and Self-Composition

Hyperproperties are verified by means of so-called relational verification
techniques: the idea is to verify if $k$ program executions satisfy a given
property [37], expressing invariants on inputs and outputs of such executions.
Several security properties (e.g., information flow) can be expressed by
relating two executions of the same program differing in the inputs: such
properties are called 2-safety properties. Global robustness in neural
networks can also be seen as a 2-safety property [8].

2-safety properties can be verified in a generic way by self-composition [37]:
the idea is to compose the program with itself and to relate the two
executions. In the context of neural networks, the self-composition of a
network $f$ is readily defined as a function over

$f(\vec{x})\times
f(\vec{x}^{\prime})=\lambda(\vec{x},\vec{x}^{\prime})\,.\,(f(\vec{x}),f(\vec{x}^{\prime}))$
(6)

where $(\vec{x},\vec{x}^{\prime})$ denotes the concatenation of the vectors
$\vec{x}$ and $\vec{x^{\prime}}$ and $\lambda\vec{x}\,.\,f(\vec{x})$ denotes
the lambda term that binds $\vec{x}$ in $f(\vec{x})$. The underlying graph
$G=(V,E)$ is simply duplicated, i.e., we obtain a graph $G\times
G^{\prime}=(V\cup V^{\prime},E\cup E^{\prime})$ where $V^{\prime}$ and
$E^{\prime}$ are primed copies of $V$ and $E$.

A counterexample to a universal 2-safety property over the self-composition of
$f$ comprises of a pair of traces of $f$ witnessing the property violation.

###  2.4 Robustness and Fairness

Robustness in neural networks refers to the ability of a model to perform
consistently in the presence of small perturbations of the input data. The
common approach to address robustness in neural networks is to define it as a
_local robustness_ [38] property. For an input $\vec{x}$, a neural network is
locally robust if it yields the same classification for $\vec{x}$ and all
inputs $\vec{x}^{\prime}$ within distance $\epsilon$ from $\vec{x}$ [39]:

######  Definition 1 (Local Robustness).

A model $f$ is locally $\epsilon$-robust at point $\vec{x}$ if

$\forall\vec{x}^{\prime}\,.\,||\vec{x}-\vec{x}^{\prime}||\leq\epsilon\to\operatorname{class}(f(\vec{x}))=\operatorname{class}(f(\vec{x}^{\prime}))$

Local robustness, therefore, is defined only for inputs within a distance
$\epsilon$ of a specific $\vec{x}$ and, thus, does not provide global
guarantees. Here $||\cdot||$ represents the distance metric used over the
input space. Intuitively, global robustness tackles this problem by requiring
that the local robustness property must hold for every input within the input
space [8]. Definition 2 gives the general definition of global robustness used
in [40, 26]. It essentially states that all input points in a small
neighborhood $\epsilon$, are mapped to the same class.

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

A model $f$ is globally $\epsilon$-robust if

$\forall\vec{x},\vec{x}^{\prime}\,.\,||\vec{x}-\vec{x}^{\prime}||\leq\epsilon\to\operatorname{class}(f(\vec{x}))=\operatorname{class}(f(\vec{x}^{\prime}))\,$

Clearly, global robustness as formalized in Definition 2 makes sense only for
selected distance metrics, which in particular avoid comparing inputs close to
the decision borders. For instance, [40] addresses this by introducing an
additional class $\bot$ to which $\operatorname{class}(f(\vec{x}))$ evaluates
whenever the difference between the highest and second-highest probability
falls below a certain threshold (determined by the Lipschitz constants of
$f$). The global robustness requirement is then relaxed at these points.

######  Definition 3 (Global fairness).

A model is said to be globally fair if:

$\forall\vec{x}=(x_{s},\vec{x_{n}}),\vec{x^{\prime}}=(x_{s}^{\prime},\vec{x_{n}^{\prime}}).\,\\\
||\vec{x_{n}}–\vec{x’_{n}}||\leq\epsilon\;\wedge(x_{s}\neq
x_{s}^{\prime})\to\operatorname{class}(f(\vec{x}))=\operatorname{class}(f(\vec{x}^{\prime}))$

where $x_{s}$ and $x_{n}$ are the sensitive and non-sensitive attributes of
$\vec{x}$, respectively.

[24, 25] address a similar problem, which arises in the context of fairness,
by partitioning the input space based on categorical features. In general, if
the input to a decision-making neural network comprises of certain sensitive
attributes, say age or gender, the network is said to be fair if the sensitive
attributes do not influence its decisions [8]. Definition 3 gives the general
definition of global fairness used in [24, 25].

Ensuring fairness in neural networks is important because these models are
increasingly being used in decision-making processes that can have significant
impacts on peoples’ lives. For example, a hiring algorithm that discriminates
against certain groups of job applicants based on their race or gender could
perpetuate existing biases and inequalities in the workplace [41].

##  3 Confidence Based Global Verification of Feed-Forward Neural Networks

We now formalize confidence-based 2-safety property, the first definition that
unifies global robustness and fairness for DNNs in Definition 4. It is a
hyperproperty that takes the confidence of the decision into account when
checking for the safety of the network. Before we give the actual definition,
we introduce additional notation. Given an input
$\vec{x}=(x_{1},\ldots,x_{n})$, we assume that its every component $x_{i}$ is
either a _categorical_ or _real_ value. We then define the distance
$d(x_{i},x^{\prime}_{i})$ as $|x_{i}-x^{\prime}_{i}|$ when $x_{i}$ is real-
valued. We use instead the following distance:

$d(x_{i},x^{\prime}_{i})=\begin{cases}0,&\text{if}\ x_{i}=x^{\prime}_{i}\\\
1,&\text{otherwise}\end{cases}$

when $x_{i}$ is a categorical value. We define
$\emph{cond}(\vec{x},\vec{x}^{\prime},\vec{\epsilon})$ as a (generic) Boolean
_condition_ that relates inputs $\vec{x}$ and $\vec{x}^{\prime}$ to a
tolerance vector $\vec{\epsilon}$.

######  Definition 4 (Confidence-based global 2-safety).

A model $f$ is said to be globally 2-safe for confidence $\kappa>0$ and
tolerance $\vec{\epsilon}$ iff

$\displaystyle\forall\vec{x},\vec{x}^{\prime}\,.\,\operatorname{cond}(\vec{x},\vec{x}^{\prime},\vec{\epsilon})$
$\displaystyle\wedge\operatorname{conf}(f(\vec{x}))>\kappa$
$\displaystyle\implies\operatorname{class}(f(\vec{x}))=\operatorname{class}(f(\vec{x}^{\prime}))$

Next, we instantiate the above 2-safety property for confidence-based global
robustness and fairness.

For _confidence-based global robustness_ , $\operatorname{cond}$ is defined
as:

$\operatorname{cond}(\vec{x},\vec{x}^{\prime},\vec{\epsilon})=\bigwedge_{i\in[1,n]}d(x_{i},x’_{i})\leq\epsilon_{i}$

For _confidence-based global fairness_ , $\vec{x}$ can be split into sensitive
$\vec{x_{s}}$ and non-sensitive $\vec{x_{n}}$ attributes. For confidence-based
global fairness,

$\displaystyle\operatorname{cond}(\vec{x},\vec{x}^{\prime},\vec{\epsilon})=\bigwedge_{x_{i}\in\vec{x_{s}}}d(x_{i},x’_{i})>0\;\wedge\bigwedge_{x_{i}\in\vec{x_{n}}}d(x_{i},x^{\prime}_{i})\leq\epsilon_{i}$

where for any categorical $x_{i}\in\vec{x_{n}}$, its associated tolerance
threshold $\epsilon_{i}=0.5$.

Intuitively, confidence-based global fairness ensures that for any data
instance, $x$ classified with high confidence $\kappa$, no other data
instance, $x^{\prime}$, that only differs with $x$ in the value of the
sensitive attribute (e.g. age, gender, ethnicity) shall be classified to a
different class.

As defined in Section 2, $f(x)$ represents the feed-forward neural network,
which maps inputs to classes with corresponding confidence scores. By
introducing the threshold $\kappa$, our definition effectively ignores
classification mismatches that arise from decisions with low confidence. The
rationale is as follows:

  * •

Different classifications close to decision boundaries need to be allowed, as
safety can otherwise only be satisfied by degenerate neural networks that map
all inputs to a single label.

  * •

On the other hand, input points classified with a high confidence should be
immune to adversarial perturbations and also uphold fairness.

###  3.1 Encoding 2-Safety Properties as Product Neural Network

In this section, we reduce checking of the 2-safety hyperproperty in
Definition 4 to a safety property over a single trace. Given a neural network
$f$ (as defined earlier in section 2), the product neural network is formed by
composing a copy of the original neural network with itself. Checking 2-safety
then reduces to checking an ordinary safety property for the self-composed
neural network that consists of two copies of the original neural network,
each with its own copy of the variables.

The product neural network is now treated as the model to be verified. A
product network allows the reduction of a hyperproperty to a trace property,
thereby reducing the problem of hyperproperty verification to a standard
verification problem, which can be solved using an existing standard
verification technique.

$\mathsf{Equation}$ | ::= |  $\mathsf{Sum}\,\Diamond\,\mathsf{Constant}$ with $\Diamond\in\\{\leq,\geq,=\\}$
---|---|---
|  | and $\mathsf{Sum}::=\mathsf{Sum}+\mathsf{Constant}\cdot\mathsf{Variable}~{}|~{}\mathsf{Constant}\cdot\mathsf{Variable}$
$\mathsf{MaxConstraint}$ | ::= | $\mathsf{Variable}=\max(\mathsf{VariableList})$
|  | and $\mathsf{VariableList}::=\mathsf{VariableList},\mathsf{Variable}~{}|~{}\mathsf{Variable}$
$\mathsf{AbsConstraint}$ | ::= | $\mathsf{Variable}=|\mathsf{Variable}|$
$\mathsf{ReLUConstraint}$ | ::= | $\mathsf{Variable}=\operatorname{ReLU}(\mathsf{Variable})$
$\mathsf{Disjunction}$ | ::= | $(\mathsf{Disjunction}\vee\mathsf{Equation})~{}|~{}\mathsf{Equation}$
Table 1: Marabou’s piecewise linear constraints

##### Product Neural Network

We encode $f(\vec{x})$ using piecewise linear constraints (see Table 1). Each
node $v_{i,j}$ is represented by two variables $\mathsf{in}_{i,j}$ and
$\mathsf{out}_{i,j}$ representing its input and output, respectively. Inputs
and outputs are related by the following constraints:

$\mathsf{in}_{i,j}=\sum_{k=1}^{|V^{i-1}|}w_{i,j}^{i-1,k}\cdot\mathsf{out}_{(i-1,)k}\quad\wedge\quad\mathsf{out}_{i,j}=a_{i,j}(\mathsf{in}_{i,j})$

where $w_{i,j}^{i-1,k}$ is the weight associated with the edge
$(v_{i-1,k},v_{i,j})$ and $a_{i,j}$ is the activation function of node
$v_{i,j}$. To encode the self-composition, we duplicate all variables and
constraints by introducing primed counterparts $\mathsf{in}^{\prime}_{i,j}$
and $\mathsf{out}^{\prime}_{i,j}$ for $\mathsf{in}_{i,j}$ and
$\mathsf{out}_{i,j}$.

##### Transfer Functions and Operators

$\operatorname{ReLU}$s can be readily encoded using
$\mathsf{out}_{i,j}=\operatorname{ReLU}(\mathsf{in}_{i,j})$. There is,
however, no direct way to encode $\operatorname{softmax}$ using the
constraints in Table 1, hence we defer the discussion to subsection 3.2.

The $\operatorname{conf}$ operator can be implemented using the $\max$
constraint (cf. Equation 3). The operator $\operatorname{class}$ as well as
the implication, on the other hand, are not necessarily supported by state-of-
the-art static analysis tools for DNNs. For instance, they are not supported
by Marabou [23], on which we base our implementation. For reference, Table 1
illustrates the linear constraints supported by Marabou. We thus introduce an
encoding, which we detail below.

First, checking the validity of the implication in Definition 4 can be reduced
to checking the unsatisfiability of

$\operatorname{cond}(\vec{x},\vec{x^{\prime}},\vec{\epsilon})\wedge\operatorname{conf}(f(\vec{x}))>\kappa\wedge\operatorname{class}(f(\vec{x}))\neq\operatorname{class}(f(\vec{x}^{\prime}))$
(7)

However, the grammar in Table 1 provides no means to encode disequality or
$\operatorname{class}$ (which returns the index of the largest element of a
vector). To implement disequality, we perform a case split over all
$n=|V^{l}|$ labels by instantiating the encoding of the entire network over
$\mathsf{out}_{l,i}$ and $\mathsf{out}^{\prime}_{l,i}$ for $1\leq i\leq n$. To
implement this in Marabou, we execute a separate query for every case.

To handle the operator $\operatorname{class}$, we can encode the disequality
$\operatorname{class}(f(\vec{x}))\neq\operatorname{class}(f(\vec{x}^{\prime})$
as:

$\ldots\;\wedge\;\overbrace{\max(\mathsf{out}_{l,1},\ldots,\mathsf{out}_{l,n})}^{\operatorname{conf}(f(\vec{x}))}>\kappa\;\wedge\left(\max(\mathsf{out}_{l,1},\ldots,\mathsf{out}_{l,n})-\mathsf{out}_{l,i}=0\right)\;\wedge\\\
\left(\max(\mathsf{out^{\prime}}_{l,1},\ldots,\mathsf{out^{\prime}}_{l,n})-\mathsf{out^{\prime}}_{l,i}\neq
0\right)\;$ (8)

The constraint
$(\max(\mathsf{out}_{l,1},\ldots,\mathsf{out}_{l,n})-\mathsf{out}_{l,i}=0)$
ensures that $\operatorname{out}_{l,i}$ corresponds to the largest element in
$f(\vec{x})$ (and hence that $\operatorname{class}(f(\vec{x})=i$).
Consequently, if
$(\max(\mathsf{out^{\prime}}_{l,1},\ldots,\mathsf{out^{\prime}}_{l,n})-\mathsf{out^{\prime}}_{l,i}\neq
0)$, then we can conclude that $\operatorname{class}(f(\vec{x}^{\prime}))\neq
i$ and hence the safety constraint is violated.

Since, Marabou does not support the disequality operator, we check whether
$(\max(\mathsf{out^{\prime}}_{l,1},\ldots,\mathsf{out^{\prime}}_{l,n})-\mathsf{out^{\prime}}_{l,i}<0)$
and
$(\max(\mathsf{out^{\prime}}_{l,1},\ldots,\mathsf{out^{\prime}}_{l,n})-\mathsf{out^{\prime}}_{l,i}>0)$,
and if both constraints are not satisfied, we know that
$(\max(\mathsf{out^{\prime}}_{l,1},\ldots,\mathsf{out^{\prime}}_{l,n})-\mathsf{out^{\prime}}_{l,i}\neq
0)$.

While the above transformation is equivalence preserving, the encoding of
$\operatorname{softmax}$ requires an approximation, described in the following
subsection.

###  3.2 Softmax Approximation

####  3.2.1 Softmax in terms of $\max$ and $\operatorname{Sig}$

We can approximate softmax using a $\max$ operator and a sigmoid function as
follows. Consider ${\operatorname{softmax}(\vec{z})\textsubscript{i}}$ (cf.
Equation 2), for i=1,

$\displaystyle{\operatorname{softmax}(\vec{z})\textsubscript{1}}$
$\displaystyle=\frac{1}{1+(e^{z{\textsubscript{\tiny
2}}}+\dotsb+e^{z{\textsubscript{\tiny n}}})e^{-z{\textsubscript{\tiny 1}}}}$
(9) $\displaystyle=\frac{1}{1+e^{log(e^{z{\textsubscript{\tiny
2}}}+\dotsb+e^{z{\textsubscript{\tiny n}}})}e^{-z{\textsubscript{\tiny
1}}}}=\frac{1}{1+e^{(-z{\textsubscript{\tiny 1}}+log(e^{z{\textsubscript{\tiny
2}}}+\dotsb+e^{z{\textsubscript{\tiny n}}}))}}$ (10)

We can now generalize the result from (9) for i

$\displaystyle\operatorname{softmax}(\vec{z})\textsubscript{i}=\frac{1}{1+e^{(-z{\textsubscript{\tiny
i}}+log(\sum_{j\neq i}^{n}e^{z{\textsubscript{\tiny
j}}}))}}=\operatorname{Sig}(z{\textsubscript{\tiny
i}}-\mathop{\operatorname*{LSE}_{1}^{n}}_{j\neq i}(z_{j}))$ (11)

where LSE (the _log-sum-exp_) is:

$\mathop{\operatorname*{LSE}_{1}^{n}}_{j\neq i}(z_{j})=log(\sum_{j=1,j\neq
i}^{n}e^{z}\textsubscript{\tiny{j}})\mbox{ and
}\operatorname{Sig}(x)=\frac{1}{1+e^{-x}}$

We know from [42] that LSE is bounded:

$\begin{split}\mathop{max_{1}^{n}}(z_{i})\leq\mathop{\operatorname*{LSE}_{1}^{n}}(z_{i})\leq\mathop{max_{1}^{n}}(z_{i})+log(n)\end{split}$
(12)

with $\mathop{max_{1}^{n}}(z_{i})=max(z_{1},\cdots,z_{n})$, in particlular,
when $z_{1}=\cdots=z_{n}$, we have:

$\begin{split}\mathop{\operatorname*{LSE}_{1}^{n}}(z_{i})=\mathop{max_{1}^{n}}(z_{i})+log(n)\end{split}$
(13)

Then softmax has as lower bound:

$\begin{split}\operatorname{softmax}(\vec{z})\textsubscript{i}\geq\operatorname{Sig}(z{\textsubscript{\tiny
i}}-\mathop{max_{1}^{n}}_{j\neq i}(z_{j})+log(n-1))\end{split}$ (14)

and as upper bound:

$\begin{split}\operatorname{softmax}(\vec{z})\textsubscript{i}\leq\operatorname{Sig}(z{\textsubscript{\tiny
i}}-\mathop{max_{1}^{n}}_{j\neq i}(z_{j}))\end{split}$ (15)

When $n=2$, the softmax is equivalent to the sigmoid:

$\displaystyle\operatorname{softmax}(\vec{z})\textsubscript{1}=\operatorname{Sig}(z{\textsubscript{\tiny
1}}-z_{2})\mbox{ and
}\operatorname{softmax}(\vec{z})\textsubscript{2}=\operatorname{Sig}(z{\textsubscript{\tiny
2}}-z_{1})$ (16)

Now that we know how to approximate a softmax using a sigmoid and max, we need
to find a piece-wise linear approximation of sigmoid since sigmoid is also a
non-linear exponential function.

####  3.2.2 Piece-wise approximation of sigmoid

We approximate sigmoid as a piece-wise linear function using the Remez
exchange algorithm[43]. The Remez algorithm is an iterative algorithm that
finds simpler approximations to functions. It aims to minimize the maximum
absolute difference between the approximated polynomial and the actual
function. The algorithm takes a maximum acceptable error $\delta$ and
generates $l$ linear segments to approximate the sigmoid function such that
the error is less than $\delta$. We use the Remez algorithm to approximate the
sigmoid in the interval
$[\operatorname{Sig}^{-1}(\delta),\operatorname{Sig}^{-1}(1-\delta)]$, where
$\operatorname{Sig}^{-1}$ is the inverse function of the sigmoid. The inverse
of sigmoid is the logit function i.e.,
$\operatorname{Sig}^{-1}(y)=logit(y)=log(y)/(1-y)$. For example, if the user
sets $\delta$ to 0.0006, then the input domain for the algorithm lies in
$[-7.423034723582278,7.423034723582278]$. Thus, the approximated sigmoid is:

$|\operatorname{\widehat{Sig}}(x)-\operatorname{Sig}(x)|\leq\delta$

We approximate $\operatorname{softmax}$ with its lower bound:

$\begin{split}\widehat{\operatorname{softmax}}(\vec{z})\textsubscript{i}=\operatorname{\widehat{Sig}}(z{\textsubscript{\tiny
i}}-\mathop{max_{1}^{n}}_{j\neq i}(z_{j})+log(n-1))-\delta\end{split}$ (17)

and the upper bound for the softmax is:

$\begin{split}\widehat{\operatorname{softmax}}(\vec{z})\textsubscript{i}\leq\operatorname{softmax}(\vec{z})\textsubscript{i}\leq\operatorname{\widehat{Sig}}(z{\textsubscript{\tiny
i}}-\mathop{max_{1}^{n}}_{j\neq i}(z_{j}))+\delta\end{split}$ (18)

######  Theorem 3.1.

Let $\operatorname{softmax}$ and $\widehat{\operatorname{softmax}}$ compute
the real and linearly approximated softmax (with precision $\delta$),
respectively for the last layer of $n\geq 2$ neurons $\vec{z}$ of a neural
network and $z_{i}=max(z_{1},\cdots,z_{n})$. Then, we have the following
result:

$\forall\vec{z}.\
\operatorname{softmax}(\vec{z})\textsubscript{i}-\widehat{\operatorname{softmax}}(\vec{z})\textsubscript{i}\leq\frac{n-2}{(\sqrt{n-1}+1)^{2}}+2\delta$

###### Proof.

Refer Appendix 0.A ∎

######  Theorem 3.2.

(Class consistency) Let $f$ and $\hat{f}$ denote the real and the approximated
(with precision $\delta$) neural networks with $n\geq 2$ outputs,
respectively. Then:

$\operatorname{conf}(\hat{f}(\vec{x}))>\frac{1}{2}\implies\operatorname{class}(\hat{f}(\vec{x}))=\operatorname{class}(f(\vec{x}))$

###### Proof.

Refer Appendix 0.A ∎

####  3.2.3 Soundness

For the confidence-based 2-safety property discussed before, our analysis
provides a soundness guarantee. This means that whenever the analysis reports
that the property specified in 4 holds, then the property also holds true in
the concrete execution.

######  Theorem 3.3.

(Soundness) Let $f$ and $\hat{f}$ be the original neural network and over-
approximated neural network, respectively. Let $b_{n,\delta}$ be the error
bound of the approximated softmax
($b_{n,\delta}=\frac{n-2}{(\sqrt{n-1}+1)^{2}}+2\delta$ (see Theorem 3.1)).
Then we have the following soundness guarantee: Whenever the approximated
neural network is 2-safe for $\operatorname{conf}(\hat{f}(\vec{x}))>(\kappa-
b_{n,\delta})$, the real neural network is 2-safe for
$\operatorname{conf}(f(\vec{x}))>\kappa$, given
$\operatorname{conf}(\hat{f}(\vec{x}))>\frac{1}{2}$. Formally:

$\left(\begin{split}\forall\vec{x},\vec{x^{\prime}}.\
\operatorname{cond}(\vec{x},\vec{x^{\prime}},\vec{\epsilon})\land{\operatorname{conf}}(\hat{f}(\vec{x}))>(\kappa-
b_{n,\delta})\\\
\implies{\operatorname{class}}(\hat{f}(\vec{x}))={\operatorname{class}}(\hat{f}(\vec{x^{\prime}}))\end{split}\right)\implies\\\
\left(\begin{split}\forall\vec{x},\vec{x^{\prime}}.\
\operatorname{cond}(\vec{x},\vec{x^{\prime}},\vec{\epsilon})\land\operatorname{conf}(\vec{f(x)})>\kappa\\\
\implies\operatorname{class}(f(\vec{x}))=\operatorname{class}(f(\vec{x^{\prime}}))\end{split}\right),\mbox{
with }\>\operatorname{conf}(\hat{f}(\vec{x}))>\frac{1}{2}$

###### Proof.

Refer Appendix 0.A ∎

##  4 Implementation

For the implementation of our technique, we use the state-of-the-art neural
network verification tool Marabou [23] as our solver. In this section, we
describe how we encode the confidence-based 2-safety property in Marabou. Note
that such an encoding can be expressed in a similar way for virtually any off-
the-shelf neural network verifier.

Marabou[23] Marabou is a simplex-based linear programming neural network
verification and analysis tool. Marabou is capable to address queries about
network’s properties, such as local robustness, by encoding them into
constraint satisfaction problems. It supports fully-connected feed-forward
neural networks. A network can be encoded as a set of linear constraints
representing the weighted sum of the neurons’ outputs feeding the next
neuron’s input, and a set of non-linear constraints defining the activation
functions. A verification query to Marabou comprises a neural network along
with a property that needs to be verified. This property is defined as ”linear
and nonlinear constraints on the network’s inputs and outputs”[23]. In
Marabou, network’s neurons are treated as variables. As a result, the
verification problem involves identifying a variable assignment that satisfies
all the constraints at the same time, or establishing that such an assignment
does not exist. The tool uses a variant of the _Simplex_ algorithm at its core
to make the variable assignment satisfy the linear constraints. During the
execution, the tool adjusts the variable assignment to either fix a linear or
a non-linear constraint violation. Although the technique implemented in
Marabou is sound and complete, the tool can work only with piece-wise linear
activation functions (including $\operatorname{ReLU}$ function and the $\max$
function) to guarantee termination. Additionally, an essential aspect of
Marabou’s verification approach is deduction – specifically, deriving more
precise lower and upper bounds for each variable. The tool leverages these
bounds to relax piece-wise linear constraints into linear ones by considering
one of its segments.

The original network g is a function of the following: input parameters,
neurons, neuron connection weights, layer biases, $\operatorname{ReLU}$
activation functions and output classes. To make Marabou amenable for
verification of 2-safety properties, we need a product neural network. This
means that the execution is tracked over two copies of the original network,
$g$ and $g^{\prime}$ (cf. subsection 2.3). Let $X_{i}$ denote the set of input
variables to $g$ and let $X^{\prime}_{i}$ be a set of primed copies of the
variables in $X_{i}$. As a result, we obtain a self-composition
$g(X_{i})\times g^{\prime}(X_{i}^{\prime})$ of $g$ over the input variables
$X_{i}\cup X_{i}^{\prime}$.

Next, we extend the output layer with softmax function in order to extract the
confidence scores with which output classes are predicted.

Linearized Sigmoid We explain our linearized sigmoid function in this
subsection. This function is used to implement an approximated piece-wise
linear sigmoid function. Let the outputs of the last inner layer $l-1$ be
represented by $z_{i}$ for $1\leq i\leq n$, where $n$ is the number of output
classes. In Marabou, we first encode the linear piece-wise sigmoid function
which we obtain by setting the maximum acceptable error to 0.005. This
provides us with a piece-wise linear approximated sigmoid with 35 segments of
the form $q_{j}=\\{m_{j}\cdot z_{i}+c_{j},\ |\ LB\leq z_{i}\leq UB\\}$, where
$z_{i}$ is the variable representing the output node whose confidence we want
to find. We encode each segment as an equation in and represent it using a
variable $q_{j}$. Next, we need to select the applicable segment corresponding
to the value of $z_{i}$. Unfortunately, Marabou does not provide a conditional
construct. So, we deploy the $\min$ and $\max$ functions to emulate if-then-
else.

First, we split the sigmoid into two convex pieces $S_{1}$ and $S_{2}$. Figure
2 illustrates this step using a simplified approximation of sigmoid with 4
linear segments $q_{1}$, $q_{2}$, $q_{3}$, and $q_{4}$. The resulting value of
$S_{1}$ can now be expressed as $S_{1}=\min(\max(0,q_{1},q_{2}),0.5)$.
Similarly, $S_{1}=\max(\min(0.5,q_{3},q_{4}),1)$. The values $0$ and $1$ are
the minimum and maximum values of the sigmoid function and $0.5$ is the value
of sigmoid at the splitting point. Second, we combine the convex segments by
adding them:

$S=\min(\max(0,q_{1},q_{2}),0.5)+\max(\min(0.5,q_{3},q_{4}),1)-0.5$

Note that we have 35 segments instead of four used in our simplified
explanation.

Linearized Softmax The next step consists in implementing the softmax function
using the output of the sigmoid function and the $\max$ function (see Equation
17). To this end, we find the maximum of all output nodes excluding the
current one, and subtract that maximum from the current output value. Finally,
we apply the linearized sigmoid (cf. section 4), to obtain the result of
softmax.

We repeat the above steps for all output nodes to obtain the softmax values
corresponding to all output classes. Finally, we find the maximum value of
these softmax outputs, which represents the confidence.

Figure 2: (Simplified) Approximation of sigmoid with 4 linear segments

##  5 Experimental Evaluation

For our evaluation, we used four publicly available benchmark datasets to
evaluate our technique. We pre-process the datasets to remove null entries,
select relevant categorical attributes, and hot-encode them. For each dataset,
we train a fully connected feed-forward neural network with up to 50 neurons
and ReLU activation functions.

German Credit: The German Credit Risk dataset [44] describes individuals
requesting credit from a bank and classified, based on their characteristics,
in two categories (”good” or ”bad”) of credit risk. The dataset comprises 1000
entries.

Adult: The Adult dataset, also referred to as the ”Census Income” dataset, is
used to estimate whether a person’s income surpasses $50,000 per year based on
census information [45].

COMPAS: COMPAS (”Correctional Offender Management Profiling for Alternative
Sanctions”) is a widely-used commercial algorithm that is utilized by judges
and parole officers to assess the probability of criminal defendants
committing future crimes, also known as recidivism [46].

Law School: The Law School Admissions Council (LSAC) provides a dataset called
Law School Admissions, which includes information on approximately 27,000 law
students from 1991 to 1997. The dataset tracks the students’ progress through
law school, graduation, and bar exams. It uses two types of academic scores
(LSAT and GPA) to predict their likelihood of passing the bar exam [47].

We use TensorFlow for training neural networks and the NN verifier Marabou
[23] whose implementation is publicly available. The accuracies for the
deployed models are as follows: German Credit: 0.71; COMPAS: 0.74; Law: 0.94;
Adult: 0.77. In our experiments, adding more layers or nodes per layer did not
result in an increased accuracy. We run all our experiments using a single AMD
EPYC 7713 64-Core Processor, Ubuntu 22.04 LTS Operating System with 32 GB RAM.

Figure 3: Input distance vs. confidence for German credit dataset

Figure 4: Input distance vs. confidence for adult dataset

Figure 5: Input distance vs. confidence for law school dataset

Figure 6: Input distance vs. confidence for COMPAS dataset

First, we present our confidence-based global robustness results. We evaluate
our implementation on the neural networks trained with the benchmark datasets
for various combinations of input distance and confidence values. We aim to
find proofs for globally robust neural networks. The plots in Fig. 4, 4, 6 and
6 show our experimental results as scatter plots. Markers denoting ’sat’
correspond to the query resulting in a counter-example. A counter-example here
means that for the input distance and confidence values in that query, the
inputs are classified into different output classes. The ’unsat’ markers stand
for the query being proved (i.e. the model is robust), which means that for
the corresponding input distance and confidence threshold, the inputs are
classified to the same output class and the model is globally robust. The
color bar on the right side denotes the time taken in seconds to run each
query; the time scale goes from deep purple to blue, green and yellow as the
time taken increases from 0 to 60 sec. The plot in 4 depicts the effect of
varying input distance and confidence on the German credit benchmark. We ran
our query with the confidence-based global robustness property for input
distance, $\epsilon$ and confidence $\kappa$ values ranging from 0.001 to 1.0
and 0.5 to 0.9, respectively. Observe that for $\kappa$ values below 0.7, the
model is sat i.e. we find counter-examples. However, for confidence values
above 0.75, even for larger input distances, the queries result in unsat and a
proof that the model is robust above a confidence threshold of 0.75.

The plots in Figures 4, 6 and 6 show the results for neural networks trained
with Adult, Law School, and COMPAS datasets. As can be observed from the
scatter plots, these models are robust. For confidence values above 0.5, they
are 2-safe and we are successfully able to prove this rather fast in 50
seconds or less.

Dataset | Sensitive attribute | Confidence threshold | Result | Time taken
---|---|---|---|---
German credit | Gender | 0.5 | unsat | 10.232 sec
German credit | Age | 0.5 | unsat | 11.478 sec
COMPAS | Gender | 0.5 | sat | 7.423 sec
COMPAS | Ethnicity | 0.5 | sat | 18.293 sec
COMPAS | Ethnicity | 0.99 | sat | 25.846 sec
COMPAS | Ethnicity | 0.999 | unsat | 171 min 15 sec
Table 2: Global fairness on German credit/COMPAS datasets for various criteria

Next, we present the results for confidence-based global fairness
verification, which are shown in Table 2. Each row in the table depicts the
verification result for a NN along with the sensitive attribute and confidence
threshold considered. If the result is ’unsat’, it means that the query is
proved (i.e. the model is fair). In other words, for the corresponding
sensitive attribute and confidence value constraints, the inputs are
classified to the same output class and the model is globally fair. On the
other hand, ’sat’ corresponds to the query resulting in a counter-example. A
counter-example here means that for the corresponding sensitive attribute and
confidence threshold in the query, the inputs are classified into different
output classes.

The German credit model is proved to be globally fair for confidence values
above 0.5 for sensitive attributes Gender and Age. Running our query with the
confidence-based global fairness property for the COMPAS model, with Gender as
the sensitive attribute gives counter-examples for all confidence values.
Additionally, when Ethnicity is considered as the sensitive attribute while
verifying the COMPAS model, we find counter-examples for lower confidence
values. However, the model is proved to be globally fair for confidence values
above 0.999.

We combined our method with binary search, to synthesize the minimum
confidence for which the DNN is globally robust or fair. We perform the binary
search, starting with confidence 0.5. If the model is unsat, we are done.
Else, we check for confidence mid = (0.5 + 1)/2, and continue in this way till
we find the minimum confidence accurate to the nearest 0.05. For instance,
binary search combined with our method, on German credit gave us 0.75 (in 45
seconds) to be the minimum confidence for which the DNN is globally robust.

Our experimental results on 2-safety properties (with regard to both, global
robustness and global fairness), clearly point out that taking confidence
along with input distance into account is crucial when verifying neural
networks.

###  5.1 Discussion

####  5.1.1 Soundness

Our proof of soundness guarantees that if our approach yields that a model is
robust or fair for a given confidence and input distance, the model is indeed
safe. In case of the German Credit model, for instance, the model is indeed
globally robust for all input distances when the confidence is at least 0.75.
Moreover, we can use binary search to find the minimal confidence value above
which a model is robust. Our approach guarantees soundness and when a model is
found to be safe, it is indeed safe. However, if a counterexample is found, it
may be a false positive. False positives (or spurious counterexamples) may in
general stem either from overapproximations of the underlying reachability
analysis tool or from our own softmax approximation. In our implementation,
the former are not present since Marabou is complete (i.e., it does not have
false positives), whereas our softmax approximation yields a confidence error
that depends on the number of DNN-outputs, as formalized in Theorem 3.1 and
quantified in its proof in Appendix 0.A. For DNNs with two outputs, such as
German Credit, Adult, and Law School, there is no error, whereas for three
outputs (COMPAS) the error is $\sim$ 0.171. Hence, if we want to certify a
three-output DNN for confidence $x$, we run our analysis for confidence
$x-0.171$: if no attack is found, we can certify the network for confidence
$x$ (soundness), otherwise we know the counterexample violates the 2-safety
property (completeness of Marabou) for confidence in between $x$ and $x-0.171$
(the possible imprecision is due to our softmax overapproximation). We report
counterexamples in this paper on German Credit and on COMPAS: the former are
true positives (2-output DNN), whereas the latter are counterexamples for
confidence in between $0.999$ (the confidence we can certify the network for)
and $0.828$. We ran the network on the counterexample reported by Marabou and
found the real confidence to be $0.969$. Hence, the network is for sure fair
for a confidence higher than $0.999$, unfair for confidence levels lower than
$0.969$, while we cannot decide it for the confidence levels in the interval
between $0.969$ and $0.999$. This means that on our datasets, our analysis is
very accurate.

####  5.1.2 Threats to Validity

Presuming a high level of confidence as a precondition can make low-confidence
networks vacuously safe. However, an accurate but low-confidence network is
not desirable in the first place. This concept is known in the literature as
miscalibration. The Expected Calibration Error is defined as weighted average
over the absolute difference between confidence and accuracy. In scenarios
where accurate confidence measures are crucial, the goal is to reduce the
Maximum Calibration Error [48] that is the maximum discrepancy between
confidence and accuracy.

This is orthogonal to our work and there is an entire field of research [49,
50] aiming at minimizing such calibration errors.

##  6 Conclusion

We introduce the first automated method to verify 2-safety properties such as
global robustness and global fairness in DNNs based on the confidence level.
To handle the nonlinear $\operatorname{softmax}$ function computing the
confidence, we approximate it with a piece-wise linear function for which we
can bound the approximation error. We then compute the self-composition of the
DNN with the approximated $\operatorname{softmax}$ and we show how to leverage
existing tools such as Marabou to verify 2-safety properties. We prove that
our analysis on the approximated network is sound with respect to the original
one when the value of confidence is greater than $0.5$ in the approximated
one. We successfully evaluate our approach on four different DNNs, proving
global robustness and global fairness in some cases while finding
counterexamples in others.

While we improve over recent verifiers for global properties that are limited
to binary classifiers [25], a limitation of our current approach is that we
can only handle DNNs with few (two to five) outputs, since the approximation
error increases with the number of outputs. We plan to overcome this
limitation in future work by devising more accurate abstractions of
$\operatorname{softmax}$.

To improve scalability, we will investigate how to refine our approach by
integrating pruning strategies, such as those developed in [25], which we
intend to refine to fit our static analysis framework.

We also plan to explore more sophisticated and effective verification
techniques for 2-safety properties, possibly tailored to specific DNN
structures.

Finally, we plan to complement our verification approach with testing
techniques to further explore the generated counterexamples.

##  7 Acknowledgements

The work published in this paper is a part of the AI4CSM project that has
received funding within the ECSEL JU in collaboration with the European
Union’s H2020 Framework Programme (H2020/2014-2020) and National Authorities,
under grant agreement No.101007326. This work was also partially supported by
the WWTF project ICT22-023, by the WWTF project 10.47379/ICT19018, by the
European Research Council (ERC) under the European Union’s Horizon 2020
research (grant agreement 771527-BROWSEC), by the Austrian Science Fund (FWF)
10.55776/F85 (project F8510-N); the Vienna Science and Technology Fund (WWTF)
through [ForSmart Grant ID: 10.47379/ICT22007]; the Austrian Research
Promotion Agency (FFG) through the COMET K1 SBA.

## References

  * [1] K. Gurney, An introduction to neural networks.  CRC press, 1997.
  * [2] I. J. Goodfellow, Y. Bengio, and A. C. Courville, Deep Learning.  Adaptive computation and machine learning, MIT Press, 2016.
  * [3] F. Amato, A. López, E. M. Peña-Méndez, P. Vaňhara, A. Hampl, and J. Havel, “Artificial neural networks in medical diagnosis,” 2013.
  * [4] Q. Rao and J. Frtunikj, “Deep learning for self-driving cars: Chances and challenges,” in Proceedings of the 1st international workshop on software engineering for AI in autonomous systems, pp. 35–38, 2018.
  * [5] J. Duan, “Financial system modeling using deep neural networks (dnns) for effective risk assessment and prediction,” Journal of the Franklin Institute, vol. 356, no. 8, pp. 4716–4731, 2019.
  * [6] H. Tran, W. Xiang, and T. T. Johnson, “Verification approaches for learning-enabled autonomous cyber-physical systems,” IEEE Des. Test, vol. 39, no. 1, pp. 24–34, 2022.
  * [7] P. Bjesse, “What is formal verification?,” ACM SIGDA Newsletter, vol. 35, no. 24, pp. 1–es, 2005.
  * [8] S. A. Seshia, A. Desai, T. Dreossi, D. J. Fremont, S. Ghosh, E. Kim, S. Shivakumar, M. Vazquez-Chanlatte, and X. Yue, “Formal specification for deep neural networks,” in Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings 16, pp. 20–34, Springer, 2018.
  * [9] G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient smt solver for verifying deep neural networks,” in Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30, pp. 97–117, Springer, 2017.
  * [10] X. Huang, M. Kwiatkowska, S. Wang, and M. Wu, “Safety verification of deep neural networks,” in Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30, pp. 3–29, Springer, 2017.
  * [11] D. Gopinath, G. Katz, C. S. Păsăreanu, and C. Barrett, “Deepsafe: A data-driven approach for assessing robustness of neural networks,” in Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings 16, pp. 3–19, Springer, 2018.
  * [12] C. Urban, M. Christakis, V. Wüstholz, and F. Zhang, “Perfectly parallel fairness certification of neural networks,” Proceedings of the ACM on Programming Languages, vol. 4, no. OOPSLA, pp. 1–30, 2020.
  * [13] X. Xie, F. Zhang, X. Hu, and L. Ma, “Deepgemini: Verifying dependency fairness for deep neural network,” in Proceedings of the AAAI Conference on Artificial Intelligence, vol. 37, pp. 15251–15259, 2023.
  * [14] L. Pulina and A. Tacchella, “Challenging smt solvers to verify neural networks,” Ai Communications, vol. 25, no. 2, pp. 117–135, 2012.
  * [15] J. Li, J. Liu, P. Yang, L. Chen, X. Huang, and L. Zhang, “Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification,” in Static Analysis: 26th International Symposium, SAS 2019, Porto, Portugal, October 8–11, 2019, Proceedings 26, pp. 296–319, Springer, 2019.
  * [16] L. Pulina and A. Tacchella, “An abstraction-refinement approach to verification of artificial neural networks,” in Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings 22, pp. 243–257, Springer, 2010.
  * [17] G. Singh, T. Gehr, M. Püschel, and M. Vechev, “An abstract domain for certifying neural networks,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, pp. 1–30, 2019.
  * [18] T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, “Ai2: Safety and robustness certification of neural networks with abstract interpretation,” in 2018 IEEE symposium on security and privacy (SP), pp. 3–18, IEEE, 2018.
  * [19] A. Baninajjar, K. Hosseini, A. Rezine, and A. Aminifar, “Safedeep: A scalable robustness verification framework for deep neural networks,” in ICASSP 2023 - 2023 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), pp. 1–5, 2023.
  * [20] C.-H. Cheng, G. Nührenberg, and H. Ruess, “Maximum resilience of artificial neural networks,” in Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings 15, pp. 251–268, Springer, 2017.
  * [21] V. Tjeng, K. Xiao, and R. Tedrake, “Evaluating robustness of neural networks with mixed integer programming,” arXiv preprint arXiv:1711.07356, 2017\.
  * [22] S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari, “Output range analysis for deep feedforward neural networks,” in NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings 10, pp. 121–138, Springer, 2018.
  * [23] G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljić, et al., “The marabou framework for verification and analysis of deep neural networks,” in Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31, pp. 443–452, Springer, 2019.
  * [24] H. Khedr and Y. Shoukry, “Certifair: A framework for certified global fairness of neural networks,” arXiv preprint arXiv:2205.09927, 2022.
  * [25] S. Biswas and H. Rajan, “Fairify: Fairness verification of neural networks,” in 45th IEEE/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023, pp. 1546–1558, IEEE, 2023\.
  * [26] Y. Chen, S. Wang, Y. Qin, X. Liao, S. Jana, and D. Wagner, “icse security classifiers with verified global robustness properties,” in Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, pp. 477–494, 2021.
  * [27] S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter, “Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification,” Advances in Neural Information Processing Systems, vol. 34, pp. 29909–29921, 2021.
  * [28] K. Xu, H. Zhang, S. Wang, Y. Wang, S. Jana, X. Lin, and C.-J. Hsieh, “Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers,” arXiv preprint arXiv:2011.13824, 2020.
  * [29] H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,” Advances in neural information processing systems, vol. 31, 2018.
  * [30] C. Ferrari, M. N. Muller, N. Jovanovic, and M. Vechev, “Complete verification via multi-neuron relaxation guided branch-and-bound,” arXiv preprint arXiv:2205.00263, 2022.
  * [31] S. Bak, H.-D. Tran, K. Hobbs, and T. T. Johnson, “Improved geometric path enumeration for verifying relu neural networks,” in Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I 32, pp. 66–96, Springer, 2020.
  * [32] G. Barthe, P. R. D’Argenio, and T. Rezk, “Secure information flow by self-composition,” Math. Struct. Comput. Sci., vol. 21, no. 6, pp. 1207–1252, 2011.
  * [33] G.-B. Huang, “Learning capability and storage capacity of two-hidden-layer feedforward networks,” IEEE transactions on neural networks, vol. 14, no. 2, pp. 274–281, 2003.
  * [34] S. Sharma, S. Sharma, and A. Athaiya, “Activation functions in neural networks,” Towards Data Sci, vol. 6, no. 12, pp. 310–316, 2017.
  * [35] A. Albarghouthi et al., “Introduction to neural network verification,” Foundations and Trends® in Programming Languages, vol. 7, no. 1–2, pp. 1–157, 2021.
  * [36] M. R. Clarkson and F. B. Schneider, “Hyperproperties,” Journal of Computer Security, vol. 18, no. 6, pp. 1157–1210, 2010.
  * [37] G. Barthe, J. M. Crespo, and C. Kunz, “Relational verification using product programs,” in FM 2011: Formal Methods: 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings 17, pp. 200–214, Springer, 2011.
  * [38] O. Bastani, Y. Ioannou, L. Lampropoulos, D. Vytiniotis, A. Nori, and A. Criminisi, “Measuring neural net robustness with constraints,” Advances in neural information processing systems, vol. 29, 2016.
  * [39] R. Mangal, A. V. Nori, and A. Orso, “Robustness of neural networks: A probabilistic and practical approach,” in 2019 IEEE/ACM 41st International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), pp. 93–96, IEEE, 2019.
  * [40] K. Leino, Z. Wang, and M. Fredrikson, “Globally-robust neural networks,” in International Conference on Machine Learning, pp. 6212–6222, PMLR, 2021\.
  * [41] R. Binns, “Fairness in machine learning: Lessons from political philosophy,” in Conference on fairness, accountability and transparency, pp. 149–159, PMLR, 2018.
  * [42] Y. V. Pant, H. Abbas, and R. Mangharam, “Smooth operator: Control using the smooth robustness of temporal logic,” in 2017 IEEE Conference on Control Technology and Applications (CCTA), pp. 1235–1240, IEEE, 2017.
  * [43] E. Y. Remez, “Sur la détermination des polynômes d’approximation de degré donnée,” 1934.
  * [44] H. Hofmann, “German credit dataset,” UCI Machine 2023 Repository [http://archive. ics. uci. edu/ml]. University of California, School of Information and Computer Science, Irvine, 1994.
  * [45] D. Dua and C. Graff, “UCI machine 2023 repository,” 2017.
  * [46] J. Larson. https://github.com/propublica/compas-analysis, 2017.
  * [47] L. F. Wightman, “Lsac national longitudinal bar passage study. lsac research report series.,” 1998.
  * [48] M. P. Naeini, G. Cooper, and M. Hauskrecht, “Obtaining well calibrated probabilities using bayesian binning,” in Proceedings of the AAAI conference on artificial intelligence, vol. 29, 2015.
  * [49] C. Guo, G. Pleiss, Y. Sun, and K. Q. Weinberger, “On calibration of modern neural networks,” in International conference on machine learning, pp. 1321–1330, PMLR, 2017.
  * [50] S. Ao, S. Rueger, and A. Siddharthan, “Two sides of miscalibration: identifying over and under-confidence prediction for network calibration,” in Uncertainty in Artificial Intelligence, pp. 77–87, PMLR, 2023.

##  Appendix 0.A Appendix

######  Theorem 1.

Let $\operatorname{softmax}$ and $\widehat{\operatorname{softmax}}$ compute
the real and linearly approximated softmax (with precision $\delta$),
respectively for the last layer of $n\geq 2$ neurons $\vec{z}$ of a neural
network and $z_{i}=max(z_{1},\cdots,z_{n})$. Then, we have the following
result:

$\forall\vec{z}.\
\operatorname{softmax}(\vec{z})\textsubscript{i}-\widehat{\operatorname{softmax}}(\vec{z})\textsubscript{i}\leq\frac{n-2}{(\sqrt{n-1}+1)^{2}}+2\delta$

###### Proof.

The error bound is the difference between the upper and lower bounds of the
$\operatorname{softmax}$ and it is a function of the number of outputs $n$ of
the neural network and the error $\delta$ for the approximation of the
sigmoid.

$\begin{split}\gamma(n,\delta,\vec{z})\textsubscript{i}=\operatorname{\widehat{Sig}}(z{\textsubscript{\tiny
i}}-\mathop{max_{1}^{n}}_{j\neq
i}(z_{j}))+\delta-\widehat{\operatorname{softmax}}(\vec{z})\textsubscript{i}\end{split}$
$\begin{split}\gamma(n,\delta,\vec{z})\textsubscript{i}=\frac{\alpha(\vec{z})\textsubscript{i}(n-2)}{(\alpha(\vec{z})\textsubscript{i}+1)((n-1)\alpha(\vec{z})\textsubscript{i}+1)}+2\delta\end{split}$

where:

$\begin{split}\alpha(\vec{z})\textsubscript{i}=e^{-z_{i}+\mathop{max_{1}^{n}}_{j\neq
i}(z_{j})}\end{split}$

Since $z_{i}=max(z_{1},\cdots,z_{n})$ then is always
$0<\alpha(\vec{z})\textsubscript{i}\leq 1$. Let us now replace
$\alpha(\vec{z})\textsubscript{i}$ with the variable $m$ and study the
function in the domain $m\in]0,1]$ with $n\in\mathbb{N},n\geq 2$:

$\begin{split}\zeta_{n}(m)=\frac{m(n-2)}{((m+1)((n-1)m+1)}\end{split}$

To compute the maximum in the domain $m\in]0,1]$ we first compute the
derivative using the quotient rule:

$\begin{split}\zeta^{\prime}_{n}(m)=\frac{(n-2)((1-n)m^{2}+1)}{((m+1)^{2}((n-1)m+1)^{2}}\end{split}$

To find the point $m_{max}$ for which we have the maximum
$\zeta_{n}(m_{max})$, we need to find the positive root for the following
equation:

$\begin{split}(n-2)((1-n)m^{2}+1)=0\end{split}$

The positive root is:

$\begin{split}m_{max}=\frac{1}{\sqrt{n-1}}\end{split}$

As a consequence, the maximum is:

$\begin{split}\zeta_{n}(m_{max})=\frac{n-2}{(\sqrt{n-1}+1)^{2}}\end{split}$

If the number of outputs is two, the softmax behaves as a sigmoid. Thus, the
only error is the one due to the piece-wise approximation ($2\delta$) of the
sigmoid. Let us assume to have three outputs and $\delta=0.0001$ then the
maximum error between the real softmax and the approximated one is
$\frac{1}{(\sqrt{2}+1)^{2}}+0.0002\sim 0.17177$.

∎

######  Theorem 2.

(Class consistency) Let $f$ and $\hat{f}$ denote the real and the approximated
(with precision $\delta$) neural networks with $n\geq 2$ outputs,
respectively. Then:

$\operatorname{conf}(\hat{f}(\vec{x}))>\frac{1}{2}\implies\operatorname{class}(\hat{f}(\vec{x}))=\operatorname{class}(f(\vec{x}))$

###### Proof.

$\operatorname{conf}(\hat{f}(\vec{x}))=\max(\hat{\operatorname{out}}(v_{l,1}),\ldots,\hat{\operatorname{out}}(v_{l,n}))>\frac{1}{2}$.
Let us assume that the component
$\hat{\operatorname{out}}(v_{l,i})>\frac{1}{2}$ is the maximum value resulting
from applying the approximated softmax. From Theorem 1 we have that
$\operatorname{out}(v_{l,i})\geq\hat{\operatorname{out}}(v_{l,i})>\frac{1}{2}$
and consequently $i$ is the class for both the real and the approximated
neural network
$\operatorname{class}(f(\vec{x}))=\operatorname{class}(\hat{f}(\vec{x}))$. ∎

######  Theorem 3.

(Soundness) Let $f$ and $\hat{f}$ be the original neural network and over-
approximated neural network, respectively. Let $b_{n,\delta}$ be the error
bound of the approximated softmax
($b_{n,\delta}=\frac{n-2}{(\sqrt{n-1}+1)^{2}}+2\delta$ (see Theorem 3.1)).
Then we have the following soundness guarantee: Whenever the approximated
neural network is 2-safe for $\operatorname{conf}(\hat{f}(\vec{x}))>(\kappa-
b_{n,\delta})$, the real neural network is 2-safe for
$\operatorname{conf}(f(\vec{x}))>\kappa$, given
$\operatorname{conf}(\hat{f}(\vec{x}))>\frac{1}{2}$. Formally:

$\left(\begin{split}\forall\vec{x},\vec{x^{\prime}}.\operatorname{cond}(\vec{x},\vec{x^{\prime}},\vec{\epsilon})\land{\operatorname{conf}}(\hat{f}(\vec{x}))>(\kappa-
b_{n,\delta})\\\
\implies{\operatorname{class}}(\hat{f}(\vec{x}))={\operatorname{class}}(\hat{f}(\vec{x^{\prime}}))\end{split}\right)\implies\\\
\left(\begin{split}\forall\vec{x},\vec{x^{\prime}}.\
\operatorname{cond}(\vec{x},\vec{x^{\prime}},\vec{\epsilon})\land\operatorname{conf}(\vec{f(x)})>\kappa\\\
\implies\operatorname{class}(f(\vec{x}))=\operatorname{class}(f(\vec{x^{\prime}}))\end{split}\right),\mbox{
with }\>\operatorname{conf}(\hat{f}(\vec{x}))>\frac{1}{2}$

###### Proof.

Let us consider all possible cases around the implications one by one and see
if they hold. The theorem to prove is of the form
$(\hat{A}\implies\hat{B})\implies(A\implies B)$ where:

$\displaystyle\hat{A}\stackrel{{\scriptstyle\textup{\tiny
def}}}{{=}}\left(\forall\vec{x},\vec{x^{\prime}}.\operatorname{cond}(\vec{x},\vec{x^{\prime}},\vec{\epsilon})\land{\operatorname{conf}}(\hat{f}(\vec{x}))>(\kappa-
b_{n,\delta})\right),$
$\displaystyle\hat{B}\stackrel{{\scriptstyle\textup{\tiny
def}}}{{=}}\left({\operatorname{class}}(\hat{f}(\vec{x}))={\operatorname{class}}(\hat{f}(\vec{x^{\prime}}))\right),$
$\displaystyle A\stackrel{{\scriptstyle\textup{\tiny
def}}}{{=}}\left(\forall\vec{x},\vec{x^{\prime}}.\operatorname{cond}(\vec{x},\vec{x^{\prime}},\vec{\epsilon})\land\operatorname{conf}(\vec{f(x)})>\kappa\right),$
$\displaystyle B\stackrel{{\scriptstyle\textup{\tiny
def}}}{{=}}\left(\operatorname{class}(f(\vec{x}))=\operatorname{class}(f(\vec{x^{\prime}}))\right)$

Case 1: If ${\operatorname{conf}}(\hat{f}(\vec{x}))\leq\kappa-b_{n,\delta}$
then $\operatorname{conf}(f(\vec{x}))\leq\kappa$ follows from Theorem 1 and
the assumption that $\operatorname{conf}(\hat{f}(\vec{x}))>\frac{1}{2}$.
$\hat{A}$ will be false and $\neg\hat{A}\implies\neg A$ so also $A$ is false
and $(\hat{A}\implies\hat{B})\implies(A\implies B)$ is true.

Case 2: Assume ${\operatorname{conf}}(\hat{f}(\vec{x}))>\kappa-b_{n,\delta}$.
From Theorem 2 we have that
$\operatorname{class}(\hat{f}(\vec{x}))=\operatorname{class}(f(\vec{x}))$ and
$\operatorname{class}(\hat{f}(\vec{x^{\prime}}))=\operatorname{class}(f(\vec{x^{\prime}}))$
so $\hat{B}\implies B$ and then independently of $A$ we have that
$(\hat{A}\implies\hat{B})\implies(A\implies B)$ is true.

The soundness theorem, thereby, states that if the confidence-based 2-safety
property holds on the over-approximated neural network, it also holds on the
original network. ∎