Due to their remarkable learning capacity and astounding accuracy on labelled datasets, Neural Networks (NNs) have become a ubiquitous paradigm in the Machine Learning (ML) based smart systems. Several present day applications including object detectors, speech recognizers, malware detectors, and even the safety-critical applications like medical diagnosis and autonomous driving increasingly rely on NNs [1][2]. However, NNs are extremely sensitive to changes in input, and even the imperceptible input noise can cause the NN to misclassify [3]. This makes obtaining reliable guarantees regarding correct NN behavior a significant need. A standard practice to ensure a good performance of a trained NN is to test it with a given validation dataset. However, the applications where NNs are deployed often have infinite input domain, for instance, when subjected to lifelong learning scenarios [4]. This makes exhaustive testing infeasible for NNs. Moreover, the validation datasets are insufficient to generalize to the vast input domain. This undermines testing as an option to obtain reliable guarantees regarding the NN. Intuitively, since formal methods ought to provide reliable guarantees regarding a system’s behavior, there has been an
Fig. 1: Overview of FANNet with Novel Contributions for the Formal Analysis of NN properties, by exploiting Model Checking
increasing interest to use formal methods [5][6] to ascertain correctness of the trained NNs. However, the non-linearity and non-convexity of the NNs, along with the NP-completeness [5] of verifying even the piece-wise linear NNs, makes formal analysis of NNs an extremely challenging task. The current objective of formal analysis of NNs is to ensure the robustness of a trained network in the presence of small input perturbations. The idea is to ensure that adding perturbations, known as the adversarial noise, to the network input must not change output classification of the network.
A. Limitations in State-of-the-Art and Open Challenges
There remains several unresolved problems in the state-of-the-art regarding formal analysis of NNs (which will be discussed further in Sections II):
1) The current formal verification frameworks like [7][8] mostly focus on ensuring network robustness in the presence of input noise. However, they seldom focus on obtaining the noise tolerance of the trained NN.
2) The decision making of the NN is often incomprehensible to humans. The understanding regarding the sensitivity of the individual NN input nodes, which often lacks in current works, may provide useful insights to the NN inference.
3) The effects of training bias of a NN deployed in practical systems are well-studied. However, its effects under input noise and use formal analysis to ensure fair training procedure remain scarcely studied topics.
B. Our Novel Contributions and Concept Overview
We propose a formal analysis methodology, FANNet, to address the aforementioned challenges; see Fig. 1. The novel contributions of this work (elaborated in Sections IV, V) are:
1) Formal modeling and analysis methodology to analyze the trained NN as a state-space model, using model checking.
2) Providing realistic estimates for the network tolerance in the presence of adversarial noise.
3) Studying input node sensitivity in the presence of noise. 4) Analyzing the effects of training bias on network accuracy. 5) Performing a case study on Leukemia Detection to demonstrate the practical significance of the above analysis.
Verification for NN Robustness - Verification for ensuring network robustness, has been an active domain of research for NNs. These works focus on either: (a) expressing the network and its robustness property in Conjunctive Normal Form (CNF), and verifying it using a satisfiability (SAT) solver [5][7]–[9], (b) transforming the problem into a set of linear constraints and objective function, and verifying the network as an optimization problem using a linear programming (LP) solver [6][10]–[12], or (c) using a combination of both SAT and LP solvers [13], under a specified space around the seed inputs. Unlike the current literature, we analyze NN properties beyond network robustness, using model checking.
Training Bias and Input Node Sensitivity - Biased training data is among the leading causes for a biased NN [14]. To solve the problem, either specialized training algorithms are proposed [15][16], or formal analysis is used to ensure fairness of the NN [17] in presence of larger (observable) bias. On the other hand, the literature focusing on input node sensitivity of NN [18][19] generally aims either to identify input features that can be pruned out of the network without hampering the network performance, in the absence of noise, or use input noise to study nodes’ response for selection of input features [20][21]. Our work, on the other hand, takes a more qualitative approach with input sensitivity, and identifies the input nodes that require precise input acquisition to avoid misclassification.
This section provides the background knowledge on basic NN concepts and properties necessary to understand our novel contributions. The notations introduced in this section will be followed in the subsequent sections.
A. Neural Network and its Properties
We consider feed-forward network, with L fully-connected (FC) layers, each containing N neurons. Each neuron of a layer is connected to all neurons of the previous layer with a deterministic relation between inputs, the associated weight matrix w and the bias vector b. The overall network is given by , where x and
represent input and output layers of the network respectively.
Except the input layer, each layer is associated with a non-linear activation function . The most common activation functions are: Rectified Linear Unit (ReLU), maxpool, sigmoid and softmax. In this paper, we focus on ReLU and maxpool activations due to their predominant use in practical NNs recently [22].
Robustness is an essential property of a NN that determines its sturdiness in the presence of small noise . A network is
Input Node Sensitivity indicates the robustness of individual input nodes to the input perturbations. The neurons (or nodes) in the input layer typically represent distinct, although often correlated, features of the input. An input node is said to be insensitive to a small noise
, if the addition of this noise does not change the predicted output label:
B. Model Checking using nuXmv
Model checking is a formal analysis technique that enables rigorous verification of the system model defined as a state-space. The standard procedure used during model checking includes the representation of system and its properties in the formal language of the model checker. Model checker then searches the system’s state-space either to ensure functional correctness or to find counterexamples in case of failure of the desired properties. The model checkers can either be based on Satisfiability solvers (SAT/SMT) or Binary Decision Diagrams (BDDs). BDD-based model checkers are limited by space due to their PSPACE-complete computational complexity. On the other hand, SAT-based model checkers, despite their NP-complete computational complexity, can handle larger number of variables. As will be shown in Section V, the state-space of NN, in the presence of noise, can grow exponentially. Hence, the SMT-based symbolic model checker, nuXmv [23], is an appropriate tool for our experiments. It supports both discrete and continuous domains, including real numbers R and unbounded integers Z, and allows the use of propositional and temporal logics.
Fig. 2 provides a comprehensive view of our FANNet methodology comprised of the following three key procedures.
A. Behavior Extraction
The NN testing samples (X) and their true labels are available at the input. In this step, the weights
and
Fig. 2: FANNet: A Methodology for Formally Analyzing Neural Network Properties using Model Checking
activations of the trained NN, which determine the network’s architecture and functionality, are first translated into the SMV model and the Temporal properties, using the formal language of the model checker. Prior to the analysis with input noise, the correctness of the NN model without noise is ensured by comparing the model’s calculated outputs (OC) against , i.e., P1 in Fig. 2.
B. Noise Tolerance Analysis
The formal analysis for noise tolerance, proceeds as follows: 1) A large noise range for the analysis is initialized. From this specified range, a unique noise vector (NV ) is non-deterministically selected in each iteration.
2) Noise is added relatively to the input, and the input then transverses through the network layers.
3) is then computed and compared to
of the input. Until counterexamples to
(i.e., P2 in Fig. 2) are available, the noise is reduced iteratively. As soon as P2 becomes true, the noise tolerance of the NN is obtained.
4) The process is repeated for all inputs in the dataset.
C. Adversarial Noise Vector Extraction
If and the NV is not already contained in e, then the NV obtained from the generated counterexample is added to e, as shown by P3 in Fig. 2. This ensures that e is an array of unqiue noise patterns to which the NN is vulnerable.
A. Problem Description
We considered a feed-forward FC neural network architecture as shown in Fig. 3. It comprises of an input layer, one hidden layer and an output layer, with 6, 20 and 2 nodes respectively. The activations used in the network are ReLU and Maxpooling. We trained the network1 to diagnose leukemia using the standard Leukemia database [24], consisting of 38 training samples and 34 testing samples containing genetic attributes for Acute Lymphoblast Leukemia (ALL) and Acute Myeloid Leukemia (AML). In total, each data sample has 7129 of these genetic
Fig. 3: (a) Feed-forward FC-NN trained for Leukemia Classification; (b) FSM for the given NN, in the absence of input noise; (c) FSM for NN with Noise Range [0, 1]%
attributes. From these, the top five most significant genes are picked as NN inputs using the Minimum Redundancy and Maximum Relevance (mRMR) feature selection method [25].
B. FANNet Implementation
Varying noise ranges were input to the network, as explained in the previous section. The main goals of the analysis are: (a) to determine noise tolerance for the given network by gradually reducing the applied noise until no noise pattern that causes the true label
to change can be found, and (b) to study network properties like training bias and input node sensitivity on the basis of the obtained counterexamples. It must also be highlighted that the objective of this work is not to exhaustively search for counterexamples, but rather to explore network properties on the basis of obtained counterexamples.
C. Formal Analysis of the Neural Network Properties
We initiate the experiment using nuXmv with a large input noise, and gradually reduce the noise until nuXmv can verify the absence of any counterexamples for the given noise. The observations and analysis from our experiments, as illustrated in Fig. 4, are as follows:
1) Noise Tolerance: For all the correctly classified inputs in the testing dataset, addition of a noise or less does not trigger misclassification for the given NN. Hence, assuming input noise to be the integer percentage values, the given NN has an estimated noise tolerance of
.
2) Classification Boundary Estimation: A few inputs among the dataset (i.e., inputs closer to the classification boundary) were observed to be highly susceptible to input noise.
Fig. 4: Estimated Noise Tolerance, Impact of Noise on inputs closer to Classification Boundary, Effects of Training bias on NN Accuracy, and Sensitivity of specific Input Nodes
On the other hand, for other inputs, noise even as large as 50% of the input did not trigger misclassification at the output. This knowledge can be used to estimate the network’s classification boundary in the hyperspace.
3) Training Bias: Inputs with were observed as more likely to be misclassified than the inputs with
. On a closer inspection of the training dataset, it is observed that approximately 70% of the data samples belong to the output class
i.e., the training is biased towards the output
. This is corroborated by our formal analysis, where the misclassification of inputs with true output
is more probable than the misclassification of inputs with true output
.
4) Input Node Sensitivity: No counterexamples were obtained with positive noise at input node . Moreover, the counterexamples suggest more noise patterns with positive noise at input node
than the other way around. The knowledge of the input node sensitivity, in some applications, could be exploited in the design of variable-precision data acquisition methodologies, where the resource-greedy measurements could be reserved for obtaining the sensitive inputs.
Input noise is known to trigger output misclassification in Neural Networks (NNs). Traditionally, the formal analysis of NNs focuses on checking network robustness for different bounded noise. However, other network properties, i.e., network tolerance, training bias, and input node sensitivity, affecting NN’s performance and are often neglected. To the best of our knowledge, this is the first model checking based formal analysis methodology that aims at investigating these properties affecting NNs. We use our methodology to estimate noise tolerance for a NN trained for Leukemia classification, to investigate training bias in the network due to the biased dataset, and to explore the sensitivity of the different genetic attributes presented by network’s input nodes.
This work was partially supported by Doctoral College Resilient Embedded Systems which is run jointly by TU Wien’s Faculty of Informatics and FH-Technikum Wien, and partially supported by the Erasmus+ International Credit Mobility (KA107).
[1] A. Esteva et al., “A guide to deep learning in healthcare,” Nature Medicine, vol. 25, no. 1, p. 24, 2019.
[2] M. Fink et al., “Deep Learning-Based Multi-scale Multi-object Detection and Classification for Autonomous Driving,” in Fahrerassistenzsysteme. Springer, 2019, pp. 233–242.
[3] C. Szegedy et al., “Intriguing properties of neural networks,” preprint arXiv:1312.6199, 2013.
[4] G. Anthes, “Lifelong learning in artificial neural networks,” Communications of the ACM, vol. 62, no. 6, pp. 13–15, 2019.
[5] G. Katz et al., “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks,” in CAV. Springer, 2017, pp. 97–117.
[6] V. Tjeng et al., “Evaluating Robustness of Neural Networks with Mixed Integer Programming,” in ICLR, 2019, pp. 1–21.
[7] N. Narodytska et al., “Verifying Properties of Binarized Deep Neural Networks,” in AAAI, 2018, pp. 6615–6624.
[8] X. Huang et al., “Safety Verification of Deep Neural Networks,” in CAV. Springer, 2017, pp. 3–29.
[9] C.-H. Cheng et al., “Verification of Binarized Neural Networks via Inter- Neuron Factoring,” in VSTTE. Springer, 2018, pp. 279–290.
[10] S. Dutta et al., “Output Range Analysis for Deep Feedforward Neural Networks,” in NFM Symposium. Springer, 2018, pp. 121–138.
[11] P. Kouvaros et al., “Formal Verification of CNN-based Perception Systems,” preprint arXiv:1811.11373, 2018.
[12] S. Wang et al., “Efficient Formal Safety Analysis of Neural Networks,” in NIPS, 2018, pp. 6367–6377.
[13] R. Ehlers, “Formal Verification of Piece-wise Linear Feed-Forward Neural Networks,” in ATVA. Springer, 2017, pp. 269–286.
[14] N. Mehrabi et al., “A survey on bias and fairness in machine learning,” arXiv preprint arXiv:1908.09635, 2019.
[15] B. Fish et al., “A confidence-based approach for balancing fairness and accuracy,” in ICDM. SIAM, 2016, pp. 144–152.
[16] L. E. Celis et al., “Classification with fairness constraints: A meta- algorithm with provable guarantees,” in FAT*. ACM, 2019, pp. 319–328.
[17] O. Bastani et al., “Verifying Fairness Properties via Concentration,” arXiv preprint arXiv:1812.02573, 2018.
[18] J. M. Zurada et al., “Sensitivity analysis for minimization of input data dimension for feedforward neural network,” in ISCAS, vol. 6. IEEE, 1994, pp. 447–450.
[19] A. Hunter et al., “Application of neural networks and sensitivity analysis to improved prediction of trauma survival,” Computer Methods and Programs in Biomedicine, vol. 62, no. 1, pp. 11–19, 2000.
[20] W. Wang, “Quantifying relevance of input features,” in IDEAL. Springer, 2002, pp. 588–593.
[21] M. Cao et al., “Neural network ensemble-based parameter sensitivity analysis in civil engineering systems,” Neural Computing & Applications, vol. 28, no. 7, pp. 1583–1590, 2017.
[22] G. Huang et al., “Densely connected convolutional networks,” in IEEE CVPR, 2017, pp. 4700–4708.
[23] M. Bozzano et al., nuXmv 1.1. 1 User Manual, 2016.
[24] “Leukemia data,” http://web.stanford.edu/hastie/CASI files/DATA/ leukemia big.csv.
[25] S. Khan et al., “A novel fractional gradient-based learning algorithm for recurrent neural networks,” CSSP, vol. 37, no. 2, pp. 593–612, 2018.