Neural network with Linear and ReLU nodes can be represented as sequential linear programs that are simple in structure but have many program paths: diferent combinations of ReLU activations correspond to paths in the corresponding program. Naive applications of conventional program analysis techniques for proving properties of such networks are hampered by the expontential number of activation patterns (i.e., program paths). In this paper, we explore a technique for scaling verification by decomposing the verification task into first finding feasible paths and then proving properties for individual paths, resulting in multiple small verification tasks (compared to monolithic analysis of the network). Moreover, this enables horizontal scaling, i.e., parallel execution, further decreasing analysis time. Finally, the proposed decomposition allows us to reuse a once computed set of feasible paths for the verfication of multiple properties, compounding performance gains when checking multiple properties on the same network.
(a) Minimal Example Network fun id(x : Double) : Double = x fun relu(x : Double) : Double =
if(x > 0) x else 0.0 val l11=id(i1*-0.64+i1*-0.02+i3*-0.63) val l12=id(i1*0.61+i1*0.35+i3*-0.37) val r21=relu(l11 * 0.43) val r22=relu(l12 * 0.14) (b) Implementation of the first and second layer in network of Figure 1a.
Related Work. Proving properties about neural networks is called neural network verification
[
In this work, we apply precise software verification techniques to neural networks. Concrretely, we use dynamic symbolic execution [13] to enumerate a network’s paths. The same technique is used to analyze the taint flow of programs [ 14, 15] or to enhance static analyses [16, 17] and has been shown to scale well to complex programs [18]. Schlüter et al. used symbolic execution to generate TADS to check network equivalence and explainability [19]. A unique benefit of this approach is that we produce an intermediate result that can be re-used and is much less complex than the original network (from the perspective of a verifier).
The size and concurrent activation pattern of neural networks can make them hard to understand. This computation model is not well suited for classical program analysis. We show this by example and transform a small neural network into a program’s linear representation. Figure 1a shows the ReLU network. It consists of four layers (including the output layer): three linear layers and a single ReLU layer. We assume, but without loss of generality, that ReLU neurons only have a single input.
We transform ReLU networks into a program that uses only multiplication, addition and function calls. For the above network’s layers one and two and their activation functions result in the code from Figure 1b: We multiply the vector of weights with the input and pass the result to the activation function. The name of every neuron consists of its activation function, its layer, and its position in this layer.
We can now apply dynamic symbolic execution (DSE) to the network. Symbolic execution replaces concrete values with symbolic values. The branching operators (if, while, etc.) decide which paths to follow by checking satisfiability of path constraints collected during execution. This may result in multiple branches being feasable and hence being followed. DSE consequently enumerates all feasible (i.e., satisfiable) paths through a program, filtering paths as soon as they become unsatisfiable (each unsatisfiable path prefix leads to the root of an unsatisfiable sub-tree of paths), and resulting in few additional queries to a constraint solver for many unsatisfiable paths. Figure 2 shows all paths through the code in Figure 1b. Notice that all combinations of assignments for the two ReLUs are possible1 and on diferent paths. A path becomes unsatisfiable if no input can fulfill the path constraints. Take for example a network with a single input and two ReLU nodes with weights and − . Only one of those nodes can be positive at a time and hence, the path where both activate positively is unsatisfiable. Whenever we talk about the paths of a neural network, we refer to the paths of the program into which we translated a neural network.
Algorithm 1 Enumerating all satisfiable paths and checking satisfiability after a layer is added.
← the paths including the first layer 1. for every ∈ 2 · · · do ← ∅ for every satisfiable ∈ × do
Add to end for ← end for return
Algorithm 2 Verification of over all satisfiable paths - Safety ← ⊤ for Every path ∈ do
← ∧ ∧ ¬ is unsatisfiable end for return A neural network corresponds to a set of program paths , divided into satisfiable ( ) and unsatisfiable ( ) paths: ∪ = with ∩ = ∅. We decompose the verification of some property on , i.e., checking if |= , into checking on all paths, i.e., |= for ∀ ∈ 1When we say “possible”, we are not saying they are all executable at runtime. Some paths may have an unsatisfiable path constraint. “Possible” here refers to the syntactic category. When we try to restrict this set to executable paths, we refer to them as satifiable. (Algorithm 2). To this end, we have to first compute . Here, we optimize the runtime by varying when we check for satisfiability of path prefixes in a breath-first exploration of all paths. Assume paths , 1, 2 with path constraints , 1, 2 respectively, such that = 12, and = 1 ∧ 2. If 1 is unsatisfiable, is also unsatisfiable and need not be explored. Thus, checking path constraints sooner, e.g. after 1 instead of after , reduces the number of path constraints to check for satisfiability. Checking path constraints after each layer (Algorithm 1) resulted in the best trade-of between runtime and potential for parallelization in our tests.
We demonstrate our approach by analyzing properties of two networks: we use neural network N1 (19 ReLUs) to analyze performance of mutiple path enumeration strategies and network N2 (38 ReLUs) to compare verification against two monolithic approaches. 2
Table 1 summarizes all results: Filtering unsatisfiable paths makes the approach tractable. Enumerating all paths and checking their path constraints afterward, was infeasible for 524 288 = 219 paths. Parallel layer-wise path enumeration was the optimal strategy. For the verification of a simple assertion on outputs , we use monolithic verification with MathSAT and Z3 as a baseline comparisons. MathSAT, a solver optimized for linear arithmetics, can solve the verification task in 43 minutes. The popular 3 SMT solver needs more than five days. Our approach needs (in a very unoptimized implementation) 15 hours for enumerating all satisfiable paths and 5 minutes and 25 seconds for checking the property on these paths. This makes us confident, that with further optimization of the implementation, the approach will pay of when multiple properties have to be checked.
As next steps, we plan to thoroughly evaluate and compare scalability to diferent sizes of networks and types of properties. We also plan to explore extending the technique to back-feeding neural networks and more activation functions. Ultimately, we are interested in definitions of properties that are of interest for neural networks. 2The hardware was a research server: Common KVM processor with 72 processors and 135 GB memory running Linux 5.4.0-125-generic. The SMT-Solver was z3 (https://github.com/Z3Prover/z3) in Version 4.11.0.
This research is partially funded by the German Federal Ministry of Education and Research (BMBF) within the Data Trust Models Funding Action (16DTM106A). The authors are responsible for the content of this publication. This work was also supported by the Research Center Trustworthy Data Science and Security, an institution of the University Alliance Ruhr. ence on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, 2020. [13] J. C. King, Symbolic execution and program testing, Commun. ACM 19 (1976) 385–394.
doi:10.1145/360248.360252. [14] M. Mues, T. Schallau, F. Howar, Jaint: A framework for user-denfied dynamic taint-analyses based on dynamic symbolic execution of java programs, in: B. Dongol, E. Troubitsyna (Eds.), Integrated Formal Methods, Springer International Publishing, Cham, 2020, pp. 123–140. [15] E. J. Schwartz, T. Avgerinos, D. Brumley, All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask), in: Proceedings of the 2010 IEEE Symposium on Security and Privacy, SP ’10, IEEE Computer Society, USA, 2010, p. 317–331. doi:10.1109/SP.2010.26. [16] T. Avgerinos, A. Rebert, S. K. Cha, D. Brumley, Enhancing symbolic execution with veritesting, in: Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, Association for Computing Machinery, New York, NY, USA, 2014, p. 1083–1094. doi:10.1145/2568225.2568293. [17] Y. P. Khoo, B.-Y. E. Chang, J. S. Foster, Mixing type checking and symbolic execution,
SIGPLAN Not. 45 (2010) 436–447. doi:10.1145/1809028.1806645. [18] P. Godefroid, M. Y. Levin, D. A. Molnar, SAGE: whitebox fuzzing for security testing, Commun. ACM 55 (2012) 40–44. URL: https://doi.org/10.1145/2093548.2093564. doi:10. 1145/2093548.2093564. [19] M. Schlüter, G. Nolte, A. Murtovi, S. Bernhard, Towards rigorous understanding of neural networks via semantics-preserving transformations, International Journal on Software Tools for Technology Transfer (2022). To appear.