The Power of Hard Attention Transformers on Data Sequences: A formal language theoretic perspective

Authors: pascal  bergsträßer
chris  köcher
anthony widjaja lin
georg  zetzsche
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-15 12:41:52

Abstract: Formal language theory has recently been successfully employed to unravel 
    the power of transformer encoders. This setting is primarily applicable in
    Natural Language Processing (NLP), as a token embedding function (where
    a bounded number of tokens is admitted) is first applied before feeding 
    the input to the transformer. 
    On certain kinds of data (e.g. time 
    series), we want our transformers to be able to handle arbitrary
    input sequences of numbers (or tuples thereof) without a priori
    limiting the values of these numbers. In this
    paper, we initiate the study of the expressive power of transformer encoders
    on sequences of data (i.e. tuples of numbers).
    Our results indicate an increase in expressive power of 
    hard attention transformers over data sequences, in stark contrast to the 
    case of strings.
    In particular, we prove that Unique Hard Attention Transformers (UHAT) over 
    inputs as data sequences no longer lie within the circuit complexity 
    class AC0 (even without positional encodings), unlike the case of string
    inputs, 
    but are still within the complexity class TC0 (even with positional
    encodings). Over strings, UHAT without positional encodings capture only
    regular languages. In contrast, we show that over data sequences
    UHAT can capture non-regular properties.
    Finally, we show that UHAT capture languages 
    definable in an extension of linear temporal logic with unary numeric
    predicates and arithmetics.

Main paper: 
 introduction: 
 Recent years have witnessed the success of transformers [42] in different applications, including natural language processing [12] , computer vision [14] , speech recognition [13] , and time series analysis [45, 46] . In the quest to better understand the ability and limitation of transformers, theoretical investigations have actively been undertaken in the last few years. Among others, formal language theory has been successfully applied to reveal deep insights into the expressive power of transformers, e.g., see the recent survey [40] and [2, 3, 8, 15, 20, 21, 30, 32, 38, 39] . In particular, relevant questions pertain to the power of various attention mechanisms, bounded/unbounded precision, positional encoding functions, and interplay between encoders and decoders, among many others.One common assumption in the formal language theoretic approach to transformers is that the input sequence ranges over a finite set Σ (called alphabet), which is then to be fed into a transformer after applying a token embedding function of the form f : Σ → R d . As a by-product, the number of tokens is finite. In certain applications (e.g. time series forecasting [28] ), we want our transformers to be able to handle arbitrary input sequences of numbers (or tuples thereof) without a priori limiting the values of these numbers. Moreover, numbers could be compared using arithmetic and (in)equality, which is not the case for elements of alphabets considered in formal language theory. For this reason, we propose to investigate the expressive power of transformers over data sequences, which takes us to the setting of formal language theory over the alphabet Σ = Q d , for some d ∈ Z >0 , e.g., see [4, 11] . That is, what properties of a sequence of (tuples of) numbers can be recognized by transformers?Connections to circuit complexity. Existing work has revealed intimate connections between transformers and circuit complexity. In particular, let us consider the following class of transformer encoders that has been the main focus of many recent papers: Unique Hard Attention Transformers (UHAT). Among others, UHAT allows arbitrary positional encoding and an attention mechanism that picks a vector at a unique minimum position in the sequence that maximizes the attention score. It is known that the class of formal languages recognized by UHAT is a strict subset of the circuit complexity class AC 0 (cf. [3, 20, 21] ), i.e., each UHAT can be simulated by a family of boolean circuits of constant depth. More concretely, this entails among others that UHAT cannot compute the parity (even/oddness) of the number of occurrences of any given letter a in the input string (for strings over an alphabet containing at least two letters).Our first contribution is that UHAT over data sequences (even without positional encodings) is no longer contained in AC 0 , unlike the case of finite number of tokens. Instead, we show that UHAT can be captured by the circuit complexity class TC 0 , which extends AC 0 circuits with majority gates. Theorem 1. UHAT with positional encoding over data sequences is in TC 0 but not in AC 0 . This complexity upper bound allows us to deduce the expressive power of UHAT over data sequences by using complexity theory. For example, since UHAT accepts only TC 0 languages, successfully constructing a UHAT (e.g. through learning) forSQRTSUM := (a 1 , b 1 ), . . . , (a n , b n ) n i=1 √ a i ≤ n i=1 b i , and each (a i , b i ) ∈ Z >0 × Z >0 , ,would constitute a major breakthrough in complexity theory (cf. [1, 18] ), i.e., showing that SQRTSUM is in the complexity class TC 0 ⊆ P/poly. A byproduct of our proof is that for each length, the set of accepted sequences is a semialgebraic set. This implies, e.g., that the graph {(x, e x ) | x ∈ R} ⊆ R 2 of x → e x (viewed as a set of length-1 sequences) is not accepted by UHAT.Connection to regular languages over data sequences. Recent results have revealed surprising connections between regular languages and formal languages recognizable by transformer encoders.In particular, it was proven (cf. [2] ) that languages recognizable by UHAT (even with no positional encodings) form a strict subset of regular languages, namely those that are "star-free" or, equivalently, definable in First-Order Logic (FO), or Linear Temporal Logic (LTL). With positional encodings, similar connections hold, by extending the logics with unary numerical predicates (cf. [2, 3] ).To investigate whether such connections extend to data sequences, we bring forth formal languages theory over infinite alphabets (cf., [4, 11] ), which has been an active research field in the last decade or so with applications to programming languages and databases (to name a few), e.g., see [11, 26, 43] . Our second contribution is a language over data sequences recognizable by UHAT without positional encodings that lies beyond existing formal models over infinite alphabets (in particular, "regular" ones). This shows the strength of UHAT over data sequences even without positional encodings, in stark contrast to the case of finite alphabets. Theorem 2. There is a non-regular language over Σ = Q d that is accepted by masked UHAT with no positional encoding.Finally, to better understand languages over data sequences recognizable by UHAT, our third contribution is to show how UHAT can recognize languages definable by the so-called Locally Testable LTL ((LT) 2 L), which extends LTL with unary numerical predicates and local arithmetic tests for fixed-size windows over the input sequence. Using (LT) 2 L, we can see at a glance what can be expressed by UHAT over data sequences. For one, this includes the well-known Simple Moving Averages. As another example, using (LT) 2 L it can be easily shown that UHAT can capture linear recurrence sequences considered in the famous Skolem problem and discrete linear dynamical systems [25, 27, 29] , i.e., sequences of the form x, Ax, . . . , A n x such that n ≥ 0 is minimal with yA n x = 0 where y ∈ Q 1×d and A ∈ Q d×d are fixed and x ∈ Q d .Theorem 3. Every (LT) 2 L-definable language is accepted by UHAT with positional encoding.Technical challenges. Obtaining our results poses several challenges. First, for the TC 0 upper bound, we need to use Boolean (constant depth) circuits to simulate UHATs, in which real constants can occur (in affine transformations or positional encodings). While in TC 0 , it is known that majority gates can be used to perform multiplication of rationals [7] , arithmetic with reals requires infinite precision and cannot be done with Boolean circuits. To this end, we compute rational approximations of reals accurate enough to preserve the acceptance condition for inputs up to a particular length n.Here, a naive attempt would be to replace each real occurring in the UHAT in affine transformations and the positional encoding by some rational approximation. However, this is not possible, meaning any rational approximation would change the behavior on input sequences of length n = 3, even for low-dimensional vectors with entries in {0, 1}. Indeed, there is a UHAT involving real numbers α, β that accepts a simple sequence of {0, 1}-vectors if and only if αβ = 2 and α = β, i.e. α = β = √ 2. Thus, α and β cannot be replaced by rationals, even for very short inputs (see Appendix A for details).Instead, we show that a UHAT can be translated into a small Boolean combination of polynomial inequalities. This format has the advantage that-as we show using convex geometry-the real coefficients of those polynomials can be replaced by suitably chosen rational numbers. In turn, the layer-by-layer construction of these polynomial inequalities requires a carefully chosen data structure to encode the function computed by a sequence of transformer layers. For example, we show that the resulting Boolean combinations of polynomial inequalities have a bound on the number of alternations between conjunctions and disjunctions, which is crucial for constructing TC 0 -circuits.Another key challenge occurs in the translation from (LT) 2 L to UHATs: In the inductive construction, we need to represent truth values using reals in [0, 1]. To implement negation, we use a UHAT gadget (with positional encodings) that can normalize these truth values to {0, 1}.Notation. In the sequel, we assume some background from computational complexity, in particular circuit complexity (see the book [44] ). In particular, we use the circuit complexity class AC 0 , which defines a class of problems that are computable by a nonuniform family of constant-depth boolean circuits, where each gate permits an unbounded fan-in (i.e. arbitrary many inputs). Similarly, the complexity class TC 0 is an extension of AC 0 , where majority gates are allowed. It is well-known that AC 0 ⊊ TC 0 . Assuming uniformity, both AC 0 and TC 0 are contained in the class of problems solvable in polynomial-time. For nonuniformity, these classes are contained in the complexity class P/poly, which admits (nonuniform) polynomial-size circuits. It is a long-standing open problem whether numerical analysis (e.g. square-root-sum) is in P/poly, e.g., see [1] .(1, 0, e 1 )(1, 0, e 2 )(1, 0, e 3 ).2. Using a standard encoding layer, we multiply the first component in each position by α.Result: (α, 0, e 1 )(α, 0, e 2 )(α, 0, e 3 ).3. Using attention, we can apply distinct affine transformations to the first three positions. We choose the following affine transformations. The first position is unchanged. The second position is mapped to (1, 0, e 2 ), and the third position is mapped to (0, α, e 3 ), using a matrix that flips the first and second component. Result:(α, 0, e 1 )(1, 0, e 2 )(0, α, e 3 ).4. Using a standard encoding layer, we multiply the first component in each position with β.(αβ, 0, e 1 )(β, 0, e 2 )(0, α, e 3 ). B Omitted definitions and proofs in Section 3Let x ∈ R be some real number. The (descriptional) size of x is size(x) = 1 + ⌈log 2 (|p| + 1)⌉ + ⌈log 2 (|q| + 1)⌉ if x = p q is a rational number (where p and q are relatively prime integers) and size(x) = 1 if x is an irrational number. Note that in the latter case we use the number 1 as some placeholder, since we do not have to represent irrational numbers in any algorithm. However, for analysis of the sizes in our constructions we still need some value. Let α be a polynomial constraint. We define the size of α inductively on the structure of the formula as follows:Let v ∈ R d be a vector. The size of v is size(v) = n + d i=1 size(v i ) where v = (v 1 , . . . , v d ) T . Let M ∈ R m×n be a matrix. The size of M is size(M ) = mn + 1≤i≤m,1≤j≤n size(a ij ) where M = (a ij ) 1≤i≤m,1≤j≤n .• if α = (p(X 1 , . . . , X n ) ∼ 0) with ∼ ∈ {>, ≥} is an atom. Then size(α) = size(p) + 1.• if α = 1≤i≤k β i or α = 1≤i≤k β i is a formula with PCs β 1 , . . . , β k , then size(α) = k + 1≤i≤k size(()β i ). Let R = (ϕ 1 , D 1 ), . . . , (ϕ k , D k ) be a CPR. Then the size of this CPR is size(R) = k + k i=1 size(ϕ i ) + size(D k ).Let us now consider a ReLU layer. Assume that we compute the ReLU-value for the j-th component, i.e., we compute max{0, x i,j } for each i ∈ {1, . . . , n + 1} where x i,j is the j-th component of x i . From each conditional assignment φ i,k → D i,k with i ∈ {1, . . . , n + 1} and 1 ≤ k ≤ s i we construct two new conditional assignments:1. ⟨e (i-1)•n+j , D i,k x⟩ ≥ 0 → D i,kwhere e h is the h-th unit vector.Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?Answer: [Yes] Justification: This paper contains theoretical results on the expressive power of transformers on data sequences. As standard in theoretical results, we try to mathematically formulate the results as as precisely as they can be.Guidelines:• The answer NA means that the abstract and introduction do not include the claims made in the paper. • The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers. • The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. • It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper. 
transformer encoders and their languages: 
 In the following, we adapt the setting of formal language theory (see [3, 21, 40] ) to data sequences. For a vector a = (a 1 , . . . , a d ) we write a[i, j] := (a i , . . . , a j ) for all 1 ≤ i ≤ j ≤ d and if i = j, we simply write a[i]. For a set S we denote the set of (potentially empty) sequences of elements from S by S * . We write S + for the restriction to non-empty sequences. We consider languages L over the infinite alphabet Σ = Q d , for some integer d > 0. That is, L is a set of sequences of d-tuples over rational numbers. We will define a UHAT (similarly as in previous papers that study formal language theoretic perspectives) as a length preserving map(Q d ) * → (R e ) * .Standard encoder layer with unique hard attention. A standard encoder layer is defined by three affine transformations A, B : R d → R d and C : R 2d → R e . For a sequence v 1 , . . . , v n ∈ R d with n ≥ 1 we define the attention vector at position i ∈ [1, n] as a i := v j with j ∈ [1, n] minimal such that the attention score ⟨Av i , Bv j ⟩ is maximized. The layer outputs the sequence C(v 1 , a 1 ), . . . , C(v n , a n ).k ∈ [1, d] on input v 1 , . . . , v n ∈ R d applies the ReLU function to the k-th coordinate of each v i , i.e. it outputs the sequence v ′ 1 , . . . , v ′ n where v ′ i := (v i [1, k -1], max{0, v i [k]}, v i [k + 1, n]).[Equivalently, one could instead allow a feedforward network at the end of an encoder layer (see [3, 21, 40] ).] Transformer encoder. A unique hard attention transformer encoder (UHAT) is a repeated application of standard encoder layers with unique hard attention and ReLU encoder layers. Clearly, using an alternation of standard layers and ReLU layers, we can assume that the output of a UHAT layer is an arbitrary composition of affine transformations and component-wise ReLU application. In particular, these compositions may use the functions max and min.Languages accepted by UHATs. The notion of "languages" accepted by a UHAT (i.e. a set of accepted sequences) can be defined, depending on whether a positional encoding is permitted. If it is permitted, a language L ⊆ (Q d ) + is accepted by a UHAT T if and only if there exists a positional encoding function p : N × N → R s and an acceptance vector t ∈ R e such that on every sequenceEQUATIONT outputs a sequence v ′ 1 , . . . , v ′ n+1 ∈ R e with ⟨t, v ′ 1 ⟩ > 0 if and only if (v 1 , . . . , v n ) ∈ L.Note that if T 1 and T 2 are UHATs with positional encoding that realize functions f 1 : (Q d ) * → (Q e ) * and f 2 : (Q e ) * → (Q r ) * , then there is a UHAT T 2 • T 1 with positional encoding that realizes the composition f 2 • f 1 by using a positional encoding that combines the positional encodings of T 1 , T 2 .In the above definition we appended an additional zero vector to the end of the input. Over finite alphabets it is often assumed that the input sequence is extended with a special unique end-of-input marker (e.g. see [21, 40] ). When the input is a sequence of (tuples of) numbers, if we allow positional encoding, then the zero vector at the end of the input can be turned into a unique vector marking the end of the input (see Section 5) . Without positional encoding, however, we have to explicitly make the zero vector at the end of the input unique. That is, a UHAT without positional encoding is initialized with the sequence (1, v 1 ), . . . , (1, v n ), 0 ∈ Q d+1 instead; this ensures, among others, that the end-of-input marker does not appear in the actual input.In the definition of a standard encoder layer the attention vector at position i ∈ [1, n] can be any vector in the sequence v 1 , . . . , v n . Using masking, one can restrict the attention vector to vectors of certain positions. A UHAT with past masking restricts the attention vector a i at position 1 ≤ i < n to be contained in the subsequence v i+1 , . . . , v n and at position n to a n := v n .(i-1)•n+j , D i,k x⟩ > 0 → M D i,k where M = (m gh ) 1≤g,h≤d ′ •(n+1) is the matrix with m gh = 1 if g = h ̸ = (i -1)• n + j and m gh = 0 otherwise (i.e., M is the unit matrix except for the (i -1) • j-th entry). Now, if the j-th component of x i is non-negative, only the first conditional assignment is satisfied and the value of this component is left untouched. Otherwise, the j-th component is negative. But then the second conditional assignment is satisfied and the value of this component is set to 0 (while the others stay unchanged). So, we obtain again some polynomial sized CPR with the same number of alternations as before.Proof of Proposition 5. Let t ∈ R e be the acceptance criterion of the UHAT and f : R d•(n+1) → R e•(n+1) be the computed function for inputs of length n. By Lemma 6, we can construct in polynomial time an O(ℓ)-alternation-bounded CPR computing f . So, let φ i,k → D i,k be the conditional assignments in this CPR (for 1 ≤ i ≤ n + 1 and 1 ≤ k ≤ s i ). Then we obtain a PC from this CPR as follows:s1 J=1 φ 1,J ∧ ⟨t, D 1,J x⟩ > 0 .Note that this PC has still polynomial size, accepts an input sequence (x 1 , . . . , x n , 0) if, and only if, the UHAT accepts (x 1 , . . . , x n ), and -if the CPR is a-alternation-bounded -then it has at most a + 2 alternations of disjunctions and conjunctions.Proof of Proposition 7. Consider a constraint p(X 1 , . . . , X n ) > 0 (or ≥ 0 resp.) in α. Then p ∈ R[X 1 , . . . , X n ] is a polynomial of degree at most 2, i.e., there are real numbersc i,j,r,s ∈ R such that p(X 1 , . . . , X n ) = 0≤r+s≤2 1≤i≤j≤n c i,j,r,s X r i X s j .Now, construct two vectors u and w with a component for each tuple (i, j, r, s): u i,j,r,s = c i,j,r,s and w = i, j, r, s = X r i X s j . Then it is clear that p(X 1 , . . . , X n ) = ⟨u, w(X 1 , . . . , X n )⟩ holds.Application of Lemma 8 yields a vector v ∈ Q t with ∥v∥ 2 ≤ (2mt) O (1) and u ∼ 2m v. Note that we need to consider rational numbers up to size 2m due to the fact that substitution of the variables in w by rational numbers x ∈ Q n ≤m yields a rational vector w(x) ∈ Q t ≤2m . Let p ′ (X 1 , . . . , X n ) be the polynomial obtained from p be replacing the coefficients c i,j,r,s ∈ R by v i,j,r,s ∈ Q. Then for each x ∈ Q n ≤m we have p(x) = ⟨u, w(x)⟩ > 0 (resp. ≥ 0) if, and only if, p ′ (x) = ⟨v, w(x)⟩ > 0 (resp. ≥ 0).Replacing each real polynomial p in α by the constructed rational polynomial p ′ results in a rationalPC α ′ with α ∩ Q n ≤m = α ∩ Q n ≤m .The rest of this subsection is devoted to proving Lemma 8, for which we rely on results from convex geometry, which requires some terminology. For a set S ⊆ R n , we define the convex hull of S asconv.hull S = {λ 1 s 1 + • • • + λ m s m | m > 0, s 1 , . . . , s m ∈ S, λ 1 , . . . , λ m ∈ [0, 1], λ 1 + • • • + λ m = 1}and the cone generated by S ascone S = {λ 1 s 1 + • • • + λ m s m | m > 0, s 1 , . . . , s m ∈ S, λ 1 , . . . , λ m ≥ 0}.We will also rely on Carathéodory's theorem, which says that a points in cones and convex sets can be obtained from at most n points. See, for example, [35, Theorems 7.1i and 7.1j].Theorem 18 (Carathéodory's Theorem). Let S ⊆ R n . For every x ∈ conv.hull S, there are x 1 , . . . , x n ∈ S with x ∈ conv.hull {x 1 , . . . , x n }. Moreover, for every y ∈ cone S, there are y 1 , . . . , y n ∈ S with y ∈ cone {y 1 , . . . , y n }.A polyhedron is a set of the form {x ∈ R n | Ax ≥ b}, where A ∈ R m×n and b ∈ R m for some m ∈ N. If the matrix A and the vector b are rational, then the polyhedron is called a rational polyhedron. It is a standard result about polyhedra that if A and b are rational of size at most m, then the polyhedron P = {x ∈ R n | Ax ≥ b} can be written asP = conv.hull {x 1 , . . . , x s } + cone {y 1 , . . . , y t },with rational vectors x 1 , . . . , x s , y 1 , . . . , y t , where each vector has size polynomial in mn. See, for example, [Proof. We define the matrix B ∈ Q (k+ℓ)×n and the vector b ∈ Q k+ℓ asB = A A ′ b = z z ′ .and consider the polyhedronP = {x ∈ R n | Bx ≥ b}.As mentioned above, we can write P = conv.hull {x 1 , . . . , x s } + cone {y 1 , . . . , y t }, where x 1 , . . . , x s , y 1 , . . . , y t are rational vectors of size polynomial in mn. By our assumption, there exists an s ∈ R n with As ≫ z and A ′ s ≥ z ′ . By Carathéodory's Theorem, wlog, s belongs to the smaller polyhedronQ = conv.hull {x 1 , . . . , x n } + cone {y 1 , . . . , y n }.Now note that we have Au ≥ z and A ′ u ≥ z ′ for every u ∈ U := {x 1 , . . . , x n , y 1 , . . . , y n }. We claim that the vectorr = 1 n (x 1 + • • • + x n ) + y 1 + • • • + y n satisfies Ar ≫ z and A ′ r ≥ z ′ .Indeed, it clearly belongs to Q ⊆ P and thus satisfies A ′ r ≥ z ′ . Moreover, for every row a ⊤ x > z of Ax ≫ z, there must be a u ∈ U with a ⊤ u > z-otherwise, we would would have a ⊤ u = z for every u ∈ U and thus a ⊤ s = z. In particular, we have Ar ≫ z. Finally, the vector r has size at most∥x 1 ∥ 2 + • • • + ∥x n ∥ 2 + ∥y 1 ∥ 2 + • • • + ∥y n ∥ 2 ,which is polynomial in mn, since each x i and each y i has size polynomial in mn.Proof of Lemma 8. Collect the set of all inequalities ⟨w, u⟩ > z or ⟨w, u⟩ ≥ z with w ∈ Q t ≤m and z ∈ Q ≤m that are satisfied for u. This results in two large matrices A ∈ Q k×t ≤m and A ′ ∈ Q ℓ×t ≤m and vectors z ∈ Q k ≤m and z ′ ∈ Q ℓ ≤m such that we have u ∼ m v if and only if Av ≫ z and A ′ v ≥ z ′ . Thus, we can construct c ′ using Lemma 10. Observe that the bound from Lemma 10 does not depend on the (exponentially large) k and ℓ.Proof of Proposition 11. Let T be some UHAT with positional encoding and n, m ∈ N be two natural numbers. In the following, we consider input sequences of T having the length n and size m. By Propositions 5 and 7 there is polynomial sized, O(ℓ)-alternation-bounded, and rational PC α (where ℓ is the number of layers in T ) such that the set of sequences of size m accepted by the UHAT T equals α ∩ Q n•d ≤m . We finally show that the PC α can be realized as a circuit of constant depth and polynomial size. So, consider a constraint of the form p( x) ∼ 0 where ∼ ∈ {≥, >}, p is a polynomial of degree at most 2 and x represents the input sequence. Since addition and multiplication of rational numbers are realizable in TC 0 [7] , it is clear that the computation of the value p( x) is also realizable. Additionally, checking whether this value is ≥ 0 (or > 0, resp.) is a simple check of the bit representing the signum (and checking that the numerator has at least one non-zero bit).Finally, we have to connect all the atoms of the form p( x) ∼ 0 to the Boolean formula α. Since α alternates only a bounded number of times between disjunctions and conjunctions, we can realize the complete formula α in a circuit of constant depth and with polynomial size. Since α is equivalent (up to the input size m), the UHAT T is realizable in TC 0 . Note that here, we need to perform iterated addition of rational numbers, which requires iterated multiplication of integers represented in binary. The latter is well-known to be possible in TC 0 [33, 34] (even uniformly [22] , but this is not needed in our setting).Recall thatDouble := {(r 1 , . . . , r n ) ∈ Q n | n ≥ 1 and 2r i < r i+1 for all 1 ≤ i < n}.We next define the notion of symbolic automata [10, 11, 43] . A symbolic automaton is a tuple (Q, δ, q 0 , F ), where Q is a finite set of states, q 0 ∈ Q is an initial state, F ⊆ Q is a set of final states, and δ is a set of transition rules of the form (p, S, q), where S ⊆ Q. For a ∈ Q, we write p → a q (read "there is a transition from p to q reading a) if there is a transition rule (p, S, q) such that a ∈ S. Slightly abusing notation, for a set S ⊆ Q, we also write p → S q to mean that (p, S, q) is a transition rule in δ. The notion of a run, and an accepting run can then be defined in exactly the same way as for finite automata (e.g. see [37] ); namely, it is a sequence of transitions q 0 → a1 • • • → an q n , where q n ∈ F , reading the sequence w = a 1 • • • a n over Q.To prove that there is no symbolic automaton recognizing Double, let us assume to the contrary that such an automaton A exists, say, with n states. Consider a sufficiently long w = a 1 • • • a m ∈ Double (i.e. of length at least n), and an accepting run of A:q 0 → S1 • • • → Sm q mwhere each a i ∈ S i and q m ∈ F . Since m + 1 > n, by pigeonhole principle, it must be the case that q r = q s for some r < s. Thus, also the sequencea 1 • • • a r (a r+1 • • • a s ) 2 a s+1 • • • a mis accepted by A and therefore contained in Double. This is a contradiction since Double imposes a s < a s .For ¬φ the UHAT T ¬φ,m first applies T φ,m and on the obtained sequence u 1 , . . . , u n , 0 ∈ Q m+1 uses a further layer followed by 1) to output w ′i := (u i [1, m], 1 -u i [m + 1]) at position i ∈ [1, n] and 0 ∈ Q m+1 at position n + 1.For φ ∨ ψ we define the UHAT T φ∨ψ,m that first applies T ψ,m+1 • T φ,m followed by a layer that on sequence u 1 , . . . ,u n+1 ∈ Q m+2 outputs w ′ 1 , . . . , w ′ n+1 ∈ Q m+1 with w ′ i := (u i [1, m], max{u i [m + 1], u i [m + 2]}) for all i ∈ [1, n + 1]. Note that if u n+1 = 0, then also w ′ n+1 = 0.For Xφ the UHAT T Xφ,m first applies T φ,m to output a sequence u 1 , . . . , u n+1 ∈ Q m+1 with u n+1 = 0. With an additional layer that uses 2) to get attention vector a i = u i+1 for all i ∈ [1, n] it then outputs at position i ∈ [1, n] the vector w ′ i := (u i [1, m], a i [m + 1]) and at position n + 1 the vector w ′ n+1 := (u n+1 [1, m] , 0) after applying 1).NeurIPS Paper ChecklistQuestion: Does the paper discuss the limitations of the work performed by the authors?Answer: [Yes]Justification: We have discussed assumptions we made in this paper (e.g., regarding the formal model of transformers) and what consequences they have (see Limitations in Concluding Remarks).Guidelines:• The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper. • The authors are encouraged to create a separate "Limitations" section in their paper.• The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be. • The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated. • The authors should reflect on the factors that influence the performance of the approach.For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations. 
uhat and tc 0: 
 In this section, we prove Theorem 1. First, we show that all languages of UHAT (even with positional encoding) belong to the class TC 0 . Then, we show that there is a UHAT (even without positional encoding) whose language is TC 0 -hard under AC 0 -reductions. We begin with the proof that all UHAT languages belong to TC 0 .Input encoding A language L ⊆ Σ * over a finite alphabet Σ belongs to TC 0 if for every input length n, there is a circuit of size polynomial n, such that the circuit consists of input gates (for each input position i, and each letter a ∈ Σ, there is a gate that evaluates to "true" if and only if position i of the input words carries an a), Boolean gates (computing the AND, OR, or NOT function) and majority gates (evaluating to true if more than half of their input wires carry true). Here, AND, OR, and majority gates can have arbitrary fan-in. In order to define what it means that a language L ⊆ (Q d ) + belongs to TC 0 , we need to specify an encoding as finite-alphabet words. To this end, we encode a sequence u 1 , . . . , u n withu i ∈ Q d as a string v 1 # • • • #v n , where v i = p 1 /q 1 □ • • • □p d /q d with p j , q j ∈ {-, 0, 1} * . Here, v i ∈ {-, /, □, 0, 1} * represents the vector u i ∈ Q d such that u i [j] = aj bj , a j , b j ∈ Z,and p j , q j ∈ {-, 0, 1} * are the binary expansions of a j and b j . Remark 4. The main challenge in proving Theorem 1 is that the constants appearing in a UHAT can be real numbers. These can in general not be avoided: There are UHAT languages over Σ = Q (even without positional encoding) that cannot be accepted by UHAT with rational constants (even with positional encoding). For example, for every real number r > 0, one can1 construct a UHAT for the language L r of all sequences over Σ = Q where the first letter is > r. Note that L r ̸ = L s for any r, s > 0, r ̸ = s. However, there are clearly only countably many languages over Σ = Q accepted by UHAT with rational constants where membership only depends on the first letter2 . Thus, there are uncountably many real r > 0 such that L r is not accepted by a UHAT with rational constants.The construction of TC 0 circuits comprises three steps. In Step I, we show that the set of accepted length-n sequences can be represented by a Boolean combination of polynomial inequalities. Importantly, (i) this representation, called "polynomial constraints" is polynomial-sized in n, and (ii) the number of alternations between conjunction and disjunction is bounded (i.e. independent of n). The polynomials in this representations can still contain real coefficients. In Step II, we show that if we restrict the input not only to length-n sequences, but to rational numbers of size ≤ m, then we can replace all real coefficients of our polynomials by rationals of size polynomial in m and n, without changing the language (among vectors of size ≤ m). In Step III, we implement a TC 0 circuit. Here, it is important that the number of alternations between conjunctions and disjunctions in our polynomial constraints is bounded, because the depth of the circuit is proportional to this number of alternations.Step I: UHAT as polynomials We first consider a formalism to describe a set of sequences over Q d . We consider such sequences (x 1 , . . . , x n ) of length n, where x i ∈ Q d for each i. In this case, we also abbreviate x = (x 1 , . . . , x n ). A polynomial constraint (PC) is a positive Boolean combination (i.e., without negation) of constraints of the form p( x) > 0 or p( x) ≥ 0, where p ∈ R[X 1 , . . . , X d•n ] is a polynomial with real coefficients. Here, plugging x ∈ (Q d ) n into p is defined by assigning the d • n rational numbers in x to the d • n variables X 1 , . . . , X d•n . The PC α accepts a sequence of vectors x ∈ (Q d ) n , if the Boolean formula evaluates to true when plugging x into the polynomials p in α. The set of accepted sequences is denoted by α . Now let a ∈ N. A PC has a alternations if the positive Boolean combination has a alternations between disjunctions and conjunctions.In the following, a constrained polynomial representation (CPR) can be used to compute from a sequence of inputs (x 1 , . . . , x n ) with x 1 , . . . ,x n ∈ R d ′a new sequence of outputs (y 1 , . . . , y n ) with y 1 , . . . , y n ∈ R d . Formally, a CPR comprises for each i ∈ {1, . . . , n} a sequence (φ 1 , D 1 ), . . . , (φ si , D si ) of pairs (φ j , D j ), where each pair (φ j , D j ) is a "conditional assignment": each (φ j , D j ) tells us that if the condition φ j is satisfied, then we return D j ( x). More precisely: (i) each φ j is a polynomial constraint where all polynomials have degree ≤ 2, (ii) for any j ̸ = m, the constraints φ j and φ m are mutually exclusive, and (iii) each D j : R d ′ •n → R d is an affine transformation. Because of their role as conditional assignments, we also write φ j → D j for such pairs. For a ∈ N, we say that the CPR is a-alternation-bounded if each of the formulas φ j has at most a alternations. A CPR as above computes a functionR d ′ •n → R d•n : Given x = (x 1 , . . . , x n ) with x 1 , . . . , x n ∈ R d ′, it computes the sequence (y 1 , . . . , y n ) if for every i ∈ {1, . . . , n}, we have y i = D j ( x), provided that j is the (in case of existence uniquely determined) index for which φ j ( x) is satisfied. The size of PCs and CPRs are their bit lengths (see Appendix B for details). Proposition 5. Fix a UHAT with positional encoding and ℓ layers. For any given sequence length n, there exists a polynomial-sized PC α with O(ℓ) alternations such that α equals the set of accepted sequences of length n.Note that Proposition 5 implies that the set of sequences of each length n is a semialgebraic set [31] . The proof is by induction on the number of layers, which requires a slight strengthening: Lemma 6. Fix a UHAT with positional encoding and ℓ layers. For any given sequence length n, one can construct in polynomial time an O(ℓ)-alternation-bounded CPR computing the functionR d•(n+1) → R e•(n+1) computed by the UHAT.Proof. We prove the statement by induction on the number of layers. First, we consider the positional encoding p : N × N → R d as some affine transformations P i : R d•(n+1) → R d mapping the input sequence x to x i + p(i, n + 1). Then we obtain a CPR with ⊤ → P i for each 1 ≤ i ≤ n + 1. Now, suppose the statement is shown for ℓ layers and consider a UHAT with ℓ + 1 layers. Suppose that the first ℓ layers of our UHAT compute a function n+1) , and the last layer computes a function n+1) . By induction, we have a polynomial size CPR consisting of conditional assignments φ i,k → D i,k for every i ∈ {1, . . . , n + 1} andR d ′ •(n+1) → R d•(R d•(n+1) → R e•(1 ≤ k ≤ s i . Here, each D i,j is an affine transformation R d ′ •(n+1) → R d .Let us first consider the case that the last layer of our UHAT is a standard encoder layer. For each (i, I, j, J) ∈ {1, . . . , n + 1} 4 , we build the conditional assignment using the formula ψ i,I,j,J :j-1 m=1 sm M =1 φ m,M ∧ p i,I,j,J,m,M ( x) > 0 ∧ n+1 m=j+1 sm M =1 φ m,M ∧ p i,I,j,J,m,M ( x) ≥ 0where p i,I,j,J,m,M ( x) is the polynomial ⟨AD i,I x, BD j,J x -BD m,M x⟩. Then, the conditional assignment is φ i,I ∧ φ j,J ∧ ψ i,I,j,J → C(D i,I x, D j,J x). Here, the idea is that (i) φ i,I expresses that the I-th conditional assignment was used to produce the i-th cell in the previous layer, (ii) φ j,J says the J-th conditional assignment was used to produce the j-th vector in the previous layer, and (iii) ψ i,I,j,J says the vector x j yields the maximal attention score for the input x i , meaning (iii-a) for all positions m < j, x m has a lower score than x j (left parenthesis), and (iii-b) for all positions m > j, x m has at most the score of x j (right parenthesis). In (iii-a) and (iii-b), we first find the index M of the conditional assignment used to produce the m-th cell in the previous layer. Note that then indeed, all the PCs ψ i,I,j,I are mutually exclusive. Moreover, the polynomials ⟨AD i,I x, BD j,J x -BD m,M x⟩ have indeed degree 2 and are of size polynomial in n. Furthermore, if the assignments φ i,k → D i,k had at most a alternations, then the new assignments have at most a + 3 alternations. Finally, the case of ReLU layers is straightforward (see Appendix B).Finally, the proof of Proposition 5 is straightforward: from the constructed CPR in Lemma 6 we obtain the polynomial constraint s1 J=1 φ 1,J ∧ ⟨t, D 1,J x⟩ > 0 with a bounded number of alternations.Step II: Replace real coefficients by rationals In our proof, the key step is to replace the real coefficients in the PC by rational coefficients so that the rational PC will define the same set of rational sequences, up to some given size. Let us make this precise. We denote by Q ≤m = {a ∈ Q | ∥a∥ 2 ≤ m} the set of all rational numbers of size at most m. A polynomial constraint is rational if all the polynomials occurring in it have rational coefficients. Proposition 7. For every m ∈ N and every PC α with polynomials having n variables, there exists a rational PC α ′ of polynomial size such that α∩ Q n ≤m = α ′ ∩ Q n ≤m .Proving Proposition 7 requires the following technical lemma, for which we introduce some notation.For two vectors u, v ∈ R t and m ∈ N, we write u ∼ m v if for every w ∈ Q t and every z ∈ Q with ∥w∥ 2 , ∥z∥ 2 ≤ m, we have (i) ⟨w, u⟩ ≥ z if and only if ⟨w, v⟩ ≥ z and (ii) ⟨w, u⟩ > z if and only if ⟨w, v⟩ > z. In other words, we have u ∼ m v if and only if u and v satisfy exactly the same inequalities with rational coefficients of size at most m.Lemma 8. For every c ∈ R t and m ∈ N, there is a c ′ ∈ Q t with ∥c ′ ∥ 2 ≤ (mt) O (1) and c ∼ m c ′ .Remark 9. For proving Lemma 8, it is not sufficient to pick a rational c ′ with ∥c ′ -c∥ < ε for some small enough ε. For example, note that if in some coordinate, c contains a rational number of size ≤ m, then in this coordinate, c ′ and c must agree exactly for c ∼ m c ′ to hold.Before we prove Lemma 8, let us see how to deduce Proposition 7: in a PC α we understand each polynomial p(X 1 , . . . , X n ) as a scalar product ⟨w, u⟩ where w constains only variables and u consists of all coefficients. Then Lemma 8 yields a vector v ∼ 2m u containing only rationals with the same behavior as u. From this we finally obtain polynomials having only rational coefficients, which also proves Proposition 7. A detailed proof of Proposition 7 can be found in Appendix B.In the proof of Lemma 8, we use the following fact about solution sizes to systems of inequalities. 1) .Lemma 10. Let A ∈ Q k×n , A ′ ∈ Q ℓ×n , z ∈ Q k , z ′ ∈ Q ℓ with ∥A∥ 2 , ∥A ′ ∥ 2 , ∥z∥ 2 , ∥z ′ ∥ 2 ≤ m. If the inequalities Ax ≫ z and A ′ x ≥ z ′ have a solution in R n , then they have a solution r ∈ Q n with ∥r∥ 2 ≤ (mn) O(We prove Lemma 10 in the appendix. The proof idea is the following. By standard results about polyhedra, the set of vectors x satisfying Ax ≥ z and A ′ x ≥ z ′ can be written as the convex hull of some finite set X = {x 1 , . . . , x s }, plus the cone generated by some finite set {y 1 , . . . , y t }. Here, the vectors in X ∪ Y are all rational and of polynomial size. By the Carathéodory Theorem, the real solution s ∈ R n to As ≫ z and A ′ s ≥ z ′ belongs to the convex hull of n elements of X, plus a conic combination of n elements of Y . We then argue that by taking the barycenter of those n elements of X, plus the sum of the n elements of Y gives a rational vector r ∈ Q n with Ar ≫ z and A ′ r ≥ z ′ . The full proof of Lemma 10 is in Appendix B.4. To prove Lemma 8, given c ∈ R n , we set up a system of (exponentially many) inequalities of polynomial size so that the solutions are exactly the vectors d with d ∼ m c. The solution provided by Lemma 10 is the desired c ′ (see Appendix B.5).Step III: Constructing T C 0 circuits It is now straightforward to translate a polynomial-sized CPR with rational coefficients and bounded alternations into a TC 0 circuit: Proposition 11. Every language accepted by a UHAT with positional encoding is recognized by a family of circuits in TC 0 .We now show that the TC 0 upper bound is tight: There is a UHAT whose language is TC 0 -hard under AC 0 reductions. In particular, this language is not in AC 0 , since AC 0 is strictly included in TC 0 .Proposition 12. There is a TC 0 -complete language that is accepted by a UHAT, even without positional encoding and masking, but is not recognized by any family of circuits in AC 0 .Proof. As shown by Buss [6, Corollary 3], the problem of deciding whether ab = c for given binary encoded integers a, b, c ∈ Z is TC 0 -complete under AC 0 -reductions. Since ab = c if and only if ab > c -1 and -ab > -(c + 1), the problem of deciding ab > c is also TC 0 -complete. We exibit a UHAT such that the problem of deciding ab > c can be AC 0 -reduced to membership in the language.It suffices to define a UHAT T that accepts a language L ⊆ (Q 2 ) + such that for all r, s ∈ Q we have that (r, s) ∈ L if and only if r > s. Then we can reduce the test ab > c to checking whether (a, c b ) ∈ L. Note that formally, c b is represented as a string containing the binary encodings of c and b separated by a special symbol. The UHAT T is by definition initialized with the sequence (1, r, s), (0, 0, 0) ∈ Q 3 since we only have to consider the accepted language restricted to sequences of length 1. It can directly check that r -s > 0 using the acceptance vector t := (0, 1, -1).• The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.) • The assumptions made should be given (e.g., Normally distributed errors). • It should be clear whether the error bar is the standard deviation or the standard error of the mean. Justification: This is a theory paper with no direct societal impacts. Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.• Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
uhat and regular languages over infinite alphabets: 
 It was shown by Angluin et al. [2] that UHATs with no positional encoding on binary input strings accept only regular languages, even if masking is allowed. We show that UHATs with masking over data sequences can recognize "non-regular" languages over infinite alphabet (Theorem 2). More precisely, a standard notion of regularity over the alphabet Σ = Q d is that of symbolic automata (see the CACM article [11] ), since it extends and shares all nice closure and algorithmic properties of finite automata over finite alphabets, while at the same time permitting arithmetics. Intuitively, a transition rule in a symbolic automaton is of the form p → φ q, where φ represents the (potentially infinite) set S ⊆ Q d of solutions to an arithmetic constraint φ (e.g. 2x = y represents {(n, 2n) : n ∈ Q}). The meaning of such a transition rule is: move from state p to state q by reading any a ∈ S.To prove Theorem 2, we define the language Double := {(r 1 , . . . , r n ) ∈ Q n | n ≥ 1 and 2r i < r i+1 for all 1 ≤ i < n} of sequences of rational numbers where each number is more than double the preceding number. Lemma 13. UHAT with past masking and without positional encoding can recognize Double.Proof. Given an input sequence u 1 , . . . , u n+1 = (1, r 1 ), . . . , (1, r n ), (0, 0) ∈ Q 2 , we need to check that for all pairs 1 ≤ i < j < n + 1, we have 2 • r i < r j . To this end, a first standard encoder layer uses the differences 2r i -r j as attention scores-except for j = n + 1, where the attention score will be 0. This is achieved by setting the attention score for positions i, j [2] . Indeed, this evaluates to 2r i -r j for i < j < n + 1, and to 0 for i < j = n + 1. In particular, for a position i ∈ [1, n], the attention score is maximized at j = n + 1 if and only if 2r i < r j for all j ∈ [i + 1, n].to 2u i [2] • u j [1] -u jThe output vector v i at position i is then set to a i [1] , where a i is the attention vector at position i. Thus, the output vector has dimension 1, and for each i∈ [1, n + 1], we have v i = 0 if and only if 2 • r i < r j holds for all j ∈ [i + 1, n].In a second standard encoder layer we now check whether all v i have value 0. To this end, we choose for i < j ≤ n + 1 the attention score v j . Let b i denote the attention vector at position i. Then b i = 0 iff v i+1 , . . . , v n are all 0. We then outputw i = 1 -(v i + b i ), which is positive if and only if v i = • • • = v n+1 = 0.Finally, with the acceptance vector t = 1 we accept if and only ifw 1 > 0, which is equivalent to v 1 = • • • = v n+1 = 0.As we saw above, the latter holds if and only if 2r i < r j for all i, j with 1 ≤ i < j < n + 1.The proof of non-regularity of Double is easy (see Appendix C). One could also easily show that Double cannot be recognized by other existing models in the literature of formal language theory over infinite alphabets, e.g., register automata [4, 9, 24, 36, 41] , variable/parametric automata [16, 19, 23] , and data automata variants [5, 17] . For example, for register automata over (Q; <) (see the book [4] ), one could use the result therein that data sequences accepted by such an automaton are closed under any order-preserving map of the elements in the sequence (e.g., if 1, 2, 3 is accepted, then so is 10, 11, 20), which is not satisfied by Double. 
logical languages accepted by uhat: 
 In this section we show that an extension of linear temporal logic (LTL) with linear rational arithmetic (LRA) and unary numerical predicates is expressible in UHAT over data sequences (Theorem 3). A formula of dimension d > 0 in locally testable LTL ((LT) 2 L) has the following syntax:φ ::= ψ k (x 1 , . . . , x k+1 ) | Θ | ¬φ | φ ∨ φ | Xφ | φU φHere, ψ k for k ≥ 0 is an atom in LRA over the d-dimensional vectors of variables x i of the form ⟨a, (x 1 , . . . , x k+1 )⟩ + b > 0 where a ∈ Q d(k+1) and b ∈ Q. Intuitively, ψ k allows one to check the values in the sequence with k "lookaheads". Furthermore, Θ is a unary numerical predicate, i.e. a family of functions θ n : {1, . . . , n} → {0, 1} for all n ≥ 1. We define the satisfaction of an(LT) 2 L formula φ over a sequence v = (v 1 , . . . , v n ) of vectors in Q d at position i ∈ [1, n], written (v, i) |= φ,inductively as follows (omitting negation and disjunction):• (v, i) |= ψ k (x 1 , . . . , x k+1 ) iff i ≤ n -k and ψ k (v i , . . . , v i+k ) • (v, i) |= Θ iff θ n (i) = 1 • (v, i) |= Xφ iff i < n and (v, i + 1) |= φ • (v, i) |= φU ψ iff there is j ∈ [i, n] with (v, j) |= ψ and (v, k) |= φ for all k ∈ [i, j -1] We write L(φ) := {v ∈ (Q d ) + | (v, 1)|= φ} for the language of φ. Example 14. Consider sequences of the form x, Ax, A 2 x, . . . , A n x such that yA n x = 0 and n ≥ 0 is minimal with this property where y ∈ Q 1×d and A ∈ Q d×d are fixed and x ∈ Q d . Theorem 3 implies that this language is accepted by a UHAT since it is defined by the (LT) 2 L formula G[(¬Last → (yx 1 ̸ = 0 ∧ Ax 1 = x 2 )) ∧ (Last → yx 1 = 0)],where Last := ¬X⊤. Example 15. Take the standard notion of 7-day Simple Moving Average (7-SMA); this can be generalized to larger sliding windows of 50-days, or 100 days, which are often used in finance. Using (LT) 2 L, it is easy to show that the following notion of "uptrend" can be captured using UHAT: sequences of numbers such that the value at each time t is greater than the 7-SMA value at time t. The formula for this is:G(X 7 ⊤ → φ(x 1 , . . . , x 7 ))where φ(x) is the formula 7x 7 > 7 i=1 x i . Note here that Gψ means (as usual for LTL) "globally" ψ, which can be written as ¬(⊤U ¬ψ). Similarly, X i means that X is repeated i times.We assume UHATs with positional encoding and a zero vector at the end of the input sequence (see Section 2). In the following we always assume that the components from the positional encoding are implicitly given and are not changed by any UHAT. So we write the sequence in Eq. ( 1) as v 1 , . . . , v n , 0. We use the following results from [3] that also hold for UHATs over data sequences.Lemma 16. Let d > 0 and ℓ ∈ [1, d].1) For every b ∈ {0, 1} there is a UHAT with positional encoding that on every sequence v 1 , . . . ,v n ∈ Q d with v i [ℓ] ∈ {0, 1} for all i ∈ [1, n] outputs the sequence v 1 , . . . , v n-1 , (v n [1, ℓ -1], b, v n [ℓ + 1, d]).2) There is a UHAT layer with positional encoding that on every sequence v 1 , . . . , v n ∈ Q d and for every i ∈ [1, n -1] picks attention vector a i = v i+1 .3) There is a UHAT layer with positional encoding that on every sequence v 1 , . . . ,v n ∈ Q d , for every ℓ ∈ [1, d] with v 1 [ℓ], . . . , v n-1 [ℓ] ∈ {0, 1} and v n [ℓ] = 0, and for every i ∈ [1, n] picks attention vector a i = v j with minimal j ∈ [i, n] such that v j [ℓ] = 0.Here, 2) and 3) directly follow from [3] . For 1) we remark that in [3] only the case b = 0 is shown. On input v 1 , . . . , v n as in 1), the UHAT uses positional encoding function p(i, n) := (i, n)and a composition of affine transformations and ReLU to output at position i ∈ [1, n] the vector(v i [1, ℓ -1], b i , v i [ℓ + 1, d]) where b i := min{v i [ℓ], n -i} if b = 0 and b i := max{v i [ℓ], i -n + 1} if b = 1.Using Lemma 16, we show that a UHAT can transform rational values > 0 to 1 and values ≤ 0 to 0. This will be used to evaluate inequalities by outputting 1 for true and 0 for false.Lemma 17. Let d > 0 and ℓ ∈ [1, d].There is a UHAT with positional encoding that on every sequence v 1 , . . . ,v n+1 ∈ Q d outputs v ′ 1 , . . . , v ′ n+1 ∈ Q d with v ′ i := (v i [1, ℓ -1], b i , v i [ℓ + 1, d]) for all i ∈ [1, n + 1] where b i := 1 if v i [ℓ] > 0 and b i := 0 otherwise. Proof. On input v 1 , . . . , v n+1 ∈ Q d , the first layer outputs at position i ∈ [1, n + 1] the vector w i := (v i [1, ℓ -1], r i , v i [ℓ + 1, d])where r i := max{v i [ℓ], 0}. Thus, r i = 0 if v i [ℓ] ≤ 0 and r i > 0 otherwise. The second layer turns the sequence w 1 , . . . , w n+1 into (0, w 1 ), . . . , (0, w n+1 ). We then apply 1) of Lemma 16 to obtain the sequence (0, w 1 ), . . . , (0, w n ), (1, w n+1 ), i.e. the last vector has first component 1, and all other vectors have first component 0. Let u 1 , . . . , u n+1 ∈ Q d+1 be the resulting sequence. The final layer uses attention score ⟨Au i , Bu j ⟩ for all 1 ≤ i, j ≤ n + 1 where the affine transformations A, B :Q d+1 → Q d+1 yield Au i = (u i [ℓ], 0, . . . , 0)and Bu j = (u j [1] , 0, . . . , 0). Let a i be the attention vector of positioni ∈ [1, n + 1]. Since u i [ℓ] ≥ 0, we have a i [1] = 0 if u i [ℓ] = 0 and a i [1] = 1 if u i [ℓ] > 0. The layer outputs v ′ i := (u i [2, ℓ], a i [1], u i [ℓ + 2, d + 1]) at position i ∈ [1, n + 1].We now prove Theorem 3. We claim that for every (LT) 2 L formula φ of dimension d and every m ≥ d there exists a UHAT T φ,m with positional encoding that on every sequence w 1 , . . . ,w n , 0 ∈ Q m outputs a sequence w ′ 1 , . . . , w ′ n , 0 ∈ Q m+1 such that for all i ∈ [1, n] we have w ′ i [1, m] = w i and w ′ i [m + 1] = 1 if (v, i) |= φ and w ′ i [m + 1] = 0 otherwise, where v := (w 1 [1, d], . . . , w n [1, d]). Then the theorem follows since for every (LT) 2 L formula φ of dimension d the UHAT T φ,d outputs on every sequencev = (v 1 , . . . , v n ) of vectors in Q d extended with the vector 0 ∈ Q d a sequence v ′ 1 , . . . , v ′ n , 0 ∈ Q d+1 such that v ′ 1 [d + 1] > 0 if and only if (v, 1) |= φ.Thus, T φ,d accepts L(φ) by taking the acceptance vector t := (0, . . . , 0, 1) ∈ Q d+1 . We prove the claim by induction on the structure of (LT) 2 L formulas. If the formula is a unary numerical predicate Θ, then we can use the positional encoding p(i, n + 1) := θ n (i) for all i ∈ [1, n] and p(n + 1, n + 1) := 0 to output on every sequence w 1 , . . . , w n , 0 ∈ Q m the sequence (w 1 , p(1, n + 1)), . . . , (w n , p(n, n + 1)), (0, p(n+ 1, n + 1)) ∈ Q m+1 .If the formula is an atom ψ k (x 1 , . . . , x k+1 ) of the form ⟨a, (x 1 , . . . , x k+1 )⟩ + b > 0, the UHAT T ψ k ,m adds in its first layer a component that is set to 1 to the top of every vector, outputting on every sequence w 1 , . . . , w n , 0 ∈ Q m the sequence (1, w 1 ), . . . , (1, w n ), (1, 0). Then we apply 1) of Lemma 16 to turn this sequence into (1, w 1 ), . . . , (1, w n ), 0. Next, T ψ k ,m uses k layers to allow each position to gather the first d + 1 components of its k right neighbors. More precisely, the ℓ-th layer, for ℓ ∈ [1, k], on sequence u 1 , . . . , u n+1 uses 2) of Lemma 16 to get for every position i ∈ [1, n] the attention vector a i = u i+1 and the attention vector a n+1 is arbitrary. Note that if ℓ = 1, then a n = 0. Then it applies an affine transformation to output at position i ∈ [1, n] the vector (a i [1, d + 1], u i ) and using 1) at position n + 1 the vector (0, a n+1 [2, d + 1], u n+1 ). Let u 1 , . . . , u n+1 ∈ Q k(d+1)+m+1 be the output of the k-th of those layers. We add another layer that using a composition of ReLU and affine functions outputs at every position i ∈ [1, n + 1] the vectoru ′ i := (u i [k(d + 1) + 2, k(d + 1) + m + 1], r i ) ∈ Q m+1 where r i := min{u i [1], ⟨a, ûi ⟩ + b} and ûi := (u i [2, d + 1], u i [d + 3, 2(d + 1)], . . . , u i [kd + k + 2, (k + 1)(d + 1)]),which contains the first d components of the initial input vector and its k right neighbors. That is, for all i ∈ [1, n] we have that r i = 0 if ⟨a, ûi ⟩ + b ≤ 0 or i + k > n since u i [1] can only be 0 if it was gathered from the vector at position n + 1 using attention. Furthermore,r i > 0 if ⟨a, ûi ⟩ + b > 0 and i + k ≤ n. Note that u ′ i [1, m]is equal to the input vector w i from the beginning if i ∈ [1, n] and 0 if i = n + 1. Finally, we apply Lemma 17 followed by 1) to output at position i ∈ [1, n] the vectorw ′ i := (u ′ i [1, m], r ′ i )where r ′ i := 1 if r i > 0 and r ′ i := 0 otherwise and at position n + 1 the vectorw ′ n+1 := (u ′ n+1 [1, m], 0) = 0. Thus, for all i ∈ [1, n] we have that w ′ i [m + 1] = 1 if (v, i) |= ψ k and w ′ i [m + 1] = 0 otherwise, where v := (w 1 [1, d], . . . , w n [1, d]).Let us now continue with the inductive step where we assume that φ and ψ are (LT) 2 L formulas of dimension d such that for all m ≥ d we already showed existence of the UHATs T φ,m and T ψ,m+1 .For the cases ¬φ, φ∨ψ, and Xφ we refer to Appendix D. For φU ψ define the UHAT T φU ψ,m that first applies T ψ,m+1 • T φ,m outputting a sequence u 1 , . . . , u n , 0 ∈ Q m+2 . Observe that (v, i) |= φU ψ for i ∈ [1, n] and v := (u 1 [1, d] , . . . , u n [1, d] ) if and only if for the minimal j ∈ [i, n] with (v, j) |= ¬φ ∨ ψ we have (v, j) |= ψ and such a j exists. Equivalently, for the minimal j ∈ [i, n + 1] with min{u j [m+1], 1-u j [m+2]} = 0 it holds that u j [m+2] = 1. To check this, we first add a layer that outputs at position i ∈ [1, n + 1] the vector u ′i := (u i , min{u i [m + 1], 1 -u i [m + 2]}) ∈ Q m+3 .Finally, we add a layer that uses 3) of Lemma 16 to get attention vector a i = u ′ j with j ∈ [i, n + 1] minimal such that u ′ j [m + 3] = 0. The layer then outputs at position i ∈ [1, n + 1] the vectorw ′ i := (u ′ i [1, m], a i [m + 2]) ∈ Q m+1 . 
concluding remarks: 
 We initiated the study of the expressive power of transformers, when the input is a sequence of (tuples of) numbers, which is the setting for applications like time series analysis/forecasting. Our results indicate an increased expressiveness of transformers on such input data, in comparison to the previous formal language theoretic setting (see survey [40] ), i.e., when a token embedding function (with a bounded number of tokens) is first applied before feeding the input to a transformer. More precisely, this represents for Unique Hard Attention Transformers (UHAT) a jump from the complexity class AC 0 to TC 0 (since AC 0 ⊊ TC 0 ), and the jump from regular to non-regular languages (when position encoding is not allowed). On the positive side, we successfully developed an expressive class of logical languages recognized by UHAT in terms of a logic called locally testable LTL, which extends previously identified logic for UHAT for strings over finite alphabets [2, 3] .Limitations. While we follow the standard formalization of transformer encoders in Formal Languages and Neural Networks (e.g. [3, 20, 21, 40] ), limitations of the models are known (see [40] for a thorough discussion). For example, used real numbers could be of unbounded precision, which allow one to precisely represent values of sin and cos functions (actually used in practice for positional encoding). In addition, the positional encoding used by the model could be uncomputable. Three answers can be given. First, an upper bound complexity on the model with unbounded precision and arbitrary positional encodings (e.g. in TC 0 ) still applies in the case of bounded precision. Second, limiting the power of UHAT (e.g. allow only rational numbers, and assuming efficient (i.e. uniform TC 0 ) computability of the positional encoding p : N × N → Q d ), our proof in fact yields uniformity of our TC 0 upper bound. Third, our lower bound for non-regularity of UHAT (cf. Theorem 2) holds even with only rational numbers and no positional encodings. Finally, to alleviate these issues, we have always made an explicit distinction between UHAT with and without positional encodings.Future directions. Our paper opens up a plethora of research avenues on the expressive power of transformers on data sequences. In particular, one could consider other transformer encoder models that have been considered in the formal language theoretic setting to transformers (see the survey [40] ). For example, instead of unique hard attention mechanism, we could consider the expressive power of transformers on data sequences using average hard attention mechanism. Similar question could be asked if we use a softmax function instead of a hard attention, which begs the question of which numerical functions could be computed in different circuit complexity classes like TC 0 . Another important question concerns a logical characterization for UHAT over sequences of numbers. This is actually still an open question even for the case of finite alphabets. Barcelo et al. [3] showed that first-order logic (equivalently, LTL) with monadic numerical predicates (called LTL(Mon)) is subsumed in UHAT with arbitrary position encodings, i.e., the transformer model that we are generalizing in this paper to sequences of numbers. There are UHAT languages (e.g. the set of palindromes) that are not captured by this. As remarked in [3] , LTL(Mon) can be extended with arbitrary linear orders on the positions (parameterized by lengths), which then can define the palindromes. [An analogous extension for (LT) 2 L can define palindromes over an infinite alphabet.] However, it is possible to show that the resulting logic is still not expressive enough to capture the full generality of UHAT. That said, although our logic does not capture the full UHAT, it can still be used to see at a glance what languages can be recognized by UHAT (e.g. Simple Moving Averages). There could perhaps be a hope of obtaining a precise logical characterization if we restrict the model of UHAT. The recent paper [2] showed that LTL(Mon) captures precisely the languages of masked UHAT with position encodings with "finite image". It is interesting to study similar restrictions for UHAT in the case of sequences of numbers.We present here an example UHAT in which two real numbers α and β occur (each occurs once in a matrix associated to a particular layer) such that the simple sequenceEQUATIONwhere e i ∈ R 3 is the i-th unit vector, is accepted if and only if αβ = 2 and α = β. This shows that even if we restrict the input sequence to a particular number B of bits (e.g. the number of bits to represent the input sequence Eq. ( 2)), it is not possible to replace the real constants α and β by rational numbers without changing the accepted sequences of up to B bits: The sequence Eq. ( 2) is only accepted if α = β = √ 2. And if we change α or β in any way, the sequence Eq. ( 2) will not be accepted anymore. 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?Answer: [NA] Justification: This is a theory paper with neither experiments, codes, nor the use of datasets.Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort.12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?Answer: [NA] Justification: This is a theory paper that uses no code, data, and models. We do not use assets of others in any form.Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.• If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode.com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset. • For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. • If this information is not available online, the authors are encouraged to reach out to the asset's creators. 
new assets: 
 Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?Answer: [NA] Justification: We do not release new assets.Guidelines:• The answer NA means that the paper does not release new assets.• Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc. • The paper should discuss whether and how consent was obtained from people whose asset is used. • At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file. 
crowdsourcing and research with human subjects: 
 Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?Answer: [NA] Justification: This is a theory paper with no crowdsourcing and no human subjects.Guidelines:• The answer NA means that the paper does not involve crowdsourcing nor research with human subjects. • Including this information in the supplemental material is fine, but if the main contribution of the paper involves human subjects, then as much detail as possible should be included in the main paper. • According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector. 
institutional review board (irb) approvals or equivalent for research with human subjects: 
 Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?Answer: [NA] Justification: This is a theory paper with no crowdsourcing and no human subjects.Guidelines:• The answer NA means that the paper does not involve crowdsourcing nor research with human subjects. • Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.• We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution. • For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.38th Conference on Neural Information Processing Systems (NeurIPS 2024).First, use a standard encoding layer to transform the sequence (x1, . . . , xn) ∈ Σ n into (r -1 x1 -1, . . . , r -1 xn -1) ∈ Σ n . Then, accept if and only if the left-most vector is > 0.2 This is because all employed affine transformations (which are rational matrices), but also the values p(1, 2), p(2, 2) ∈ Q of the positional encoding can be described using finitely many bits. 
 
 Appendix:  


Decision: All reviewers agree that the submission makes a significant contribution on revealing the expressive power of transformers through the lens of formal languages, and that several important findings are drawn. Although all reviewers pointed out some potential weaknesses, all of them are addressed by the authors in rebuttal. All reviewers seem satisfactory on the responses and give positive confirmations, leaving only some comments on improving the presentation which are easy to handle. Considering the significant theoretical contributions of the submission, a spotlight acceptance is recommended.

Reviews: review: paper_summary: paper_summary: This paper studies the expressive power of transformer encoders with leftmost-hard attention and strict past-masking, where the input is not a sequence of symbols from a finite alphabet, but a sequence of rational vectors. The three main results are:

1. Transformers (under the assumptions above, with or without position encodings) are in TC0 but not in AC0.
2. There is a UHAT that recognizes a non-regular language (that is, cannot be accepted by a finite automaton whose transitions are labeled with arithmetic constraints instead of symbols).
3. Every language definable in locally testable linear temporal logic (that is, linear temporal logic where an atomic formula can check a linear constraint on the current “symbol” and k lookahead “symbols”) is recognizable by a UHAT with position encoding.
strength_weakness: strength_weakness: Theorem 1: I didn’t exactly understand why the inputs are rational vectors but the parameters are allowed to be real. Appendix A shows why allowing reals makes a difference, but:
(a) It doesn’t explain why the difference is important.
(b) It doesn’t show that language (2) requires real parameters, only that a particular UHAT requires real parameters to recognize language (2).
(c) One could make exactly the same argument about UHATs for strings over a finite alphabet.

With rational weights, I take it Proposition 9 would be fairly easy.

How do you define Boolean circuits that take sequences of rational vectors as input? This is hinted at in line 273 but should be spelled out more explicitly for Proposition 10 and its proof to be clear.

Theorem 2: I think it would be helpful not to reuse variable names.

Theorem 3: Just a minor comment on the phrase “logical language” in the title of Section 5. I understand a “logical language” to be the syntax of a logic, not the set of strings models of a logical sentence, so I find this phrase confusing.
questions: questions: Could you explain why it's important for the parameters to be real, not just rational?

How do you define Boolean circuits that take sequences of rational vectors as input?

Could you expand on the significance, in this setting, of the classes AC0, regular, and TC0? Perhaps it would be helpful to give some examples of languages that do/don’t belong to these classes and expand on the practical implications. You allude to the language at lines 321-324 being important, but don’t explain why.
limitations: limitations: Yes
paper_summary: paper_summary: The paper studies the computational expressiveness of unique hard attention transformers (UHAT) on formal languages formed over an infinite alphabet. The work is motivated by the application of transformers to time series forecasting where input values can be unbounded. Specifically, the authors assume the language to be formed over tuples of rational numbers. To this end, the paper contributes three novel results: (1) The languages recognized by UHAT belong to the circuit complexity class $\mathsf{TC}^0$ and there exists a language recognized by UHAT which is $\mathsf{TC}^0$-hard. (2) There exists a non-regular language over the alphabet $\mathbb{Q}^d$ that is recognized by a UHAT with past masking and no positional encoding. (3) UHAT with positional encoding recognize all languages expressible in an extension linear-time temporal logic with unary numerical predicates and linear rational arithmetic.
strength_weakness: strength_weakness: - There seems to be an important restriction to the first result: because real precision is assumed for UHAT, language inclusion can only be shown for words up to a particular length n. I assume that without this restriction the two classes are actually incomparable. At the same time, the authors seem to suggest in the concluding remarks that some results still hold when assuming rational precision for UHAT. The importance and implications of this choice should be discussed more clearly in the paper.
- The paper does not clearly convey the practical implications of the results. The infinite precision of rational numbers can not be represented in real-world systems. Instead, they would be approximated by floating point numbers such that the result of previous work applies.
- Minor: It would be helpful if the abstract already states that arbitrary input refers to the rational numbers, to avoid confusion with a real-valued input.
questions: questions: Do the same results hold for formal languages over the alphabet $\mathbb{Q}$? If yes, why are the results derived in terms of tuples?
limitations: limitations: The authors have addressed limitations adequately, except for the real precision of UHAT. As detailed in the review it seems that some results only hold for inputs up to a particular length n. The theorems themselves do not state this.
paper_summary: paper_summary: This paper focuses on analyzing the expressive power of transformers through the lens of formal languages, inspired by Angluin's approach. Specifically, while traditional unique hard attention transformers (UHAT) on strings are associated with $AC^0$ and regular languages definable in first-order logic, the authors here explore the implications of using data sequences instead of words as input. The main findings are:
- UHATs over data sequences with positional encodings fall within $TC^0$, not $AC^0$.
- Non-regular languages can be recognized even by masked UHATs without positional encodings.
- UHATs can recognize all languages definable in $(LT^2)L$, an extension of LTL with unary predicates and local arithmetic tests over finite windows over the data.
strength_weakness: strength_weakness: **W1: Coverage of $TC^0$**
While the characterization of UHAT on data sequences in $TC^0$ is commendable, it does not fully encompass $TC^0$. A precise characterization of the power of UHATs would strengthen the paper. This observation also applies to the other main results: Which logic precisely captures UHAT?

**W2: Accessibility**
The authors make little effort to make the paper accessible to the broader ML community. As it stands, the paper could have been submitted to any computer science theory conference. Consequently, the results may not be surprising to those communities.

**W3: Practical Implications**
The paper lacks discussion on the practical implications of the theoretical analysis for transformer design. Coupling the theory with practical insights would enhance the paper's value.

In summary, the paper provides significant insights into the expressive power of transformers over data sequences, presenting elegant and theoretically sound results. However, a broader characterization of UHATs' power, increased accessibility for a wider audience, and practical implications would strengthen the paper further.
questions: questions: Please comment on **W1** and **W3**.
limitations: limitations: This has been addressed in a satisfactory way by the authors.

Comments: title: Rebuttal Read
comment: I thank the authors for their detailed rebuttal, in particular for clarifying on the input length $n$. This was indeed a misunderstanding on my part.
Thanks for your responses!
I have read the rebuttal. Thank you for your responses. There are indeed interesting open questions here related to the logic. The "application" related comment serves as a good additional motivation and should preferably be added to the paper.