Knee-Deep in C-RASP: A Transformer Depth Hierarchy
Authors: Andy Yang
Michaël Cadilhac
David Chiang
Venue: NeurIPS 2025 poster ()
Keywords: Transformers
Depth
Layers
Formal Language Theory
Temporal Logic
Expressivity
Primary area: theory
TL;DR: We prove precisely how deeper transformers (with appropriate rounding) become more expressive, and show that empirical behaviour tracks our theory.

Abstract: It has been observed that transformers with greater depth (that is, more layers) have more capabilities, but can we establish formally which capabilities are gained? We answer this question with a theoretical proof followed by an empirical study. First, we consider transformers that round to fixed precision except inside attention. We show that this subclass of transformers is expressively equivalent to the programming language $\textsf{C}$-$\textsf{RASP}$ and this equivalence preserves depth. Second, we prove that deeper $\textsf{C}$-$\textsf{RASP}$ programs are more expressive than shallower $\textsf{C}$-$\textsf{RASP}$ programs, implying that deeper transformers are more expressive than shallower transformers (within the subclass mentioned above). The same is also proven for transformers with positional encodings (like RoPE and ALiBi). These results are established by studying a temporal logic with counting operators equivalent to $\textsf{C}$-$\textsf{RASP}$. Finally, we provide empirical evidence that our theory predicts the depth required for transformers without positional encodings to length-generalize on a family of sequential dependency tasks.

Knee-Deep in C-RASP:
A Transformer Depth Hierarchy
Andy Yang
Michaël Cadilhac
David Chiang
University of Notre Dame ay ayang4@nd.c .du
DePaul University mi chhael@cadi www.eeaaaaaa...cccccce name
University of Notre Dame dchiangênd. .du
Abstract
It has been observed that transformers with greater depth (that is, more layers) have more capabilities, but can we establish formally which capabilities are gained? We answer this question with a theoretical proof followed by an empirical study. First, consider transformers that round to fixed precision except inside atten- tion. We show that this subclass of transformers is expressively equivalent to the programming language C-RASP and this equivalence preserves depth. Second, we prove that deeper C-RASP programs are more expressive than shallower C-RASP programs, implying that deeper transformers transformers (within the subclass mentioned above). The same also proven for transformers with positional encodings (like RoPE and ALiBi). These results established by studying a temporal logic with counting operators equivalent to C-RASP. Finally, we provide empirical evidence that theory predicts the depth required for transformers without positional encodings to length-generalize on a family of sequential dependency tasks.
expressive than shallower
1 Introduction
Transformers in practice have been getting deeper and deeper over time. The original implementation (Vaswani et al., 2017) used transformers with 8 layers. BERT-Large (Devlin et al., 2019) had 24; GPT-2-XL (Radford et al., 2019) had 48; GPT-3 175B (Brown et al., 2020) had 96. Can we explain what the effects of deepening the networks?
Accuracy
Fixed-precision
depth
transformers
C-RASP
1
2
3
4
5
6
7
8
9
10
L3
100
100
100
100
100
100
100
100
100
100
L4
22
100
100
100
100
100
100
100
100
100
UI
$
L6
L
11
51
100
100
100
100
100
100
100
100
depth 3 = C-RASP
L6
10
8
37
100
98
100
100
100
100
100
U
UK
Ls
L,
20
49
100
100
100
100
depth
C-RASP
Ls
5
19
52
75
95
100
100
100
100
UI
14
L9
7
7
6
24
29
66
95
99
98
93
depth C-RASP
L10
12
49
96
98
La
L1
2
2
3
3
6
11
46
31
96
89
L12
0
0
2
30
27
62
Figure C-RASP expressively equivalent to fixed-precision transformers at each depth level. Then, because deeper C-RASP programs can solve more problems, deeper fixed-precision transformers can solve more problems as well.
Figure 2: Our theoretical results predict that transformer with depth can recognize language L but not LR+3 (demarcated by the black line). This closely aligns with our experimental results.
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

We can empirically observe capabilities that deeper transformers exhibit which shallower transformers do not. For instance, Clark al. (2019) and Tenney et al. (2019) find that attention heads at lower layers exhibit lower-order patterns (e-g., each symbol attends to the previous symbol), while heads at higher layers exhibit higher-order patterns (e.g., each direct object attends to its verb). However, we do not have many theoretical guarantees about the impacts of depth in transformers.
In classical theoretical computer science, one studies the power of computational models by asking what languages they can express an equivalent way of asking what problems they can solve. Our question becomes: What languages can be expressed by transformers of various depths? We explore this question using the temporal logic TL[ #1. which is equivalent to the programminn language C-RASP (Yang and Chiang, 2024), a variant of the RASP language (Weiss al., 2021). Previously, C-RASP had been shown to be no less expressive than fxxe-prrcisioe transformers and no more expressive than wrbitrary-precision transformers. are defined with rounding to fixed precision except inside attention (see Section 2.1 for more precise statement), transformers are expressively equivalent TL[#]. Moreover, the equivalences between C-RASP, TL[#] #1, J. and transformers preserve depth.
this paper, we prove that when transformers
We can therefore investigate transformer depth by investigating TL[#] #1 depth. Here, we prove strict depth hierarchy for TL[#], meaning that there is a problem that is solvable by a depth-k TL[#] formula, but not solvable by any depth-(k - 1) formulas. This implies a strict depth hierarchy for C-RASP and transformers (Fig. 1). (We also prove a strict depth hierarchy for the more expressive logic TL[ H, #1. This implies a strict depth hierarchy for FO[ -uniform LTC", which was not previously known.) We find experimentally that the C-RASP depth hierarchy closely predicts the depth that transformers require to solve problems with particular sequential dependencies (Fig. 2).
The languages Lx. which separate transformers of different depths, are just sets of strings with k runs of symbols. This suggests that, for example, in a speech recognition system where each phoneme can extend over multiple frames, a transformer with fixed depth may have difficulty recognizing k-grams of phonemes, for k sufficiently large.
We are aware of three previous depth separation results for transformers. Yang et al. (2024) established strict depth hierarchy for unique-hard attention transformers, based on the Until hierarchy for linear temporal logic (Etessami and Wilke, 2000). However, unique-hard attention transformers appear to diverge from transformers as used in practice (Huang et al., 2025; Liu et al., 2023). Sanford et al. (2024) proved, conditioned on a widely known conjecture (Ghaffari et al., 2019), that depth @(log (k) is necessary and sufficient for transformers to solve the k-hop induction heads problem. The first unconditional depth-width tradeoff, based on communication complexity lower bounds, was shown by Chen al. (2025). In essence, a transformer with depth & would require impractically large width of (n)) to perform the sequential composition of k + functions, while a transformer with depth 1 can implement a solution with a modest width of (pooyyoggzz))
The latter two results used transformers whose parameters depended on the sequence length n. Our results parameter-umifone that is, they construct transformers with parameters independent of making them applicable to inputs of arbitrary length and better predictors of length generalization. Below, we compare and contrast these depth separation results with ours:
model
transformer
unconditional
parameter-uniform
Yang et al. (2024)
temporal logic
unique-hard
yes
yes
Chen et al. (2025)
communication complexity
softmax yes no
Sanford et al. (2024)
massively parallel
softmax no no
computation temporal logic
This work
softmax
yes
yes
2 Preliminaries
We write N for the set of nonnegative integers and [n] for the set (1....,n), n). With w = w.-.-W, a string over Σ, we write wli: for the substring Wi wj With L language, we write L for the Kleene star of L (L" Uk2o L and + for LL". See Appendix G for index of all notation used.

---

2.1 Transformers
In this paper, we consider transformers that use fixed-precision numbers. Merrill and Sabharwal (2023) have pointed out that in transformer that uses fixed precision for all operations, there is some length beyond which the attention weights necessarily round to zero, making attention unable to attend to anything. To get around this, we define fixed-precision transformers without rounding of numbers that scale as or 1/n. Namely, define an operation on two n-dimensional vectors,
sumdiv(a, b)
Σ bj
Then if q e Iid is a query vector, K E Raxd is a matrix of keys, and v E Ra*l is value vector, attention can be written as
qtt(q. = sumdiv qk exp
where is componentwise multiplication. Because the intermediate results of sumdiv scale with we do not round them; we only round the final result. Our transformers use future-masking but no position encodings. See Appendix B.I for a full definition.
2.2 Temporal logies with counting
Temporal logics are used to express properties of (finite and infinite) strings, using predicates and temporal operates to assert properties of the current position. For instance, in linear temporal logic (Gabbay et al., 1980), one can express things like "at some time in the future, there is an a." Temporal logic with counting (Hirshfeld and Rabinovich, 2012; Barceló et al., 2024) adds more general integer- valued counting operators: a property such as "at some time in the future, there is an a" thus becomes "the number of 's in the future is at least 1." Here, equivalent to (variants of) transformers (Section 3 and Appendix B).
interested in these logics because they
Definition 2.1. The syntax of past temporal logic with counting, or TL[ [[[#], as follows:
é == 2. | 11 < 12 - I &1 A Φ2
o OE
coolean-valued formulas
# [ 11+ 12
integer-valued terms
Temporal logic with counting, or TL[ #. #). adds an operator #, and is discussed in Appendix D. In Appendix F.1, further extend the logic with MOD predicate and Y operator corresponding to positional encodings in transformers. Other operators, like S. 2. V, -, multiplication by integer constants, and integer constants other than 1, can be defined in terms of the above.
The semantics of TTL #) and TL #, #) are defined by the relation w, } Φ. meaning that the formula position i. First, w. }= Qo holds when the i-th symbol of w is The term # [ evaluated on string w at position i, counts the number of positions in w[1 i] that satisfy 6. Similarly, # [Ø] counts the number of positions in wli n| that satisfy & (where [w]). Terms can be added (+) or compared (<). See Definition A.1 for the full definition. We write w }= $ iff w. |n] }= Φ; that is, & is satisfied by at its final position.' Finally, the language defined by ( [w E E" | w == d).
is satisfied by string
Example 2.2. The Dyck language the set of strings of balanced and matched parentheses. The formula Oraionce = (# [Q1 = # ([2,]) checks that the number of left and right parentheses is equal. The formula &match # I # [Q < # #11,1] = 0) checks that, in every prefix, the number of right parentheses does not exceed the number of left parentheses. So the Dyck language is defined by &alance A @match. Appendix A.2 shows more detailed traces of this formula some example strings.
The depth of formula or term of TL # or TL H. #
the maximum depth which # and # operators are nested. TL[ # l is the class of all TL formulas with depth most k, and similarly for TL[ #. #]x and the other logics we use. See Definition A.2 in Appendix A. I for a formal definition. A depth-1 formula may be a Boolean combination of other formulas of depth 0 and I; minimal depth-l formula is one that does not contain other depth-1 1 formulas, that is, a formula of the form 1 < t2
Usually, the semantics of temporal logics detined by w } & iff w. F 6. However, in our setting. our definition mimics the behavior of generative transformer decoders. which for each position, consider all previously generated tokens (to the left) in order to produce the next token.

---

where 1j and 12 are depth-1 1 terms. For example, 0a & 1+1) 1) has depth 0, Qa (# #10b))
has depth but is not minimal, and [Q2a #[@+] + # #[2.]
is minimal depth-1 formula.
Yang and Chiang (2024) called [L[#] ] by different name, [+] They showed that is equivalent C-RASP, which admits notion of depth that corresponds exactly formula depth.
2.3
Parikh vectors
At the heart of TL[#] the ability count symbols, introduce some notation related to counts.
Definition 2.3 (Parikh, 1966). Let Σ (0), 02....m.mmmmm be (ordered) alphabet. The Parikh vector of w, written P(w), records the number of times each symbol occurs in w, ignoring order. That is,
V: Σ" - N
V (w) [i E [[wl]
w/ w/
V(w) = (V (w), V Vo, (w)...., V (w)).
Definition 2.4. For a Parikh vector V (V1, V2...., P|E)) E NIE we write the length of V as |ل]| = V1 v2 ........ VIEI. access individual coordinates, we write [7],, oVlo,oo for Vi.
Definition 2.5. For Parikh vectors J. E N we write 7 s iff M o S [] for all or Σ. We write [7. 7l for the set of all vectors such that 7 s J. We call [] an interval in NIE), and we write I EI for the set of all intervals in N A family of intervals is function I: N - I ((NE)).
Definition 2.6. For each partial function a: N x N + {0, such that (VV, is defined iff 1 IsiS [[]|,, define predicate II, called Parikh numerical predicate or PNP:
w.i II = I()(w), 1.
We write TL[# PNP] and TL[ # #. PNP] for the logics TL[#] and TL #, #1, respectively, aug- mented with arbitrary PNPs.
2.4 Piecewise testable languages
Piecewise testable languages are a subclass of regular languages that has been studied in semigroup theory and logic (Simon, 1975). Here, they will be key to separating the depth levels of both TL| # and TL[ #, #].
Definition 2.7. A J J-expressioon is a language of the form E''''' ... ..',T'" where 01....,00 ok Σ. A language k-piecewise testable if it is Boolean combination of -xeexpressoons with at most k fixed symbols. A language is piecewise testable if it is k-piecewise testable for some Lemma 2.8. For all k 2 0, define 1.p to be the language of strings with alternating blocks of a's and b' b's, starting with a:
L* (atbt) (atbt)(t-112
k even
k odd.
Then LA is k-piecewise testable. Proof. Define the following k-piecewise testable languages:
A Σ {
k even
Σ'(bE'aE') B₁ E' ("bb''E")) (L
k even k odd.
((E k odd
Then La is a Boolean combination of these:
== BB
Lemma 2.9. Any k-piecewise testable language is definable in TL [[[ lx. and any (2k + 1)ppiecewise testable language is definable in TL[#. #]
Proof sketch. Since our logics are closed under Boolean operations, we simply need to show the statement for T-expressions, Let sketch this in the case
There is straightforward way to
define L a' by' cE" in TL[ 22+1:
[( [ [2a] 2 1) Qb1 2 1) e.1 2 1.
With both past and future counting, we can find the middle symbol b and check the left and right:
# #I#1 2 A Q, A # [ 2 1] 2 1.
This is in TL[ #, # 1+1. desired. See Appendix A.4 for the full proof.

---

[[bb]
# #[Qb]
w
5
4
3
2
# [Qal
# [[aa
3
5
9
2
(a) Strings can be pictured as paths, and minimal depth-1 subformulas as half-plan aalf-planes.
(b) Within a sufficiently large rectangle (?), one can find a sub- rectangle (!") within which the depth-1 sub- formulas are either always true always false.
Figure Visualization of the reduction lemma (Lemma 4.9).
3 Transformer Equivalence
Logics like TL[ provide a way to reason about the computations that occur in transformers. Yang and Chiang (2024) proved that transformers can simulate TL[ # and TL[ # can simulate transformers that round all values to fixed precision. Here, we show that fixed precision, with rounding slightly loosened as Section 2.1, makes possible to obtain an exact equivalence.
Theorem 3.1. A language defined by a formula of TL[ of depth and only if <BOS> recognized by a
transformer of depth k.
Proof. See Appendix B.
In Appendix F, we will extend the transformer-to-logiit direction of this result several position encodings and an extension of TL[ #].
Depth Hierarchy
To prove a strict depth hierarchy for TL[#], adapt the technique of Behle al. (2009), which was originally used on MAJ2[<]. a logic equivalent to TL[ #. # The main idea to assume, towards contradiction, that certain language is definable by formula, then to simultaneously restrict the language and reduce the depth of the formula down depth 1. The contradiction will be that the restricted language has a property (namely, sensitivity to ordering) that is not definable at depth 1. This technique can also be applied to the bidirectional logic TL[ #, #], with implications for other logics and circuit classes, as detailed in Appendix D.
4.1 Intuition and example
As an example of the technique, consider the following formula:
(2# Qal 3# (#bl)))
( [2al + #1 10) 2b1 1.
11
This formula has depth 2 and it has two minimal depth-1 subformulas, Φ and 62. We want to replace &1 and d2 with depth-O subformulas, reducing the depth of & from while restricting the language defined.
Since &i and d2 are linear inequalities in the counts # 1r can picture them half-planes (Fig. 3a). A string can be pictured as a path, and a prefix of the string as a point on the path. For concreteness, we fix vector ă = (9, 8) and let / be the interval [Ō, πj. (In the formal proof, ň will not be fixed, and will a family of intervals depending on π..) Suppose we can find some subinterval I' (which can be pictured as a rectangle, as in Fig. 3b) that does not cross any of the half- half-plane boundaries. All points I' are equivalent in the sense that the truth value of &1 and de is the same for all points in l'
5

---

We restrict the language by choosing prefix corresponding to path from the bottom left of / to the bottom left of I', and a suffix corresponding path from the top right of I' the top right of In our example, we picked baaaaa and bbababb. Informally, we can define the restriction of & to this prefix and suffix like so:
o' "prefix is baaaaa" A "suffix is bbababb"
A (#l01 A 02 A Qb A "inside ['] + # A 02 A Qb A "in prefix/suftix"] 2 1).
Then the occurrences of Φ) and Φ marked (+) are always true and false, respectively, while the occurrences marked (+) depend only on the position. As we will see, we can replace all of these by PNPs, reducing the depth of the formula from 2 to 1.
Carefully iterating this process (Lemmaa 4.9) leads depth-1 formula defining restriction of the original language. In this language, we will show that the ordering of symbols matters, but we will see in Lemma 4.6 that depth-1 1 formulas are (in particular sense) insensitive to the ordering of symbols. This a contradiction, demonstrating that the original language is not definable.
4.2 A ffix restrictions
We start by defining the affix restrictions that were informally introduced in the start of this section. Krebs (2008) enforced similar restrictions using the algebraic tool of non-uniform morphisms, while Behle et al. (2009) used numerical predicates on languages with restricted Parikh image. We follow the latter approach of expressing this idea within purely logical framework, but introduce Parikh numerical predicates as a way to generalize the technique.
Definition 4.1 (cf. Def. 6.5 of Krebs, 2008), An affix restriction is a pair (A, Q). where d, 0: N Σ' For any language L C Σ' and affix restriction (d, @), we define the restriction of L to (2, g)
.l. {w E L: 3w' E E" such that w = A(Y(w)) w' (o'ee(((())))
In the definition above, the set of positions occupied by w' within each string is the only part not fixed by (d, g) This region is important for the depth reduction process, so we give it name: Definition 4.2. The middle of an affix restriction (2, @) is the family of intervals given by ñ + (V)() ñ (((())]]
In order for the middle of an affix restriction to not be too restricted, typically require affix restrictions to have the following property.
Definition 4.3. We say that a family of intervals I is accommodating for any 3 E N there is an interval [] in the image of such that 3 s j-ī, or, equivalently, 3 e
We say that
affix restriction (d. @) is accommodating if its middle is accommodating.
An example of non-accommodating affix restriction, with Σ {aa, b). is ((na.n))) e and o((aav n3)) a² b" In this case دا will have at most one string for each (πa. mb).. An accommo- dating affix restriction the trivial one 2 (((a, g((n., nb)) c. this case 2Le will have [nu (Ma+ strings for each (b).
na
Accommodating affix restrictions will be key to depth-reduction. If language has an accommodating middle under restriction (2, @), then there is enough room to apply another restriction (2', g") inside the middle, while decreasing the depth of the formula. As long as the property of accommodation is preserved at each step, this process can be iterated until we reach depth I.
4.3 Properties of depth
In this section, exhibit inherent limitations of depth-1 1 formulas. Informally, show that these formulas only recognize commutative languages, that is, languages where the order of symbols does matter. But need qualify this statement slightly, and need some technicalities well.
In particular, affix restrictions will fix the ordering of symbols the prefix and suffix, so affix- restricted languages can only be commutative in the following sense:

---

Definition 4,4, We say that a language L is commutative on the middle of an affix restriction (2, @) if for any w, w' E Zg such that ((w) '(('), we have w E L if and only if w' E L.
We will use PNPs to enforce ordering in the prefix and suffix, but to allow languages to be commutative on the middle, we need to prevent the PNPs from enforcing ordering in the middle.
Definition 4.5. We say that a formula & is constant on a family of intervals 1: N - I(NEE) if the following holds for all ñ e N El: For all w, w' E' with ((w) P(w') ń and all positions i, in 1(7), we have w. i F= & if and only if w', , F d.
Lemma 4.6 (Commutativity of depth 1). For any depth-1 formula & of TL PNP]: or TL #. PNP]; and any affix restriction (d, @) with le(n)) 2 for all n. if the PNPs of o are constant on the middle of (A, Q). then {()) is commutative on the middle of (d. o).
Proof. See Appendix C.I. The reason for the condition le(ā) 2 is that the 2o predicates are able to test the symbol in the last position.
4.4 Cropping and reduction lemmas
In this section, we show how to decrease the quantifier depth of a formula & while specifying precisely how L(d) is weakened. Our approach follows Lemma 3 of Behle et al. (2009) and Lemma 6.8 of Krebs (2008), but faces additional technical difficulties specific to TL[ # and, to lesser extent, the use of PNPs. Since we will be applying this technique on two-letter alphabets, we set Σ = {a, b} for the rest of this section. Thus, we can visualize Parikh vectors and intervals in the plane, with the number of a's on the horizontal axis, and the number of b's on the vertical axis.
First, the cropping lemma takes family of intervals / and "crops" it down to family of subintervals on which the minimal 1epth-1 subformulas are constant. This is done while controlling where I' sits within I, and we start by formalizing this notion:
Definition 4.7. We say that an interval (t', J'1 sticks to the top of an interval [7.]] if s (I. and 1r']-= = Lsl. Graphically, this means that the top edge of the rectangle [". is included the top edge of the rectangle [7. j}. We define an interval sticking to the bottom, left, or right analogously.
Lemma 4.8 (Cropping Lemma for TL[ # #I). For any formula & TL PNP] and any accommodat- ing family of intervals 1: NIE - I 21) such that the PNPs of & are constant on I, there exists an accommodating. family of intervals I': 2 - I E such that (7) sticks only to the top (and no other )ide) of I(ñ) for all ñ E N and all of the minimal depth-I subformulas (and PNPs) of & are constant on I' Additionally, there exists such an I' such that I'(i) sticks only to the right of I(î).
Proof. See Appendix C.2.
Second, the reduction lemma takes an affix restriction (whose middle is I' given by the cropping lemma) and rewrites away the minimal depth-1 subformulas, reducing the depth of the formula by 1.
Lemma 4.9 (Reduction Lemma). For any depth-k formula & of T PNP] (or TL[#, H, #, PNP];) and affix restriction (d, e). if the PNPs and minimal depth-1 subformulas of 6 are constant on the middle of (2, e), then there is a formula o' of depth (k - 1) of TL[#, PNP] (or TL[#, #, #, PNP] k. resp.) that defines 2L()). o. and the PNPs of 3' are constant on the middle of (2,
Proof. See Appendix C.3.
4.5 Non-definability results
As described by Behle et al. (2009), the key to applying this lemma is to choose a language L and appropriate affix families such that the restricted language does not become trivial. We now use the cropping and reduction lemmas to derive the strictness of the depth hierarchy of T[[#].
Theorem 4.10. Let > O. The language LE+1 (Eq, (1)) is definable in TL[#] but not in TL[ #)
Proof. Assume that is even (the odd case is similar). For a contradiction, assume there exists some depth-k formula d E #] which defines LE+1. Let ( = [(1,0) (1,0), de (m) a, ( a, and de = ob Note that (dz, @x) is accommodating, and Φe has no PNPs.
For ( = k 1, k 2, ..... 1. we will define the following:
7

---

1. An accommodating family of intervals ( S (n);
2. An accommodating affix restriction (n) Li-r+1 and @r Ea':
3. A depth-L formula or PNP)) which defines 2e (Lx+1) and only uses PNPs which are constant over (de, Cc).
We use the following iterative procedure:
1. Using Lemma 4.8, find accommodating family of intervals Ie such that for all n. ( sticks only to the top of le+1 ( and the minimal depth-1 subformulas Φe+1 are constant on (n).
2. Choose an affix restriction whose middle is 4,, as follows. Let [ī.j] 12+1 and [ j (ñ); then
In)
(++
er (T
Aet det1 (a) b10--i l odd det1 (î) blP -i--- PP-il even
er a (1+
An
Because de+1 (7) E Lk-L and (ñ) sticks only to the top of (ñ), we have that de E Lk-ett- At the same time, (r(î) a+.
3. Using Lemma 4.9, we can find a depth-E formula or of TL PNP]r that defines de (Lx+1) and only
PNPs which are constant (Ar, er).
At the end of the procedure above, we are left with the accommodating affix restriction (1) E Lk and @ (ñ) at, as well as the depth-1 formula $1 E TL[#, #, PNP) which defines 2; (Lk+1) and only uses PNPs which are constant over (d1, 21).
Since (d1, @1) is accommodating, choose π so that the middle has s, 2 occurrences of a and 2 occurrences of Construct the strings
(n)bb (n)
w' = (n) (i))
The prefix 21 (ñ) has & blocks ending with b. and the suffix p1 (ū) is all a's. So has (k 1) blocks and is therefore in LR+1, while w' has (k + 3) blocks and is therefore not in LK+1- But by Lemma 4.6, we have w += Φi = w' |= Φ1. This is contradiction, we conclude that no formula & with depth k can define Lx+1-
If k is odd, the argument is the same, with the following changes. First, symbols and b are swapped, but de still starts with a. Second, 1e (ñ) sticks to the right of (++1 instead of the top.
Finally, by Lemma 2.8, Le+1 is (k -ppieceeise testable. Thus, by Lemma 2.9, Les1 is definable in TL[ k++1.
This depth hierarchy on TL[#] implies a depth hierarchy for -eed-precision transformers. Theorem 4.11. A depth-(k 1) fixed-precision transformer can recognize 1.t+1, but depth-k fixed-precision transformer can.
This also implies a depth hierarchy for transformers using several commonly used positional encodings (with a different separating language). Definitions and details can be found in Appendix F.
Theorem 4.12. A depth-(k + 1) fixed-precision transformer can recognize Ex+1. but no depth-k fixed- precision transformer can, if the transformers can use sinusoidal positional embeddings (Vaswani et al., 2017), RoPE (Su et al., 2024), or ALiBi (Press et al., 2022).
Experiments
Our depth hierarchy result suggests that transformers will require greater depth in order to model deeper sequential dependencies. We empirically validate this by training future-mate masked transformers with positional encodings and varying depths to lear the Lę language, for varying k.? Here, the
2The code used for our experiments is provided at https: // thub. http://ww..onaaoooooee////s//.e
LLMs were used to assist in writing code and debugging.

---

Accuracy on 250]
Accuracy on [251,
depth -
depth
2
4
6
7
8
9
10
2
4
6
7
8
9
10
L3
100
100
100
100
100
100
100
100
100
100
L3
100
100
100
100
100
100
100
100
100
100
L4
41
100
100
100
100
100
100
100
100
100
L4
32
100
100
100
100
100
100
100
100
100
1.5
36
76
100
100
100
100
100
100
100
100
1.5
24
65
100
100
100
100
100
100
100
100
L6
36
37
74
100
100
100
100
100
100
100
L6
26
24
59
100
100
100
100
100
100
100
L7
39
40
53
87
100
100
100
100
100
100
L7
27
24
39
74
100
100
100
100
100
100
L8
37
42
53
78
96
100
100
100
100
100
L8
23
26
43
82
93
100
100
100
100
100
Lo
32
41
45
61
74
93
100
100
100
100
L
31
28
25
50
59
91
100
100
100
99
110
36
50
80
100
100
L10
17
26
71
91
99
100
1.11
37
41
45
49
55
60
77
77
100
100
1.11
19
20
21
26
33
42
69
64
100
98
L12
27
23
34
34
36
47
59
74
73
86
L12
6
5
12
12
21
53
60
56
75
Accuracy on (301,350)
Accuracy on [351, 4000
depth -
depth -
2
4
6
7
8
9
10
2
4
6
7
8
9
10
1
100
100
100
100
100
100
100
100
100
100
1.3
100
100
100
100
100
100
100
100
100
100
1.
26
100
100
100
100
100
100
100
100
100
1.4
22
100
100
100
100
100
100
100
100
100
Ls
59
100
100
100
100
100
100
L5
51
100
100
100
100
100
100
L6
17
14
49
100
99
100
100
100
100
100
L6
10
8
37
100
98
100
100
100
100
100
L7
13
12
25
59
100
100
100
100
99
100
L7
8
20
49
100
100
100
100
98
100
Ls
11
14
29
68
85
99
100
100
100
100
Ls
6
19
52
75
95
100
100
100
100
L.9
14
13
11
34
43
80
98
100
99
97
1.9
7
7
6
24
29
66
95
99
98
93
10
5
12
58
98
99
110
2
6
49
96
L11
6
6
6
8
14
21
59
45
99
96
L11
2
3
11
46
31
96
89
L12
2
2
3
9
37
42
38
68
L12
0
0
0
4
21
30
27
62
Figure 4: Experimental results. Corollary 5.2 predicts that transformer with depth & can recognize language La+2 but not L4+3 (demarcated by the black line). Up to at least L12, this closely predicts experimental results (shown as numbers and colors).
La language serves as a minimal testbed for depth separation because it represents the simplest form of sequential dependency (ordering of symbols) using only an alphabet of size 2.
5.1 Problem
Our experimental setup differs slightly from the framework presented above. For the language recognition problem considered above, training a transformer would require data containing both positive and negative examples, with the distribution of negative examples potentially having an important impact on learnability. Following Bhattamishra et al. (2020) and Huang et al. (2025), we reframe 1.,, as next-token prediction problem: For each prefix of a string, output the set of possible next symbols of the string.
Our data consist of source-target pairs, where the source is string in Lx. preceded by beginning- of-string symbol <BOS>, and the target a string of the same length. Each target symbol is a code standing for the set of possible next source symbols. If k is odd, for example, L3 a* b* at, then after <BOS>, there is only one possible set, {a} (coded as O), and after subsequent symbols, there are two possible sets, {a, b) (coded 0) if the string is in a* b², and {a, <EOS>) (coded as 1) if the string is in a" bO a+ (where <EOS> stands for the end of the string). An example source-target pair is:
S = <BOS> a baabbbbaaaae
T O 0000000110
If is even, the possible sets would be {a} (coded as 0) after <BOS>, and {a, b) (coded as 0) and (<EOS>, b) (coded as 1) subsequently. It turns that for l.c, the output for prefix <BOS> w[1 should be if and only if w[1: : L4-
We can define the next-token prediction problem for TL in the same way, but without <BOS>; Definition 5.1 (Next-Toker Prediction Problem for I.t). We say a TL #1 formula a can solve the next-token prediction problem for Lx for all w E La and s i S [w], we have w[1 i] }= =

---

w[1: : i] E Lg- That is, w[1: F if the prediction is 1, while w[1 i] |F 6 if the prediction is O. Note that, unlike in recognition, we only consider prefixes of strings that are in Li.
The depth hierarchy from Theorem 4.10 can be adapted to the next-token prediction problem for La- Corollary 5.2 (Corollary of Theorem 4.10). A depth-(k + 1) TL[#) formula can solve the next-token prediction problem for LR+3, but no depth-k k TL[ # formula can.
Proof. See Appendix C.4.
5.2 Setup
We generated samples of L& to place into bins [201, 250], [251, [301, 350], [351, 400] by uniformly sampling length n from the bin and uniformly sampling positions which to switch between a and b. For each & and each bin, 1000 strings were generated. The [201. 250] bin of 1000 examples was split into a training set of 800 examples and validation set of 200 examples. The other bins were reserved for evaluation.
We trained future-masked transformers without positional encodings. Because the of next tokens are mutually exclusive, we trained the transformer to perform multi-class classification with cross- entropy as the loss function. Adam was used the optimizer (Kingma and Ba, 2015). The dimension d and learning rate were tuned by searching over d E [256. 512] and E [10- 10-"). Each hyperparameter configuration was trained for 25 epochs or until 100% accuracy was achieved on the validation set. Then we evaluated the trained model on the test sets, considering the transformer to have made correct prediction if and only if its prediction matched the target at every single position. The experiments were run on an internal cluster of GPUs. Performing the training loop for given number of layers over all L3 required an average 9.37 10 TFLOPs and 936.8 MiB of memory.
5.3 Results
Figure 4 shows the final accuracies of models with varying depth on L3 with varying k. Corollary 5.2 predicts that a TL[ [ formula must have depth least in order solve the next-token prediction problem for Lk+2. In most cases, the transformer obtains 100% accuracy when Corollary 5.2 predicts it, and even generalizes to lengths up to double the training length. Other factors, like width, data diversity, and training dynamics of deeper transformers, may also play role in practice.
6 Limitations
Our theoretical results apply to fixed-precision transformers with and without positional encodings, whose definition differs subtly from both standard real-valued softmax transformers and fixed- precision transformers considered in previous work. Our experimental results did not use positional encodings because expect that extremely long input lengths are required to see our negative results apply. Additionally, our experiments only concern formal language tasks - namely, the languages Lμ-
Conclusion
This paper adds the growing list of exact equivalences between variants of transformers and logies or complexity classes (Yang et al., 2024; Merrill and Sabharwal, 2024; Li et al., 2024; Li and Cotterell, 2025). Here, we have shown that transformers that round to fixed precision except inside attention are exactly equivalent to TL and C-RASP. Moreover, we have proven a strict depth hierarchy for TL| H], which implies strict depth hierarchy for (this variant of) transformers. Unlike previous depth separations for softmax transformers (Sanford et al., 2024; Chen et al., 2025). our results apply to darameter-unifomay transformers and are particularly relevant length generalization. Future work on the experimental side could look for real-world phenomena that involve sequential dependencies like those in l and study how well language models handle them.
10

---

Acknowledgements
This material is based in part upon work supported by the National Science Foundation under Grant No. 2502292 and a Graduate Research Fellowship under Grant No. 2236418. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation. We would like to thank Dana Angluin and Lena Strobl for their generous input on the presentation of the theoretical results and development of the experiments in this paper. We also thank Michael Hahn for introducing us to the fascinating connection between TL[ #. #1 and [AJ][<], which paved the way towards the results proven here, and Gavin Dooley, Peter Cholak, and Anand Pillay for insightful conversations about TL[#] #J. Finally, we thank the anonymous reviewers for their helpful comments.
References
Pablo Barceló, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir V. Podolskii. 2024. Logical languages accepted by transformer encoders with hard attention. In Proceedings of the Twelfth International Conference Learning Representations (ICLR).
Christoph Behle, Andreas Krebs, and Mark Mercer. 2013. Linear circuits, two-variable logic and weakly blocked monoids. Theoretical Computer Science, 501:20-33.
Christoph Behle, Andreas Krebs, and Stephanie Reifferscheid. 2009. Regular languages definable by majority quantifiers with variables. In Developments Language Theory: 13th International Conference, DLT 2009, pages 91-102.
Satwik Bhattamishra, Kabir Abuja, and Navin Goyal. 2020. On the ability and limitations of transformers 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-Von Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, and 12 others. 2020. Language models are few-shot learners. In Advances in Neural Information Processing Systems 33 (NeurlPS), pages 1877-1901.
Lijie Chen, Binghui Peng, and Hongxun Wu. 2025. Theoretical limitations of multi-layer Transformer. In Proceedings of the IEEE 66th Annual Symposium on Foundations of Compuler Science (FOCS).
To appear.
David Chiang, Peter Cholak, and Anand Pillay. 2023. Tighter bounds on the expressivity of trans- former encoders. In Proceedings of the 40th International Conference on Machine Learning (ICML), pages 5544-5562.
Kevin Clark, Urvashi Khandelwal, Omer Levy, and Christopher D. Manning. 2019. What does BERT look at? An analysis of BERT's s attention. In Proceedings of the ACL Workshop BlackboxNLP: Analyzing and Interpreting Neural Networks for NLP, pages 276-286.
Jacob Devlin, Ming-Wer 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 (NAACL HLT), pages 4171-4186.
Kousha Etessami and Thomas Wilke. 2000. An until hierarchy and other applications of an Ehrenfeucht-Fraiissé game for temporal logic. Information and Computation, 160(1):88-108.
Dov Gabbay. Amir Pnucli, 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.
Mohsen Ghaffari, Fabian Kuhn and Jara Uitto. 2019, Conditional hardness results for massively parallel computation from distributed lower bounds. In Proceedings of the IEEE 60th Annual Symposium Foundations of Computer Science (FOCS), pages 1650-1663.

---

Yoram Hirshfeld and Alexander Rabinovich. 2012. Continuous time temporal logic with counting. Information and Computation, 214:1-9.
Xinting Huang, Andy Yang, Satwik Bhattamishra, Yash Sarrof, Andreas Krebs, Hattie Zhou, Preetum Nakkiran, and Michael Hahn. 2025. A formal framework for understanding length generaliza- tion in transformers. In Proceedings of the Thirteenth International Conference on Learning Representations (ICLR).
Diederik P. Kingma and Jimmy Lei Ba. 2015. Adam: A method for stochastic optimization. In Proceedings of the Third International Conference on Learning Representations (ICLR).
Andreas Krebs. 2008. Typed semigroups, majority logic, and threshold circuits. Ph.D. thesis, Universität Tübingen.
Jiaoda Li and Ryan Cotterell. 2025. Characterizing the expressivity of transformer language models. In Advances Neural Information Processing Systems 38 (NeurIPS). To appear.
Zhiyuan Li, Hong Liu, Denny Zhou, and Tengyu Ma. 2024. Chain of thought empowers transformers to solve inherently serial problems. In Proceedings of the Twelfth International Conference on Learning Representations (ICLR).
Bingbin Liu, Jordan T. Ash, Surbhi Goel, Akshay Krishnamurthy, and Cyril Zhang. 2023. Exposing attention glitches with flip-flpp language modeling. In Advances in Neural Information Processing Systems 36 (NeurIPS).
William Merrill and Ashish Sabharwal. 2023. logic for expressing log-precision transformers. In Advances in Neural Information Processing Systems 36 (NeurIPS), pages 52453-52463.
William Merrill and Ashish Sabharwal. 2024. The expressive power of transformers with chain of thought. In The Twelfth International Conference on Learming Representations (ICLR).
Thomas Mesnard, Cassidy Hardin, Robert Dadashi, Surya Bhupatiraju, Shreya Pathak, Laurent Sifre, Morgane Rivière, Mihir Sanjay Kale, Juliette Love, Pouya Tafti, Léonard Hussenot, Aakanksha Chowdhery, Adam Roberts, Aditya Barua, Alex Botev, Alex Castro-Ros, Ambrose Slone, Amélie Héliou, Andrea Tacchetti, and 30 others. 2024. Gemma: Open models based on Gemini research and technology. arXiv:2403.08295.
Rohit J. Parikh. 1966. On context-free languages. Journal of the ACM, 13(4):570-
Ofir Press, Noah Smith, and Mike Lewis. 2022. Train short, test long: Attention with linear biases enables input length extrapolation. In Proceedings of the Tenth International Conference on Learning Representations.
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. 2019. Language models are unsupervised multitask learners. OpenAl.
Clayton Sanford, Daniel Hsu, and Matus Telgarsky. 2024. Transformers, parallel computation, and logarithmic depth. In Proceedings of the 41st International Conference on Machine Learning (ICML), pages 43276-43327.
Imre Simon. 1975. Piecewise testable events. In Automata Theory and Formal Languages: 2nd Gl Conference, pages 214-222.
Jianlin Su, Murtadha Ahmed, Lu, Shengfeng Pan, Wen Bo, and Yunfeng Liu. 2024. RoFormer:
Enhanced transformer with Rotary Position Embedding. Neurocomputing, 568.
Ian Tenney, Dipanjan Das, and Ellie Pavlick. 2019. BERT rediscovers the classical NLP pipeline. In Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics (ACL).
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 Goldherg, and Eran Yahav. 2021. Thinking like transformers. In Proceedings of the 38th International Conference on Machine Learning, pages 11080-11090.
12

---

Andy Yang and David Chiang. 2024. Counting like transformers: Compiling temporal counting logic into softmax transformers. Proceedings of the First Conference on Language Modeling (CoLM).
Andy Yang, David Chiang, and Dana Angluin. 2024. Masked hard-attention transformers recog- nize exactly the star-free languages. In Advances in Neural Information Processing Systems 37 (NeurIPS), pages 10202-10235.
13

---

A Logic Preliminaries
A.1 Temporal Logies with Counting
Definition A.1. The syntax of TL[# is as follows:
é == Q. 11 < -0 I Φ1 A 02
a OE
Boolean
Boolean-valued valued formulas
# [ 12
integer-value valued terms
The syntax of [L[#, #1 additionally has counting terms t :== # [Ø]. The semantics of formulas is defined as follows:
w, i F Qo
= Wi o
(3a)
w, =
w.i |
(3b)
w, = 01 22
=
w. i F= Φ and w, Ø2
(3c)
w.i - < 12
1 1
w.l
(3d)
The semantics of terms is defined as follows:
#16] = |(j E [1.4] w.j F= 6)
(4a)
#1 = [(j E [i. w +1
(4b)
(11 + 12)
w.l 1
= w.
(4c)
(4d)
We write }= if /wl } and we say that & defines the language L(Φ) {w Φ).
Definition A.2. The depth of formulas and terms of TL[ and TL| #, # defined by:
dp((.) = 0
dp(-4) = dp(#)
dp(á1 A Φ2) = mpx(d
dp(1) < <12) max(dp((1).dp(t))
dp( (0)# dp( # [Ø]] = dp(()
dp(41 + (2) = max (dpp(()))).((12)
dp(1) = O.
We write TL[#]R l (or TL[#, #))) for the set of all TL[ # (or TL #, #), resp.) formulas with depth at most
We will often assume that any comparison fj < 12 can be written in the form Erer [x] 2 C or Exee Ax Lx] EyER d Lx] 2 C. where L, R are sets of formulas and de. C
A.2 Examples of TL(#}
Recall from Example 2.2 that the Dyck language is defined by the formula
Dyck
[ # (12)) # @ # [[2]]] 0).
The table below shows how this formula works for the string (0)), which belongs to the Dyck language.
subformula
description
Q
is left paren is right paren num of left parens num of right parens balanced
T
T
L
T
1
Q
T
1
T
T
1
T
# [@d
3
3
[e,]
3
1 11
T
T
# #101] #10,1
violates matching num of violations matched
T
1
T
# 1
0
0
0
0
# (1011 =
T
T
T
T
T
# (0011 < =10 11
matched and balanced
T
T
T
T
T
T
14

---

The table below shows how this formula works for the string 0)06 which does not belong to the Dyck language.
subformula
description
Q
is left paren is right paren num of left parens num of right parens balanced
T
Q
1
T
T
1
T
1
# l@d
2
2
3
# [0,]
3
3
# #10 = #10,1
1
T
[[0 [
violates matching
# #1 #10,11
of violations
2
2
# 1 #10 =0
matched
1
1
# [ < #[0,1] = OA =
matched and balanced
T
T
1
1
1
A.3
Extensions to TL #
We will often make use of the following operator in TL[# #]. which does not increase its expressive power affect the depth of formulas, but saves space when writing.
Jthen felse
w. }= Φ
(6 fthen felse) wwd
w. i / d
Lemma A.3 (Yang and Chiang 2024). Any formula o of TL # that uses the ? operator can be converted into a formula that does not use the operator, defines the same language as o and has the same depth as
Proof. Any comparison formula involving the operator can be written in the form
(V/1 ? Ithnn felse) +
Σ t 2 {5(m]
which can be rewritten
Σ 11 2 [E[m]
Telse + 1
Vir
Ethen
This rule can be used iteratively to rewrite all the ? operators out of a formula.
It can also be convenient to allow an unmasked counting operator # and strict counting operators # and #, which do count the current position.
# [b) w.f K [1. [w]] w, Φ) wif = Kij [w] - 1] w.j F Φ) #
# [ e [i+ 1, [w]] w.j
Lemma A.4, Any formula & of TL[#, #1 that uses #, # or can be converted into a formula that does not use #, #, defines the same language 6, and has the same depth as $. Proof. These counting terms can be rewritten equivalently using and #:
# # [ # (o 11:0
# [ = # [6) (6 :
# (b] = # [6] - 0).
A.4 Proof of Lemma 2.9 (definability of piecewise testable languages)
Lemma 2.9. Any k-piecewise testable language is definable TL[#]e lx. and any (2k 1) pipeeecees testable language is definable in TL[ #. k+1
15

---

Any k k-piecewise testable language L can, by definition, be written as Boolean combination of J eexpressions of the form
E'o'E''''''. ...
This is defined by the TL| #] formula of depth k:
# l2 2 1] A 1o. 20,121.
Any (2k + 1) pieeceeee testable language L can, by definition, be written Boolean combination of J-expressions of the form
,n ... E'
We need to show that this is expressible with k 1 nestings of # and #. We do this by first finding the middle symbol 0k+1 and checking to the left and right that the correct symbols appear. First, define depth-k subformulas that check the left and right halves of the J exppression:
L = # or A #1 A #1-- #le., 2 1 ... 1 1 = 1J 2
ΦR # 1m A #12ou. A # #1e om.. 1 2 1.... 2 1] 2 1] 2 I.
Then, defined by the TL[ # formula of depth (k + l):
# Quaas A ΦR 1.
B Transformer Equivalence
In this section and below, the expression I[:] has the value if the statement inside the brackets is true, and O otherwise.
B.1 Transformers
Definition B.1. A fixed-precision number with p total bits and s fractional bits is a rational number of the form 2- where is an integer and -2P-1 S 2P-1 We write F p.s. simply F, for the set of all fixed-precision numbers with total bits and 8 fractional bits.
We represent negative numbers using two's complement. If E [p], the b-th bit of a fixed-precision number x, written (x)b, defined as
(x) = (1
if [x/2b-s-11 odd
otherwise.
If x is a real number, we write roundy or simply round(x) for the greatest element of FP less than or equal
The following definition abstracts away from number of details, but suffices for our purposes (which to prove Proposition B.6).
Definition B.2. A future-masked fixed pixed-precision transformer of depth k is a function T: E" - R.
defined in terms of functions
- pd w(O w(t) wl( p(l); pd - Fd
t 1...,
W Fd - R.
On input w, T(w) is computed as follows:
h (w) = Eww))
(5)
16

---

For ( = I.....k:
(w) = w(()
[h ((--1) ww)
(6)
ky (0 (w) = w
(h, ((-1)) ( (w)
// (w) = w (n (6-1) (w)
(8)
sj (w) = ab 1 (w) kj (2) (w)
(0
Σj round exp (/ (w) v/
9 (w) = round
(10)
(0) Σj= round exp $ij (w))
h (w) = p(() (c (w) + +h, (w))
(11)
where we say Eq. (10) evaluates to the average of all v if the denominator is O, and finally
T(w)= = Wout (8) (w))
(12)
We say that accepts w if T(w) O.
Note crucially that Eq. (10) is written so that even if 2", still possible to obtain nonzero values.
B.2 Proof of Theorem 3.1
Theorem 3.1. A language defined by a formula of TL[#] of depth and only if <BOS> is recognized by a fixed-precision transformer of depth k.
We first define what it means for fixed-precio exed-precision transformer and formula to simulate each other. Definition B.3. We say that a TL[ # formula & simulates fixed-precision transformer' T for all E Σ,
i.i w & = T(<BOS> w);
In other words, w F= & and only if accepts <BOS> w.
transformer T with depth and dimension d simulates formula & of TL[ # if. for all w Σ",
We say that
T(<BOS> w); 0 = w.i w.i
Again, accepts <BOS> w if and only if } d.
We prove the two directions Theorem 3.1 separately: from TL [[ to fixed-precision transformers in Proposition B.4, and from fixed- precision transformers TL[# in Proposition B.6.
Proposition B.4. Let & be a TL[ # formula of depth There exists a fixed-precision transformer To of depth k which simulates db
Proof. This essentially shown by Yang and Chiang (2024), but they simulated [ # using infinite-precision transformers with layer normalization. Here, we modify the proof to use rounding instead of layer normalization to simulate comparison operations."
The case that differs is that of a subformula & = Exe dy # [x] 2 C. Assume that previous layers have computed I[w, j |= x] for x L all positions E [n]. We want to construct a new layer that computes I[w. }= w/] at all positions E [n:]. Use uniform attention and construct the value
projection Wy so that
Σ Ay F x1 - -I[[ = <BOS>]. x
=
'A further difference that store Boolean values (2024) used [+]] for false and [=]] for true. They used this more complicated encoding in order to deal with layer normalization, which is unnecessary here. Our proof could be modified straightforwardly to accommodate layernorm using this representation.
false and for true, while Yang and Chiang
17

---

After averaging, we get
I[..J F -c)
Σ YEL
xx Σ /=1
which rounds to -2 below if d is false, and rounds to 0 or above if ø is true. We can then use the FFNN f to map these two cases to or I, respectively.
If is the entire formula, the output function Wont just takes the computed value I[w,J F Φ) and maps 0 and to and +1, respectively.
The following lemma will be used repeatedly.
Lemma B.5 (Chiang al., 2023). If F: Σ" - is length-preserving g: F F. and there are formulas (FF' such that
w,i (FF (F(w)ib
then there is a formula (g(F)) such that
w,i i= (gg(F)),
(g(F(w))))> 1.
Similarly i is function of more than one fixed-precssion number.
Proposition B.6. Let T be a fixed-precision transformer of depth k. There exists TL[#] formula or of depth k which simulates T.
Proof. We will show that for every activation h (0 and b E [p], there is some formula o "n lo that
such
w.i Φ (h. 1b
( (w)), =
(13)
The construction proceeds by induction on l. For = 0, define the word embedding as
Q
(he
(E(())))==
so that Eq. (13) holds for f O.
Now suppose that Eq. (13) holds for layer l, and consider layer (f+ 1). Use Lemma B.5 on Wº. WK.
and Wy obtain formulas (g 'n, o (k "." and o (vv"") such that
(b.
w. i }= Φ (
= (g (0) (w)) =
(14)
w, i |= o (k!
(k.2 =
(15)
(v (v(( (w)) =.
w.i -= 1 (v!)) w
(16)
Equation (14) in particular allows us write formulas Qqin=q for each q E Fd such that
w,i (q
द.
Next, we want to compute the summands in the numerator and denominator of Eq. (10). These depend on two positions (i and j). whereas a formula of TL[ ## only depends on one position. But since qi can only take on finitely many values, we can enumerate all its possible values. That is, use Lemma B.5 again to obtain formulas
w, j } a ( q.c.b
(ound(exp(( k/((w)) (w)) (12)))/)()))) =1
w.j } ((()
(xpp(e k. (w) (w)) =1
q.h
and then write counting terms A (0)
and B(() that represent the numerator and denominator of (e)
A (0) = Σ
1 9q(== =q ?
2P-1 #
a
q.C.P
Σ 2b-1
a
(e) q.c.b
:0
be(p-1]
B(0=
Σ
$ (0 mq ?
-
[8(()
Σ 1
#
:0
q.P.
4
b
18

---

so that
(A ) =2 Σ
round (exp (1. (
(w) (ww)
(w)( (2()
|s1
(B(0) wi = =2"
Σ J5h
round (exp (q) t0 (w) k (10)w
Next, to define c we need to divide the numerator A by the denominator B(O), We note that B(O) will be nonnegative because exp always returns a nonnegative value. We assume B(() > 0, but the other case is similar. The sign bit is then defined by
= A <0
The remaining bits can be defined, from most least significant, using the grade-school algorithm for long division:
(d))) 22p-1B'0 :) fp-2 1p-1 - (6 (0(6))) 99
f-11 _ +
(0)
1 p-1 pp-1 2 2(- 1 pp-2 2 B())
? ?2p 2()) 0)
fp-3 = 1p-2 - (0 (a!")) ( 1-=
2P 3())
8 1-3 = =1p33 2 2P 2l0)
( !n 2 B())) 0) 11
(e ) 11 2 B((
Finally, we use Lemma B.5 on f to obtain formulas (b satisfying Eq. (13).
C Depth Hierarchy for TL[#]
C.1 Proof of Lemma 4.6 (Commutativity of depth 1)
Lemma 4.6 (Commutativiity of depth 1). For any depth-1 formula 6 of TL(#, PNP), or TL[#, #. PNP]; and any affix restriction (A, Φ) with le(ğ) 2 for all ñ, if the PNPs of a are constant on the middle of (A, Q). then [()) is commutative on the middle of (d, g).
Let |w| and w' 2 with V(w)= "'w"). As such, there is permutation æ:: [n] - [n] such that w/ wx(() for all i, and if a position in the prefix (2))) suffix (e(R)), then x(i) i. We want to show for depth-0 formulas that w, x(i) F= X = F
If X Qo: Since w/ Wx(() we have w, (1) |= X - w'
If x II for some Parikh numerical predicate II: i position in the prefix or suffix, then x(i) = i,
while if i is position in the middle, II is constant. In either case, w. (i) F = w', i = X.
If X "1 or X X1 X2 where X1. X2 have depth 0, then w. x1) F X w',i = x follows from the semantics of - and A.
Any minimal depth-1 formula & can be written, for finite sets of depth-O formulas & and R, as
Σ X
d #
#x1++ + Σ #x
XeR
We showed above that for each X. have (i) - x = w', i x. The terms count all positions, so # [x] = "' The terms only count the last position, and x x()) = n, so w.. 1x .n for all x. Thus, - = w' = d.
Finally, s -hi or & = &1 d2 where 11, Φ2 have depth at most 1, then w, x() |= & - w'. . |= & again follows from the semantics of - and A.
19

---

C.2 Proof of Lemma 4.8 (Cropping Lemma for TL(#))
Lemma 4,8 (Cropping Lemma for TL[ # D. For any formula & TLI PNP] and any accommodat- ing family of intervals I: Ni - I El) such that the PNPs of & are constant I, there exists an accommodating family of intervals I': Ni - I (N(E)) such that (ñ) sticks only to the top (and no other side) of (()) for all ñ E N and all of the minimal depth-1 subformulas (and PNPs) of are constant on I', Additionally, there exists such an I' such that I' (ī) sticks only to the right of I()).
Let 11, 2/. .... be the minimal depth-1 subformulas of Φ. That is, for C E [c].
Σ xx 2 Ce. rEL
UC=
Because any PNPs in each v are constant on I, each th defines a half-plane in # [Qal and # [[2,], where w. } the iff w[l i]] lands in the corresponding half-plane. Then & is Boolean combination of these half-planes. Thus [w[[1: i]) and 4'w [[[ : (')) both land in the same half-planes, they will both satisfy & or both not satisfy 6.
We will show that for desired size 3, there is ((î) sufficiently large such that, there is a subinterval (') with size at least 3 sticking only to the top of ((ī) (and no other side).
Let be the minimum absolute slope of any non-horizontal boundary line, and let h be the maximum b-intercept of any horizontal boundary line.
For any 3 = (Sa. sb), 3' = (6) = (sa + 2, sb + I), and choose ń such that I(7) has size at least [3 max(s,,/m / s,)) h + s/11. Our goal is to find a subinterval ('ii) that has size 3", sticks to the top of [()), and does not cross any boundary lines.
Let Ic be arbitrary subinterval of size [3 maxxss,/m,s$ s.), s that sticks to the top of I(ñ). We will prove by induction on c: Given an interval le with size [3 max(s', (o,, sa). s/2)] that sticks to the top of ((z) and set of c boundary lines, there a subinterval I' (ñ) of size 3' that sticks to the top of (ñ) and does not cross any boundary lines.
The base case
is trivial: There are no boundary lines cross, and s s max(s' /, s'),, so choose any subinterval of In with size 3", and shrink I unit from the left, bottom, and right obtain a subinterval (") of size ă that does not to stick to the left, right, or bottom of lo-
If O, take an arbitrary boundary line and call it & and let le be interval with size [3 max(s',/m, /m,, s.))),)))
If C is horizontal, it must have b-intercept at most h, so there must be at least s space above it inside I(A). So Ie does not cross l, and neither does any subinterval of Ic. Arbitrarily choose l--1 to be the middle third of Ic. and use the induction hypothesis on I--1 and the remaining boundary lines.
I())
l
l--1
If é is not horizontal, it must have absolute slope at least m. The part of le that crossed by must have width at most s m, whereas Ie has width 3 max(s', ( m/.s's)s s'g) 2 35/, m,, either the left third ///m
20

---

or right third of lc does not cross t. Choose lc-1 to be that third, and use the induction hypothesis on ---1 and the remaining boundary lines.
C
I(
le
le-1
s/g/m
35///m
A similar argument (with and swapped) can be used to find an ('i)) sticking only to the right of I(ñ).
C.3 Proof of Lemma 4.9 (Reduction Lemma)
Lemma 4,9 (Reduction Lemma), For any depth-k formula & of TL[# PNP] (or TL[ #, PNP]<) and affix restriction (d, @), the PNPs and minimal depth-1 subformulas of constant on the middle of (d, Q). then there is a formula s' of depth (k -x-1) 1) of TL[#, PNP] (or TL #. #, |N resp.) that defines 2L) o. and the PNPs of are constant on the middle of (2. g).
Let te be the minimal depth-1 subformulas of t. Each te for 1 s s c is the form
Σ # XEL
Ve
Φ is formula of TL PNP] & or
ve + Σ
Axll 2 Cc. XER,
XEL
& is a formula of TL[# #, PNP]
In either case, de is constant the middle of (A, g), meaning that for given स. each thr has the same truth value for w E 2 with P((w) = at positions such that [a) i s || [p())) The truth value of vr. given the restriction (2, Ø), determined solely by the Parikh vector of the word and the position i at which it is evaluated. Thus there is a PNP M, which "hard-codes" the behavior of dee Moreover, Mj constant on the middle of (d, @) because the is. Thus we replace the depth-1 formula de with the depth-0 formula My- Call the result éred-
The last step is write a formula that checks if w E 2 For E, define a Parikh numerical predicate rI, that is true at position if position belongs to the prefix/suffix and the symbol at that position of the prefix/suffix o::
((P(w) =o
i (W)))
w IIr
=
e (((()))- =o 12 |w| (el-l(
otherwise.
21

---

This is Parikh numerical predicate because it is conditioned only on the position and the Parikh vector of w. Moreover, constant on the middle of (d. Q).
Then we can write the following formula, which checks whether w 2 by checking whether w at every position i has the correct prefix/suffix:
aff
[ITa Qa) (I A 2b)] #[T))
Finally, define the new formula
6' red A Daff
which has depth (k 1) and defines .l. Note that since aal does not contain #, if & did not contain # then ø' does not either, so if & TL #. PNP] then o' E TL[ KNP]
C.4 Proof of Corollary 5.2
Corollary 5.2 (Corollary of Theorem 4.10). A depth- + 1) TL[#] formula can solve the next-token prediction problem for Lk+3, but no depth-k TL[ # formula can.
First, we show that the prediction problem for Lg43 solvable in TL[#]<+1 To decide whether to predict 0 1, we need to check that starts with and has exactly (k + 3) blocks so far: if so, predict 1; if not, predict 0. Since we may assume that the entire string w belongs to LR+3, we know that it starts with block of a's and there are more than (k 2) blocks after that. We can check blocks through (k + 2) by checking if w belongs to B&+1 (see Eq. (2)), and we can check the last block by testing whether the current symbol is (if k is even) or b (if is odd).
More formally, let &B.. define B by Lemma 2.9, and let
BBa A Qa
k is even
d A Qb
k is odd.
Then, for all w E L2+3 and s s [wl we have that
w[1 i] E LL+3 =
In the other direction (the prediction problem for L243 is not solvable in TL[#]k), suppose we had depth-k formula & TL[ # l such that for all LR+3 and 1 s w[] } Φ < w[l i] LL+3. Assume that & is even (the odd case is similar). We can use Lemmas 4.8 and 4.9 just as in the proof of Theorem 4. 10 obtain an accommodating affix restriction d ( L. and @1 (ñ) e a*, as well as a depth-1 formula Φ1 E TL PNP],, which defines a, (L4+3) and only uses PNPs which are constant over (1).01)
Since (di, @1) is accommodating, choose ñ so that the middle has sa 2 occurrences of a and sb 2 occurrences of b. Construct strings
(1) a -000-- bagi(n)
w' A1(bbbb (a)
which both belong to LR+3 (because the prefix d1 (ñ) has & blocks ending with block of b's and the suffix @ (π) is all a's, so both strings have (A + 3) blocks). Let = [2 (π) + s. + + lei that is, the position of the last symbol of e(ī). Then w [1 i] L2+3, while w'[1 i] & L2+3. But by -= Φ1. This is contradiction, so we conclude that no formula & with depth & can solve the prediction problem for L243.
Lemma 4.6, we have w[] i] F= Φ1 = w'l1
If k is odd, the argument is the same, except with and swapped.
D Depth Hierarchy for TL[#
We can also obtain strict depth hierarchy for TL #, #]. The key observation is that to modify Lemma 4.8 for TL[#, #, # we use the fact that the Parikh vector of word fixed we can rewrite # in terms of and n.
22

---

Lemma D.1 (Cropping Lemma for [], cf. Lemmas 1-2 of Behle et al., 2009). For any formula & TL #. PNP] and any accommodating family of intervals I: N - I (NIE)), such that I(π) S [ ñi] and the PNPs of & are constant on I, there exists an accommodating family of intervals I Ni + I(ElE)) such that I' I') S In) but does not stick to any side of ((n) for all and all of the minimal depth-1 subformulas (and PNPs) of d are constant on l'.
Proof. Let 1...1........................1 ...........4.................... Me be the minimal depth-1 subformulas of Φ. That is, for l [c],
Ve
Σ 2x + rEELi
Ea PER
2 Ce..
For any size 3 = (sa, 8b) e N let 3' (sa 2, sb + 2). We may, since is accommodating, set ň such that ((i) has size least (2 s'a 2c s/)).
Then we rewrite the as
Xx # [x] KELL
Σ
+
Σ HER,
1 -FLX)) C
na +
if X T if x Qa
Aaa
Cx
1b 0
x 2b
if X T.
(Regarding the strict counting operator #, see Lemma A.4.) Now each the defines half-plane over # [[Qa] and # [Q>1, where w, }= the iff w[1 i] lands on the correct side of the half-plane. Then & a Boolean combination of these half-planes. Thus w[1 i] and w'[1 r'] land the same half-planes, they will both satisfy & both not satisfy d.
Next, we prove that can find an interval with size least 3' on which all the the are constant, by induction on c. The base case = 0 is trivial. For с O, we split the interval into four quadrants, each of size (2 S'g, -0-12())) sg)). Since line can only intersect at most three quadrants, there is one quadrant that is completely contained in the half- salf-plane for &he or completely outside. Use the inductive hypothesis on this quadrant and the remaining half half-planes for .........c.1..
Finally, shrink the interval slightly to obtain an interval I' (ñi of size ë that does not touch any side of ((n).
Then, order to prove a depth hierarchy for TL # each step of reduction needs to eliminate a block on both the left and the right.
Theorem D.2. Define the family of languages DA L2L-1 = (a* b+ lat. Then D2+1 is definable TL[#, #JR+1 but not in #L #)a-
Assume, for the sake of contradiction, that there exists some depth & formula & E TL[# #] which defines DR+1- Let I (n) [(1, 0), 7 (1.0), (ñ) @ (ñ) a, and Φx sb Note that (Ak, @x) is accommodating, and Φx has no PNPs.
Proof.
For l = k 1, k ...... we will define the following, writing R for the reversal of L, that is, the set of reversal of strings in L.:
1. A accommodating family of intervals (ñ) S (7).
2. An accommodating affix restriction dy (n) E Lę-z+1 and ( RE-1+1
3. A depth-& formula de E TL[# $1 PNP], which defines 2, (Dx+1) and only uses PNPs which constant over (de, Qc).
We use the following iterative procedure:
1. Using Lemma 1. find accommodating family of intervals lt such that (e( S Ie+1 and does not stick to any side of (π) for all î, and the minimal depth-1 subformulas of de+i are constant on I.
23

---

2. We choose an affix restriction whose middle is 4e, as follows. Let [i,}] Le+1 (i) and
1 [r. (ñ); then
Ir-1
odd
2r (1)
Ac(+)
Ac+1 bilo 1--- even
bli-Pla @c+1 ald-ila ai--ilabii bli- (e)
k odd
er
k - f even.
Because (ñ) Lk-e-1+1 and It (ñ) does not stick to any side of (e)1 we have that de E Lk-C+1- Similarly, or Lk-et1". R.
3. Using Lemma 4.9 we can find depth- formula de of TL[ #, PNP], that defines 2 (Dx+1)er er and only uses PNPs which constant on (de, 2c).
At the end of this procedure we are left with
An accommodating affix restriction d1 (ñ) & Lx and @ı E L.
A depth-1 formula Φ1 E TL[# #, PNP]: which defines a (Dx))) and only uses PNPs which are constant over (2).11)
Since (d1, 21) is accommodating, choose ñ so that the middle has sa 2 2 occurrences of a and 2 occurrences of Construct strings
w = (a)aa ((( w' = A1())aaaa - (0) (b)
The prefix (n) and suffix @1 (ñ) both have & blocks, and d1 (ï) ends with the same letter that (π) starts with. So w has (2k + 1) blocks and is therefore D while w' has (2k + 3) blocks and is therefore not in DR+1. But by Lemma 4.6, we have w -= Φ1 = w' |= Φ1 This is contradiction, so we conclude that no formula o with depth can define DR+1-
Finally, by Lemma 2.8, D2+1 = 12x+1 is a (2k + 1)- pieccewise testable language. Thus, by Lemma 2.9, D is definable in TL[ #]
E Equivalence of TL[# # # to Other Formalisms
The logic TL| #, #] is equivalent to two other formalisms studied in the literature. The multiple different ways of characterizing this class of languages suggest that this a robust class languages.
Definition E.1. The syntax of MAJ2[ <]
is follows:
= (x(x) 1x(r)
Ix<ylye <x
1 11 A d2
dm) (AJ bm)
m 2 I.
The semantics of formulas is defined by the relation w. }= &. where & is a partial function from variables in {x.y) 3 to truth values in (0, 1}. We write ε[x + for the function E' such that (x)

---

and () = -(y), and similarty for E H jl.
w.S F (x)
We(x)
(17a)
w.5 F (+(
wgl)) =0
(17b)
w.S y
5(x) < 5())
(17c)
w.g F <x
5()) < <((x)
(17d)
w.E F =
w.5 # $
(17e)
w.g + Ø1 A 22
w. F $1 and w. & T= 62
(17f)
lw|
ww/m
w.g - MAJx (Ø) 6m)
Ex i] + 0r)
(17g)
2
[w
Iw/m
w.g += MAJy (61.
dm)
Tw. /I = Φc
(17h)
2
J=l
We write w }= & to mean w. 0,O -= Φ. and we say that a closed formula & defines the language [()) [w w F d).
Definition E.2. The depth of formulas and terms of MAJ2[<] is defined by:
dp)(.-(x) dp((Qr())) =0
dp(x <) dp(y <x) =
dp(-Φ) dp(Ø)
dp( A 62) max (ax
(é).. =
=
We write MA for the class of all formulas & such that dp( s k.
Lemma F.3. Any formula & of MAJ2[<] that uses V or can be converted into a formula that does not use V or 3, defines the same language as &, and has the same depth as &
Proof. These quantifiers can be rewritten equivalently using MAJ:
[x[Ø] = MAJ (Ø. T)
[x[ -MAJ,( (-0,
Now, we show the equivalence of TL #] with MAJ2[<] [<]. First, show how translate TL # # MAJ2[ <) (Theorem E.4) and then how translate MAJ2[<] to TL[#, # (Theorem E.6).
Theorem E.4. Let & be a formula of TL #, #1a. Then there exists a MAJ2| [ formula &' (x(x with one free variable such that w, b w. w d' (x) for all and < [w].
Proof. We define a transformation M. [.] from formulas of TL[ # formulas of MAJ2[<] with one free variable x:
M, [ (x)
M, [-6] = MM
My (1 Φ2] M, [bill a Mr [d]
Any comparison formula can be written in the form
7
E=1
where 1t and 1/ are terms. Since this tests whether the sum is greater than 0, whereas the MAJ quantifier tests whether the sum is greater than half of its maximum possible value, need to pad
25

---

the positive terms (tt) with an equal number of trivially true formulas. Similarly, we need to pad the negative terms (fy) with an equal number of trivially false formulas.
m
ni
M
0
MAJ, (Fx [1]. ...... F.....T..II1..... (m T, Fr 1ill
Fx I'' 1
(18a)
Tx [ (y x M, Iol)
(18b)
F. [[ (y A My [Q]])
(18c)
T [+ 11
(18d)
Fx [1] xy)
(18e)
To see why this works, we can show by induction that for all strings w, assignments g, formulas Ø, and terms i, both of the following hold:
w.5 + M₂ [o] = wxf(x) F
(19a)
Tw.ely F =))((()
(19b)
The interesting case is
m
w,E = Mx
Σ
11
1 0
W, F MAJ, (Fx [1 T F. T, FFx [1]]
-Fx m1
[w
(776)
[
f. F.
Fx I' + +[=]]
[w](m
1w1
m
Σ ww& - F 11
Σ
Il + == F.
[(ll
>0
m'
(1z) mxE(x)
(10 wxE(x) > 0
m'
(4c)
w. (x)(x)
F
>
tt
11
>
1=1
t=1
Observe that formula of the form M2 [ JJ may only have free variable because in Eq. (18a), MAJ,, binds y.
In the special case of comparison formula of terms, the resulting MAJ2[<] formula will be closed.
Proposition E.S. Let Mx |I be as in Theorem E.4. 6 is of the form #[v] then M2 [ is closed.
Proof. Recall that formula of the form M, [ may only have free variable because in Eq. (18a), MAJy, binds y. But the special case of M2 [# O]l is closed, because F, [#[W]] My T (Eq. (18d)) only has free variable y, and Eq. (18a), MAJy binds y.
Theorem E.6. Let (xxx be formula of MAJ2[<]a with one free variable Then there exists TL[ #. #) #1& formula de (x) such that for all w and all [[w]], we have w,x i ((x) = w.i FF 6..
26

---

Proof. We define a transformation Tx that transforms formula of MAJ2[<] with free variable x into formula of TL[ #].
[x) = Qo
T. [=]]((x]] = [Tx]((
Tx T (x) x2(x) = A
Tx MAJy (6) (x, y), 2m (x,
Σ (o
Σ c (- [E(m]
tE[m]
The transformation Ty is defined similarly.
The transformation Cy [ (x, y) turn, can be read as "count the number of positions y that make & (x,y) y) true." Without loss of generality, assume that & is in full disjunctive normal form, that is, & Vealme e and most one of the de can be true at the same time. Then we define
Cy
(x(x)= (E(m')
(x(
Σ [ve(())] CE(m²)
Each of the de be written conjunction of literals with free variable x, literals with free variable y, and possibly comparison < y, < y,
x, or < x. Then we define
Cy [ver(x) A #12(7) Ax < Men # T, [+ :0
Cy [vee(() A (12(y) ^x = Men # [T [b22())]] :0
Cy L(ee(x) A (12(F) < <x] = Men # TT [+ :0
Cy [ver(x) A (12(2)) A M/n ? # T [()(())]] :0
Cy [Vr(()) v)a()) thn ? [T [,>e(y)]]
:
The transformation C₂ defined similarly. (Regarding the strict counting operators and ## see Lemma A.4.)
Theorem E.7. L(TL #)) L (MMJ2 <)) = [(FO[
< uniform LTC"). Furthermore, for all 2 O we have TL #} MAJ2l R+1 and MAJ2| <| TL[ #]k-
Proof. The equivalence L ((MA2214) [(FO|<)- LTC") was shown by Krebs (2008, The- orem 4.33).
We will show the following:
. L(TL[ #1x) E L(MAJ2 [<]x+1) using Theorem E.4.
L[MAJ22 <<]x)) L (TL H.. #lx) using Theorem F.6.
If is formula of TL[ # lk then by Theorem E.4, there is an equivalent MAJ2[<]e formula d'(x). This, in turn, is equivalent to the following closed formula:
8" (- > x) (xx)..
This accounts for the end-satisfaction of TL #. formulas, but adds level of depth to the MAJ2[ <] formula.
Conversely, if is closed formula of MAJ2[<] <]x, we may think of it as having one free variable so by Theorem E.6 below, there is a TL #] formula equivalent to ø.
This theorem combined with our Theorem D.2 implies the following answer to an open question.
Corollary E.8. The circuit depth hierarchy for Fum=o-um LTC circuits strict.
Proof. By Theorem D.2 and Theorem E.7 we know that D [(MAJ <))). On the other hand, let Φ be the TL[ 4, # ll formula given by Lemma 2.9 for Dg. Then apply Theorem E.4 get formula & of MAJz[<], < that defines Dx. Since dy of the form #[W] > 0, by Proposition E.5, & is closed. Thus, the depth hicrarchy for MAJ2[ <] is strict.
27

---

By Theorem of Behle et al. (2013), F LTC* circuits form a hierarchy in the circuit depth iff MAJ2[<] formulas form hierarchy in the quantifier depth. Their theorem states that there exists a constant c such that a circuit depth can be expressed as a formula of depth k c, and formula of depth k can be expressed circuit of depth ck.
F Position Encodings
In this section, we extend the results Sections 3 and 4 to handle position encodings. On the logic side, we extend TL[ #1 with new predicates MOD,,. which test whether the position is congruent to modulo m, and a new operator Yœ, which tests whether & is true at the previous position. On the transformer side, we consider the original sinusoidal position encodings, as well as RoPE (Su et al., 2024) and ALiBi (Press et al., 2022).
TL[# #. Y, MOD]
We extend TL[#] to a more expressive logic, TL[#, Y, MOD] (which is equivalent to C-RASP[local, periodic] of Huang et al. (2025)). The new syntax rules are:
Φ : Yá MOD
The semantics of the extensions are defined follows:
w i + Yá
w, (i - F & and i >
(20a)
w, = MOD
isr (mod m).
(20b)
F.2 Depth Hierarchy
To prove a strict depth hierarchy for TL[ # Y, Y,MOD], we first we define an intermediate step to simplify the construction. formula is in Y-normal form if Y only appears around atomic formulas. That is, the set of formulas in Y-normal form is defined by the following grammar.
Φ := fi 12 -61
Φ1 $2 v
:: Q MOD YvI
[b]
11 + 12
Below, we will use the shorthand, for any 2 O,
Y" Y Yo
times
Lemma F.1. For every formula o T, Y, YOMOD] there exists a formula d' TL Y, MOD] such that w. }= 6 = wii & for all w E E", and o' is Y-normal form.
Proof. Define transformation No L.II, where c 2 O, applying to both formulas and terms, that pushes Y's inwards. The superscript keeps track of how many Y's s are being pushed. For any formula é, we have i.i t= = w,i-c N [ and for any term have yw.i No [ w.t-c.
No [e.] ] = Y Q. N [MOD, m Y MOD"
N' [-6] = -No [+]
N [ Φ2 = N [Ø1]] No [Ø2]]
N' [n < = N [n]] < N [
N' [Y$] ] NC+1 [+]
N [[o]] [N' [+]]
N f1 + 12 No [n] No [ta]
N [ =
Now for any formula of TL Y, MOD]e, easily verified that &' No [ is of the same depth and in the desired normal form.
28

---

W
W1
W22
W3
JI
W
e
f(w)
i
:
e
e
e
Figure 5: of many formulas on string w of length n can simulate a formula & on string f(w) of length x([w 1).
Lemma F.2. Let be a formula of TL[#. Y. Y.MOD] over alphabet E (e) for Σ. There exists formula 6' TL le and mapping (for some x 2 1)
-
WIw2 Wn e' w x-1
such that for all w E E", f(w) F = #
Proof. First, let M be the least common multiple of all moduli used in & (or M 1 if there none), and let Y be the Y-depth of d. Set x M(Y + 1). This ensures that x = mod m for any modulus m, and which important conditions for the following proof.
Intuitively, the technical challenge here that in w we can index only [w] many positions, but to simulate formula over f(w), need to simulate procedure which index x(we] 1) many positions. We address this by defining a transformation T, II-II. for y [x], from formulas of TL[ #, Y. MOD] to TL At position i, Ty [ simulates & at position (xi + y) (and similarly for terms t). That is, for all and and for all strings and E [[w]],
f(w)xi+y = w.d F [
f(w) = 11
(21)
The first positions f(w are not simulated; they are dealt with specially below. In the end, Eq. (21) will ensure that f(w) } 6 = w }= &x. Intuitively. this construction "stores f(w) vertically" at each symbol w; w, and thus we can simulate, in place, the value of & at each position of (w;). We can visualize w W1W2W3 ... wn and (ww as in Fig. 5, with each f(w;) viewed as vertical column of symbols in an array. We can read w left-to-right, and read (ww) up-to-down within each column, and left-to-right across all columns.
29

---

Without loss of generality, we assume by Lemma F.1 that ø is in Y-normal form. Then we define the following transformation:
Qa y-c=1 otherwise
or EEE Σ
1
y-c=1 otherwise
T y-cEr mod
Ty IY'MOD,
otherwise
Ty [-- -T, [
T (6 A = [ AT, [+]]
T = [n] [2]
[*
Σ
,' 001:001 + E
Σ y'E[x]
#ITy [oll
Σ
Ty T ?1:0
x
[rlly
T In +/2] = 11 + + r
[1]=1
We prove Eq. (21) by induction on the structure of Φ.
If Φ = Q² for o ( -f c- then
f(w) Y = f(w)xi = = w/
But yf 1, then
fw)) = f(w)xit--==0 =o ==
In either case, and whether or e, Eq. (21) holds.
If Φ Y"MOD,, Because is multiple of every m, have
f(w). + YOMOD,
xi y + MOD,,
y-C mod
w.i - Ty MOD
I = # [[]]: We split the count into three parts,
(# (#16))(0).x44
= Iij e [xi + y) [(w). क)1
= [[/ [1,x] f(w). F l)
+ Ii e L, f(w). } Φ
+lli [xi+ |xi+ 1,x+ f(w). *
In relation to Fig. 5, the first term sums the first column, the second term sums the columns corresponding to W Wn-Wn and the third term sums the last column (corresponding to
30

---

Wn). Taking these three terms one at time:
10 [
F o)
Σ ,y F 2
y'[[x]
K0 e [x + x,x [(w), /= 6)
Σ
Hi [1, 1] ((w), +y F #
y'
ind. hyp
Σ
[ [1, 11 w. Ty [01)
y'E[x]
w.
Σ IT
[+]]]
Kj e [xi+ 1,xi +J f(w). -= H6 e [1. y) f(w). +y #1
ind. hyp.
16 E [1.y] wi F Ty [+]l
Σ EEE
Ty [b] ?1:0
The remaining cases are straightforward.
By construction, T. [ has the same depth as Φb Setting d' Ts [ completes the proof.
Finally, we show the depth separation for TL[#, Y, MOD]. Let Eg the language formed by allowing unlimited insertions of anywhere into strings of Lg. In other words, Eş del (Lx). where del: (E U {e))) - E' is the string homomorphism given by del(or) = for E Σ and del(e)
Theorem F33 Let k > 0. The language Ex+1 is definable in TL Y, MOD] k+1 but not in TL # Y, MOD]
Proof. Suppose @ E TL Y, MOD] defines EX+1. By Lemma F.2, there is a string mapping and a formula d' E TL[ [[ such that for all E E", f(w) }= $ = -= d'. However, this implies that }= 6' w L2+1, which contradicts Theorem 4.10.
F.3 Sinusoidal position encoding
The original definition of transformers (Vaswani al., 2017) used sinusoidal position encoding, which redefines Eq. (5) as follows. Assume d is even. Define the rotation matrix
cos 0
sin 0
0
sin 0
cos 0
0
0
0
cos 02
sin 02
R(Ø) = round
sin 0g
cos 0g
(22)
0
0
0
0
cos 02/2
sin 0//2
0
sin 0a/2
cos 0a/2
31

---

where for c [d/2], 0. = 10000-(ce1)). Then
sin 0
cos
h (0) (w) -((w) R(0)
:
(23)
sin 0 cos
For the rest of this section, let us assume that in a sinusoidal position encoding, all the angles are rational (that is, rational multiples of π), so that the encodings periodic. Then we extend Theorem 3.1 to transformers with sinusoidal positional encoding and TL[ #, MOD], using exactly the same technique Yang al. (2024, Cor, 8).
Theorem F.4. A language I. is defined by formula of TL[#, MOD] of depth k 2 1 if and only if <BOS> recognized by depth-k fixed-pre preciison transformer with sinusoidal positional encoding.
Theorem F.S. A depth-(k 1) fixed-precision transformer with sinusoidal positional encoding can recognize E but no depth-k fixed-precision transformer with sinusoidal positional encoding can.
Proof. Firstly, Ex+1 is definable by fixed-precision transformer of depth k + 1 even without sinusoidal positional encodings. Secondly, by Theorem F.4, every language definable by fixed- precision transformer with RoPE is definable in TL[ #. MOD] but by Theorem F.3, Ex+1 is not definable in TL[ MOD]
F,4 RoPE
Rotary Positional Embedding or RoPE (Su et al., 2024) is currently the de facto standard method for incorporating positional information in transformers (e.g., Mesnard et al., 2024). It modifies Eq. (9) as follows:
$ (w) R(Ō) (0 (ww) (())k/((()
(24)
where R is as in Eq. (22).
Again, let us assume that the angles in 0 are rational, so that the transformation R(ōy is periodic in i. This ultimately allows simulation using MOD.
Proposition F.6. Let T be depth-k k predcireciiion transformer with RoPEs. There exists a depth k- formula of TL[ MOD] that simulates' T.
Proof sketch. This is a straightforward adaptation of Proposition B.6. The rotation matrices R R(ō) and R(Ø)) can be computed in fixed-precision using Lemma B.5 and MOD, as in the proof of Yang al. (2024, Cor. 8). The attention scores S R@0 qr R(0)kk, ky can be computed using Lemma B.5 and the trick of enumerating all possible queries, as the proof of Proposition B.6.
Theorem F.7. A depth-(k + 1) sxeed-precision transformer with RoPE can recognize Ex+1, but no depth-k fixed-precision transformer with RoPE
Proof. Firstly, Ex+1 is definable by a fixed-precision transformer of depth + even without RoPE, Secondly, by Proposition F.6, every language definable by a fxee-precision transformer with RoPE is definable in TL[ MOD] but by Theorem F.3, Ex+1 is not definable in TL[ MOD]
F,5 ALiBi
ALiBi stands for Attention with Linear Bias, introduced by Press et al. (2022) as a method for improving length generalization in transformers. It decreases the attention scores (Sij) by amount that scales linearly with the distance between the key and query positions and j. That is, it modifies Eq. (9) to:
(w) (w) (0 (w) (w) - a. fi-
(25)
First, we note that there is some distance beyond which ALiBi rounds the attention score to This ultimately allows simulation using Y, as the following shows.
32

---

Lemma F.8. Let be fixed-precision representationn and let a > 0. There exists Da such that for all j Aa and E F we have that reund(exp(x a(i- 0.
Proof. The attention scores (Sij) are bounded above by some > 0 (Chiang et al., 2023, Prop. 21). Recall that the smallest positive number in is 2 so there score so = log 2-= such that round(exp so) O. Let A (S sa) Then if j 2 Au. then round(exps5
0.
Proposition F.9. Let T be a depth-k fixed-precision transformer with ALiBi. There exists depth-k TL Y] formula dr that simulates T.
Proof sketch. If a O, we can use the same construction as in Proposition B.6. If a O, we cannot use the trick of enumerating all possible queries, as in the proof of Proposition B.6. Instead, by Lemma F.8, there is finite window [ Aa.i] which receives nonzero attention. At query position we can use formulas & (k?") "."" Y d (k. ( "n ................................ y (x!)) ),
obtain the keys positions - 1.-....... Ag. We can then use Lemma B.5 to compute the attention scores according to Eq. (25).
Theorem F.10. depth-(k 1) fixed-precision transformer with ALiBi can recognize Ex+D. but no depth-k fixed-precision transformer with ALiBi con.
Proof. Firstly, Ex+1 is definable by fixed-precisiee precision transformer of depth k even without ALiBi. Secondly, by Proposition F9,, every language definable by fixed-precision transformer with ALiBi definable in TL[ Y]k. but by Theorem F.3, Eg+1 is not definable in TL[ [, YJk-
33

---

G Index of Notation
scaling factor for ALiBi (Appendix F.5)
A, B
terms for numerator and denominator of attention (Proposition B.4)
Ak. Bk
languages (Eq. (2))
a, b
numerator and denominator sumdiv (Section 2.1)
a.
symbols (E Σ)
a.
formulas for numerator and denominator of attention (Proposition B.4)
b
bit number (e [p], Proposition B.4)
threshold linear inequality (Appendix A.I and Proposition B.4)
C
transformation for counting (Theorem E.6)
attention output vector (Definition B.2)
number of minimal depth-1 formulas (Appendix C.2 and Lemma D.I)
coordinate (E [d], Proposition B.6)
constant (Corollary E.8)
DE
language separating TL| #, #] depth levels (Theorem D.2)
d
hidden dimension (Definition B.2)
window of positions [i A] (Lemma F.8)
e
neutral letter (Lemma F.2)
Ex
Lk with a neutral letter (Theorem F.3)
E
word embedding (Definition B.2)
F
transformation (Theorem E.4)
function - (Lemma B.5)
F
all fixed- sreed-preiisoo numbers (Definition B.1)
function computing FFNN (Definition B.2)
g
funetion F - F (Lemma B.5)
b-intercept (Appendix C.2)
hidden vector (Definition B.2)
learning rate (Section 5)
interval (family of intervals) (Definition 2.5, Lemma 4.8, and Theorem 4.10)
of all intervals (Definition 2.5, Lemma 4.8, and Theorem 4.10)
endpoints of interval (Definition 2.5, Lemma 4.8, and Theorem 4.10)
position (e [m]) (Section 2 and Appendix A.1)
K.k
key matrix/vector (Definition B.2)
depth, number of blocks or pieces (Definitions A.2, B.2 and E.2)
language (C Σ Section 2)
L
language (Eq. (1)) separating TL[ #1 depth levels (Theorem 4.10)
L
language recognized/defined by a formula or logic (Theorem E.7)
E
of bodies of left-counting terms (Appendix C.1 and Lemmas 4.8 and 4.9)
loop from to (Theorems D.2 and 4.10) index of half-plane or minimal depth-1 formula (E [c], Lemma 4.8)
C
C
index of formula in MAJ, term in sum (E [m]. Theorems E.4 and E.6)
t
line (Lemma 4.8)
A
prefix family (Definition 4.1)
A
coefficient in linear inequality (Appendix A.I, Proposition B.4, and Lemma 4.9)
M
transformation (Theorem F.4)
M
Parikh numerical predicate (Lemma 4.9)
|Σ], only used when |Σ| would be circular (Definition 2.3)
m
significand of fixed- -recissnn number (Definition B.
34

---

slope (Lemma 4.8)
number of formulas in MAJ, terms in (Definition E.1 and Theorem E.4)
n
length of w (Section and Appendix C.1)
7
Parikh vector of w (Sections 2.3 and 4)
E
truth assignment (Definition E.
P
number of bits (Definition B.1)
PNP (Parikh numerical predicate) (Definition 2.6 and Lemma 4.9)
π
function corresponding to PNP (Definition 2.6)
permutation of [n] (Appendix C.I)
Qo
symbol predicate (Appendix A.1 and Definition E.1)
fixed-precssonn value of q (Proposition B.6)
query vector (Definition B.2)
rotation matrix (Appendix F.3)
R
set of bodies of right-counting terms (Appendix C.I and Lemmas D.I and 4.9)
suffix family (Definition 4.1)
size of interval (Definition 4.3 and Lemma 4.8)
s
number fractional bits (Definition B.1)
Σ
alphabet (Sections 2 and 2.3)
symbol (E Σ) (Section 2.4)
transformer (Section 3)
transformation (Theorem E.6)
t
term (Appendix A.
value (Definition B.2)
Parikh vector (Section 2.3 and Lemma 4.8)
Wk. Wo. Wv, Wout
weight matrices (Definition B.2)
w
string (E Σ¹) (Section 2 and Definition 4.1)
fixed-precision or real number (Section 3)
padding size in reduction proof (Lemma F.2)
x.
formal variables (Definition E.1)
y
index in reduction proof (Lemma F.2)
formula (Section 4 and Appendix A.1)
formula, esp. body of counting term (Lemma 4.8)
Y
Parikh map (Σ" - 2 (Section 2.3)
formula, esp. comparison (Lemmas 4.8 and 4.9 and Theorem E.6)
0
angle for rotation matrix (Appendix F.4)
35

---

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 claimed equivalence between fixedprrcisiion transformers and C-RASP shown in Appendix B, the claimed depth hierarchy was shown in Section 4.5, and the claimed empirical evidence was provided in Section 5.
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 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 it is clear that these goals are not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: The section Section 6 summarizes the limitations of our work. Theoretical limitations of our model compared to other works are discussed in the introduction, and empirical limitations are discussed in Section 5.
Guidelines:
The answer NA means that the paper has 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 well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or speech-to-text system might not be used reliably provide closed captions for online lectures because it fails 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 fairesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't acknowledged
the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an 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
36

---

Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
Justification: All lemmas and theorems have proofs in the appendix besides Theorem 4. 4.10, which has proof in the body of the paper. Throughout the paper, intuitive explanations and proof sketches can be found. The only secion where proofs are omitted is Appendix D, but this is because they are essentially identical to the proofs of Lemma 4.9 and Lemma 4.6.
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 or referenced in the statement of any theorems.
The proofs 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 provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix 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 of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
The definition of the formal language LA was given in Lemma 2.8. Our method of generating strings from La well as the transformer training setup are all fairly standard and were described in Section
Justification:
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 to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make 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 to 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 a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS 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 the architecture clearly and fully.
model architecture, the paper should describe
(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).
37

---

(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 be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, described in supplemental material?
Answer: [Yes]
Justification: The code will be provided in the supplemental material, and made publicly available in github repo sometime in the future.
Guidelines:
The answer NA means that paper does not include experiments requiring code. Please see the NeurIPS code and data submission guidelines (https://nips.c
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" is 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 the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https: / //nips. cttpssccccpblb/p /i//i//uuu httggguddess//// /eb/eeeeeeeeiissss wwiiiissssoossooooooo
for more details.
The authors should provide instructions on data access and preparation, including how to 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. 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 as much information as 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: [Yes]
Justification:
These details were provided Section 5.
Guidelines:
The answer NA means that the paper does include experiments.
The experimental setting should be presented 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
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [No]
Justification: The experiments were primarily designed to support our theoretical proof of existence and non-existence of transformers solving the next-token prediction task for Lt- Section the existence of single transformer attaining 100% is sufficient to confirm our theoretical existence result, and there are also many data-points that affirm the thcoretical
38

---

non-existence result thus, we don't believe that error bars would substantially useful information for the reader.
Guidelines:
The answer NA means that the paper does include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, 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, overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report I-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error 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 out range (e.g. negative error 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 in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification:
The metrics provided by the internal cluster used were reported in Section
Guidelines:
The answer NA means that the paper does include experiments.
The paper should indicate type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (c.g., preliminary or failed experiments that didn't 't make into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics https: http///wwwp..cpppollo////eccaaaa ines?
Answer: [Yes]
Justification: We have reviewed the NeurIPS 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 NeurlPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (c.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
39

---

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 or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there 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
Does the paper deseribe 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)?
Question:
Answer: [NA].
Justification: Our code is only for training transformers on strings of a's and b's and thus has no forsecable method of misuse.
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 (c.g., code, data, models), used in the paper, properly credited and the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [NA].
Justification: [NA].
Guidelines:
40

---

The answer NA means that the paper does not 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 is used and, if possible, include URL.
The name of the license (c.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 provided.
assets are released, the license, copyright information, and terms use in the package should be provided. For popular datasets, paper swi thcode. com/ datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. If this information is not available online, the authors are encouraged to reach out to the asset's '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]
Justification: The code implementing our experiments is attached supplemental material, and the method of training and data generation is described within Section 5.
Guidelines:
The answer NA means that the paper does release new assets. Researchers should communicate the details the dataset/code/moodll as part 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 used.
At submission time, remember anonymize your assets (if applicable). You can either create an 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: [NA]
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information 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 the main paper.
According to the NeurIPS Code of Ethics, workers involved data collection, curation, or 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
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?
Question:
Answer: [NA]
41

---

Justification: [NA]
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with
human subjects.
Depending 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.
recognize that the procedures for this may vary significantly between institutions and locations, and we 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.
16. Declaration of LLM usage
Question: Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, or originality the research, declaration is not required.
Answer: [Yes]
Justification: A footnote in Section 5 acknowledged the use of LLMs for assistance in implementing standard methods and writing parsers. The code was manually inspected and corrected afterwards.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, non-standard components.
for Please refer our LLM policy http:////eeriiss.ccc/eeeeeeeeeee what should or should not be described.
42


Reviews:
[{"review_id": "hJyTxg4PtV", "reviewer": "Reviewer_CRAK", "summary": "This paper aims to investigate the expressive power of a specific transformer, the future-masked fixed-precision transformer. The authors first establish an equivalence between this transformer and the programming language C-RASP, then prove a depth hierarchy for the language, demonstrating that deeper C-RASP models possess greater expressive power. Overall, the paper provides a clear understanding of how the expressive power of transformers varies with depth. The accompanying experiments are well aligned with the theoretical analysis.", "questions": "In addition to the concern raised in the Weaknesses section, I have a question regarding the experiments. In some cases, the accuracy for the depth-(k-1) model remains quite high, while for depth-(k-2) and lower, the accuracy drops significantly. For example, in Figure 5, the \"Accuracy on [201,250]\" shows this. Why does the depth-(k-1) model perform so differently compared to models with lower depth? Could you provide some explanation or intuition for this observation?", "limitations": "As noted in the Weaknesses and Questions sections, the omission of residual connections and positional encoding may impact the generality of the results. I am not very familiar with this research area, while the statement seems valid with sufficient experiemtns, I lean toward accepting this paper, if there are any misunderstandings in my comments, please let me know.", "rating": 4, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths\n\n1. This work establishes a connection between transformers of varying depth and a specially designed language with corresponding depth, making it possible to analyze and understand the expressive power of these models.\n\n2. The paper rigorously analyzes the expressive power of transformers with varying depths, accomply with solid theoretical proofs, provding insights for mechanisms interpretion and architecture design for practical transformers.\n\n3. The experimental results are consistent with the theoretical findings.\n\nWeaknesses\n\nThe analysis appears to overlook an important aspect of practical transformers: the residual connections between layers. Additionally, since positional encoding is not considered in this work, it may be challenging for the model to distinguish tokens at different positions, potentially limiting its expressive power.", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your review.\n\n> The analysis appears to overlook an important aspect of practical transformers: the residual connections between layers.\n\nSorry for the mistake. We did assume residual connections, and our translation from $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$ to transformers depends on them. \n\nDefinition A.8 does not specify that $f$ has to be a FFNN, so $f$ could include a residual connection.\n\nHowever, equation 8 indeed omitted residual connections for self-attention layers. In the final version, we will correct the equation to $\\\\mathbf{h}^{(\\\\ell)}\\_{i}(w) = f^{(\\\\ell)}\\left(\\\\mathbf{c}^{(\\\\ell)}\\_{i}(w) + \\\\mathbf{h}^{(\\\\ell-1)}_i(w)\\\\right)$.\n\n> Additionally, since positional encoding is not considered in this work, it may be challenging for the model to distinguish tokens at different positions, potentially limiting its expressive power.\n\nWe acknowledge that this is a limitation of the paper in its present form. Although transformers with no position encodings (NoPE) have been considered in practice (Kazemnejad et al., 2023), we do have something to say about position encodings and would be happy to add it to the paper. It would be easy to extend Theorem 3.1 (fixed-precision transformers are equivalent to $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$) to include periodic position encodings on the transformer side and modular predicates on the logic side. Then, by adding a neutral letter to $L\\_{k}$ (that is, by allowing some letter, say, $e$, to be inserted anywhere in a string without changing membership), we can show a strict depth hierarchy even in the presence of modular predicates, and therefore for transformers with periodic position encodings.\n\n> In some cases, the accuracy for the depth-(k-1) model remains quite high, while for depth-(k-2) and lower, the accuracy drops significantly. For example, in Figure 5, the \"Accuracy on [201,250]\" shows this. Why does the depth-(k-1) model perform so differently compared to models with lower depth? Could you provide some explanation or intuition for this observation?\n\nIf we understand correctly, you are asking why the numbers in the diagonal just below the the black line are considerably higher than the next diagonal below. In general, the presence of non-zero numbers below the line can be explained by the fact that the training and test data consist of strings of bounded length, whereas the theory only makes guarantees about strings of unbounded length. It stands to reason that these non-zero numbers would fade the further one goes below the line, and fade more sharply as the test length increases. But whether there is something special about the diagonal immediately below the line is not so clear to us, and we don't have any guesses about what would cause that if true. \n\nKazemnejad et al., 2023. The Impact of Positional Encoding on Length Generalization in Transformers. NeurIPS. arXiv:2305.19466."}, {"review_id": "jrIUyJnYRM", "reviewer": "Reviewer_zNc9", "summary": "Building on prior work in C-RASP and temporal logic (TL[#]), the authors show that (a subclass of) transformers are equivalent to C-RASP and TL[#]-left. This subclass includes models where computations use fixed-precision rounding everywhere except within the attention mechanism. Based on this equivalence, the paper establishes a \"depth hierarchy,\" demonstrating that there are specific tasks deeper transformers can solve which shallower ones cannot. Finally, the authors provide empirical evidence showing their theoretical predictions on model expressivity align well with practice. They test this on a next-token prediction variant of the $L_k$ language recognition task.", "questions": "1.  The work of Yang and Chiang (2024) seems to present similar results regarding the equivalence of C-RASP, TL[#]-left, and certain transformers. Could you elaborate on how your work differs from theirs? In particular, their work was not included in the comparison table in Section 1, and the equivalence of transformers and TL[#]-left, which appears to be their contribution, is presented as a contribution of the current work on line 29. Clarifying the distinction would be very helpful.\n\n2.  Based on the equivalence results you provide, could you elaborate on the depth required to learn tasks like parity and modular addition?\n\n3. Regarding the experiments, accuracy is shown to sharply decline for $k \\geq 10$, even for models with sufficient depth. You attribute this to challenges with learnability, not expressibility. Could you provide more insight into the specific learning challenges for these more difficult cases and speculate on what might be required to solve them?", "limitations": "yes", "rating": 5, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 3, "significance": 3, "originality": 2, "strengths_and_weaknesses": "**Strength:**\nThe paper is well-written, and the presentation is solid. The theoretical demonstration of a clear depth hierarchy under non-prohibitive constraints is a very interesting contribution to the broader community. I also appreciate that the authors provided empirical results to support their theoretical findings. This strongly demonstrates the practical applicability of their results and shows that the underlying theoretical assumptions were practical.\n\n**Areas for Improvement:**\nThe paper's primary weakness is its accessibility. While the results are interesting for a general audience, the work may be difficult to follow for those not already familiar with temporal logic or C-RASP. I understand that these concepts are built on previous work, but including more intuitive or illustrative examples of them would be very helpful. Adding a brief introductory section on these topics in an appendix could significantly improve the paper's clarity and open it up to a larger audience.", "was_revised": true, "final_justification": "I recommend accepting the paper. It is well-written and clearly presented, with a strong theoretical contribution demonstrating a clear depth hierarchy under non-prohibitive constraints. The inclusion of empirical results to support the theoretical findings further strengthens the work by highlighting its practical applicability. While the paper could be improved by adding a brief introduction to temporal logic and C-RASP to enhance accessibility, these are minor issues that do not detract from the overall quality and significance of the contribution.", "rebuttal": "Thank you very much for your review.\n\n> [I]ncluding more intuitive or illustrative examples of [temporal logic and C-RASP] would be very helpful. Adding a brief introductory section on these topics in an appendix could significantly improve the paper's clarity and open it up to a larger audience.\n\nWe agree that examples would be helpful, and will add examples in the final version, either in the extra page or in the appendix.\n\n> 1. The work of Yang and Chiang (2024) seems to present similar results regarding the equivalence of C-RASP, TL[#]-left, and certain transformers. Could you elaborate on how your work differs from theirs? In particular, their work was not included in the comparison table in Section 1, and the equivalence of transformers and TL[#]-left, which appears to be their contribution, is presented as a contribution of the current work on line 29. Clarifying the distinction would be very helpful.\n\nYang and Chiang (2024) did not prove an exact equivalence; they proved that $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$ can be converted to an arbitrary-precision transformer, and a transformer with $O(1)$ precision (even inside attention) can be converted to $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$. Here, we have tightened these bounds by proving that transformers with $O(1)$ precision (except inside attention) are exactly equivalent to $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$. We will clarify these differences in the final version.\n\n(The comparison table at the end of Section 1 is for depth separation results, and Yang and Chiang (2024) did not prove any depth separations, so their paper is not included in the table.)\n \n> 2. Based on the equivalence results you provide, could you elaborate on the depth required to learn tasks like parity and modular addition?\n\nOur equivalence between transformers and C-RASP proves that tasks like parity and modular addition cannot be expressed by transformers of any depth (without positional encodings). Huang et al. (2025) show that C-RASP programs cannot perform modular counting, which is a prerequisite for both parity and modular addition.\n\n> 3. Regarding the experiments, accuracy is shown to sharply decline for, even for models with sufficient depth. You attribute this to challenges with learnability, not expressibility. Could you provide more insight into the specific learning challenges for these more difficult cases and speculate on what might be required to solve them?\n\nOne possible cause is insufficient diversity in the training data. Because we restricted the training data to strings of length [101,150], languages $L_k$ for large $k$ tend to have very short contiguous blocks of $a$'s and $b$'s, in order to fit $k$ alternations within the string. Thus, the particular distribution of blocks may become an extraneous signal for $L_k$ that hampers learning as $k$ gets larger.\n\nOther possible causes could be: insufficient training time, insufficient width ($d$), or the so-called \"curse of depth\" (Sun et al., 2025).\n\nHuang et al., 2025. A Formal Framework for Understanding Length Generalization in Transformers. ICLR. arXiv:2410.02140.\n\nSun et al., 2025. The Curse of Depth in Large Language Models. arXiv:2502.05795.\n\nYang and Chiang, 2024. Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers. CoLM. arXiv:2404.04393."}, {"review_id": "4Iy91FPDZg", "reviewer": "Reviewer_AK8r", "summary": "This paper uses a simplified form of a transformer to study the relation between depth of the transformer (number of stacked transformer blocks) and depth in a formal language modeled by TL (temporal Logic) which is equivalent to C-RASP. The paper establishes a tight connection between depth of a transformer model and a programming language: C-RASP. Using the established connection, authors claim to characterize a family of transformers that can length-generalize.", "questions": "1. In empirical results, authors claim that the drop after 10 layers does not contradict their findings. I thought their findings were tight so I am surprised why this happens. Can you elaborate?\n\n2. Can you elaborate on how findings on TL generalize to other classes of logic?\n\n3. It is unclear to me if the choice of no positional embedding is to ease theoretical demonstrations or if it is something that also helps improve results. Having no positional embeddings can clearly be problematic in many cases. It would help to have a more clear explanation on this.", "limitations": "The paper's language highly relies on notations and definitions defined in a narrow set of papers. It may be hard to follow for a general audience. Empirical results are limited and there is a gap there which is uncovered (see Question 1 above)", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 2, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths: The paper presents a solid theoretical work, and proves a non-trivial result.\n\nWeaknesses: \n\nThe paper accumulates a large number of definitions and also heavily relies on objects defined in a few previous background papers (e.g. Chiang et al 2024) which are necessary for readers to follow the paper's arguments. It is therefore a hard to follow paper. Authors could make an effort in summarizing the background content required for the reader to read through the paper and only present the necessary. \n\nIt is also not clear which of the assumptions are made to make proof of theoretical results easier and which are made to improve the model / results. \n\nEmpirical experiments have some shortcomings. Authors seem to have run some more experiments during the rebuttal. I am uncomfortable with those results since they seem to have let the model train for longer / have slightly different hyperparameters.", "was_revised": true, "final_justification": "It's a good paper with string results, but presentation is rough and there are some strong assumption / surprises in the paper.", "rebuttal": "Thank you very much for your review.\n\n> The paper accumulates a large number of definitions and also heavily relies on objects defined in a few previous background papers (e.g. Chiang et al 2024) which are necessary for readers to follow the paper's arguments.\n\nWe agree that the paper is heavy on formalism, and think that Reviewer CRAK's suggestion to add examples of C-RASP and/or $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$ would be helpful. We will do so in the final version, either in the extra page or in the appendix.\n\nWe also agree that there are quite a few definitions used in the proof of Section 4 (accommodating, Parikh numerical predicates, etc.). These definitions represent our effort to clarify ideas developed in previous papers (esp. Behle et al., 2009). We will put some further effort into making the argument clearer, especially the sketch in Section 4.1.\n\n> 1. In empirical results, authors claim that the drop after 10 layers does not contradict their findings. I thought their findings were tight so I am surprised why this happens. Can you elaborate?\n\nOne possible cause is insufficient diversity in the training data. Because we restricted the training data to strings of length [101,150], languages $L_k$ for large $k$ tend to have very short contiguous blocks of $a$'s and $b$'s, in order to fit $k$ alternations within the string. Thus, the particular distribution of blocks may become an extraneous signal for $L_k$ that hampers learning as $k$ gets larger.\n\nOther possible causes could be: insufficient training time, insufficient width ($d$), or the so-called \"curse of depth\" (Sun et al., 2025).\n\n> 2. Can you elaborate on how findings on TL generalize to other classes of logic?\n\nIn Appendix E we derive a depth hierarchy for $\\\\widehat{\\\\mathsf{MAJ}}_2[<]$, a logic studied by Behle et al. (2009). Our results can also be extended straightforwardly to show a depth hierarchy for the extension of $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$ with successor and modular predicates. An interesting future question is whether this can be shown for the logic with arbitrary numerical predicates, which would correspond to $\\\\mathsf{TC}^0$ circuits with linear gates.\n\nBehle et al., 2009. Regular Languages Definable by Majority Quantifiers with Two Variables. International Conference on Developments in Language Theory.\n\nSun et al., 2025. The Curse of Depth in Large Language Models. arXiv:2502.05795."}, {"review_id": "Dxzw2CHVlc", "reviewer": "Reviewer_CcuD", "summary": "This paper investigates the role of depth in transformer architectures by drawing a connection to a logical framework known as temporal logic with counting (TL[↼#]). The authors focus on fixed-precision transformers: all computations are performed with limited numerical precision, except within the attention mechanism. The core theoretical contribution is to show that these fixed-precision transformers are equivalent in expressivity to the programming language C-RASP, which is equivalent to the logic TL[↼#]. The equivalence is depth-preserving: the number of layers in the transformer corresponds to the nesting depth of the counting operators in the logic. Using this correspondence, the authors establish a depth hierarchy: deeper TL[↼#] formulas can define more complex sequence patterns than shallower ones. This implies that deeper transformers are more expressive than shallower ones. To support the theory, the paper presents empirical results showing that transformers require greater depth to solve formal language tasks as the complexity of the sequence dependencies increases. These results align with the theoretical depth requirements predicted by TL[↼#].", "questions": "1. Are there insights into whether width can compensate for depth (especially on these synthetic tasks), even if not in a fully expressive way?\n2. The authors note performance degradation at higher k values (e.g., $k \\geq 10$). Is this due to optimization difficulties, data sparsity, or theoretical limitations?", "limitations": "* The theoretical framework assumes fixed-precision computation and omits positional encodings. This diverges from common transformer use cases, which limits immediate applicability to current architectures.\n* The experimental validation is limited to synthetic tasks. While effective for proving the point, these tasks do not capture the complexity or variability of natural language.\n* While the authors prove depth separation for expressivity, they do not provide results regarding learnability or training stability at increasing depths.", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "**Strengths:**\n\n* The authors provide a mathematically grounded depth hierarchy theorem, building on logics with counting and extending previous results in a novel and robust way.\n* The equivalence between fixed-precision transformers and TL\\[↼#] is not only elegant but also preserves depth, which is central to the paper’s claims.\n* A careful experimental setup shows that the theory’s predictions about depth requirements hold up in practice, at least on synthetic language tasks.\n\n**Weaknesses:**\n\n* The results apply specifically to fixed-precision transformers without positional encodings. While this is reasonable in a theoretical sense, it limits immediate applicability to real-world transformer architectures.\n* The empirical validation is limited to formal language tasks. It remains unclear how these results translate to real-world NLP tasks.\n* The no-position-encoding assumption diverges from most practical models, which might limit the audience’s perception of the impact.", "was_revised": true, "final_justification": "I am satisfied with the authors' response during rebuttal.", "rebuttal": "Thank you very much for your review.\n\n> The results apply specifically to fixed-precision transformers without positional encodings. While this is reasonable in a theoretical sense, it limits immediate applicability to real-world transformer architectures....The no-position-encoding assumption diverges from most practical models, which might limit the audience’s perception of the impact.\n\nWe acknowledge that this is a limitation of the paper in its present form. Although transformers with no position encodings (NoPE) have been considered in practice (Kazemnejad et al., 2023), we do have something to say about position encodings and would be happy to add it to the paper. It would be easy to extend Theorem 3.1 (fixed-precision transformers are equivalent to $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$) to include periodic position encodings on the transformer side and modular predicates on the logic side. Then, by adding a neutral letter to $L_{k}$ (that is, by allowing some letter, say, $e$, to be inserted anywhere in a string without changing membership), we can show a strict depth hierarchy even in the presence of modular predicates, and therefore for transformers with periodic position encodings.\n\n> The empirical validation is limited to formal language tasks. It remains unclear how these results translate to real-world NLP tasks.\n\nIt is true that our results are limited to formal language tasks, but the family of formal languages we use, $L_k$, may well be related to real-world tasks. Since it requires searching left to find an $a$, then searching left to find a $b$, and so on up to $k$ times, it can be seen as a prerequisite to any task that involves a chain of $k$ long-distance dependencies.\n\nFor example, the $k$-hop induction heads task involves iterating the following procedure $k$ times: at position $i$, find a previous position $i'<i$ with the same symbol as $i$, then find a previous position $i''<i'$ with the same symbol as $i'+1$, and so on, which is essentially the same procedure needed to solve $L_k$. Although more work would be needed to make this more precise, we predict on the basis of our theory that $k$ hops require $k$ layers. (Sanford et al (2024) predict $\\log k$ layers; the difference is that they assume a fixed string length, whereas we assume unbounded length.)\n\nAnother basic application to NLP would be recognizing \"stretched\" $k$-grams. Our results imply that for any sequence of symbols $a_1, a_2, \\ldots, a_k$, the language $\\Sigma^* a_1^+ a_2^+ \\cdots a_k^+ \\Sigma^*$ requires depth $k$. This is immediately applicable to a modality where each symbol is \"stretched\" out, like recognizing words in speech. It would be an interesting question for future research to investigate the case without \"stretching\".\n\n> Are there insights into whether width can compensate for depth (especially on these synthetic tasks), even if not in a fully expressive way?\n\nOur results show that width cannot compensate for depth if we would like the transformer to operate uniformly over every input length. However, if we are satisfied with a fixed context window then it is possible. In fact, every finite language can be defined by a depth-2 $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$ formula, which will imply the same for transformers. However, this requires a width exponential in the context window size. It would be an interesting question to study depth-width tradeoffs for $\\\\mathsf{TL}[\\\\overset{\\\\leftharpoonup}{\\\\#}]$ formulas in the fixed length regime.\n\n> The authors note performance degradation at higher k values (e.g., $k\\ge10$). Is this due to optimization difficulties, data sparsity, or theoretical limitations?\n\nOne possible cause is insufficient diversity in the training data. Because we restricted the training data to strings of length [101,150], languages $L_k$ for large $k$ tend to have very short contiguous blocks of $a$'s and $b$'s, in order to fit $k$ alternations within the string. Thus, the particular distribution of blocks may become an extraneous signal for $L_k$ that hampers learning as $k$ gets larger.\n\nOther possible causes could be: insufficient training time, insufficient width ($d$), or the so-called \"curse of depth\" (Sun et al., 2025).\n\n> While the authors prove depth separation for expressivity, they do not provide results regarding learnability or training stability at increasing depths.\n\nOur results sharply mark the boundary between expressible and inexpressible functions at varying depths, allowing future investigation to isolate issues of learnability and training stability. Two questions in this vein arise due to our results. First, why is there degradation in learnability past $k=10$, despite the languages being expressible? Second, why is there non-zero performance for $k$ which are inexpressible? \n\nKazemnejad et al., 2023. The Impact of Positional Encoding on Length Generalization in Transformers. NeurIPS. arXiv:2305.19466.\n\nSanford et al., 2024. Transformers, parallel computation, and\nlogarithmic depth. ICML. arXiv:2402.09268.\n\nSun et al., 2025. The Curse of Depth in Large Language Models. arXiv:2502.05795."}]

Author rebuttal:

Meta-review: (a) Summary

The paper proves a depth-preserving equivalence between fixed-precision transformers (with residuals, no positional encodings) and C-RASP, then establishes a strict depth hierarchy - deeper models are strictly more expressive. Experiments on formal language tasks support the theory, and additional runs during rebuttal confirm that models below the predicted depth fail to length-generalize.

(b) Strengths

- Strong theoretical contribution with a clear depth hierarchy result.
- Tightens prior work by proving exact equivalence.
- Empirical evidence aligns with theory, rebuttal adds convincing results.
- Provides a framework for reasoning about depth and generalization.

(c) Weaknesses

- Assumes no positional encodings.
- Maybe hard to follow for non-specialists.
- Experiments are synthetic, real-world implications are discussed but not shown.

(d) Reason

Even with some weaknesses, the theoretical advance is significant and well-supported.

(e) Discussion & Rebuttal

Reviewers raised concerns about residuals, positional encodings, and empirical anomalies. Authors clarified residuals were assumed, outlined how to handle PEs, and ran stronger experiments confirming the depth threshold. Concerns about accessibility remain, but technical soundness and novelty are clear.
Decision: Accept (poster)