Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages
Authors: Andy Yang
David Chiang
Dana Angluin
Venue: NeurIPS 2024 poster (2024)
Keywords: Transformers
Formal Language Theory
Logic
Automata
Expressivity
Primary area: deep_learning_architectures
TL;DR: We prove masked hard-attention transformers recognize exactly the star-free regular languages.

Abstract: The expressive power of transformers over inputs of unbounded size can be studied through their ability to recognize classes of formal languages. In this paper, we establish exact characterizations of transformers with hard attention (in which all attention is focused on exactly one position) and attention masking (in which each position only attends to positions on one side). With strict masking (each position cannot attend to itself) and without position embeddings, these transformers are expressively equivalent to linear temporal logic (LTL), which defines exactly the star-free languages. A key technique is the use of Boolean RASP as a convenient intermediate language between transformers and LTL. We then take numerous results known for LTL and apply them to transformers, showing how position embeddings, strict masking, and depth all increase expressive power.

Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages
Andy Yang University of Notre Dame
David Chiang University of Notre Dame
Dana Angluin Yale University
Abstract
The expressive power transformers over inputs of unbounded size can be studied through their ability to recognize classes of formal languages. In this paper, we establish exact characterizations of transformers with hard attention (in which all attention is focused on exactly one position) and attention masking (in which each position only attends to positions on one side). With strict masking (each position cannot attend to itself) and without position embeddings, these transformers are expressively equivalent linear temporal logic (LTL.), which defines exactly the star-free languages. A key technique is the use of Boolean RASP as convenient intermediate language between transformers and LTL. We then take numerous results known for LTL and apply them transformers, showing how position embeddings, strict masking, and depth all increase expressive power.
Introduction
Significant progress has been made in the last few years on characterizing the expressivity of transformers (Vaswani al., 2017) in terms of well-understood classes of formal languages (Strobl et al., 2024b). Results have been obtained for wide range variants of transformers, and nearly all take the form of either upper bounds (transformers recognize only languages in class C) or lower bounds (transformers recognize all languages in class C). In this paper, we establish exact characterizations of transformers with hard attention (in which all attention is focused exactly one position) and attention masking (in which each position only attends to positions on one side of i).
With strict masking (in which each position cannot attend to itself) and without position embeddings, these transformers recognize exactly the class of star-free regular languages. The left side of Figure summarizes results relating masked hard-attention transformers and linear temporal logic (LTL), which defines exactly the star-free regular languages.
key technique in these proofs is the use of B-RASP, which, like RASP (Weiss et al., 2021), is small programming language that compiles into transformers. B-RASP is restricted Boolean values and compiles to masked hard-attention transformers. Additionally, masked hard-attention transformer can be decompiled back B-RASP program. We use B-RASP as an intermediate language between transformers and LTL.
The equivalence of masked hard-attention transformers with LTL (and other equivalent characteriza- tions, like counter-free automata and first-order logic) enables us to take numerous results known for LTL and apply them transformers, shown the right side of Figure
Strict future-masked masked rightmost-hard attention is sufficient; adding past-masked, non non-masked, and/or leftmost-han hard attention does not increase expressivity (Section 5.1).
Strict masking is important (Section 5.2); without it, masked hurd-attention transformers less expressive, recognizing only the stutter- inviriaann star-free languages.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

masked hard-attention transformers
finite-
image PEs
rational
$5.3
sinusoidal PEs / strict future- masking
$3.4
$4.2
striet future- and past- masking
$5.1
LTL B-RASP
$5.2
depth
nonstrict masking
$5.4
depth
depth
Figure I: Overview of results in this paper. One-way arrows denote strict inclusion; two-way arrows denote equivalence. PE = position embedding.
Adding position embeddings increases the class recognized languages to other well- studied classes (Section 5.3); for example:
With rational sinusoidal position embeddings, masked hard-attention transformers recognize exactly the regular languages in AC
With arbitrary finite-image position embeddings, they equivalent to LTL[Mon] (linear temporal logic with arbitrary monadic predicates).
Adding more layers always increases expressive power (Section 5.4).
Background
2.1 Preliminaries
Let Σ be a finite alphabet, and let w = wi... Wr be an input string of length n, where each E E. Throughout, we assume that (We disallow empty strings because several formalisms used here require a designated position where an accept/reeect decision appears. Adding possible to handle the empty string.) We write [n] for the set (1....,
empty. We write Σ* for the
all non-empty strings over
or EOS token not in Σ for this purpose would make
The star-free regular languages the closure of 0, (E), and (or for each e E, under the operations of union, concatenation, and complementation. For example:
Σx is star-free because E' - (ab)" is star-free because (ab)* (bE' U'' O'
(aa)* is regular but star-free.
This class of languages has several other characterizations. including counter-fre free automata (Ap- pendix B.5), first-order logic with order (McNaughton and Papert, 1971), and linear temporal logic (Kamp, 1968), which is what we will focus on in this paper.
2.2 Transformer variants
The original transformer (Vaswani al., 2017), designed for machine translation, had both an encoder and decoder. In practice, both encoder-only models like BERT (Devlin et al., 2019) and decoder- only models like GPT (Brown et al., 2020) are common. Like much previous work on transformer expressivity (e.g. Hahn, 2020), we study encoder-only setup, where the input is a string and the output is binary classification; but our results could easily be adapted to decoder-only setting where the input is prefix and the output is the next symbol.

---

The transformers studied here use unique hard attention (or simply hard attention). in which an attention head focuses all attention on the position with the highest score, with ties broken the left or right. Although this is different from the soft attention in actual transformers, theoretical studies unavoidably involve models of the real objects of study, and we are using unique-hard attention as stepping-ston stoppinng-sooeeeeeee towards understanding real transformers. However, unique- haique-hard attention may be more appropriate than appears:
Real transformers often observed to focus attention very small number of positions (Merrill et al., 2021). On Dyck languages, they have been found to learn effectively unique- hard attention in their second layer (Ebrahimi et al., 2020, Figure 1).
There exist soft-attention transformers that compute parity (Chiang and Cholak, 2022), but in practice, transformers cannot learn parity (Bhattamishra et al., 2020). Unique-hard attention transformers also cannot compute parity (Hahn, 2020), so they are in some sense more realistic.
Hard attention has occasionally been used in practice in previous research on interpretability (Kinley, 2020) and efficiency (Gupta et al., 2021; Xu et al., 2021).
In this paper, we use future masking, in which every position may only attend to positions to its left. This kind of masking is common in decoder-only models and has been studied in encoder-only models as well (Bhattamishra et al., 2020). We also consider past masking (Yao et al., 2021).
2.3 Previous work
Pérez et al. (2021) show that average-hare attention transformer runs for a polynomial number of steps before accepting or rejecting string, recognize all of (that is, all languages decidable by deterministic Turing machine in polynomial time). Merrill and Sabharwal (2024) prove another version of this result, and further observe that all such transformers are in P. This result is the only other exact characterization of any transformer variant that we are aware of.
where the decoder
Hao et al. (2022) show that (non- masnem hard-attention transformer encoders with arbitrary position embeddings have an upper bound of AC (that is. languages defined by circuit families with polyno- mial size, unbounded fan-in, and bounded depth), and Barceló al. (2024) show that they have lower bound of LTL [Mon]. which is linear temporal logic with all possible monadic numerical pred- icates. They leave open the question of whether these transformers are equivalent to [To[Mon]- question which, with suitable adjustments, we answer here in the affirmative.
3 Boolean RASP
RASP (Weiss et al., 2021) a programming language intended to help programmers "think like transformers." It has the same basic operations as transformers, but it is casier to compose these operations in RASP than to write transformers by hand. Variants of RASP have been used fruitfully to study transformers'
oongtt-generalizztion capabilities (Zhou et al., 2024) and expressive power (Strobl et al., 2024a; Yang and Chiang, 2024). In this section, we define a version of RASP restricted to Boolean values, which we call Boolean RASP B-RASP. As will see, it can be compiled into masked hard-attention transformers, and masked hard-attention transformers can be decompiled back into B-RASP. We use it as intermediate language between transformers and LTL, and find it more convenient to work with than either of them.
3.1 Definition
The input B-RASP program is string = ...., W E vector, which is a vector of Boolean values indexed by i E [n]. The initial Boolean vectors are Q for each o E Σ, where (i) iff w;
Σt. There is one type of data, Boolean
B-RASP program is sequence of operations that compute new Boolean vectors. Although they may have descriptive names, and names may be reused, here, to streamline definitions and proofs, we assume that all the Boolean vectors are numbered consecutively. That is, Pl...., Plzi are the initial Boolean vectors Qo for E E, and the Boolean vectors computed by the program are numbered
3

---

imput
imput
rr
cerret
Qr
0
Qr
Q
0
1
0
Qr
0
Pr
0
0
Pe
1 0
1
1
0
S
0
0
S
1
0
0
0
1
0
1 0
0
0
0
1
0
Bt
0
0
0
Ay
0
A,
1 0
Y
Y
O
0
(a) DFA
recognizing
(b) Boolean vectors for membership of string (Errttrlrr in L1,2-
(c) Boolean vectors for non-membership of string Errltlrerl in L,,-
L1,--
Figure 2: Examples related to /-1,2 (Dyck-1 of depth 2). The left bracket is and the right bracket r.
starting from PJE|+1 without repetition. After the first vectors, vector Pr+1 computed using one of the following operations.
Position-wise operations. (r) can be be computed by (r+1(1) == R(1), where R(i) is a Boolean combination of zero more of (Pi(i)..... P,))).
Attention operations. (i) be computed by either of
Pr+1 ((t.) V(i,f) D(i) Pi+1(1) == (M(..)) V(i.)) D(1)
where:
Mi. f), the mask predicate, is one of Mi,,)) (no masking), M(i.)) (j < i) (strict future masking), or (i. j) = (j > i) (strict past masking).
S(i,j), the score predicate, a Boolean combination of zero or more atomic formulas from (P.())....,P((i)) (P)()))))))))))).....))))))))))) (j)).
V(i, f), the value predicate, has the same form as the predicate.
D(),, the default value predicate, is Boolean combination of zero more atomic formulas from (i)......PP.
For each [n], let ji be the minimum (if the operator is 4) maximum (if P) value j E [n] such that M(i.)) j) and S(i, f) = 1. If exists, then P (f) V(i, fi). If ji does not exist, then (i) (().
If P is Boolean vector computed by program P, we write w ł P(t) just in case P(i) when is run on input string w. To make a B-RASP program P recognize a language, one Boolean vector Y is designated the output vector, and position input string w accepted iff } Y()). To make a B-RASP program compute a length-preserving requence-to-seqeene function from Σ to 1*. we designate collection of output Boolean vectors Yy indexed by the symbols E r, and consider the output at position to be iff (1 is true.
designated the output position. Then, the
3.2 Example: Dyck-1 of depth 2
As example, consider the Dyck language with pair of parentheses, limited depth or L for short. It recognized by the DFA in Figure 2a, where and r are left and right brackets. We show how to define this language in B-RASP, with construction very similar that of Yao et al. (2021).
Consider input string llrrlErlrr, which should be accepted. The basie idea is to identify brackets that are immediately matched (ECrrlfrErr), then look at the remaining brackets (Elrrtlrérz) to make sure they are matched. We describe the B-RASP program for this problem below; the resulting Boolean vectors are shown in Figure 2b.

---

We first construct Boolean vectors (i( and (i) that indicate whether the predecessor (respectively, successor) symbol of is (respectively, r). This is done with attention operations:
Pε(1) , [] < 2c(): S,(1) , [j > 11 2-() :0
Vector (i) makes position attend to the position immediately to its left, and its value predicate Qc(j) tests whether that position has an é. Vector S, is similar.
The Boolean vector ((i) indicates whether position is in consecutive pair (r, that is, whether is immediately matched:
((1) = (2r(0 A, (
The Boolean vectors (i) and (i) test if the symbol before (respectively, after) i that is not immediately matched is & (respectively, r). Then C checks each position to see if immediately matched, or it has l and the following not po--immediately-mateee preceding aed-immmeiately matched symbol is t:
symbol is т, or it has r and the
By(1) := , (i<i,--()) Qc()):0
A,(1) == .,(>>i.-1() :
C(I) := I(1) (Qr()) A,00) (2,() A Bc()).
Finally, the output Boolean vector y tests if C(i) is true everywhere:
Y(i) = -C. 0:
Boolean vectors for deciding non-membership of Errlllrrrl in L1,2 are shown in Figure 2c. is straightforward to generalize this technique to recognize Dyck-k depth D in B-RASP. For another example program for associative recall task, please Appendix A. A B-RASP simulator that allows one to write and run additional examples can be found at https: //bp:ss////rapppp github.oo. io/.
3.3 Normal forms
In B-RASP, the value predicate (i.. depends on both (the query position) and (the key/value position), but in actual transformers, it depends on j only. The dependence on is sometimes convenient, but it does not change expressivity (see Appendix B.1).
The score predicate S(i.) j) depends both and j in both B-RASP and actual transformers. Perhaps surprisingly, in B-RASP, it too can be made to depend only on j without reducing expressivity, but as tradeoff the program may become exponentially larger in size (see Appendix B.2).
3.4 Equivalence with linear temporal logic
We prove that B-RASP recognizes exactly the star-free languages, by proving that B-RASP is equivalent to linear temporal logic. Appendix B.5 gives another proof of the Can-free-to-B-RAAS direction via counter-fres automata.
In linear temporal logic or LTL (Kamp, 1968), every formula implicitly depends on single "time" (or position). The atomic formulas are 2.r for every o E Σ, and we have the usual connectives A, V. and as well as operators since and until. 2 For any input string wT ......... w,, and position e [n].
Because we prove in Lemma 21 that B-RASP programs can be simulated by masked hard-attention transformers, this result contradicts the claim in Thearem 4.3 (= Theorem C.1) of the paper by Yao et al. (2021);
according to cognizant co-author of that paper, Lemma C.2 in that paper is not true (Peng, 2023)
Other presentations of LTL may define non-strict operators since' and until' (in which j or can be equal to i) and add previous and next operators. These definitions are expressively equivalent, but the proof' here are more straightforward when defined this way.
5

---

we define w, i F= & follows:
w.i = Qo
w; o if w, F Φi and w,i d22
w, F $1 d/
w. F $1 V 22
w., = or w. F d2
w,i F +
if w. + +1
w,i = Φ since Φ2
for some j < i, we have w. j F d2. and for all k such that j < k < we have w, k F= d1
w,i F Φ1 until 0
for some j > i, we have w. }= d2.
and for all & such that i k < j. we have w, k |= Φ1.
To use formula & of LTL to define language over Σ, for an input string w E Σ* of length n we designate the last position as the output position, so that w [(Φ) if and only if w, n F Φ.
For example, let Σ = {a, b. #) and consider the following formulas:
Φ = Q#
Φ2 Q# A (Ob since 2+)
Φ: = Q* A (Qs since (Q+ (Qa since Qa)))
44 Q* A (Ob since (Q+ (la since (Q+ A -(0 since 1))))).
The formula Φ1 defines the language H, which contains all and only strings with a # in the last position. The formula Φ2 defines the language #b# and Φ3 defines the language #a#a'# Finally, 64 defines the language #a'#b" #, because (0 since 1) is only true at the first position.
Theorem 1. For any formula of LTL that defines language I. S Σt, there is a B-RASP program that recognizes I..
Proof. See Appendix B.3. This is shown via direct construction.
Theorem 2. For any B-RASP program that recognizes a language L C Σ*, there is a formula of LTL that defines L.
Proof. See Appendix B.4. We the unary normal forms (Section 3.3) to facilitate this proof.
4 Masked Hard-Attention Transformers
4.1 Definition
masked hard-attention transformer layer with width d is a length-preserving function
layer: (Rd)) - (Rd)+
(X1...., (y1, (yl...., Vn)
(CI...., Cn) = .x. (x),..., y1 ff(ci) C
(I)
i= I. L
The self-attention layer att is specified by
A score function, which bilinear function fs: Rd x Rd - -R
A mask, which is (i. 1 (no masking), (i. (j (strict future masking), or (ii (i < j) (strict past masking).
A tie-breaking function C to select one element of finite non-empty set c N., which is either C(/) min (choose leftmost position) or C(J) max / (choose rightmost position).
A value function, which is linear transformation fv: Rd Rd
The layer works as follows, for each [n]. Let
U: = [j [m] M(i.))
unmasked positions
= E (Vj' UD(s((x))y)) s fs(x)xx)))
best-scoring unmasked positions

---

If U, * 0, let J, = C(;)) and output = fx(x;;;; but if U, = 0, output e; 0.
The function ffn is feed-forward neural network with 2 layers and ReLU activations in between.
Then masked hard-attention transformer is length-preserving function
T: Σ (R*)+
T layer .... layer, emb
where emb: Σ+ (R4)+ is a position-wise function (a word embedding), and each layer, is masked hard-attention transformer layer.
We write [T()), for the final activation value at position i [n]] when T is run input To use T as a language recognizer, we add an output layer, which linearly projects [T(w)] to a scalar. If the result is nonnegative, we accept w; otherwise, we reject. The exact criterion does not matter much, as the transformers we construct only output + or -3. and could easily be changed to another convention. The language recognized by T (with the output layer) is the set of strings accepts.
Our definition above differs from the standard definition (Vaswani et al., 2017) in a few ways besides unique-hard attention, which was discussed above in Section 2.2. Ours lacks layer normalization and position embeddings, but we add them in Sections 4.3 and 5.3, respectively. We only use single-head attention; multi-hean attention can simulated by summing the outputs of multiple single-head attentions, or it can be added to the definition, in Appendix D.3.1. Our attention masking is strict, but we consider non-strict masking in Section 5.2.
4.2 Equivalence with B-RASP
Theorem 3. For any B-RASP program that recognizes language L S Σt, there is masked hard-attention transformer (with output layer) that recognizes
Proof. See Appendix C.I. Attention layers simulate attention operations, and FFNs simulate position- wise operations.
Theorem 4. For any masked hard-attention transformer (with output layer) that recognizes language L s Σt, there is B-RASP program that recognizes L.
Proof. See Appendix C.2. To convert masked hard-attention transformer to B-RASP, first show that all of the intermediate values computed by the transformer are drawn from finite set and therefore can be represented using (1) bits."
4.3 Layer normalization
Standard transformers (Vaswani et al., 2017) include layer normalization (Ba et al., 2016), but our definition above does not. Since layer normalization is position-wise function, the proof of Lemma 24 is unaffected. But the construction of Lemma 21 does need to be modified to circumvent layer normalization (cf. Chiang et al., 2023, Proposition 22). Previously, we used I to represent true and 0 to represent false; now, we use pair of activations to represent truth value, (1,0) for true and (0, 1) for false. This ensures that every vector has mean and variance independent of the input w. so we can set the parameters of each layer normalization so that it has no effect. (In the proof of Theorem 3, we use flag to indicate whether there are any unmasked positions or not. This flag already uses the encoding described above, and does not need to be modified.)
5 Further Results
In this final section, leverage results from temporal logic and the equivalences established above to obtain numerous new results for masked hard-attention transformers (and B-RASP).
3 Hao et al. (2022) previously proved that hard-attention transformers use (log n) bits; the difference that they assumed arbitrary position embeddings, but we assume either no position embeddings, or position embeddings with finite image (Section 5.3).
7

---

5.1 Asymmetric attention
Our definitions of both B-RASP and masked Hard-attention transformers include both leftmost-har and rightmost-hard attention, and both future and past masking. But we can use the fact that, in LTL, if the output is read out only at the last position, suffices to have only since and not until (Gabbay et al., 1980) to obtain the following result.
Theorem 5. Both B-RASP and transformers with only future- mature-masked rightmost- hard attention recognize exactly the star-free languages.
Proof. Any star-free language can be defined in LTL using only since (Gabbay et al., 1980), and restricting Theorem 1 to translate from LTL with only since into B-RASP will only use future-masked Therefore, B-RASP with only future-masked > can define any star-free language. Similarly, the translation (Theorem 3) from B-RASP with only future-masked > masked hard-attention transformers only uses sature-mased rightmost-hare attention. Therefore, transformers with only future-masked rightmost-haid hard attention can define any star-free language.
Note that this applies only in a setting where we accept or reject strings by looking at the output at the last position. does not apply to other settings, like transduction (Strobl et al., 2024a).
5.2 Non-strict masking
Our definitions of both B-RASP and masked hard-attention transformers use strict masking, in which position cannot attend to itself. Standard transformers, however, use non-strict masking. We can modify the definitions to use non-strict masking, that is, i S j or j S
Non-strictness is known to reduce expressivity in LTL (Peled and Wilke, 1997), so it reduces expressivity in B-RASP and masked hard-attention transformers as well. Intuitively, non-strict masked operations are unable to distinguish between consecutive positions that have the same symbol. More formally, a language over Σ is called stutter-invariant iff for all u, V E E" and Σ, uov iff nv E L. An example of language that is stutter-invarien star-free is (a*b")' (where o+ means "one or more occurrences of o)"); a language that is star-free but not stutter- -uvterrinvariint is (ab)*.
Theorem 6. Both B-RASP and masked hard-attention transformers with only non-strict masking recognize exactly the stutter-invariant star-free languages.
Proof. Peled and Wilke (1997) prove that LTL with non-strict since' and until' recognizes exactly the stutter-invarian star-free languages. The proofs of Theorems and 2 may be adapted to use non-strict temporal operators and non-strict masking. Thus, non-strict B-RASP and non-strict LTL are equivalent. Similarly, using j S or j 2 as M (i, j) in the proofs of Theorems 3 and 4, we can show that non-strict masked hard-attention transformers are equivalent to non-strict B-RASP.
In Section 3.2, we showed how to define 2 Dyck-1 of depth 2. Bhattamishra et al. (2020, $7.1) find experimentally that L1,2 is not learnable by transformers, and they argue that is not even expressible by transformers (with soft attention, non-strict masking, and no position embeddings). The reason is that while reading the prefix of l's at the start of the string, the soft-attention layer computes the same value vector at every position and cannot count the number of occurrences of f. However, with the addition of BOS symbol, soft attention can measure what fraction of symbols are f, overcoming this limitation as observed empirically by Ebrahimi et al. (2020). The similarities between how strict masking in the hard attention setting and the addition of BOS in soft attention both enable positions to be distinguished are notable for future investigation.
5.3 Position embeddings
Our definition of transformer does not, so far, include position embeddings; all information about ordering comes from attention masking. A position embedding is a family of functions e = (#m)220 where (,()) is scalar or vector representation of position i in string of length n. Then the input layer emb becomes the sum of a word embedding and a position embedding.
We say that θ has finite image if Unzo Im 0, is finite. In general, our results extend to transformers with any position embedding that has finite image. The class of languages recognized may grow, and we give a recipe for characterizing the new class of languages.
We thank reviewer of previous version of this paper for directing to the notion of
8

---

We can add numerical predicates to LTL and initial Boolean vectors to B-RASP as follows, Let (Tp) be family of functions xn [n] (0. Then there an additional predicate symbol II such that for any string with length ST,
= (1) iff (1) =1
in B-RASP
w. = (1) =1
in LTL.
For example, Mid,, is true iff n odd and [n/2], then we can define the language ##a"**""# 2 0) in [TL[Mid] as:
Q+ A (Oo since (Mid A Qa (Qa since (Q#A A(0 since 1))))).
A similar definition could be written in B-RASP[Mid].
Theorem 7. Let (0n)n20 be a position embedding with finite image. There exists a collection of predicates Pe such that the following classes of languages are the same:
languages recognized by masked hard-attention transformers with position embedding
languages defined by B-RASP[Pa]
languages defined by LTL[Pe].
Proof. See Appendix D.1.
We discuss two important special cases below.
Sinusoidal position embeddings The original transformer (Vaswani et al., 2017) used position embeddings with coordinates of the form f2n cos cos(2x If the f's are rational (though in the original definition they were not), then the position embeddings form finite set, so Lemma 22 still holds. For any even let us define a rational sinusoidal positional embedding with d dimensions to be position embedding Q (0n)n20 where
,, = [sin 2nt fíi cos 2nt fii
sin 2n fajzi cos 2n fa12]"
f1..... E &Q.
Corollary 8. Masked hard-atter attention transformers with rational sinusoidal position embeddings recognize exuctly the regular languages in AC (that is, regular languages definable by a family of Boolean circuits with polynomial size and constant depth).
Proof. This uses the fact that the regular languages in AC are exactly the languages definable in first-order logic with modular predicates (Barrington et al., 1992). See Appendix D.2 for details. c
An example of language that belongs to this class but is not star-free is (aa)". The classic example of language that is regular but not in AC is PARITY (w ba, has an odd number of b b's) (Furst et al., 1984).
Arbitrary position embeddings Finally, we may consider arbitrary position embeddings, subject to the condition of finite image. The corresponding collection of predicates is the set of all possible monadic predicates, which we call Mon.
Corollary 9. Masked hard-attention transformers that have position embeddings with finite image recognize exactly the languages definable in LTL[Mon]
Вarceló al. (2024) show that any language definable [TL[Mon] can be recognized by hard- attention transformer without attention masking and with some position embedding (with infinite image), but left the other direction as an open question. Here, by making use of attention masking and restricting position embeddings to those with finite image, we have obtained an exact characterization.
The addition of attention masking appears be important. With finite image position embeddings but without attention masking, there must be two positions i and j with the same position embedding (by the pigeonhole principle), so an unmasked attention transformer would one string with a and b at positions i and j and another string with a and b at positions j and i. So no masked hard-attention transformer with finite image position embeddings and unmasked attention can recognize the language #a #b* #, but we showed already how to define this language even in LTL.
be able distinguish
5 AAthoogh Barrington et al. (2005) define Mon to be the collection of all monadic predicates without dependence other authors (Hao et al., 2022: Barceló et al., 2024) do allow them to depend

---

5.4 Depth hierarchy
Finally, we establish that (unlike with feed-forward networks), we can always increase expressive power of masked hard-attention transformers by adding more self-attention layers. We consider masked hard-attention transformers with only future masking (as typical in practice) and with only hightmost-hart attention. Other masking and tie-breaking schemes treated in Appendix D.3. We also add multi-head attention (as is typical in practice).
First, we define depth for all models in this paper. The layer depth of a masked hard-attention transformer the number of attention layers. The temporal depth of LTL formula is as follows:
d = dp(-6) = dp(
dp(á v)) dp( v v)) = max
dp(ń since v) = dp( until v)) max(dp( +
The attention depth of a B-RASP expression is defined as follows:
(p) =0 dp(-P(0) = dp()(i))
(1(P) P2(0) (1) P2(1) mmx (d))
We then extend this definition to B-RASP operations. P()) == d(i) (a position-wise operation),
dp(P()) = dp()(i)).
If P() == (M..).. v(..): D() or P(i) == a [M f). S(. v(i.)) D(), (()) max j)). dp(V(i. (ppp)))dddpp((() (p))()))) + 1.
Finally, the attention depth of program is the maximum of the attention depths of all of its operations.
Let MUHAT F)x (respectively, B-RASP ()x)) be the languages recognizable by multi-head transformers of depth k (respectively, B-RASP programs of depth k) using only future-masked rightmost-hare attention. Let (since)) be the languages definable by LTL formulas of depth without until.
Theorem 10. For every k 2 O, there is a language Lx+1 such that no multi-head masked hard- attention transformer of depth recognizes Lg, but a transformer of depth (k+1) 1) does recognize LK+1-
Proof. The constructions in the proofs of Theorems and 2 preserve depth, so B-RASP ( F)x (sincin Moreover, by Theorem 4 (shallower version in Appendix C.2), and by Theorem 27 (a depth-preserving version Theorem found in Appendix D.3), MUHAT( F)x = (--RASP( Finally, Etessami and Wilke (2000) prove that (sinee) ç LTL(since):s K+1- Namely, the classes are separated by LK+1 STAIR which is the language over Σ = {a, b, c} of strings which, after deleting c's, contain a k+1 as substring. This gives the following picture:
S (in(cc) ç LTince))) S...
B-RASP - F)k
B-RASP( - F)
MUHAT F)k
MUHAT( F)
Therefore, MUHAT( Ç MUHAT( F)
6 Limitations
This work focuses exclusively on masked hard-attention transformers. We discussed the rationale for hard attention in Section 2.2. These results do not apply to softmax-attenntion transformers, although they demonstrate what kinds of results one might hope to obtain for softmax-attenttin transformers. Nor do they apply to transformers with unmasked attention.
Finally, our restriction of position embeddings to have finite image, and in particular our restriction of sinusoidal position embeddings have angles that are rational multiples of π, does not exactly match the standard definition.
10

---

Acknowledgements
We would like to thank Peter Cholak, Anthony Widjaja Lin, Anand Pillay, and the anonymous reviewers, including the reviewers of previous version of this paper, for their helpful comments.
References
Jimmy Lei Ba, Jamie Ryan Kiros, and Geoffrey E. Hinton. 2016. Layer normalization. In NIPS Deep Learning Symposium.
Pablo Barceló, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir Podolskii. 2024. Logical languages accepted by transformer encoders with hard attention. In Proceedings of the 12th International Conference on Learning Representations (ICLR).
David A. Mix Barrington, Kevin Compton, Howard Straubing, and Denis Thérien. 1992. Regular languages in NC'. Journal of Computer and System Sciences, 44(3):478-49)
David A. Mix Barrington, Neil Immerman, Clemens Lautemann, Nicole Schweikardt, and Denis Thérien. 2005. First-order expressibility of languages with neutral letters or: The Crane Beach conjecture. Journal of Computer and System Sciences, 70(2)101-127.
Satwik Bhattamishra, Kabir Ahuja, and Navin Goyal. 2020. On the ability and limitations of Transformers to recognize formal languages. In Proceedings of the Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 7096-7116.
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chris Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. 2020. Language models are few-shot learners. In Advances in Neural Information Processing Systems 33 (NeurIPS), pages 1877-1901.
David Chiang and Peter Cholak. 2022. Overcoming a theoretical limitation of self-attention. In Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (ACL), pages 7654-7664.
David Chiang, Peter Cholak, and Anand Pillay. 2023. Tighter bounds on the expressivity of trans- former encoders. Proceedings of the 40th International Conference on Muchine Learning (ICML), pages 5544-5562.
Jacob Devlin, Ming- Wei Chang, Kenton Lee, and Kristina Toutanova. 2019. BERT: Pre-training of deep bidirectional Transformers for language understanding. In Proceedings of the Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (NAACI. HITT), pages 4171-4186.
Javid Ebrahimi, Dhruv Gelda, and Wei Zhang. 2020. How can self-attention networks recognize Dyck-n languages? In Findings of the Association for Computational Linguistics: EMNLP 2020, pages 4301-4306.
Kousha Etessami and Thomas Wilke. 2000. An until hierarchy and other applications of an Ehrenfeucht--Fraissé game for temporal logic. Information and Computation, 160(1-2):88-108.
Dan Friedman, Alexander Wettig, and Danqi Chen. 2023. Learning Transformer programs. In Advances in Neural Information Processing Systems 36 (NeurIPS).
Merrick Furst, James Saxe, and Michael Sipser. 1984. Parity, eircuits, and the polynomial-tnn time hierarchy. Mathematical Systems Theory, 17:13-27.
Dov Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. 1980. On the temporal analysis of fairness. In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 163-173.

---

Ankit Gupta, Guy Dar. Shaya Goodman, David Ciprut, and Jonathan Berant. 2021. Memory-efficcte efficient transformers via top-k attention. In Proceedings of the Second Workshop on Simple and Efficient Natural Language Processing, pages 39-52.
Michael Hahn. 2020. Theoretical limitations of atff-attention in neural sequence models. Transactions of the Association for Computational Linguistics, 8:156-171 171.
Yiding Hao, Dana Angluin, and Robert Frank. 2022. Formal language recognition by hard atten- tion Transformers: Perspectives from circuit complexity. Transactions of the Association for Computational Linguisties, 10:800-814
Johan Anthony Willem Kamp. 1968. Tense Logic and the Theory of Linear Order. Ph.D, thesis, University of California, Los Angeles.
Jambay Kinley. 2020. Two-Stream Transformer Architecture With Discrete Attention for Better Interpretrability and Separation of Model Concerns. Bachelor's thesis, Harvard College.
Oded Maler. 2010. On the Krohn-Rhodes cascaded decomposition theorem. In Time for Verification: Essays in Memory of Amir Prueli, pages 260-278. Springer.
Robert McNaughton and Seymour Papert. 1971. Counter-Free Automata. Number 65 in M.I.T. Press Research Monographs. The M.I.T, Press.
William Merrill, Vivek Ramanujan, Yoav Goldberg, Roy Schwartz, and Noah A. Smith. 2021, Effects of parameter norm growth during transformer training: Inductive bias from gradient descent. In Proceedings of the Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 1766-1781.
William Merrill and Ashish Sabharwal. 2024. The expressive power of transformers with chain of thought. Proceedings of the 12th International Conference on Learning Representations (ICLR).
Catherine Olsson, Nelson Elhage, Neel Nanda, Nicholas Joseph, Nova DasSarma, Tom Henighan, Ben Mann, Amanda Askell, Yuntao Bai, Anna Chen, Tom Conerly, Dawn Drain, Deep Ganguli, Zac Hladield-Dodds, Danny Hernandez, Scott Johnston, Andy Jones, Jackson Kernion, Liane Lovitt, Kamal Ndousse, Dario Amodei, Tom Brown, Jack Clark, Jared Kaplan, Sam McCandlish, and Chris Olah. 2022. In-context learning and induction heads. arXiv:2209.1 1895..
Doron Peled and Thomas Wilke. 1997. Coutter-invarian temporal properties are expressible without the next-time operator. Information Processing Letters, 63(5):243.246.
Binghui Peng. 2023. Personal communication.
Jorge Pérez, Pablo Barceló, and Javier Marinkovic. 2021. Attention is Turing-complete. Journal of Machine Learning Research, 22:75:1-75:35.
M. Schützenberger.. 1965. On finite monoids having only trivial subgroups. Information and Control, 1(2):190-194.
Lena Strobl, Dana Angluin, David Chiang, Jonathan Rawski, and Ashish Sabharwal. 2024a. Trans- formers as transducers. arXiv:2404.02044.
Lena Strobl, William Merrill, Gail Weiss, David Chiang, and Dana Angluin. 2024b. What formal languages can transformers express? A survey. Transactions of the Association for Computational Linguistics, 12:543-561.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. In Advances in Neural Information Processing Systems 30 (NIPS).
Gail Weiss, Yoav Goldberg, and Eran Yahav. 2021. Thinking like Transformers. In Proceedings of the 38th International Conference on Machine Learning (ICML), pages 11080-11090.
Hongfei Xu, Qiuhui Liu, Josef van Genabith, and Deyi Xiong. 2021. Learning hard retrieval decoder attention for Transformers. In Findings of the Association for Computational Linguisties: EMNLP, pages 779-785.
12

---

Andy Yang and David Chiang. 2024. Counting like transformers: Compiling temporal counting logic into softmax transformers. In Proceedings of the Conference on Language Modeling (CoLM).
Shunyu Yao, Binghui Peng, Christos Papadimitriou, and Karthik Narasimhan. 2021, 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 (ACL-IJCNLP), pages 3770-3785.
Hattie Zhou, Arwen Bradley, Etai Littwin, Noam Razin, Omid Saremi, Josh Susskind, Samy Ben- gio, and Preetum Nakkiran. 2024, What algorithms can Transformers learn? A study in length generalization, In Proceedings of the 12th International Conference on Learning Representations (ICLR).
13

---

A Additional B-RASP Example: Associative Recall
We consider a variation of the simple associative recall task studied by Friedman et al. (2023) and many others in connection with induction heads and in-context learning (Olsson al., 2022). Inputs are strings over the alphabet {a, b..b 1, 2.).3) where letters and numbers alternate, starting with letter and ending with a number, for example symbol ?. The desired output sequence copies the letters, and for number at position i, if or is the letter at position - 1, then the most recent previous occurrence of o is found, say at position j. and the number at position 1 is output. If there is previous occurrence of then ? is output instead. For the given example input w, the output should be y = a.bbbba3c?aacl.
u.32bb 1022baa2cla/3... The output alphabet adds the
The Boolean vector Pa determines whether there is an a in the preceding position. Similarly, the Boolean vectors Pb and Pe indicate whether there is b or e, respectively, the preceding position:
Pa(i) ; [i < < 1] :
Pы(1) > < @x()) :
P.(0) 1 [1]] Q-()) :0.
The program has an output Boolean vector Y, for each symbol o E Σ indicating whether the output symbol is σ. For a E (1,2.3), if position is preceded by letter, the output Boolean vector Yor attends to the most recent position j preceded by the same letter (if any), and returns the value of Q (J) for that
(/()) >; ; /J i (Pa(1) A PA()) (Pb() P&O)) V (P&() P.OM 2:():0
Y2(1) > (i A Pa()) (Ps() PAO)) V (Pa() A P.OM) :0
Yi( = ((,(() A Pa(D) (P&() P&O)) v (P:() P.O)) 2x():
For E ba, the output Boolean vector Y,- is just Qo:
Ya(1) = Qa(1)
(,) 2+(i)
Yz(1) := (1).
Finally, the output Boolean vector Y, is true if the position is preceded by letter but number was assigned:
(1( = (Pa()) v Pa()) Pa()) A (1) Y2(1) Ys()).
The Boolean vectors in the computation for the example string w are shown below.
input
b
b
2
3
Qa
1
0
0
0
0
0
0
0
O
0
0
0
0
1
0
1
0
0
0
0
0
0
0
Q.
0
0
0
0
Pa
0
0
0
0
0
Pb
O
0
0
0
0
0
0
0
0
0
P.
0
0
Y1
Y2
O
Ya
0
0
0
0
0
0
Yb
0
1
1
0
Y-
0
Y
0
0
0
0
output
a
b
b
a
C
2
14

---

B Proofs for Section 3 (Boolean RASP)
B.1 Unary value predicate
Proposition 11. Every B-RASP program is equivalent to one in which all value predicates V(i, ji depend only on j.
Proof. This can be seen by the fact that the simulation of since/until (Appendix B.3) does not use value predicate that depends on i, but we can show this more directly by induction on the structure of V(i.)) We only show how to handle >; the case of is very similar.
Consider an attention operation with the form
P(i) [M(i..) S(. v(i.): D()).
The base cases are V(i, () B(),, for some Boolean vector B, which already has the desired form, and v(i. B()), in which case P is equivalent to
A(i) J [M (,, S(i, 1:0 P() = (A(1) B()) v (-A(1) D(i).
= = Vi(.,) A V2(i. f), then P(i) is equivalent to
A(I) == ((,, 1:0 Ci(f) > S(i, Vi(i,)) :0
C2(1) == ,, (M... V2(i.)) :0
P(t) == (A(O) A Ci()) A C2()) (-A(i) A D()).
Similarly for disjunction and negation.
B.2 Unary score predicate
Lemma 12. Every B-RASP program is equivalent one in which all score predicates S(i. j) depend only on j.
Proof. Again, we only show the case of as the case of is very similar. Consider a B-RASP attention operation P.
P()) == ((i,.). v() D(i).
Observe that
= f(a()),
(1), Bi(). BIn
where f some Boolean function, and the A, and B, are B-RASP operations. Let {AI...., Ara ). and for each S A, define an assignment of truth values to the A,
A, E
A
0 A
and use it to define unary score (x) which uses the truth assignment x plugged into the A₁:
s*()= f(A AY. Bi B1().... Br, ()).
Now, P(i) is equivalent to Pi),,, where:
px(1) = ,, (M(..) S* (DI v()) D()
for each A
P'() V P A (A,() A
REA
SE(Tx]
To see why, observe that for any i, there is exactly one truth assignment Xi that satisfies Are(Ta) (Ar(1) + A²). This Xi also makes 5ii (j) equivalent to S(i, j), and pxi(f) equivalent to P()).
Note that each attention operation translates into as many TT operations.
15

---

B.3 Proof of Theorem 1 (LTL to B-RASP)
Theorem follows from the following lemma.
Lemma 13. For any formula of LTL, there is B-RASP program with Boolean vector a such for any input w of length n and all E [n]. we have w. iff Po(i).
Proof. By induction on the structure of the formula Φ. We assume that B-RASP program always contains the initial Boolean vectors 2 for E.
Φ = e Add operation
Po(1)= = Q))
If = - By the induction hypothesis, convert Φ1 to B-RASP operations, including one that computes P Poi Then add the operation
P :00==-P0
If o Φ1 A 62: By the induction hypothesis, convert Φ1 to B-RASP operations, including one that computes P then convert d2 B-RASP operations, including that computes P ww- Then add operation
(i( P Po.
If é = 61 V 02: Similar, but add
(o(1) = Poi (a) (P
If since 22: Similar, but add
P : p=(0==>(i<<i.Pa,000
Po)
6 = Φ1 until o Similar, but add
P Po(i) 4, ( (i) P., (.)
B.4 Proof of Theorem 2 (B-RASP to L.T.)
Theorem follows from the following lemma.
Lemma 14. For any Boolean vector P of B-RASP program there a formula & LTL such that for any input w of length n and all E [n], we have w - P() iff w,i i dp.
Proof. First, by Lemma 12 and Proposition 11 we can rewrite p to an equivalent program such that every attention operation only uses unary scores and unary values.
Each initial Boolean vector Q (i) translates to the atomic formula Q
For each operation (i()) (for t [E], if is position- operation, that is,
= (....)......
where f is Boolean function, then by the inductive hypothesis, there are LTL formulas &, for each P, ()). Then convert (i) into 6, f(d1...... 1)))
If (i) is an attention operation, define
exists d since d exists, & = until Φ
also known as eventually
exists ø (exists +) V d (exists> +)
rightmost & = & -(exists> 6).
If P, (i) and future masking, that is,
Pr(1) , Lf < <i.(() vO) D()
16

---

then by the inductive hypothesis, there are LTL formulas Øs. Øv and ØD for the corresponding B-RASP operations. Then we can convert (i( into the LTL formula
Φ ( since (Øs A Φv)) V (-(exists Φ DD).
If (1()) uses and past masking, that is,
, i,S) v(): D()
then
Φ, = (exists> ((rightmost os) A Φv)) V (-(exists, os) A QD).
And if (1) uses
with no masking, that is,
P,(0) = = (1,S0)] V(): (()
then
Φ (exists ((rightmost ds) σv)) (-(exists 6s) A ΦD).
The cases for are symmetric.
B.5 Counter-free automata to B-RASP
In this section, we give alternative proof of Theorem 1 using the fact that the star-free languages are exactly those recognized by counter-free automata.
deterministic finite automaton (DFA) is a tuple A = (Σ, 0), where is the input alphahet, Q is the finite set of states, and 8: QxE Q the transition function. counter-free automaton a DFA in which no string induces a permutation on any subset of Q other than the identity. Schützenberger (1965) proved that the star-free languages are exactly those recognized by counter-free automata.
Theorem 15. For any counter-free DFA that recognizes language Σ*, there is B-RASP program that recognizes L.
counter-free automaton can be decomposed using Krohn-Rhodd theory into cascade of identity- reset automata, each of which can be simulated in B-RASP.
Maler (2010) gives the following automata-theoretic version of the Krohn-Rhodes decomposition theorem, which we explain below.
Theorem 16 (Maler, 2010, Theorem 3). For every [deterministic finite] automaton A there exists cascade decomposition
C o..... Bk
such that the following true.
1. Each Bj is a permutation- automaton.
2. There is a homomorphism & from C to A.
3. Any permutation group in some B, is homomorphic to subgroup of the transformation semigroup of A.
The pair () is called cascade decomposition of A.
If Bi = (1,6) and By = (Q) X 22, are DFAs, their cascade product C B B2 is the automaton (E, Q1 2) such that 5(g142. (ō1 or) 62(22, ()), (To reduce clutter, we write tuples of states without commas.) The cascade product allows the automaton B3 to see the current state of B, in deciding what transition take. We define iterated cascade product inductively Bg. This allows each B, to see the current state of all By with j S in deciding what transition take. (For readers more familiar with finite transducers (Mealy machines), Bj and B, could be thought of as transducers whose transitions are all of the form (g,
by B Bg o ...... Bg (B] o B2 o... ... BB-
Then the cascade product is just composition.)
17

---

2
3
R
Automaton A3: move right (R), move left (L).
B
B,R R
A,
D
B,R
A.L
BD.R
AC.L
BD.R
AC,L
(b) Cascade of identity-resct automata for Ag. Omitted transitions self-loops; for example, inputs A, and self-loops on C and
ACE(O)
BCE(1)
ACF(L)
(2F(2)
L.
L
L
ADE(I)
BDE
ADF(2)
BDF(3)
(c) The global automaton of the cascade product in part (b). For state g, the number in parentheses is state ((g) in Ag.
Figure 3: Example automaton and its cascade decomposition.
In Property (1), permutation-resst automaton is DFA A (E, 2, such that for every E. the mapping q + 5(q. or) is either a permutation (for all r, there is a such that 5(q. o)) = r) or constant (there is ou such that ö(q, .r) or for all q)
Property (2) says that there is mapping & from the states of C to the states such that for any state q of C, we have ((òc(g,o)) = (d)
counter-free, then all of the automata B, in the cascade decomposition are identity-reset automata. An identity-esel automaton is a DFA A = (E, Q, 6) such that for every
Property (3) implies that if the automaton
E. the mapping q - ō(q. or) either the identity (8(g. σ)) = for q) or constant (there is a g such that ō(g. o = q for all q).
For example, consider the automaton A₃ shown in Figure 3a. A decomposition of this automaton into a cascade product of three identity-reset automata is shown in Figure 3b. The global automaton derived from the decomposition is shown in Figure 3e with the homomorphism & to states of A3.
Let (Σ. Q) be DFA and s Q. For string w ..- W,, E Σ' the sequence of states traversed by A from state this input is .0..... .n. where do and for each k, 4&+1 5(g2. wx). A B-RASP program p simulates started state s iff for every input word w Σ', output Boolean vectors of input encode the sequence of states traversed by A from state on input w. The state at position is the state before the symbol at position is read.
Lemma 17. Let = 2,5) be any identity-rese automaton, and let s Q be a start state. There exists a B-RASP program P that simulates B started in state
18

---

Proof. For each state r E Q, let R, C be the state of symbols that reset to r (that is, 6(q, 0) = for all q Q). Let R Ureo R, To determine if B is in state q # before reading w,, it is sufficient to attend to the closest position j < i that contains symbol from R, if any. If exists and wj R then B is in state
position Otherwise, it not.
The case of state is slightly different. In the case that there is no position j < that contains symbol from R. then B never left the initial state s, so it is still in state at position
B-RASP, we can define Boolean vector (1), which is true iff
state q at position i:
j <i, Veou
Vea :0 for q #
(T) ==
oreR
OEE
B,(1) : || jui, Veo()) oeR
1
OrE.
Lemma 18. Let B1 (1) be DFA that can be simulated from state S1 by B-RASP program PB. Let B2 = (Q1 Σ. Q2, 82) be an identity-rssel automaton and let C= By o Bz. Then there is B-RASP program Pc that simulates C started in state (2) for arbitrary $2 Q2.
Proof. Let (i) be predicates that test whether BJ in state q at position started in state st. and let (2.q(i) be predicates that test whether B2 is in state at position started in state (by
Lemma 17). Define
(1) B1,g (1)
q Q1,0
and for every line in the definition of the B2.q. replace every occurrence of Q(q. with Q og This yields the definition of new predicates B'2.g- Then we can define predicates Ciq.r) (7) that test whether C == Bi B2 is in state r) position
Cig.r) (1) (1. (1)
q Q1. Q2.
By induction on k we have the following.
Lemma 19. Let B1 o B2 o ... By be a cascade product such that each B; is an identity-reset automaton, and Si is state of B,. Then there B-RASP program Pc that can simulate from state (81, S2,...,
If we add instructions the program in Lemma 19 that compute the homomorphism & (from property (2) of Theorem 16) from the states of the cascade product C to the automaton A:
(1) = C,
qeQ
$(g)=r
then we get a B-RASP program PA that simulates A started in state s.
Finally, we add to this program position- position-wise operations (i) that decide whether A started in state ends up in state q after reading the symbol position
(,)
(Ag(0)
QEQ
O
8(g.0)
If ff is the final state of A. then let Yy be the output vector of the program. Since (y(n) 1 and only if A accepts w, this completes the proof of Theorem 15.
C Proofs for Section (Masked Hard-Attention Transformers)
C.1 Proof of Theorem (B-RASP to masked hard-attention transformers)
We will make use of the following lemma repeatedly:
19

---

Lemma 20, Any function f: (0, 1) {0, 11 can be computed by a two-layer FFN with ReLU activation functions.
Proof. Any Boolean function can be written in full disjunctive normal form (DNF), which is disjunction of conjunctions, and each conjunction is conjunction of one positive or negative literal for each of the arguments, so that at most one conjunction is for any assignment.
Each component of f can be put into full DNF and computed by two-layer FFN with ReLU activation functions. The first layer computes all the negations and conjunctions, using the fact that for any Boolean values bj, b , bn have
-b
by A bn ReI.U(b) + b2 b2+ + hm - (m - 1))-
The second layer computes the disjunction simply by adding the values of the conjunctions.
Let P be B-RASP program with Boolean vectors Pi..... Pr. We say that masked hard-attention transformer with width simulates iff for every input E* with length n, we have, for all í E [n] and / [7].
[T(w) (
if F= P,(1) otherwise.
Theorem follows from the following lemma: Lemma 21. Let P be a B-RASP program. There exists a masked hard-attention transformer Tp that simulates P.
Proof. We prove that the first operations of p can be simulated by a masked hard-attention transformer, by induction
12,, let or the e-th symbol in E. Let emb( be the The base case is [Σ]. For I...., one-hot vector with [emb(ora)e 1.
For the inductive step, assume that the Boolean vectors Pi...., Pr can be simulated by masked hard-attention transformer. We want to show that Pr+1 can be simulated as well.
If Pre1 (i) is a Boolean combination of Lemma 20.
it can be computed by two-layer FFN by
The most important case is if (1+1(1) is an attention operation, either of (i) == 4 S(..) v(i.)) D() (i) == > S(i..)) v(i.)) D(1.
We only show the case; similar. We need to slightly modify the value predicate:
(ii = (S(i.) A v(i,)) V (-S(i,) A D()).
This does not change the behavior of Pr+1 (because S(i, j) is always true when evaluating the value predicate), but it will preserve the correct behavior leftmost maximum score. By Proposition 11, the attention operation can be rewritten so that that the value predicate depends only on j. So, without loss of generality, assume that there is a Boolean function g such that
transformer, where attention attends to the
(i
The score predicate S(i, f) can be written in full DNF in terms of the Pr( and Pe(j). We separate each conjunction S(i f) into a conjunction of literals depending on and a conjunction literals depending on j. Thus, there is a collection of Boolean functions az and Be such that
S(i,)) = V (O) ((()) A 1=1
20

---

We construct two layers, as follows. For brevity, we write
P((1)
P(()
(i())
(v vr)
(i(VI.....VV)
à aVI......
B(vI..... vz)
(m vy)
Bm (v) vz).
and for any m we write 0 for the m m-ddimensional zero vector.
Assume that the input to the first layer
P())
Boolean vectors already computed
0
Boolean vector be computed
0 7
Boolean vectors not yet computed
0m
0"
scratch space
O
O
The first self-attention has value vectors set to 0, so that the residual connection computes the identity function (c,") = =x; (1)) ), and the first position-wis wiio FFN can be constructed, by Lemma 20, so that
= fp (c()) +c
P())
0
0--111
a(P((). P.(
query
(.),,,...
key
(2)
set default flag to true value
1
(P),,,,,,PPPP.C (D)
In the second layer, the self celf-attention has mask M. The score function is
((2)
(2)
(2)
(2)
W
(2) x
x x
x
((P((i) ..... .....(.)))))
a(PI())....PP.C P.())
(1) ((())),,,,))
f
MEXM
....).....PPOI))
(P) ... P.(0) (c(Pi(O......PCI)))
t=1
= S(i.))
21

---

where maxm and paxo are the m x m zero and identity matrices.
The value function svr is such that for any j [n],
0
O
07 -
1/ (x))))
change default flag false
-1
8(P P.()))
value
So the output of the second self-attention, after the residual connection, is as follows.
If 1:
If 1:
c = (2)
(2)
(2) +x;
0 (2)
P(1)
P(1)
0
07-111
T--11
(1P
P2())
a(P((). P()
(()
P((
((P(()) P,())
default flag (false)
default flag (true)
0
(.()) (PP(()). P,(D))
())
((Pr()...... P,O))
attended-to value
no value
. it copies the attended-to The second feed-forward network f(2 checks the default flag. If is [8]. value 8 (P)) PiOi)) to the 1)+tt coordinate. it [9] it computes ((i) (using Lemma 20) in the (1 1)-st coordinate. Thus, the output after the residual connection is as follows.
If 1:
=:
y (22))( +c²
(2) Ci
y = (2)
(2) C1
cc,
+
P(i) (iP Pc(i)) 7-i-1
P(i)
answer
D())
answer
07-1-1
((P)(). P(())
ā(Pi())
P.(
((P) P(())
((P
P.(
0
1
(1)..)..... .P.,,, ...())
(P), P.())
(fi. P.(I))
0
In either case, the (r + 1) coordinate is now 1 if w F= (r+ and 0 otherwise.
The last step is construct the output layer, which simply projects the final-layer activation vectors down the coordinate that simulates Y and subtracts J. This completes the proof of Theorem 3.
22

---

C.2 Proof of Theorem 4 (masked hard-attention transformers to B-RASP)
The key the translation from masked hard-attention transformers to B-RASP the following lemma:
Lemma 22. Let be masked hard-attention transformer. There a finite set & R such that for all input strings w, all the attention scores and activations computed by T input belong to B.
Proof. We prove that regardless of the input, layer k has at most (|Σ) 1)2* different possible output activation vectors, by induction on k. The base case is just the embedding function. Since there are no position embeddings, the embedding at position is determined entirely by w,, so there
are at most |K| = (1 1)2 possible activation vectors.
Assume that T has (k 1) layers and that layer k has at most ([ 1)2* possible activation vectors. The self-attention's 's output at position depends only on two vectors: (1) layer k's output at position (because of the residual connection) and (2) either layer k's output position ji (the position that attends to) or 0 (if there are no unmasked positions). Thus the number possible activation vectors that the self-attention can output is most
(1 + 1)2* - 11) (| + 1)2* = -(12) + )) - -(1
1)2*
[[Σ] 1)2 - + 1)2*
s (|Σ) + 1)2" -
And the number of possible activation vectors that the position- FFN can output is also at most (|Σ) + 1)22.1
As for the attention scores, at layer (A + 1), every attention score depends on two activation vectors from layer k, there are at most ((|Σ] + 1)2* 1)² s (( + 1)2* possible scores.
Then F the union over all layers of the possible attention scores and components of the possible activation vectors.
So any attention score or component of an activation vector can be represented using B = [log, [F]]
bits. Define mapping (-): F {0, ... 2 1} such that < iff (u) (v), and write (v), for the bit of (v) with place value 2b.
Lemma 23, For any function f: F F, there are Boolean formulas & (x. for b [B] such that for any B, (b((())......... (x) holds iff (f(x)) 1.
Proof. One way to define ds is:
&b (x) (x.....X .B)
Xb
-
XCP
BE([B]
b'E(B] (x))==0
(f(0))
(x))==1
Depending on the mapping (-), more efficient definitions may be possible.
Hopefully, it clear how to generalize this lemma to functions Fd Fd - (0. 1) or Fd - Fdd
Next, we prove Theorem 4. Let T be a masked hard-attention transformer with width d. Let B be the number of bits needed to store T's activation vector components and attention scores, by Lemma 22. A B-RASP program P. simulates T if in P there are Boolean vectors Yo.b for [d] and 0 s b < B such that for any input w E Σ+ of length n, for all i e [n], c [d], and s < B, we have
+ (f) iff ([T(w)l.c)b== Lemma 24. For any masked hard-attention transformer T, there is a B-RASP program Pr that simulates T.
Proof. We proceed by induction on the depth of T. The base case is the input embedding function emb, which is simulated by Boolean vectors for E [d] and 0 s b < B:
Embe,s A (1) ([emb(or) deE
23

---

Assume that the first k layers of T are simulated by program P. We extend p to simulate layer (k + 1) as follows.
the self-attention uses rightmost-hard attention with mask M j), assume (by Lemma 23) that the score function (t, has been converted Boolean expressions Sy (f, for the b-th bit of the score for positions and j, and the value function fv(j) has been converted to Boolean expressions Vi,,(i for the b-bit of the c-th coordinate of the value.
We give two translations. The first version has depth 1, which is important in Section 5.4. The second version deeper in general, but much smaller.
Shallower version:
Because F is finite, by Lemma 23 can define, for all predicates
S, (i. just in case fs.
(i, f) just in case fs >.
Then for each F, add operations for Max, (i), which check that the score v is the maximum, and Rightmost, (f), which retrieve the value at the rightmost position with score v:
[M( (i, 0: Rightmost, v,,b (1) = (,,
Max, (f)
(
Then add operations for (t), which hold just in case the b-th bit of the e-th coordinate of the attention output is I, by taking disjunction over the finitely many possible scores:
(i) = V (M) A Rightmost, (c..)()) veF
Smaller version:
We need to define predicate Argmax(i, j) that tests whether j maximizes S(í. j). To do this, we define a sequence of Boolean vectors that test whether j maximizes bits b.....B of S j):
Argmax y (i.
For = - 1, 2, ... 0:
Max == > [M Argmax (i. A A,DAS,,,))) (1, 1:0
B1-1
Argmax, (i.j) \ (i. Max (i)
6b Argmax(i. j) (i.
Finally, we add operations that simulate attention:
(t) := , [M /). Argmax(i. (c, :0 00
To simulate leftmost-hard attention, simply change to 4.
For the position-wii wise feed-forward network, use Lemma 23.
The last step in the program is to use position-wise operations to simulate T's output layer, yielding an output Boolean vector Y. This completes the proof Theorem 4.
D Proofs for Section 5 (Further Results)
D.1 Proof of Theorem (position embeddings can be simulated by predicates)
Because θ has finite image, Lemma 22 still holds for any masked hard-attention transformer with position embedding O Let Pe be the collection of predicates that test whether the b-th bit of the c-th coordinate of (i) is set. The proof of equivalence of masked hard-attention transformers with B-RASP extends easily to equivalence of masked hard-attention transformers with position embedding O and E-RASP(Pal When converting a transformer to B-RASP program, represent each coordinate transformer, we represent each predicate in Po with its coordinate, whose value {0, 1).
with B predicates from Pg. When converting a B-RASP program
Since Theorems and 2 hold for any collection of unary predicate symbols, B-RASP[Pe] equivalent to LTL[Pe].

---

D.2
Proof of Corollary 8 (masked hard-attention transformers with sinusoidal position embeddings recognize the regular languages in AC
Let MOD be the collection of predicates MOD (i) for all 0 s m. which hold just in case (mod m).
Let @ be sinusoidal positional embedding. Since the fo are rational, O has finite image. By Theorem 7, transformers with positional embedding are equivalent to LTL[Pa].
It's easy to see that every predicate in Pe can be expressed in terms of MOD; for the converse, observe that we can use a 2-layer ReLU network to compute MOD (Chiang al., 2023, Lemma 20):
h() = ReLU (sin 2zr 2ini cos 2 / cos 2ni b cos 2m) MOD
(i)_U((cos(2iiir))/)))))
n (f) = (1 - cos (
Thus transformers with sinusoidal positional embeddings are equivalent to LTL[[OD]] which is equivalent to MOD) (Kamp, 1968), which defines exactly the class of regular languages in AC (Barrington et al., 1992).
D.3
Details for Section 5.4 (depth hierarchy)
D.3.1 Multi-head attention
To prove Theorem 10 and related results, we need to make Theorem 3 more efficient in terms of the depth of the constructed transformer. To do this, we'll need to make use of multi-head attention. This allows multiple self-attentions the same depth to run in parallel. In a multi- head masked hard-attention transformer transformer layer, the equation for the self-attention (Equation (1)) is replaced by
(CI, (CI..... Cn)
at hat.h(i Mo..h(x)........ (xI.....
where each att. is self-attention layer.
is straightforward to extend Theorem 4 to multi-head masked hard-attention transformers, simulat- ing multi-head masked hard-attention transformer of depth & with B-RASP program of depth k. Each head at depth & can be simulated by B-RASP attention operation attention depth k, and their sum be simulated by position-wise operation (Lemma 23).
D.3.2 Parallel composition
The parallelization accomplished by the following construction.
Lemma 25. transformer Ti of depth k with H₁ heads and transformer T2 of depth k2 with H2 heads can be parallet-copposed into transformer Ti @ T2 of depth max(k1, k2) with Hi + -l2 heads such that
T (w))
(Ti + (w) =
[2(w)]
Proof. First, add layers that compute the identity function to the shallower transformer that both have depth max(kı, (k1, k2).
Next, concatenate their word embedding vectors
lmbb (ar) embz(o)
(embr @ emb))
At each level, we compose the self-attentions using multiple heads to simulate them in parallel. For each multi-head self-attention layer all, and allz at the same depth in each transformer, we multiple heads to simulate both alt and atta in parallel. Let att .h.fs be the score function of
25

---

the h-th head of att, and similarly for at.,. att,,h.C, and ath, .tt.h.ff and similarly for atty. Let di d2 and H H1 H2. Construct new ceff-attention layer att atta with
att h. (xyld;+)=))
Ish5 h H1
(ath @ h. (xL. =
[atl. (h- - H1) (sx (xild+ta)
Hi+ s shss
h.
1 1 H1 H1 11+12 +l+sshsp
(all) h.
attz. Hi).M
att
1 h H1
(ath) attz) h.C
attz. HI).C
Hi h H
att (v((x))))) 0ch
1 Hi
(att) @ hll)). =
0di alt2. - H.).
H
For the feed-forward networks fin; and ffn,, create a new network ffn, @ fin with
w0))
bb()
(ff, @ ffff). w(1)
(fn fffz)).b())
ffn.W(l))
[ffzz.b(1)
[mn b(()
(ffn, @ fffn). w(2)
(ff, @ ffn)).((2)
(())
lfng.b(2)
is straightforward to verify the correctness of this construction.
D.3.3 B-RASP masked hard-attention transformers, preserving depth
We give a more efficient version of Theorem which uses parallel composition to optimize the depth of the constructed transformer.
Lemma 26. Let T be a transformer (without output layer) with width d and depth k, and whose activations in {0, }}. For any function g: {0, 1}d - {0, 13d, there is transformer (g 'T) with depth k such that, for all w and i, [[g (w)),; = (([(()))))
Proof. If k = 0: T consists of just an embedding function emb: Σ - {0, 1)d. Then T emb also an embedding function and therefore depth-0 transformer.
> O: Let f: (0, 11dd - {0. 1id be the top FFN of T. Then o f also a function {0, 1}dd {0, 1 and can therefore be computed by single FFN, by Lemma 20.
Theorem 27. For any B-RASP program P of depth that recognizes a language multi-head head masked hard-attention transformer with depth k that recognizes L.
Σ*, there is
Proof. Let P be any B-RASP program. For any operation P, (i) of P, we say that a transformer T with width d simulates (i(1) if there is a c E [d] such that, for all w E Σ*
if F (1) otherwise.
(T(W))..c
We prove the following statement by induction on r: For any operation (i) of P with depth k, there a multi-head masked hard-attention transformer with depth & that simulates (i)..
The base cases are 1 = [Σ], where every operation can be simulated by a transformer with depth using one-hot word embeddings, just as in the proof of Theorem 3.
If > μΣ], assume that each previous operation Pr with depth k' can simulated by a transformer with depth k', We will construct transformer of depth & that simulates (,)).
If P,(i) is an attention operation, then its S, V, and D predicates have depth at most (k 1) and therefore depend only on operations which can be simulated by transformers of depth (k 1), by the inductive hypothesis. Parallel-compose all of these into single transformer
26

---

rightmost-hare hard-attention, and (using Lemma 25) to obtain a transformer 7, of depth (k 1) that simulates all the operations that (i) depends on.
Then, extend T, to compute the attention operation as the proof of Theorem 3. Although that construction the identity function, and its FFN can be fused with the last FFN in T, by Lemma 26. So there exists a transformer 7, of depth k that simulates (1)
transformer layers, the first layer's 's self-attention just computes
If (i) is position-wiss operation of depth also have depth k. By the inductive hypothesis, these can be simulated by transformers of depth Parallel-compose them to get a transformer T, of depth k, by Lemma 25. Then, the computation of (i) itself can be fused with the last feed-forward network in f, by Lemma 26. This again results in a transformer T, of depth k that simulates Pr(().
may depend on earlier operations that
Thus, Pr is the output vector of and has depth k, then there a transformer that simulates Pr and has depth k. Add an output layer that transforms the output at position n to + if F Pr(n) and otherwise. Then, recognizes the same language that P recognizes.
D.3.4 Other attention variants
Earlier, we used transformers and B-RASP with only LTL with only since. Theorem 10 showed that
(sincc)))):
S (sinc))))) ç ....
B-RASP F)k
B-RASP F)R+I
MUHAT F)k
MUHAT( F)R+1
The separating language was STAIR which is the language over Σ (a, b, of strings which, after deleting c's, contain k+1 as substring. We can recognize STAIR; with formula yx I since yk. defined as follows:
= Qa
Y& Qa (le since yk-1))
k
Note the slight deviation from Etessami and Wilke (2000), because their presentation of LTL used the next and eventually operators as well as non-strict until'
Next, allow both masked rightmost and past- masked leftmost attention. We will notate these with MUHAT( 2)) and B-RASP F, PP), respectively, In LTL, we allow access to both temporal operators; let LTL; be the languages definable by formulas of depth k.
Proposition 28. Restricted only rightmost fulure-masked and lefimost past-masked attention, multi-head masked hard-altention transformers with depth (k + 1) are strictly more expressive than multi-head masked hard-atlention transformers with depth k.
Proof. The constructions in Theorems and preserve depth for rightmost future-masked and left- most mast-masked attention, B-RASP 4P)x LTL,- Moreover, the constructions in Theo- rems 3 and are identical regardless of attention type, so MUHAT( P)) = B-RASP( Finally, Etessami and Wilke (2000) show that with access both temporal operators it still the case that LTL S LTL2 (except the separating language is STAIR2: instead of STAIR;), Thus, have
P))-
LTL
C
LTL
B-RASP 4P)
B-RASP F. 4P)
II MUHAT F. P)) MUHAT P)
and in particular, MUHAT 4P) C MUHAT F, PR)+
Finally, we allow all six types of attention. These will be notated with MUHAT, and B-RASP
27

---

With access to future,, past-, and no masking and both leftmost- hard and rightmost- hard attention, multi-hear masked hard-attention transformers of depth (2k are strictly more expressive than multi-head masked hand-attention transformers of depth k.
Proposition 29.
Proof. As above, MUHAT, B-RASPR- However, in the proof of Theorem 2, the simulations of leftmost masued and rightmost past-masked attention require two levels nesting of since and until, it only shows that B-RASP, LTL As in the previous proof, LTL2x S 2TL (Etessami and Wilke, 2000). Finally, by Theorem 1, we again have 2TL S B-RASS22+1 21+1- Using all these observations, conclude that:
& LTL Ç
LTL2411 C... IN
B-RASP B-RASP 2k+1
II
MUHAT MUHAT 2k+1
Thus MUHAT & MUHAT 2++1
28

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification:
The abstract and introduction both summarize the paper.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
It is fine to include aspirational goals as motivation long is clear that these goals are not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Sections 2.2 and address the main limitation the paper, which is that the kind of transformers studied (unique-hard attention) differ from actual transformers.
Justification:
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model sell-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't It acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]

---

Theorems I to 7 and 10 and Corollary 8 all have proofs in the appendix and brief proof ideas in the main text, when appropriate. Corollary is very straightforward and in our opinion does not need an explicit proof.
Justification:
Guidelines:
The answer NA means that the paper does not include theoretical results. All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated referenced in the statement of any theorems.
The proof' can either appear in the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [NA]
Justification: This paper does not include any experimental results.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, it may be necessary either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, or other means that appropriate to the research performed.
While NeurlPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make clear how reproduce that algorithm. (b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
30

---

Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
Justification: The only code public github page which contains a B-RASP simulator implemented in HTML and Javascript. Using it, it is straightforward to recreate and run the example programs in the paper.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips.cc.
cobllcc/guies////e Saaiddee/ooeSuumisseeee cetibmmsssiooooicyyy. for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https:
ctppp//cc/bbb///guuu http///ddde//ee/ee http://gggiieeeeeeeeuttttiiiiii ssionPolicy) for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [NA]
Justification: This paper does not include any experiments.
Guidelines:
The answer NA means that the paper does include experiments.
The experimental setting should be presented in the core the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment Statistical Significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer:
[NA]
Justification: This paper does not include any experimental results.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
31

---

The method for calculating the error bars should be explained (closed form formula, call a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma enror bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are of range (e.g. negative enror rates).
If error bars reported in tables plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables the text.
8. Experiments Compute Resources
Question: For each experiment, does the paper provide sufficient information on the computer resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Answer: [NA]
Justification: This paper does not include any experiments.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the ines?
NeurIPS Code of Ethics https: /tte::///euuss./eeeeeee httpp//ccccpllltttttttttttt
Answer: [Yes]
Justification: We have reviewed the NeurlPS Code of Ethics and believe that the research in this paper conforms to it.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g.. if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification: This paper is purely theoretical, and we do not foresee any direct societal impacts.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
32

---

Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), faimesss considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Answer: [NA]
Justification: This paper is purely theoretical and poses no such risks.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e-g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [NA]
Justification: This paper does not use existing assets.
Guidelines:
The answer NA means that the paper does use existing assets. The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website). the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in package should be provided. For popular datasets, paperswi www.we.tttoo...oe. com/ datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
33

---

For existing datasets that are re-packaged, both the original license and the license of the derived asset (if has changed) should be provided.
If this information is available online, the authors are encouraged to reach out to the asset's s creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
The only new asset is a webpage hosted in a publicly accessible github repository.
Justification:
Guidelines:
The answer NA means that the paper does release assets.
Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: This paper does involve crowdsourcing or research with human subjects,
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: This paper does not involve crowdsourcing research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if' applicable), such the institution conducting the review.
34


Reviews:
[{"review_id": "HyID6kahiV", "reviewer": "Reviewer_u2XQ", "summary": "The authors connect masked hard-attention transformers (with single-head attention) with LTL via a Boolean version of RASP, namely B-RASP. Due to established results on LTL, they show that this type of transformer recognizes exactly the star-free languages.\n\nWhile unique hard attention transformers have been studied before, the authors also use strict future (and past) masking which essentially means that each position can't attend to itself but only to positions to the left (or right), respectively. RASP is a programming language by Weiss et al that was invented to have a language very close to how transformers work. This paper uses a Boolean version of it and shows equivalence with hard-attention transformer encoders with strict future masking. Linear Temporal Logic (LTL) is a well researched logic which recently has been linked to unique hard attention transformer encoders and shown equivalent in this paper. Some known results lead to further connections to and characterisations of transformers, including some extensions such as the use of position embeddings. The authors also show that increasing the number of attention layers always increases expressive power in multi-head masked hard-attention transformers.", "questions": "None.", "limitations": "The authors have thoroughly discussed the limitations of their findings one by one.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "The paper is very well-written and I enjoyed the examples for B-RASP which made it very easy to understand both the programming language and the equivalence proofs.\nThe first 4 sections lead through the results nicely. The last section is a bit more over the place but gives the impression that the authors looked into multiple directions and found numerous possible extensions that follow with little adjustments from their main result.\nThe discussion of previous work in between the results gives a good overview about similar lines of work and was very fitting.", "weaknesses": "First of all, I was missing a discussion about implications of the results and possible future work.\nUnique hard attention transformer encoders have been known to be in AC⁰ and have been linked to LTL[Mon] before. In my eyes, the main contribution of this paper is therefore the result that this characterisation is exact and the results on strict vs. non-strict masking. While these are useful realizations, they might not make the biggest impact on practical applications. Even more so, because hard attentions is hardly used in practice.\n\nThere is a typo in line 31: exp(r)essivity", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your review and your positive assessment of our paper!\n\n> In my eyes, the main contribution of this paper is therefore the result that this characterisation is exact and the results on strict vs. non-strict masking.\n\nYes, but we would also remind the reviewer of the other results in Section 5, which consider not only strict and non-strict masking (Thm 6) but also masking direction (Thm 5), position embeddings (Thm 7, Cor 8-9), and network depth (Thm 10). Put together, these results run the gamut of masked hard-attention architectures, and form a fuller picture with the two results you highlighted.  \n\n> I was missing a discussion about implications of the results and possible future work.\n\nThis point is well-taken, and we'll be sure to expand on this given extra space in the final version. Although there are some interesting remaining open questions about unique hard attention transformers, we primarily see these results as showcasing what kinds of results we can hope to obtain in the future: in particular, how do attention masking, position embeddings, and network depth affect expressivity? We've given rigorous answers for unique-hard attention transformers, and hope to obtain answers for more realistic (i.e., soft attention) transformers.", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "EctFsItZ2m", "reviewer": "Reviewer_6xK6", "summary": "The paper studies the expressive power of transformer encoders in terms of their ability to recognize regular languages. The main result in the paper establishes that if such encoders are equipped with hard attention, future masking is permitted, and positional encodings are disallowed, then the languages accepted by this model are precisely the ones that can be defined in linear temporal logic (LTL), which in turn coincides with the star-free languages. Several other results are presented in the paper, but in my view, these are corollaries of the main result and known properties of the relationship between LTL and certain classes of regular languages.", "questions": "Please explain why the detour through B-RASP is key to your proof and why you have decided to leave this connection in the body of the paper instead of keeping it in the appendix as part of the main proof. What kind of conceptual benefit do you feel that this connection brings to the paper?", "limitations": "Limitations are correctly addressed in the paper.", "rating": 6, "confidence": 5, "soundness": 4, "presentation": 2, "contribution": 3, "strengths": "The ability of Transformers to recognize languages, under different assumptions (e.g., attention mechanism, presence of decoders, type of positional encoding), is by now an active area of research. But this is one of the few results in the area that presents a precise characterization of an important Transformer model. While the proofs are more or less straightforward, I find the results beautiful and relevant, so I support the acceptance of this paper.", "weaknesses": "I find the detour through B-RASP unnecessary. First of all, proofs are not presented in the main body, and hence for someone without access to the appendix, there is no support for the claim that this detour is key. What is it that makes it \"key\"? Second, I think that a direct translation from LTL to Transformers, and back, is possible. The upper bound only depends on the finiteness of the vectors considered by the Transformers. In turn, for the lower bound, you can use similar techniques to those in Barceló et al, i.e., induction on the structure of formulas (this time by using positional masking as opposed to positional encodings).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your review, and for your assessment of our results as \"beautiful\" (!).\n\nIt's true that the equivalence of LTL and masked hard-attention transformers could be proven directly, without going through B-RASP. We have worked out the LTL to transformer direction outside of this paper. However, we forsee that the proof from transformers to LTL would have the same challenges as the proof of transformers to B-RASP, and would be harder to follow.\n\nWe would need a version of Lemma 12 for transformers: every unique hard attention transformer is equivalent to one in which the attention queries do not depend on the position. We think the matrix manipulations needed to prove this would be far more difficult than the present Lemma 12.\n\nThis is because LTL does not have a syntax for binary predicates, so we must eliminate relations that depend on two positions before doing the translation into LTL. While this works for masked-hard attention transformers due to Lemma 21, the same technique will not apply to other transformer variants. Thus we foresee the proof of transformers into B-RASP, with its binary score predicates S(i,j), as more relevant to future work than the version directly to LTL. By publishing this version of the proof, we hope to provide a template for extensions towards more realistic transformers.\n\nFor the general conceptual benefits of B-RASP, please see our global response.", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "1yTZau4Qnr", "reviewer": "Reviewer_6BGB", "summary": "This paper presents new theoretical results related to the expressive power of Transformers. The authors focus on Transformers with \"hard\" attention (a simplifying assumption) and strict future masking (i.e. attention can only attend to positions to the left). The paper develops an equivalence between such Transformers and B-RASP, and between B-RASP and Linear Temporal Logic (LTL), where B-RASP is a binary-valued version of RASP, a programming language for Transformers proposed by prior work. Thereby, the authors establish an equivalence between the proposed class of Transformers and LTL.", "questions": "Questions:\n\n* Is there an example of a commonly used positional encoding scheme with \"infinite image\"? (section 4.3)\n* It seems commonly used schemes for relative position encodings (e.g. https://arxiv.org/abs/1803.02155, https://arxiv.org/abs/1910.10683) could presumably enable expressing attention operations with strict future masking, without requiring this to be an implicit part of the architecture. Is this true? (section 4.3)\n\nSuggestions:\n\n* Nit - perhaps briefly defining terms such as complexity classes AC0 and P on their first mention could help make paper more accessible. \n* The main results focus on architectures with strict future masking and without positional encodings. Both choices are a very uncommon configuration for Transformers. However, per the question above, strict future masking is not necessary if using common positional encoding schemes. This is discussed to some degree in section 5.3, but this result could have potentially been mentioned earlier to justify the otherwise somewhat odd focus on strict future masking without positional encodings.\n* Section 5.2 mentions that \"Soft-attention can measure what fraction of symbols are l\". Potentially relevant: the RASP paper also discusses an algorithm for this, termed `selector_width`, and how this can be implemented with a start symbol or without (relying on positional encodings).\n* Section 5.3 mentions that positional information only comes from attention masking. Perhaps relevant: https://arxiv.org/abs/2305.19466 shows that absolute and relative positions can be recovered from only future masking (although I believe their proof relies on soft attention).", "limitations": "Some limitations are mentioned throughout the paper (e.g. section 2.2), but it might be helpful to have an explicit limitations section.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "* The paper adds to our understanding of the theoretical expressiveness of Transformers.\n* The use of B-RASP as an intermediate representation to establish the equivalence between Transformers and LTL was an interesting approach, and perhaps could inspire future work towards establishing the expressiveness of various Transformer variants.", "weaknesses": "* While the authors justify their choice of focusing on \"hard attention\", this puts some limits on the applicability of their results to real Transformers. However, this is also a common assumption made by prior theoretical work related to the expressiveness of Transformers.\n* Prior work has already established that hard attention Transformers can express LTL.\n* The main results that extend beyond prior work to establish the *equivalence* with LTL focuses on architectures with strict future masking and without positional encodings. Both choices are a very uncommon configuration for Transformers.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your review! We're glad you found the paper interesting and see its potential to inspire future work.\n\n> The main results [focus] on architectures with strict future masking and without positional encodings. Both choices are a very uncommon configuration for Transformers.\n\nOur results, which consider strict and non-strict masking (Thm 6), masking direction (Thm 5), and position embeddings ranging from nothing to sinusoidal to Mon (Thm 7, Cor 8-9), run the gamut of masked hard-attention architectures, both common and uncommon. It's true that our main result concerns an unusual combination of strict masking and position embeddings, but this is because it corresponds to the most well-known language class (star-free regular languages). (It may be worth noting that transformers with masking but no position embedding have been tried in practice and perform rather well (e.g., [Haviv et al 2022], [Kazemnejad et al 2023]).)\n\n> Is there an example of a commonly used positional encoding scheme with \"infinite image\"? (section 4.3)\n\nIt depends what you mean by \"commonly used\". In theoretical papers, yes, it's common to use quantities like 1/(i+1), i, or i² in position embeddings (e.g., [Perez et al 2019]). In practice, many commonly-used embeddings only go up to a fixed maximum position and therefore trivially have finite image, while many (e.g., RoPE, ALiBi) are architectural modifications and not just embeddings from positions to vectors.\n\n> It seems commonly used schemes for relative position encodings (e.g. [Shaw et al 2018], [Raffel et al 2020]) could presumably enable expressing attention operations with strict future masking, without requiring this to be an implicit part of the architecture. Is this true? (section 4.3)\n\nRelative position encodings would be interesting objects of further study. In principle, it seems that they could be used to simulate attention masking, but the encodings of [Shaw et al 2018] and [Raffel et al 2020] only go up to a fixed maximum distance, so they would not be suitable for this purpose.\n\n> [P]erhaps briefly defining terms such as complexity classes AC0 and P on their first mention could help make paper more accessible.\n\nThanks for the suggestion; we'll do that in the final version.\n\n> [I]t might be helpful to have an explicit limitations section.\n\nWe'll definitely give this some thought for the final version.\n\n[Haviv et al 2022]: https://arxiv.org/abs/2203.16634\n[Kazemnejad et al 2023]: https://arxiv.org/abs/2305.19466\n[Perez et al 2019]: https://arxiv.org/abs/1901.03429302.html\n[Raffel et al 2020]: https://arxiv.org/abs/1910.10683\n[Shaw et al 2018]: https://arxiv.org/abs/1803.02155", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "dkrCjPooXd", "reviewer": "Reviewer_rKKi", "summary": "The paper presents results about several forms of masked unique hard-attention transformers by classifying the class of languages recognized by these models using formal languages. Roughly put, a masked unique hard-attention transformer is an encoder that uses unique hardmax as its attention mechanism. In cases of ambiguity, either the leftmost or the rightmost position is attended to. Additionally, the attention heads are masked, meaning that a position only attends to (strictly) preceding ones (future masking) or (strictly) succeeding ones (past masking).\n\nIn summary, the presented results are:\n- Future-masked rightmost-hard attention transformers without positional embedding recognize exactly the star-free languages (Theorem 5).\n- Non-strict masked hard-attention transformers without positional embedding recognize exactly the stutter-invariant star-free languages (Theorem 6).\n\nTo establish these results, the paper introduces an auxiliary language called B-RASP to analyze masked hard-attention architectures. The paper shows that B-RASP exactly captures the considered transformer models (Theorems 3 and 4) and that it is as expressive as strict or non-strict Linear Temporal Logic (LTL) (Theorems 1 and 2). Then, the general proof idea of Theorems 5 and 6 is to translate results from strict or non-strict LTL via B-RASP to the respective transformer model. Additionally, the authors also establish that masked-hard attention transformer recognize the same languages as LTL with monadic predicates.", "questions": "- Can you explain in more detail why masked attention is of interest in the encoder parts of transformers?\n- In the proof of Theorem 3, Lemma 20 establishes a translation from B-RASP to masked hard-attention transformers. It appears that you use non-strict masking in the first layer to achieve self-attention. Am I correct? If so, how can you prove Theorem 5 based on this, since it concerns future-only masked hard-attention transformers?\n- In the proof sketch of Theorem 4, can you elaborate on why you focus on precision?\n- Can you explain in more detail the idea presented in line 264 regarding how a specific symbol BOS helps?\n- Can you explain in more detail how attention masking helps in recognizing all LTL[Mon] languages, as discussed in the paragraph starting on line 308?", "limitations": "The authors clearly describe their considered transformer model and specify where it differs from those commonly used in practice. However, these statements are somewhat scattered throughout the paper. A dedicated subsection summarizing all relevant limitations would be very helpful.", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "The results, mainly Theorem 5 and 6, in this paper follow an intriguing line of research trying to understand the expressive capabilities of transformer models from a formal languages perspective and, therefore, this research is well placed.  \n\nIn general, the technical proofs of the appendix are convincing and sufficiently argued and, thus, allow to verify them.", "weaknesses": "The contribution of this work is intriguing, though its significance may not be immediately apparent. The primary contributions are Theorems 5 and 6, and the transformer architectures considered are quite specific, possibly tailored for these particular results. There is some uncertainty about their broader interest. As the authors note, masked attention is almost exclusively used in the decoder parts of transformers. However, in this work, it is extensively used in encoder-only transformers.\n\nThe presentation of the paper is mixed. The first 5 pages are primarily devoted to preliminaries and the introduction of B-RASP, which, while interesting, serves mainly as a tool. This allocation of space would be justified if B-RASP were particularly complex, but it is relatively straightforward. Consequently, almost all theorems in the main paper lack proof sketches or intuitive explanations. Although the appendix adequately supports the theorems’ statements, the main paper itself does not. Additionally, the paper features a very brief introduction and lacks sections like ‘outlook’, ‘open questions’, ‘limitations’, or an equivalent closing and summarizing section. This omission makes it challenging for readers to place the results in the broader context of research.\n\nThe clarity of the paper is also mixed. First, the paper uses a form of LTL with a strict until operator and no next operator. Most readers are likely more familiar with non-strict until and the inclusion of the next operator. While this is a minor issue, a single sentence clarifying this would assist non-expert readers. There are more significant issues, which I address in my questions below. For example, in the brief sketch of Theorem 4, it is stated that the transformer “… can be represented using $\\mathcal{O}(1)$ bits.” It is unclear why this result focuses on representation sizes. Another example is Theorem 5, which states that future-only masking transformers recognize exactly the star-free languages. The proof relies on a translation from B-RASP to the transformer, and in this translation, it appears they use a self-attention mechanism requiring mixed masking. This may be a case of unclear explanation, but the current version of the paper makes it difficult to understand. If not clarified, this result could be incorrect.\n\nEdit: My concern about the correctness were cleared in the rebuttal. I changed my rating accordingly.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your review. We are glad that you find our work convincing, intriguing, and well-placed.\n\nOn B-RASP, please see our global response.\n\n> [T]he paper...makes it challenging for readers to place the results in the broader context of research.\n\nThis point is well-taken, and we'll be sure to expand on this given extra space in the final version. Although there are some interesting remaining open questions about unique hard attention transformers, we primarily see these results as showcasing what kinds of results we can hope to obtain in the future: in particular, how do attention masking, position embeddings, and network depth affect expressivity? We've given rigorous answers for unique-hard attention transformers, and hope to obtain answers for more realistic (i.e., soft attention) transformers.\n\nRegarding LTL with strict \"since\" versus non-strict \"since\" and \"previous\": We'll be happy to include a brief remark about this.\n\n> [T]he transformer architectures considered are quite specific, possibly tailored for these particular results.\n\nOur results, which consider strict and non-strict masking (Thm 6), masking direction (Thm 5), and position embeddings ranging from nothing to sinusoidal to Mon (Thm 7, Cor 8-9), run the gamut of masked hard-attention architectures, both common and uncommon. It's true that our main result concerns an unusual combination of strict masking and position embeddings, but this is because it corresponds to the most well-known language class (star-free regular languages). (It may be worth noting that transformers with masking but no position embedding have been tried in practice and perform rather well (e.g., [Haviv et al 2022], [Kazemnejad et al 2023].))\n\n> Can you explain in more detail why masked attention is of interest in the encoder parts of transformers?\n\nIt's true that masking is more commonly associated with decoders than encoders. We call the transformers studied here \"encoders\" because the string is the input rather than the output. But if one wishes, one could view them as decoders, with the string as the prompt and the accept/reject decision as the single-symbol output. On this view, perhaps, the use of future masking seems more natural.\n\n> In the proof of Theorem 3, Lemma 20...It appears that you use non-strict masking in the first layer to achieve self-attention. Am I correct? \n\nWe think you are referring line 629, which says: \"The first self-attention simply computes the identity function\". This means that the self-attention uses zero vectors for the values, letting the residual connection compute the identity function. The masking in this self-attention does not matter. We'll be sure to clarify this in the final version.\n\nOn the other hand, if you're referring to the fact that whatever masking is used in the B-RASP program is preserved in the transformer (line 631), then it's true that the transformer uses a mix of masks. But it's explained under Theorem 5 (line 233) that in LTL, any star-free language can be defined using only strict \"since,\" which translates to only strict future-masking in B-RASP, which translates to only strict future-masking in the transformer.\n\n> In the proof sketch of Theorem 4, can you elaborate on why you focus on precision?\n\nYes, we can elaborate on this in the final version. As explained in the full proof (line 663 and below), this makes it possible to represent any number computed by the transformer using a finite-sized logical formula. We do agree that line 676 is too terse and will expand it in the final version.\n\n> Can you explain in more detail the idea presented in line 264 regarding how a specific symbol BOS helps?\n\nThis idea is tangential to our paper, as it concerns soft-attention transformers, but if a string has a prefix $\\ell^k$, then at position $k$, a transformer (without position embeddings) cannot count how many $\\ell$'s there are; it can only measure what fraction of symbols are $\\ell$, which is 100%. But if we add a BOS symbol, then the fraction of symbols becomes $k/(k+1)$, so the transformer can discern different numbers of $\\ell$'s.\n\n> Can you explain in more detail how attention masking helps in recognizing all LTL[Mon] languages, as discussed in the paragraph starting on line 308?\n\nIt's possible that this paragraph is misplaced and is really more about LTL rather than LTL[Mon].\n\nWith neither position embedding nor attention masking, transformers are \"permutation equivariant\" ([Yun et al 2020]) (insensitive to reordering of the vectors in its input sequence). Position embeddings are one way to break the symmetry, and attention masking is another.\n\nThis paragraph makes the further point that even a transformer with a finite-image position embedding and no attention masking would not recognize all languages in LTL. For the final version, we'll reevaluate where the best place to make this point is.\n\n> A dedicated subsection summarizing all relevant limitations would be very helpful.\n\nWe'll definitely give this some thought for the final version.\n\n[Haviv et al 2022]: https://arxiv.org/abs/2203.16634\n[Kazemnejad et al 2023]: https://arxiv.org/abs/2305.19466\n[Yun et al 2020]: https://arxiv.org/abs/1912.10077", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: All four reviewers are positive about the contribution and the significance of this paper, and most praised its technical achievement.  On the other hand, none of them recommended acceptance clearly and with high confidence, most had reservations around practical relevance of this work, and some questioned the value of working through the intermediate formalism.
Decision: Accept (poster)