Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers
Authors: Andy Yang
David Chiang
Venue: COLM (2024)
Keywords: Transformer Encoders, Transformer Decoders, Formal Expressivity, Formal Language Theory, RASP, Temporal Logic, Counting Logic,
TL;DR: We identify the strongest known logic that the standard softmax transformer can simulate, and explain how to use it to hand-code algorithms into transformers with unbounded input length

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.

Published as a conference paper at COLM 2024
Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers
Andy Yang & David Chiang
University of Notre Dame {ayang4, dchiangg@nnd edu
Abstract
Deriving formal bounds on the expressivity of transformers, as well as studying transformers that are constructed to implement known algo- rithms, are both effective methods for better understanding the compu- tational power of transformers. Towards both ends, we introduce the temporal counting logic Kg [ alongside the RASP variant 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 at- tention transformers with unbounded input size. We prove this by show- ing all [+##) formulas can be compiled into these transformers without any additional positional embeddings.
1 Introduction
What problems can transformers (Vaswani et al., 2017) solve, what problems can they not solve, and how can we prove it? Formal logic, connection with programming language theory, formal language theory, and finite model theory, give framework in which to investigate these questions.
Previous theoretical work, surveyed by Strobl et al. (2024), has advanced our under- standing of transformers immensely. However, it has not provided full account their expressive power. Much of this work only considers modifications of transformers, like average-hard attention transformers (AHÁTs) (Barceló et al., 2024) or unique-hard atten- tion transformers (UHATs) (Angluin et al., 2023), which are not known to be either subset or superset of standard, soft-attention transformers (SMATs). At the same time, program- ming languages like RASP (Weiss et al., 2021) propose 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,(#), temporal counting logic. Along the way we develop a RASP variant called C-RASP, equivalent to K, #). Both are, to our knowledge, the tightest- 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 K2 #
We prove that the previous best lower bound, FODD+;MOD] (Chiang et al., 2023), is strictly less expressive than K, ().
We prove that transformers which use fixed-precision numbers (as real-world transform- ers do) can be compiled back to K,##).

---

Published as a conference paper at COLM 2024
2 Background
Previous theoretical work 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 fu- ture masking. In particular, these encoders perform the same computations as one step of transformer decoder. Decoder-only models like GPT (OpenAT, 2023) currently dominate applications of transformers, while empirical work has noted they have significant lim- its 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 closely approximate real-life behavior) is TC (Merrill and Sabharwal, 2023). The previous best lower bound is FOC[+; MOD] (Chiang et al., 2023). We strengthen this lower bound using Kt 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.
2.1 Hard and Soft Attention
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 AHAI' and the standard SMATs actually remains very open area of inquiry at the moment.
In particular, is not yet clear how the expressivity bounds on average-hard attention transformers apply to softmax attention transformers. On the one hand, average-hard at- tention 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 expres- sivity 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, [), we note that they only prove is a lower bound for average-hard attention transformers, not soft at- tention transformers. We can view Ki [#] and C-RASP 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 average- hard and softmax attention.
2.2 RASP and Tracr
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 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 inap- propriate for compilation into standard transformers.
The primary example is RASP, which makes three strong assumptions. First, the transform- ers 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;
2

---

Published as a conference paper at COLM 2024
this allows compilation of expressions involving arbitrary binary predicates like x y x < y. Third, they assume position-wise feed-forward networks can implement any com- putable function, with the rationale that any continuous function can be approximated by the universal approximation theorem (Hornik et al., 1989).
Building RASP, Tracr (Lindner et al., 2023) compiles subset of RASP into standard transformers. It compiles RASP selectors to dot-product attention, although this requires 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 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, #).
2.3 FOC[+;MOD)
Counting logics are rich area (van Benthem and Icard, 2023) of logic, whose connec- tion 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 positions can very naturally simulate counting terms. Chiang et al. (2023) define a variant of first- order logic with counting quantifiers, called + hand, any sentence of +ÖC[+; MOD] can be translated into an equivalent soft attention transformer encoder, and on the other hand, any fixed-precision soft attention transformer encoder can be translated into an equivalent sentence of FOC]+;MOD).
and prove that, the one
However, [DC[+;MOD) seems somewhat underpowered. It has normal form that uses only one quantifier alternation (3x.3=*p. p....) and only one position variable. This means the equivalent transformer only has depth 2, and only uses the output of self-attention at one position. By considering an ordering on positions (and future-masking on the corre- sponding transformers) we derive much better lower-bound result.
2.4 Temporal logic
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 position in from 1 to n, would seem to correspond to tensor of n² values in the corresponding transformer, but transformers only have It values at each layer and n² values in the attention weights.
Whereas FOC[+;M MOD] avoids this difficulty by using normal form with only one vari- able, 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 string w.
Until the first symbol I, w contains only l's. Only the symbol has appeared since position 2 in w. At no position does contains a
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
3

---

Published as a conference paper at COLM 2024
can only depend times < i- provides natural way to model future-masking in trans- formers. 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-utilize in the field of formal methods (Fisher, 2011), solidifying this connection with transformers may allow more ideas to get shared across disciplines.
C-RASP
We follow in the footsteps Weiss et al. (2021) to define a variant of RASP called C-RASP. The audience may find the syntax of C-RASP is easier to follow, so present it first before defining K, (although both are equivalent in the end). proofs, we generally prefer the more compact syntax of K #), but for writing programs,
C-RASP.
3.1 Definitions
Definition 3.1 (C-RASP). A C-RASP program is defined sequence Pl...., Pr of C-RASP operations. There are two types of operations:
Boolean- Boolean-Valued Operations
Count-Valued Operations
Initial
P(i) == Qa(i) for a EE
Counting
C(i) = # # P()
Boolean
P(i) := (i)
Conditional
C(i) == ()) C2(1
P(i) := (i A (2(
Addition
C(i) +2()
Comparison
P(i) :- ()) I C2(1)
Subtraction
C(i) C) -2))
Constant
P(i) := 1
Min/Max
C(i) == min min(G (1),
C(i) == max (1),
Constant
C(1) :
Counting operations count the positions < i such that P(j) holds, returning the sum We could also extend the syntax to use an expression P(ij) which depends on both and j; this can be transformed to P(j) since our logic has only unary predicates, as shown in Lemma A.1. Conditional operations return C1 holds, and C2 otherwise.
By convention, when using C-RASP program to recognize languages, of the last operation, which must be Boolean-valued, at the last position, determine ac- ceptance. That is, if the program is D, then we accept w if and only if D(n) is true.
use the value
input w with length n, and the last operation is
Example 3.2. We present program to recognize Dyck-1 example. More annotated examples can be found in Appendix A.2
C()) == |i < 1] (())
The number of ( (pp to position
(i(1) := | i ()()
The number of) ) up to position
V(1) := (,))
Violation: there are more ) than
Ct()) := # []
The number of Violations
M(1) := Cy(1)
Matched: zero Violations
B(i) := G()=-(()
Balanced: same number of and)
D(1) = A(I)
String is Matched and Balanced
4

---

Published as a conference paper at COLM 2024
4
The Temporal Counting Logic K;
In this section, we define the temporal counting logic K
4.1 Definitions
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 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 Kg (#] in Backus-Naus form:
F : Qa -F -F FAFFICCC C = := # C+CIC-C|1
In temporal logics, formulas and terms are written without arguments because they are always interpreted with respect to structure at a specified position. In our setting, they are interpreted with respect to a string w at a position i, where w = W1W2- ... Wn and i E n]. integer, written C and defined as follows.
A count term C is interpreted
# [F
K E [1 w. F}1
(C1 + C2)
Cti + C2
(C1 C2)
Cip C2
=
1 w.
1
As syntactic sugar, we allow the use of any natural number as constant, which implicitly is defined as sum of 1's. Similarly, 0 can be defined #[-T], and as #[T]. Next, the interpretation of formula F at position i, written w, i = F, defined as follows:
w, i = Qa
Wi = a
w, i = FF
w.i 7 F
w, F F F
w, í F1 and w, F F2
CT < J
T
is always the case
We say that string with length end-satisfies & formula of Kg whenever w,n F (Maler and Pnueli, 1990). The language defined by & is the set of all strings end-satisfied by Φ. As final note, whenever is implicit, can write F(i) which is True iff w, F F and also write C(1) which is equal to C
4.2 Examples
Although an exact characterization of K₃ ( is not currently known, we see that it can define a variety of regular, context-free, and non-context-free languages.
We pronounce Ki as "K-t-sharp". The logic K, 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 strings. Additionally, is the modal counting operator, which is fairly standard notation in counting logics.

---

Published as a conference paper at COLM 2024
Language
Formula
dbb'
#[Qa A [[Qb] 2 1)] =
a" a"
#[Qb A # Q (#10s) 1] =0
a c"
#[Q; A (#[Q.) =0] = #[Ob]
A#[Qa ( - 0)] #(A
A#[ = #[Qx] = = QQ: = #[Ow]
Dyck-1 hello
Q # -
5 Q
=1 =
is of note that the context sensitive language a c" has been observed to be learnable by transformers (Bhattamishra et al., 2020).
4.3
Modal Depth
The modal depth of a formula & or term C, which we notate as md(4), is the maximum level of nesting of # terms. That is,
Definition 4.1.
md(Qu Qx)
0
md(1) md (#(Ø)) + md
md
md
(d A 92) = max(md (Q2)) md(C C2) (G)
md C2) max max (C)) md(C2))
The following construction gives some intuition on the effect of modal depth.
Lemma 4.2. For every string of length n, there exists a formula &a of modal depth such that w = 4a if and only if w contains as subsequence.
Proof. Let = $1$2 Sn. Then define 4: := In 2 where
# #[Q.,]
QOt+I A Tk 2 1]
6k 6k+1
+
Q A T > 2]
S% 5k+1
Verification is left as an exercise for the reader.
As a consequence of the above and Theorem 5.7, we see that masked soft attention trans- formers can recognize all the piecewise testable languages (Klíma and Polák, 2010), a subset of the star-free languages. Recall, however, that K, can express much more: for example, the context sensitive language a"b"c". A comprehensive study of the expressive power of K and C-RASP (and the effect of modal depth on expressivity) would be informative, and is left for future work.
4.4 K2 and C-RASP
C-RASP may have a more convenient syntax to write programs in, but C-RASP programs and K2(#] formulas are exactly equivalent in expressivity.
Theorem 4.3. C-RASP program recognizes language L iff a Ki(#] formula defines L. More precisely, given alphabet E, for any (#) formula & there is C-RASP program P such that Σ end-salisfies & iff w is accepted by P, and vice versa.
Proof. See Appendix A.3.
From K, to Masked-Attention Transformers
In this section, we show how to compile Ki into transformers. It would also be possible to translate directly from C-RASP to transformers; this would use fewer dimensions, but more layers.

---

Published as a conference paper at COLM 2024
5.1 Transformers
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 a over a finite alphabet Σ. We prepend to special symbol BOS, which assume is not in Σ. We abbreviate и + 1 as n².. A word embedding with dimension d over Σ is function WE: UU (BOS) - Id applied position-wise to string of length to form tensor in Raxx""
Definition 5.2 (Transformer Block). A transformer block B, defined with dimension d, R Raxx' that computes
specifies a function B: Rdxn'
B(A) = (FF(FFN(A') + A
A' = LN:(SA(A) + A)
where SA denotes a self-attention layer, by the standard definition (Vaswani et al., 2017), FFN denotes two layer feed-forward neural network with ReLU activations between the layers, and LN, and IN2 denote position-wise applications of LayerNorm. This setup is commonly referred to "post-norm" block.
5.2 Overview of the translation
The input and output of transformer block are tensors in Rdxn'' 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 count term of a K.(#) formula in different dimension of the residual stream.
Let A RR be tensor in the residual stream. Formulas Ox are stored as two rows of A:
1 - 24h (1) +1 -24xx +
(2 (1) +
A2k- 1:2k, -1
+24 (1) -1 +2 (2)
-
+2
Similarly, count terms C are stored as:
0
(11)
(2 3
C2(n)
2
A
G1
+ (2
C,(x)
0
2
The division of C(i) by 11 is a consequence of the fact that attention computes an average rather than a sum. Dealing with these divisions is common feature of many transformer constructions. In contrast to other constructions that undo the divisions using nonstandard embeddings (Pérez al., 2021; Barceló 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 (Ap- pendix 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 LoyerNorm. ensures that all feature vectors have zero mean, so LayerNorm only applies 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. Con- sequently, for count terms, the BOS position is always O. We can ensure this with a feed- forward layer.
Lemma 5.3. Using the word embedding and a single ford-forward layer, we can set the BOS posi- tion to False, without disturbing the Boolean value at any other position.
Proof. See Appendix B.1.

---

Published as a conference paper at COLM 2024
5.3 Counting using masked uniform attention
Count terms in { can be simulated by uniform self-attention layers.
Lemma 5.4. Let A2 1:2ky store Boolean vector as defined above. For any i, let Ck. be the number of positions S such that A2k 122,j is True. Then there is a transformer block that
Cyi and Csi computes, at each position i, and in two other dimensions 2k' -1,2,, the values FF
Proof. See Appendix B.2 for proof and pictures.
5.4 Other operations using position-wise feed-forward networks
All other Kg (([#] formulas and terms can be simulated by feed-forward layers.
Lemma 5.5. The following position-wiis wise operations can be simulated by a single transformer block, using existing dimensions as imput and a fresh dimension as output: addition (+), subtraction (-), comparison (S), and Boolean operations (A, -),
Proof. See Appendix B.3.
5.5 Compiling K. # formulas into masked uniform attention transformers
Definition 5.6. Fix an alphabet Σ, and assume that the symbol BOS is not in E. We say masked soft attention transformer (as composition of blocks with d dimensions simulates K, [#) formula if for every input to E E" with length n and every subformula 4/ of Φ, there is some dimension dx such that
BB o... B1 WE)
if w. 4%
[T(OOS -124,,
otherwise.
Theorem 5.7.
For every K($# 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 formula of modal depth m + 1. By Section 4.3, Φ is Boolean combination of:
Subformulas of modal depth at most m.
Subformulas of the form Σxek # 4/x 2 0, where K is a set of indices, 0g are integers, and dt: are subformulas of modal depth m.
By the inductive hypothesis, for each subformula a of modal depth at most m, there is transformer Tę which simulates it. Parallel-compose all the Tę as described by Ap- pendix B.4 into single transformer. Then we need to perform the following operations in sequence:
Compute H1pp for all relevant 4h, as described Lemma 5.4.
2. Compute all formulas of the form Σtek K a## yhx] 2 0, as described in Appendix B.3. Compute all Boolean combinations the above subformulas as necessary.
4. Ensure the BOS position is False.
This can be achieved by adding one block. The first step can be achieved with a self- attention 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 single feed- forward layer.
8

---

Published as a conference paper at COLM 2024
6 Relationship to other formalisms
The expressivity of K # can be characterized in relation to other bounds on transformer formal expressivity. To begin with, the previous best lower bound on soft attention trans- former encoders was FOC[+; ; MOD], lower bound due to its ability to model order.
by Chiang et al. (2023). However, K (#) forms tighter
Lemma 6.1. Kg(#] formulas can simulate FOC[+] formulas, and K, { MOD] can simulate FOC[+; MOD]. In general, for any set P of unary predicates, the extension FOC[+;P] is con- tained in K #; PI.
Proof. See Appendix A.3.
We've seen that C-RASP can define Dyck-1 (Example 3.2), and Bhattamishra et al. (2020) prove that transformers, under the same assumption as ours, can express Dyck-1 1 via very similar construction. However, it's easy show that FOC[+;MOD) cannot define Dyck-1. Thus, K, # is a more realistic lower bound for transformers than FOC[+;MOD]]
Proposition 6.2. There is no sentence of FOC[+; MOD] that defines Dyck-1.
Proof. Suppose that such sentence exists. Chiang et al. (2023) show that there exists an M such that o cannot distinguish between two strings that differ only by swapping symbols exactly M positions apart. Since (M)M E Dyck-1 and (M-1()-- g Dyck-1 but o cannot distinguish them, we have a contradiction.
On the other hand, it does not seem that K,[#] 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.
Indeed, reconciling the K, [#)] bound softmax transformers with other bounds on hard- attention transformers poses challenges. For instance, K,[#] seems to be incomparable with FO[<] (Angluin et al., 2023). K; can express Dyck-1 but FO <<] cannot, and FO <<] can
express >x aa>" which K₁ does not seem able to do.
Furthermore, we also note that K, { is strict subset of LTL(C,+) which Barceló al. (2024) show is a lower bound on average-hard attention transformer expressivity. How- ever, average-hard attention transformers are known be either 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 tention transformers is left for future exploration, and is expected to require modifications to the standard architecture in order to derive an exact inclusion.
As final note, there appears to be a sizeable gap between the lower bound of K, [#] and the upper bound FOM [BIT] shown in Merrill and Sabharwal (2023). In particular, the latter can express integer multiplication, but suspect K₃ [#) 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 clearer picture of transformer expressivity.
7 From Fixed-Precision Transformers to K,
In practice, transformers fixed-precision numbers. We adapt the proof that FOC[+] can simulate fixed-precision soft attention transformers (Chiang et al., 2023) to show that K; # can simulate fixed-precision, masked soft attention transformers. If K, #) is extended with modular predicates, it can also simulate sinusoidal positional encodings.
Theorem 7.1. K, [4] can simulate -reci-preiiioon masked soft attention transformers without posi- tional encodings, and K, #; MOD] can simulate exxed-rreission masked soft attention transformers with sinusoidal positional encodings.
Proof. See Appendix C.

---

Published as a conference paper at COLM 2024
8 Autoregressive C-RASP Programs
With a simple extension, we can use C-RASP to construct decoder language models.
Definition 8.1 (C-RASP Language Model), Assume C-RASP program over alphabet Σ has vectors Na (i) defined for each a Σu (EOS). Then a C-RASP program can con- verted to autoregressive language model with greedy decoding in the following manner
Translate the program into a transformer.
2. Append linear layer, which selects the dimensions which simulate Na
3. Consider last position as a uniform probability distribution: dimensions with will have the same maximum probability score, and all those with ((wl = 0 will have the minimum probability.
Na((w))
4. Run the transformer on w, and then select an such that the N,, dimension holds the maximum probability, with arbitrary tie-breaking. Append a to w. and repeat until EOS selected.
We say a C-RASP language model assigns nonzero probability to word w = WD n iff w, i == Ne for all 0 n 1, and w, F NEos- We say a C-RASP Language Model recognizes language I. whenever it assigns nonzero probability to w iff w E L.
In logical terms, we can construct C-RASP language model to recognize L iff there exists formula & of K # which recognizes L and for all E Σ we can define formulas N such that w += N₂ < .waww F 4. In this case, NEos Φ
Example 8.2. Append to the end of Dyck program in Example 3.2 the following operations:
(i) = - Qios(i)
(1) == QEos( ((()) c((1)
(1) D(1)
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 lan- guage L we can define a formula + of K. which recognizes L. Next, observe that it is always the case that 3w wwaw' } Φ. Finally, define NEos & and Na T for all E. 0
Concluding Remarks
We have introduced the temporal counting logic K, () 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 K2 can com- pile directly into standard transformers. As such, an implementation of C-RASP should prove appropriate for constructing transformers to run experiments on, and further the- oretical analysis of ((#)) and its extensions should shed light on the expressive power of transformers.
10 Acknowledgements
We would like to thank Dana Angluin, Pablo Barceló, Stephen Bothwell, Peter Cholak, Dakotah Lambert, Anthony Widjaja Lin, Anand Pillay, Jon Rawski, Darcey Riley, Ken Sible, Aarohi Srivastava, Lena Strobl, and Chihiro Taguchi for their feedback and support.
10

---

Published as a conference paper at COLM 2024
References
Dana Angluin, David Chiang, and Andy Yang. Masked hard-attention transformers and Boolean RASP recognize exactly the star-free languages, 2023. URL htt.tttss////aiv..ttm abs/2310. 13897. arXiv:2310.13897
Raman Arora, Amitabh Basu, Poorya Mianjy, and Anirbit Mukherjee. Understanding deep neural networks with rectified linear units. In Proceedings of ICLR, 2018. URL https:
//openreview. net/ ftrff/rrummdd1111 rgWRW.
Pablo Barceló, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir Podolskii.
Logical languages accepted by transformer encoders with hard attention. In Proc. ICLR, 2024. URL
Satwik Bhattamishra, Kabir Ahuja, and Navin Goyal. On the ability and limitations of Transformers to recognize formal languages. In Bonnie Webber, Trevor Cohn, Yulan He, and Yang Liu, editors, Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 7096-7116, 2020. doi: 10.18653/v1/ //2200.. org.ee/2r//2222 emnlp- mamllpmmin.55. 576.
mmnll-main.576 URL
Shaked Brody, Uri Alon, and Eran Yahav. On the expressivity role of LayerNorm in Trans- formers' attention. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki, editors, Findings of the Association for Computational Linguistics: ACL 2023, pages 14211-14221, 2023. doi: 10.18653/vl http///12223..fmm/// findings-acl..8 URL https://aclanthollog org/2023. findings-and auss-acl.00 895.
David Chiang, Peter Cholak, and Anand Pillay. Tighter bounds on the expressivity of transformer encoders. In Proc. ICML, 2023. URL http::///aaxiv..orabbssssse
10743.
Stéphane Demri and Denis Lugiez. Complexity of modal logics with Presburger con- straints. Journal of Applied Logie, 8(3): 2010. doi: 10.1066/jaal.201000..001
Nouha Dziri, Ximing Lu, Melanie Sclar, Xiang Lorraine Li, Liwei Jiang, Bill Yuchen Lin, Sean Welleck, Peter West, Chandra Bhagavatula, Ronan Le Bras, et al. Faith and fate: Limits of transformers on compositionality. Advances in Neural Information Processing Systems, 36, 2024.
Nelson Elhage, Neel Nanda, Catherine Olsson, Tom Henighan, Nicholas Joseph, Ben Mann, Amanda Askell, Yuntao Bai, Anna Chen, Tom Conerly, Nova DasSarma, Dawn Drain, Deep Ganguli, Zac Hatfield-Dodds, Danny Hernandez, Andy Jones, Jackson Kernion, Liane Lovitt, Kamal Ndousse, Dario Amodei, Tom Brown, Jack Clark, Jared Kaplan, Sam McCandlish, and Chris Olah. A mathematical framework for transformer circuits. Transformer Circuits Thread, 2021. URL tttts::/ttransfomme--iiii 0021/framework/ing wwtp///inxx..... html.
pub/
Michael Fisher. An infroduction to practical formal methods using temporal logic. John Wiley & Sons, 2011.
Dov Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. On the temporal analysis of fairness. In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programminn Languages (POPI., pages 163-173, 1980. doi: D0.1109/FSCS. SECSCCSS199.888 1999..9589,
Kurt Hornik, Maxwell Stinchcombe, and Halbert White. Multilayer feedforward net- works universal approximators. Neural Networks, 255):359-366 1989. 10. 1016/ 0893-6080 (89))
Ondrej Klima and Libor Polák. Hierarchies of piecewise testable languages. Interna- tional Journal of Foundations of Computer Science, 21(4):517-533 2010. doi: 10.1142/
50129054110007404
David Lindner, János Kramár, Matthew Rahtz, Thomas McGrath, and Vladimir Mikulik. Tracr: Compiled transformers as a laboratory for interpretabil- ity. In Advances in Neural Information Processing Systems 36 (NeurIPS), pages 37876-37899, 2023. URL https: http::::/ppppssnnt/ee nips. cc/ cwtpppppppppppeeeeecceecceeee. files//aper//222//1e 7711 771155abaae7 44eaaaae774688111114441 (t115/777113bbb777--------6 77 wtt.o//baaaaaabbttttat----ooooeo
html. html..
11

---

Published as a conference paper at COLM 2024
Oded Maler and Amir Pnueli. Tight bounds the complexity of cascaded decomposi- tion automata. In Proceedings of the 31st Annual Symposium on Foundations of Computer Science (FOCS), pages 672-682, 1990. doi:
William Merrill and Ashish Sabharwal. A logic for expressing log-precision trans- formers. In Advances in Neural Information Processing Systems 36 (NeurIPS), pages 52453-52463, 2023. URL https: httpppaappsss//////eee/eeeeeeeep nips. cc/ wtweeerfieeeseeeeeeeeeee html.
William Merrill and Ashish Sabharwal. The expressive power of transformers with chain of thought. In Proceedings of the Twelfth International Conference on Learning Representations (ICLR), 2024. URL https://openrewwe nwt/forummiddateeeeeee idwirunnhii
William Merrill, Vivek Ramanujan, Yoav Goldberg, Roy Schwartz, and Noah Smith. Ef- fects of parameter norm growth during transformer training: Inductive bias from gradi- ent descent. In Proceedings of the 2021 Conference on Empirical Melhods Natural Language Processing (EMNLP), pages 1766-1781, 2021. doi: 10.18653/v / http:/022.emmmmmaai.......
URL /tthhttt////lllanoolooyy hwwphhholog..ooooo...ooooo org/20211 http:222eeemmmmmaiii....m 133.
OpenAL. GPT-4 technical report, 2023. arXiv:2303.08774
URL http:///arii..or//b//223..01111
Jorge Pérez, Pablo Barceló, and Javier Marinkovic. Attention is Turing-complete. Journal of Machine Learning Research, 22:75:1-75:35, 2021. URL http://jmlr.org/// wwtp:ppers//p////// 20-302 302. html.
Nicholas Rescher and Alasdair Urquhart. Temporal Logic, volume Springer Science & Business Media, 2012.
Lena Strobl, William Merrill, Gail Weiss, David Chiang, and Dana Angluin. What formal languages can transformers express? survey. Transactions of the Association for Compu- fational Linguistics, 2024. To appear.
Johan van Benthem and Thomas Icard. Interleaving logic and counting. Bulletin of Symbolic Logic, 294455333- 2023. doi: 10.10177bsl.2023.3
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in Neural Information Processing Systems 30 (NeurIPS 2017), 2017. 1 14w.0000ee1.14444-aaaaaeeeeeeeee
URL https:/
https::/pproceedings new.eeiddiinnnnuniss..... cctppaper//1////a/ae/
Gail Weiss, Yoav Goldberg, and Eran Yahav. Thinking like Transformers. In Proceedings of the International Conference on Machine Learning (ICML) pages 11080-11090, 2021. URL https:// https://proceedings morssmmr.... www..press/vi. 39 wtt.:eeee//111//iiss222111 html.
Shunyu Yao, Binghui Peng, Christos Papadimitriou, and Karthik Narasimhan. Self- attention networks can process bounded hierarchical languages. In Proceedings of the 59th Annual Meeting of the Association for Computational Linguistics and the 11th International Joint Conference on Natural Language Processing (Volume 1: Lonng Papers), pages 3770-3785, 2021.
Hattie Zhou, Arwen Bradley, Etai Littwin, Noam Razin, Omid Saremi, Josh Susskind, Samy Bengio, and Preetum Nakkiran. What algorithms can Transformers learn? A study in length generalization. In Proceedings of the Twelfth International Conference on Learning Representations (ICLR), 2024. URL
12

---

Published as a conference paper at COLM 2024
A Proofs Related to C-RASP
A.1 Extensions
Lemma A.1. Consider extension of C-RASP in which the counting operation has the form
C(i) lj S F(i,))
which allows F to be a Boolean combination of C-RASP operations P(1) and P(j) evaluated at both i and j. Any program with this extended operation is actually equivalent to C-RASP program with only the normal counting operation.
Proof. Let F be a Boolean combination of PI...., Ps evaluated either or j. First, observe that C(i) = (i) + C2(1) - C3(1) where
C(i) #2 lj S i V(i))
((f) #2 [J R(t))
C2(1) == #2 [ /] B(L))
C1(i) :- #2 1 A(LD)AA
Now, write F in DNF and split using the above. Now every single counting operation is of the form
(ARCOAA A P.()) xEJ
C(i) = #11
xel
Where I and store the indices of C-RASP operations which depend on i and j, respec- tively, within the counting operation. Observe then that this equivalent to
C(i)
A XEINj
P2(O)
Thus, every #2 operation be factored out sequence of normal # operations.
A.2 More C-RASP Examples
We sometimes put multiple C-RASP operations on the same line for brevity.
a*b" b" over I = b}
Ca(i) # Qa(i) (,(1) = # (x())
# positions with a's
# positions with b's
V(i) ==
1
Violation: an a has b's preceding it Violations
Cv()) == # v({<
Y(i) == (v
Zero Violations
13

---

# ends of subsequence ba the subsequence bab ends at # ends of subsequence bab Published as a conference paper at COLM 2024
a a" over I {a,b}
Ca(i) # # Qa())
# positions with a's # positions with b's
Cg(1) # $ Q6()
BA(i) :- Qa(i) A ((() 21
A subsequence ba ends at i
(ia := # #] BA())
BAB(1) == Qb(1) A Cba 21
Caab (1) = # [j S i] BAB())
Y(i) == Cbub
There are no subsequences bab
cn over Σ (a, b,
(a) : [j S 1] Q=(1)
positions with a's positions with b's # positions with c's No preceding b's or c's
C5(i) == [j 1 Q+())
C.(1) := # [ [ Q=()
A(I) == C,()) =0
B(I) := C=
No preceding c's
(x()) == # # ((O))(())
a's with no preceding b's or c's b's 's with no preceding c's no a's have preceding b's or no b's have preceding c's same number of a's, b's, c's Correct order and number of symbols
Cы(i) := # Q6()) B())
Gf) == Ca(1)= ca(1
Gf( = Cb(i) C,()
Gabe (f) = (1) C.) = C.)
Y(i) Ga(t) A Gi) A Gube (i)
hello over Σ = (,,
(i) [j S i] Qe(1)
positions with e's # positions with ht's positions with l's positions with o's symbols in string A subsequence ends at ends of subsequence he A subsequence hel ends at ends of subsequence hel
C,(f) == [ < | 2x())
C/() := # [ S Q/())
(f()) := [] Qx
(1) := # [j
HE(() = (,,)) =1
(i) = $ HE())
(EL Qi(1) A (i) =1
(i) # $] HEL(i)
HELLO(() = (.(1) A (1) =2
A subsequence hello ends at Length and contains subsequence hello
Y()) = HELLO(i) A C=(i =
As potential point of clarification for the HELLO(1) line, observe that if string con- tains two positions that are the end of subsequence hel, then that string must contain the subsequence hell.
A.3 Equivalence with K, (
Theorem 4.3. A C-RASP program recognizes language L iff K formula defines L. More precisely, given alphabet Σ, for any K,(#) formula & there C-RASP program such that w I' end-satisfies & iff w is accepted by P, and vice versa.
14

---

Published as a conference paper at COLM 2024
Proof. is straightforward to translate Ki(#) formulas into C-RASP programs.
In the other direction, we induct on the length of C-RASP program P = ,,,..., Pn. Assume that Boolean operations (i) are simulated by formulas Px, and count operations C₂(i) = # lj S 1] V(j are simulated by terms Cg This is straightforward, but there are many cases. min/max max operation, we divide the formula into two cases depending on what the result of the operation should be.
The main idea is that whenever we have a conditional or min/
If Pu+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 Px+ = =Qo(1), let Pk+1 = Qa-
If PK+1 (i) -Pr(i) let P2+1 -P,-
If P&+1 -Pe(i) A (i) let PK+1 Pe Pm
If 1 Ci((i) - (i) we need to divide on cases to handle if (f) is condi- tional or min/ max, as Kt does not have these terms built in. This is straightfor- ward, but there are many cases.
If Cii) # I (1 let č₁ #[A]. Then:
(m) # و i| P2(1), let P = C₁ [
C.) (2(1) ? C3(() (1),,, let P-, = (B2n C2 C)) C4).
If (1) min(C.(ii,C(())) let Pat1 = (C3 S ( CAA
C. C4).
If (i) max(Cs(i),C((i)) let PAt1 = (Cs 2 CAce s v))( N
C,)C5(C)..
C P1+1 S. Sc
((C C2)),, then:
(i),,, (i),),tt let PA+11 ( (
= = B/ (CCGG//AAAAA/GGG)(()//...../
[ let - (
CocGCc/cccCCAAGGGGGGCCCC......C. GAG5
C4).
(1) = ()x(C)(), let A (A)
&SCMM < (,) (CC S (1).
If (t) c, for C let P 1 -QASSOVVAAAASS5
If Cx() = ()) then:
If C.) ( P2(1), let P = (G s C2G # [12) 2 C2A
((
Cf) = ? C3(f) : C4(,), C(() (CC
S
C2 P3 A G
C1).
Cm) = (() let = $
G,C () GAGZGGGEC)
(G&GAG 2 (G
If = ma) let P.y = (
GAG=GGG
Cf force P.ts (G < G GGGGGGG)))
15

---

Published as a conference paper at COLM 2024
If (i()) max (i), this identical to the previous case but just switch G < C2 with C₁ Cz-
If Ci( с for c E IN, this should be straightforward given the above cases written out.
[ contains FOC[+], and MOD) contains MOC[+;MOD] In general, for any set P of unary predicates, the extension FOC[+;P] is contained in K,(#;P,, when defined expected.
Lemma 6.1.
Proof. All FOC[+] sentences can be rewritten in the following normal form (Chiang et al., 2023, Theorem 1):
3x1 ... Exp. EV (...p) X
where all 4i and quantifier-free, and is set of linear constraints on Xu- With respect end-satisfiablity, this is simply equivalent to the K formula.
X (# (#(41) ..... #(.....(.#11.) ((pp))
The same is true for FOC(+;MOD), if we extend Ki(#) with modular predicates to Kc[*MOD]] where (w, F MOD, = i = mod m.
In general, from this normal form we can see that for any set unary predicates, the extension FOC[+;P] is contained in K,[#;P], when defined appropriately. Furthermore, all of these will be K.(#] formulas of modal depth 1.
B Proofs: From K₁ # to Transformers
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 LayerNorm
Definition B.1. LayerNorm is a function f IRd + Id such that
f(x) x- 0
where
μl
1 Σ 7 X
1 d
Xi 11) 2
Observe 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 Boolean vector that is True at the BOS position and False everywhere else. We call this a Start-Separating Vector, adapting termi- nology from Merrill and Sabharwal (2024). Using the word embedding for BOS, can construct dimension that holds such a vector (ensuring WE(w,) is true dimensions 2k. 1, 2k2 only when w; BOS).
16

---

Published as a conference paper at COLM 2024
1
2
n'
2kg -1
1
-1
+1
+1
2kg
+1
-1
-1
B.1 BOS Handling Lemma
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 feed-forward layer which computes the min of every value in an odd dimension with the value in dimension 2k, of the Start-Separating Vector and the max of every value in even dimension with the value in 2k,, described in Lemma 5,5, Since we' ve maintained that values are #1 in our Boolean representation, this sets the BOS position to be False, while the others unmodified.
B.2 Counting Lemma
Lemma 5.4. Let A2x-1:23 store a Boolean vector defined above. For any i, let Cj. be the number of positions < such that A2-1:22, is True. Then there a transformer block
that computes, at each position i, and in two other dimensions 2k' 1,2K, the values 1=1
Ct
and Gu
Proof. First, recall the definition of masked self attention layer SA: Rdxx 4 Rdxn;
SA(A) [Co Cx] where
w(O); Rd Rd
W(K); Rd R4
W(V) Rd + Rd
Sij = W(R) A.; W(() A.j
Va
exp(si)) (s W(()
A.j
C Σ o exp(s;))
To simulate count term #[Ø] C(i) of [] we need to construct transformer block such that if the Boolean values (f) are stored in some dimension 2k - k, we can compute C(i)
TFI in some other dimensions 2k' 1,K'
To achieve this, only need uniform attention that is, at each position i, we set W(Q) w(k) 0, which makes sij for all i.j. This spreads attention weight evenly across all positions <
Furthermore, by setting WVV as follows, we can add the value from position in dimen- sions 2k - 1, 2k to position i in dimensions 2 1,2k'.
17

---

Published as a conference paper at COLM 2024
2k
1
2k
2k
2k
2k 1
2k
W(V)
2K
1
0
2k
As such, we get the attention layer to compute the average of all unmasked positions S Recalling the definition once more, the general expression reads:
C1 E Exxe A.,yk
0 exp(sij)
Then, with the use of uniform attention and our carefully constructed W(V), we compute in position i of dimension k, the value G₁A, which is the average of all values up position i dimension k, The expression reduces to:
Ci = Σ o (Wp(s;)[W(\>A,
Σ (WWW(( Ej=0exp(ss) exp(sij)
Σ Avi Σj i+1
Σ Auj
E
Before moving on, note that we represent Booleans -1, instead of 0, and we'll also write the sum of positions j < i that hold True as Cja- Here we write out the resulting tensor after the described self-attention layer showing the relevant dimensions positions 0,1,...,ft nt, We write B; E { be the Boolean value at position
n
:
2k - 1
+1
-B +1
2B +
2k
+2B
+2B,
-2 9id
Eua +1 u+1
2k -
+1
-2
+2 9
+2 Cus'
2k
0
-1
1
Note, however, that instead of the desired value , we have actually computed 2 Ci
.1 1. We use a feed-fo 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 feed-forward layer that simply adds dimension 2kg - to and 2kg to 2k order to remove the +, and then divides by to get the result:
18

---

Published as a conference paper at COLM 2024
1
2
n¹
:
2k
0
1
S
1+1
2k
2
#+1
L:
As final note, which is relevant for the later subsection on arithmetic comparison, we will make every self-attention layer compute counting operation over the start-separating vector (Appendix B.1) in order to compute the value . at every position in some dimen- sion.
B.3 Feed-Forward Lemma
Lemma 5.5. The following position-wise operations can be simulated by a single trans- former block, using existing dimensions as input and fresh dimension output: addition subtraction (-), comparison (<), and Boolean operations (A, -). Arbitrary Boolean ex- pressions in DNF 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 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 W1 such that we add the appropriate values to the fresh dimension, and negate using W2 if needed.
Min/Max: Recall that ReLU(x)) = max(0, x). Then min y) = x ReLU(xx - y).
If < y, then ReLU(x y) 0, so x ReLU y) min(x,y) If 2 y, then ReLU(x y) = x - y, so x ReLU - y) = (x- = min(x,y).
Similarly, max(x,y) x ReLU(y x). Therefore there exist FFNs to compute the min or max of two real numbers:
min(x,y)
max(x,y)
1
1
-1
-1
1
-
1
-
1
-
X
X
To 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.
19

---

Published as a conference paper at COLM 2024
Comparison: This requires access to + + in some dimensions 2ko 2kg. This is easily achieved by requiring every self-attention layer to perform counting operation over the start-separating vector (Appendix B.1).
First we explain how to simulate comparison of two count terms G (i) S C2(1). Then, we describe how to extend this to compare linear combinations count terms.
Suppose that want to compare C and C₂ in dimensions 2k 1, 2kg and 2k2 1, 1,2k2, and put the result in dimension 2k3 1, 2k3. Initially, the residual stream looks like this:
2kg 1
2kg
2k1 1
-00
G(0
2kg
C2
2k2
I+1
2k2
2k3
0
2k3
0
We construct feed-forward layer that computes the function:
0.5
(2))22
gtz(((1)) min (
/0.5 0.5
((i) 0.5
-min (0, X(i)
0
1+1'7+ 11 1 1+1)
7+1
0.5
1
0
1
2
X(i)
equals if C() < C2(1), and - - otherwise. This because the counts C2(1) must be integers, so if (2),,, then C2(1) - (i) + 0.5 2 0.5, and the expression will evaluate to 0.5 and the expression will evaluate - 0.5
Observe that
#1
Otherwise, C2 - (1) + 0.5 < -0.5,
#+
f
is straightforward, then, to use the construction for min/max from above produce feed-forward layer that computes gtz (C2(i) (f)). Essentially, we use W1 to compute the values (using the pre-existing values from the residual stream)
0.5
C2(1 - (1) + 0.5
C2(1) (1) +
i+1
i+1
Then use W2 to compute
20

---

Published as a conference paper at COLM 2024
0.5
0.5
C2 - ( + 0.5 -05
0.5
(2 - (i) 0.5
+ ReLU
ReLU
i+1
i+1
i+1
i+1
i+1
which equals gtz (c2( - G()) as desired.
Similarly, it is straightforward to construct a feed-forward layer to compare linear combi- nations of count terms. That is, for disjoint sets of indices K1 and K2, to compute
Ea 2...0. C.(0 E. xccc(i))
C2(1))
gtz
KCK2
kck1
So we can construct feed-forward layer f Rdd + Rd that computes in each dimension the following
gtz(v1) gtz(U2)
U1
U2
gtz Licke C Cx(i) Lick, a C+(i) gtz Etek, C Cx(1) LtER, CK (()
O
V4-1
gtz(Ud 1) gtz(Ua)
This truncates all positive values in the residual stream at this point to be at position H+
and all nonpositive values to be 0.5 :II As result, the next application of LayerNorm (with appropriate parameter settings) scales every single value to +1. In particular, all
previously-computer Boolean values are preserved, and the newly-computed dimensions 2k3 1,2k hold the correct Boolean value based the desired comparison
As a side effect, all mreiiousyy-copputee counts also get changed to 11, but we do not need these counts any longer due how we organized the construction in Theorem 5.7.
Boolean operations: The Boolean operations A and - can be computed by FFNNs with ReLU activations. Conjunction (A) equivalent min mmx:
2B1 +1
1
2B2 +1
max
-B1 + 1, 1B + 1)
A
2B
1
2B
-1
min( 2B 1, 2B2 1)
Logical negation (-) is equivalent to arithmetic negation, or swapping the positive and negative components:
1
2B
+1
21

---

Published as a conference paper at COLM 2024
For arbitrary Boolean formula, convert it to canonical disjunctive normal form, which is a disjunction 41 V... on of clauses, at most one which can be true for any value of the inputs. Each clause is of the form Im ΛKEK,, Bk, where each By is an input or negated input and Km is set of indices for each clause. A slightly different construction can be used to compute A over inputs in Km- Observe that:
A kEKm
B = ReLU ReLU
Σ km
Bx
(1Kml -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 2Kg 2,g as described in Appendix B.2. Then, because at most one clause can be true, the sum of all clauses will either be or O. Then, we convert back to the +1 representation of truth values.
((I RE
V
A kkEK
Bk
=
11 Σ
ReLU
Σ
Bk
(|Kmll (1) -
#==1
This can all be done in single feed-forward layer.
B.4 Parallel Composition of Transformers
Lemma B.2. Here detail the claim Theorem 5.7 that we can compose many transformers, into a larger transformer which simulates all the formulas the smaller transformers do, in paraliel.
Two transformers Tr and Tz simulating formulas 41 and 422 (using the construction described in Theorem 5.7) can be composed into single transformer T3 that simulates both 11 and 4/2
Proof. We will just sketch out the construction. Let with blocks in d, dimensions and word embedding Emb; simulate Φ and Tr with by blocks in d2 dimensions and word embedding Emb₂ simulate 4/2 the manner described in Theorem 5.7. We can construct Ti + T2 with max (b,, b2) blocks in d1 + d2 dimensions which simulates both Φ1 and Φ2, such that
Ti (w) [2(ww)
(Tr + (1)) =
First, add layers that compute the identity function to the shallower transformer so that both have depth max(k; k2).
Next, concatenate their word embedding vectors
Emb; (a) Emb2 (a)
(Emby + (ab
Then, at each level, we can compose the feed-forward networks FF, and FF, in parallel by creating new FF with
((())
b
W
B(1)
0
w(
6
(2(2)
(
((2)
b(2)
0
(2)
6
22

---

Published as a conference paper at COLM 2024
Furthermore, compose the self-attentions in exactly the same manner, only uni- form attention is used in the construction.
W( w/O
w())
W(K) = W
((())
W(Q) = 0
It is straightforward to verify the correctness of this construction, given we follow the pro- cedure in Theorem 5.7 organizing the simulation by modal depth.
C Fixed Precision Masked Transformers to K; #; MOD]
Definition C.1. A preed--rreiiton mumber with integer bits and s fractional bits is number in Fr,s (i/2 -2 < the two's complement representation of a. That is,
2 For any value E Fy, we write (a), for the b-th bit of
(a); a 2--2- [a 2 b-1 .2.
This a two's complement representation.
helps to access each individual bit of
Proposition C.2. We write x for the b-th bit of x, whenever a fixed-precision number. Then, observe that we can write a formula Fm(x) = x Fm iff we can write formulas (x) =
xb = 1.
Proof. This should be clear by example: 1001 in F5.0- We write Fm)
Fx) A
-FI (x) (x) A -P)
Let us first define what it means for a formula of K MOD] to simulate a Fixed Precision transformer.
Definition C.3. Let E" >> pdxn' be fixed-precision masked soft attention transformer defined exactly the same except we use Fr,s instead of IR. We say T can be simulated in K; MOD] if for every Fm E Fr,s and every dimension of of we can write a formula & such that
[T(BOS w)]kit+ Fm
w, F= D
Similarly, defining predicates Bh (i) for the BOS position. Essentially this means that can write a formula that tells us what value the transformer must output, given any input.
Theorem 7.1. K can simulate fixed-precision masked soft attention transformers with- out positional encodings, and K, #; MOD] can simulate fixed-precision masked soft atten- tion transformers with sinusoidal positional encodings.
Proposition C.4. Assume we have Boolean functions (i) which return true iff the value at posi- tion i in dimension k is Fm FF Then any function of the form fı (2)) f2(xx...,, xx,,..., Xa) where the xx is the value at dimension in position i, can be written as a Boolean combination of F (i).
Proof. Essentially, this is F" x F + {0, which only takes on finitely many values. Thus tedious, but straightforward, to enumerate all tuples of x which should return true, and write formula that returns the correct answer. Let
K {mm m)) (F Fmg) (2(mpr-.... Fk=m,))
23

---

Published as a conference paper at COLM 2024
That is, I stores all n-tuples K of indices such that given n-tuple of fixed-precision numbers which each have the corresponding index in K, the equality holds. Then write
V (AF KEK
This formula will return iff x in dimensions position have the correct fixed -ieed-preciiion values in order to satisfy the equality.
As result, for any function f: 11 F 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 (i), for each feed-forward layer FFN to check whether the output at position in dimension is Fm E Fr,s- Same for LayerNorm LN
Proof. This is direct consequence of Proposition C.4 because these functions all take finite number of fixed-precision inputs, and have 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 out here.
Lemma C.6. Assume we are using Fr,s as our fixed-precision representation. Assume have access predicates F² (i) which tell us if the value at position i has in the b-th bit of its fixed- precision representation. Then we can compute the following summation counting term
2 ΣΣx Xj isi
where Xj is value at position j-
Proof. Observe this summation equivalent to
Σ x Σ ( +2 FF ... 2 151
prts-1(1) 22+s.
Σ Fr+s(i)
1S1
= = + 2#
2 (
As a clarifying note, recall we are using two's complement, which is why the most signifi- cant bit is subtracted.
Lemma C.7. We can write formulas (1) which are true iff the output of a self-attention layer at dimension in position i is Fmm E IFr,
Proof. Recall the definition of a self-attention layer in a fixed-precision masked soft atten- tion transformer, SA: Fdx=_ pdxn.
SA(A) = Cco
cn] where
w( Fd 6s
F
T.
W(K); Fd
F.
1.
W(V); F.d
Fdd
w(Q) A,; W(K), A.,;
Sij
Vd
E exp(s;;) W(() A.)
=
Σ exp((si)
24

---

Published as a conference paper at COLM 2024
More specifically, we want to define a formula cm (k) such that
E Ejsieliki
cm (i)
- Fm
Fm +
where V is the k-th component of the A., The bounds are because division in Fy,s must perform some sort of rounding to the nearest number. We rearrange the equation to the following:
pm (1)
Σ Fm Fm..ekkk
s >E (QOKIVA)) < E ((Pr (
Now observe that we can enumerate all the (finitely many) values that the Fst vector Q; as (Qx)x order to get an expression that only depends on
E Si Fm elr
s Djsi (clrkivt) Ejsi (Fim +2 5) f).e e.er.K))
Q: Q1
e [x
Ejsi
Ejst F' clokk)
s Ljisi (clxKipt) < Ejsi
Q = Q2
(1) +
Ejsi (cl kiv+.
(Fim + 2 5) . el2
Ejsi Fm Cuir+s) 8)
$ Ejzsi (elurtn) K1v e(ams))))
Q -Qa(++s)
[jii (oltsss K1p)) Ejsi (Fm +2 -
This can straightforwardly be translated into Boolean combination of formulas et Q, (i)*
etc., which by Proposition C.4 are definable. Furthermore, by the same proposition it is also straightforward to construct formula QKV(j) that specifies the value of eox elr-Ki
at position j, as well as a formula Fm] that specifies the value of Fm ei This allows us to write the above expression in form such that Lemma C.6 can be applied directly to both sides the equation, thus computing both as count terms and allowing their comparison within K, #; MOD]. Notice that by applying Lemma C.6 we are implicitly scaling both sides up by 29, but this is fine, as equality would still be preserved under this scaling factor.
Finally, to complete the simulation it remains to show that we write formulas that simu- late the word embedding and positional encoding, which will be similar to the construction of Chiang al. (2023).
Lemma C.8. We can write K,(#] formulas WEE (1) that check that the k-th dimension of the em- bedding at position has the value Fm E IFy,,
Proof. For a E E E (BOS), let WE(a) [Empar..., Emgal denote the fixed-precision word embedding for Then, using the same notation as earlier, we can write
WEk (1) =
V
Qa())
(c(o)WE(a)) F..)
25

---

Published as a conference paper at COLM 2024
Similarly, define (i) (i), which checks the word embedding for BOS has value Fm at dimension Sinusoidal positional encodings can be described in the same manner, using modular predicates.
Finally,
Proof. As a direct consequence of the above lemmas, we can write formula of K,(#), which simulates fixed-precision masked soft attention transformer without positional encodings. Adding modular predicates allows Kg #; 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 of the transformer, and width roughly (2(F))) in the precision F and width d of the transformer.
26


Reviews:
[{"review_id": "UnajfpFSks", "reviewer": "Reviewer_TQ9j", "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.", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": true, "final_justification": "", "rebuttal": "Thank you very much for your review. \n\nYou wrote that our results are an improvement over previous results, but the improvement is not so clear. As a lower bound, Kₜ[#] is better than FOC[+;MOD] in the sense of defining a strict superset of languages, but we think you're asking for some intuition of how much better it is. In short, Kₜ[#] is able to account for the expressive power gained by using causal masking and by increasing depth, which the previous result FOC[+;MOD] cannot.\n\nFirst, 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. \n\nSecond, 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].\n\nYou also wrote that our results do not take into account decoding steps, e.g., chain-of-thought. The expressive power of transformer decoders that are allowed to take intermediate steps (chain-of-thought) is by now fairly well understood ([Merrill and Sabharwal, 2024]), and you're right that intermediate steps make the model much more expressive. But there are many situations when it's not desirable to allow intermediate steps; in particular, training data for intermediate steps is not always available. So understanding what transformers are capable of in a single step remains an important question.\n\n[Ebrahimi, 2020]: https://aclanthology.org/2020.findings-emnlp.384/\n[Merrill and Sabharwal, 2024]: https://arxiv.org/abs/2310.07923", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "The paper shows Transformer could recognize language in Kt[#], this gives some improvement on the previous expressiveness result.", "reasons_to_reject": "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.\n\n\n-----------------\nPost rebuttal: I slightly raise my score.", "questions_to_authors": ".", "extra_scores": {}}, {"review_id": "z9TRb7lAf5", "reviewer": "Reviewer_NmSc", "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.\nThe authors show that they are the tightest known lower bound on the expressive power of transformers with causal masking (no positional embeddings).\nSimultaneously, they show that such transformers, when using fixed-precision, can be compiled back into these formalisms.\n\nGiven 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:\n\nCLARITY: 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.\n\nQUALITY: I followed the constructions and believe the formal results to be correct.\n\nORIGINALITY: 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.\n\nSIGNIFICANCE: Providing stronger formal lower bounds on the expressive capacity of transformers addresses foundational questions about modern LMs.", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your insightful review. Regarding the lack of position embeddings, we've considered modular predicates, but it is possible, as [Angluin et al., 2023] do for LTL, to consider any finite-image position embedding in Theorem 7.1.\n\nRegarding LTL(C,+), the short answer is that LTL(C,+) is not known to be simulatable by SMATs, but Kₜ[#] restricts LTL(C,+) just enough so that it can be simulated by SMATs, while remaining above the previous bound of FOC[+;MOD]. For the longer answer, please see below.\n\n# Responses to questions\n1. Indeed, the fact that our results apply to the softmax-attention transformers (SMATs) used in practice rather than AHATs is the main distinction from [Barcelo et al 2024]. Their construction uses a table-lookup operation that relies crucially on the \"winner-takes-all\" behavior of hard attention, so it cannot directly be applied to SMATs.\nFurther differences include:\n- They use nonstandard positional encodings to implement the table-lookup operation. In contrast, ours does not require positional encodings.\n- They interleave unmasked self-attention layers to \"broadcast\" a final value to every other position. Our construction uses only future-masked attention, like in practice.\n- They do not consider layernorm, so any construction that relies on maximizing an attention score at a particular position, like their Lemma 1 or simulation of X (\"next\" operator), may break when the position-dependent scaling factor of layernorm is added. In contrast, our construction works with (and indeed requires) layer normalization. \n2. 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. It's also true that changing the order of operations might affect the final output; for example, [Li et al., 2024] argue that rounding should take place after every term of the summation. Our final version will make explicit where and how rounding should take place.\n3. Regarding the comment on \"overwritten\" values, further explanation is on page 20. Our construction appends computed values to the \"residual stream\", where they are left untouched. However, integers eventually get clipped to ±1 due to technicalities of the comparison operation. The correctness of the construction is unaffected. \n\n[Angluin et al., 2023]: https://arxiv.org/abs/2310.13897 \n[Li et al., 2024]: https://openreview.net/pdf?id=3EWTEy9MTM", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "* Provides simple and intuitive formalisms lower-bounding the capacity of realistic transformers, addressing foundational questions about transformers and LMs\n* Unlike a good deal of the literature on transformer expressiveness, this work applies to realistic soft-attention transformers\n* Provides a construction applying at arbitrary input lengths\n* Provides some idea of how the result could lead to understanding of expressiveness, through example languages and a construction of piecewise testable languages", "reasons_to_reject": "Weaknesses:\n* Except for the finite precision setting (with sinusoidal embeddings), the results do not apply to transformers with positional embeddings.\n* 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.\nUPDATE: The authors have provided useful clarification, which I encourage them to include in the paper.", "questions_to_authors": "* 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?\n* 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?\n* Page 7: “integer values get overwritten” – I didn’t follow this, the statement might be made clearer.\n* first paragraph of Section 5.1 has LaTeX \"??\"\n\n\n[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.", "extra_scores": {}}, {"review_id": "u5NgRwqbAu", "reviewer": "Reviewer_QRfH", "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).", "questions": "", "limitations": "", "rating": 7, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your review!\n\nYou observed that our translation from Kₜ[#] to transformers uses uniform attention, so Kₜ[#] is also a lower bound on AHATs; we'll add this result to the final version! Then, you ask what our results say about softmax-attention transformers (SMATs) as opposed to AHATs. [Barcelo et al 2024] prove LTL(C,+) is a lower bound on AHATs, but their construction relies on the \"winner-take-all\" behavior of AHATs, and it's unclear how to adapt it to SMATs. By contrast, Kₜ[#] restricts LTL(C,+) just enough so that it can be simulated by SMATs, while remaining above the previous lower bound of FOC[+;MOD].\n\nComparisons with other bounds:\n\n- FOC[+;MOD] is \"underpowered\" and Kₜ[#] is a \"much better\" lower bound because of the example of Dyck-1, which is relevant for practical applications, and because FOC[+;MOD] translates to 2-layer transformers whereas Kₜ[#] translates to deeper transformers.\n\n- FOM[BIT] ([Merrill and Sabharwal 2023]) is likely a much looser upper bound than Kₜ[#]. For instance, integer multiplication is in FOM[BIT], but transformers are observed to struggle with it ([Dziri et al 2023]), and it does not seem definable in Kₜ[#].\n\n- B-RASP ([Angluin et al 2023]) cannot express Dyck-1, but Kₜ[#] can. On the other hand, FO[<] can express Σ\\*aaΣ\\*, which we suspect Kₜ[#] and SMATs can't without positional encodings. \n\n# Answers to questions:\n\n1. We agree UHAT languages are likely a subset of AHAT and SMAT languages. To our knowledge, this has not been shown (we hope to in future work). However, the relationship between AHAT and SMAT is not clear: SMATs have nonuniform attention, but AHATs have \"winner-take-all\" behavior, suggesting AHATs may recognize a language SMATs can't, or vice versa. We know of no examples, but note that all published proofs that transformers with chain-of-thought are Turing-complete (https://arxiv.org/abs/1901.03429, https://arxiv.org/abs/2006.09286, https://arxiv.org/abs/2310.07923) use average-hard attention.\n\n2. On FOC[+;MOD], please see above.\n\n3. Regarding size, we'll note in the final version the formula will have depth O(L) for L attention layers (even with multiple heads), and width $O((2^F)^d)$ in the precision F and width d of the transformer. \n\n[Angluin et al 2023]: https://arxiv.org/abs/2310.13897\n[Barcelo et al 2024]: https://arxiv.org/abs/2310.03817\n[Dziri et al 2023]: https://arxiv.org/abs/2305.18654\n[Merrill and Sabharwal 2023]: https://arxiv.org/abs/2210.02671", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "- This paper is written very clearly for the most part, and I enjoyed reading it.\n- I think Kt[#] could be a useful logic for thinking about softmax transformers. Kt[#] brings together several ideas from prior work: counting logics (used by Chiang et al., 2023; Merrill and Sabharwal, 2023) and temporal logics (used by Angluin et al., 2023; Barcelo ́ et al., 2024), and authors also connect it to RASP (Weiss et al., 2021). I find this to be a nice and intuitive formalism for thinking about transformers: temporal logics are a natural way of thinking about operations on strings, and incorporating counting makes them more expressive and better aligned with soft attention/hard averaging attention transformers.\n- I also appreciate that the paper provides explicit feed-forward constructions for the unary predicates in the logic. Compared to RASP/Tracr, this means all expressions can be compiled into a standard transformer, and it also makes it possible to give upper bounds on the number of layers.\n- The paper gives a tighter lower bound for soft attention transformers.\n\nOverall, despite some reservations (see below), I think the paper is clearly written and introduces an interesting and potentially useful set of tools, and I would recommend accepting it.", "reasons_to_reject": "- 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.\n- 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. \n- 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.\n\nTo summarize, my main concerns are related to how the contributions are framed relative to prior work. \nWhile 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_to_authors": "- 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?\n- 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.\n- 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?", "extra_scores": {}}, {"review_id": "02jj7Td3Ms", "reviewer": "Reviewer_d2M3", "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$[#].", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your positive review! We will try to make the final version of the paper more accessible to a broader CoLM audience.\n\n# Responses to questions:\n\nYes, our results imply that any fixed-precision transformer can be converted to a uniform-attention transformer (albeit a very big one); in fact, this was already shown by [Chiang et al., 2023]. \n\nTo answer your interesting question, we can specify exactly where the parameters are distributed. The base GPT-2 model has 12 attention layers, 12 heads, and an embedding dimension size of 768, so we can give an idea on how many parameters a uniform-attention transformer needs to be to simulate 4-bit GPT-2 by estimating the number of layers, heads, and embedding dimensions it requires.\n\nNearly all of the overhead comes from needing to preprocess the attention scores so they can be simulated with uniform attention. Essentially, we have to enumerate all $(2^4)^{768}$ possible query vectors, and write predicates to access each bit of each dimension of each vector. Therefore, as a ballpark estimate, $16^{768}\\cdot4\\cdot768$ embedding dimensions get added (this enumeration allows us to simulate all heads with one). \n\nThen, following Theorem 5.7, an upper bound of $4$ blocks are needed to simulate each fixed-precision attention layer. Altogether, we roughly estimate that it would take a transformer with embedding dimension of $16^{768}\\cdot3072$, $48$ single-head attention layers (with query and key weights all zero), and $48$ FFN's with hidden dimension $16^{768}\\cdot3072$ in order to simulate 4-bit GPT-2. \n\n[Chiang et al., 2023]: https://arxiv.org/abs/2301.10743", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "1. The paper makes a solid contribution to the softmax decoder Transformer's lower bound of expressivity. In particular, counting logic is required for a variety of tasks. RASP is known for its inability for seemingly simple addition, and the problem is addressed in this paper.\n\n2. The paper is clear, with abundant examples. The proof in the appendix is also well organized.", "reasons_to_reject": "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_to_authors": "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?", "extra_scores": {}}]

Author rebuttal:

Meta-review: 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.
Decision: Accept