Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers

Authors: andy  yang
david  chiang
Venue: colmweb_org_COLM_2024_Conference
Published: 2024-03-23 04:22:42

Abstract: Deriving formal bounds on the expressivity of transformers, as well as studying transformers that are constructed to implement known algorithms, are both effective methods for better understanding the computational power of transformers. Towards both ends, we introduce the temporal counting logic $\textbf{K}_t$[#] alongside the RASP variant $\textbf{C-RASP}$. We show they are equivalent to each other, and that together they are the best-known lower bound on the formal expressivity of future-masked soft attention transformers with unbounded input size. We prove this by showing all $\textbf{K}_t$[#] formulas can be compiled into these transformers without any additional positional embeddings.

Main paper: 
 introduction: 
 What problems can transformers (Vaswani et al., 2017) solve, what problems can they not solve, and how can we prove it? Formal logic, in connection with programming language theory, formal language theory, and finite model theory, give a framework in which to investigate these questions.Previous theoretical work, as surveyed by Strobl et al. (2024) , has advanced our understanding of transformers immensely. However, it has not provided a full account of their expressive power. Much of this work only considers modifications of transformers, like average-hard attention transformers (AHATs) (Barcel ó et al., 2024) or unique-hard attention transformers (UHATs) (Angluin et al., 2023) , which are not known to be either a subset or superset of standard, soft-attention transformers (SMATs). At the same time, programming languages like RASP (Weiss et al., 2021) propose a human-readable language with which to understand transformer computations. However, current languages compile into transformers that appear to be more powerful than standard transformers (Weiss et al., 2021) , or require approximations and restrictions on input length (Lindner et al., 2023) to do so.Here, we target soft attention transformers (as originally defined (Vaswani et al., 2017) and as used in practice). We prove that future-masked soft attention transformer encoders, with no restriction on input length, can recognize all the formal languages defined by formulas of K t [#], a temporal counting logic. Along the way we develop a RASP variant called C-RASP, equivalent to K t [#] . Both are, to our knowledge, the tightest-known lower bound on the expressivity of soft attention transformer encoders. Our contributions are as follows:-We define C-RASP, the first variant of RASP that provably compiles into future-masked soft attention transformer encoders with no restrictions on the input length. -We prove that C-RASP is equivalent to K t [#] .-We prove that the previous best lower bound, FOC[+; MOD] (Chiang et al., 2023) , is strictly less expressive than K t [#] . -We prove that transformers which use fixed-precision numbers (as real-world transformers do) can be compiled back to K t [#] . 
background: 
 Previous theoretical work on the expressivity of transformers has related them to a variety of automata, circuit classes, and logics, all under varying assumptions (Strobl et al., 2024) .Here, we focus on using logics to characterize soft attention transformer encoders with future masking. In particular, these encoders perform the same computations as one step of a transformer decoder. Decoder-only models like GPT (OpenAI, 2023) currently dominate applications of transformers, while empirical work has noted they have significant limits and perplexing behavior. We believe theoretical analysis can provide valuable insight towards understanding how to best use these models in practice.The previous best upper bound on log-precision transformers (which are argued to closely approximate real-life behavior) is TC 0 (Merrill and Sabharwal, 2023) . The previous best lower bound is FOC[+; MOD] (Chiang et al., 2023) . We strengthen this lower bound using K t [#], a temporal counting logic, and C-RASP, a new variant of the programming language RASP. We show both can be simulated by soft attention transformers.Many previous works have investigated the expressivity of hard attention transformers, including Angluin et al. (2023) ; Barcel ó et al. (2024) ; Yao et al. (2021) . However, reconciling the differences between the theoretical model of AHATs and the standard SMATs actually remains a very open area of inquiry at the moment.In particular, it is not yet clear how the expressivity bounds on average-hard attention transformers apply to softmax attention transformers. On the one hand, average-hard attention transformers can express sparse attention patterns by assigning weights of zero to positions, but soft attention transformers can only approximate these patterns (scores are always non-zero). On the other hand SMATs can express non-uniform attention patterns, which AHATs cannot. As such it is not known whether softmax attention can simulate average-hard attention (or even the other way around), so lower bounds on the expressivity of average-hard attention transformers cannot directly be applied to soft attention transformers.Thus, while the counting logic LTL(C, +) (Barcel ó et al., 2024) contains K t [#], we note that they only prove it is a lower bound for average-hard attention transformers, not soft attention transformers. We can view K t [#] and C-RASP as a gentle enough restriction of LTL(C, +) so as to render it simulatable by softmax attention transformers, but still above previous known bounds. We hope future work will clarify the disparities between averagehard and softmax attention.Implementing algorithms in transformers using human-readable programming languages gives researchers and engineers a deeper understanding of the computations transformers can perform. We believe that using this formalism to understand transformers has not only pedagogical benefits, but theoretical ones as well. For example, this perspective has been used by Zhou et al. (2024) to shed light on the length-generalization capabilities of transformers.These programming languages promise to compile into transformers that implement known algorithms, which are therefore interpretable by construction. However, existing examples make several unrealistic assumptions about transformers, rendering them inappropriate for compilation into standard transformers.The primary example is RASP, which makes three strong assumptions. First, the transformers that RASP compiles into use average-hard attention, which are not known to be exactly simulated by soft attention transformers (although average-hard attention behavior has been observed to be learned approximately, in practice (Merrill et al., 2021) ). Second, the attention weights (selectors) are not restricted to be dot-products of query and key vectors;this allows compilation of expressions involving arbitrary binary predicates like x = y or x < y. Third, they assume position-wise feed-forward networks can implement any computable function, with the rationale that any continuous function can be approximated by the universal approximation theorem (Hornik et al., 1989) .Building on RASP, Tracr (Lindner et al., 2023) compiles a subset of RASP into standard transformers. It compiles RASP selectors to dot-product attention, although this requires a syntactic restriction on selectors and a maximum string length, and it compiles RASP element-wise operations to ReLU FFNs, though only approximately.Furthermore, neither of these consider layer normalization, which Brody et al. (2023) show contributes to the expressivity of transformers.Here, we define a variant of RASP that has more restrictions, but that can be compiled exactly into a soft attention transformer encoder. Our variant, C-RASP, is based on the temporal counting logic K t [#].Counting logics are a rich area (van Benthem and Icard, 2023) of logic, whose connection with transformers has been noted by Chiang et al. (2023) and Barcel ó et al. (2024) . In essence, uniform attention patterns -where attention is spread evenly across positionscan very naturally simulate counting terms. A technical challenge when simulating variants of first-order logic with transformers is that a formula with k free variables, each of which is interpreted as a position in from 1 to n, would seem to correspond to a tensor of n k values in the corresponding transformer, but transformers only have n values at each layer and n 2 values in the attention weights.Whereas FOC[+; MOD] avoids this difficulty by using a normal form with only one variable, Angluin et al. (2023) and Barcel ó et al. (2024) avoid it by relying on linear temporal logic.Temporal logics (Gabbay et al., 1980) have been widely adopted as tools for the formal verification of state properties during the execution of programs over time. Intuitively, temporal logics can be used to formalize statements such as the following:Until the first train arrived at the gate, the bar remained lowered. My arm has been sore since Tuesday. At no point will the temperature go below zero.More abstractly, we can also use the syntax of temporal logic to specify the occurance of symbols in a string w.Until the first symbol t, w contains only l's. Only the symbol s has appeared since position 2 in w.At no position does w contains a z.We believe that temporal logics are a very appropriate specification language for thinking about masked self-attention. Firstly, the temporal accessibility relation -properties at time i can only depend on times j ≤ i -provides a natural way to model future-masking in transformers. Secondly, the restricted use of variables in temporal logic corresponds closely to the computational processing resources of the standard transformer, where scores depend on only two positions. Finally, temporal logics are highly-utilized in the field of formal methods (Fisher, 2011) , so solidifying this connection with transformers may allow more ideas to get shared across disciplines.Counting operations count the positions j ≤ i such that P(j) holds, returning the sum. We could also extend the syntax to use an expression P(i, j) which depends on both i and j; this can be transformed to P(j) since our logic has only unary predicates, as shown in Lemma A. C ( (i) := # [j ≤ i] Q ( (j)The number of ( up to position iC ) (i) := # [j ≤ i] Q ) (j)The number of ) up to position iV(i) := C ( (i) < C ) (i) Violation: there are more ) than ( C V (i) := # [j ≤ i] V(j) The number of Violations M(i) := C V (i) = 0 Matched: zero Violations B(i) := C ( (i) = C ) (i)Balanced: same number of ( and )D(i) := M(i) ∧ B(i)String is Matched and Balanced 
the temporal counting logic k t [#]: 
 In this section, we define the temporal counting logic K t [#].The temporal logic we target here is the past fragment of the Minimal Tense Logic (Rescher and Urquhart, 2012) , with counting terms (Barcel ó et al., 2024) . It can also be thought of as a modal logic with arithmetic constraints, like that of Demri and Lugiez (2010) , simply restricted to the setting where the structures are strings.We present the syntax of K t [#] in Backus-Naur form:1 F ::= Q a | ¬F | F ∧ F | C ≤ C | ⊤ C ::= #[F] | C + C | C -C | 1In temporal logics, formulas and terms are written without arguments because they are always interpreted with respect to a structure at a specified position. In our setting, they are interpreted with respect to a string w at a position i, wherew = w 1 w 2 • • • w n and i ∈ [1, n].A count term C is interpreted as an integer, written C w,i and defined as follows.#[F] w,i = |{j ∈ [1, i] | w, j ⊨ F}| (C 1 + C 2 ) w,i = C w,i 1 + C w,i 2 (C 1 -C 2 ) w,i = C w,i 1 -C w,i 2 1 w,i = 1As syntactic sugar, we allow the use of any natural number as a constant, which implicitly is defined as a sum of 1's. Similarly, 0 can be defined as #[¬⊤], and i as #[⊤]. Next, the interpretation of a formula F at position i, written w, i ⊨ F, defined as follows:w, i ⊨ Q a ⇐⇒ w i = a w, i ⊨ ¬F ⇐⇒ w, i ̸ ⊨ F w, i ⊨ F 1 ∧ F 2 ⇐⇒ w, i ⊨ F 1 and w, i ⊨ F 2 w, i ⊨ C 1 ≤ C 2 ⇐⇒ C w,i 1 ≤ C w,i 2 w, i ⊨ ⊤ is always the caseWe say that a string w with length n end-satisfies ϕ a formula of K t [#] whenever w, n ⊨ ϕ (Maler and Pnueli, 1990) . The language defined by ϕ is the set of all strings end-satisfied by ϕ. As a final note, whenever w is implicit, we can write F(i) which is True iff w, i ⊨ F and also write C(i) which is equal to C w,i .Although an exact characterization of K t [#] is not currently known, we can see that it can define a variety of regular, context-free, and non-context-free languages.Language Formulaa * b * #[Q a ∧ (#[Q b ] ≥ 1)] = 0 a * b * a * #[Q b ∧ #[Q a ∧ (#[Q b ] ≥ 1)] ≥ 1] = 0 a n b n c n #[Q b ∧ (#[Q c ] = 0)] = #[Q b ] ∧#[Q a ∧ (#[Q b ∨ Q c ] = 0)] = #[Q a ] ∧#[Q a ] = #[Q b ] ∧ #[Q b ] = #[Q c ] ∧ #[Q c ] = #[Q a ] Dyck-1 # Q ( = # Q ) ∧ # # Q ) > # Q ( = 0 hello #[⊤] = 5 ∧ Q o ∧ #[Q l ∧ #[Q e ∧ #[Q h ] = 1] = 1] = 2It is of note that the context sensitive language a n b n c n has been observed to be learnable by transformers (Bhattamishra et al., 2020) .Definition 4.1. The modal depth of a formula ϕ or term C, which we notate as md(ϕ), is the maximum level of nesting of # terms. That is,md(Q σ ) = 0 md(1) = 0 md(¬ϕ) = md(ϕ) md(#[ϕ]) = 1 + md(ϕ) md(ϕ 1 ∧ ϕ 2 ) = max(md(ϕ 1 ), md(ϕ 2 )) md(C 1 + C 2 ) = max(md(C 1 ), md(C 2 )) md(C 1 ≤ C 2 ) = max(md(C 1 ), md(C 2 ))The following construction gives some intuition on the effect of modal depth. Lemma 4.2. For every string s of length n, there exists a formula ϕ a of modal depth n such that w ⊨ ϕ a if and only if w contains s as a subsequence. Proof. Let s = s 1 s 2 • • • s n . Then define ϕ s := τ n ≥ 1 whereτ 1 := #[Q s 1 ] τ k+1 := # Q s k+1 ∧ τ k ≥ 1 s k ̸ = s k+1 # Q s k+1 ∧ τ k ≥ 2 s k = s k+1Verification is left as an exercise for the reader.As a consequence of the above and Theorem 5.7, we see that masked soft attention transformers can recognize all the piecewise testable languages (Klíma and Polák, 2010) , a subset of the star-free languages. Recall, however, that K t [#] can express much more: for example, the context sensitive language a n b n c n . A comprehensive study of the expressive power of K t [#] and C-RASP (and the effect of modal depth on expressivity) would be informative, and is left for future work.C-RASP may have a more convenient syntax to write programs in, but C-RASP programs and K t [#] formulas are exactly equivalent in expressivity. Theorem 4.3. A C-RASP program recognizes language L iff a K t [#] formula defines L. More precisely, given alphabet Σ, for any K t [#] formula ϕ there is a C-RASP program P such that w ∈ Σ * end-satisfies ϕ iff w is accepted by P, and vice versa. Proof. See Appendix A.3. 
from k t [#] to masked-attention transformers: 
 In this section, we show how to compile K t [#] into transformers. It would also be possible to translate directly from C-RASP to transformers; this would use fewer dimensions, but more layers.We assume familiarity with the transformer architecture (Vaswani et al., 2017) , and only review the basic definitions particular to our setting. To simplify our analysis, we do not consider positional encodings at first, deferring them to Section 6. Definition 5.1. (Word Embeddings) Let w be an input string of length n over a finite alphabet Σ. We prepend to w a special symbol BOS, which we assume is not in Σ. We abbreviate n + 1 as n ′ . A word embedding with dimension d over Σ is a function WE : Σ ∪ {BOS} → R d applied position-wise to a string of length n to form a tensor in R d×n ′ . Definition 5.2 (Transformer Block). A transformer block B, defined with a dimension d, specifies a function B : R d×n ′ → R d×n ′ that computesB(A) = LN 2 (FFN(A ′ ) + A ′ ) A ′ = LN 1 (SA(A) + A)where SA denotes a self-attention layer, by the standard definition (Vaswani et al., 2017) , FFN denotes a two layer feed-forward neural network with ReLU activations between the layers, and LN 1 and LN 2 denote position-wise applications of LayerNorm. This setup is commonly referred to as a "post-norm" block.The input and output of a transformer block are tensors in R d×n ′ . The resulting sequence of tensors across transformer blocks is sometimes referred to as the "residual stream" (Elhage et al., 2021) . We store the values of each subformula or count term of a K t [#] formula in a different dimension of the residual stream.Let A ∈ R d×n ′ be a tensor in the residual stream. Formulas ϕ k are stored as two rows of A:A 2k-1:2k, * = 1 -2ϕ k (1) + 1 -2ϕ k (2) + 1 • • • -2ϕ k (n) + 1 -1 +2ϕ k (1) -1 +2ϕ k (2) -1 • • • +2ϕ k (n) -1 .Similarly, count terms C k are stored as:A 2k-1:2k, * =   0 -C k (1) 2 -C k (2) 3 • • • -C k (n) n ′ 0 + C k (1) 2 + C k (2) 3 • • • + C k (n) n ′   .The division of C(i) by (i + 1) is a consequence of the fact that attention computes an average rather than a sum. Dealing with these divisions is a common feature of many transformer constructions. In contrast to other constructions that undo the divisions using nonstandard embeddings (Pérez et al., 2021; Barcel ó et al., 2024) or nonstandard versions of LayerNorm (Merrill and Sabharwal, 2024) , our construction uses no position embeddings and only standard LayerNorm. A minor consequence of our handling of comparison (Appendix B.3) is that while Boolean values are preserved throughout the computation, integer values can get overwritten.The reason for representing every value as two transformer activation values is to account for LayerNorm. It ensures that all feature vectors have zero mean, so LayerNorm only applies a position-wise scaling factor. When necessary, we describe how to use LayerNorm to remove this scaling factor in Appendix B.3.Observe that for subformulas, our convention states the BOS position is always false. Consequently, for count terms, the BOS position is always 0. We can ensure this with a feedforward layer.Lemma 5.3. Using the word embedding and a single feed-forward layer, we can set the BOS position to False, without disturbing the Boolean value at any other position.Proof. See Appendix B.1.Count terms in K t [#] can be simulated by uniform self-attention layers. Lemma 5.4. Let A 2k-1:2k , * store a Boolean vector as defined above. For any i, let C k,i be the number of positions j ≤ i such that A 2k-1:2k,j is True. Then there is a transformer block that computes, at each position i, and in two other dimensions 2k ′ -1, 2k ′ , the values -C k,i i+1 and C k,i i+1 .Proof. See Appendix B.2 for proof and pictures.All other K t [#] formulas and terms can be simulated by feed-forward layers.Lemma 5.5. The following position-wise operations can be simulated by a single transformer block, using existing dimensions as input and a fresh dimension as output: addition (+), subtraction (-), comparison (≤), and Boolean operations (∧, ¬).Proof. See Appendix B.3.Definition 5.6. Fix an alphabet Σ, and assume that the symbol BOS is not in Σ. We say a masked soft attention transformer T (as a composition of blocksT = B b • . . . • B 1 • WE) with d dimensions simulates a K t [#] formula ϕ if for every input w ∈ Σ * with length n and every subformula ψ k of ϕ, there is some dimension d k such that [T(BOS • w)] 2d k -1:2d k ,i+1 =              -1 +1 if w, i ⊨ ψ k +1 -1 otherwise.Theorem 5.7. For every K t [#] formula ϕ, there exists a soft attention transformer which simulates ϕ. Moreover, the transformer will have at most md(ϕ) blocks.Proof. We induct on the modal depth of ϕ. If ϕ is of modal depth 0, it must be a Boolean combination of Q σ formulas. This can be simulated in the word embedding.For the inductive step, let ϕ be a K t [#] formula of modal depth m + 1. By Section 4.3, ϕ is a Boolean combination of:-Subformulas of modal depth at most m.-Subformulas of the form This can be achieved by adding one block. The first step can be achieved with a selfattention layer. We've described how to compute each of the next three steps individually using a feed-forward layer, but their composition can also be performed with a single feedforward layer.∑ k∈K a k #[ψ k ] ≥ 0,6 Relationship to other formalisms Proof. Suppose that such a sentence σ exists. Chiang et al. (2023) show that there exists an M such that σ cannot distinguish between two strings that differ only by swapping symbols exactly M positions apart. Since ( M ) M ∈ Dyck-1 and )( M-1 () M-1 ̸ ∈ Dyck-1 but σ cannot distinguish them, we have a contradiction.On the other hand, it does not seem that K t [#] can express Dyck-2, so a treatment of this language would be an informative target for future work. We note that Yao et al. (2021) shows transformers can recognize Dyck-2, but using hard attention. (2024) show is a lower bound on average-hard attention transformer expressivity. However, average-hard attention transformers are not known to be either a subset or superset of standard, soft-attention transformers. More comments on hard and soft attention can be found in Section 2.1. Understanding the precise connection between AHATs and soft attention transformers is left for future exploration, and is expected to require modifications to the standard architecture in order to derive an exact inclusion.As a final note, there appears to be a sizeable gap between the lower bound of K t [#] and the upper bound of FOM[BIT] shown in Merrill and Sabharwal (2023) . In particular, the latter can express integer multiplication, but we suspect K t [#] cannot. Incidentally, transformer models are observed to have difficulty with integer multiplication (Dziri et al., 2024) , so harmonizing these theoretical and empirical results would be helpful to paint a clearer picture of transformer expressivity. 
from fixed-precision transformers to k t [#]: 
 In practice, transformers use fixed-precision numbers. We adapt the proof that FOC[+] can simulate fixed-precision soft attention transformers (Chiang et al., 2023) 3. Consider last position as a uniform probability distribution: dimensions with N a (|w|) = 1 will have the same maximum probability score, and all those with N a (|w|) = 0 will have the minimum probability. 4. Run the transformer on w, and then select an a such that the N a dimension holds the maximum probability, with arbitrary tie-breaking. Append a to w, and repeat until EOS is selected.We say a C-RASP language model assigns nonzero probability p to word w = w 0 • • • w n-1 iff w, i ⊨ N w i+1 for all 0 ≤ i < n -1, and w, n -1 ⊨ N EOS . We say a C-RASP Language Model recognizes language L whenever it assigns nonzero probability to w iff w ∈ L.In logical terms, we can construct a C-RASP language model to recognize L iff there exists a formula ϕ of K t [#] which recognizes L and for all a ∈ Σ we can define formulas N a such that w ⊨ N a ⇐⇒ ∃w ′ .waw ′ ⊨ ϕ. In this case, N EOS = ϕ Example 8.2. Append to the end of Dyck program in Example 3.2 the following operations:N ( (i) := ¬Q EOS (i) N ) (i) := ¬Q EOS (i) ∧ C ) (i) < C ( (i) N EOS (i) := D(i)Corollary 8.3. For every piecewise testable language L, there exists a C-RASP Language Model which recognizes L.Proof. This is an immediate consequence of Lemma 4.2. For any piecewise testable language L we can define a formula ϕ of K t [#] which recognizes L. Next, observe that it is always the case that ∃w ′ .waw ′ ⊨ ϕ. Finally, define N EOS = ϕ and N a = ⊤ for all a ∈ Σ. 
concluding remarks: 
 We have introduced the temporal counting logic K t [#] alongside the RASP variant C-RASP and proved that they are the best-known lower bound on the expressivity of future-masked soft attention transformers, with unbounded input size. Unlike previous results, we have made minimal extra assumptions about transformers, so all formulas in K t [#] can compile directly into standard transformers. As such, an implementation of C-RASP should prove appropriate for constructing transformers to run experiments on, and further theoretical analysis of K t [#] and its extensions should shed light on the expressive power of transformers.A.1 Extensions Lemma A.1. Consider an extension of C-RASP in which the counting operation has the formC(i) := # 2 [j ≤ i] F(i, j)which allows F to be a Boolean combination of C-RASP operations P(i) and P(j) evaluated at both i and j. Any program with this extended operation is actually equivalent to a C-RASP program with only the normal counting operation.Proof. Let F be a Boolean combination of P 1 , . . . , P k evaluated at either i or j. First, observe thatC(i) = C 1 (i) + C 2 (i) -C 3 (i)whereC(i) := # 2 [j ≤ i] F 1 (i, j) ∨ F 2 (i, j) C 1 (i) := # 2 [j ≤ i] F 1 (i, j) C 2 (i) := # 2 [j ≤ i] F 2 (i, j) C 3 (i) := # 2 [j ≤ i] F 1 (i, j) ∧ F 2 (i, j)Now, write F in DNF and split using the above. Now every single counting operation is of the formC(i) := # 2 [j ≤ i]   x∈I P x (i) ∧ x∈J P x (j)  Where I and J store the indices of C-RASP operations which depend on i and j, respectively, within the counting operation. Observe then that this is equivalent toC(i) := # [j ≤ i]   x∈I∩J P x (j)  Thus, every # 2 operation can be factored out as a sequence of normal # operations.We sometimes put multiple C-RASP operations on the same line for brevity.a * b * over Σ = {a, b} C a (i) := # [j ≤ i] Q a (j) # positions with a's C b (i) := # [j ≤ i] Q b (j) # positions with b's V(i) := Q a (i) ∧ C b (i) ≥ 1Violation: an a has b's preceding itC V (i) := # [j ≤ i] V(j) # Violations Y(i) := C V (i) = 0 Zero Violations a * b * a * over Σ = {a, b} C a (i) := # [j ≤ i] Q a (j) # positions with a's C b (i) := # [j ≤ i] Q b (j) # positions with b's BA(i) := Q a (i) ∧ C b (i) ≥ 1 A subsequence ba ends at i C ba (i) := # [j ≤ i] BA(j) # ends of subsequence ba BAB(i) := Q b (i) ∧ C ba ≥ 1 the subsequence bab ends at i C bab (i) := # [j ≤ i] BAB(j) # ends of subsequence bab Y(i) := C bab (i) = 0There are no subsequences baba n b n c n over Σ = {a, b, c} C a (i) := # [j ≤ i] Q a (j) # positions with a's C b (i) := # [j ≤ i] Q b (j) # positions with b's C c (i) := # [j ≤ i] Q c (j) # positions with c's A(i) := C b (i) + C c (i) = 0 No preceding b's or c's B(i) := C c (i) = 0 No preceding c's C A (i) := # [j ≤ i] Q a (j) ∧ A(j) # a's with no preceding b's or c's C B (i) := # [j ≤ i] Q b (j) ∧ B(j) # b's with no preceding c's G a (i) := C A (i) = C a (i) no a's have preceding b's or c's G b (i) := C B (i) = C b (i) no b's have preceding c's G abc (i) := C a (i) = C b (i) = C c (i) same number of a's, b's, c's Y(i) := G a (i) ∧ G b (i) ∧ G abc (i)Correct order and number of symbolshello over Σ = {e, h, l, o} C e (i) := # [j ≤ i] Q e (j) # positions with e's C h (i) := # [j ≤ i] Q h (j) # positions with h's C l (i) := # [j ≤ i] Q l (j) # positions with l's C o (i) := # [j ≤ i] Q o (j) # positions with o's C Σ (i) := # [j ≤ i] 1 # symbols in string HE(i) := Q e (i) ∧ C h (i) = 1 A subsequence he ends at i C he (i) := # [j ≤ i] HE(j) # ends of subsequence he HEL(i) := Q l (i) ∧ C he (i) = 1 A subsequence hel ends at i C hel (i) := # [j ≤ i] HEL(j) # ends of subsequence hel HELLO(i) := Q o (i) ∧ C hel (i) = 2 A subsequence hello ends at i Y(i) := HELLO(i) ∧ C Σ (i) = 5Length 5 and contains subsequence helloAs a potential point of clarification for the HELLO(i) line, observe that if a string contains two positions that are the end of a subsequence hel, then that string must contain the subsequence hell. In the other direction, we induct on the length of C-RASP program P = P 1 , . . . , P n . Assume that Boolean operations P k (i) are simulated by formulas Pk , and count operations C k (i) = # [j ≤ i] V(j) are simulated by terms Ĉk . This is straightforward, but there are many cases.The main idea is that whenever we have a conditional or min/max operation, we divide the formula into two cases depending on what the result of the operation should be.-If P k+1 is a count-valued vector, it is not used for string acceptance as defined in 3.1. Thus the formula for this is the formula for the last Boolean-valued vector, by the IH.-If P k+1 (i) = Q a (i), let Pk+1 = Q a . -If P k+1 (i) = ¬P ℓ (i) let Pk+1 = ¬ Pℓ . -If P k+1 (i) = P ℓ (i) ∧ P m (i) let Pk+1 = Pℓ ∧ Pm . -If P k+1 (i) = C ℓ (i) ≤ C m (i) we need to divide on cases to handle if C ℓ (i) is a condi- tional or min/max, as K t [#]does not have these terms built in. This is straightforward, but there are many cases.- If C ℓ (i) = # [j ≤ i] P 1 (i), let Ĉℓ = # P1 . Then: -If C m (i) = # [j ≤ i] P 2 (i), let Pk+1 = Ĉℓ ≤ # P2 . -If C m (i) = P 2 (i) ? C 3 (i) : C 4 (i), let Pk+1 = ( P2 ∧ Ĉℓ ≤ Ĉ3 ) ∨ (¬ P ∧ Ĉℓ ≤ Ĉ4 ). -If C m (i) = min(C 3 (i), C 4 (i)), let Pk+1 = ( Ĉ3 ≤ Ĉ4 ∧ Ĉℓ ≤ Ĉ3 ) ∨ ( Ĉ4 ≤ Ĉ3 ∧ Ĉℓ ≤ Ĉ4 ). -If C m (i) = max(C 3 (i), C 4 (i)), let Pk+1 = ( Ĉ3 ≥ Ĉ4 ∧ Ĉℓ ≤ Ĉ3 ) ∨ ( Ĉ4 ≥ Ĉ3 ∧ Ĉℓ ≤ Ĉ4 ). -If C m (i) = c, for c ∈ N let Pk+1 = Ĉℓ ≤ c. -If C ℓ (i) = P 1 (i) ? C 1 (i) : C 2 (i), then: -If C m (i) = # [j ≤ i] P 2 (i), let Pk+1 = ( P1 ∧ Ĉ1 ≤ # P2 ) ∨ (¬ P1 ∧ Ĉ2 ≤ # P2 ). -If C m (i) = P(i) ? C 3 (i) : C 4 (i), let Pk+1 = ( P1 ∧ P2 ∧ Ĉ1 ≤ Ĉ3 ) ∨ ( P1 ∧ ¬ P2 ∧ Ĉ1 ≤ Ĉ4 ) ∨ (¬ P1 ∧ P2 ∧ Ĉ2 ≤ Ĉ3 ) ∨ (¬ P1 ∧ ¬ P2 ∧ Ĉ2 ≤ Ĉ4 ). -If C m (i) = min(C 3 (i), C 4 (i)), let Pk+1 = ( P1 ∧ Ĉ3 ≤ Ĉ4 ∧ Ĉ1 ≤ Ĉ3 ) ∨ ( P1 ∧ Ĉ3 ≥ Ĉ4 ∧ Ĉ1 ≤ Ĉ4 ) ∨ (¬ P1 ∧ Ĉ3 ≤ Ĉ4 ∧ Ĉ2 ≤ Ĉ3 ) ∨ (¬ P1 ∧ Ĉ3 ≥ Ĉ4 ∧ Ĉ2 ≤ Ĉ4 ). -If C m (i) = max(C 3 (i), C 4 (i)), let Pk+1 = ( P1 ∧ Ĉ3 ≥ Ĉ4 ∧ Ĉ1 ≤ Ĉ3 ) ∨ ( P1 ∧ Ĉ3 ≤ Ĉ4 ∧ Ĉ1 ≤ Ĉ4 ) ∨ (¬ P1 ∧ Ĉ3 ≥ Ĉ4 ∧ Ĉ2 ≤ Ĉ3 ) ∨ (¬ P1 ∧ Ĉ3 ≤ Ĉ4 ∧ Ĉ2 ≤ Ĉ4 ). -If C m (i) = c, for c ∈ N let Pk+1 = ( P1 ∧ Ĉ1 ≤ c) ∨ (¬ P1 ∧ Ĉ2 ≤ c). -If C ℓ (i) = min(C 1 (i), C 2 (i)), then: -If C m (i) = # [j ≤ i] P 2 (i), let Pk+1 = ( Ĉ1 ≤ Ĉ2 ∧ Ĉ1 ≤ # P2 ) ∨ ( Ĉ1 ≥ Ĉ2 ∧ Ĉ2 ≤ # P2 ). -If C m (i) = P(i) ? C 3 (i) : C 4 (i), let Pk+1 = ( Ĉ1 ≤ Ĉ2 ∧ P2 ∧ Ĉ1 ≤ Ĉ3 ) ∨ ( Ĉ1 ≤ Ĉ2 ∧ ¬ P2 ∧ Ĉ1 ≤ Ĉ4 ) ∨ ( Ĉ1 ≥ Ĉ2 ∧ P2 ∧ Ĉ2 ≤ Ĉ3 ) ∨ ( Ĉ1 ≥ Ĉ2 ∧ ¬ P2 ∧ Ĉ2 ≤ Ĉ4 ). -If C m (i) = min(C 3 (i), C 4 (i)), let Pk+1 = ( Ĉ1 ≤ Ĉ2 ∧ Ĉ3 ≤ Ĉ4 ∧ Ĉ1 ≤ Ĉ3 ) ∨ ( Ĉ1 ≤ Ĉ2 ∧ Ĉ3 ≥ Ĉ4 ∧ Ĉ1 ≤ Ĉ4 ) ∨ ( Ĉ1 ≥ Ĉ2 ∧ Ĉ3 ≤ Ĉ4 ∧ Ĉ2 ≤ Ĉ3 ) ∨ ( Ĉ1 ≥ Ĉ2 ∧ Ĉ3 ≥ Ĉ4 ∧ Ĉ2 ≤ Ĉ4 ). -If C m (i) = max(C 3 (i), C 4 (i)), let Pk+1 = ( Ĉ1 ≤ Ĉ2 ∧ Ĉ3 ≥ Ĉ4 ∧ Ĉ1 ≤ Ĉ3 ) ∨ ( Ĉ1 ≤ Ĉ2 ∧ Ĉ3 ≤ Ĉ4 ∧ Ĉ1 ≤ Ĉ4 ) ∨ ( Ĉ1 ≥ Ĉ2 ∧ Ĉ3 ≥ Ĉ4 ∧ Ĉ2 ≤ Ĉ3 ) ∨ ( Ĉ1 ≥ Ĉ2 ∧ Ĉ3 ≤ Ĉ4 ∧ Ĉ2 ≤ Ĉ4 ). -If C m (i) = c, for c ∈ N let Pk+1 = ( Ĉ1 ≤ Ĉ2 ∧ Ĉ1 ≤ c) ∨ ( Ĉ1 ≥ Ĉ2 ∧ Ĉ2 ≤ c). -If C ℓ (i) = max(C 1 (i), C 2 (i)), this identical to the previous case but just switch Ĉ1 ≤ Ĉ2 with Ĉ1 ≥ Ĉ2 . -If C ℓ (i) = c for c ∈ N,∃x 1 . . . ∃x n . i ∃ =x i p.ψ i (p) ∧ χ(x 1 , . . . , x n )where all ψ i and χ are quantifier-free, and χ is a set of linear constraints on x 1 . . . x n .With respect to end-satisfiablity, this is simply equivalent to the K t [#] formula.χ (#[ψ 1 ] , . . . , #[ψ n ])The same is true for FOC[+; MOD], if we extend K t [#] with modular predicates to K t [#;MOD] where (w, i) ⊨ MOD k m ⇐⇒ i ≡ k mod m. In general, from this normal form we can see that for any set P of unary predicates, the extension FOC[+;P] is contained in K t [#;P], when defined appropriately. Furthermore, all of these will be K t [#] formulas of modal depth 1.In all proofs, we omit the scaling factor applied by LayerNorm, because it can be confusing and also does not affect the end result. However, whenever relevant, we mention how to account for this scaling factor.Here, we recall the definition of LayerNormDefinition B.1. LayerNorm is a function f : R d → R d such that f (x) = x -µ σ where µ = 1 d d ∑ i=1 x i σ = 1 d d ∑ i=1 (x i -µ) 2Observe that if µ = 0, LayerNorm only applies a scaling factor to all values in a position.Observe furthermore if the absolute value of all values in a position are equal, LayerNorm scales all of them to be ±1, which is important in Appendix B.3.An essential part of our construction is access to a Boolean vector that is True at the BOS position and False everywhere else. We call this a Start-Separating Vector, adapting terminology from Merrill and Sabharwal (2024) . Using the word embedding for BOS, we can construct a dimension that holds such a vector (ensuring WE(w i ) is true at dimensions 2k s -1, 2k s only when w i = BOS).1 2 n ′               . . . . . . . . . 2k s -1 -1 +1 • • • +1 2k s +1 -1 • • • -1 . . . . . . . . .Lemma 5.3. Using the word embedding and a single feed-forward layer, we can set the BOS position to False, without disturbing the Boolean value at any other position.Proof. Construct a feed-forward layer which computes the min of every value in an odd dimension with the value in dimension 2k s -1 of the Start-Separating Vector and the max of every value in an even dimension with the value in 2k s , as described in Lemma 5.5. Since we've maintained that all values are ±1 in our Boolean representation, this sets the BOS position to be False, while the others are unmodified.Lemma 5.4. Let A 2k-1:2k , * store a Boolean vector as defined above. For any i, let C k,i be the number of positions j ≤ i such that A 2k-1:2k,j is True. Then there is a transformer block that computes, at each position i, and in two other dimensions 2k ′ -1, 2k ′ , the values -C k,i i+1andC k,i i+1 .Proof. First, recall the definition of a masked self attention layer SA : R d×n → R d×n :SA(A) = [c o • • • c n ] where W (Q) : R d → R d k W (K) : R d → R d k W (V) : R d → R d s ij = W (Q) A * ,i • W (K) A * ,j √ d c i = ∑ i j=0 exp(s ij )W (V) A * ,j ∑ i j=0 exp(s ij ) To simulate a count term #[ϕ] = C(i) of K t [#],we need to construct a transformer block such that if the Boolean values ϕ(i) are stored in some dimension 2k -1, k, we can computeC(i) i+1 in some other dimensions 2k ′ -1, k ′ .To achieve this, we only need uniform attention -that is, at each position i, we set W (Q) = W (K) = 0, which makes s ij = 0 for all i, j. This spreads attention weight evenly across all positions j ≤ i.Furthermore, by setting W (V) as follows, we can add the value from position i in dimensions 2k -1, 2k to position i in dimensions 2k ′ -1, 2k ′ .W (V) = 2k -1 2k 2k ′ -1 2k ′                         . . . . . . . . . . . . 2k -1 • • • 0 0 • • • 0 0 • • • 2k • • • 0 0 • • • 0 0 • • • . . . . . . . . . . . . 2k ′ -1 • • • 1 1 • • • 0 0 • • • 2k ′ • • • 1 1 • • • 0 0 • • • . . . . . . . . . . . .As such, we get the attention layer to compute the average of all unmasked positions j ≤ i.Recalling the definition once more, the general expression reads:c i,k = ∑ i j=0 exp(s ij )[W (V) A * ,j ] k ∑ i j=0 exp(s ij )Then, with the use of uniform attention and our carefully constructed W (V) , we compute in position i of dimension k, the value c i,k , which is the average of all values up to position i in dimension k, The expression reduces to:c i,k = ∑ i j=0 exp(s ij )[W (V) A * ,j ] k ∑ i j=0 exp(s ij ) = ∑ i j=0 [W (V) A * ,j ] k ∑ i j=0 1 = ∑ i j=0 A k,j ∑ i j=0 1 = ∑ i j=0 A k,j i + 1Before moving on, note that we represent Booleans as -1, +1 instead of 0, 1, and we'll also write the sum of positions j ≤ i that hold a True as C i,k . Here we write out the resulting tensor after the described self-attention layer showing the relevant dimensions at positions 0, 1, . . . , n ′ . We write B i ∈ {0, 1} be the Boolean value at position i.1 2 n ′                                   . . . . . . . . . 2k -1 +1 -2B 1 + 1 • • • -2B n + 1 2k -1 +2B 1 -1 • • • +2B n -1 . . . . . . . . . 2k ′ -1 0 -2 C 1,d ′ 2 + 1 • • • -2 C n,d ′ n+1 + 1 2k ′ 0 +2 C 1,d ′ 2 -1 • • • +2 C n,d ′ n+1 -1 . . . . . . . . .Note, however, that instead of the desired valueC i,ki+1 , we have actually computed 2C i,ki+1 -1. We use a feed-forward layer to undo this transformation by subtracting (or adding) 1 and then dividing by 2 in dimension d (or d + 1). Then, it is straightforward to construct a feed-forward layer that simply adds dimension 2k 0 -1 to 2k -1 and 2k 0 to 2k in order to remove the ±, and then divides by 2 to get the result:1 2 n ′                 . . . . . . . . . 2k ′ -1 0 - C 1,d ′ 2 • • • - C n,d ′ n+1 2k ′ 0 + C 1,d ′ 2 • • • + C n,d ′ n+1 . . . . . . . . .As a final note, which is relevant for the later subsection on arithmetic comparison, we will make every self-attention layer compute a counting operation over the start-separating vector (Appendix B.1) in order to compute the value 1 i+1 at every position i in some dimension.Lemma 5.5. The following position-wise operations can be simulated by a single transformer block, using existing dimensions as input and a fresh dimension as output: addition (+), subtraction (-), comparison (≤), and Boolean operations (∧, ¬). Arbitrary Boolean expressions in DNF can be simulated using two blocks.Proof. A two-layer feed-forward network with ReLU activations on the first layer and none on the second layer can compute any continuous piecewise linear function with a finite number of pieces, or CPWL (Arora et al., 2018) . All of these operations are CPWL, but we give explicit constructions for concreteness, and the case of comparisons requires special care.We consider each type of operation in turn. All constructions only use the feed-forward layer. We can force the self-attention layer to perform no changes to the residual stream by setting all weights to 0; the residual connection then adds the original values back in.Addition and subtraction: These operations are straightforward: put 1's in W 1 such that we add the appropriate values to the fresh dimension, and negate using W 2 if needed.Min/Max: Recall that ReLU(x) = max(0, x). Then min(x, y) = x -ReLU(xy).-If x < y, then ReLU(xy) = 0, so x -ReLU(xy) = x = min(x, y).-If x ≥ y, then ReLU(xy) = xy, so x -ReLU(xy) = x -(xy) = y = min(x, y).Similarly, max(x, y) = x + ReLU(yx).Therefore there exist FFNs to compute the min or max of two real numbers:x y 1 -1 1 -1 min(x, y) 1 -1 -1 x y 1 -1 -1 1 max(x, y) 1 -1 1To compute the min of two count terms, we compute the min of their positive components and the max of their negative components. Similarly for the max of two count terms.Comparison: This requires access to ± 1 i+1 in some dimensions 2k 0 -1, 2k 0 . This is easily achieved by requiring every self-attention layer to perform a counting operation over the start-separating vector (Appendix B.1).First we explain how to simulate a comparison of two count terms C 1 (i) ≤ C 2 (i). Then, we describe how to extend this to compare linear combinations of count terms.Suppose that we want to compare C 1 and C 2 in dimensions 2k 1 -1, 2k 1 and 2k 2 -1, 2k 2 , and put the result in dimension 2k 3 -1, 2k 3 . Initially, the residual stream looks like this:i                                                                   . . . 2k 0 -1 • • • -1 i+1 • • • 2k 0 • • • + 1 i+1 • • • . . . 2k 1 -1 • • • -C 1 (i) i+1 • • • 2k 1 • • • + C 1 (i) i+1 • • • . . . 2k 2 -1 • • • -C 2 (i) i+1 • • • 2k 2 • • • + C 2 (i) i+1 • • • . . . 2k 3 -1 • • • 0 • • • 2k 3 • • • 0 • • • . . .We construct a feed-forward layer that computes the function:gtz(X(i)) = min 0.5 i + 1 , X(i) i + 1 - 0.5 i + 1 -min 0, X(i) i + 1 .-1 0 1 2-0.5 i+1 0 0.5 i+1 X(i) gtz(X(i)) Observe that gtz(C 2 (i) -C 1 (i) + 0.5) equals 0.5 i+1 if C 1 (i) ≤ C 2 (i), and -0.5 i+1 otherwise. This is because the counts C 1 (i), C 2 (i) must be integers, so if C 1 (i) ≤ C 2 (i), then C 2 (i) -C 1 (i) + 0.5 ≥ 0.5, and the expression will evaluate to 0.5 i+1 . Otherwise, C 2 (i) -C 1 (i) + 0.5 < -0.5, and the expression will evaluate to -0.5 i+1 . It is straightforward, then, to use the construction for min/max from above to produce a feed-forward layer that computes gtz (C 2 (i) -C 1 (i)). Essentially, we use W 1 to compute the values (using the pre-existing values from the residual stream)0.5 i + 1 , C 2 (i) -C 1 (i) + 0.5 i + 1 , - C 2 (i) -C 1 (i) + 0.5 i + 1 Then we use W 2 to compute 0.5 i + 1 + ReLU 0.5 i + 1 - C 2 (i) -C 1 (i) + 0.5 i + 1 -ReLU 0.5 i + 1 - C 2 (i) -C 1 (i) -0.5 i + 1 which equals gtz(C 2 (i) -C 1 (i)) as desired.Similarly, it is straightforward to construct a feed-forward layer to compare linear combinations of count terms. That is, for disjoint sets of indices K 1 and K 2 , to computegtz ∑ k∈K 2 c k • C k (i) -∑ k∈K 1 c k • C k (i) .So we can construct a feed-forward layer f : R d → R d that computes in each dimension i the followingf                           v 1 v 2 . . . 0 0 . . . v d-1 v d                           =              gtz(v 1 ) gtz(v 2 ) . . . gtz ∑ k∈K 2 c k • C k (i) -∑ k∈K 1 c k • C k (i) gtz ∑ k∈K 2 c k • C k (i) -∑ k∈K 1 c k • C k (i) . . . gtz(v d-1 ) gtz(v d )              .This truncates all positive values in the residual stream at this point to be 0.5 i+1 at position i, and all nonpositive values to be -0.5 i+1 . As a result, the next application of LayerNorm (with appropriate parameter settings) scales every single value to ±1. In particular, all previously-computed Boolean values are preserved, and the newly-computed dimensions 2k 3 -1, 2k hold the correct Boolean value based on the desired comparison As a side effect, all previously-computed counts also get changed to ±1, but we do not need these counts any longer due to how we organized the construction in Theorem 5.7.Boolean operations: The Boolean operations ∧ and ¬ can be computed by FFNNs with ReLU activations. Conjunction (∧) is equivalent to min/max:     . . . -2B 1 + 1 2B 1 -1 . . .      ∧      . . . -2B 2 + 1 2B 2 -1 . . .      =       . . . max(-2B 1 + 1, -2B 2 + 1) min( 2B 1 -1, 2B 2 -1) . . .       .Logical negation (¬) is equivalent to arithmetic negation, or swapping the positive and negative components:2B -1 -2B + 1 1 1 1 -1 -1 1For an arbitrary Boolean formula, convert it to canonical disjunctive normal form, which is a disjunction ϕ 1 ∨ • • • ∨ ϕ n of clauses, at most one of which can be true for any value of the inputs. Each clause is of the form ϕ m = k∈K m B k , where each B k is an input or a negated input and K m is a set of indices for each clause. A slightly different construction can be used to compute ∧ over inputs in K m . Observe that:k∈K m B k = ReLU ∑ k∈K m B k -(|K m | -1)And this can be computed for each clause using the first layer and ReLU of a feed-forward layer. Recall again that if a constant is fixed, we can retrieve it by multiplying the constant ±1 from dimensions 2k 0 -1, 2k 0 as described in Appendix B.2. Then, because at most one clause can be true, the sum of all clauses will either be 1 or 0. Then, we convert back to the ±1 representation of truth values.n m=1 k∈K m B k = 2 • n ∑ m=1 ReLU ∑ k∈K m B k -(|K m | -1) -1.This can all be done in a single feed-forward layer.Lemma B.2. Here we detail the claim in Theorem 5.7 that we can compose many transformers, into a larger transformer which simulates all the formulas the smaller transformers do, in parallel.Two transformers T 1 and T 2 simulating formulas ψ 1 and ψ 2 (using the construction described in Theorem 5.7) can be composed into a single transformer T 3 that simulates both ψ 1 and ψ 2 .Proof. We will just sketch out the construction. Let T 1 with b 1 blocks in d 1 dimensions and word embedding Emb 1 simulate ϕ 1 and T 2 with b 2 blocks in d 2 dimensions and word embedding Emb 2 simulate ϕ 2 in the manner described in Theorem 5.7. We can construct T 1 ⊕ T 2 with max(b 1 , b 2 ) blocks in d 1 + d 2 dimensions which simulates both ϕ 1 and ϕ 2 , such that(T 1 ⊕ T 2 )(w) = T 1 (w) T 2 (w) .First, add layers that compute the identity function to the shallower transformer so that both have depth max(k 1 , k 2 ).Next, concatenate their word embedding vectors(Emb 1 ⊕ Emb 2 )(a) = Emb 1 (a)Emb 2 (a) .Then, at each level, we can compose the feed-forward networks FF 1 and FF 2 in parallel by creating a new FF withW (1) = W (1) 1 0 0 W (1) 2 b (1) = b (1) 1 b (1) 2 W (2) = W (2) 1 0 0 W (2) 2 b (2) = b (2) 1 b (2) 2 .Furthermore, we can compose the self-attentions in exactly the same manner, as only uniform attention is used in the construction.EQUATIONIt is straightforward to verify the correctness of this construction, given we follow the procedure in Theorem 5.7 organizing the simulation by modal depth.Definition C.1. A fixed-precision number with r integer bits and s fractional bits is a number in F r,s = {i/2 s | -2 r+s ≤ i < 2 r+s }. For any value a ∈ F r,s , we write ⟨a⟩ b for the b-th bit of the two's complement representation of a. That is,⟨a⟩ b = ⌊a • 2 -b ⌋ -⌊a • 2 -b-1 ⌋ • 2.This is a two's complement representation.It helps to access each individual bit of x.Proposition C.2. We write x b for the b-th bit of x, whenever x is a fixed-precision number. Then, observe that we can write a formula F m (x) ⇐⇒ x = F m iff we can write formulas F b (x) ⇐⇒ x b = 1.Proof. This should be clear by an example: 1001 in F 5,0 . We write F m (x) ⇐⇒ F 0 (x) ∧ ¬F 1 (x) ∧ ¬F 2 (x) ∧ F 3 (x). Proposition C.4. Assume we have Boolean functions F k m (i) which return true iff the value at position i in dimension k is F m ∈ F r,s Then any function of the form f 1 (x 1 , . . . , x d ) = f 2 (x 1 , . . . , x d ), where the x k is the value at dimension k in position i, can be written as a Boolean combination of F k m (i). Proof. Essentially, this is F n × F n → {0, 1}, which only takes on finitely many values. Thus it is tedious, but straightforward, to enumerate all tuples of x which should return true, and write a formula that returns the correct answer. Let K = {(m 1 , . . . , m d ) | f 1 (F m 1 , . . . , F m d ) = f 2 (F m 1 , . . . , F k=m d )}That is, K stores all n-tuples K of indices such that given an n-tuple of fixed-precision numbers which each have the corresponding index in K, the equality holds. Then writeK∈K k≤d F k K k (i)This formula will return 1 iff x k in dimensions k at position i have the correct fixed-precision values in order to satisfy the equality.As a result, for any function f : F d r,s → F d r,s we can write formulas ϕ(i) to check which fixed-precision value the output of the function is at position i, given the formulas that check the values of the inputs at position i. This means Lemma C.5. We can write formulas FFN k m (i), for each feed-forward layer FFN to check whether the output at position i in dimension k is F m ∈ F r,s . Same for LayerNorm LN k m (i). Proof. This is a direct consequence of Proposition C.4 because these functions all take a finite number of fixed-precision inputs, and have a finite number of outputs.The same is not the case for self-attention layers, as we have no bound on the input length. However, count terms help us out here. Lemma C.6. Assume we are using F r,s as our fixed-precision representation. Assume we have access to predicates F b (i) which tell us if the value at position i has a 1 in the b-th bit of its fixedprecision representation. Then we can compute the following summation as a counting term2 s • ∑ j≤i X jwhere X j is a value at position j.Proof. Observe this summation is equivalent to ∑ j≤i X j = 2 0 • ∑ j≤i F 0 (j) + 2 1 • ∑ j≤i F 1 (j) . . . + 2 r+s-1 • ∑ j≤i F r+s-1 (j) -2 r+s • ∑ j≤i F r+s (j) = #[F 0 ] + 2#[F 1 ] + . . . + 2 r+s-1 # F r+s-1 -2 r+s # F r+s . As a clarifying note, recall we are using two's complement, which is why the most significant bit is subtracted.Lemma C.7. We can write formulas C k m (i) which are true iff the output of a self-attention layer at dimension k in position i is F m ∈ F r,s Proof. Recall the definition of a self-attention layer in a fixed-precision masked soft attention transformer, SA : F d×n r,s → F d×n r,s :SA(A) = [c o • • • c n ]whereW (Q) : F d r,s → F d k r,s W (K) : F d r,s → F d k r,s W (V) : F d r,s → F d r,s s ij = W (Q) A * ,i • W (K) A * ,j √ d c i = ∑ i j=0 exp(s ij )W (V) A * ,j ∑ i j=0 exp(s ij )Similarly, we define β k m (i), which checks the word embedding for BOS has value F m at dimension k. Sinusoidal positional encodings can be described in the same manner, using modular predicates.Proof. As a direct consequence of the above lemmas, we can write a formula of K t [#], which simulates a fixed-precision masked soft attention transformer without positional encodings. Adding modular predicates allows K t [#; MOD] to simulate fixed-precision masked soft attention transformer with sinusoidal positional encodings. This formula will have modal depth O(L) in the number of layers L of the transformer, and width roughly O((2 F ) d ) in the precision F and width d of the transformer.We pronounce K t [#] as "K-t-sharp". The logic K t is E.J. Lemmon's minimal tense logic(Rescher and Urquhart,2012), where K is the minimal modal logic, and the t refers to "tense", indicating that our structures are linear, like timelines or strings. Additionally, # is the modal counting operator, which is fairly standard notation in counting logics. 
 
 Appendix:  


Decision: The paper studies the problem of characterizing the classes of computational problems that can be solved by autoregressive transformers. This is done purely from the expressive power perspective. This is an important theoretical problem with considerable recent interest. The paper under review provides a new class of problems that can be expressed in a temporal counting logic. They also provide another equivalent formalism C-RASP. Their formalism is natural and clean and arguably provides the largest class of computational problems expressible by transformers so far. There are technical issues here that arise when comparing to prior work regarding soft and hard attention and other elements of transformers. The current paper appears to be closer to transformers as used in practice. 

Out of the four, three reviewers were positive about the paper. Among the questions, perhaps the most important was about how much bigger is the class of problems proposed in the present paper compared to the previously known classes. This remains an open question. Nevertheless, I think the contributions of the present paper are sufficient to warrant acceptance.

Reviews: review: paper_summary: paper_summary: The paper studies the representation power of Transformer and proves that constant layer Transformer could recognize all the formal languages defined by formulas of Kt[#]. This is proved by showing Transformer could recognize C-RASP, a variant of RASP (Restricted Access Sequence Processing Language), and then prove the equivalence of Kt[#] and C-RASP.
strength_weakness: strength_weakness: While the construction of Transformer to recognize language in Kt[#] gives some improvement on the previous expressiveness result, the improvement is not so clear since there is no good characterization of Kt[#], and this result is very hard to parse for people outside of programming language area. Moreover, the expressive result is restricting as it does not count the decoding step performed by Transformer (e.g. CoT) and this gap might be very large.


-----------------
Post rebuttal: I slightly raise my score.
questions: questions: .
paper_summary: paper_summary: This paper introduces two equivalent formalisms (a temporal logic Kt[#] and a RASP fragment called C-RASP) which aim to describe counting capabilities in transformers.
The authors show that they are the tightest known lower bound on the expressive power of transformers with causal masking (no positional embeddings).
Simultaneously, they show that such transformers, when using fixed-precision, can be compiled back into these formalisms.

Given the topic, I found the dimensions listed on https://colmweb.org/ReviewGuide.html very hard to apply. Nonetheless, I believe the paper to be a good fit to the "Science of LMs" Research Area of COLM. I'm evaluating the paper according to the four categories given in the review form:

CLARITY: I found the paper to be generally clearly written and presented. The paper nicely fits with a recent line of research on investigating the expressive power of transformers.

QUALITY: I followed the constructions and believe the formal results to be correct.

ORIGINALITY: My main concern here is the comparison to the recent result about  LTL(C, +) proven by [1], as described under “Questions”. Clarification from the authors could help here.

SIGNIFICANCE: Providing stronger formal lower bounds on the expressive capacity of transformers addresses foundational questions about modern LMs.
strength_weakness: strength_weakness: Weaknesses:
* Except for the finite precision setting (with sinusoidal embeddings), the results do not apply to transformers with positional embeddings.
* As described in the Summary and under Questions, I believe the paper does not currently do a sufficiently good job of explaining how the result substantially adds over the  LTL(C, +) result by [1]: this appears to be a similar recent result, in that it also shows that a temporal logic lower-bounds the power of a certain formalization of transformers. The paper under review could do a much stronger job making clear how the new results are substantially novel compared to the LTL(C, +) result beyond replacing positional encodings with positional masking and AHAT by soft attention, or why these changes require substantial innovations.
UPDATE: The authors have provided useful clarification, which I encourage them to include in the paper.
questions: questions: * I would like to know more about the link to LTL(C, +), proven by [1] to lower-bound AHAT. An obvious difference is that LTL(C, +) includes general unary predicates, establishing that it is strictly more powerful than Kt[#], but this difference just concerns whether or not positional encodings are used. The authors point out that the result from the paper under review applies to soft-attention transformers, different from and more realistic than AHAT. Nonetheless, I’m curious about what’s so different: can’t the construction from [1] be just adapted to softmax transformers?
* How is a finite-precision transformer defined? While the proof of Lemma C.7 asks the reader to recall the definition, I couldn’t find it anywhere. Naively: For any given head, its attention weights will be 1/N on average where N is the input length. When N is large and precision is finite, many of these will – if one naively applies finite precision – be rounded to 0. If one claims finite precision as a realistic theoretical assumption for transformers, then this seems like an undesirable result, as it effectively prevents finite-precision transformers from performing averaging. Lemma C.7 apparently gets around this by applying rounding after division. Is that the *definition* of finite-precision transformers?
* Page 7: “integer values get overwritten” – I didn’t follow this, the statement might be made clearer.
* first paragraph of Section 5.1 has LaTeX "??"


[1] Pablo Barcel ´o, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir Podolskii. Logical languages accepted by transformer encoders with hard attention. In Proc. ICLR, 2024.
paper_summary: paper_summary: This paper proposes to use Kt[#], a temporal counting logic, as a formalism for characterizing soft attention transformers. The paper also introduces C-RASP, a variant of RASP corresponding to Kt[#]. The paper proves that Kt[#] formulas can be compiled into transformers, fixed-precision transformers can be compiled into Kt[#], and it offers a tighter lower bound on expressiveness compared to the best prior result (that used a counting logic).
strength_weakness: strength_weakness: - It's not entirely clear to me how much these results reveal about soft attention transformers in particular, as apposed to averaging hard attention transformers (AHATs). It seems that the translation from Kt[#] to transformers (section 5.3/appendix B.2) exclusively uses uniform attention. (So Kt[#] is not necessarily so useful as a language for thinking about soft attention transformers---for example, constructing transformers with soft but non-uniform attention patterns.) It does seem notable that that softmax transformers can be decompiled into Kt[#] expressions (but this is also true of FO[+]). I think it would be helpful to include some discussion about why Kt[#] is specifically useful for softmax transformers and not just AHATs.
- The paper states that it derives a "much better lower-bound result," but I find it a little difficult to understand how much better it is. From what I understand, the main lower-bound result is that Kt[#] can define Dyck-1, but FO[+;MOD] cannot. It would be nice if there was a more general characterization of the lower-bound, or at least a more detailed discussion of how exactly this compares to expressivity results from prior work. 
- The paper might benefit from some more discussion of other formalisms in section 6, like first-order logic with majority quantifiers (Merrill and Sabharwal, 2023). In particular, Angluin et al. (2023) also introduce a RASP variant (Boolean RASP) for unique hard attention transformers, and prove that it recognizes exactly the star-free languages. I think it would be worthwhile to discuss the relationship between these results at greater length.

To summarize, my main concerns are related to how the contributions are framed relative to prior work. 
While I still think the paper is worth accepting, it would be stronger if it could offer a clearer discussion of how exactly these results differ from prior work.
questions: questions: - The introduction states that AHATs and UHATs "are not known to be either a subset or superset of standard, soft-attention transformers." What exactly does this mean? It seems to me that AHATs and UHATs clearly aren't supersets of soft-attention transformers. Is the point that some AHATs/UHATs might not be expressible using a standard transformer? Is there a reference for this point?
- Could you elaborate on why exactly FOC[+;MOD] is underpowered (section 2.2)? Is this saying that every sentence in FOC[+;MOD] can be expressed as a two layer transformer? I think it would be helpful to make this more clear.
- Regarding the translation from a transformer to a Kt[#] expression: Would it be possible to give any characterization of the size of the Kt[#] expression?
paper_summary: paper_summary: This paper extends the original RASP language to a variant called C-RASP to express temporal counting logic $\textbf{K}_t$[#] and compile them to future-masked soft attention transformers with unbounded input sizes. They show that any constant precision softmax decoder Transformer can be expressed via the C-RASP language. Further, they show how to use $\textbf{C-RASP}$ to construct language models that via greedy decoding generate sentences that have properties specified in $\textbf{K}_t$[#].
strength_weakness: strength_weakness: 1. The paper may require some rewriting to be understood by a broader audience. Currently, the reader may need a familiarity with representation theory and RASP language.
questions: questions: 1. The paper mentions that any constant precision softmax decoder Transformer can be expressed via the C-RASP language. In the proof that compiles the C-RASP language, the transformer constructed has uniform attention. Does this mean it is possible to compile a general Transformer to a larger uniform attention Transformer with more precision? If such is the case, how large would the larger Transformer be if one would translate a 4-bit GPT-2 Transformer with 124M parameters as an example?

Comments: title: Thank you for your response
Checking for additional concerns
Response to reviewer
Thank you for your reply
comment: I thank the authors for the rebuttal. I slightly raise my score. I am still not very excited by the improvement, but I will carefully read other reviews and ask for their opinions.
We thank the reviewer for the comments. As the discussion period is close to its end, we believe that we have addressed all of your questions, but please let us know if there are any remaining concerns.
Thanks very much for your feedback!
Thanks very much for your feedback and for reconsidering your score!
We thank the reviewer for the valuable comments. Since it is close to the end of author-reviewer discussion, please let us know if we have properly addressed your questions.
Thank you for the response! I will keep my score as is.
We appreciate you taking a second look. See our responses below:

1. Other examples of languages definable in Kₜ[#] but not FOC[+;MOD] include:

- $a^nb^nc^n$ (§3.2), a context-sensitive language  which is also observed to be learnable by [Bhattamishra, 2020].

- All piecewise testable languages, like $\Sigma^\*a\Sigma^\*b\Sigma^\*c\Sigma^\*$ (§3.3).

- All strings with the letter $a$ in the second position and nowhere else. 

- All valid email addresses (name@domain.com)

We make no claim of novelty in showing that Kₜ[#] and therefore transformers can recognize Dyck-1. The paper already cites [Bhattamishra et al, 2020] for showing that transformers recognize a language similar to Dyck-1, and we thank you for pointing out [Yao et al, 2021], which is a better reference.

Our focus here is not just on individual languages, but on the formalisms Kₜ[#] and C-RASP, which provide building blocks that can be combined to show that transformers recognize a whole class of languages.  The fact that [Yao et al, 2021] shows that transformers can recognize Dyck-1 strengthens, rather than weakens, our claim that Kₜ[#] is a better characterization of transformers than FOC[+;MOD].

At present, we don't know how to define Dyck-2 in Kₜ[#], so this would be a good target for future work. But we note that [Yao et al, 2021]'s Theorem B.3 appears to use hard attention, and also relies on Lemma B.1, which implicitly uses a nonstandard variant of layer normalization that can apply only to a subset of vector components (cf. multi-pre-norm from [Merrill and Sabharwal, 2024]). As such, it may not be straightforward to apply their construction directly to standard transformers, which is the setting we are working in. 

2. By "deeper," we mean the number of transformer blocks (where a block is self-attention layer followed by a feed-forward layer). Our construction simulates a Kₜ[#] formula that has modal depth $k$ (§3.3) by a transformer with $4k+1$ blocks. (We are unsure what you mean by $t$, but to be clear, the depth of the transformer does not depend on the input string length.)

This is in contrast to FOC[+;MOD], which [Chiang et al, 2023] show can be simulated by a transformer that only needs $2$ blocks. Since in practice it seems that deeper transformers are better for more complex applications, it seems to be a strength of Kₜ[#] that it translates into deeper transformers.

Let us know if you have more questions or concerns, and we would be glad to elaborate!

[Bhattamishra et al, 2020]: https://aclanthology.org/2020.emnlp-main.576

[Chiang et al, 2023]:
https://arxiv.org/abs/2301.10743

[Merrill and Sabharwal, 2024]: https://arxiv.org/pdf/2310.07923

[Yao et al, 2021]: 
https://aclanthology.org/2021.acl-long.292/
> First, the paper gives the particular example of Dyck-1, which is definable in Kₜ[#] but not FOC[+;MOD]. Many other separating languages exist, due to the inability of FOC[+;MOD] to model ordering, but this is an especially important one. It has clear practical relevance to modeling natural languages and programming languages, and we also know empirically (Ebrahimi, 2020) that transformers can learn Dyck-1.

The inclusion of Dyck1 is nice. Do you have other examples that are not in FOC[+; MOD] but in $K_t[#]$? I ask this because [1] already shows Dyck can be represented by two-layer Transformer. (actually not only dyck1 but also general deck language, but of course it only shows dyck so it has no confliction with this work)

[1]  Self-attention networks can process bounded hierarchical languages, ACL 2021, Yao S, Peng B, Papadimitriou C, et al.

> Second, whereas the translation from FOC[+;MOD] outputs a transformer of bounded depth, our translation from Kₜ[#] outputs deeper transformers for deeper formulas. While we don't know whether deeper transformers are in fact more expressive, we suspect that they are, and practical applications certainly suggest that they are. So the fact that Kₜ[#] translates to deeper transformers suggests Kₜ[#] is much stronger and closer to actual transformers than FOC[+;MOD].

What do you mean by deeper? Does the number of layer you constructed depends on $t$?
I thank the authors for the useful response.

The points about LTL(C,+) are well taken. I encourage the authors to make the differences more explicit in the revision.

> Indeed, attention weights may become zero on large enough inputs if we round to the nearest number, but we don't think this is a fatal objection. Another reasonable policy, like rounding up, would avoid this.

If one rounded up values on the order of 1/N to some small nonzero fixed-precision number \epsilon, and then summed up over all inputs, one would get a number on the order \epsilon N simply when each position has the value 1 -- certainly an undesirable situation, and seemingly breaking the proof of Lemma C.7. Perhaps rounding after division leads to more reasonable results. I take the authors' word that they will make this more explicit in the final version.

In reaction to the authors' response, I am increasing my score.