On Challenges and Opportunities in the Translation of Deep Neural Networks into Finite Automata

Abstract

The certification of safety properties and interpretation of neural networks is a topic of great concern. We recently devised an automata-based approach for addressing these tasks. It translates a neural network with ReLU activations into a finite automaton, capturing the input-output relation induced by the neural network. We report on a proof-of-concept implementation of this translation for a subclass neural networks, so called binarized neural networks, pointing out dificulties and opportunities of the proposed approach.

Keywords

• eol>Neural Networks
• Finite Automata
• Verification and Interpretation

1. Introduction

2. Preliminaries

at any node is the ReLU function relu(x) = max(0, x). same input dimension. A DNN is a sequence of layers 1, . . . , such that for all , +1 the input dimension of nodes in +1 is equal to the size of . The function computed by is given by (− 1(. . . 1() . . .)). In this work, we only consider DNN in which the activation function Let Σ be a finite alphabet. We denote the

multi-track alphabet consisting of -vectors of symbols from Σ by Σ. A multi-track (nondeterminstic) finite automata (NFA) is defined as a usual NFA with transitions over some Σ. Similarly, the language of such a multi-track NFA is defined as usual. In the remainder of this paper the term NFA refers to such multi-track NFA over a number of tracks , which is clear from the context.

3. From Deep Neural Networks to NFA over Multi-Track Words

example, the vector (− 3.725, 9.125) is represented by Let be some DNN computing R

→ R, defining the relation = {(, ) | ∈ R, = ()} of all its input-output pairs. Now, [ 1 ] presents a construction of a finite automaton over a multi-track alphabet Σ+ such that the language ( ) of captures in the sense that each word in ( ) can be decoded into a pair (, ) ∈ and each such pair of can be encoded into a word ∈ ( ). An obvious way to encode a tuple (, ) as a word over some Σ+ is based on the usual binary encoding, leading to the use of automata over infinite words. It can be observed that weak nondeterministic Büchi automata sufice [ function over (Z∖2)

→ (Z∖2) where (Z∖2) are the dyadic rational numbers, which are exactly those that have a finite binary representation. Furthermore, we assume that all weights and biases used in are also from (Z∖2).1 Then, we can represent each (, ) using a finite word over Σ+ with Σ = {+, − , 0, 1, .}, used henceforth for the remainder of this article. For = − ︂[ ]︂ [︂ 0 ︂] [︂ 0 ︂] [︂ 1 ︂] [︂ 1 ︂] [︂ .︂] [︂ 1 ︂] [︂ 1 ︂] [︂ 0

︂] + 1 0 0 1 .

0 0 1 .

We denote the function mapping such a multi-track word to the unambiguous vector of values from (Z∖2) by dec. Then, one of the core results of [ 1 ] transfers easily.

Theorem 1. Let be a DNN with input dimension and output dimension . There is NFA s.t. ( ) = { ∈ (Σ+)* | (dec(1), . . . , dec()) = (dec(+1), . . . , dec(+))}. Proof sketch. First observe that a DNN-node computes its output using four basic operations: 1. addition of two values; 2. multiplication of a value with a fixed constant; 3. addition of a value with a constant; and 4. the application of the ReLU function. The relation of value triples and tuples induced by each of these operations can be recognized by an NFA. We refer to [ 1 ] for details with the indication that the constructions are similar for our setting. An example of an NFA recognising the addition relation is given in Figure 1. Second, observe that we can combine these NFA using join and projection operations on single tracks to build an NFA recognising the 1This restriction is no limitation considering the presumed applications of this translation, namely the verification and interpretation of DNN used in practice. There DNN necessarily contain and work over finitely representable parameters and values.

+ ⎡0⎤⎡0⎤⎡1⎤ ⎡0⎤ ⎣0⎦,⎣1⎦,⎣01⎦ ⎣0⎦ 0 1 1 ⎡1⎤ ⎣1⎦ 0 input-output relation defined by a DNN-node. Then, we use the same operations to establish an inductive procedure to generate an NFA recognising the input-output relation defined by a DNN. This is possible due to the inductive structure of DNN as indicated in Sect. 2. Again, see [ 1 ] for details.

4. A Proof-of-Concept Implementation

We present a proof-of-concept implementation, translating so called Binarized Neural Networks (BNN), into input-output equivalent NFA as discussed in Sect. 3. The BNN model [ 5 ] evolved as a simple but powerful neural network model, defined similar to DNN but with weights and bias restricted to +1 and − 1. It was shown, that BNN nearly achieve state-of-the-art performances in comparison to standard DNN [ 6 ].

The code is written in Python.2 The construction of an NFA for a given BNN conceptually follows the inductive construction described in Sect. 3 but uses two optimisations: first, we represent transition labels symbolically. Consider the NFA for addition in Fig. 1. It is notable that transitions are invariant under permutations of the labels in tracks one and two. This is not surprising as addition is commutative. Consequently, the transition labels in these automata can be stored symbolically as a pair (, ) with ∈ {0, 1} representing the resulting bit in the addition, and ∈ N representing the number of 1-bits in the tracks to be added up. Second, we use minimisation. After each construction that may create a non-minimal automaton, explicit minimisation is employed. Since NFA minimisation is PSPACE-hard in general, we use bisimulation quotienting instead. It may not produce minimal automata but it can be done in low polynomial time [ 7 ], and it typically yields good results in practice [ 8 ].

As benchmarks we use semi-randomly generated BNN: the input size is 1, the output size of the BNN is 1 and all layers in between consist of 2 nodes. We denote such BNN with BNNfix . The parameters (weights and bias) of the considered BNNfix were chosen uniformly from {− 1, 1}. The benchmarks were computed on an Apple M1 Pro CPU with 32GB RAM. In the first part, we run our translation without intermediate minimisation steps for BNNfix as specified above with 1 to 5 layers. The results are presented in the left chart of Fig. 2. The number of layers is plotted 2Available via https://github.com/marcosaelzer/NN2NFA on the horizontal axis and the runtime, number of states/transitions on the two logarithmically scaled vertical axes. The exponential blowup is clearly indicated by the linear interpolations of the three data series, even for these relatively shallow BNNfix . The fluctuations are due to the varying amount of − 1 and 1 parameters. In the right chart of Fig. 2 we see the efect of minimisation. We considered 5 randomly generated BNNfix with 4 layers. The chart depicts the percentage of reduction of the state set due to minimisation. The state size reduction is >80%, which indicates that our construction leads to an enormous amount of redundant states.

5. Discussion and Outlook

We presented a proof-of-concept implementation of the translation from DNN into finite automata, here NFA over multi-track words, as introduced in [ 1 ]. The translation is exponential, necessarily so since it reduces NP-hard DNN-reachability [ 9 ] to the NLOGSPACE problem for emptiness of (weak) NBA. Unsurprisingly, this blow-up is visible in the benchmarks. In order to achieve manageable runtimes, we focused our implementation on BNN of small size. There are two takeaways from this restriction: first, the maximum representation size of a parameter in the original DNN is crucial for the performance of the translation and, second, the inductive approach presented in [ 1 ] leads to many redundant states as indicated by the high amount of reduction achieved by minimising the NFA in intermediate steps. This opens a clear path for future work. The presumed applications of the DNN to NFA translation, namely vericfiation and interpretation of DNN, are clearly tailored for DNN with parameters of small size, for example Quantized Neural Networks [ 10 ]. Furthermore, the inductive translation approach seems intractable, due to the amount of redundant states generated and, thus, future work must focus on establishing a translation of a more direct manner.

References

[1] M. Sälzer , E. Alsmann , F. Bruse , M. Lange , Verifying and interpreting neural networks using finite automata , 2022 . arXiv: 2211 . 01022 .

[2] X. Huang , D. Kroening , W. Ruan , J. Sharp , Y. Sun , E. Thamo, M. Wu , X. Yi , A survey of safety and trustworthiness of deep neural networks: Vericfiation, testing, adversarial attack and defence, and interpretability , Comput. Sci. Rev . 37 ( 2020 ) 100270 . doi: 10 .1016/ j.cosrev. 2020 . 100270 .

[3] P. Barceló , M. Monet , J. Pérez , B. Subercaseaux , Model interpretability through the lens of computational complexity , in: Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020 , NeurIPS 2020 , December 6- 12 , 2020 , virtual, 2020 . URL: https://proceedings.neurips.cc/paper/2020/hash/ b1adda14824f50ef24f1c05bb66faf3-Abstract.html.

[4] B. Boigelot , S. Rassart , P. Wolper , On the expressiveness of real and integer arithmetic automata (extended abstract) , in: Automata, Languages and Programming , 25th International Colloquium, ICALP'98, Aalborg , Denmark, July 13-17 , 1998 , Proceedings, volume 1443 of Lecture Notes in Computer Science, Springer, 1998 , pp. 152 - 163 . doi: 10 .1007/BFb0055049.

[5] I. Hubara , M. Courbariaux , D. Soudry , R. El-Yaniv , Y. Bengio , Binarized neural networks , in: Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016 , December 5- 10 , 2016 , Barcelona, Spain, 2016 , pp. 4107 - 4115 . URL: https://proceedings.neurips.cc/paper/2016/ hash/d8330f857a17c53d217014ee776bfd50-Abstract.html.

[6] I. Hubara , M. Courbariaux , D. Soudry , R. El-Yaniv , Y. Bengio , Quantized neural networks: Training neural networks with low precision weights and activations , Journal of Machine Learning Research 18 ( 2018 ) 1 - 30 . URL: http://jmlr.org/papers/v18/ 16 - 456 .html.

[7] R. Paige , R. Tarjan , Three partition refinement algorithms , SIAM Journal on Computing 16 ( 1987 ) 973 - 989 .

[8] J. Högberg , A. Maletti , J. May, Backward and forward bisimulation minimization of tree automata , Theoretical Computer Science 410 ( 2009 ) 3539 - 3552 . doi:https://doi.org/ 10.1016/j.tcs. 2009 . 03 .022, implementation and Application of Automata (CIAA 2007 ).

[9] M. Sälzer , M. Lange , Reachability is NP-complete even for the simplest neural networks , in: Proc. 15th Int. Conf. on Reachability Problems , RP' 21 , volume 13035 of LNCS , Springer, 2021 , pp. 149 - 164 . doi: 10 .1007/978-3- 030 -89716-1\_ 10 .

[10] T. Liang , J. Glossner , L. Wang , S. Shi , X. Zhang, Pruning and quantization for deep neural network acceleration: A survey , Neurocomputing 461 ( 2021 ) 370 - 403 . URL: https: //doi.org/10.1016/j.neucom. 2021 . 07 .045. doi: 10 .1016/j.neucom. 2021 . 07 .045.