arXiv:2604.25733v1 [cs.LO] 28 Apr 2026
Verification of Neural Networks Lecture Notes
Benedikt Bollig Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF Gif-sur-Yvette, France
Preface These lecture notes provide an introduction to the verification of neural networks from a theoretical perspective. We discuss feed-forward neural networks, recurrent neural networks, attention mechanisms, and transformers, together with specification languages and algorithmic verification techniques. They are based on a lecture series given in the academic year 2023/2024 as part of the MPRI 2.8 course “Advanced Techniques of Verification”. I thank the students of the course for their questions and comments during the lectures, which helped improve the presentation of the material. The neural-network drawings presented in Sections 3.1 and 3.2 are adapted from Izaak Neutelings [37], available at tikz.net, and used under the CC BY-SA 4.0 license. All other figures are original unless stated otherwise. Any comments, suggestions, errata, etc. are very welcome. Please send them by email to [email protected].
2
Contents 1 Introduction
4
2 Preliminaries 2.1 Sets, Functions, Vectors, Matrices . . . . . . . . . . . . . . . . . . . . . . 2.2 Languages and Büchi Automata . . . . . . . . . . . . . . . . . . . . . . .
6 6 7
3 Feed-Forward Neural Networks 3.1 Definition of Neural Networks . . . . . . . . . . . . . . . . . . . . . . . . 3.2 A Specification Language for Neural Networks . . . . . . . . . . . . . . . 3.3 Proof of Decidability of LRA . . . . . . . . . . . . . . . . . . . . . . . . . 3.4 An Efficiently Solvable Fragment of NNL . . . . . . . . . . . . . . . . . . 3.5 Beyond ReLU Neural Networks . . . . . . . . . . . . . . . . . . . . . . .
10 10 14 23 32 38
4 Recurrent Neural Networks 4.1 Definition and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2 Undecidability of the Emptiness Problem . . . . . . . . . . . . . . . . . .
42 42 45
5 Attention and Transformers 5.1 Attention . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 The Transformer Architecture . . . . . . . . . . . . . . . . . . . . . . . . 5.3 Encoder-Only Transformers . . . . . . . . . . . . . . . . . . . . . . . . .
54 54 57 61
3
Chapter 1 Introduction AI-based systems, particularly neural networks, are playing an important role in our daily lives. Neural networks are used for image and speech recognition, in autonomous cars, medical diagnostics, anomaly detection, financial and weather forecasting, etc. As they are increasingly used in safety-critical applications (e.g., in autonomous cars or medical diagnostics), there are of course high safety requirements for AI-based components. However, neural networks are black-box models with a rather opaque structure where small changes can have significant effects. Another reason to ask: Can we give formal guarantees for a given neural network? Or, in other words, can we verify a neural network? Formal methods are well-suited to provide answers here. They include techniques that first mathematically model systems and requirements specifications and then algorithmically determine the compatibility of system and specification. Formal methods are often associated with verifying systems written in some programming language. Now, neural networks are not a program in this sense (they are written or trained by a machine). However, like “programs,” they follow a precise sequence of instructions and are, in principle, amenable to formal verification. While the specification of programs is often natural (think of terms like termination or deadlock freedom), it may appear unclear what correctness means for neural networks. For example, when is an image classifier that is supposed to classify animals correct? Probably, when it recognizes a dog as such, a cat as a cat, and so on. But to apply formal methods, we must formalize correctness in a precise mathematical sense. Now, to write down when a picture represents a dog and when a cat, is naturally incredibly challenging. And if we could, we probably would not need a neural network anymore. But there are many other desirable properties that we can formalize. For example, when an image classifier is robust, that is, when small changes in a given image do not entirely change the classification. Or when a neural network is fair, that is, when it does not take sensitive features into account in order to assign credits or jobs. Neural networks often serve as building blocks of larger systems and may act as a controller, i.e., choose an action to be performed in a given state. We are then in the setting of reactive systems. Verifying them is particularly challenging, as specifications usually combine temporal properties with arithmetic expressions such as “whenever a system variable x reaches a critical threshold γ, i.e., x ≥ γ, then there is a time point in the near future when it falls back below the threshold, i.e., x < γ.” 4
Introduction Applying formal methods to neural networks is an exciting new field with many interesting developments. We refer here to various survey papers and lecture notes [2, 8, 30, 53, 57] that we recommend for further reading. We do not aim to provide optimal algorithms. The goal of this lecture is to give a sense of what verification of a neural network means and to explore its theoretical possibilities and limitations. However, one should remember that scalability is an essential criterion for verification methods for neural networks, which can have millions of parameters.
5
Chapter 2 Preliminaries In this chapter, we recall some standard concepts from linear algebra and automata theory. Linear algebra allows one to describe neural networks in a compact, elegant manner. We will use automata-based techniques (among others) to address their verification.
2.1
Sets, Functions, Vectors, Matrices
Sets and Functions. By N = {0, 1, 2, . . .}, we denote the set of natural numbers, and by N+ = {1, 2, . . .} the set of positive natural numbers. The set of real numbers is denoted R, and the set of rational numbers by Q. As part of an input to a decision problem or of an object like a matrix, we implicitly assume that a rational number is effectively given in terms of binary encodings of its numerator and denominator. For x, y ∈ R, we let [x, y] = {z ∈ R | x ≤ z ≤ y}, (x, y] = {z ∈ R | x < z ≤ y}, and so forth. For functions f : A → B and g : B → C, we denote by g ◦ f : A → C the composition of f and g, defined by (g ◦ f )(a) = g(f (a)) for all a ∈ A. Moreover, given A′ ⊆ A, we let f A′ : A′ → B denote the restriction of f to the domain A′ . For a finite set A, the number of elements in A is denoted by |A|. Vectors and Matrices. Let m, n ∈ N+ . For a vector x ∈ Rn and i ∈ {1, . . . , n}, we let xi refer to the i-th component of x, i.e., x = (x1 , . . . , xn )⊤ . If n = 1, we may simply write x for x. Similarly, y = (y1 , . . . , yn )⊤ , x′ = (x′1 , . . . , x′n )⊤ , and so on. Moreover, for a matrix A ∈ Rn×m , i ∈ {1, . . . , n}, and j ∈ {1, . . . , m}, we let ai,j refer to the element of A in the i-th row and j-th column, i.e., a1,1 a1,2 . . . a1,m a2,1 a2,2 . . . a2,m n×m A = .. . .. .. ∈ R . . . . . . an,1 an,2 . . . an,m Similarly, A′ = a′i,j i,j and so forth. For f = (f1 , . . . , fm ) with f1 , . . . , fm : R → R and x ∈ Rm , we define f (x) = (f1 (x1 ), . . . , fm (xm ))⊤ ∈ Rm . 6
Preliminaries
□□
□□
The vertical concatenation of matrices A ∈ Rm×n and B ∈ Rk×n is defined by A B = C ∈ R(m+k)×n where ci,j = ai,j for all i ∈ {1, . . . , m} and j ∈ {1, . . . , n}, and ci,j = bi−m,j for all i ∈ {m + 1, . . . , m + k} and j ∈ {1, . . . , n}. The horizontal concatenation of A ∈ Rm×n and B ∈ Rm×k is defined accordingly by A □□ B = C ∈ Rm×(n+k) where ci,j = ai,j for all i ∈ {1, . . . , m} and j ∈ {1, . . . , n}, and ci,j = bi,j−n for all i ∈ {1, . . . , m} and j ∈ {n+1, . . . , n+k}. The special case of vectors is defined analogously. In particular, the vertical concatenation of x ∈ Rm and y ∈ Rn is x y = (x1 , . . . , xm , y1 , . . . , yn )⊤ ∈ Rm+n . For a given m ∈ N+ (which we suppose to be clear from the context), we let ( Rm → 2{1,...,m} argmax : x 7→ {i ∈ {1, . . . , m} | xi = max(x)} .
For m ∈ N+ , the set of permutations π : {1, . . . , m} → {1, . . . , m} is denoted Sm . We extend π to π : Rm → Rm letting π(x) = (xπ(1) , . . . , xπ(m) ). This convention reads the coordinates of x in the order π(1), . . . , π(m); using the inverse convention would give equivalent definitions below after renaming the permutation. Below we define two properties that play an important role in the realm of neural networks: Definition 2.1: Permutation Equivariance and Invariance Let m ∈ N+ and A be a set.
– A function f : Rm → A is called permutation invariant if, for all x ∈ Rm and π ∈ Sm , we have f (x) = f (π(x)).
– A function f : Rm → Rm is called permutation equivariant if, for all x ∈ Rm and π ∈ Sm , we have f (π(x)) = π(f (x)).
2.2
Languages and Büchi Automata
Automata are a useful tool in verification and for deciding arithmetic theories such as Presburger arithmetic and linear real arithmetic [18]. In this course, we will need to decide linear real arithmetic and, to do so, rely on Büchi automata, which are devices that run over infinite words (or strings). Later on, these infinite words will represent real numbers. An alphabet is a nonempty set (possibly infinite). Let Σ be an alphabet. A finite word over Σ of length n ∈ N is a finite sequence w = u1 . . . un with u1 , . . . , un ∈ Σ. We denote the length n of w by |w|. If n = 0, then w is the empty word, denoted by ε. An infinite word over Σ is a countably infinite sequence w = u1 u2 u3 . . . with u1 , u2 , . . . ∈ Σ. The set of finite words over Σ is denoted by Σ∗ , the set of nonempty finite words over Σ by Σ+ (i.e., Σ+ = Σ∗ \ {ε}), and the set of infinite words by Σω . We will often deal with mappings of the form δ : Q × Σ → Q where Q is a (possibly infinite) set. This mapping can be inductively extended to δ̂ : Q × Σ∗ → Q letting δ̂(q, ε) = q and, for w ∈ Σ∗ and u ∈ Σ, δ̂(q, w · u) = δ(δ̂(q, w), u). Abusing notation, we usually still write δ instead of δ̂. 7
Preliminaries In the remainder of this section, we consider finite alphabets. Definition 2.2: Büchi Automaton Let Σ be a finite alphabet. A Büchi automaton over Σ is a tuple A = (Q, ∆, ι, F ) where – Q is a finite set of states, – ∆ ⊆ Q × Σ × Q is the set of transitions – ι ∈ Q is the initial state, and – F ⊆ Q is the set of final states. Büchi automaton A recognizes a language L(A) ⊆ Σω as follows. A run of A is an infinite sequence ρ = q0 u1 q1 u2 q2 . . . ∈ Q(ΣQ)ω such that q0 = ι and, for all i ∈ N+ , (qi−1 , ui , qi ) ∈ ∆. The label of ρ is defined as label (ρ) = u1 u2 u3 . . . ∈ Σω . Run ρ is called accepting if it sees some final state infinitely often, i.e., the set {i ∈ N | qi ∈ F } is infinite. Finally, the language recognized by A is defined by L(A) = {label (ρ) | ρ is an accepting run of A} ⊆ Σω .
Example 2.1: The figure below depicts a Büchi automaton A = (Q, ∆, ι, F ) over the alphabet Σ = {0, 1}. We have Q = {q0 , q1 }, ι = q0 , and F = {q1 }. The set of transitions ∆ includes (q0 , 0, q0 ), (q0 , 1, q1 ), etc. The language L(A) is the set of words from Σω in which letter 1 occurs infinitely often. 0
1 1
q0
q1 0
Büchi automata enjoy several useful closure and decidability properties: 1
2
α3 α3 Theorem 2.1: Closure Properties of Büchi Automata 2 α3
β
Let Σ be a finite alphabet and let A, A1 , A2 be Büchi automata over Σ. We can q2 1 effectively construct a Büchi qautomaton (a) A1 ∪ A2 over Σ such that L(A α 131 ∪ A2β) = L(A1 ) ∪ L(A2 ); (b) A1 ∩ A2 over Σ such that L(A1 ∩ A2 ) = L(A1 ) ∩ L(A2 ); (c) A over Σ such that L(A) = Σω \ L(A).
8
Preliminaries Theorem 2.2: Büchi Automata Emptiness The following problem is decidable: Input: A finite alphabet Σ and a Büchi automaton over Σ. Question: Is L(A) nonempty? The complexity is linear in the number of states and transitions. For more background on languages and automata, we refer the reader to [51].
9
Chapter 3 Feed-Forward Neural Networks In this chapter, we define feed-forward neural networks and their verification problem. We also present a specification language for neural networks. It is based on linear real arithmetic, which encompasses, as we will see, many pertinent properties of neural networks.
3.1
Definition of Neural Networks
A neural network is a stack of layers. Every layer transforms an input vector into an output vector. The more layers we have, the deeper is the network. In practice, the term deep learning is used when several such transformations are composed. A layer and its computation are depicted in Figure 3.1. It consists of m input nodes and n output nodes, and it maps an input vector x = (x1 , . . . , xm )⊤ ∈ Rm to an output vector y = (y1 , .P . . , yn )⊤ ∈ Rn . Here, intermediate values zi are computed as a linear combination bi + j ai,j · xj . Thus, the transformation induced by a layer can be written in terms of matrix multiplications. Definition 3.1: Layer Let m, n ∈ N+ . A feed-forward layer with input dimension m and output dimension n is a triple L = (A, b, f ) where A ∈ Qn×m is the weight matrix, b ∈ Qn is the bias vector, and f : Rn → Rn is the activation function. We let in(L ) = m denote the input dimension of L . Moreover, out(L ) = n is the output dimension, which is usually referred to as the number of neurons of L . In other words, the weights of the i-th output neuron are given by the i-th row of A. We also let dim(L ) = (m, n) (note the difference from the dimension of the matrix A). Layer L defines the function ( Rin(L ) → Rout(L ) JL K : x 7→ f (A · x + b) . Let us turn to neural networks. A (feed-forward) neural network is a sequence of feedforward layers such that neighboring layers have compatible input/output dimensions. The idea is that the output of one layer is the input to the next layer. Thus, the function 10
Feed-Forward Neural Networks
x1
+b1
a1,1 a1,2
x2
z1
a1,3 a1,4
z2
x3 a1,m
z3
.. .
x4
.. .
z1 a1,1 a1,2 z a2,1 a2,2 2 . = .. .. .. . . a a zn n,1 n,2 z=A·x+b
x1 b1 . . . a1,m . . . a2,m x2 b2 .. .. + .. .. . . . . . . . an,m xm bn
y = f (z)
zn
xm Figure 3.1: A neural network layer with activation function f : Rn → Rn input
hidden layers output layer
Figure 3.2: Structure of a neural network with 4 layers (+ 1 input layer) defined by a neural network is the composition of the functions defined by its layers. The neural network illustrated in Figure 3.2 consists of 4 layers (we omit weights and activation functions). Definition 3.2: Feed-forward Neural Network A feed-forward neural network is a sequence N = (L (1) , . . . , L (ℓ) ) of layers L (k) = (A(k) , b(k) , f (k) ) such that out(L (k) ) = in(L (k+1) ) for all k ∈ {1, . . . , ℓ − 1}. Since, in this chapter, we only talk about feed-forward neural networks (rather than recurrent neural networks or graph neural networks), we just say neural network. Note that, in the literature, the number of layers usually considers the collection of input values as a separate layer, which indeed makes sense when looking at the graph 11
Feed-Forward Neural Networks representation of a neural network (cf. Example 3.1). Thus, while N = (L (1) , . . . , L (ℓ) ) has ℓ layers, the “graph representation” exhibits ℓ + 1 layers. Similarly to a layer, in(N ) = in(L (1) ) is the input dimension, and out(N ) = out(L (ℓ) ) the output dimension of N . In addition, we let dim(N ) = (in(N ), out(N )). The neural network computes JN K : Rin(N ) → Rout(N ) defined as the function composition JN K = JL (ℓ) K ◦ . . . ◦ JL (1) K . We will switch between a graph representation and matrix view at discretion. Moreover, we will consider Rm and Rn as sets of vectors or sets of tuples whatever is more convenient. In particular, we may simply write JN K(x1 , . . . , xm ) = (y1 , . . . , yn ) instead of JN K((x1 , . . . , xm )⊤ ) = ((y1 , . . . , yn )⊤ ). (1)
(ℓ )
(1)
(ℓ )
Two neural networks N1 = (L1 , . . . , L1 1 ) and N2 = (L2 , . . . , L2 2 ) such that out(N1 ) = in(N2 ) can be concatenated, and we let (1)
(ℓ )
(1)
(ℓ )
N1 · N2 = (L1 , . . . , L1 1 , L2 , . . . , L2 2 ) . Note that dim(N1 · N2 ) = (in(N1 ), out(N2 )). Activation Functions. There are different types of activation functions used in practice. They usually depend on the concrete task at hand (e.g., classification vs. regression) and the type of the layer (internal vs. output layer), but also on training-related issues such as the choice of the loss function (a precise discussion is, however, not in the scope of this course). Often, a layer L = (A, b, f ) has a local activation function f in the following sense: There is g : R → R such that, for all x ∈ Rn , we have f (x) = (g(x1 ), . . . , g(xn ))⊤ . The definitions and graphs of some common local activation functions are given in Figure 3.3 (the activation function NLReLU was recently studied in [32]). Their extensions to Rn → Rn are denoted in the same way (σ, tanh, and ReLU), where we always assume that n is clear from the context. Another example of a local activation function is the identity function, which we denote by id : Rn → Rn (again assuming that n is understood). An instance of a global activation function is
softmax :
Rn → Rn
e xi x 7→ (y1 , . . . , yn ) where yi = Pn xj j=1 e
It “squeezes” or normalizes a vector so that it represents a probability distribution. It is, therefore, frequently used in classification tasks. An important class of neural networks employs ReLU activation functions (or the identity function, mostly in output layers): Definition 3.3: Standard and ReLU Neural Network A neural network N = (L (1) , . . . , L (ℓ) ) with layers L (k) = (A(k) , b(k) , f (k) ) is called a ReLU neural network if, for all k ∈ {1, . . . , ℓ}, we have f (k) ∈ {id, ReLU}.
12
Feed-Forward Neural Networks 3 ReLU NLReLU sigmoid (σ) tanh
ReLU(x) = max(0, x)
g(x)
2 NLReLU(x) = ln(1 + ReLU(x)) 1
1 σ(x) = 1 + e−x
tanh(x) =
ex − e−x ex + e−x
x −3
−2
−1
1
2
3
−1
Figure 3.3: (Local) activation functions given by g : R → R Classification vs. Regression. As far as feed-forward neural networks are concerned, two predominant classes of tasks are classification and regression. In a regression problem, the goal is to predict a continuous, numerical value or quantity. In other words, one is trying to find a relationship between input features and the output, which is a real-valued number. Corresponding tasks can be price prediction, weather forecast, or estimating health indicators. In a classification problem, objects are assigned a category or label among n labels. In that case, frequently, the last layer has output dimension n and uses a softmax activation function, which works well with the categorical cross-entropy loss function during training. When N acts as a classifier with JN K : Rm → Rn , element x ∈ Rm is assigned category min(argmax(JN K(x))) ∈ {1, . . . , n}. In the case of binary classification (i.e., in presence of two classes to choose from), it is also common to have n = 1 and σ as activation function in the last layer, and to choose one class or the other depending on whether JN K(x) ∈ [0, 1] exceeds a given threshold γ ∈ [0, 1]. In the case of binary classification, possible applications are object detection, fraud detection, medical diagnostics, etc. Example 3.1: Neural Networks Below are two simple neural networks: (a)
(b) ReLU
ReLU
1
x1
0.33
−1
x1
1 ReLU
1
1
−0.10
id
ReLU
0.84
1.13
x2
−1
0 −1
0.24 +0.07
0
x2
0.20
−1.03
ReLU
13
0.97
1.03
ReLU
id
Feed-Forward Neural Networks
(a) We have N = (L (1) , L (2) ) where L (k) = (A(k) , b(k) , f (k) ). Function f (1) is the ReLU activation function and f (2) is the identity. Moreover, we have b(1) = (0, 0, 0)⊤ , b(2) = (0), 1 −1 1 ∈ R3×2 , and A(2) = 1 1 −1 ∈ R1×3 . A(1) = 0 0 −1 Note that N computes the maximum function, i.e., JN K(x1 , x2 ) = max(x1 , x2 ) = max(x1 − x2 , 0) + x2 for all (x1 , x2 ) ∈ R2 .
(b) This neural network has the same structure and activation functions as in (a), but different weights: We have b(1) = (0, 0, 0)⊤ , b(2) = (0.07), 0.33 0.2 1.13 ∈ R3×2 , and A(2) = 0.24 0.84 0.97 ∈ R1×3 . A(1) = −0.1 1.03 −1.03
It is, however, less clear what N computes. For example, we have JN K(3, 2) = 3.049, JN K(4, 9) = 9.026, and JN K(4, 93) = 92.79.
The first neural network is taken from [19], where the authors study the question how many layers are needed to compute certain functions in a ReLU neural network.
Convolutional Neural Networks. Note that the neural networks that we defined above are fully connected: every neuron is connected to all neurons in the previous layer. In particular, all the weights/parameters in a weight matrix are, in principle, trainable and can be adjusted by the learning algorithm. There are other types of neural networks, such as convolutional neural networks (CNNs), that relax this condition. A CNN is illustrated in Figure 3.4. Certain neurons in CNNs share weights and they are sparse in the sense that some of the connections to preceding neurons are missing. A CNN can be captured in terms of our definition by setting the corresponding weights to 0. However, one should have in mind that, when considering training algorithms, one has to make a distinction between trainable parameters and those that cannot be modified. When defining neural networks as graphs, this is simple, as one would just omit the corresponding edges.
3.2
A Specification Language for Neural Networks
In this section, we will discuss what it means for a neural network to be correct. Here, we mean correctness in a strict mathematical sense. This, in turn, requires a formal specification to be given. Below are some examples of specifications. After discussing them, we will see a formal specification language that encompasses all of them. (a) JN K : Rm → R computes the maximum function.
(b) JN K : Rm → Rm implements a sorting algorithm. (c) JN K : Rm → Rn is permutation invariant. 14
Feed-Forward Neural Networks input
fully-connected hidden layers
convolutional layers
output layer
Figure 3.4: A convolutional neural network (CNN) (d) JN K : Rm → Rm is permutation equivariant.
(e) JN K : Rm → Rn such that, for given sets R ⊆ Rm and K ⊆ {1, . . . , m}, the following holds: for all x, x′ ∈ R satisfying xi = x′i for all i ∈ K, we have argmax(JN K(x)) = argmax(JN K(x′ )).
(f) JN K : Rm → Rn such that, for a given set R ⊆ Rm and ε > 0, the following holds: for all x ∈ R and x′ ∈ Rm such that ∥x, x′ ∥Manhattan ≤ ε, we have argmax(JN K(x)) = argmax(JN K(x′ )).1
(g) JN1 K, JN2 K : Rm → Rn such that, for a given set R ⊆ Rm , the following holds: for all x ∈ R, we have argmax(JN1 K(x)) = argmax(JN2 K(x)). Exercise 3.1: For all of the above properties, discuss whether they are typically relevant for machine-learning tasks and provide corresponding examples. Can you come up with other relevant specifications? Are there specifications that imply others? Solution: (a) Computing the maximum function is not a typical machine-learning task: it does not require learning from data to discover unknown or hidden patterns (though, in principle, the task can be addressed by learning a machinelearning model). (b) The same discussion as for (a) applies to the sorting problem. (c) Here, we aggregate multiple inputs into one or several values. Suppose every input value is the age of a particular person in a group of m people, and that the neural network makes a prediction on the number of votes that a particular candidate may receive in the upcoming election. The prediction should not depend on the order of the input values. In other words, permuting the 1
For x, x′ ∈ Rm , the Manhattan distance of x and x′ is defined as ∥x, x′ ∥Manhattan =
15
Pm
′ i=1 |xi − xi |.
Feed-Forward Neural Networks
input values should result in the same output value. (d) Similarly to the previous case, suppose that each input represents the probability of a medical staff member being infected, and the output determines, for every medical staff member, whether they should be tested or quarantined. Again, the decision per agent should not depend on the order of the input values. That is, permuting the input values should result in the same output values permuted. (e) Suppose the neural network takes features of a person as input, such as age, gender, salary, etc., and the neural network’s task is to decide whether a loan is granted. This decision should be independent of sensitive features like gender or ethnicity. Such a property is referred to as a fairness property. The property thus considers that the features in {1, . . . , m}\K are sensitive. (f) We can think of N as an image classifier. If R represents a set of images, e.g., the set the classifier was trained on, we would like N to be robust in the sense that small perturbations on the input images do not change the predictions. This would be particularly important when N is used in an autonomous car to detect traffic signs. (g) The formula states that neural networks N1 and N2 are equivalent on an input set R. That is, for every input in R, they yield the same index/class from {1, . . . , n}. Suppose that N2 is much smaller than N1 . If the property is satisfied, we could safely replace N1 with the more efficient neural network N2 . Exercise 3.2: Let n = 3. For each of the specifications (a) and (b), provide a neural network satisfying it. Exercise 3.3: Consider the neural networks from Example 3.1 and the properties (a)–(f) above. For every combination of a neural network N and a property φ, verify whether φ is a suitable specification for N (syntactically) and, if so, whether N satisfies φ. Can the two neural networks from the example be considered equivalent? And what would a corresponding specification look like? The formal specification language for neural networks will be based on linear real arithmetic, a decidable logic that allows one to combine logical connectives with linear expressions. It is defined over an infinite countable set of variables X = {x, y, x1 , x2 , . . .} that range over the real numbers.2
2
Note that we use x etc. to denote both real numbers and variables. Variables will be interpreted as real numbers so that denoting them in the same way makes sense. However, it is important to keep in mind that variables and real numbers are different objects.
16
Feed-Forward Neural Networks Definition 3.4: Linear Real Arithmetic Formulas from LRA (linear real arithmetic) are given by the following grammar: terms
t ::= a · x | b | t + t
formulas φ ::= t ≤ t | ¬φ | φ ∨ φ | ∃x.φ where x ∈ X and a, b ∈ Q. An occurrence of a variable is free in an LRA formula φ if it is not in the scope of a quantifier ∃/∀. A variable is called free in φ if it has some free occurrence in φ. Given a tuple of variables x = (x1 , . . . , xn ), we may write φ(x) or φ(x1 , . . . , xn ) for a formula φ whose free variables are among x1 , . . . , xn (though not all of them need to have a free occurrence). A sentence is a formula without free variables. We define some common abbreviations such as x for 1 · x, t1 = t2 for t1 ≤ t2 ∧ t2 ≤ t1 , t1 < t2 for t1 ≤ t2 ∧ ¬(t1 = t2 ), φ ∧ ψ for ¬(¬φ ∨ ¬ψ), φ ⇒ ψ for ¬φ ∨ ψ, φ ⇔ ψ for (φ ⇒ ψ) ∧ (ψ ⇒ φ), ∀x.φ for ¬∃x.¬φ, etc. We will also write ∃x1 , . . . , xn .φ instead of ∃x1 .∃x2 . . . . ∃xn .φ and so forth.
Moreover, for (tuples of) variables x, y = (y1 , . . . , yn ), y′ = (y1′ , . . . , yn′ ), and a set K ⊆ {1, . . . , n}, we define the following abbreviations: x∈y ≡
n _
x = yi
i=1
x = max(y) ≡ x ∈ y ∧ argmax(y) = K ≡ argmax(y) = argmax(y′ ) ≡
^
i∈K
n ^
i=1
yi ≤ x
yi = max(y) ∧ _
K ⊆ {1,...,n}
^
i∈{1,...,n}\K
¬(yi = max(y))
(argmax(y) = K ∧ argmax(y′ ) = K)
The latter definition takes into account that argmax returns the set of indices carrying the maximal value in a tuple/vector. Example 3.2: Consider the formulas φ1 (x, y) = x < y ⇒ ∃z.(x < z ∧ z < y) φ2 (x, y) = x < y ⇒ ((x < 0.5 · x + 0.5 · y) ∧ (0.5 · x + 0.5 · y < y)) Both, φ1 and φ2 have free variables x and y. The formulas ∀x.∀y.φ1 (x, y) and ∀x.∀y.φ2 (x, y) are sentences, as they do not have any free variables. The semantics of LRA formulas is defined inductively. To evaluate formulas with free variables, such as φ(x, y) = (x ≤ 0.2 · y), we need to assign values to x and y. This is 17
Feed-Forward Neural Networks done by an interpretation function I : X → R. The above formula φ is evaluated to true iff I(x) ≤ 0.2 · I(y). Towards the semantics, we will first assign to each term t a real number I(t) ∈ R inductively as follows: – I(a · x) = a · I(x) – I(b) = b – I(t1 + t2 ) = I(t1 ) + I(t2 ) Now, models of formulas φ are interpretation functions: – I |= t1 ≤ t2 if I(t1 ) ≤ I(t2 ) – I |= ¬φ if I ̸|= φ – I |= φ ∨ ψ if I |= φ or I |= ψ – I |= ∃x.φ if there is r ∈ R such that I[x 7→ r] |= φ Here, I[x 7→ r] is the interpretation function that coincides with I on all variables apart from x, while x is mapped to r. We say that formula φ is satisfiable if there is an interpretation function I such that I |= φ. Note that, to evaluate a formula (a term), it is enough to know the interpretation of the free variables (variables, respectively) that occur in it. Therefore, given a formula φ(x1 , . . . , xn ) and r1 , . . . , rn ∈ R, we write |= φ(r1 , . . . , rn ) if I |= φ(x1 , . . . , xn ) for some interpretation I such that I(xi ) = ri for all i ∈ {1, . . . , n}. In the particular case where φ is a sentence, satisfiability is independent of an interpretation function. That is, we either have one of the following: – I |= φ for all interpretation functions I – I ̸|= φ for all interpretation functions I In the former case, we write |= φ, and we say that φ is true. In the latter case, φ is false. Example 3.3: We continue Example 3.2. The sentences ∀x.∀y.φ1 (x, y) and ∀x.∀y.φ2 (x, y) are both true. On the other hand, ∀x.∀y.∃z.(x < z ∧ z < y) is false. Definition 3.5: Satisfiability Problem For a class of formulas F, the decision problem SAT(F) is defined as follows: Input: A formula φ ∈ F. Question: Is φ satisfiable? Note that free variables in the given formula φ are implicitly interpreted as existential variables, as the question is whether there is a suitable interpretation function. Moreover, if φ is a sentence, then the problem amounts to asking if φ is true. 18
Feed-Forward Neural Networks The definition of SAT(F) applies to all classes of formulas F that we consider in this lecture, as they will all be based on interpretation functions of the form I : X → R. Theorem 3.1: The problem SAT(LRA) is decidable. Before we prove this theorem, we give our specification language for neural networks. It is basically LRA, but with an additional predicate that allows us to talk about the input-output relation induced by a neural network. Definition 3.6: Neural Network Logic Formulas from NNL (neural network logic) are given by the following grammar: t ::= a · x | b | t + t
φ ::= t ≤ t | ¬φ | φ ∨ φ | ∃x.φ | N (x1 , . . . , xm ) = (y1 , . . . , yn ) where N is a neural network with input dimension m ∈ N+ and output dimension n ∈ N+ , x, x1 , . . . , xm , y1 , . . . , yn ∈ X , and a, b ∈ Q. Note that, in the formula N (x1 , . . . , xm ) = (y1 , . . . , yn ), the variables x1 , . . . , xm and y1 , . . . , yn are free. As NNL is an extension of LRA, it only remains to define the semantics of N (x1 , . . . , xm ) = (y1 , . . . , yn ): I |= N (x1 , . . . , xm ) = (y1 , . . . , yn ) if JN K(I(x1 ), . . . , I(xm )) = (I(y1 ), . . . , I(yn )) Accordingly, given an NNL sentence φ, we write |= φ (and say that φ is true) if I |= φ for some/all I. Given an NNL formula φ containing the neural networks N1 , . . . , Nk , we may write φ[N1 , . . . , Nk ] instead of just φ to highlight that φ talks about N1 , . . . , Nk .3 For a set of NNL formulas F and a set of activation functions A, we denote by F[A] the set of formulas φ ∈ F such that every neural network occurring in φ uses only activation functions from {id} ∪ A. To simplify notation further, we may just write a list of functions instead of a set. For example, NNL[ReLU] is the set of NNL formulas whose neural networks use the identity function or ReLU in their layers. Similarly, NNL[ReLU, σ, tanh] admits activation functions from {id} ∪ {ReLU, σ, tanh}, while NNL[∅] admits only the identity function. Now, let us define some concrete NNL specifications: Exercise 3.4: Let N be a neural network with in(N ) = out(N ) = 2. Write NNL sentences φ1 [N ] and φ2 [N ] such that the following hold: – JN K is surjective iff |= φ1 [N ] 3
We could have defined NNL formulas using “neural network variables” so that models interpret these variables as neural networks, but this would cause some notational overhead.
19
Feed-Forward Neural Networks
– JN K is injective iff |= φ2 [N ] Solution: – φ1 [N ] = ∀y1 , y2 .∃x1 , x2 . N (x1 , x2 ) = (y1 , y2 ) N (x1 , x2 ) = (y1 , y2 ) ∧ N (x′1 , x′2 ) = (y1 , y2 ) ⇒ – φ2 [N ] = ∀x1 , x2 , x′1 , x′2 , y1 , y2 . x1 = x′1 ∧ x2 = x′2 Exercise 3.5: Write an NNL sentence for the XOR function: A given neural network N should compute a function R2 → R that, for every input (x1 , x2 ) ∈ {0, 1}2 , outputs the truth value x1 ⊕ x2 . Exercise 3.6: Write NNL sentences for the properties (a)–(g) given at the beginning of Section 3.2: For each property P among (a)–(f), define an NNL sentence φ[N ] such that |= φ[N ] iff N satisfies P . For property (g), write an NNL sentence φ[N1 , N2 ] such that |= φ[N1 , N2 ] iff N1 , N2 satisfy (g). Solution: For a (definable) set R ⊆ Rm , let φR (x1 , . . . , xm ) be an LRA formula such that, for all r1 , . . . , rm ∈ R, we have (r1 , . . . , rm ) ∈ R iff |= φR (r1 , . . . , rm ). (a) ∀x1 , . . . , xm , y. (N (x1 , . . . , xm ) = y ⇒ y = max(x1 , . . . , xm ))
(b) ∀x1 , . . . , xm , y1 , . . . , ym . (c) ∀x1 , . . . , xm .∃y1 , . . . , yn .
N (x1 , . . . , xm ) = (y1 , . . . , ym ) ^
⇒
1≤i<j≤m
^
π∈Sm
yi ≤ yj ∧
m _ ^
xi = yπ(i)
π∈Sm i=1
N (xπ(1) , . . . , xπ(m) ) = (y1 , . . . , yn )
(d) ∀x1 , . . . , xm , y1 , . . . , ym . ^
π∈Sm
N (x1 , . . . , xm ) = (y1 , . . . , ym ) ⇒
N (xπ(1) , . . . , xπ(m) ) = (yπ(1) , . . . , yπ(m) )
20
Feed-Forward Neural Networks
(e)
∀x, x′ , y, y′ .
N (x) = y ∧ N (x′ ) = y′ ∧ φR (x) ∧ φR (x′ ) ∧ ⇒
^
xi = x′i
i∈K
argmax(y) = argmax(y′ )
(f) N (x) = y ∧ N (x′ ) = y′ ∧ φR (x) (xi ≤ x′i ⇒ zi = x′i − xi ) m ^ ∧ ∧ ∃z1 , . . . , zm . i=1 ∀x, x′ , y, y′ . ′ ′ ) < x ⇒ z = x − x (x i i i i i ∧ z1 + . . . + zm ≤ ε ⇒ ′ argmax(y) = argmax(y )
(g) ∀x, y, y′ .
N1 (x) = y ∧ N2 (x) = y′ ∧ φR (x) ⇒
argmax(y) = argmax(y′ )
An NNL formula φ[N1 , . . . , Nk ] is considered to represent a neural network specification. Verifying N1 , . . . , Nk amounts to deciding whether φ[N1 , . . . , Nk ] is satisfiable. We will assume that N1 , . . . , Nk are all ReLU neural networks, i.e., φ ∈ NNL[ReLU]. To establish decidability of verification, due to Theorem 3.1, it is then enough to show that φ can be translated into an equivalent LRA sentence. Definition 3.7: Let F1 and F2 be classes of formulas (whose semantics depends on interpretation functions I : X → R). We write F1 ≤ F2 if there is an algorithm that translates every φ(x1 , . . . , xn ) ∈ F1 into φ̃(x1 , . . . , xn ) ∈ F2 such that, for all interpretation functions I, we have I |= φ iff I |= φ̃. If the translation can be done in polynomial time, then we write F1 ≤poly F2 . Proposition 3.1: We have NNL[ReLU] ≤poly LRA.
Proof. We only need to consider formulas involving neural networks. To do so, we translate every neural network N , say with input dimension m and output dimension n, into 21
Feed-Forward Neural Networks an LRA formula φN (x1 , . . . , xm , y1 , . . . , yn ) such that for all r1 , . . . , rm , s1 , . . . , sn ∈ R, we have JN K(r1 , . . . , rm ) = (s1 , . . . , sn ) iff |= φN (r1 , . . . , rm , s1 , . . . , sn )
(3.1)
We proceed by induction and first suppose that N = (L ) has one layer L = (A, b, f ). If f = id, we set φN (x1 , . . . , xm , y1 , . . . , yn ) =
n ^
yi = bi +
i=1
If f = ReLU, we set
φN (x1 , . . . , xm , y1 , . . . , yn ) = ∃z. i=1 n ^
m X j=1
z = bi +
m X
Then, statement (3.1) holds by the very definitions.
ai,j · xj
. ! (z ≤ 0 ∧ yi = 0) ∨ (z > 0 ∧ yi = z) j=1
∧
ai,j · xj .
Now assume N = (L (1) , . . . , L (ℓ) , L (ℓ+1) ) with ℓ ≥ 1. Let N1 = (L (1) , . . . , L (ℓ) ) and N2 = (L (ℓ+1) ) and assume we already have formulas φN1 (x1 , . . . , xm , z1 , . . . , zk ) and φN2 (z1 , . . . , zk , y1 , . . . , yn ) as required, where k = out(N1 ) = in(N2 ). Then, we set φN1 (x1 , . . . , xm , z1 , . . . , zk ) φN (x1 , . . . , xm , y1 , . . . , yn ) = ∃z1 , . . . , zk . . ∧ φN2 (z1 , . . . , zk , y1 , . . . , yn ) Indeed, for all r1 , . . . , rm , s1 , . . . , sn ∈ R we have iff
JN K(r1 , . . . , rm ) = (s1 , . . . , sn )
(JN2 K ◦ JN1 K)(r1 , . . . , rm ) = (s1 , . . . , sn )
JN1 K(r1 , . . . , rm ) = (p1 , . . . , pk )
iff
there are p1 , . . . , pk ∈ R:
iff
there are p1 , . . . , pk ∈ R:
iff
|= φN (r1 , . . . , rm , s1 , . . . , sn ) .
and JN2 K(p1 , . . . , pk ) = (s1 , . . . , sn ) ! |= φN1 (r1 , . . . , rm , p1 , . . . , pk )
!
and |= φN2 (p1 , . . . , pk , s1 , . . . , sn )
Now, to translate a given NNL formula φ into the LRA formula φ̃ as required, we replace, in φ, every occurrence of an atomic subformula N (x1 , . . . , xm ) = (y1 , . . . , yn ) by φN (x1 , . . . , xm , y1 , . . . , yn ). Exercise 3.7: For the NNL sentence φ for the maximum function, and the neural network N from Example 3.1(a), determine φ̃ according to Proposition 3.1. As a corollary from Proposition 3.1 and Theorem 3.1 (decidability of SAT(LRA)), we obtain the following result:
22
Feed-Forward Neural Networks Theorem 3.2: The problem SAT(NNL[ReLU]) is decidable. We still need to show Theorem 3.1, i.e., decidability of LRA, which deserves its own section.
3.3
Proof of Decidability of LRA
We use automata-theoretic techniques, which are versatile tools for deciding arithmetic theories and can often be easily extended to cover even richer theories [18]. The automatatheoretic approach to deciding arithmetic theories goes back to Büchi [9]. Given an LRA formula φ, the idea is to construct a Büchi automaton Aφ such that φ is satisfiable iff the language of Aφ is nonempty. In the description below, we adopt several constructions and some notation from the paper [42], where Sälzer et al. provide translations of neural networks into Büchi automata. Encoding Real Numbers as Words. The main idea is to encode a real number as a word over the alphabet Σ = {0, 1, •, +, −}, and a k-tuple of real numbers as a word over Σk . We call a word w ∈ Σω well-formed if it is of the form w = sun−1 . . . u0 • v1 v2 . . . ∈ {+, −}{0, 1}∗ {•}{0, 1}ω with n ≥ 0, s ∈ {+, −}, and un−1 , . . . , u0 , v1 , v2 , . . . ∈ {0, 1}. Then, w encodes the real number in binary dec(w) = (−1)sign(s) ·
n−1 X
∞ X
1 ui · 2 i + vi · i 2 i=0 i=1
!
where sign(+) = 0 and sign(−) = 1. Note that w determines a unique value dec(w). On the other hand, given r ∈ R, there may be several well-formed words w ∈ Σω such that dec(w) = r. For example, we have dec(+0 • 000 . . .) = dec(−000 • 000 . . .) = 0 and dec(+0110 • 1000 . . .) = dec(+110 • 0111 . . .) = 6.5. Let k ≥ 0. A word
u1,1 u1,2 u1,3 w = ... ... ... . . . ∈ (Σk )ω uk,1
uk,2
uk,3
may be seen as the k-tuple (u1,1 u1,2 u1,3 . . . , . . . , uk,1 uk,2 uk,3 . . .) of words over Σ. Thus, a language L ⊆ (Σk )ω can, equivalently, be considered as a relation L ⊆ (Σω )k and the latter is the view that we mostly adopt in the following. Now, a tuple (w1 , . . . , wk ) ∈ (Σk )ω of well-formed words encodes the tuple of real numbers (dec(w1 ), . . . , dec(wk )) ∈ Rk . However, the algorithmic manipulations we perform on automata to simulate arithmetic operations require that the comma • in the binary representations be aligned. Therefore, we introduce the set of (k-ary) well-formed words, 23
Feed-Forward Neural Networks {0, 1}k {+, −}k
{0, 1}k {•}k
Figure 3.5: The Büchi automaton Akwf denoted WFk . A word from (Σk )ω is well-formed if it is of the form s1 u1,n−1 u1,0 • v1,1 v1,2 .. .. .. .. .. .. . . . . . . . . . . . . sk uk,n−1 uk,0 • vk,1 vk,2
such that si ∈ {+, −}, ui,j ∈ {0, 1}, and vi,j ∈ {0, 1} for all i and j. In particular, all • are aligned in the same column. If k = 0, we have a unique infinite word over a singleton alphabet, which we define to be well-formed. Recall that we may consider WFk ⊆ (Σω )k . For w ∈ (Σω )k , we let wi refer to the i-th component of w, i.e., w = (w1 , . . . , wk ). Proposition 3.2: For k ≥ 0, we can effectively construct a Büchi automaton Akwf over Σk such that L(Akwf ) = WFk .
Proof. The automaton Akwf is given in Figure 3.5. It checks that each “row” is contained in {+, −}{0, 1}∗ {•}{0, 1}ω and that the •-symbols are aligned in the same column. We present two further useful automata constructions. Proposition 3.3: Büchi Automata Projection Let k ≥ 1 and i ∈ {0, 1, . . . , k}. Let A be a Büchi automaton over Σk . We can effectively construct a Büchi automaton proj ≤i (A) over Σi such that L(proj ≤i (A)) = {(w1 , . . . , wi ) | (w1 , . . . , wk ) ∈ L(A)} . Proof. Let A = (Q, ∆, ι, F ) be a Büchi automaton over Σk . The Büchi automaton proj ≤i (A) has the same structure (i.e., the same states, initial states, transitions, final states). The only thing that changes are the transition labels, which instead of k symbols, [u1 , . . . , uk ], only contain the first i symbols [u1 , . . . , ui ]. That is, we set proj ≤i (A) = (Q, ∆′ , ι, F ) with ∆′ = {(p, [u1 , . . . , ui ], q) | (p, [u1 , . . . , uk ], q) ∈ ∆} . Note that, when i = 0, proj ≤i (A) is a Büchi automaton over a single-letter alphabet. The correctness proof is now straightforward. Applying projection to well-formed words does not necessarily preserve closure under removing leading zeros. Therefore, we will make use of another useful closure property.
24
Feed-Forward Neural Networks Proposition 3.4: Let k ≥ 1 and let A be a Büchi automaton over Σk such that L(A) ⊆ WFk . We can construct a Büchi automaton cl (A) over Σk such that L(cl (A)) is the least set satisfying the following: – L(A) ⊆ L(cl (A)) and
– for all words w ∈ L(cl (A)) of the form w = (s1 , . . . , sk )(0, 0, . . . , 0)w′ (i.e., s1 , . . . , sk ∈ {+, −}), we have (s1 , . . . , sk )w′ ∈ L(cl (A)). Exercise 3.8: Prove Proposition 3.4. From LRA to Büchi automata. We are now ready to describe how Büchi automata can be used to decide whether a given LRA sentence is true. We start with some constructions for k-ary relations of real numbers that will serve as building blocks in the translation. They are due to [42]. Proposition 3.5: Büchi Automata Constructions Let k ≥ 1, i, j, i1 , i2 ∈ {1, . . . , k}, and a, b ∈ Q. We can effectively construct automata Aki=j , Aki≤j , Aki=add(i1 ,i2 ) , Aki=mult(a,j) , and Aki=const(b) over Σk such that L(Aki=j ) = {w ∈ WFk | dec(wi ) = dec(wj )} L(Aki≤j ) = {w ∈ WFk | dec(wi ) ≤ dec(wj )} L(Aki=add(i1 ,i2 ) ) = {w ∈ WFk | dec(wi ) = dec(wi1 ) + dec(wi2 )} L(Aki=mult(a,j) ) = {w ∈ WFk | dec(wi ) = a · dec(wj )} L(Aki=const(b) ) = {w ∈ WFk | dec(wi ) = b} Proof. We start with equality and addition. The other automata will build on them. We only consider constructions with pairwise distinct indices. The remaining cases follow similar patterns. Equality. The equality Büchi automaton A21=2 is depicted in Figure 3.6. Note that two binary representations of real numbers can still be equal when they have different signs. The right-hand side of the automaton also takes care of real numbers that have a suffix of the form 1ω . The general case Aki=j allows for arbitrary values in the components different from i and j (while checking that the word be well-formed). k Addition. Consider first the Büchi automaton Bi=add(i as illustrated in Figure 3.7 1 ,i2 ) 3 for the special case B3=add(1,2) (the cases with different signs are similar, since x3 = x1 −x2 iff x1 = x2 + x3 and so on). It performs bitwise addition of the first two numbers, while checking, each time, whether a carry bit has to be produced. Whereas this procedure
25
Feed-Forward Neural Networks !
1 0
"
!
A21=2
! !
!
0 0
0 0
+ −
!
+ +
"!
"!
− +
"
− −
"
!
0 0
"!
1 1
!
"
!
"
"
!
• •
"
!
0 1
0 1
1 0
"
"
!
!
• •
• •
• •
!
"
"
"
"
!
0 1
1 0
"
" !
!
1 0
0 0
"!
1 1
"
"
!
0 1
"
Figure 3.6: The Büchi automaton A21=2 k ) does not yields, for all possible input strings, at least one valid result, L(Bi=add(i 1 ,i2 ) k 3 ) contain all w ∈ WF such that dec(wi ) = dec(wi1 )+dec(wi2 ). For example, L(B3=add(1,2) does not contain the word + 0 0 • 1 1 1 1 + 0 0 • 1 1 1 1 . . . + 1 0 • 0 0 0 0
but instead
+ 0 0 • 1 1 1 1 + 0 0 • 1 1 1 1 . . . + 0 1 • 1 1 1 1
We include all admissible triples using an additional tape and the equality automaton defining k+1 Aki=add(i1 ,i2 ) = cl (proj ≤k (Bk+1=add(i ∩ Ak+1 i=k+1 )) . 1 ,i2 ) Multiplication. The cases a ∈ {0, 1} are easy. Suppose a = 2. We create an additional tape, k + 1, to “copy” the value of tape j using the Büchi automaton for equality. Tape i should then contain the sum of tapes j and k + 1. We finally erase tape k + 1. All this is realized by k+1 Aki=mult(2,j) = cl (proj ≤k (Ak+1 k+1=j ∩ Ai=add(j,k+1) )) . 26
Feed-Forward Neural Networks
3 B3=1+2
⎤⎡ ⎤⎡ ⎤ 0 0 1 ⎣ 0 ⎦⎣ 1 ⎦⎣ 0 ⎦ ⎤ 0 1 1
⎡
⎤ ⎡ + − ⎣ + ⎦ ⎣ − ⎦ + −
⎡
0 ⎣ 0 ⎦ 1
⎡
⎤⎡ ⎤⎡ ⎤ 0 1 1 ⎣ 1 ⎦⎣ 0 ⎦⎣ 1 ⎦ 0 0 1
⎤ 1 ⎣ 1 ⎦ 0
⎤ • ⎣ • ⎦ •
⎡
⎤ • ⎣ • ⎦ •
⎡
⎤ 0 ⎣ 0 ⎦ 1
···
⎤⎡
⎤
⎡
⎡
⎡
⎡
⎤⎡
⎤
0 0 1 ⎣ 0 ⎦⎣ 1 ⎦⎣ 0 ⎦ 0 1 1
⎡
⎤ 1 ⎣ 1 ⎦ 0
⎡
⎤⎡ ⎤⎡ ⎤ 0 1 1 ⎣ 1 ⎦⎣ 0 ⎦⎣ 1 ⎦ 0 0 1
3 Figure 3.7: The intermediate Büchi automaton B3=add(1,2)
Now suppose a is an integer such that a ≥ 3 (negative constants are handled similarly). Let un−1 . . . u0 ∈ {0, 1}∗ be the binary representation of a of minimal length, i.e., a = dec(+un−1 . . . u0 • 000 . . .). Furthermore, let K = {i1 , . . . , id } ⊆ {0, . . . , n − 1} be the set of indices ℓ such that uℓ = 1. In particular, n − 1 ∈ K. Note that, for all x ∈ R, we have a·x=
n−1 X ℓ=0
uℓ · 2ℓ · x =
X ℓ∈K
uℓ · 2ℓ · x .
Thus, we can set Aki=mult(a,j) = cl (proj ≤k (Ak+n k+1=j ∩
n−1 \ ℓ=1
k+n Ak+n k+1+ℓ=mult(2,k+ℓ) ∩ Ai=add(k+1+i1 ,...,k+1+id ) )) .
Note that we use a Büchi automaton performing an addition of possibly more than two elements. We obtain the corresponding Büchi automaton by induction, letting, for n ≥ 3, k+1 Aki=add(i1 ,...,in ) = cl (proj ≤k (Ak+1 k+1=add(i1 ,...,in−1 ) ∩ Ai=add(in ,k+1) ))
for integers m ∈ Z and n ∈ N+ . For any real numbers Finally, suppose that a = m n m x, y ∈ R, we have x = n · y iff n · x = m · y. Thus, we can set k+2 k+2 Aki=mult(a,j) = cl (proj ≤k (Ak+2 k+1=mult(n,i) ∩ Ak+2=mult(m,j) ∩ Ak+1=k+2 )) .
The remaining constructions are left as an exercise.
27
Feed-Forward Neural Networks Exercise 3.9: Determine the Büchi automata Aki≤j and Aki=const(b) (for b ∈ Q). From LRA to Büchi Automata. We now have all the ingredients to transform a given formula into a Büchi automaton that we can then test for nonemptiness. For simplicity, we suppose we are given a sentence, without free variables. Given an LRA sentence, we first transform it into a logically equivalent formula in Prenex normal form, i.e., into a sentence of the form Ψ = θ1 x1 . . . θm xm .Φ(x1 , . . . , xm ) where θ1 , . . . , θm ∈ {∃, ¬∃}, the x1 , . . . , xm are pairwise distinct, and Φ is quantifier-free. For background on the Prenex normal form, we refer the reader to [12]. Let t1 , . . . , tn be all distinct occurrences of terms in Φ, including4 x1 , . . . , xm . That is, m ≤ n and ti = xi for all i ∈ {1, . . . , m}. With w = (w1 , . . . , wm , wm+1 , . . . , wn ) ∈ WFn , we associate an arbitrary interpretation function Iw such that Iw (xi ) = dec(wi ) for all i ∈ {1, . . . , m}. Lemma 3.1: We can construct a Büchi automaton Aterm over Σn such that L(Aterm ) = {w ∈ WFn | Iw (ti ) = dec(wi ) for all i ∈ {m + 1, . . . , n}} . Proof. We set Aterm = where
n \
i=m+1
n Ai=add(j,k) Bin = Ani=mult(a,j) n Ai=const(b)
Bin
if ti = tj + tk if ti = a · xj if ti = b
with a, b ∈ Q. Correctness follows from Proposition 3.5 by induction. Example 3.4: Consider the sentence Ψ = ¬∃x1 .∃x2 . (x1 ≤ x2 ∧ ¬((x1 ≤ 0.5 · x1 + 0.5 · x2 ) ∧ (0.5 · x1 + 0.5 · x2 ≤ x2 ))) {z } | Φ(x1 , x2 )
in Prenex normal form. The terms occurring in Φ are x1 , x2 , 0.5 · x1 , 0.5 · x2 , 0.5 · 4
Strictly speaking, a variable is not a term.
28
Feed-Forward Neural Networks
x1 + 0.5 · x2 , and we have x1 + 0 1 • 0 0 0 0 x2 + 1 0 • 0 0 0 0 0.5 · x1 + 0 0 • 1 0 0 0 . . . ∈ L(Aterm ) . 0.5 · x2 + 0 1 • 0 0 0 0 0.5 · x1 + 0.5 · x2 + 0 1 • 1 0 0 0 Using Aterm , we now proceed by induction to transform any subformula φ(x1 , . . . , xm ) of Φ (including Φ) into a Büchi automaton Bφ over Σn such that, for all w ∈ L(Aterm ), w ∈ L(Bφ ) iff Iw |= φ(x1 , . . . , xm ) .
(3.2)
Term Comparison. Suppose φ(x1 , . . . , xm ) = (ti ≤ tj ). We set Bti ≤tj = Ani≤j . Let w = (w1 , . . . , wn ) ∈ L(Aterm ). We will show (3.2). Suppose w ∈ L(Bφ ). Since w ∈ L(Aterm ), we have Iw (ti ) = dec(wi ) and Iw (tj ) = dec(wj ). By w ∈ L(Ani≤j ) and Proposition 3.5, we have dec(wi ) ≤ dec(wj ). Thus, Iw (ti ) ≤ Iw (tj ), which implies Iw |= ti ≤ tj . Conversely, suppose Iw |= ti ≤ tj . Then, Iw (ti ) ≤ Iw (tj ). Since w ∈ L(Aterm ), we also have dec(wi ) ≤ dec(wj ), which implies w ∈ L(Ani≤j ). We conclude w ∈ L(Bti ≤tj ). Disjunction. Suppose φ(x1 , . . . , xm ) = φ1 ∨ φ2 . We set Bφ1 ∨φ2 = Bφ1 ∪ Bφ2 . To show (3.2), let w ∈ L(Aterm ). We have w ∈ L(Bφ1 ∨φ2 ) iff w ∈ L(Bφ1 ) ∪ L(Bφ2 ) iff (by induction hypothesis) Iw |= φ1 ∨ φ2 . Negation. Suppose φ(x1 , . . . , xm ) = ¬ψ. We set B¬ψ = Bψ . Let us show (3.2). For w ∈ L(Aterm ), we have w ∈ L(B¬ψ ) iff w ̸∈ L(Bψ ) iff (by induction hypothesis) Iw ̸|= ψ iff Iw |= ¬ψ. We thus hold a Büchi automaton BΦ over Σn such that, for all w ∈ L(Aterm ), w ∈ L(BΦ ) iff Iw |= Φ(x1 , . . . , xm ) . Consider the Büchi automaton AΦ = cl (proj ≤m (BΦ ∩ Aterm )). 29
Feed-Forward Neural Networks Lemma 3.2: We have L(AΦ ) = {w ∈ WFm | Iw |= Φ(x1 , . . . , xm )} . Proof. Let w ∈ L(AΦ ). There is w′ = (w1′ , . . . , wn′ ) ∈ L(BΦ ∩ Aterm ) such that, for all i ∈ {1, . . . , m}, the word wi′ equals wi modulo (possibly) extra leading zeros. In particular, dec(wi′ ) = dec(wi ) for all i ∈ {1, . . . , m}. Due to w′ ∈ L(BΦ ), we have Iw′ |= Φ and, therefore, Iw |= Φ. Conversely, assume w = (w1 , . . . , wm ) ∈ WFm such that Iw |= Φ(x1 , . . . , xm ). Let w′ = (w1′ , . . . , wn′ ) ∈ WFn such that, – for all i ∈ {1, . . . , m}, wi′ equals wi but possibly has extra leading zeros, – for all i ∈ {m + 1, . . . , n}, dec(wi′ ) = Iw (ti ). Then, we have w′ ∈ L(Aterm ) and, since Iw′ |= Φ, w′ ∈ L(BΦ ). Altogether, we have ′ ) ∈ proj ≤m (BΦ ∩ Aterm ) and, finally, w = (w1 , . . . , wm ) ∈ L(AΦ ). (w1′ , . . . , wm Towards a Büchi automaton for Ψ = θ1 x1 . . . θm xm .Φ(x1 , . . . , xm ) where θi ∈ {∃, ¬∃}, we add quantifiers (and so eliminate free variables) by induction: Let Ψm = Φ(x1 , . . . , xm ) and, for i = m − 1, . . . , 0, let Ψi = θi+1 xi+1 . . . θm xm .Φ(x1 , . . . , xm ) . For i = m, . . . , 0 (the number of free variables yet to be eliminated), we build a Büchi automaton AΨi over Σi such that L(AΨi ) = {w ∈ WFi | Iw |= Ψi (x1 , . . . , xi )} .
(3.3)
Note that AΨm = AΦ . Now, let i = m − 1, . . . , 0. Towards AΨi , we will have to eliminate free variable xi+1 . Existential Quantification. If θi+1 = ∃, then we set AΨi = cl (proj ≤i (AΨi+1 )) . We show (3.3). We certainly have AΨi ⊆ WFi . Let w = (w1 , . . . , wi ) ∈ WFi . Suppose w ∈ L(AΨi ). Then, there is w′ ∈ L(AΨi+1 ) ⊆ WFi+1 such that, for all j ∈ {1, . . . , i}, wj′ equals wj modulo extra leading zeros. By induction hypothesis, we have that Iw′ |= Ψi+1 (x1 , . . . , xi+1 ). But this implies Iw |= ∃xi+1 .Ψi+1 (x1 , . . . , xi+1 ). Conversely, suppose Iw |= Ψi = ∃xi+1 .Ψi+1 (x1 , . . . , xi+1 ). There is a real number r ∈ R ′ such that Iw [xi+1 7→ r] |= Ψi+1 (x1 , . . . , xi+1 ). Let w′ = (w1′ , . . . , wi+1 ) ∈ WFi+1 such that ′ ′ dec(wi+1 ) = r and, for all j ∈ {1, . . . , i}, wj equals wj but possibly has extra leading zeros. We have Iw′ |= Ψi+1 (x1 , . . . , xi+1 ). By induction hypothesis, w′ ∈ L(AΨi+1 ). We conclude w ∈ L(AΨi ). 30
Feed-Forward Neural Networks Negated Existential Quantification. If θi+1 = ¬∃, then we set AΨi = cl (proj ≤i (AΨi+1 )) ∩ Aiwf . That is, we first apply projection and closure as in the previous case, then complement the automaton, and finally intersect it with Aiwf . By the preceding discussion, we have w ∈ L(AΨi )
w ∈ WFi and Iw ̸|= ∃xi+1 .Ψi+1 (x1 , . . . , xi+1 )
iff iff .
w ∈ WFi and Iw |= ¬∃xi+1 .Ψi+1 (x1 , . . . , xi+1 ) | {z } = Ψi
To wrap up, we obtain the Büchi automaton AΨ0 over Σ0 (a singleton alphabet) such that L(AΨ0 ) ̸= ∅ iff |= Ψ0 (recall that Ψ0 = Ψ). Nonemptiness of the language of a Büchi automaton is a decidable problem due to Theorem 2.2. Exercise 3.10: Consider the extension NNL+ of NNL given by the following grammar: t ::= a · x | b | t + t
φ ::= isPowerOfTwo(x) | t ≤ t | ¬φ | φ ∨ φ | ∃x.φ | N (x1 , . . . , xm ) = (y1 , . . . , yn ) where N is a neural network with input dimension m ∈ N+ and output dimension n ∈ N+ , x, x1 . . . , xm , y1 , . . . , yn ∈ X , and a, b ∈ Q. The semantics of the new atomic formula isPowerOfTwo(x) is given as follows (for an interpretation function I): I |= isPowerOfTwo(x) if there is n ∈ N such that I(x) = 2n Show that the problem below is decidable: Input: An NNL+ specification φ[N1 , . . . , Nk ] such that N1 , . . . , Nk are all ReLU neural networks. Question: Does |= φ[N1 , . . . , Nk ] hold? It is enough to describe the modifications wrt. the decidability proof for NNL. Historical Notes and Remarks on Complexity. LRA corresponds to the firstorder theory of real numbers with addition, denoted by FO(R, +, <). Tarski showed that even FO(R, +, · , <), i.e., non-linear real arithmetic (including multiplication), is decidable [50]. While his algorithm was nonelementary, FO(R, +, · , <) was shown to be solvable in doubly exponential time [10]. The automata-based decidability proof for FO(R, +, <) presented in this section can be easily extended to FO(R, +, <, Z), which has an additional unary predicate for the integers Z. Another well-known decidable theory is FO(N, +, <), also known as Presburger arithmetic. On the other hand, FO(N, +, · , <), i.e., Peano arithmetic, is undecidable due to Gödel [17]. 31
Feed-Forward Neural Networks The automata-theoretic approach to deciding FO(R, +, <, Z) is due to Büchi [9]. Note that projection and negation together may cause an exponential blow-up in the automata size, which a priori does not allow us to infer an elementary bound on the automata size and computation time. Boigelot, Jodogne, and Wolper showed that the models of every FO(R, +, <, Z)-formula are recognized by a weak deterministic Büchi automaton, in which every strongly connected component contains either only final states or only nonfinal states [7]. Löding showed that minimization of these automata can be reduced, in linear time, to the minimization of DFAs [33]. Moreover, a doubly and triply exponential upper bound on the size of minimal weak deterministic Büchi automata for formulas from FO(R, +, <) and FO(R, +, <, Z) were shown by Klaedtke [27] and, respectively, Eisinger [13]. For Presburger arithmetic and finite automata, a triply exponential upper bound is due to Klaedtke [26]. These (finite) automata can even be computed in triply exponential time, as was shown by Durand-Gasselin and Habermehl [11]. These results suggest that automata-based decision procedures may still enjoy a good complexity and run well in practice. Various automata-based libraries for deciding arithmetic theories are available [4, 7, 29]. NNL specifications can often do without quantifier alternation, i.e., they belong to the existential fragment, which has a favorable complexity. We will address this in the next section. We will also discuss theories that correspond to deciding NNL sentences with activation functions such as σ and tanh [21].
3.4
An Efficiently Solvable Fragment of NNL
Our goal is now to identify a fragment of NNL[ReLU] that comes with an efficiently solvable satisfiability problem. Observe that many specifications that we have seen previously have a relatively simple structure in the sense that they can do without quantifier alternation. For example, consider Exercise 3.4. While φ1 has one quantifier alternation, φ2 is the negation of an existential formula: N (x1 , x2 ) = (y1 , y2 ) ∧ N (x′1 , x′2 ) = (y1 , y2 ) ∧ φ2 [N ] = ¬∃x1 , x2 , x′1 , x′2 , y1 , y2 . ¬(x1 = x′1 ) ∨ ¬(x2 = x′2 ) We will indeed show that satisfiability for existential NNL[ReLU] formulas is NP-complete (and, therefore, satisfiability for universal NNL[ReLU] formulas coNP-complete). Let us first define the corresponding fragment: Definition 3.8: Existential NNL (∃NNL) Formulas from ∃NNL are given by the following grammar: t ::= a · x | b | t + t
φ ::= t ≤ t | t < t | φ ∨ φ | φ ∧ φ | ∃x.φ |
N (x1 , . . . , xm ) = (y1 , . . . , yn ) | ¬ (N (x1 , . . . , xm ) = (y1 , . . . , yn ))
where N is a neural network with input dimension m ∈ N+ and output dimension n ∈ N+ , x, x1 , . . . , xm , y1 , . . . , yn ∈ X , and a, b ∈ Q. 32
Feed-Forward Neural Networks Note that, as formulas are in negation normal form (negation is pushed inwards), we include atomic formulas of the form t1 < t2 and ¬ (N (x1 , . . . , xm ) = (y1 , . . . , yn )), which are otherwise no longer expressible. We also use the abbreviations t1 = t2 ≡ t1 ≤ t2 ∧ t2 ≤ t1 and t1 ̸= t2 ≡ t1 < t2 ∨ t2 < t1 . Note that existential quantifiers are not strictly necessary when considering satisfiability. However, we include them to be able to preserve the number of free variables when translating forth and back between various logics. We will see that we can translate ∃NNL[ReLU] into existential LRA, which is defined analogously: Definition 3.9: Existential Linear Real Arithmetic (∃LRA) Formulas from ∃LRA are generated by the following grammar: t ::= a · x | b | t + t
φ ::= t ≤ t | t < t | φ ∨ φ | φ ∧ φ | ∃x.φ where x ∈ X and a, b ∈ Q. We use the abbreviations t1 = t2 and t1 ̸= t2 as in ∃NNL. Theorem 3.3: Complexity of ∃LRA The problem SAT(∃LRA) is NP-complete. The decision procedure can resort to SMT solvers combining, for example, DPLL(T), Simplex (linear programming) and Tseitin’s transformation. See [2] or [28] for a detailed exposition. Actually, we still need to say what the size of a formula is. It is the length of the formula when constants are written in binary encoding: The length of a rational number m/n (the fraction being simplified), with m ∈ Z and n ∈ N+ , is defined as 1 + ⌈log(|m| + 1) + 1⌉ + ⌈log(n + 1) + 1⌉. Similarly, concerning ∃NNL[ReLU], we define the size of a matrix/vector as the sum of the sizes of all its coefficients. Our goal is to show the following result: Theorem 3.4: The problem SAT(∃NNL[ReLU]) is NP-complete. The lower bound follows from the obvious fact that ∃LRA ≤poly ∃NNL[ReLU]. However, we will show it for a smaller fragment of ∃NNL. The upper bound stated in Theorem 3.4 is due to the following reduction:
33
Feed-Forward Neural Networks Lemma 3.3: We have ∃NNL[ReLU] ≤poly ∃LRA. Proof. We proceed like in the general case of Lemma 3.1 and translate N , say with input dimension m and output dimension n, into ∃LRA formulas φN (x1 , . . . , xm , y1 , . . . , yn ) and φ′N (x1 , . . . , xm , y1 , . . . , yn ) such that, for all r1 , . . . , rm , s1 , . . . , sn ∈ R the following hold: – JN K(r1 , . . . , rm ) = (s1 , . . . , sn ) iff |= φN (r1 , . . . , rm , s1 , . . . , sn ) – JN K(r1 , . . . , rm ) ̸= (s1 , . . . , sn ) iff |= φ′N (r1 , . . . , rm , s1 , . . . , sn )
We define φN (x1 , . . . , xm , y1 , . . . , yn ) exactly like in the proof of Lemma 3.1. Note that this gives indeed rise to an ∃LRA formula. Moreover, we set φN (x1 , . . . , xm , z1 , . . . , zn ) n _ φ′N (x1 , . . . , xm , y1 , . . . , yn ) = ∃z1 , . . . , zn . , ∧ yi ̸= zi i=1
which is an ∃LRA formula, too. The overall translation produces a formula of polynomial size.
We will now present a stronger lower bound, due to [24, 43, 44], for the reachability fragment of ∃NNL[ReLU]: Definition 3.10: Reachability Formulas A formula from REACH is an ∃NNL formula of the form N (x1 , . . . , xm ) = (y1 , . . . , yn ) ∧ φ1 (x1 , . . . , xm ) ∧ φ2 (y1 , . . . , yn ) where φ1 and φ2 are quantifier-free formulas generated by the grammar t ::= a · x | b | t + t
φ ::= t ≤ t | φ ∧ φ with x ∈ X and a, b ∈ Q.
In particular, all variables are implicitly existentially quantified. Theorem 3.5: Reachability is NP-hard [43, 44] The problem SAT(REACH[ReLU]) is NP-hard. Proof. We follow [43, 44] and provide a polynomial-time reduction from 3SAT (satisfiability of 3CNF formulas). A 3CNF formula is a conjunction of clauses. Every clause is the disjunction of three literals. A literal is a propositional variable Xi or its negation ¬Xi . An example formula over the variables X1 , X2 , X3 , X4 with three clauses is (X1 ∨ X2 ∨ X3 ) ∧ (¬X1 ∨ X2 ∨ ¬X3 ) ∧ (¬X2 ∨ X3 ∨ X4 ) . {z } | {z } | {z } | C1 C2 C3 34
Feed-Forward Neural Networks id
1 x1
x1 +1
−1
ReLU −1
¬x1
id +1
+1 −1
−1 1 x2
x2
−1
+1 −1
1 −1
¬x2
id +1
+1
−1 1 x3 −1
1 x4
x3
−1
+1
−1
¬x3
x4
C1
−1
C2
1
y
1
+1
−1
+1 −1
C3
−1
+1 −1
¬x4
1
1
−0.5 1
xi
−0.5
1
+0.5
−1
1
zi
1
Figure 3.8: Neural network for (X1 ∨ X2 ∨ X3 ) ∧ (¬X1 ∨ X2 ∨ ¬X3 ) ∧ (¬X2 ∨ X3 ∨ X4 )
The satisfiability problem for 3CNF formulas is NP-complete: Given a 3CNF formula Φ = C1 ∧ . . . ∧ Ck over variables X1 , . . . , Xm , is there a valuation val : {X1 , . . . , Xm } → {0, 1} such that val (Φ) = 1 (with the canonical extension of val to formulas)? We will first build a neural network N such that
JN K {0,1}m :
{0, 1}m → R
r = (r1 , . . . , rm ) 7→ val r (C1 ) + . . . + val r (Ck )
where val r (Xi ) = ri for all i ∈ {1, . . . , m}. The neural network N is illustrated in the 35
Feed-Forward Neural Networks upper part of Figure 3.8. Correctness follows because, for all r1 , r2 , r3 ∈ {0, 1}, we have 1 − ReLU(1 − r1 − r2 − r3 )
= 1 − max(0, 1 − r1 − r2 − r3 ) 0 if r1 = r2 = r3 = 0 = 1 otherwise.
It follows that
Φ is satisfiable iff
N (x1 , . . . , xm ) = y m ^ ∧ is satisfiable. (x = 0 ∨ x = 1) i i i=1 ∧ y=k
However, the latter is not a REACH formula (there cannot be a suitable REACH formula, as {0, 1}m is not a hyperrectangle). So we add some more neurons to N that allow us to enforce xi ∈ {0, 1} in the sentence (cf. lower part of Figure 3.8). We then obtain a neural network N ′ with in(N ′ ) = m and out(N ′ ) = m + 1. Note that, for all r ∈ R, the following holds: bool (r) = ReLU(r − 0.5) + ReLU(0.5 − r) − 0.5 ( r − 1 if r ≥ 0.5 = −r if r < 0.5 In particular, we have bool (r) = 0 iff r ∈ {0, 1}. Therefore,
Φ is satisfiable iff
N ′ (x1 , . . . , xm ) = (y, z1 , . . . , zm ) m ^ ∧ is satisfiable. zi = 0 i=1 ∧ y=k
As the latter is a REACH formula whose size (in particular N ′ ) is polynomial, we are done.
Theorem 3.6: NP-hardness for ReLU layers [43, 44] NP-hardness from Theorem 3.5 also holds for ReLU neural networks such that all but the last layers are ReLU layers.
Proof. We replace a neuron with activation function id by a gadget employing activation 36
Feed-Forward Neural Networks +b1 id
a′1
y1
x1
ReLU
−a1
···
···
+b
xm
a1
a′n
am
!
yn
a′1
−a′1
+b
am
a′n
−am
−a′n
yn
xm
+bn
y1
···
a1
···
x1
+b1
+bn
−b
Figure 3.9: Replacing an id neuron with ReLU neurons function ReLU. This is illustrated in Figure 3.9. Indeed, we have
b+
m X i=1
ai xi · a′j
m m X X ′ ai xi · (−a′j ) = ReLU b + ai xi · aj + ReLU − b + i=1
i=1
m m X X ′ = ReLU b + ai xi · aj + ReLU −b + −ai xi · (−a′j ) i=1
i=1
This concludes the proof. NP-hardness results for even stronger restrictions on the neural networks can be found in [43, 44, 55]. Observe that, when the only activation function allowed is the identity function id, satisfiability of REACH[∅] can be reduced to a linear-programming problem. Therefore, we obtain the following result: Theorem 3.7: The problem SAT(REACH[∅]) is solvable in polynomial time. Recall that many NNL specifications are negations of ∃NNL[ReLU] sentences. As a corollary of Theorem 3.4, we can cover this case, too: Theorem 3.8: The following decision problem is coNP-complete. Input: A sentence φ ∈ ∃NNL[ReLU]. Question: Do we have |= ¬φ?
37
Feed-Forward Neural Networks 3 ReLU NLReLU sigmoid (σ) tanh
ReLU(x) = max(0, x)
g(x)
2 NLReLU(x) = ln(1 + ReLU(x)) 1
1 σ(x) = 1 + e−x
tanh(x) =
ex − e−x ex + e−x
x −3
−2
−1
1
2
3
−1
Figure 3.10: (Local) activation functions given by g : R → R Exercise 3.11: In Theorem 3.8, why do we have to restrict inputs to sentences?
3.5
Beyond ReLU Neural Networks
So far, we mainly considered ReLU neural networks. But how about decidability for general neural networks? In this section, we establish equivalence between verification for a particular set of activation functions and LRA extended by the exponential function [21]. Definition 3.11: First-Order Formulas over the Real Exponential Field Formulas from REF (first-order formulas over the real exponential field ) are defined as follows: t ::= a | x | t + t | t · t | et φ ::= t ≤ t | ¬φ | φ ∨ φ | ∃x.φ
where x ∈ X and a ∈ Q.
The semantics of the new terms is given as follows (for an interpretation function I): – I(et ) = eI(t) – I(t1 · t2 ) = I(t1 ) · I(t2 )
Let NNL∗ be a shorthand for NNL[ReLU, NLReLU, σ, tanh]. We recall these activation functions in Figure 3.10. The decidability status of SAT(REF), also called Tarski’s exponential function problem, is unknown. We show a result, due to [21], stating that the problem is effectively equivalent to SAT(NNL∗ ). Theorem 3.9: Expressive Equivalence of NNL∗ and REF [21] We have NNL∗ ≤ REF and REF ≤ NNL∗ . 38
Feed-Forward Neural Networks Proof. The statement follows from the two propositions below. Proposition 3.6: We have NNL∗ ≤ REF. Proof. It remains to consider neural networks N = (L ) with L = (A, b, f ) and f = σ or f = tanh or f = NLReLU. Let m = in(L ) and n = out(L ). We construct an REF formula φN (x1 , . . . , xm , y1 , . . . , yn ) such that, for all real numbers r1 , . . . , rm , s1 , . . . , sn ∈ R, JN K(r1 , . . . , rm ) = (s1 , . . . , sn ) iff |= φN (r1 , . . . , rm , s1 , . . . , sn ) . We set φN (x1 , . . . , xm , y1 , . . . , yn ) =
n ^
i=1
where
∃z.
z = bi +
m X j=1
∧ αf (z, yi )
ai,j · xj .
yi · (1 + ez ) = ez if f = σ y · (e2z + 1) = (e2z − 1) if f = tanh i αf (z, yi ) = ! (z ≤ 0 ∧ yi = 0) if f = NLReLU ∨ (z > 0 ∧ eyi = z + 1)
The rest of the induction follows exactly the lines of the proof of Proposition 3.1. Now, we translate REF formulas into NNL∗ formulas. In the following, let η = NLReLU. Proposition 3.7: We have REF ≤poly NNL∗ . Towards the proof, we establish a series of intermediary results: Lemma 3.4: For every function f : R → R from {ReLU, η, σ, tanh, σ −1 , tanh−1 }, there is an NNL∗ formula φf (x, y) such that, for all interpretation functions I, we have I |= φf (x, y) iff f (I(x)) = I(y) . Proof. For f ∈ {ReLU, η, σ, tanh}, let Nf = (L ) where L = ((1), (0), f ). We have JNf K = f . Therefore, we can set φf (x, y) = (Nf (x) = y). Moreover, we let φσ−1 (x, y) = (Nσ (y) = x) and φtanh−1 (x, y) = (Ntanh (y) = x). Henceforth, we will write f (x) = y as a shorthand for φf (x, y).
39
Feed-Forward Neural Networks Lemma 3.5: There is an NNL∗ formula φln (x, y) such that, for all interpretation functions I, we have I |= φln (x, y) iff ln(I(x)) = I(y) . Proof. We will express ln in terms of σ −1 , tanh−1 , and η: – For all r ∈ R such that r ≥ 1: η(r − 1) = ln(r) – For all r ∈ R such that 0 < r < 1: σ −1 (r) = ln(r) − ln(1 − r) 1 tanh−1 (r) = (ln(1 + r) − ln(1 − r)) 2 σ −1 (r) − 2 tanh−1 (r) + η(r) = ln(r) − ln(1 − r) − ln(1 + r) + ln(1 − r) + ln(1 + r) = ln(r) Thus, we can set
x>0
∧ (x ≥ 1 ⇒ ∃z.(z = x − 1 ∧ η(z) = y)) y = z − 2 · z + z 1 2 3 . φln (x, y) = ∧ σ −1 (x) = z 1 ∧ (x < 1 ⇒ ∃z1 , z2 , z3 . −1 ∧ tanh (x) = z2 ∧ η(x) = z3
This concludes the proof. Lemma 3.6:
There is an NNL∗ formula φexp (x, y) such that, for all interpretation functions I, we have I |= φexp (x, y) iff eI(x) = I(y) . Proof. We set φexp (x, y) = φln (y, x) (obtained by exchanging x and y in φln (x, y)). Henceforth, we will write ex = y as a shorthand for φexp (x, y). Lemma 3.7: There is an NNL∗ formula φmult (x, y, z) such that, for all interpretation functions I, we have I |= φmult (x, y, z) iff I(x) · I(y) = I(z) . 40
Feed-Forward Neural Networks Proof. Recall that, for all r, s ∈ R with r, s > 0, we have r · s = eln(r)+ln(s) . We can set (x = 0 ∨ y = 0) ⇒ z = 0 ln(x) = z 1 ∧ (x > 0 ∧ y > 0) ⇒ ∃z1 , z2 , z3 . ∧ ln(y) = z2 ∧ z1 + z2 = z3 z 3 ∧ e = z ′ x = −x φmult (x, y, z) = ′ ln(x ) = z 1 ∧ ln(y) = z2 ∧ (x < 0 ∧ y > 0) ⇒ ∃z , z , z , x′ , z ′ . 1 2 3 ∧ z + z = z 1 2 3 ∧ e z3 = z ′ ′ ∧ z = −z ∧ ··· Completing the formula is left as an exercise. Exercise 3.12: Fill the dots in the definition of φmult (x, y, z) in the proof of Lemma 3.7. Henceforth, we will write x · y = z as a shorthand for φmult (x, y, z).
We are now ready to prove Proposition 3.7 stating that REF ≤ NNL∗ : Proof of Proposition 3.7. Consider a formula φ = (t1 ≤ t2 ) and let T be the set of subterms occurring in t1 or t2 . We replace φ with ∃(zt )t∈T .(zt1 ≤ zt2 ∧ ψt1 ∧ ψt2 ) where ψt1 and ψt2 are defined inductively by ψa ψx ψt+t′ ψt · t′ ψet
= = = = =
(za = a) (zx = x) (zt + zt′ = zt+t′ ∧ ψt ∧ ψt′ ) (zt · zt′ = zt · t′ ∧ ψt ∧ ψt′ ) (ezt = zet ∧ ψt )
Doing this with all inequalities t1 ≤ t2 , we obtain the desired NNL∗ formula.
41
Chapter 4 Recurrent Neural Networks Feed-forward neural networks process one single input vector and produce an output vector. In this chapter, we look at neural networks that process sequences. More precisely, they may translate sequences of input vectors into sequences of output vectors, or serve as sequence classifiers.
4.1
Definition and Semantics
We consider a simple class of recurrent neural networks, also known as Elman neural networks [14], rather than more advanced architectures such as long short-term memory (LSTM) [20]. Definition 4.1: Recurrent Neural Network A recurrent neural network (RNN) is a triple R = (L in , L out , h(0) ) where, for some m, n, o ∈ N+ , – L in is a feed-forward layer with dim(L in ) = (n + m, n),
– L out is a feed-forward layer with dim(L out ) = (n, o), – h(0) ∈ Qn is the initial (hidden) state vector. If L in uses activation function f and L out uses activation function g, we call R an (f, g)-RNN. We call – state(R) = n the state dimension of R (i.e., the dimension of each hidden state), – in(R) = m the input dimension of R (i.e., the dimension of each input symbol), – out(R) = o the output dimension of R (i.e., the dimension of each output symbol). However, states are considered to be hidden, and the type of the input-output relation is solely described by dim(R) = (m, o). When we see R as a sequence-to-sequence trans42
Recurrent Neural Networks
···
L in
h(τ−1) ∈ Rn
y(τ) ∈ Ro
y(τ+1) ∈ Ro
L out
L out
L in
h(τ) ∈ Rn
x(τ) ∈ Rm
h(τ+1) ∈ Rn
···
x(τ+1) ∈ Rm
Figure 4.1: Sequence processing by an RNN through time ducer1 , we consider the mapping ( (Rm )+ → (Ro )+ JRK : x(1) . . . x(ℓ) 7→ y(1) . . . y(ℓ) where, for all discrete time points τ ∈ {1, . . . , ℓ}, x(τ) )
□□
h(τ) = JL in K(h(τ−1) y(τ) = JL out K(h(τ) )
□□
Recall that h(τ−1) x(τ) is the vertical concatenation of h(τ−1) and x(τ) . The computation is illustrated in Figure 4.1. That is, along the way, R also computes a sequence of hidden states h(1) . . . h(ℓ) ∈ (Rn )+ . Note that JRK is length preserving, i.e., an input sequence containing ℓ vectors is always mapped to an output sequence containing ℓ vectors. □□
It can actually be useful to view R as an (infinite) automaton coming with a statetransition function δR : Rn × Rm → Rn defined by δR (h, x) = JL in K(h x), which is canonically extended to sequences. When considering R as a sequence-to-vector transducer, we would be interested in the mapping ( (Rm )+ → Ro ⟪R⟫ : w 7→ JL out K(δR (h(0) , w)) . RNNs as String Transducers. Though input and output symbols are vectors over real numbers, they allow us to deal with symbols from a finite alphabet as well. This is important in natural language processing, where words are considered as single symbols and are encoded, for example via one-hot encoding, as vectors. 1
We use the terms sequence and string interchangeably. However, we rather avoid the term word in this context. In NLP, words often refer to what we call letters (or tokens).
43
Recurrent Neural Networks Definition 4.2: One-Hot Encoding Let Σ be a finite alphabet with |Σ| = m. A one-hot encoding enc Σ of Σ is an injective mappingPΣ → {0, 1}m ⊆ Rm such that, for all α ∈ Σ, the vector x = enc Σ (α) satisfies m i=1 xi = 1. For example, for Σ = {α, β}, we may set enc Σ (α) = ⊤ (1, 0) and enc Σ (β) = (0, 1)⊤ .
The corresponding one-hot decoding is the mapping dec Σ : Rm → Σ defined by dec Σ (x) = α where α is such that min(argmax(enc Σ (α))) = min(argmax(x)). For example, we have dec Σ ((0.7, 0.5)⊤ ) = dec Σ ((0.5, 0.5)⊤ ) = α, and dec Σ ((0.2, 0.5)⊤ ) = β. Remark 4.1: Binary Alphabets If Σ is a binary alphabet such as {α0 , α1 }, we may also choose the dimension to be m = 1 and define enc Σ (αi ) = i as well as dec Σ (x) = α1 iff x > θ (or x ≥ θ) for some given threshold θ. This is particularly common in the output layer in combination with activation function σ and threshold θ = 0.5. The mappings enc Σ and dec Σ are extended to sequences as expected, i.e., enc Σ (α1 . . . αℓ ) = enc Σ (α1 ) . . . enc Σ (αℓ ) and dec Σ (x(1) . . . x(ℓ) ) = dec Σ (x(1) ) . . . dec Σ (x(ℓ) ). In the following, we assume that all finite alphabets come with their one-hot encoding/decoding. Let Σ and Γ be finite alphabets with associated one-hot encodings enc Σ and enc Γ , and decodings dec Σ and dec Γ . Furthermore, assume |Σ| = in(R) and |Γ| = out(R). Then, RNN R defines the mappings ( ( Σ+ → Γ+ Σ+ → Γ JRKΣ,Γ : ⟪R⟫Σ,Γ : w 7→ dec Γ (JRK(enc Σ (w))) w 7→ dec Γ (⟪R⟫(enc Σ (w))) Remark 4.2: Alternative Semantics If the activation function of L out is softmax, we may consider the mapping ( Σ+ → Distr (Γ) ⟪R⟫prob : Σ,Γ w 7→ ⟪R⟫(enc Σ (w)) where Distr (Γ) is the set of probability distributions over Γ. The idea is that, for the vector y = ⟪R⟫prob Σ,Γ (w), the probability of selecting β ∈ Γ as the next letter is ymin(argmax(enc Γ (β))) . This view has applications in character-level language modeling or text generation. In the context of reactive systems, which are supposed to run forever, it is particularly interesting to consider infinitary versions of JRK and ⟪R⟫, which are of the following form and whose definitions are as expected: JRKω : (Rm )ω → (Ro )ω
JRKωΣ,Γ : Σω → Γω 44
Recurrent Neural Networks RNNs as String Classifiers. Let R be an RNN and m = in(R). If out(L out ) = 1, then R can be viewed as a classifier of strings over Rm : For ▷◁ ∈ {≥, >, =} and θ ∈ R, we define L▷◁ θ (R) = {w ∈ (Rm )+ | ⟪R⟫(w) ▷◁ θ} to be the language of R, i.e., the set of strings that have a sufficient “score“, or acceptance probability, and are therefore classified by R as positive.2 Suppose we are given a finite alphabet Σ. The RNN R is called an RNN over Σ if m = |Σ|. Like above, R can then take one-hot encoded letters from Σ as inputs. If, again, out(L out ) = 1, we can interpret R as a classifier of strings over Σ. For ▷◁ ∈ {≥, >, =} and θ ∈ R, we let + θ L▷◁ Σ (R) = {w ∈ Σ | ⟪R⟫(enc Σ (w)) ▷◁ θ} be the language of R over Σ. Example 4.1: Example Applications of RNNs Among the classical practical applications of RNNs, let us mention price prediction, text translation, or text classification. Several concrete use cases are given in the blog article [23]. Consider, for example, an email spam classifier that processes a text, i.e., a sequence over a finite alphabet Σ (where each letter represents a single word), and outputs a probability of being classified as spam. In other words, we θ are interested in filtering emails contained in a language of the form L≥ Σ (R). Here, it is up to the user to decide on the threshold θ to achieve a reasonable trade-off between sensitivity (true positive rate) and specificity (true negative rate).
4.2
Undecidability of the Emptiness Problem
In this section, we demonstrate that, unfortunately, determining the emptiness of the language of a given RNN, when treated as a string classifier, is undecidable. Theorem 4.1: Undecidability of RNN Language (Non)emptiness For all ▷◁ ∈ {≥, >, =}, the following decision problem is undecidable: Input: A finite alphabet Σ and a (ReLU, σ)-RNN R over Σ with out(R) = 1. ▷◁ 1
Question: Do we have LΣ 2 (R) ̸= ∅ ? As this fundamental decision problem is already undecidable for RNNs, this will also be the case for the majority of non-trivial verification tasks. Thus, it is important to identify suitable abstractions or restrictions. There has been an ongoing and fruitful effort to establish positive verification results specifically designed for RNNs [1, 22, 25, 41, 52]. The rest of this section is dedicated to the proof of Theorem 4.1. We first show that (ReLU, σ)-RNNs can simulate all probabilistic finite automata (PFAs). PFAs were introIf the activation function of L out is the sigmoid function σ, we can also interpret the score as acceptance probability. 2
45
Recurrent Neural Networks duced and studied by Rabin [40]. Their (non)emptiness problem is undecidable and they are strictly more expressive than finite automata. Definition 4.3: Probabilistic Finite Automaton (PFA) Let Σ be a finite alphabet. A probabilistic finite automaton (PFA) over Σ is a tuple A = ((Pα )α∈Σ , λ, γ) where, for some n ∈ N+ , P – Pα = (pαj,i ) ∈ ([0, 1] ∩ Q)n×n such that, for all i ∈ {1, . . . , n}, nj=1 pαj,i = 1, P – λ ∈ {0, 1}n is the initial state vector (a column vector) such that ni=1 λi = 1, – γ ∈ {0, 1}n is the final state vector (a row vector).
Note that Pα is a left stochastic matrix. We call it the transition-probability matrix of α ∈ Σ. The intuition is that A has an (implicit) set of states Q = {q1 , . . . , qn }, and pαj,i is the probability that, when reading α in state qi , we go to state qj .3 Thus, A has an equivalent representation as a state-transition graph (Q, ι, ∆, F ), which is basically a finite automaton with transition probabilities. The initial state is ι = qi for λi = 1, and the set of final states is F = {qi | i ∈ {1, . . . , n} with γi = 1}. Moreover, we have a set of transitions ∆ ⊆ Q × Σ × (0, 1] × Q containing, for all α ∈ Σ and all i, j ∈ {1, . . . , n} such that pαj,i > 0, the transition (qi , α, pαj,i , qj ). We will switch between these representations at discretion. PFA A defines the mapping ( Rn × Σ → Rn δA : (x, α) 7→ Pα · x . Suppose that δA gets (x, α) as arguments and that x represents a probability distribution over {q1 , . . . , qn }, i.e., xi is the probability of being in state qi . Then, letting x′ = δA (x, α), x′i can naturally be interpreted as the probability of being in state qi after reading α. Using the extension of δA to strings, we obtain the mapping ( Σ∗ → [0, 1] JAK : w 7→ γ · δA (λ, w) . Thus, starting from the initial state, JAK(w) is the probability of reaching a final state after reading w. Finally, for ▷◁ ∈ {≥, >, =} and θ ∈ [0, 1], we define the language L▷◁ θ (A) = {w ∈ Σ+ | JAK(w) ▷◁ θ} . We restrict to nonempty strings here, aligning with the definition of RNN languages.
3
α We choose pα j,i rather than the more standard pi,j , as it reflects the way computations are represented in the layers of RNNs, where the transition matrix on the left is multiplied with the current state on the right-hand side.
46
Recurrent Neural Networks Remark 4.3: Reactive vs. Generative Probabilistic Automata PFAs due to Rabin are also called reactive, as they yield a probability distribution when providing an input. On the other hand, generative probabilistic automata (also called Segala automata [45]) generate the next letter according to a probability distribution over Σ × Q. In formal terms, we may consider that reactive PFAs (as we study here) are equipped with a transition function δ : Q × Σ → Distr (Q), whereas generative PFAs have a transition function of type δ : Q → Distr (Σ × Q). Example 4.2: Probabilistic0 Finite Automaton1 1
Let Σ = {α, β}. Consider the PFA A = ((Pα , Pβ ), λ, γ) over Σ given by q0 q1 ! ! ! 1 1 1 0 1 3 3 β λ= Pα = P = γ= 1 0 0 2 2 0 1 0 3 3 Alternatively, A can be represented by its state-transition diagram: α 13
α 23
α 23
β
q1
q2 α 13
β
For k ∈ N, we have k
JAK(αβ ) = 1 0 ·
0 1 1 0
!k
·
1 3
1 3
2 3
2 3
!
·
! 1 0
=
1 3 2 3
if k is even if k is odd
It is easy to see that every string ending in α leads to the final state with proba1 bility 31 . Thus, no such string is in L≥ 2 (A). Altogether, we obtain 1
L≥ 2 (A) = {β k | k ∈ N+ is even} ∪ {wαβ k | w ∈ {α, β}∗ and k is odd} . Note that the image of JAK is finite since we have JAK(w) ∈ {0, 13 , 23 , 1} for all w ∈ Σ+ . In general, however, this is not the case. PFAs enjoy some essential closure properties: Lemma 4.1: Closure Properties of PFAs Let Σ be a finite alphabet, p ∈ [0, 1] be rational, and A and B be PFAs over Σ. We can effectively construct PFAs C1 , C2 , C3 over Σ such that, for all w ∈ Σ+ , – JC1 K(w) = 1 − JAK(w),
– JC2 K(w) = p · JAK(w) + (1 − p) · JBK(w), and
47
Recurrent Neural Networks
– JC3 K(w) = JAK(w) · JBK(w). Exercise 4.1: Prove Lemma 4.1. The next theorem states that RNNs with a particular set of activation functions are at least as expressive as PFAs. It constitutes the first step towards showing that emptiness of RNNs is undecidable. Theorem 4.2: RNNs Recognize All PFA Languages Let Σ be a finite alphabet and A be a PFA over Σ. Moreover, let ▷◁ ∈ {≥, >, =} and θ ∈ [0, 1] be rational. We can effectively construct a (ReLU, σ)-RNN R over Σ such that out(R) = 1 and ▷◁ 1
LΣ 2 (R) = L▷◁ θ (A) . Before we prove the theorem formally, we illustrate the construction using an example. Example 4.3: From PFAs to RNNs An obvious first idea is to choose L in such that in(L in ) = |Σ| (with one-hot encoded letters as inputs) and state(L in ) = |Q| as state dimension. The corresponding matrix Ain would then have dimension |Q| × (|Q| + |Σ|). However, in A, we have |Σ| · |Q|2 transition probabilities, which thus may not fit into Ain .
The solution will be to “augment” the set of states so that every state has incoming transitions of a unique letter type. Consider, for example, the PFA A from Example 4.2. Recall that Σ = {α, β} and suppose enc Σ (α) = (1, 0)⊤ and enc Σ (β) = (0, 1)⊤ . The PFA A′ illustrated in Figure 4.2a, is equivalent to the PFA A from Example 4.2, i.e., JAK(w) = JA′ K(w) for all w ∈ Σ∗ . However, every state of A′ now has only incoming transitions labeled with a dedicated letter α or β (which we accordingly call an α- or β-state). Note that A′ is given by the following ingredients: 1 1 1 1 0 0 0 0 1 3 3 3 3 2 2 2 2 0 0 0 0 0 3 3 3 3 β α 1 0 1 0 P = γ = P = λ= 0 1 0 1 0 0 0 0 0 0 0 0 0 1 0 1 0 0
Thanks to the transformation, the transition-probability matrices Pα and Pβ no longer “overlap”: for all i, j ∈ {1, 2, 3, 4}, at most one of pαj,i and pβj,i is non-zero. That is, the sum Pα and Pβ accommodates all probabilities occurring in A′ in a single matrix of dimension R4×4 . The layer L in of the desired RNN is illustrated in Figure 4.2b for a neuron belonging to the α-state q2 . If the input letter is α, i.e., the input vector is (1, 0)⊤ , the output neuron indeed receives the updated probability
48
q1
Recurrent Neural Networks
q1 q1
2 3
q2
q2 h q3
2 3 2 3 2 3
ReLU
q3
−1
ReLU
−1
q2
q4
q4
1
q2
α 13
q x41
α 23
0
x x2
β
(a) PFA A′ where every state has a unique “incoming letter”
(b) A neuron for target α-state q2
Figure 4.2: Simulating a PFA with an RNN
of being in q2 after processing the input. If, on the other hand, the input is β and, respectively, (0, 1)⊤ , then the result before applying ReLU will be ≤ 0 so that the overall result is 0. As q2 is an α-state, the probability of being in q2 after processing β is indeed 0. The study of the expressive power of RNNs and their extensions and variants in terms of formal languages has a long tradition and is still an active research field [35]. In this context, a prominent result by Siegelmann and Sontag states that RNNs can simulate all Turing machines [47]. A general technique of transforming finite-state machines into equivalent RNNs goes back to Minsky [36]. It has recently been generalized to deterministic generative PFAs [49], which define probability distributions over Σ∗ (cf. Remark 4.2). Here, we apply this technique to translate (reactive) PFAs into RNNs, aiming to show undecidability of the RNN emptiness problem. Now, let us formally prove Theorem 4.2. Proof of Theorem 4.2. Let Σ be a finite alphabet and m = |Σ|. Let A = ((Pα )α∈Σ , λ, γ) be a PFA over Σ, with state-transition representation (Q, ι, ∆, F ) where Q = {q1 , . . . , qn }. Moreover, fix ▷◁ ∈ {≥, >, =} and a rational number θ ∈ [0, 1]. Without loss of generality, we assume that, for every i1 , i2 , j ∈ {1, . . . , n}, α, β ∈ Σ, and p1 , p2 ∈ (0, 1] such that (qi1 , α, p1 , qj ) ∈ ∆ and (qi2 , β, p2 , qj ) ∈ ∆, we have α = β.4 We call 4
If A does not satisfy this property, we can convert it as follows. Choose some β0 ∈ Σ, replace Q by Q × Σ, and take (ι, β0 ) as initial state. For all (qi , α, p, qj ) ∈ ∆ and β ∈ Σ, add the transition ((qi , β), α, p, (qj , α)). The final states are F × Σ. Thus, after reading a nonempty prefix ending in α, the second component records that last input letter; the first component has exactly the same distribution
49
q3 α 13 α 23 β
Recurrent Neural Networks state qj whose incoming transitions all carry letter α an α-state. Note that the transition probability matrices are not “overlapping”, i.e., for all α, β ∈ Σ and i, j ∈ {1, . . . , n} such that pαj,i > 0 and pβj,i > 0, we have α = β. We now formally construct the corresponding (ReLU, σ)-RNN R = (L in , L out , h(0) ) over ▷◁ 1
Σ such that out(L out ) = 1 and LΣ 2 (R) = L▷◁ θ (A). – We let h(0) = λ.
– Define L in = (Ain , bin , ReLU) as follows: Let Ain = P □□ C be the concatenation of the matrices P ∈ [0, 1]n×n and C ∈ {0, 1}n×m defined by X P= Pα α∈Σ
and, for all j ∈ {1, . . . , n} and k ∈ {1, . . . , m}, 1 if there is α ∈ Σ such that qj is an α-state and min(argmax(enc Σ (α))) = k cj,k = 0 otherwise. Finally, for all j ∈ {1, . . . , n}, we set bin j = −1.
– We define L out = (Aout , bout , σ) by Aout = γ and bout = (−θ).
δR (h, enc Σ (α)) = δR (h, x) = JL in K(h
x)
x) + bin )
□□
= ReLU((P □□ C) · (h
x) + bin )
□□
= ReLU(Ain · (h
□□
Correctness Proof. Let us show that, for all hidden states h ∈ [0, 1]n and α ∈ Σ, δR (h, enc Σ (α)) = δA (h, α). Let x = enc Σ (α). We have
= ReLU(P · h + C · x + bin ) P = ReLU(( β∈Σ Pβ ) · h + C · x + bin )
Let y = (y1 , . . . , yn )⊤ = C · x + bin . For all j ∈ {1, . . . , n}, we have ( 0 if qj is an α-state yj = −1 otherwise.
P Thus, letting z = ( β∈Σ Pβ ) · h + y ∈ Rn , we get, for all j ∈ {1, . . . , n}, ( zj = Pαj · h if qj is an α-state zj ≤ 0 otherwise. where Pαj is the j-th row of Pα . We conclude δR (h, enc Σ (α)) = ReLU(z) = Pα · h = δA (h, α) . as in A. Hence the resulting PFA is equivalent to A on all words.
50
Recurrent Neural Networks With this, we obtain that, for all w ∈ Σ+ , ⟪R⟫(enc Σ (w)) ▷◁ 12 iff JL out K(δR (h(0) , enc Σ (w))) ▷◁ 12 iff JL out K(δA (λ, w)) ▷◁ 12
iff σ(γ · δA (λ, w) − θ) ▷◁ 12 iff γ · δA (λ, w) − θ ▷◁ 0 iff γ · δA (λ, w) ▷◁ θ iff JAK(w) ▷◁ θ ▷◁ 1
We have shown LΣ 2 (R) = L▷◁ θ (A). To prove Theorem 4.1, i.e., undecidability of RNN language emptiness, it remains to establish the corresponding facts for PFAs, depending on ▷◁ ∈ {≥, >, =}. The following undecidability results for PFAs are due to [5] and [38]. The proofs were later simplified and strengthened in [16]. For a concise overview of what is decidable and undecidable in PFAs, we refer to [15]. Theorem 4.3: Undecidability of PFA Language Emptiness [5, 38] The following three decision problems are undecidable: Input: A finite alphabet Σ and a PFA A over Σ. 1
Question 1: Do we have L= 2 (A) ̸= ∅ (i.e., JAK(w) = 12 for some w ∈ Σ+ )? 1
Question 2: Do we have L≥ 4 (A) ̸= ∅ ? 1
Question 3: Do we have L> 8 (A) ̸= ∅ ? Proof. We first consider Question 1. The proof is a reduction from the following modified Post’s correspondence problem (modified PCP)5 . Input: A finite alphabet Σ and morphisms f1 , f2 : Σ∗ → {0, 1}∗ such that fi (α) ∈ 1(0 + 1)∗ for all i ∈ {1, 2} and α ∈ Σ. Question: Is there w ∈ Σ+ such that f1 (w) = f2 (w)? Given an instance f1 , f2 of the modified PCP, we will effectively construct a PFA A over Σ such that, for all w ∈ Σ+ , we have f1 (w) = f2 (w) iff JAK(w) = 21 , which implies the theorem. The standard undecidable PCP does not have the restriction fi (α) ∈ 1(0 + 1)∗ . However, when we start with an unrestricted instance of the form g1 , g2 : Σ → {0, 1}+ , we can translate it into f1 , f2 : Σ → {0, 1}∗ defined by fi = f ◦ gi where f : {0, 1}∗ → {0, 1}∗ is the morphism given by f (0) = 10 and f (1) = 11. Then, fi (α) starts with 1 for all α ∈ Σ. Moreover, we easily see that g1 (w) = g2 (w) for some w ∈ Σ+ iff f1 (w) = f2 (w) for some w ∈ Σ+ 5
51
Recurrent Neural Networks Let ε = 0 and, for u1 . . . uk ∈ {0, 1} with k ≥ 1, u1 . . . uk = 0.uk uk−1 . . . u1 (in binary) =
uk uk−1 u1 + + . . . + . 21 22 2k
Thanks to the modified PCP, we have, for all w ∈ Σ∗ , f1 (w) = f2 (w) iff f1 (w) = f2 (w). Towards the PFA A, we will construct two PFAs A1 and A2 over Σ such that, for all i ∈ {1, 2} and w ∈ Σ∗ , we get JAi K(w) = fi (w) .
(4.1)
We then combine A1 and A2 using Lemma 4.1 and obtain a PFA A over Σ such that, for all w ∈ Σ∗ , 1 JAK(w) = (JA1 K(w) + (1 − JA2 K(w))) . 2 1 Then, we are done as JAK(w) = 2 iff f1 (w) = f2 (w) iff f1 (w) = f2 (w). PFA Evaluating Binary Numbers. The main building block in the construction of both A1 and A2 will be a PFA B = ((P0 , P1 ), λ, γ) over {0, 1} such that, for all ν ∈ {0, 1}∗ , JBK(ν) = ν.6 Thus, B “evaluates” ν. It is given by ! ! ! 1 1 1 21 0 2 λ= P0 = P1 = γ= 0 1 1 0 12 0 1 2 We show JBK(ν) = ν, by induction on k = |ν|. The claim clearly holds for k = 0, i.e., ν = ε. Moreover, for the case k = 1, JBK(0) = p02,1 = 0.0 = 0 and
JBK(1) = p12,1 = 0.1 = 1
Now suppose, for ν = u1 . . . uk with k ≥ 1, that JBK(ν) = ν holds. Moreover, assume ! 1−p δB (λ, ν) = p for suitable p ∈ [0, 1]. In particular, p = JBK(ν) = ν .
Let u ∈ {0, 1}. We have
JBK(u1 . . . uk u) = 0 1 · Pu · = 6
1−p p
!
=
p 2
1 p + 2 2
(4.2)
if u = 0
if u = 1
u p (4.2) + = 0.u + 0.0uk . . . u1 = 0.uuk . . . u1 = u1 . . . uk u 2 2
Note that P0 and P1 should not be confused with powers of some matrix P.
52
Recurrent Neural Networks Construction of A. Let i ∈ {1, 2}. Building on the PFA B = ((P0 , P1 ), λ, γ), we now construct the PFA Ai = ((Pα )α∈Σ , λ, γ) over Σ such that, for all strings w ∈ Σ∗ , we have JAi K(w) = fi (w). For ν = u1 . . . uk with k ≥ 1, define Pν = Puk · . . . · Pu1 . With this, given a letter α ∈ Σ, we let Pα = Pfi (α) . Indeed, for all w = α1 . . . αℓ ∈ Σ∗ , we obtain JAi K(w) = γ · Pαℓ · . . . · Pα1 · λ
= γ · Pfi (αℓ ) · . . . · Pfi (α1 ) · λ
= γ · Pfi (w) · λ = fi (w) .
This concludes the proof of undecidability of the first problem. Questions 2 and 3. Question 1 can be reduced to Question 2 as follows: From the given PFA A, we construct, using Lemma 4.1, a PFA B over Σ such that, for all w ∈ Σ∗ , we have JBK(w) = JAK(w) · (1 − JAK(w)) .
Note that 14 is the global maximum of the function r 7→ r · (1 − r), which is only reached for the argument r = 12 . Thus, we have JBK(w) ≥ 41 iff JAK(w) = 12 . Undecidability of Question 3 can be obtained by analyzing the transition probabilities in the automata considered so far. We refer the reader to [16].
We have now shown Theorem 4.1, using the effective constructions from Theorems 4.2 and 4.3 to reduce PFA emptiness problems for ▷◁ ∈ {≥, >, =} to RNN emptiness. Specifically, for every PFA A over Σ, we constructed (ReLU, σ)-RNNs R1 , R2 , R3 over Σ whose output layers have output dimension 1 and such that the following hold: =1
1
≥1
1
>1
1
LΣ 2 (R1 ) = L= 2 (A) LΣ 2 (R2 ) = L≥ 4 (A) LΣ 2 (R3 ) = L> 8 (A) Exercise 4.2: Explicitly determine a (ReLU, σ)-RNN R over Σ = {a} with out(R) = 1 such that ≥1
LΣ 2 (R) = {(aa)n | n ∈ N+ }. Exercise 4.3:
For (local) activation functions f, g : R → R, we define the decision problem RNN-NonEmptiness(f, g) as follows: Input: A finite alphabet Σ and an (f, g)-RNN R over Σ with out(R) = 1. ≥1
Question: Do we have LΣ 2 (R) ̸= ∅ ? (a) Show that RNN-NonEmptiness(ReLU, ReLU) is undecidable. (b) Show that RNN-NonEmptiness(heaviside, ReLU) is decidable.
53
Chapter 5 Attention and Transformers Transformers have been introduced by Vaswani et al. as a powerful alternative to RNNs and their variants [54]. Like RNNs, transformers can be used as sequence-to-sequence transducers, as they process sequences of arbitrary length. For language-recognition tasks, we will consider only the encoder (or decoder) part, as is the case in popular language-model architectures like BERT and GPT. Verification issues for transformers have only been addressed sparingly so far. The main purpose of this chapter is to highlight a few interesting questions for future research.
5.1
Attention
An essential component of a transformer is attention, specifically, an attention head. There is an analogy between attention heads and channels of convolutional neural networks. Both allow the network to focus on different aspects and parts of an input. Therefore, one usually has several attention heads per layer. Definition 5.1: Attention Head An attention head H = (Q, K, V) is given by three matrices (i.e., linear transformations) Q, K ∈ Qnkey ×n and V ∈ Qnvalue ×n for some n, nkey , nvalue ∈ N+ . They are respectively called query, key, and value matrix. We let in(H) = n, out(H) = nvalue , and dim(H) = (n, nvalue ). Later, we will see that n can be understood as the dimension of the hidden state of a transformer. Attention head H defines a mapping ( (Rn )+ × Rn → Rnvalue JHK : (z(1) . . . z(ℓ) , x) 7→ y which allows it to situate a vector (word/letter embedding or hidden state) inside a whole sequence. Let q = Q · x. Moreover, for i ∈ {1, . . . , ℓ}, let k(i) = K · z(i) and v(i) = V · z(i) . The semantics y = JHK(z(1) . . . z(ℓ) , x) is then given by y=
ℓ X i=1
pi · v(i)
54
Attention and Transformers !
!
p1
pj · v(j)
p2
"#
y
=
p3
pℓ
···
$
softmax* a1
a2
a3
aℓ
k(1)
v(1)
k(2)
v(2)
k(3)
v(3)
K
V
K
V
K
V
z(1)
z(2)
z(3)
···
k(ℓ)
v(ℓ)
K
V
···
q Q x
z(ℓ)
Figure 5.1: Illustration of an attention head H = (Q, K, V) where (p1 , . . . , pℓ ) = Weights(a1 , . . . , aℓ ) with ai = √
1 · (q⊤ · k(i) ) . nkey
The scaling parameter √n1key is optional. The function Weights : R+ → R+ is a lengthpreserving weight function. Usually, one chooses Weights = softmax∗ : R+ → R+ , where the latter is softmax adapted for sequences, i.e., for a variable number of input arguments, instead of a fixed number of input values. For theoretical considerations, one sometimes replaces softmax∗ by other weight functions, in particular: – min-argmax∗ : R+ → {0, 1}+ , also called leftmost-hard attention, and – avg-argmax∗ : R+ → R+ , called average-hard attention.
Here, min-argmax∗ (x1 , . . . , xℓ ) = (b1 , . . . , bℓ ) where bi = 1 iff i = min(argmax(x1 , . . . , xℓ )). For example, min-argmax∗ (3, 7, 4, 7) = (0, 1, 0, 0). Moreover, avg-argmax∗ takes the average for all maximal elements, i.e., avg-argmax∗ (x1 , . . . , xℓ ) = (b1 , . . . , bℓ ) where bi =
1 |argmax(x1 , . . . , xℓ )|
for all i ∈ argmax(x1 , . . . , xℓ ), and bi = 0 for all other i. avg-argmax∗ (3, 7, 4, 7) = (0, 0.5, 0, 0.5).
For example, we have
The working principle of attention heads is illustrated in Figure 5.1. In the following, we develop an attention head that will later serve as a building block of transformers (cf. Examples 5.2 and 5.3).
55
Attention and Transformers Exercise 5.1: Attention Head Computing the Maximum Define an attention head Hmax = (Q, K, V), using avg-argmax∗ as weight function and with parameters n = 3 and nkey = nvalue = 1, such that JHmax K : (R3 )+ × R3 → R where, for all z1 , . . . , zℓ , x ∈ R, JHmax K((z1 , 0, 1)⊤ . . . (zℓ , 0, 1)⊤ , (x, 0, 1)⊤ ) = max{z1 , . . . , zℓ } . Solution: Note that dim(Hmax ) = (3, 1). The matrices can be chosen as follows: Q= 0 0 1 K=V= 1 0 0
This actually also works with min-argmax∗ instead of avg-argmax∗ . An illustration of Hmax can be found in Figure 5.5. Several attention heads can be combined to form layers. Definition 5.2: Multi-Head Attention Layer A (multi-head) attention layer A = (H(1) , . . . , H(d) , W) has d ≥ 1 attention heads H(i) = (Q(i) , K(i) , V(i) ) and one additional linear transformation in terms of a matrix W. We require that all attention heads share the same dimensions n, nkey , nvalue ∈ N+ and that W ∈ Qn×(d · nvalue ) . We let in(A ) = out(A ) = n and dim(A ) = (n, n). We can assign to A three different semantics: – The (cross-)attention semantics is given by ( (Rn )+ × (Rn )+ → (Rn )+ JA K : (w, x(1) . . . x(ℓ) ) 7→ y(1) . . . y(ℓ) ...
H(d) (w, x(i) )) .
□□
y(i) = W · (H(1) (w, x(i) )
□□
where – The self-attention semantics is defined by ( (Rn )+ → (Rn )+ JA Kself : w 7→ JA K(w, w) . – Finally, the masked self-attention semantics is defined by ( (Rn )+ → (Rn )+ JA Kmasked : x(1) . . . x(ℓ) 7→ y(1) . . . y(ℓ)
56
...
H(d) (wi , x(i) )) .
□□
y(i) = W · (H(1) (wi , x(i) )
□□
where (letting wi = x(1) . . . x(i) )
Attention and Transformers head H(d)
h(d,i)
···
h(1,i)
h !
head H(1)
!
=
"#
···
(2,i)
y
(i)
= W·
h(1,i)
···
h(2,i)
head H(2)
h(d,i)
$
softmax*
K(1)
K(1)
V(1) x(1)
···
···
···
V(1)
K(1)
x(i−1)
(1) V(1) Q
x(i)
x(i+1)
···
x(ℓ)
Figure 5.2: A multi-head attention layer with masked self-attention semantics Note that JA Kself and JA Kmasked are length-preserving, and JA K is length-preserving in the second argument. Masked self-attention is illustrated in Figure 5.2. Example 5.1: Attention Layer We continue Exercise 5.1. Let Hmax be the attention head developed there. We obtain a (single-head) attention layer Amax when we add the matrix Wmax = (0, 1, 0)⊤ ∈ Q3×1 , which writes the result delivered by Hmax into the second component of the three-dimensional zero-vector. For an illustration, consider Figure 5.7.
5.2
The Transformer Architecture
Encoder Layer. An encoder layer is of the form E = (A , N ). It has two components, a multi-head attention layer A (with self-attention semantics) and a feed-forward neural network N with dim(A ) = dim(N ) = (n, n) for some n ∈ N+ .1 Abusing notation, JN K can be extended to a mapping (Rn )+ → (Rn )+ letting JN K(x(1) . . . x(ℓ) ) = JN K(x(1) ) . . . JN K(x(ℓ) ). We can now define JEK : (Rn )+ → (Rn )+ by JEK(w) = Norm(w b + JN K(w)) b
1
where w b = Norm(w + JA Kself (w)) .
Typically (but not mandatorily), N is a two-layer neural network with ReLU and id as activation functions, respectively.
57
Attention and Transformers ···
···
Norm
Norm
Norm
+
+
+
feed forward
feed forward
Norm
Norm
Norm
+
+
+
···
feed forward
Norm
Norm
Norm
+
+
+
feed forward
feed forward
Norm
Norm
Norm
Norm
Norm
Norm
+
+
+
+
+
+
feed forward
···
···
cross attention ···
self-attention
masked self-attention ···
···
···
···
Figure 5.3: The interplay between an encoder layer (left) and a decoder layer (right) Here, Norm : (Rn )+ → (Rn )+ is the length-preserving layer norm 2 and addition is position-wise (thus length preserving, too). Accordingly, we define dim(E) = (n, n). The structure of an encoder layer is illustrated on the left-hand side of Figure 5.3. Remark 5.1: Normalization and Addition Optionally, the layer norm(s) may be chosen to be the identity function. Moreover, addition (also called residual connection) may be omitted. However, both greatly help in the training process of transformers. Moreover, in some applications one may consider adopting the masked self-attention semantics. That is, alternative semantics for encoder layer E can be given as JEK = JN K ◦ JA Kself
or JEK = JN K ◦ JA Kmasked . Decoder Layer. A decoder layer is similar to an encoder layer, but since part of its input comes from an encoder layer, its semantics is described in a different way. A decoder layer (of dimension n) is of the form D = (A (1) , A (2) , N ). It features two multi-head attention layers A (1) and A (2) and, like the encoder layer, a feed-forward neural network 2
The layer norm usually includes learnable parameters, which we omit in the definition of E for simplicity.
58
Attention and Transformers N such that dim(A (1) ) = dim(A (2) ) = dim(N ) = (n, n). Its semantics is a mapping JDK : (Rn )+ × (Rn )+ → (Rn )+ defined by JDK(wenc , w) = Norm(w2 + JN K(w2 )) where w2 = Norm(w1 + JA (2) K(wenc , w1 )) w1 = Norm(w + JA (1) Kmasked (w)) . Thus, A (1) is actually a masked multi-head attention layer, and A (2) is a cross multi-head attention layer. We define dim(D) = (n, n). Note that JDK is length-preserving in its second argument. The decoder layer is illustrated on the right-hand side of Figure 5.3. Note that Remark 5.1 applies here as well, i.e., normalization and residual connections are optional. However, in NLP tasks, applying the masked-self attention semantics in decoder layers allows one to feed complete input and output sequences during training while avoiding that the decoder can “look into the future”. In fact, its decisions should be based solely on what it has read/produced so far. Transformer. Transformers were initially introduced for machine translation. For that case, we assume ordered finite alphabets Σ and Γ (of words or tokens). We assume that Γ contains a start-of-sequence symbol SOS and an end-of-sequence symbol EOS. They indicate when the translation of the output sentence will start and end, respectively. The semantics of a transformer T over Σ and Γ will define a (partial and not necessarily length-preserving) mapping JT KΣ,Γ : Σ+ → Γ∗ .
We start with a length-preserving encoding of the input sequence, realized by an embedding embΣ : Σ+ → (Qn )+ . It is obtained from a word embedding 3 WEΣ : Σ → Qn and a positional encoding PE : N+ → Qn and defined, for w = α1 . . . αℓ ∈ Σ+ by embΣ (w) = x(1) . . . x(ℓ) where x(i) = WEΣ (αi ) + PE(i). We include the mappings embΣ and embΓ in the definition of a transformer, as they are in principle learnable. A transformer consists of a stack of encoder layers and a stack of decoder layers.4 Definition 5.3: Transformer A (machine-translation) transformer with hidden-state dimension n ∈ N+ over Σ and Γ is a tuple T = (embΣ , embΓ , (E (1) , . . . , E (κ) ), (D(1) , . . . , D(κ) ), Nout ) such that – embΣ : Σ+ → (Qn )+ and embΓ : Γ+ → (Qn )+ are embeddings, – E (1) , . . . , E (κ) are encoder layers with dim(E (i) ) = (n, n), – D(1) , . . . , D(κ) are decoder layers with dim(D(i) ) = (n, n), 3
The one-hot encoding enc Σ is a special case of a word embedding. RNNs and LSTMs can also be presented in that way, especially when we consider text generation. We will present transformers in their full form, but then focus on encoders and their capability as language recognizers. 4
59
Attention and Transformers
softmax neural network
encoder layer
decoder layer
encoder layer
decoder layer
encoder layer
decoder layer
input embedding
output embedding (shifted)
Figure 5.4: The interplay between encoder layers (left) and decoder layers (right)
– Nout is a feed-forward neural network with a softmax activation function in its last layer and dim(Nout ) = (n, |Γ|). + + → Γ, Before defining JT KΣ,Γ , we define an intermediate semantics JT Knext Σ,Γ : Σ × Γ + + which, for a given input sequence win ∈ Σ and an output sequence wout ∈ Γ generated so far, provides the next output letter JT Knext Σ,Γ (win , wout ) ∈ Γ to be appended to wout . To determine JT Knext (w , w ), we compute in out Σ,Γ (κ)
(κ−1)
win = JE (κ) K(win
(κ)
(κ)
(κ−1)
(2)
(κ)
(1)
(1)
(κ)
(0)
wout = JD(κ) K(win , wout )
)
.. .
.. .
(2)
(1)
wout = JD(2) K(win , wout )
(1)
(0)
wout = JD(1) K(win , wout )
win = JE (2) K(win ) win = JE (1) K(win ) (0)
(0)
win = embΣ (win )
wout = embΓ (wout )
This interplay between encoder and decoder layers is illustrated in Figures 5.3 and 5.4. With this, JT Knext Σ,Γ (win , wout ) is the min(argmax(Nout (x)))-th letter from Γ where x is the (κ) last vector in wout . Now, SOS is a dummy symbol that allows the decoder to produce a first output. Thus, JT Knext Σ,Γ (win , SOS) generates the first letter after “reading” the input 60
Attention and Transformers string win . Continuing this scheme, we let β1 = JT Knext Σ,Γ (win , SOS)
β2 = JT Knext Σ,Γ (win , SOS β1 )
β3 = JT Knext Σ,Γ (win , SOS β1 β2 ) .. .
Consider the smallest index ℓ ≥ 0 such that βℓ+1 = EOS. If ℓ does not exist, JT KΣ,Γ (win ) is undefined. Otherwise, JT KΣ,Γ (win ) = β1 . . . βℓ .
5.3
Encoder-Only Transformers
Based on the general transformer architecture, we now extract simple architectures, solely based on encoder layers, that define simpler functions or serve as language recognizers. Henceforth, all encoder layers E = (A , N ) may or may not use masked self-attention. Also recall that residual connections and the normalization are optional in every layer. Definition 5.4: Encoder-Only Transformer An encoder-only transformer is a tuple T = (Nin , E (1) , . . . , E (κ) , Nout ) where, for some m, n, o ∈ N+ , – Nin and Nout are feed-forward neural networks with dim(Nin ) = (m, n) and dim(Nout ) = (n, o), and – E (1) , . . . , E (κ) are encoder layers with dim(E (i) ) = (n, n). Similarly to RNNs, we let in(T ) = m, out(T ) = o, dim(T ) = (m, o), and state(T ) = n. Analogously, we can now define a length-preserving mapping JT K : (Rm )+ → (Ro )+ as the function composition JT K = JNout K ◦ JE (κ) K ◦ . . . ◦ JE (1) K ◦ JNin K
where, again, JNin K and JNout K are straightforwardly extended to sequences. We also define ⟪T ⟫ : (Rm )+ → Ro such that ⟪T ⟫(w) returns the last vector in the sequence JT K(w).
Just as for RNNs, we can view an encoder-only transformer as a sequence classifier. Suppose dim(T ) = (m, 1). Then, for ▷◁ ∈ {≥, >, =} and θ ∈ R, we can define the language L▷◁ θ (T ) = {w ∈ (Rm )+ | ⟪T ⟫(w) ▷◁ θ} . Again, we can adjust this definition to cope with languages over a finite alphabet Σ coming with a one-hot encoding enc Σ . If m = |Σ| and dim(T ) = (m, 1), then we let θ + L▷◁ Σ (T ) = {w ∈ Σ | ⟪T ⟫(enc Σ (w)) ▷◁ θ} .
61
Attention and Transformers 0
1
0
1
Nout
Nout
Nout
Nout
1 0 1
0 0 1
1 0 1
0 0 1
N (1)
N (1)
N (1)
N (1)
3 7 1
7 7 1
4 7 1
7 7 1
+
+
+
+
Wmax
Wmax
Wmax
Wmax
7
7
7
7
0
avg-argmax∗
3
0.5
7 3
3 key
0 4
7
7
4
0.5 query
4
1
E (1)
= (Amax , N (1) )
Amax
= (Hmax , Wmax )
Hmax
7 7
7
value
3 0 1
7 0 1
4 0 1
7 0 1
Nin
Nin
Nin
Nin
3
7
4
7
Figure 5.5: Transformer implementing argmax∗ Example 5.2: Encoder-Only Transformer For argmax∗ We continue Example 5.1. Consider the length-preserving mapping argmax∗ : R+ → {0, 1}+ over arbitrarily long sequences of real numbers. We will define an encoder-only transformer T with dim(T ) = (1, 1) and state(T ) = 3 such that JT K = argmax∗ . It is illustrated in Figure 5.5.
In a preprocessing step, we apply Nin such that Nin (x) = (x, 0, 1)⊤ . Next, we use self-attention in Amax . Thus, H outputs, at every position, the maximum number occurring in the sequence. Thanks to the residual connection, the output is added to the input vectors. It remains to identify the positions where the first two components are identical (those are the positions originally carrying the maximum number). This is taken care of by the neural network N (1) , which outputs 0 iff the first two components are equal. More precisely, for x = (x1 , x2 , x3 )⊤ , ( (0, 0, 1)⊤ if x1 = x2 JN (1) K(x) = (1, 0, 1)⊤ if x1 ̸= x2 62
Attention and Transformers 0 0 1
0 0 1
1 0 1
0 0 1
N (1)
N (1)
N (1)
N (1)
3 3 1
7 7 1
4 7 1
7 7 1
+
+
+
+
Wmax
Wmax
Wmax
Wmax
3
7
7
7
E (1)
= (Amax , N (1) )
Amax
= (Hmax , Wmax ) masked
0
avg-argmax∗
3
7 3
3 key
4
7
7
Hmax
0
1
4
query
4
1
7
7
value
3 0 1
7 0 1
4 0 1
7 0 1
Nin
Nin
Nin
Nin
3
7
4
7
Figure 5.6: Transformer recognizing sorted sequences (lower part)
Here, we leave the third component unchanged, as this will be useful in the subsequent example. The neural network N (1) makes use of heaviside as (local) activation function, defined by ( 0 if x ≤ 0 heaviside(x) = 1 if x > 0 . However, we could also use a combination of ReLU and σ, adjusting the interpretation of the output accordingly. Finally, Nout inverts the first component. The specification of Nin , N (1) , and Nout is left to the reader as an exercise. Example 5.3: Encoder-Only Transformer Recognizing Sorted Sequences Again, we will build on Example 5.1. Our goal now is to model a function f : R+ → {0, 1} that returns 1 if the input sequence is sorted, and 0 otherwise. We will define an encoder-only transformer T with dim(T ) = (1, 1) and state(T ) = 3 such that, for all w ∈ R+ , the last element in the sequence JT K(w) is f (w). In other words, L= 1 (T ) = L≥ 0.5 (T ) is the set of sorted sequences over R. The transformer T = (Nin , E (1) , E (2) , Nout ) is illustrated in Figures 5.6 and 5.7.
63
Attention and Transformers 1
1
0
0
Nout
Nout
Nout
Nout
0 0 0
0 0 0
1 0 0
1 0 0
N (2)
N (2)
N (2)
N (2)
0 0 0
0 0 0
0 1 0
0 1 0
Wmax
Wmax
Wmax
Wmax
0
0
1
1
output
E (2)
= (Amax , N (2) )
Amax
= (Hmax , Wmax ) masked
0
avg-argmax∗
0
0
1
0
0 key
0
1
0 0
1
0
0
1
0
Hmax query
0
1
value
0 0 1
1 0 1
0 0 1
0 0 1
Figure 5.7: Transformer recognizing sorted sequences (upper part)
We use the very same components as in Example 5.2. However, we now adopt the masked self-attention semantics. In that case, every position i in the sequence can only “see” the previous positions (including i). Thus, at the last position, we use Hmax in the second encoder layer to detect whether some violation of the order has occurred. Note that the neural network N (2) will just invert the first two components so that we can apply Nout as in the previous case. Note that the encoder layer E (2) could also use the non-masked self-attention semantics, as we are only interested in the output at the very last position.
Example 5.4: Well-Formed Bracket Strings The last example, which is due to [6], is concerned with the language L over the finite alphabet Σ = {⟨ , ⟩} given by the following grammar: A ::= ⟨ A ⟩ | AA | ε Thus, L is the set of well-formed bracket strings. Figure 5.8 sketches an encoder0 only transformer T with two encoder layers such that L= Σ (T ) = L. Here, we assume enc Σ ( ⟨ ) = (1, 0)⊤ and enc Σ ( ⟩ ) = (0, 1)⊤ . The idea is that the first component of a global state checks whether, in every prefix,
64
Attention and Transformers 0 Nout 0 1
0 1
0 1
0 0
0 1
0 0
id
id
id
id
id
id
0 1
0 1
0 1
0 0
0 1
0 0
+
+
+
+
+
+
sum
masked self-attention with avg-argmax∗
0 1
0 1
0 1
0 0
0 1
0 0
heaviside
heaviside
heaviside
heaviside
heaviside
heaviside
−1 ÷1 +1
−2 ÷2 +2
−1 ÷3 +1
0 0
÷4
−1 ÷5 +1
0 ÷6 0
masked self-attention with avg-argmax∗
−1 +1
−1 +1
+1 −1
+1 −1
−1 +1
+1 −1
Nin
Nin
Nin
Nin
Nin
Nin
1 0
1 0
0 1
0 1
1 0
0 1
Figure 5.8: Transformer recognizing well-formed bracket strings
there are at least as many opening as closing brackets. The second component checks whether, in the entire word, there are as many closing as opening brackets. A violation of the former property would result in some value 1 in the first component after the first encoder layer. If not violated, the original string is valid if the second component is zero, too. The second encoder layer checks zeroness in both cases. A series of recent papers established a rather complete picture of the language classes defined by transformer architectures, both in terms of logic and circuit complexity. Examples include [3, 6, 34, 48, 56]. To the best of our knowledge, only a few works address the verification of transformers. Exceptions are [31, 46], which study robustness verification. General positive decidability results for transformers have yet to be explored. Due to Turing completeness of the general architecture [39], the challenge lies in identifying 65
Attention and Transformers architectures that allow for deciding interesting properties. This represents a crucial area for future research, particularly in the context of verification. A related question is what a useful specification could be, for example in the spirit of NNL.
66
Bibliography [1] Michael E. Akintunde, Andreea Kevorchian, Alessio Lomuscio, and Edoardo Pirovano. Verification of rnn-based neural agent-environment systems. In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019, pages 6006–6013. AAAI Press, 2019. [2] Aws Albarghouthi. Introduction to Neural Network Verification. verifieddeeplearning.com, 2021. http://verifieddeeplearning.com. [3] Pablo Barceló, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir V. Podolskii. Logical languages accepted by transformer encoders with hard attention. CoRR, abs/2310.03817, 2023. [4] Bernd Becker, Christian Dax, Jochen Eisinger, and Felix Klaedtke. LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, volume 4590 of Lecture Notes in Computer Science, pages 307–310. Springer, 2007. [5] Alberto Bertoni. The solution of problems relative to probabilistic automata in the frame of the formal languages theory. In Dirk Siefkes, editor, GI - 4. Jahrestagung, Berlin, 9.-12. Oktober 1974, volume 26 of Lecture Notes in Computer Science, pages 107–112. Springer, 1974. [6] Satwik Bhattamishra, Kabir Ahuja, and Navin Goyal. On the ability and limitations of transformers to recognize formal languages. In Bonnie Webber, Trevor Cohn, Yulan He, and Yang Liu, editors, Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing, EMNLP 2020, Online, November 16-20, 2020, pages 7096–7116. Association for Computational Linguistics, 2020. [7] Bernard Boigelot, Sébastien Jodogne, and Pierre Wolper. On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, volume 2083 of Lecture Notes in Computer Science, pages 611–625. Springer, 2001. [8] Benedikt Bollig, Martin Leucker, and Daniel Neider. A Survey of Model Learning Techniques for Recurrent Neural Networks. In Nils Jansen, Mariëlle Stoelinga, and Petra van den Bos, editors, A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 67
BIBLIOGRAPHY 60th Birthday, volume 13560 of Lecture Notes in Computer Science, pages 81–97. Springer, 2022. [9] J. Richard Büchi. Symposium on Decision Problems: On a Decision Method in Restricted Second Order Arithmetic. In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors, Logic, Methodology and Philosophy of Science, volume 44 of Studies in Logic and the Foundations of Mathematics, pages 1–11. Elsevier, 1966. [10] George E. Collins. Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition - Preliminary Report. SIGSAM Bull., 8(3):80–90, 1974. [11] Antoine Durand-Gasselin and Peter Habermehl. Ehrenfeucht-Fraı̈ssé goes elementarily automatic for structures of bounded degree. In Christoph Dürr and Thomas Wilke, editors, 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, volume 14 of LIPIcs, pages 242–253. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. [12] Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas. Mathematical Logic. Undergraduate Texts in Mathematics. Springer, 1994. [13] Jochen Eisinger. Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract). In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 431–445. Springer, 2008. [14] Jeffrey L. Elman. Finding structure in time. Cogn. Sci., 14(2):179–211, 1990. [15] Nathanaël Fijalkow. Undecidability results for probabilistic automata. SIGLOG News, 4(4):10–17, 2017.
ACM
[16] Hugo Gimbert and Youssouf Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 527–538. Springer, 2010. [17] Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173–198, 1931. [18] Christoph Haase. Approaching Arithmetic Theories with Finite-State Automata. In Alberto Leporati, Carlos Martı́n-Vide, Dana Shapira, and Claudio Zandron, editors, Language and Automata Theory and Applications - 14th International Conference, LATA 2020, Milan, Italy, March 4-6, 2020, Proceedings, volume 12038 of Lecture Notes in Computer Science, pages 33–43. Springer, 2020. [19] Christoph Hertrich, Amitabh Basu, Marco Di Summa, and Martin Skutella. Towards Lower Bounds on the Depth of ReLU Neural Networks. SIAM J. Discret. Math., 37(2):997–1029, 2023. [20] Sepp Hochreiter and Jürgen Schmidhuber. Long short-term memory. Neural Comput., 9(8):1735–1780, 1997. 68
BIBLIOGRAPHY [21] Omri Isac, Yoni Zohar, Clark W. Barrett, and Guy Katz. DNN Verification, Reachability, and the Exponential Function Problem. In Guillermo A. Pérez and JeanFrançois Raskin, editors, 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium, volume 279 of LIPIcs, pages 26:1–26:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. [22] Yuval Jacoby, Clark W. Barrett, and Guy Katz. Verifying recurrent neural networks using invariant inference. In Dang Van Hung and Oleg Sokolsky, editors, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 57–74. Springer, 2020. [23] Andrej Karpathy. The unreasonable effectiveness of recurrent neural networks. http: //karpathy.github.io/2015/05/21/rnn-effectiveness/, May 2015. Accessed: December 19, 2023. [24] Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science, pages 97–117. Springer, 2017. [25] Igor Khmelnitsky, Daniel Neider, Rajarshi Roy, Xuan Xie, Benoı̂t Barbot, Benedikt Bollig, Alain Finkel, Serge Haddad, Martin Leucker, and Lina Ye. Analysis of recurrent neural networks via property-directed verification of surrogate models. Int. J. Softw. Tools Technol. Transf., 25(3):341–354, 2023. [26] Felix Klaedtke. Bounds on the automata size for Presburger arithmetic. ACM Trans. Comput. Log., 9(2):11:1–11:34, 2008. [27] Felix Klaedtke. Ehrenfeucht-Fraı̈ssé goes automatic for real addition. Inf. Comput., 208(11):1283–1295, 2010. [28] Daniel Kroening and Ofer Strichman. Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2016. [29] The LASH toolset. research/lash/.
https://people.montefiore.uliege.be/boigelot/
[30] Martin Leucker. Formal Verification of Neural Networks? In Gustavo Carvalho and Volker Stolz, editors, Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings, volume 12475 of Lecture Notes in Computer Science, pages 3–7. Springer, 2020. [31] Brian Hsuan-Cheng Liao, Chih-Hong Cheng, Hasan Esen, and Alois Knoll. Are transformers more robust? towards exact robustness verification for transformers. In Jérémie Guiochet, Stefano Tonetta, and Friedemann Bitsch, editors, Computer Safety, Reliability, and Security - 42nd International Conference, SAFECOMP 2023, Toulouse, France, September 20-22, 2023, Proceedings, volume 14181 of Lecture Notes in Computer Science, pages 89–103. Springer, 2023. 69
BIBLIOGRAPHY [32] Yang Liu, Jianpeng Zhang, Chao Gao, Jinghua Qu, and Lixin Ji. Naturallogarithm-rectified activation function in convolutional neural networks. CoRR, abs/1908.03682, 2019. [33] Christof Löding. Efficient minimization of deterministic weak ω-automata. Inf. Process. Lett., 79(3):105–109, 2001. [34] William Merrill, Ashish Sabharwal, and Noah A. Smith. Saturated transformers are constant-depth threshold circuits. Trans. Assoc. Comput. Linguistics, 10:843–856, 2022. [35] William Merrill, Gail Weiss, Yoav Goldberg, Roy Schwartz, Noah A. Smith, and Eran Yahav. A formal hierarchy of RNN architectures. In Dan Jurafsky, Joyce Chai, Natalie Schluter, and Joel R. Tetreault, editors, Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, ACL 2020, Online, July 5-10, 2020, pages 443–459. Association for Computational Linguistics, 2020. [36] Marvin Lee Minsky. Neural Nets and the Brain Model Problem. PhD thesis, Princeton University, 1954. [37] Izaak Neutelings. Neural network diagrams with tikz. https://tikz.net/neural_ networks/, 2021. [38] Azaria Paz. Introduction to probabilistic automata. Academic Press, 1971. [39] Jorge Pérez, Pablo Barceló, and Javier Marinkovic. Attention is Turing-complete. J. Mach. Learn. Res., 22:75:1–75:35, 2021. [40] Michael O. Rabin. Probabilistic automata. Inf. Control., 6(3):230–245, 1963. [41] Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh, Andrei Marian Dan, and Martin T. Vechev. Scalable polyhedral verification of recurrent neural networks. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, volume 12759 of Lecture Notes in Computer Science, pages 225–248. Springer, 2021. [42] Marco Sälzer, Eric Alsmann, Florian Bruse, and Martin Lange. Verifying and interpreting neural networks using finite automata. Inf. Comput., 308:105398, 2026. [43] Marco Sälzer and Martin Lange. Reachability is NP-Complete Even for the Simplest Neural Networks. In Paul C. Bell, Patrick Totzke, and Igor Potapov, editors, Reachability Problems - 15th International Conference, RP 2021, Liverpool, UK, October 25-27, 2021, Proceedings, volume 13035 of Lecture Notes in Computer Science, pages 149–164. Springer, 2021. [44] Marco Sälzer and Martin Lange. Reachability in simple neural networks. Fundam. Informaticae, 189(3-4):241–259, 2022. [45] Roberto Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1995. [46] Zhouxing Shi, Huan Zhang, Kai-Wei Chang, Minlie Huang, and Cho-Jui Hsieh. Robustness verification for transformers. In 8th International Conference on Learning 70
BIBLIOGRAPHY Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. [47] Hava T. Siegelmann and Eduardo D. Sontag. On the computational power of neural nets. J. Comput. Syst. Sci., 50(1):132–150, 1995. [48] Lena Strobl, William Merrill, Gail Weiss, David Chiang, and Dana Angluin. What formal languages can transformers express? A survey. Trans. Assoc. Comput. Linguistics, 12:543–561, 2024. [49] Anej Svete and Ryan Cotterell. Recurrent neural language models as probabilistic finite-state automata. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, EMNLP 2023, Singapore, December 6-10, 2023, pages 8069–8086. Association for Computational Linguistics, 2023. [50] Alfred Tarski. A Decision Method for Elementary Algebra and Geometry. RAND Corporation Paper, 1948. [51] Wolfgang Thomas. Languages, automata, and logic. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 389–455. Springer, 1997. [52] Hoang-Dung Tran, Sung Woo Choi, Xiaodong Yang, Tomoya Yamaguchi, Bardh Hoxha, and Danil V. Prokhorov. Verification of recurrent neural networks with star reachability. In Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2023, San Antonio, TX, USA, May 9-12, 2023, pages 6:1–6:13. ACM, 2023. [53] Caterina Urban and Antoine Miné. A Review of Formal Methods applied to Machine Learning. CoRR, abs/2104.02466, 2021. [54] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pages 5998–6008, 2017. [55] Adrian Wurm. Complexity of reachability problems in neural networks. In Olivier Bournez, Enrico Formenti, and Igor Potapov, editors, Reachability Problems - 17th International Conference, RP 2023, Nice, France, October 11-13, 2023, Proceedings, volume 14235 of Lecture Notes in Computer Science, pages 15–27. Springer, 2023. [56] Andy Yang, David Chiang, and Dana Angluin. Masked hard-attention transformers recognize exactly the star-free languages. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors, Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, December 10 - 15, 2024, 2024. 71
BIBLIOGRAPHY [57] Huan Zhang, Kaidi Xu, Shiqi Wang, and Cho-Jui Hsieh. Formal Verification of Deep Neural Networks: Theory and Practice. https://neural-network-verification. com, 2022.
72