ソフトウェア・シンポジウム 2023 in 仙台

Testing-based formal veriﬁcation for ReLU-based neural networks
Haiyi Liu
Hiroshima Universityd200101@hiroshima-u.ac.jp

Shaoying Liu
Hiroshima University
sliu@hiroshima-u.ac.jp

Ai LiuHiroshima University
liuai@hiroshima-u.ac.jp

Yujun Dai
Hiroshima Universityd201609@hiroshima-u.ac.jp

is diﬃcult to be explained, that is, it is diﬃcult for
us to ﬁgure out what features the result of neural network reasoning is based on. For instance, although aneural network correctly recognizes the cat in the picture, we cannot determine whether the neural network
correctly recognizes the cat through its features or thewatermark in the picture.
Generally, the post-condition of a neural network iseasy to give. If the pre-condition can be derived fromthe neural network by using the post-condition, thenusers can use the pre-condition to explain and verify
the reliability of the neural network. However, since
the veriﬁcation of neural networks is an NP-hard problem, it is very diﬃcult to derive the preconditions fromthe post-conditions simply by using the veriﬁcation algorithm.
Existing methods mainly focus on how to accelerate the veriﬁcation speed of neural network under thepremise of given formal speciﬁcation [2, 3, 4, 5]. Thesestudies provide a basis for the veriﬁcation of neural networks, but do not discuss how to give a pre-condition
to explain neural networks. Test-based neural network
interpretation algorithm can explain the behavior of
the local neural network by testing and constructing
the local interpretation model of the neural network[6, 7, 8]. But they cannot be used to formally verify the reliability of neural networks. In other words,
it can not be guaranteed that there is no adversarial
examples in the neural network within a certain range.

Abstract
Since neural networks are widely used, how to ensure thereliability of neural networks has become a hot research
topic. The ﬁrst diﬃculty is that it is diﬃcult to give thepre-condition and post-condition for neural networks, andthe second diﬃculty also exists in traditional software, i.e.,
the problem of exploding execution paths. Fortunately, theoutput range of a neural network is easier to give and when
an input is given, we can obtain the activation order ofneurons in the neural network. Based on the above facts,
we propose DeepTBFV, a method for pre-trained neuralnetworks, which uses a testing-based formal veriﬁcation algorithm to derive the pre-condition of the neural network
on a speciﬁed path by post-condition. The purpose is toverify and explain the behavior of the neural network.

1. Introduction
Although neural network has been widely used inmany ﬁelds such as NLP (natural language processing), image processing and even MMML（Multi-modal
Machine Learning）, its poor reliability has also been
criticized by users for a long time. Speciﬁcally, there
are two aspects. One is that the neural network is
diﬃcult to be veriﬁed. The reason is that the architecture of the neural network is based on experience, andthe parameter is constructed by back-propagation of
the training data. It is diﬃcult to give a formal speciﬁcation like traditional software, and the veriﬁcationof the neural network is an NP-hard problem[1], whichmakes it diﬃcult to achieve complete veriﬁcation of thelarge models. The second is that the neural network

44

SEA

ソフトウェア・シンポジウム 2023 in 仙台

2.2. Floyd-Hoare Logic

In this paper, We propose DeepT BF V , a method
to give the pre-condition of neural network by backward derivation of the post-condition of neural network. DeepT BF V is inspired by Testing-based formal
veriﬁcation (TBFV) [9, 10, 11] in traditional software.
First, we select a test case that can be correctly recognized by the neural network and execute it. During theexecution of the test case, the activation of each neuron
is recorded. Here, we compare the activation sequenceof neurons to the execution path of the test case in traditional software. Therefore, recording the activation
sequence of neurons is the execution path of the test
case generated by the neural network. Then, according to the execution results of the neural network, thepost-condition of the test case is given, which is used
to derive the pre-condition.
Finally, we combine the post-condition and the execution path on the neural network to form a systemof linear inequalities with multiple variables. The precondition of the neural network is obtained by solving the system of linear inequalities with multiple variables.
In brief, the main contributions of this paper are as
fellows:

Floyd Hoare logic, also known as Hoare logic, represents predicate logic and a set of axioms in the form of
Hoare triples, and then deﬁnes the semantics of the programming language. The speciﬁc form of Hoare triples
is as follows:{pre} c {post}
where c is a speciﬁc program code, pre indicates thepreconditions in the program, which describes the program state before executing c, and post indicates thepost condition in the program, which describes the programs the program state after executing c. Such a
Hoare logic triple indicates that if an input of the program c meets its pre, the output of c should meet post
after executing program c. Otherwise, program c musthave errors.
In order to formalize the program, Hoare logic deﬁnes inference rules for each of grammar clauses. The
detailed rules are as follows.
Assign{Q(E/x)} x := E {Q}

The rules is to perform the assignment statement
x := E on all x in the precondition {Q(E/x)}, that is,
to replace all x in the precondition with E to obtain
the post condition {Q}. Similarly, the following two
rules can exist.
Preconditions reinforcement rule:• To my best knowledge, we develop the ﬁrst testingbased formal veriﬁcation method for DNNs.
• We design a veriﬁcation based neural network retraining algorithm.

P re

2. Preliminary

P ⇒ P ′ {P ′ }c{Q}{P }c{Q}

Post conditional weakening rule:

2.1. Testing-based formal veriﬁcation

P ost

The testing-based formal veriﬁcation (TBFV) is proposed to ensure the correctness of all traversed program
paths in traditional software. The ﬁrst step of TBFV
is to generate a test case T based on the test condition in the formal speciﬁcation. The second step is toobtain a traversed program path by executing the test
case T execution program P , where the path contains
a series of conditions. The third step is to verify thereliability of the path under the formal speciﬁcation byusing symbolic execution or Hoare logic [12].

{P }c{Q′ } Q′ ⇒ Q{P }c{Q}By formalizing the program with these rules, we canget a series of constraints of the program, and then use
SMT solver. Solve the corresponding rules.
2.3. Veriﬁcation of neural networks
Deep neural network is a mapping in highdimensional space, which can be formally expressed as
f : Rn → Rm .

45

SEA

ソフトウェア・シンポジウム 2023 in 仙台

3.1. Testing-based neural network execution
path generation
The execution of a test case by the neural network
means that the test case is used as the input for forward
propagation. In the process of forward propagation,
the state of each neuron is ﬁxed. That is, we consider
a neuron ni in a neural network N N to be activatedfor the test case if its output is greater than a thresholdvalue. Conversely，if ni is less than the threshold, then
the neuron ni is not activated. We record the activation
state of each neuron when the N N forward propagate
for the test case.
Formally, we deﬁne all neurons in N N as the set
neurons. Then, the neurons activated in N N can bedeﬁned as the set ActiveN = {n | n ∈ neurons ∧Out(n)>θ}, where θ is the threshold in neurons andout(n) record as the output value of neuron. Similarly,
the inactive neurons in N N can be deﬁned as the set
InactiveN = {n | n ∈ neurons ∧ Out(n) ≤ θ}. asshown in ﬁgure 1, in the forward propagation of neuralnetwork, we use blue for the neurons activated in thetest case and red for the inactive neurons. Then, theprocess of assigning activation states to the neuron inneurons through the test cases is called execution pathgeneration.

Figure 1. Execution path generation
if there is a set of constraints ϕ which is the precondition of f on Rn , and existence a set of constraints
φ which is the post condition of f on Rm . Then, theproblem of neural network veriﬁcation is transformed
into proving that ∀x ∈ Rn : ϕ(x) → φ(f (x)) is satisﬁed
or not.

3. Methodology
In this section, we propose an algorithm to derive thepre-condition of a pre-trained neural network from its
post-condition, named DeepTBFV. The pre-condition
can be used to verify and explain the behavior of theneural network and assist developers to increase thereliability of the neural network. First, we forward
propagate a test case on a neural network, and generate the execution path of the test case. Second, we
propose a technique to encode the execution path as amultivariate linear inequality system, and since the activation state of neurons is ﬁxed in the execution path,the linear constraints generated by the execution path
do not need to introduce the relaxation variables. Finally, we use the classiﬁcation results obtained fromthis test case to deﬁne the post-condition of the test
case and derive the pre-condition in reverse. The process of deﬁning the post-condition is based on an assumption that will be described in the third summary.

3.2. Formal modeling of neural network pathes
Since the state of activation of each neuron is ﬁxed,
we can convert the state of each neuron into a multiplei−1
i−1linear inequality. Let N euronij = {xi−11 , x 2 , · · · xn }is the set of inputs of the j-th neuron in the i-th layerof the neural network N N . If the activation functionof Neuron is ReLU and is activated by the test case,the activation state of the neuron can be modeled asfollows,
If : N euronij ∈ ActiveN
T hen : Out(N euronij ) = w1i−1 · xi−1
· · · + wni−1 · xi−1
n >01Similarly，if the neuron is not activated by the test
case, then the activation state of the neuron can bemodeled as follows,
If : N euronij ∈ InactiveN

46

SEA

ソフトウェア・シンポジウム 2023 in 仙台

T hen : Out(N euronij ) = w1i−1 ·xi−1· · ·+wni−1 ·xi−1
≤0
n
1

or
fji (x1 , x2 , · · · xn )>0

According to the above rules, we can model the process of forward propagation of test cases in the neuralnetwork into a system of multivariate linear inequalities. Algorithm 1 speciﬁcally describes how to model
the execution path of nn.

The constraints of the output layer of the neuralnetwork are diﬀerent from those of the middle layer.
It should conform to the user-deﬁned post-condition.
Here, the constraints of neurons in the output layer
can be denoted as,

Algorithm 1: Formal modeling of N N pathes
Input: N eurons ; ActiveN ; InactiveN// List of linear constraints
corresponding to neural network
Output: Constraint
1 Constraint = list()
2 for neuron in Neurons do
3
if neuron in ActiveN then4
Constraint.append(Out(neuron)>0)
else
5
Constraint.append(Out(neuron) ≤
0)
6
end
7
8
9

αj ≤ yj (x1 , x2 , · · · xn ) ≤ βjWhere yj (x1 , x2 , · · · xn ) is a multivariate linear
polynomial.j represents the j-th output of the output layer. The interval Oj = [αj , βj ] means the postcondition of yj .
In addition, we also propose a method to construct a
post-condition for the path generated by test cases. If
the test case activates a neuron in the output layer, itmeans that the output value of the activated neuron isgreater than that of other inactive neurons. Therefore,
we can formally record this statement as yja >yiin , wherei ∈ {1, 2 · · · m}\{j}, a represents activated neuron，inrepresents inactive neurons. The activated neurons aremarked as j. Since the output value of a neuron has
an upper and lower limit, such as IN T 8 quantizationof a neural network, the output values of neurons arequantized to the [−128, 127]. Therefore, we can also
give the upper and lower limits of the output value of
neurons in the output layer. Let the upper and lower
bounds of the output layer neurons be [l, u]，where the ldenote upper bound, and u denote lower bound. Then,end
end
return Constraint

3.3. Deriving Preconditions from Postconditions
When the state of each neuron in the neural network
is ﬁxed, we only need to carry out the Floyd-Hoare
Logic assignment statement for the constraint of eachneuron. This means that the constraints of each neuron are replaced by variables through the assignment
statement. The constraints of each neuron we can get
only include the input of the neural network.
Speciﬁcally, let Inp = {x1 , x2 , · · · xn }, Inp ∈ Rn as
the input of the N N and Out = {y1 , y2 , · · · ym }, out ∈Rm as the output of the N N . Moreover, We record
the replacement expression of the j-th neuron in thei-th layer as fji . Then the constraint corresponding toneurons can be denoted as∀yi ∈ Out, ∃ αi ≤ yi ≤ βi
where i ∈ {1, 2, · · · m}, and m is the number of output
layer.

4. Case StudyIn this section, we use a three-layer neural network
to show how DeepTBFV works and to demonstrate its
eﬀectiveness. Consider a ReLU-based neural network
G. The structure and weights of this network are shownin Fig 2. Without loss of generality, we can assume
that bias = 0 for each neuron in G. We denote thefji (x1 , x2 , · · · xn ) ≤ 0

47

SEA

ソフトウェア・シンポジウム 2023 in 仙台

neurons of the input layer, the neurons of the hidden
layer and the neurons of the output layer as {x1 , x2 },{h1 , h2 , h3 }, {y1 , y2 } respectively.
To execute DeepTBFV for G, all the steps are given
in sequence as follows:
Step 1: Select the test case of interest as input to theneural network, suppose we use x1 = 1, x2 = 2 as thetest case.
Step 2: Record the activation of each neuron in thehidden layer of the neural network,

1
x1

-1

2
x2

-2

2

-1

1

h2 = ReLU (2x1 − x2 = 0) ∈ InactiveN
h3 = ReLU (x1 + x2 = 3) ∈ ActiveN
Step 3: Generate neural network middle layer constraints,

1

1

h2

h1

h1 = ReLU (−x1 + 2x2 = 3) ∈ ActiveN

-1

1

h3

1

2

0.5

y1

y2

5  y1  7

3  y2  5

Figure 2. Example showing How to execute
DeepTBFV

h1 = −x1 + 2x2 >0
h2 = 2x1 − x2 ≤ 0
h3 = x1 + x2 >0

5. Related Work

Step 4: Generate output layer constraints, here weassume that the output layer has constraints,

In recent years, with the extensive application ofdeep learning, its reliability and interpretability havebeen increasingly concerned by the security community. Heuristic algorithms provide a fast and eﬃcient
way to interpret neural networks.
The heuristic algorithm provides a fast and eﬀective
way to explain the neural network. LIME[13] uses atesting-based method combine regression to explain thelocal characteristics of neural networks. Similar algorithms are anchors, etc[14, 15, 16]. Although heuristic
algorithms can provide quick explanations, the resulting explanations are not guaranteed by formal veriﬁcation.
Meanwhile, rigorous formal veriﬁcation provides another perspective to ensure reliability and provide explanations. The work of reluplex et al.[17, 18, 19] performs formal veriﬁcation of neural networks based on
speciﬁcation. It can guarantee that the veriﬁed neuralnetwork is safe and secure under formal speciﬁcation.

5 < y 1 = h1 − h2 + h3 < 7
3 < y1 = h1 + 2h2 + 0.5h3 < 5
Step 5: Through Floyd-Hoare Logic, the system ofinequality equations for each neuron in the input layer
is derived backwards,
2x1 − x2 ≤ 0−x1 + 2x2 >0−x1 − x2 <0
3< − 0.5x1 + 2.5x2 <5
5<3x2 <748

SEA

ソフトウェア・シンポジウム 2023 in 仙台

However, reluplex[?] also proved that the veriﬁcation
problem of neural networks is NP hard. And the interpretation of veriﬁcation-based neural networks is likewise based on veriﬁcation solvers. Therefore, Trustable
XAI et al.[20, 21] faces the same problem of diﬃculty
in interpreting large neural networks.

In: Computer Aided Veriﬁcation: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30.
(Springer, 2017. pp. 97–117[2] Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana,
S. ‘Formal security analysis of neural networks using symbolic intervals’. In: 27th {USENIX} Security Symposium ({USENIX} Security 18). (, 2018.
pp. 1599–1614

6. Conclusion
We propose DeepTBFV, a test-based approach togenerate execution paths for a test case in a neural network and derive the pre-condition(linear constraints) of
the input to the neural network backwards by meansof a custom post-condition. To my best knowledge, weare the ﬁrst to apply the idea of TBFV to the ﬁeld of
veriﬁcation and interpretation of neural networks.

[3] Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R. ‘Eﬃcient veriﬁcation of relubased neural networks via dependency analysis’.
In: Proceedings of the AAAI Conference on Artiﬁcial Intelligence. vol. 34. (, 2020. pp. 3291–3299[4] Katz, G., Huang, D.A., Ibeling, D., Julian, K.,
Lazarus, C., Lim, R., et al. ‘The marabou framework for veriﬁcation and analysis of deep neuralnetworks’. In: Computer Aided Veriﬁcation: 31st
International Conference, CAV 2019, New York
City, NY, USA, July 15-18, 2019, Proceedings,
Part I 31. (Springer, 2019. pp. 443–452

7. Future WorkIn this paper, we focus on how to use the principle of
TBFV to generate the pre-condition of neural network.
However, it did not analyze in detail how to generate
test cases and how to use the generated constraints toverify or explain the behavior of neural networks. In
future work, we will focus on the following two parts:[5] Shriver, D., Elbaum, S., Dwyer, M.B. ‘Dnnv: A
framework for deep neural network veriﬁcation’.
In: Computer Aided Veriﬁcation: 33rd International Conference, CAV 2021, Virtual Event, July
20–23, 2021, Proceedings, Part I 33. (Springer,
2021. pp. 137–150• How to choose the appropriate test case so thatthe constraints generated by DeepTBFV for thattest case are more locally interpretable.
• How to analyze the constraints generated by
DeepTBFV so that the constraint results can help
people intuitively understand the neural network.

[6] Sun, Y., Huang, X., Kroening, D., Sharp, J.,
Hill, M., Ashmore, R. ‘Deepconcolic: Testing and debugging deep neural networks’. In:
2019 IEEE/ACM 41st International Conference
on Software Engineering: Companion Proceedings(ICSE-Companion). (IEEE, 2019. pp. 111–114

8. The Acknowledges
This authors acknowledge funding from the JSTSPRING, Grant Number JPMJSP2132.

[7] Pei, K., Cao, Y., Yang, J., Jana, S. ‘Deepxplore:
Automated whitebox testing of deep learning systems’. In: proceedings of the 26th Symposium on
Operating Systems Principles. (, 2017. pp. 1–18

References[1] Katz, G., Barrett, C., Dill, D.L., Julian, K.,
Kochenderfer, M.J.
‘Reluplex: An eﬃcient
smt solver for verifying deep neural networks’.

[8] Goodfellow, I.J., Shlens, J., Szegedy, C.: ‘Explaining and harnessing adversarial examples’, stat,
2015, 1050, pp. 20

49

SEA

ソフトウェア・シンポジウム 2023 in 仙台[9] Liu, S. ‘Testing-based formal veriﬁcation for theorems and its application in software speciﬁcation
veriﬁcation’. In: Tests and Proofs: 10th International Conference, TAP 2016, Held as Part of
STAF 2016, Vienna, Austria, July 5-7, 2016, Proceedings 10. (Springer, 2016. pp. 112–129[18] Gehr, T., Mirman, M., Drachsler.Cohen, D.,
Tsankov, P., Chaudhuri, S., Vechev, M. ‘Ai2:
Safety and robustness certiﬁcation of neural networks with abstract interpretation’. In: 2018
IEEE symposium on security and privacy (SP).
(IEEE, 2018. pp. 3–18

[10] Wang, R., Liu, S., Sato, Y.: ‘Sit-se: aspeciﬁcation-based incremental testing methodwith symbolic execution’, IEEE Transactions on
Reliability, 2021, 70, (3), pp. 1053–1070[19] Ehlers, R. ‘Formal veriﬁcation of piece-wise linear feed-forward neural networks’. In: AutomatedTechnology for Veriﬁcation and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings 15. (Springer,
2017. pp. 269–286[11] Liu, A., Liu, S.: ‘Enhancing the capability of
testing-based formal veriﬁcation by handling operations in software packages’, IEEE Transactions
on Software Engineering, 2022, 49, (1), pp. 304–
324

[20] Ignatiev, A., Narodytska, N., Marques.Silva, J.
‘Abduction-based explanations for machine learning models’. In: Proceedings of the AAAI Conference on Artiﬁcial Intelligence. vol. 33. (, 2019.
pp. 1511–1519[12] Pratt, V.R. ‘Semantical considerations on ﬂoydhoare logic’. In: 17th Annual Symposium on Foundations of Computer Science (sfcs 1976). (IEEE,
1976. pp. 109–121[21] Calegari, R., Ciatto, G., Omicini, A.: ‘On the integration of symbolic and sub-symbolic techniques
for xai: A survey’, Intelligenza Artiﬁciale, 2020,
14, (1), pp. 7–32

[13] Ribeiro, M.T., Singh, S., Guestrin, C. ‘” whyshould i trust you?” explaining the predictions of
any classiﬁer’. In: Proceedings of the 22nd ACM
SIGKDD international conference on knowledge
discovery and data mining. (, 2016. pp. 1135–1144[14] Ribeiro, M.T., Singh, S., Guestrin, C. ‘Anchors:
High-precision model-agnostic explanations’. In:
Proceedings of the AAAI conference on artiﬁcial
intelligence. vol. 32. (, 2018.
[15] Lundberg, S.M., Lee, S.I.: ‘A uniﬁed approach tointerpreting model predictions’, Advances in neural information processing systems, 2017, 30[16] Smilkov, D., Thorat, N., Kim, B., Viégas, F.,
Wattenberg, M.: ‘Smoothgrad: removing noise
by adding noise’, arXiv preprint arXiv:170603825,
2017,[17] Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana,S.: ‘Eﬃcient formal safety analysis of neural networks’, Advances in neural information processing
systems, 2018, 31

50

SEA