Characterizing the Expressivity of Fixed-Precision Transformer Language Models
Authors: Jiaoda Li
Ryan Cotterell
Venue: NeurIPS 2025 spotlight ()
Keywords: transformers
expressivity
formal language
logic
automata
Primary area: deep_learning

Abstract: Transformer-based language models (LMs) have achieved widespread empirical success, but their theoretical expressive power remains only partially understood. In this work, we analyze a restricted idealization of fixed-precision transformers with strict future masking, soft attention, and no positional encodings. We establish that this class of models is exactly as expressive as a specific fragment of linear temporal logic that contains only a single temporal operator: the $\texttt{past}$ operator. We further connect this fragment to established classes in formal language theory, automata theory, and algebra, yielding a unified framework for understanding transformer expressivity under this idealization. Finally, we present empirical results that align closely with our theory: transformers trained on languages within their characterized expressive capacity generalize reliably across sequence lengths, while they consistently fail to generalize on languages beyond it.

Characterizing the Expressivity of Fixed-Precision Transformer Language Models
Jiaoda Li Ryan Cotterell
jiaoda. 1i
Eyan. cotterell @inf. ethe.cc. ch
EIH zurich
Abstract
Transformer- language models (LMs) have achieved widespread empirical success, but their theoretical expressive power remains only partially understood. In this work, we analyze restricted idealization of fixed-precision transformers with strict future masking, soft attention, and no positional encodings. We establish that this class of models is exactly expressive temporal logic that contains only a single temporal operator: the past operator. We further connect this fragment to established classes in formal language theory, automata theory, and algebra, yielding a unified framework for understanding transformer expressivity under this idealization. Finally, we present empirical results that align closely with our theory: transformers trained on languages within their characterized expressive capacity generalize reliably across sequence lengths, while they consistently fail to generalize on languages beyond it
specific fragment of linear
Introduction
Transformer-basee language models (LMs) have demonstrated remarkable empirical success 46 36
12] on wide variety of natural language tasks 47
19 41 inter alia). This success has sparked grow- ing interest in understanding the theoretical expressive power of transformers, i.e., what languages they can and cannot recognize, and, by extension, what tasks they and cannot perform. A signif- icant body of work approaches this question by relating transformers to well-established frameworks such as formal languages, logic, and circuit complexity analysis, theoreticians often propose idealizations of transformers, For instance, while practical imple- mentations of transformers operate under fixed precision, e.g., single (32-bit) half (16-bit) precision, many authors assume arbitrary
[18 31 50 42 To facilitate their theoretical
[38] 18 34) or length-dependen precision [32 77. Although such ide- alizations capture key aspects of transformers, they tend to overestimate their expressive power [38
recent step toward a more faithful theoretical understanding of the expressive power transformers comes from Yang al. [50), who show that Exxe-prrccsson transformers with strict future masking and unique hard attention (UHA) are exactly as expressive as linear temporal logic LTL (T, F,S, U which includes four temporal operators: P (past), F (future), S (s (since), and U (until). However, UHA still deviates from the soft attention used in practice. To address this gap. Yang and Chiang [49] analyze fixed-preet -xeedipre transformers with striet future masking and soft attention, an idealization that most closely reflects the models deployed in real-world applications. Yang and Chiang 49 show that such models are upper bounded by C-RASP, counting-basee programming language, though a precise characterization of these models' expressivity remains open.
In this paper, close this gap by providing exact characterization of the expressive power of fixed-precision transformers with soft attention, strict masking, and no positional encodings (NoPE). We show they precisely characterized by [PL( restricted fragment of LTL(P, F,S, Uj that
Code available GitHub repository
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

R-trivial
monoid
Lemma C.4
Theorem 3.3
transformer
Theorem 3.2
left-leterministic
polynomial
[4]
Lemma C.I
LTL
Theorem 2.1
PODEA
Theorem 5.2
Theorem 5.1
|F
transformer language model
Figure 1: Roadmap of the paper. Red arrows indicate novel results.
only the past operator (P). We further demonstrate that LTL(P] is equivalent in expressivity to partially ordered deterministic finite automata (PODFAs), which are characterized by R-trivial monoids and recognize left-determiisstic polynomials. These results offer detailed and principled characterization of the expressive power of this idealization, delineating its strengths and limitations. Crucially, findings imply that many simple languages, e.g., bounded Dyck languages, which have been shown to be recognizable under more permissive idealizations, are beyond the reach of the models study. We also extend our theoretical results transformer LMs, showing that their expressivity matches that of transformer recognizers. A visual overview of the theoretical landscape provided in Fig. I
To arrive at a compelling theory, it is essential to show that it faithfully reflects the behavior of models trained under standard machine learning paradigms. To this end, we provide empirical evidence using the length generalization framework, a widely used method for gauging neural network expressivity We construct suite of languages spanning fine-grained hierarchy of formal language classes. Our results (Tab. [T) exhibit strong alignment between theory and practice: for all languages that transformers are predicted recognize, the models generalize perfectly over lengths (100% accuracy); for languages beyond their theoretical capacity, they consistently make generalization errors, regardless of learning rates random seeds.
10 22
2 Background
In this section, we present the necessary background knowledge that underpins our analysis.
2.1 Strings and Languages
An alphabet, denoted as E, a finite, non-empty set symbols. A string over Σ is a finite sequence of symbols drawn from Σ. The set of all strings over Σ is denoted by its Kleene star Σ" A subset of E is called a language. A regular expression a declarative way to describe a language, defined recursively as follows:
( and each E Σ are regular expressions;
If a and regular expressions, the union + concatenation a:3, the Kleene star a*, and complement a.
language regular if and only if it can be described by a regular expression 26]. A regular language is said to be star-free if it can be described by regular expression without the Kleene star 28 As an example, Σr, the set of strings over Σ, star-free, as it can described by (
2.2 []
Linear temporal logic LTL F.S.U 25 full definition is given in A.1 LTT. that includes only one temporal operator (past). Formulas LTL are composed of atomic formulas т. for every Σ, Boolean connectives A, and temporal operator P. The
is modal logic, with modalities referring to time. The In this paper, we define fragment of [TL[P, F. F.S, U. dendooeed as

---

disjunction V is definable in terms of A and as:
t ( -222).
(I)
When defined over strings, the formulas are interpreted with respect string w M...... ww at position E {1.....N N). The semantics are defined inductively. Given string position and formula vi we define w, n F v (w satisfies & at position n2) as follows:
W, n Na
if and only if if and only if
the symbol of w an a.
W, n V1 A 2/2
w. n + t1 and W, F 4/2.
W, n -a
if and only if
w. n j tb.
W, n Pt
if and only if
there exists such that m < n and w, m vb
Example:
abb, F=
the first symbol is a.
a 3 Pra an occurs before position
To say a string w of length N satisfies a formula vb, written as w }= vb we evaluate from position N + 1 (the position after the final symbol):
ト
2 if and only if w, N + F tb.
(2)
The language defined by a formula vp is the set L(v) of all strings that satisfy vb.
Example:
Pa defines all the strings that contain at least one occurrence of i.e.,
L(Pa) = Σ'."*
(3)
2.3
PFO*[<]
First-order logic FO|<] can also be used to describe formal languages. In contrast to (linear) temporal logic, where formulas are interpreted at a single position, FO[<] formulas may contain multiple position variables, making it better-suited to simulating mechanisms in transformers that involve more than one position, such as attention; see $$ B.2 and 3.2 In this paper, we introduce fragment of FO called [ the past fragment of first-order logic with two variables. The atomic formulas of PFO [<] consist of unary predicates n, for each a e Σ and binary numerical predicate < that can be used determine the sequential order between variables. Formulas in PFO*[<] can have at most two distinct variables, x and In addition to the usual Boolean connectives A and there a bounded existential quantifier By < æ, where y the variable bounded by the quantifier, and is the free variable. In case there is no free variable, the bounded existential quantifier behaves like an ordinary existential quantifier. The formulas in PFO?[<] are constructed inductively as follows:
Every atomic formula is a formula;
A Boolean combination of formulas a formula it does not contain more than two variables;
If pxx, y) is formula with two variables x, y. By < x p(r,, y) and Ex Φ( y) are formulas;
If (xx) is formula with one variable x, 3x y ((x) is a formula;
((x) a formula with one variable x, 3x ((x) a formula.
The bounded universal quantifier Vy
be defined using By < and For instance:
Vy < x (( -y < x _0 ().). y).
(4)
formula with no free variables is called sentence. We write w J & is satisfied for w. A sentence defines language, the set of strings over Σ satisfying it, denoted as L(Ø).

---

Example:
The sentence below defines all the strings that contain abc subsequence (symbols appearing in order, possibly non-coniguuously:
Ex : (T)) A By < x (Tx 3x y na (z))).
(5)
Note that the variable x is reused, as permitted PFO [<] The formulas below, however, are not definable PFO [<]:
y (more than two variables):
Vx (Sy
I T. (v)) (disallowed use of the quantifier By 2 x).
PFO" <| is specifically designed to match the expressive power of LTL(P), allowing us to leverage
both formalisms in analysis of transformer expressivity.
Theorem 2.1. [=) and [TL have the same expressive power.
Proof. See A.2.3
Transformers
In this section, formally define the transformer idealization under consideration and establish two central expressivity results: (i) every transformer can be translated into equivalent PFO*[<] for- mula, and (ii) every LTL(P] formula can be simulated by a transformer. Combined with Theorem 2.1 these results imply that transformers are expressively equivalent to both [TL[P] and [F)]
3.1 The Transformer Architecture
The transformer considered in this section follows the architecture described by Yang et al. [50], with the exception that we use soft attention in place of unique hard attention (UHA). Before formally defining the architecture, first state explicitly the assumptions that will govern our model as follows.
Assumption 3.1. We assume that the transformer satisfies the following conditions:
1. Fixed precision: There exists a finite values that the flouting-point numbers can assume. We denote this set as F = (f1.f2.....
2. No positional encoding (NoPE): Positional encodings omitted for now, but are addressed in
F.
3. Soft attention: Attention weights are computed using the softmax function. We also treat average hard attention (AHA) in SF..] showing that AHA equally expressive as soft attention.
4. Strict future masking: As in Yang et al. (50), the attention is strictly future-mskker Strict masking shown be more expressive than non-strict masking $122
Recognition: Following standard practice in expressivity studies [42], the transformer treated
language recognizer. We will extend the analysis to transformer language models in $
Transformers take strings as input. Given a string w = -wi ... wy over an alphabet Σ, we append a special end-of-sentence symbol BOS E to form a completed string wi ... wNEOS over the extended alphabet Σ def yo [EOS}. An initial embedding layer E: N+1 + (D+(N++) maps each input symbol including BOS to D-dimensional representation. We define the embedding layer as the th layer of the transformer:
def
(6)
The embedding is followed by a stack of hidden layers. Each hidden layer contains two sublayers: self-attention mechanism (0); (Dx(++1) + FD*(N+1,, and feedforward net- work F(O) DDx(N+1) + DD((++)) These components composed sequentially. For each

---

E (0.1...... 1}. we define:
(6+05))
LN
A (4)
( + H
(7a)
H
H(+ def
FF()) (H(C+0.5) LN
+ H ((t0.5))
(7b)
where LN denotes layer normalization [ Finally, a classification head C: IFD + - maps the representation at the EOS position in the final layer to scalar output:
o ww) C H N1).
(8)
We use H (1)
(w),n W d.n. to denote the (d.n)" 1)th entry in the matrix. Similarly, H (w)., refers to the column vector at position n, and [[))(w); refers to the row vector corresponding to dimension d. Consequently, a transformer defines a function of type EN+1 >> F, where N is parameter of the type. We say string is accepted by the transformer if of o(w) > A detailed specification of the architecture is provided in $B.I
3.2 From Transformers to PFO
In this subsection, we discuss the following theorem.
Theorem 3.2. Every transformer can be simulated by PFO2 [<].
Proof. See
B.2
Our proof closely follows the approach of Chiang al. 19 Section 5], with key difference: the simulation of summation in soft attention. While prior work makes use of counting quantifiers to simulate summation, Li al. (27] demonstrate that summation with iterative rounding can be simulated with FO[ <|] We take this a step further by showing that the specific summation involved in soft attention can be simulated by PFO [<]. Here, we provide a high-level overview the proof. We identify two summations in soft attention. The first occurs in the denominator of the softmax
function, defined for D-dimensional vector x, as follows:
softmax(x), def exp(xa) for d (1....,
El exp(x;))
exp is deterministic function. Under the fixed precision assumption, the possible input and output values of exp form a finite set, allowing PFO [<] formulas to encode exp by explicit enumeration of these values. Since exp outputs only non-negative values, the summation in the denominator reduces sum of non-negative terms, which can be simulated by PFO [<] (Lemma B.S). Additionally, the second summation is weighted sum, in which the weights are produced by the softmax function.
Under fixed precision, the output of softmax contains bounded number of non-zero entries (Proposition [.6). Therefore, the weighted sum involves only bounded number of terms and can similarly be simulated by PFO*[<]
(Lemma B.7
3.3 From [P] to Transformers
In this subsection, discuss the following theorem.
Theorem 3.3. Every [ can be simulated by transformer.
Proof. See
B.3
Our proof is adapted from that of Yang al. [50] Appendix C.I]. Intuitively, each LTL formula encoded in dedicated coordinate d E {1..... D) of the transformer's 's hidden state. At each position, this coordinate takes the value if the formula satisfied at that position, and otherwise. The key challenge in proving Theorem 3.3 lies in simulating the temporal operator P. Prior constructions typically employ uniform attention, which assigns equal weight all preceding positions, to simulate such operators. However, under fixed precision, soft attention has limited attention span, as the
5

---

output of the softmax function contains only bounded number of non-zero entries. We refer to this bound as the maximum attention span, denoted by Naxx. To overcome this limitation, previous work has relied on non-fixed numerical precision- as arbitrary precision
g 49 or log precision
31 to prevent attention weights from vanishing. contrast, we present a construction that overcomes this issue without requiring increased numerical precision.
We begin by describing base construction that applies when attention weights do not vanish, and then extend it to handle cases where vanishing weights may occur.
Base Construction. Suppose formula dh simulated by coordinate dj at the 4dh layer, i... by H (4) (omitting the input string w for brevity), and let Pib be the formula we aim to simulate. We construct an attention sublayer that uniformly attends to all previous positions m < n such that H(() m
dy
such positions exist, we set an unused coordinate dp to i.e., H (((+0.0) 1 and otherwise to O. dp.n
Handling Vanishing Weights. However, when too many (more than Maxx) previous positions satisfy v), the resulting attention weights will underflow to O. This results in H (1(6-0.5) even when
dy.n
Peb is true, leading to incorrect behavior. To address this, we first compute the logical conjunction of d1 and dp and store it in dx, i.e.,
if H dn.n 1 and H (2 1, otherwise.
(++1) daan
dp.n
(10)
The number of positions n with H (6+1)
dy,n = 1 is bounded by Nmax since beyond the (Nmax + 1)th po- sition, the first attention sublayer will suffer from vanishing attention weights, causing H (f+0.5) 0. dp.m
Next, we construct a second layer in which the attention sublayer uniformly attends to all positions m < n. where H((+)) 1. This produces a coordinate dpp that simulates P( A Pv)). Since the number of positions satisfying H dm 1 is bounded, this second attention sublayer is not subject to vanishing attention weights and therefore computes its output reliably.
The formula P( A Pe) effectively asks whether there are least two positions before n that satisfy vb. Thus, if there is exactly one position m < n satisfying th, then P(u A Pt) differs from the target formula Pvb. In this case, however, the first attention sublayer (producing dy) correctly simulates Pub, since the attention only needs to cover one position. We therefore take the logical disjunction of dp and dpp, implemented via the subsequent feedforward sublayer. The resulting coordinate dy correctly simulates the formula Pvb. This completes the proof sketch.
Example:
Assume the attention span is limited to I position. The following example illustrates the simulation process, with defective simulations highlighted in red.
formula
coordinate
position
&
dj
Pt
dp
0
1
1
0
0
V P
d,
0
1
0
P A P.))
dpp
0
0
0
1
Pvb P(W P
dy
4 Characterizations of [P]
We have established the expressive equivalence between transformers and LTL[P]. This connection becomes especially compelling when paired with precise and rich characterizations of [PL To that end, we prove the following theorem.
Theorem 4.1. Let L C Σ* be a regular language, M. be its syntactic monoid, and A be the DFA accepting it. The following assertions are equivalent: (1) T. is a lefi-deteriiiistic polynomial, (2) M is R-trivial, (3) A is partially ordered, and (4) L is definable by [PL.P]

---

Proof. See CC
In the remainder of this section, we focus on the PODFA characterization, which will be central to later developments. The other characterizations are defined in $ which also includes discussion of superclasses of LTL summarized Tab.
Definition 4.2. A deterministic finite automaton (DFA) 5-tuple A (2, Q, qr, F,8) where
Σ is an alphabet;
Q is finite set of states;
q1 E Q the initial state;
C Q is the set of final states;
5: Q E + Q is a total transition function;
qR Q
rejecting sink state, i.e., ö(gR, a) QR for every a E Σ.
Given an automaton A = (E, Q. F,8), we say A is in state upon reading string w W1 WN e 1' and only if there exists a sequence states qo..... . qN such that
= yr:
1++1 8(4, Mat1) for E [N- 1];
4N = g.
A string is accepted by if reaches one of the final states upon reading Definition 4.3. A DFA is said to be partially ordered if there exists partial order - on Q such that for every state q E Q and symbol a E L, have q 3 8(g, a).
Informally, in a partially ordered DFA, once the automaton leaves state, it never revisits it, An example non-partin non-partially ordered DEA is provided in
Transformer Language Models
In this section, extend our analysis to transformer LMs. Formally, an LM constitutes distribution over " typically factorized autoregressively as follows:
N
p(w) def
(EOS w) II
p (wo wzn)-
(11)
==1
where Wen
del W1 ... Wn-1- We define an LM p's prefix probability Ppeetx as:
Pprctix (w) def Σ p(ww)).
(12)
WEX
To adapt transformer for language modeling, we feed the input string w into the model autore- gressively, and the classification head is replaced with language modeling head L: FD g/>! which maps the representation in the last layer T. at the most recent position n 1 to probability distribution over Σ. This defines the local distribution p as follows:
D (wn wen) def
( (Wen).n-1) M..
(13)
where (4) in denotes the probability assigned to the symbol Wa. Under fixed pre- cision, this distribution may not be perfectly normalized, as the sum of its components can deviate from due rounding errors.
As transformer LMs do not introduce any new computational components beyond those already present in transformer recognizers, the same constructions and proofs apply. Therefore, every transformer LM can be simulated by [F)
7

---

Theorem 5.1. Every transformer LM can be simulated by PFO*|<]
Proof. See $D
The converse direction is more subtle. Yang and Chiang
show how to compile transformer LM from C-RASP. Here, we present an alternative approach that is more intuitive. Our construction leverages the PODFA characterization of [T]( Given PODFA A (Σ, Q, 2r, F,5), we can define a corresponding LM P.A by specifying the local distribution p A as follows: Suppose A is in state q upon reading the prefix Weni
49
If $ F and q & QR. da(a wenn) assigns uniform probability over all symbols in {a ò(g, a) Q {qnl);
If E F. aa | Wen) assigns uniform probability over all symbols in {a 8(q. a) Q [9n)) } {BOS};
q - qn. 7. A wen) for all E E, i.e, Pprefix (wen) = O.
Note that in practice, soft cannot produce all-zero vector. For technical convenience, therefore extend the Σ with special symbol UNK & E, which receives all the probability mass when
A reaches the rejecting state, i.c., 7 AUNK wecn) = 1 if q = qR. Accordingly, we extend the LM head L to accommodate this special symbol: L: RD + [RSUUUNK]]
Theorem 5.2. Every PODFA LM can be simulated by transformer LM.
Proof. See D
Intuitively, for each state q E Q, we can construct a [P] formula ,h, such that Wen, + 1 and only if the automaton in state q after reading the prefix Wen- By Theorem 333] each formula by can be encoded into a designated coordinate dg of the transformer's hidden state. The language modeling head, extended include the special token UNK, then maps these coordinates to the corresponding probability distribution specified by TAA
Experiments
The experiments are divided into two parts: language recognition and language modeling.
6.1 Language recognition
We have shown that transformer can recognize only left-deterministic polynomials. In this section, we conduct a series of language classification experiments to empirically validate this claim. We consider five language classes, arranged in a strict inclusion hierarchy-eate each class is proper subset of the one preceding languages are listed in Tab. 1 and their detailed definitions are provided in 1.1.2
For each class, select one or more representative languages. These
6.1.1 Experimental setup
We implement the transformer that we theorize about (Assumption 3.1 For comparison, we also train a long short-term memory (LSTM) (20). Models are trained on strings up to length 40, and tested on strings of length 41 500. Each experiment is run with different random seeds and learning rates. We consider transformer to have successfully recognized language if it achieves 100% accuracy at least one of the runs. Details of the experimental setup and model configurations are provided in I.I
6.1.2 Results
We compute classification accuracy and report both the maximum and mean values across all runs in Tab. [ The LSTM achieves perfect accuracy on all tasks, consistent with previous work showing that LTSMss can recognize regular languages [29] and implement counting mechanisms [48]. This confirms that the tasks are learnable given the available training data. Results transformers align

---

0
1
2
(a) RDP-1
(b) LDP-1
(c) LDP-2
Figure 2: Visualization of the transformer's 's representations for different DFA states. -1 denotes the
rejecting state qn- The filled contours represent the decision boundaries of a linear classifier.
precisely with theoretical predictions: under fixed precision, transformers with soft attention and NoPE can recognize exactly the class of left-deterministic polynomials. They achieve perfect accuracy all [dT/(p)deefnnbll languages but consistently fail on tasks outside this class, though prior work has shown that some of these languages are theoretically recognizable under more
permissive idealizations [ 31 49 51 Notably, we use ppegel-ie (32-bit) floating-point numbers, and the string lengths never exceed the maximum attention span of the transformer. That is, attention can uniformly cover all prior positions without numerical underflow or overflow. Yet, despite these favorable conditions, the transformer exhibits no expressive power beyond what is predicted by our formal characterization. more detailed breakdown of the results can be found in 1.33
6.2 Language modeling
We now turn to experiments on language modeling, focusing on three representative languages: RDP- 1, LDP-2, and LDP-1. The corresponding automata are illustrated in Fig. 3 We train the transformer LMs using the standard cross-entropy loss. For evaluation, a predicted symbol is considered correct has non-zero probability under the target distribution p induced by the DFA. Per-token accuracies are reported in Tab. 3 The transformer LM successfully learns LDP-1 1 and LDP-2 with perfect accuracy. For RDP-1, the best performance reaches 98.3%, but the model consistently falls short of achieving 100.0%. This gap becomes more evident upon inspecting the hidden states of the model.
Table Language recognition experiments. Language classes are ordered by decreasing complexity. For each class, examples are chosen to be minimally more complex than those in the immediately lower class. Maximum and mean accuracies (# standard deviation) are reported. Exact values of 100.0% accuracy are highlighted in bold.
Transformer
LSTM
Class
Language
max (%)
mean (%)
max (%)
mean (%)
Counter languages
CNT
83.3
53.6 + 8.6
100.0
86.9 + 20.9
Regular languages
PARITY
52.1
50.6 1:: 0.8
100.0
100.0 0.0
DYCK- (1, 2)
83.4
64.2 8.0
100.0
99.3 - 1.0
Star-free
DYCK-(1, 1)
87.7
71.5
100.0
88.8 + 17.3
1.T-2
62.1
57.9 + 2.3
100.0
100.0 + 0.0
RDP-1
90.0
71.1 11.5
100.0
100.0 - 0.0
Unambiguous polynomials
LAST
64.8
57.3 2.7
100.0
100.0 0.0
PT-2
100.0
98.3 0.33333
100.0
99.7 +
IT-1
100.0
+9.8111.8
100.0
93.0
Left-determinittic polynomials
LDP-2
100.0
100.0
100.0
100.0
LDP-1
100.0
9.0
100.0
100.0
FIRST
100.0
9..4
100.0
100.0

---

We extract the representation H at each position n by concatenating the outputs of all self self-attention and feedforward sublayers:
H
H (0.5)
T
H
(14)
To assess whether the model internally tracks the states in the DFAs, we train linear classifier to predict the state the DFA is in upon reading Weens given -n The classifier consists of two linear layers with no intermediate nonlinearity: the first projects to F² for visualization, and the second performs classification. Fig. 2 we plot the 2D projections and overlay the decision boundaries of the classifier.
The visualizations reveal that, for I.DP-I and I.P-2, the transformer does distinguish the states, as their representations are linearly separable. In contrast, for RDP-1, state representations are intermixed. Notably, even when we train neural probe with nonlinearity on the representations, perfect probing accuracy remains elusive. This suggests that the transformer does not learn to fully separate the states in the non-partin corrpattyl ordered DFA corresponding to RDP-1.
Acknowledgments
This publication was made possible by an ETH AI Center doctoral fellowship to Jiaoda Li.
References
[1] Jimmy Lei Ba, Jamie Ryan Kiros, and Geoffrey E. Hinton. Layer normalization. In NIPS Deep Learning Symposium, 2016. URL
[2] Pablo Barcelo, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir Podolskii. Logical languages accepted by transformer encoders with hard attention. In The Twelfth Interna- tional Conference on Learning Representations, 2024. htthhttps://opeeeeeee
net/
forum? frrumidd=gbrüzo00
[3] Satwik Bhattamishra. Kabir Ahuja, and Navin Goyal. On the Ability and Limitations of Transformers to Recognize Formal Languages. In Bonnie Webber, Trevor Cohn, Yulan He, and Yang Liu, editors, Proceedings of the 2020 Conference on Empirical Methods Natural Language Processing (EMNLP), pages 7096-7116, Online, November 2020. Association for Computational Linguistics. doi: 10. 18653/v 1/2020 200200.mmll-mmin.5766
URL https://
lac wellanthelooy.orrg//oo
emnlp ma maain.5766
[4] J.A. Brzozowski and Faith E. Fich. Languages of R-trivial monoids. Journal of Com- puter and System Sciences, 20(1):32 1980. ISSN 0022-00000. doi: https://doi.org/10
10160002-00000189990003.. URL httl::ttps///// wwt.:wwccenne....coc rect. wwt.:rettttttctteeeeeeeoeeeeeeee wcom/scciene////ccccccccc/..o..c
[5] J. Richard Büchi. On a Decision Method in Restricted Second Order Arithmetic, pages 425- 435. Springer New York, New York, NY. 1990. ISBN 978- 1-68---8-881-8166666-111- doi: 1001/ 978-1-4613-
org
[6] Alexandra Butoi, Ghazal Khalighinejad, Anej Svete, Josef' Valvoda, Ryan Cotterell, and Brian DuSell. Training neural networks as recognizers of formal languages. In The Thirteenth International Conference Learning Representations, 2025, WRL htttps://opereeieeee net/
[7] David Chiang. Transformers in uniform TC Transactions on Machine Learning Research, 2025. ISSN 2835-8856. htthhtts:: heetps://openxxevieee 2t wtt.ooouww..222A0000000000000 2A7D4nQuQE
[8] David Chiang and Peter Cholak. Overcoming a theoretical limitation of self-attention. In Smaranda Muresan, Preslav Nakov. and Aline Villavicencio, editors, Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume Long Papers), pages 7654-7664, Dublin, Ireland, May 2022. Association for Computational Linguis- ties. doi: 10. 1/028686//11222.cclll acl hel-long.er 527
URL. https: pects://accaane aoo https:////aaaaaaoooaoaaoooooooao htt.oaogggoo.o/22002222
10

---

[9] David Chiang, Peter Cholak, and Anand Pillay. Tighter bounds on the expressivity of transformer encoders. In Andreas Krause, Emma Brunskill, Kyunghyun Cho. Barbara Engelhardt. Sivan Sabato, and Jonathan Scarlett, editors, Proceedings of the 40th International Conference on Machine Learning, volume 202 of Proceedings of Machine Learning Research, pages 3544-5562 PMLR, 23-29 Jul 2023.
ml htt.gg.........s///....
chiang23a. html
[10) Gregoire Deletang, Anian Ruoss, Jordi Grau-Moya, Tim Genewein, Li Kevin Wenliang, Elliot Catt, Chris Cundy, Mareus Hutter, Shane Legg, Joel Veness, and Pedro Ortega. Neural networks and the chomsky hierarchy, In The Eleventh International Conference on Learning Representations, 2023. URL
httperiwwwwweeeeeeeeeeeeeeeee maet/forum?? www.eiddwdwxxttkkedooeoo
[11] Volker Diekert, Paul Gastin, and Manfred Kufleitnrr. A survey on small fragments of first-order logic over finite words. International Journal of Foundations of Computer Science, 19(03): 513-548, 2008, doi:
URL
50129054108005302
[12] Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, Anirudh Goyal, Anthony Hartshom, Aobo Yang. Archi Mitra, Archie Sravankumar, Artem Korenev, Arthur Hinsvark, Arun Rao, Aston Zhang, Aurelien Rodriguez, Austen Gregerson, Ava Spataru, Baptiste Roziere, Bethany Biron, Binh Tang, Bobbie Chern, Charlotte Caucheteux, Chaya Nayak, Chloe Bi, Chris Marra, Chris McConnell, Christian Keller, Christophe Touret, Chunyang Wu, Corinne Wong, Cristian Canton Ferrer, Cyrus Nikolaidis, Damien Allonsius, Daniel Song, Danielle Pintz, Danny Livshits, David Esiobu, Dhruv Choudhary, Dhruy Mahajan, Diego Garcia-Olano, Diego Perino, Dieuwke Hupkes, Egor Lakomkin, Ehab AlBadawy, Elina Lobanova, Emily Dinan, Eric Michael Smith, Filip Radenovic, Frank Zhang, Gabriel Synnaeve, Gabrielle Lee, Georgia Lewis Anderson, Graeme Nail, Gregoire Mialon, Guan Pang, Guillem Cucurell, Hailey Nguyen, Hannah Korevaar, Hu Xu, Hugo Touvron, Iliyan Zarov, Imanol Arrieta Ibarra, Isabel Kloumann, Ishan Misra, Ivan Evtimov, Jade Copet, Jaewon Lee, Jan Geffert, Jana Vranes, Jason Park, Jay Mahadeokar, Jeet Shah, Jelmer van der Linde, Jennifer Billock, Jenny Hong, Jenya Lee. Jeremy Fu, Jianfeng Chi, Jianyu Huang, Jiawen Liu, Jie Wang. Jiecao Yu, Joanna Bitton, Joe Spisak, Jongsoo Park, Joseph Rocca, Joshua Johnstun, Joshua Saxe, Junteng Jia, Kalyan Vasuden Alwala, Kartikeya Upasani, Kate Plawiak, Ke Li, Kenneth Heafield, Kevin Stone, Khalid El-Arini, Krithika Iyer, Kshitiz Malik, Kuenley Chiu, Kunal Bhalla, Lauren Contala-Yeary Laurens van der Maaten, Lawrence Chen, Liang Tan, Liz Jenkins, Louis Martin, Lovish Madaan, Lubo Malo, Lukas Blecher, Lukas Landzaat, Luke de Oliveira, Madeline Muzzi, Mahesh Pasupuleti, Mannat Singh, Manohar Paluri, Marcin Kardas, Mathew Oldham, Mathieu Rita, Maya Pavlova, Melanie Kambadur, Mike Lewis, Min Si, Mitesh Kumar Singh, Mona Hassan, Naman Goyal, Narjes Torabi, Nikolay Bashlykov, Nikolay Bogoychev, Niladri Chatterji. Olivier Duchenne. Onur Çelebi. Patrick Alrassy, Pengchuan Zhang, Pengwei Li, Petar Vasic, Peter Weng, Prajiwal Bhargava, Pratik Dubal, Praveen Krishnan, Punit Singh Koura, Puxin Xu, Qing He, Qingxiao Dong. Ragavan Srinivasan, Raj Ganapathy, Ramon Calderer, Ricardo Silveira Cabral, Robert Stojnic, Roberta Raileanu, Rohit Girdhar, Rohit Patel, Romain Sauvestre, Ronnie Polidoro, Roshan Sumbaly, Ross Taylor, Ruan Silva, Rui Hou, Rui Wang, Saghar Hosseini, Sahana Chennabasappa, Sanjay Singh, Sean Bell, Seohyun Sonia Kim, Sergey Edunov, Shaoliang Nie. Sharan Narang. Sharath Raparthy, Sheng Shen, Shengye Wan, Shruti Bhosale, Shun Zhang, Simon Vandenhende, Soumya Batra, Spencer Whitman, Sten Sootla, Stephane Collot, Suchin Gururangan, Sydney Borodinsky, Tamar Herman, Tara Fowler, Tarek Sheasha, Thomas Georgiou, Thomas Scialom, Tobias Speckbacher, Todor Mihaylov, Tong Xiao, Ujjwal Karn, Vedanuj Goswami, Vibhor Gupta, Vignesh Ramanathan, Viktor Kerkez, Vincent Gonguet, Virginie Do Vish Vogeti, Vladan Petrovic, Weiwei Chu, Wenhan Xiong, Wenyin Fu, Whitney Meers, Xavier Martinet, Xiaodong Wang, Xiaoqing Ellen Tan, Xinfeng Xie, Xuchao Jia, Xuewei Wang. Yaelle Goldschlag, Yashesh Gaur, Yasmine Babaei, Yi Wen, Yiwen Song. Yuchen Zhang. Yue Li, Yuning Mao, Zacharie Delpierre Coudert, Zheng Yan, Zhengxing Chen, Zoe Papakipos, Aaditya Singh, Aaron Grattafiori, Abha Jain, Adam Kelsey, Adam Shajnfeld, Adithya Gangidi, Adolfo Victoria, Ahuva Goldstand, Ajay Menon, Ajay Sharma, Alex Boesenberg, Alex Vaughan, Alexei Baevski, Allie Feinstein, Amanda Kallet, Amit Sangani, Anam Yunus, Andrei Lupu, Andres Alvarado, Andrew Caples, Andrew Gu, Andrew Ho, Andrew Poulton, Andrew Ryan, Ankit Ramchandani, Annie Franco, Aparajita
11

---

Saraf, Arkabandhu Chowdhury, Ashley Gabriel, Ashwin Bharambe, Assaf Eisenman, Azadeh Yazdan. Beau James, Ben Maurer, Benjamin Leonhardi, Bernie Huang, Beth Loyd, Beto De Paola, Bhargavi Paranjape, Bing Liu, Bo Wu, Boyu Ni, Braden Hancoek, Bram Wasti, Brandon Spence, Brani Stojkovic, Brian Gamido, Britt Montalvo, Carl Parker, Carly Burton, Catalina Mejia, Changhan Wang. Changkyu Kim, Chao Zhou, Chester Hu, Sching-Hsiane Chu, Chris Cai, Chris Tindal, Christoph Feichtenhofer, Damon Civin, Dana Beaty, Daniel Kreymer, Daniel Li, Danny Wyatt, David Adkins, David Xu, Davide Testuggine, Delia David, Devi Parikh, Diana Liskovich, Didem Foss, Dingkang Wang. Due Le, Dustin Holland, Edward Dowling, Eissa Jamil, Elaine Montgomery. Elconora Presani, Emily Hahn, Emily Wood, Erik Brinkman, Esteban Arcaute, Evan Dunbar, Evan Smothers, Fei Sun, Felix Kreuk, Feng Tian. Firat Ozgenel, Francesco Caggioni, Francisco Guzmán, Frank Kanayet, Frank Seide, Gabriela Medina Florez, Gabriella Schwarz, Gada Badeer, Georgia Swee, Gil Halpern, Govind Thattai, Grant Herman, Grigory Sizov, Guangyi, Zhang. Guna Lakshminarayanan, Hamid Shojanazeri, Han Zou, Hannah Wang, Hanwen Zha, Haroun Habeeh, Harrison Rudolph, Helen Suk, Henry Aspegren, Hunter Goldman, Ibrahim Damlaj, Igor Molybog, Igor Tufanov, Irina-Elena Veliche, Itai Gat, Jake Weissman, James Geboski, James Kohli, Japhet Asher, Jean-Baptiste Gaya, Jeff Marcus, Jeff Tang. Jennifer Chan, Jenny Zhen, Jeremy Reizenstein, Jeremy Teboul, Jessica Zhong, Jian Jin, Jingyi Yang. Joe Cummings, Jon Carvill, Jon Shepard, Jonathan McPhie, Jonathan Torres, Josh Ginsburg, Junjie Wang, Kai Wu, Kam Hou U, Karan Saxena, Karthik Prasad, Kartikay Khandelwal, Katayoun Zand, Kathy Matosich, Kaushik Veeraraghavan, Kelly Michelena, Keqian Li. Kun Huang, Kunal Chawla, Kushal Lakhotia. Kyle Huang, Lailin Chen, Lakshya Garg, Lavender A, Leandro Silva, Lee Bell, Lei Zhang, Liangpeng Guo, Licheng Yu, Liron Moshkovich, Luca Wehrstedt, Madian Khabsa, Manav Avalani, Manish Bhatt, Maria Tsimpoukelli, Martynas Mankus, Matan Hasson, Matthew Lennie, Matthias Reso, Maxim Groshev, Maxim Naumov, Maya Lathi, Meghan Keneally, Michael L. Seltzer, Michal Valko, Michelle Restrepo, Mihir Patel, Mik Vyatskov, Mikayel Samvelyan, Mike Clark, Mike Macey, Mike Wang. Miquel Jubert Hermoso, Mo Metanat, Mohammad Rastegari, Munish Bansal, Nandhini Santhanam, Natascha Parks, Natasha White, Navyata Bawa, Nayan Singhal, Nick Egebo. Nicolas Usumier, Nikolay Pavlovich Laptev, Ning Dong, Ning Zhang, Norman Cheng, Oleg Chernoguz, Olivia Hart, Omkar Salpekar, Ozlem Kalinli, Parkin Kent, Parth Parckh, Paul Saab, Pavan Balaji, Pedro Rittner, Philip Bontrager, Pierre Roux, Piotr Dollar, Polina Zvyagina, Prashant Ratanchandani, Pritish Yuvraj, Qian Liang, Rachad Alao, Rachel Rodriguez, Rafi Ayub, Raghotham Murthy, Raghu Nayani, Rahul Mitra, Raymond Li, Rebekkah Hogan, Robin Battey, Rocky Wang. Rohan Maheswari, Russ Howes, Ruty Rinott, Sai Jayesh Bondu, Samyak Datta, Sara Chugh, Sara Hunt, Sargun Dhillon, Sasha Sidorov, Satadru Pan, Saurabh Verma, Seiji Yamamoto, Sharadh Ramaswamy, Shaun Lindsay, Shaun Lindsay, Sheng Feng, Shenghao Lin, Shengxin Cindy Zha, Shiva Shankar, Shuqiang Zhang, Shuqiang Zhang, Sinong Wang, Sneha Agarwal, Soji Sajuyigbe. Soumith Chintala, Stephanie Max, Stephen Chen, Steve Kehoe, Steve Satterficld, Sudarshan Govindaprasad, Sumit Gupta, Sungmin Cho, Sunny Virk, Suraj Subramaniam, Sy Choudhury, Sydney Goldman, Tal Remez, Tamar Glaser. Tamara Best, Thilo Kohler, Thomas Robinson, Tianhe Li, Tianjun Zhang, Tim Matthews, Timothy Chou, Tzook Shaked, Varun Vontimitta, Victoria Ajayi, Victoria Montanez, Vijai Mohan, Vinay Satish Kumar, Vishal Mangla, Vitor Albiero, Vlad lonescu, Vlad Poenaru, Vlad Tiberiu Mihailescu, Vladimir Ivanov, Wei Li, Wenchen Wang. Wenwen Jiang. Wes Bouaziz, Will Constable, Xiaocheng Tang, Xiaofang Wang, Xiaojian Wu, Xiaolan Wang, Xide Xia, Xilun WU, Xinbo Gao. Yanjun Chen, Ye Hu, Ye Jia, Ye Qi, Yenda Li, Yilin Zhang, Ying Zhang, Yossi Adi, Youngjin Nam, Yu, Wang, Yuchen Hao, Yundi Qian, Yuzi He, Zach Rait, Zachary Vitioo, Zef Rosnbrick, Zhaoduo Wen, Zhenyu Yang, and Zhiwei Zhao. The llama 3 herd of models. Computing Research Repository, Version 2.
arXiv:2407.21783 2024. URL bttpss://aaae http:p/:/aaaav...o//aa///////// wtt.orgggg......ooe.orr 21783
[13] K. Etessami and T. Wilke. An until hierarchy for temporal logic. In Proceedings 11th Annual IEEE Symposiam on Logic in Computer Science, pages 108-117, 1996. doi: 10.1 1996.561310. URL httttps://leeexllrrrt www.eeeeeeeeeoooeeeeeeeeeeeeeeee wttp///oommmm///511110
[14) Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke, First-order logic with two variables and unary temporal logic. Information and Computation, 179(2):279-295 2002. ISSN 0890- 5401, doi: http::/ddoooogg//....ommiinnnono
Utt www. sci eeceeiiceiiicc rect
com/ ccw.://ciinooearttreeeees////sa1
12

---

[15] Patrick C. Fischer, Albert R. Meyer, and Amold L. Rosenberg. Counter machines and
counter languages. Mathematical systems theory, 2:265-283, 1968. URL htttp:://iink
spri ingerrrr.. www.comccccoooooooo httpc///arr...eee....110////111/
[16] Dov Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. On the temporal analysis of fairness. POPL '80. page 163-173, New York, NY, USA, 1980. Association for Computing Machinery. ISBN 0897910117. doi: 10.1 10.1145/567446.567444
URthttps::/ /tt////o.... org/
10.1145/567488 627462
[17] Michael Hahn. Theoretical limitations of self-attention in neural sequence models. Transactions of the Association for Computational Linguistics, 8:156-177 2020. doi: 10.1 a 00306. URL htttpsss/aalanthooooy..ooo
[18] Yiding Hao, Dana Angluin, and Robert Frank. Formal language recognition by hard at- tention transformers: Perspectives from circuit complexity. Transactions of the Associa- tion for Computational Linguistics, 10:800-810, 2022. doi: 10.1162/tacl a 00490. URL
ht https::/aclanttoo.ggs wwwp://oyw..r.//2....ooo tac.z2..acl12 1.46
[19] Dan Hendrycks, Collin Burns, Steven Basart, Andy Zou, Mantas Mazeika, Dawn Song, and Jacob Steinhardt. Measuring massive multitask language understanding. International Con- ference on Learning Representations, 2021. URL
wwwp://wwwwwww..eeeeeeeeeeeeeeee forum?
id=d7KB jmi 3GmQ
[20] Sepp Hochreiter and Jürgen Schmidhuber. Long short-term memory. Neural computation, 9: 1735-80, 12 1997. doi: 10. 6t2///co.1997.9.... 1735. URL.htttp::/// acm. www..orrgooooooo
10.1162/neco. 1997 9. 1735
[21] Cheng-Zhi Anna Huang, Ashish Vaswani, Jakob Uszkoreit, Ian Simon, Curtis Hawthorne, Noam Shazeer, Andrew M. Dai, Matthew D. Hoffman, Monica Dinculescu, and Douglas Eck. Music transformer. In The Seventh International Conference on Learning Representations, URL
2019.
[22] Xinting Huang, Andy Yang, Satwik Bhattamishra, Yash Sarrof, Andreas Krebs, Hattie Zhou, Preetum Nakkiran, and Michael Hahn. A formal framework for understanding length generaliza- tion in transformers. In The Thirteenth International Conference on Learning Representations, 2025. URL https::/
www.:net/ffrmm///o net. forum? d=1J4 9NSV51 rU
[23] IEEF. Teee standard for Doating-point arithmetic. IEEE Std 754-2008, pages 1-70, 2008. doi: 10.1109//EESTTD
[24] Neil Immerman and Dexter Kozen. Definability with bounded number of bound variables. Information and Computation, 83(2):121 139, 1989. ISSN 0890-5401. doi: https://oi.orr//00 1016/0890-54001199990000
URL /ttp:://www.ccceeeeeeeee... com/ comms///eeeertccoocccccceeeeee science/
Articleep11/08905001199990
[25] Johan Anthony Wilem Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Univer- sity of Califoria, Los Angeles, 1968. URL https: www www.:wppwoouu...coomm com/ docview/
302320357
[26] S. C. Kleene. Representation of Events in Nerve Nets and Finite Automata, pages 3-42. Princeton University Press, Princeton, 1956. ISBN 978 400882618, doi: 10.1515/9981440088222 -002
httt:::////o http:///ooo.orgg/0/// 151. ott.atppe//oo.ooooo......15..1..
[27] Zhiyuan Li, Hong Liu, Denny Zhou, and Tengyu Ma. Chain of thought empowers transformers to solve inherently serial problems. In The Twelfth International Conference on Learning Representations, 2024. URL httttps://openrevieete
net net//ooumm 3EWETn
[28] R. McNaughton and S. Papert. Counter-free Automata. M.I.T. Press research monographs. M.I.T. Press, 1971. ISBN 97802621 URL
9780262130769 counter aree-auromata/
13

---

[29]
William Merrill. Sequential neural networks as automata. In Jason Eisner, Matthias Gallé, Jeffrey Heinz, Ariadna Quattoni. and Guillaume Rabusseau, editors, Proceedings of the Workshop on Deep Learning and Formal Languages: Building Bridges, pages 1-13, Florence, August 2019. Association for Computational Linguisties. doi: 10. 1/113//1/11993001.. URL. https
7/aclantho www.aanttoooooooooooooooooo.. ogy. org///r///3 009//1939111 9-09
[30] William Merrill. On the linguistic capacity of real-time counter automata. Computing Research Repository, arXiv:2004.0688 2020. URL
Version 2.
[31] William Merrill and Ashish Sabharwal. A logic for expressing log-precision transformers, In
A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine, editors, Advances in Neu- ral Information Processing Systems, volume 36, pages 52453 Curran Associates, Inc.,
http://eaeapeeeeeeeeaaaaeeeeeeee files//apez/20233 Fi fi122448557770006665155522222333
2023. URL /ts//tttpp////ooeeddngg...ss
Conferrroooffeeeccee.. pdd
[32] William Merrill and Ashish Sabharwal. The parallelism tradeoff: Limitations of log-precision transformers. Transactions of the Association for Computational Linguistics, 1 11:531-545, 2023,
doi: 10.1 121166/2c___a00000 _
BtR.https://att antho wtw.oogg........o. tacll
[33] William Merrill and Ashish Sabharwal. The expressive power of transformers with chain of thought. In The Twelfth International Conference on Learning Representations, 2024. URL https:///penneeveww net htt.aeennnnnttooooooooaaaaannnaa
[34] William Merrill, Ashish Sabharwal, and Noah A. Smith. Saturated transformers are constant- depth threshold circuits. Transactions of the Association for Computational Linguistics, 10: 843 856, 2022. doi: 10. 10.1162/tacl a 00493. URL htttt::s//aclantoooo...... tacl-1.49 49
[35] Franz Nowak, Anej Svete, Alexandra Butoi, and Ryan Cotterell. On the representational capacity reasoning. Lun-Wet Ku, Andre Martins,
of neural language models with and Vivek Srikumar, editors. Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Pupers), pages 12510- 12548, Bangkok, Thailand, August 2024. Association for Computational Linguistics. doi: 676 /tthts::::/ http://////alaatttoooooooor/////
[36] OpenAl. GPT-4 technical report. Computing Research Repository, arXiv:2303.08774, 2023. 2001000000...030077777.7
[37] Amir Pnucli. The temporal logic of programs. In 18th Annual Symposium Foundations of Computer Science (sfcs 1977), pages 46-57, 1977. doi: 1091///SS...197..3... URL
htttps:/ieeexploreee leee..e..... org/ wwrooument/4557700
[38] Jorge Pérez, Javier Marinković, and Pablo Barceló. On the turing completeness of modern neural network architectures. In The Seventh International Conference on Learning Representations, 2019. URL httpthttts///pereeeeeee
ew net./ fo rum? d=HyGBdo0qFm
[39] Peter Shaw, Jakob Uszkoreit, and Ashish Vaswani. Self-attention with relative position rep- resentations. In Marilyn Walker, Heng Ji, and Amanda Stent, editors, Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguis- tics: Human Language Technologies, Volume 2 (Short Papers), pages 464-468, New Orleans, Louisiana, June 2018. Association for Computational Linguistics. doi: (0.18653/1/N18-2200
URL httt::tp//// httpp:://acaanthoooos/ /aaaaaaaaanttoogee org org/N18- 2074
[40] Imre Simon. Piecewise testable events. In H. Brakhage, editor, Automata Theory and Formal Languages, pages 214-222, Berlin, Heidelberg, 1975. Springer Berlin Heidel- berg. ISBN 978-3-540-3392332 1007/3-540-07407-44
URL wtt.:httt/s/llll spri nger. cwm/ cccm//hhater/10
[41] Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R. Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, Agnieszka Kluska, Aitor Lewkowyez, Akshat Agarwal, Alethea Power, Alex Ray, Alex Warstadt, Alexan- der W. Kocurek, Ali Safaya, Ali Tazary, Alice Xiang, Alicia Parrish, Allen Nie, Aman Hussain,
14

---

Amanda Askell, Amanda Dsouza, Ambrose Slone, Ameet Rahane, Anantharaman S. Iyer. Anders Johan Andreassen, Andrea Madotto, Andrea Santilli, Andreas Stuhlmüller, Andrew M. Dai, Andrew La, Andrew Kyle Lampinen, Andy Zou, Angela Jiang, Angelica Chen, Anh Vuong, Animesh Gupta, Anna Gottardi, Antonio Norelli, Anu Venkatesh, Arash Gholamidavoodi, Arfa Tabassum, Arul Menezes, Arun Kirubarajan, Asher Mullokandov, Ashish Sabharwal, Austin Herrick, Avia Efrat, Aykut Erdem, Ayla Karakaş, B. Ryan Roberts, Bao Sheng Loe, Barret Zoph, Bartlomiej Bojanowski, Batuhan Özyurt, Behnam Hedayatnia, Behnam Neyshabur, Benjamin Inden, Benno Stein, Berk Ekmekci, Bill Yuchen Lin, Blake Howald, Bryan Orinion, Cameron Diao, Cameron Dour, Catherine Stinson, Cedrick Argueta, Cesar Ferri, Chandan Singh, Charles Rathkopf, Chenlin Meng, Chitta Baral, Chiyu Wu, Chris Callison- Christian Voigt, Christopher D Manning. Christopher Potts, Cindy Ramirez, Clara E. Rivera, Clemencia Siro, Colin Raffel, Courtney Ashcraft, Cristina Garbacea, Damien Sileo, Dan Gar- rette, Dan Hendrycks, Dan Kilman, Dan Roth, C. Daniel Freeman, Daniel Khashabi, Daniel Levy, Daniel Moseguí González, Danielle Perszyk, Danny Hernandez, Danqi Chen, Daphne Ippolito, Dar Gilboa, David Dohan, David Drakard, David Jurgens, Debajyoti Datta, Deep Ganguli, Denis Emelin, Denis Kleyko, Deniz Yuret, Derek Chen, Derek Tam, Dieuwke Hupkes, Diganta Misra, Dilyar Buzan, Dimitri Coelho Mollo, Diyi Yang. Dong-Ho Lee, Dylan Schrader, Ekaterina Shutova, Ekin Dogus Cubuk, Elad Segal, Eleanor Hagerman, Elizabeth Barnes, Eliza- beth Donoway, Ellie Pavlick, Emanuele Rodolà, Emma Lam, Eric Chu, Eric Tang. Erkut Erdem, Ernie Chang, Ethan A Chi, Ethan Dyer, Ethan Jerzak, Ethan Kim, Eunice Engefu Manyasi, Evgenii Zheltonozhskii, Fanyue Xia, Fatemeh Siar. Fernando purtinez-Plumed Francesca Happé, Francois Chollet, Frieda Rong, Gaurav Mishra, Genta Indra Winata, Gerard de Melo, Germàn Kruszewski, Giambattista Parascandolo, Giorgio Mariani, Gloria Xinyue Wang. Gon- zalo Jaimovitch-Lopez, Gregor Betz, Guy Gur-Ari, Hana Galijasevic, Hannah Kim, Hannah Rashkin, Hannaneh Hajishirzi, Harsh Mehta, Hayden Bogar, Henry Francis Anthony Shevlin, Hinrich Schuetze, Hiromu Yakura, Hongming Zhang, Hugh Mee Wong. Ian Ng, Isaac Noble, Jaap Jumelet, Jack Geissinger, Jackson Kernion, Jacob Hilton, Jachoon Lee, Jaime Fernández Fisac, James B Simon, James Koppel, James Zheng, James Zou, Jan Kocon, Jana Thompson, Janelle Wingfield, Jared Kaplan, Jarema Radom, Jascha Dicksiics,,,,,, Jason Phang, Jason Wei, Jason Yosinski, Jekaterina Novikova, Jelle Bosscher, Jennifer Marsh, Jeremy Kim, Jeroen Taal, Jesse Engel, Jesujoba Alabi, Jiacheng Xu, Jiaming Song, Jillian Tang, Joan Waweru, John Burden, John Miller, John U. Balis, Jonathan Batchelder, Jonathan Berant, Jörg Frohberg, Jos Rozen, Jose Hernandez-Orallo, Joseph Boudeman, Joseph Guerr, Joseph Jones, Joshua B. Tenenbaum, Joshua S. Rule, Joyce Chua, Kamil Kanclerz, Karen Livescu, Karl Krauth, Karthik Gopalakrishnan, Katerina Ignatyeva, Katja Markert, Kaustubh Dhole, Kevin Gimpel, Kevin Omondi, Kory Wallace Mathewson, Kristen Chiafullo, Ksenia Shkaruta, Kumar Shridhar, Kyle McDonell, Kyle Richardson, Laria Reynolds, Leo Gao, Li Zhang, Liam Dugan, Lianhui Qin, Lidia Contreras-Ochanddo Louis-Philippe Morency, Luca Moschella, Lucas Lam, Lucy Noble. Ludwig Schmidt, Luheng He, Luis Oliveros-Colón, Luke Metz, Lütfi Kerem Senel, Maarten Bosma, Maarten Sap. Maartje Ter Hoeve, Maheen Farooqi. Manaal Faruqui, Mantas Mazeika, Marco Baturan, Marco Marelli, Marco Maru, Maria Jose Saamirez-Quintany Marie Tolkiehn, Mario Giulianelli, Martha Lewis, Martin Potthast, Matthew I. Leavitt, Matthias Hagen, Mátyás Schubert, Medina Orduna Baitemirova, Melody Arnaud, Melvin McElrath, Michael An- drew Yee, Michael Cohen, Michael Gu, Michael Ivanitskiy, Michael Starritt, Michael Strube, Michal Swędrowski, Michele Bevilacqua, Michihiro Yasunaga, Mihir Kale, Mike Cain, Mimee Xu, Mirac Suzgun, Mitch Walker, Mo Tiwari, Mohit Bansal, Moin Aminnaseri, Mor Geva, Mozhdeh Gheini, Mukund Varma T, Nanyun Peng. Nathan Andrew Chi, Nayeon Lee, Neta Gur-Ari Krakover, Nicholas Cameron, Nicholas Roberts, Nick Doiron, Nicole Martinez, Nikita Nangia, Niklas Deckers, Niklas Muennighoff, Nitish Shirish Keskar, Niveditha S. Iyer, Noah Constant, Noah Fiedel, Nuan Wen, Oliver Zhang, Omar Agha, Omar Elbaghdadi, Omer Levy, Owain Evans, Pablo Antonio Moreno Casares, Parth Doshi, Pascale Fung. Paul Pu Liang. Paul Vicol, Pegah Alipoormolabashi, Peiyuan Liao, Percy Liang, Peter W Chang, Peter Eckers- ley, Phu Mon Htut, Pinyu Hwang, Piotr Milkowski, Piyush Patil, Pouya Pezeshkpour, Priti Oli, Qiaozhu Mei, Qing Lyu, Qinlang Chen, Rabin Banjade, Rachel Etta Rudolph, Raefer Gabriel, Rahel Habacker, Ramon Risco. Raphaël Millière, Rhythm Garg, Richard Bamnes, Rif A. Saurous, Riku Arakawa, Robbe Raymaekers, Robert Frank, Rohan Sikand, Roman Novak, Roman Sitelew, Ronan Le Bras, Rosanne Liu, Rowan Jacobs, Rui Zhang, Russ Salakhutdinov, Ryan Andrew Chi, Seungjae Ryan Lee, Ryan Stovall, Ryan Teehan, Rylan Yang, Sahib Singh, Saif M. Mohammad, Sajant Anand, Sam Dillavou, Sam Shleifer, Sam Wiseman, Samuel Gruet-
Christopher Waites,
15

---

ter, Samuel R. Bowman, Samuel Stern Schoenholz, Sanghyun Han, Sanjeev Kwatra, Sarah A. Rous, Sarik Ghazarian, Sayan Ghosh, Sean Casey, Sebastian Bischoff, Sebastian Gehrmann, Sebastian Schuster, Sepideh Sadeghi, Shadi Hamdan, Sharon Zhou, Shashank Srivastava, Sherry Shi, Shikhar Singh, Shima Asaadi, Shixiang Shane Gu, Shubh Pachchigar, Shubham Toshniwal, Shyam Upadhyay, Shyamolima Shammie Debnath, Siamak Shakeri, Simon Thormeyer, Simone Melzi, Siva Reddy, Sneha Priscilla Makini, Soo-Hwan Lee, Spencer Torene, Sriharsha Hatwar, Stanislas Dehaene, Stefan Divic, Stefano Ermon, Stella Biderman, Stephanie Lin, Stephen Prasad, Steven Piantadosi, Stuart Shieber, Summer Misherghi, Svetlama Kiritchenko, Swaroop Mishra, Tal Linzen, Tal Schuster, Tao Li, Tao Yu, Tariq Ali, Tatsunori Hashimoto, Te-Lin Wu, Théo Desbordes, Theodore Rothschild, Thomas Phan, Tianle Wang, Tiberius Nkinyili, Timo Schick, Timofei Kornev, Titus Tunduny, Tobias Gerstenberg, Trenton Chang, Trishala Neeraj, Tushar Khot, Tyler Shultz, Uri Shaham, Vedant Misra, Vera Demberg, Victoria Nyamai, Vikas Raunak, Vinay Venkatesh Ramasesh, vinay uday prabhu, Vishakh Padmakumar, Vivek Srikumar, William Fedus, William Saunders, William Zhang. Wout Vossen, Xiang Ren, Xiaoyu Tong, Xinran Zhao, Xinyi Wu, Xudong Shen, Yadollah Yaghoobzadeh, Yair Lakretz, Yangqiu Song, Yasaman Bahri, Yejin Choi, Yichi Yang. Sophie Hao, Yifu Chen, Yonatan Belinkov, Yu Hou, Yufang Hou, Yuntao Bai, Zachary Seid, Zhuoye Zhao, Zijian Wang, Zijie Wang. Zirui Wang. and Ziyi Wu. Beyond the imitation game: Quantifying and extrapolating the capabilities of language models. Transactions on Machine Learning Research, 2023. ISSN 2835-8856. URL https: openreviee net forum 1dd
Featured Certification.
[42] Lena Strobl, William Memill, Gail Weiss, David Chiang, and Dana Angluin. What formal languages can transformers express? a survey. Transactions of the Association for Computa- lional Linguistics, 12:543-561 05 2024. ISSN 2307-387X. doi: 10.1 10.1162taclaa_0000 00066... URL
https: / www.lo.rgr1...0 11t.11122ata...
00663
[43] Jianlin Su, Murtadha Ahmed, Yu Lu, Shengfeng Pan, Wen Bo, and Yunfeng Liu. Roformer: Enhanced transformer with rotary position embedding. Neuroccoputting, 568: 12706,, 2024. ISSN 0925-2312. doi: http://////go//o///////////////0
hwtp::/...cccccc..o....... 127066. URL https: //ww www
sciencedirect httpa//cc...cooo..o.occ..a/aea/s
[44]
Anej Svete and Ryan Cotterell. Transformers can represent n-gram language models. In Kevin Duh, Helena Gomez, and Steven Bethard, editors, Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume I: Long Pupers), pages 6845 -888, Mexico City, Mexico, June 2024. Association for Computational Linguistics. doi:
URL http:::ttt//t......... hatpa/aaaantttootoooo/ wwg.bo24g//22224 wwwp22222.aaa1l-aa11 nww.laaalll-ccmmm hwa.c-aaannnngg.a 381/
[45] Pascal Tesson and Denis Thérien. Diamonds are forever: The variety DA, pages 475-499.
2002. doi: 10. 10.1114299889881776688 0021. URL https:/ wwww.wwwwooomoo www.wooieeeciniiiccccmc
hom//oi/abs//in /1t.:///ab//11.11/9/99/93399
0021
[46] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, ukasz Kaiser, and Illia Polosukhin. Attention all you need. In I. Guyon, U. Von Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, editors, Ad- vances in Neural Information Processing Systems, volume 30. Curran Associates, Inc., 2017. 2017//111/
URL MRRlttpps://prcceedingg neurips........p..po.....r wttp:/cccpppppeeeeeee Paper. pdf
3f
[47] Alex Wang, Yada Pruksachatkun, Nikita Nangia, Amanpreet Singh, Julian Michael, Felix Hill, Omer Levy, and Samuel Bowman. Superglue: A stickier benchmark for ameral-purpose language understanding systems. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32. Curran Associates, Inc., 2019. URL httppsss//ppooeedisss....eeppppp pecps//....................ppr filees/papex/203//ELL 44 44366722afee77766666668448883883
[48] Gail Weiss, Yoav Goldberg, and Eran Yahav. On the practical computational power of finite precision RNNs for language recognition. In Iryna Gurevych and Yusuke Miyao, editors, Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), pages 740-745, Melboume, Australia, July 2018. Association for
16

---

Computational Linguistics. doi: 12..88653/1//118-2110 URL https::/aallattho...o
erq/P18-2117
[49] Andy Yang and David Chiang. Counting like transformers:
Compiling temporal counting logic into softmax transformers. In First Conference Language Modeling, 2024. URL
https://openreview
[50] Andy Yang, David Chiang, and Dana Angluin. Masked hard-attention transformers recognize exactly the star free languages. Computing Research Repository, arXiv:2310.13897 2024. URL
https: arxiv. org/ abs/2310. 13897
Version 3.
[51] Shunyu Yao, Binghui Peng, Christos Papadimitriou, and Karthik Narasimhan. Self-attention networks can process bounded hierarchical languages. In Chengqing Zong, Fei Xia, Wen- jie Li, and Roberto Navigli, editors, Proceedings of the 59th Annual Meeting of the Asso- ciation for Computational Linguistics and the 11th International Joint Conference on Nat- ural Language Processing (Volume 1: Long Pupers), pages 3770-3785, Online, August 2021. Association for Computational Linguistics. doi: 10. (0.18633/v1/000 1/2021 aall-long.292. URL https: //a:: antho ogy org /2011 long- 292
A
Background
In this section, we provide background information that was omitted from the main text for brevity. We include here for the sake of completeness.
A.1
Temporal logic
Temporal logic 37 is special case modal logic, with modalities referring to time.
A.1.1 LT,(P,F,S,U)
Linear temporal logic L,L U] includes four temporal operators: P (past), F (future)), (since) and U (until) Notably, P. F, and one of S or U can be omitted without loss of expressive power [16]. We write T to denote TRUE and 1. to denote FALSE. The semantics of the formulas defined inductively as follows:
w, + T. iff the th symbol of is an a.
w, 72 = eh A 2he iff w, n F tha and w, n 1/2-
w, 7 += - iff w. + sb.
m + Pib iff there exists such that
and w, m - tb
w,n += Fib iff there exists m such that m > n and w, m = th.
w,n += Syin iff there exists m such that m < n, W. m
} 12. and for every k such that
m n, }= 4/1.
w. = t U2/2 iff there exists m such that m > n, w, m }= 122 and for every k such that
m, 2/1
Example:
abb, == the first symbol is
abb,3 P as an occurs before position
abb,3 = ST, as n. holds at position (before position 3), and my holds at every position between and 3.
To say a string w of length satisfies a formula v, written as w } w, we imagine we start at a position outside the string, e.g., position 0 or N 1.
17

---

Example:
abb + myST the formula is satisfied at position 4, outside the string.
abb + n. U as the formula is satisfied at position 0, outside the string.
The language defined by formula dà is the set of all strings that satisfy v), denoted by [L(1)):
L(w) del E E"
(15)
Example:
(TA)Taa = ab"""
(16a)
L (T_ Umb) a'bE"
(16b)
We define the operator depth of formula vb denoted od( as the maximum number of nested temporal operators in v. defined recursively as follows:
(d(
(1/1/1 A 222) = (d)
od( ((-b) od(v/)
od (v) od(U)) +1
od(F+) od(v)) +1
(1 Stb2)
(d(2))) +
od( v) U max(od((5) od (v2))
A.1.2 LTL
Unary temporal logic [PL F] is the fragment of LTL(P,, F,S. U] that excludes the binary operators S and U. This restriction renders LTL[P, strictly less expressive than L, U] 13 14
Example:
Consider the language consisting of all words that begin with and end with b. To enforce that word starts with a, we require that occurs at the beginning of the word, i.e., it is preceded by nothing. This can be expressed as P(m, A -PT). Symmetrically, ending with can be expressed using the dual condition involving F. Thus, the formula
L(P(Ta, A PPT) P(m. A -FT)) = aE'b
(17)
defines the desired language.
A.1.3 LTL(P)
We define [PL[[P] as the past fragment of LPL F). which excludes the F operator. Proposition A.1. LTL[P] is strictly less expressive than [..
Proof. Since LTL(P] is syntactic fragment of LTL,P, FJ. every formula expressible in LTL is also expressible in [PL F). To establish strictness, it suffices to exhibit language definable in LTL P.P. F that is not definable in [P] Consider again the language aE*b. It is definable in [P] as expressing the end of a string requires the ability to look forward, which LPL lacks.
A.2 First-order logic
The seminal work of Büchi 5 demonstrated how properties of languages can be described using logical formulas, while McNaughton and Papert 28 was the first to restrict these formulas to first-order logic (FO[<)).
18

---

A.2.1 F
The atomic formulas of FO [] consist of unary predicates for each E Σ and binary numerical predicate < that can be used determine the sequential order between variables. Formulas FO |<] may use arbitrarily many variables. However, it has been shown that three variables are both necessary and sufficient to define all first-order definable languages [25 24). addition to the usual Boolean connectives A and m, there is an existential quantifier 3. The formulas in FO [<] are constructed inductively as follows:
Every atomic formula is a formula;
Boolean combination of formulas a formula;
(()..... is a formula, so is 3x : o(z,...);
The universal quantifier V can be defined follows:
Vx :ez....... _ -3x -o(x......
(18)
formula with no free variables is called sentence. We write F= Ø if di is satisfied for under the interpretation, where variables range over the positions in w, unary predicates T, (x) hold if the symbol at position is a, and is interpreted as the natural order positions. A sentence & can define a language, the set of strings over Σ satisfying it, denoted as L()).
Example:
The formula below defines the language a bb::
BrVydz (T= S
(19)
where x S y is shorthand for x < y VVV==
The quantifier depth of formula Φ denoted )d is defined recursively as follows:
qd(m=a)
(d(@1 A Φ2) = max (d1)
qd( (d)-)) qd())
qd( E2:: ((), (d()) +1
is well known that [O[<] and LTL F,S, U| are equivalent in expressive power 25 and they both define exactly the class of star-free languages (28).
A.2.2
[
F [<] the fragment of FO[<] restricted using only two distinct variables (typically reused via quantification).
Example:
The formula Eq. (19 can written as a formula FO as follows:
3x (I) A Vy (a S Br (y S x A (=)))).
(20)
which uses only two distinct variables and y.
It is shown that LTL F] and FO² [<] recognize precisely the same languages
[14
A.2.3 PFO*
We define PFO [<] as the past fragment (FO(<)) in which formulas are restricted so that whenever free variable x is present, every existential quantifier must be of the form Fy < r.. This ensures that all quantification limited to positions or before x, i.e., only past positions relative to the free variable accessed.
19

---

PFO < has precisely the same expressive power as LTL(P]. We establish this equivalence by providing translations both directions.
Lemma A.2. Every formula &b in L.TL(P] can be translated into an equivalent single-variable
formula ((z) [+)
Proof. We proceed by structural induction the formula vb.
Base case. If Wa. translate it to ((x) na (2:).
Induction step. Assume 1t1 and 1/2 can be translated into d1 (x) and Φ2(x) respectively, We translate compound formulas as follows:
If d 1 A 22, then o(x) A
If d 1 then d(x) -01(2)) (z).
t = Pt/1, then ((x) = By < x 61
each case, the resulting formula (xx) belongs to PFO* since it uses at most two variables (the free variable and bound variable y), both of which can be reused.
Lemma A.3. Every single-variable formula (xx) in [F] can be translated into equivalent formula & in []
Proof. We proceed by induction on the quantifier depth qd()).
Base case. If (d 0, then ((x) is Boolean combination of atomic formulas such as va (x), which are directly translatable into [P] formulas.
Induction step. Assume that every formula of quantifier depth at most can be translated into an equivalent LTL formula. Consider a formula ((x) of depth k 1. The formula can be written as a Boolean combination of:
Subformulas of quantifier depth at most k which can be translated into LTL[P] by the inductive hypothesis;
Subformulas of the form By < 2 (1()), where Φ1 has depth most k. By the inductive hypothesis, d (v) translates to a [P] formula whi and the whole subformula translates to a = P
Combining the two lemmas, we obtain the following theorem.
Theorem 2.1. PFO [<] and LTL(P) have the same expressive power.
Proof. The result follows directly from Lemma A.2 and Lemma A.3 To define languages, [] formulas are interpreted position N 1. Similarly, PFO formulas with single variable x can be converted into sentences by prefixing them with Er, which is semantically equivalent to Rr N 1.
B Transformers
In this section, we describe the transformer idealization under consideration in more detail. The formal proofs for the following two results are also given: (i) every transformer be translated into an equivalent 2FO² formula, and (ii) every LTL(P) formula can be simulated by transformer.
20

---

B.1 Transformer architecture
The assumptions we make are restated as follows:
Assumption 3.1. We assume that the transformer satisfies the following conditions:
1. Fixed precision: There exists finite set of values that the floating-pone point numbers assume. We denote this set as IF f2..22......
2. No positional encoding (NoPE): Positional encodings are omitted for now, but are addressed in FF.
Soft attention: Attention weights are computed using the softmax function.. We also treat average hard atlention (ATIA) in SF.1. showing that AHA is equally expressive as soft atlention.
Strict future masking: As in Yang et al. [50], the attention strictly future-mskkdd Strict masking is shown be more expressive than non-strict masking in F22
Recognition: Following standard practice in expressivity studies 42), the transformer treated
as language recognizer. We will extend the analysis to transformer language models in $
We denote the of non-negative floating-poine numbers 2g C F. Similar notation is used for positive numbers, negative numbers, and other subsets. The set I includes two special values, oc and oc, representing positive and negative infinity. Their behaviors defined follows:
Yf F {-00), 00 del
vf F f 0o del
-0 and f (-00) del oo;
oc;
Yf E ( (-00, -00 + -o;
Af foc, -00 f/00 _ 0:
Vf E Fso. f
and f (-o0)
exp(oo) and exp(-oo) = 0.
Transformers take strings as inputs. Given a string w = Wi ... over an alphabet E, we append special end-of-sentence symbol EOS & E to form the extended string def extended alphabet ø Σ U {EOS).
W1 FOS the
The transformer consists of an input layer, followed by stack of L hidden layers and a final output layer.
B.1.1 Input layer
An embedding function of type Σ + FD maps each symbol to a D-dimensional column vector. The embedding layer applies each symbol w to produce the input representation: E(w) EDx(N+1), i.e.
w
der e(wn), n E (1,...,,N . 1
(21)
where WN+1 BOS.
B.1.2
Hidden layers
Each hidden layer contains two sublayers: self-attention mechanism and feedforward network.
The self-attention mechanism is function of type DDx(N+1) DD+(1+1), Given input H(w)
DD++++1), we compute:
H (w),
(22a)
K
(22b)
H(W),,
(22c)
where O K @ E D are learnable parameter matrices.
A pairwise compatibility score S E I(N++)x(NN+) is computed via scaled dot product:
K Kmm.
Sn.m
(23)
21

---

We then compute attention weights E F(N+1)X(N+1) using softmax:
exp n
def
(24)
(S,,)
iin
In practice, the softmax numerically stabilized by subtracting the maximum score from all scores before exponentiation:
exp(S max;<n Sa,s)
def
(25)
jen exp(Snn - maxica Sn.i)
The attention output at position is then computed as a weighted sum of the value vectors:
W def Σ On.m V V.m-
(26)
We assume single attention head, since multiple heads do not increase expressive power 27
The feedforward sublayer is function of type FDx(N+1) - (N+(1))) and consists of two linear transformations with ReLU nonlinearity:
F(H(W)) 2 (OF) ((W).((...... + b + b
(27)
where e E FD'xD bel FD', O DD'xD b pp trainable parameters, D' is the
hidden size of the intermediate layer.
B.1.3
Output layer
The final output layer is a function of type DDx - IF that computes scalar score based on the representation at the final position (corresponding to EOS):
C ((H( (0)) H WAN+I + +
(28)
where 8C F and bc E FF are learnable parameters.
B.2 From transformers to PFO
In this sub-section, we show that any transformer can be simulated by PFO* We begin by formalizing what means for a function to be simulated by PFO* With a slight abuse of notation, write D to refer either to the model's hidden dimensionality or to in the case of scalar classification output.
Definition B.1. ffuunction H: NN (DX(N+)) said to be simulated by PFO (<] for every dimension d E (1...., D} and every floating-point value f E F, there exists single-variable formula x(x) in [<) such that for every position E +11..
H(w) am =
if and only if
w. w
(29)
Similarly, function H of type E N+1 - (N++) is said to be simulated by PFO for every floating- point value F, there exists a two-variable formula o(x, y) in PFO such that for every pair of positions n, m E [I,...,N + 1}.
H = and only if w. 6(x,)).
(30)
We will prove the following proposition, which we will use repeatedly.
Proposition B.2. Let H, H2 be functions of type E N+1 + FD, and let H be either function
RD RD' (where D' is not necessarily equal D) or FD RDD - F. both H1 and H2 can be simulated by PFO? then so can H(H;) and H(H, Hz).
Proof. Since the inputs are diee-diimnsiooal vectors over F, the number of possible value combi- nations is finite. For any given output value F, one enumerate all input configurations for which the function yields f. and construct a 2 formula expressing their disjunction.
22

---

This proposition accounts for all components of the transformer architecture, such as the feedforward sublayers, projection operations, dot products, elementwise operations such as addition, scalar operations such division, the exp function, and the classification head- for the embedding layer, the summations involved in the attention computation, and the operation of identifying the maximum score introduced by the stabilized softmax.
We handle the embedding layer as follows:
Lemma B.3. The embedding layer can be simulated by [<)
Proof. For any dimension d and position n, the embedding layer outputs fixed value I' the symbol at position n is mapped to f by the embedding function e in the d-th coordinate. Since E is finite and is fixed, we can express this using a disjunction over all symbols that are mapped to f in coordinate d:
w d,n f
if and only if Wnn aE(ale(a)a f
V
Te(x).
(31)
We next address the summations in the attention mechanism. We begin by establishing the following result:
Proposition B.4. P=)* can count up to threshold.
Proof. The threshold counting quantifiers can be defined as follows.
The quantifier for "there exists at least one" coincides with the standard bounded existential
quantifier:
y < x Φly) ~ By < x oly).
(32)
"There exist at least two" can be defined as:
2 y < x x(v) By < x (o(v) ^ Ex < y 6(x)).
(33)
We can define "exactly one" by combining the above:
3' < <by) 3ー! < s(v) A -322 < x d(v).
(34)
Additional counting quantifiers up to a threshold can be defined in a similar fashion.
Soft attention involves two types of summations, which we address turn. The first appears in the denominator of the softmax function, used to compute the attention weights (Eq. (24). Since exp
outputs non-negative values, this summation consists entirely of non-negative numbers and can be simulated by PFO [<].
Lemma B.S. PFO* can simulate a sum of non-negative fixed-ppecision floatiniiiiioooooiiigggeaog dloating-poin numbers.
Proof. Since Fzo is finite, there exists a finite non-negative, for each such sum there are only finitely many combinations of input values that yield it. Each combination can be characterized using the threshold-counting quantifiers introduced in Proposition B.4 Too many positive entries lead to overflow, while O's do not affect the sum. Taking finite disjunction over all such combinations defines a 2FO formula that holds exactly when the prefix equals given value.
possible sums. Moreover, because all values are
The second summation occurs in the computation of attention outputs (Eq. 26 The value matrix V (N+(N++) may include both positive and negative values, so we cannot apply the previous approach directly. However, as pointed out by Merrill and Sabharwal (31]
Proposition B.6. Under fixed precision, there exists upper limit the number of non-zero entries the output of softmax function. We refer to the upper bound as the maximum attention span
N Nmax-
23

---

Proof. This upper bound is given by:
min max (oo)))
N Nmax
(35)
min(F
where [.] the floor function.
Consequently, the number of nonzero attention weights is bounded. It follows that Eq. 26 the sum over bounded number of terms, which can be simulated by PFO*|<]:
computes
Lemma B.7. [=) can simulate sum of a bounded number of numbers.
Proof. Since the number of summands is bounded, can enumerate all possible combinations of inputs. This behavior can be simulated using the threshold counting quantifiers introduced in Proposition B.4
Finally, we account for the numerical-stabille adjustment in Eq. 25 The only additional operation introduced by this stabilization is the identification of the maximum score among finite set of floating-pinnt values, which can be expressed in PFO [<] follows:
Proposition B.8. PFO* [<] can identify the maximum score maxi<n Sn.i.
oo). For each E F, let (x)) be (=)o that holds iff the value at position x equals f. Since the set floating-point numbers is finite, we can enumerate all possible maximum values. For each candidate maximum value f. we can construct a PFO? [<] formula @ that holds if and only the scores among positions y
Proof. Let the ordered set of Moating-poin values be F = J1.
less than or equal to f. and least one value equals They can be defined inductively over the total order of IF as follows:
def By x (y)
(36a)
def
(-3y
max (1)) A Fy < : (v),
(36b)
max
xx)
def
-y <x:
V
()px(1)) (1)
By < x 2r (v),
(36c)
fE(co,
max (x)
def
-By x::
V
max (v)
AB < x (y)
(36d)
fE(0o./x.....111
We have now completed the proof of the following theorem: Theorem 3.2. Every transformer can be simulated by PFO" [<].
Proof. By Lemma B.3 the embedding layer can be simulated by PFO* By Proposition B.2 simulation by PFO is closed under all subsequent operations the transformer, except for
summations. By Lemma B.5 Proposition B.6 and Lemma B.7 the summation operations involved in attention computation can also be simulated by PFO*|] Therefore, the entire transformer can be simulated by PF02

---

B.3 From [P] to transformers
In this subsection, we show that every [TL(P) formula can simulated by transformer. The central idea is to encode the truth value of the formula each position dedicated coordinate within the transformer's s hidden state: the value 1 represents T, and 0 represents 1.
The formal definition is as follows.
Definition B.9. LTL formula vb is said be simulated by a function H of type E N+1 EDx(N+1) thee exists coordinate d E {I...., D) such fho every position {l,..., .1....,N+1) and every input string w Σ.
1,
if F
H dn
(37)
0, otherwise.
We introduce one-hot encoding function []. which maps index to column vector of zeros except for single entry equal to 1 at that index. Let denote the all-zero column vector.
We first show that the atomic formulas can be translated into an embedding layer.
Lemma B.10. The atomic formulas na for E can be simulated by embedding layer.
Σ with map g: E {L..... [ J. Since the biases in attention mechanisms are sometimes omitted, we include dedicated bias coordinate d, that always holds a constant value 1. The embedding layer is then defined as follows:
Proof. We assign distinct coordinate d every distinct symbol
1, if d do.
1, if = gwn), H (w) d.n
(38)
0, otherwise.
Coordinates that remain inactive at this stage are initialized to they will later be used store logical formulas introduced in subsequent layers.
Next, we show that the Boolean connectives can be simulated.
Lemma B.11. If th1 and the can be simulated by transformer, then their Boolean combinations can also be simulated by transformer.
Proof. Assume vi and 1/2 are simulated by H(() and H(() respectively. For brevity, write
X = H di. and = ( (W) so x, E [Ix(N+1) are row vectors indexed by positions.
All operations below are applied elementwise.
~ Construct layer that computes, in a fresh coordinate d...
1.
(39)
This can be implemented with an FFN as follows. Select hidden unit d' in the intermediate hidden state {1...., D') and set the first linear transformation to:
FI d.
[d.]'
ifd= d', otherwise,
F [d'].
(40)
The second linear transformation maps d' to the output coordinate d.:
[dd O T
ifd d-, otherwise.
d,
m = 0.
(41)
The attention sublayer is bypassed by setting O @k @ to zero matrices.
25

---

e 11 A 1/2 Compute, in fresh coordinate d^.
ReLU (x+ 1)
(42)
Implement this with single FFN as follows. Select hidden unit d' and set the first linear transformation
[di]]
[2]
if d'. otherwise,
b [d'].
(43)
d.
The second linear transformation connects d' to the output coordinate dx:
[dd
if = da. otherwise,
=== 0.
(44)
0
Again, the attention sublayer is bypassed.
Finally, we address the temporal operator P.
Lemma B.12. If be simulated by transformer, then Pijs can also be simulated by transformer
Proof. We start by introducing the base construction and then discuss two issues arising from fixed-precision arithmetic, together with their corresponding fixes. Assume si is simulated by H(() di."
Base construction. formly to all previous positions m < n where H()) dmm = Specifically, we need the attention scores to be:
We construct an attention mechanism such that each position n attends uni-
H dm 1, if d. = O,
Sn,m
(45)
-uage
where fluge F is a large enough positive floating poating-point number such that exp(-fluge 0. This ensures that positions where va is 1 receive zero attention weight.
This behavior can be implemented by configuring the query and key vectors as follows:
= funge d d1,
Vn, Qan
(46)
otherwise,
and
K ( (w) 1. where the subtraction by applied elementwise. The corresponding attention projection weights are:
(47)
Junge [db]] if = d1, otherwise,
- d,
(48)
1
and
Ok d, = - -[db]"
(49)
where d, denotes the bias coordinate.
Next, we copy the values from H (f) di into an unused coordinate dp via the value projection:
[d,]
if = dp. otherwise.
@ d:
(50)
0
Thus, V becomes:
dy. if dp, H
V d,:
(51)
OT
otherwise.
Let NT denote the number of positions
such that H( H()
1. If N 0. then
On,m 1/NT, giving (++0.55 (W)d.n 1. Otherwise, NT 0, the attention weights are
distributed uniformly over previous positions, all of which satisfy H (w)d, 0, yielding
(f+00.)) (((+0..)(w)dd. 0. Hence, H (C+0.5) simulates P in the ideal case.
26

---

Patch 1: Vanishing Attention Weights When too many previous positions with H(C) i... NT > Nmaxx the resulting attention weights On will underflow to O This causes H(++0.5) W W)de.n = even when Pt true, leading to incorrect behavior.
d1.m 1,
To fix this, we first compute the logical conjunction of dj and dr and store the result in dA via the feedforward sublayer. When H((t) 1, it indicates that the position satisfies v and there exists at least one prior position that also satisfies ts. The number of such positions is bounded by Nmax as starting from the (N + 1)th position, the first attention sublayer will suffer from vanishing attention weights, causing H (e+0.5) dp,n 0.
Next, we construct second layer in which the attention sublayer uniformly attends to positions m where (((+))((waa) (W),,.
This constructs coordinate drr simulating P( A Pv)). Since the number of positions where (((+1) = bounded, this second attention sublayer not subject dr m to vanishing attention weights and reliably computes output.
Note that P( A Pv) evaluates to T when at least two earlier positions satisfy sh. exactly one earlier position satisfies v, then Pe holds but P(ń Pv²) does not. In this case, however, the first attention sublayer (producing dp) already correctly simulates Ptù, since the attention only needs to cover one position. Thus, we take the logical disjunction of dp and dpp, implemented via the feedforward sublayer. The resulting coordinate dy correctly simulates the formula Ptb.
Patch 2: Rounding Errors Fixed-precision arithmetic introduces rounding errors when computing the attention weights Om,m- The fraction I/NT may be exactly representable by imite-precision floating-pons number. Moreover, the iterative summation in Eq. (26) can further accumulate rounding errors. Consequently, the output H (((+00.) may equal value very close 1, when it should be exactly 1. This could lead to incorrect results in subsequent computations.
We address this with thresholding mechanism implemented via a feedforward sublayer. Define round(1) as the set of floating-point numbers that deviates from 1 by at most 8:
r1) {f
E F
If
1 6).
(52)
In standard seatting-poin systems, such as IEEE 754 23 ô is on the order of the machine precision, e.g., approximately 2-24 for single precision and 2 for half precision. Let fmmall be small positive floating-pot -ponnt number such that 1/fsmall also representable, fsmall Fuuil S > We rectify the value at dp using: Let fsmall be a small positive floating point number such that 1/f smmal is also representable, Ssmall value at dp using:
1
and min(round
Tena 1, and min(dou)d(1)) - ssmlll 0. We rectify the
dp. (ReLU (1(6-005) - Samal)
H ((t0.)))
Samall
ReLU
dp.:
(53)
This function outputs 1 if (((+0..) E r1), and if H (e+0.5) dp.n
To implement this with
dp.n
FFN, select two hidden units d' d2 and define:
[dp]
if = di or d dz
Fl
d.:
0
otherwise,
b = - -ssmml Idm
(54)
and
F2 (Ld)' + [d
if de, otherwise,
b
(55)
So far, we have ignored layer normalization. We now show that its presence does not affect the representational power of transformers.
Proposition B.13. If LTL formula i can be simulated by a transformer without layer normal- ization, then it can also be simulated by transformer with layer normalization.
27

---

Proof. Let x be vector. Layer normalization is defined as follows:
LayerNorm V + 7
(56)
where j and the and standard deviation of the elements in x, 7 and / parameters, and e is a small constant for numerical stability.
We introduce, for every logical coordinate d. mirror coordinate and enforce
H (W),.
(57)
d,n
for all sublayers and positions n. This guarantees that for every position n,
Pn and
o
(58)
independently of the particular truth assignment.
With this structure, we can choose the parameters of layer normalization such that the operation becomes the identity function (i.e., has no effect):
o + V 3 Mm
1
(59)
However, the attention sublayer may produce values close 1 but not exactly equal it. Conse- quently, layer normalization can slightly perturb these values away from the intended Boolean values. We denote by (0) and r1und(1) the sets of floating-por respectively, by at most small constant 6, which is again on the order of the machine precision. This deviation harmless, since the subsequent feedforward sublayer rectify the outputs using the following thresholding function: let d, be the coordinate we hope to rectify and choose fı, E F with max(rrund fi f2 < min(rrund(()). Apply:
numbers that deviate from 0 and 1,
f2 fi ((H
(HHO( (w)
fi) ReLU ( (H), -f))
f2))
(60)
To implement this with FFN, select two hidden units di dg and define:
[d,]
if d' or d22,
F d,
b = =- f2[d']l
(61)
0
otherwise,
and
/2-h (L [dlT]) if d d1,
O d,
b
(62)
otherwise,
This yields 1 if (0) dy.n E round and 0 if (()) (())))d (O).
Now, we obtain the following theorem:
Theorem 3.3. Every [T] can be simulated by a transformer.
Proof. By applying structural induction to the formula, using the lemmas Lemma B. Lemma B. and Lemma B.12, we demonstrate that each formula i be simulated by dimension de in the transformer's ' hidden state. Furthermore, by Proposition B.13] we can nullify the effect of layer normalization.
Finally, the classification head only needs to copy the relevant dimension dy as the output.
C Characterizations of [P
In this section, we introduce three alternative formalisms and show that they are equivalent in expressive power to [P]
28

---

C.1 Left-deterministic polynomials
monomial over an alphabet Σ is a language of the form:
Ej ... an 2
(63)
where ......, E Σ and Mo. Ei,.... 2n 3
A monomial is called
left-deterministic if for every & [I.....n). ak Ex-1,
right-deterministic if for every &s E (l,.... n), ak & Ek.
unambiguous is either left-deterministic or right-deterministic.
polynomial is finite union of monomials, and it is said be left-deterministic (resp. right-
deterministic or unambiguous) if it a finite disjoint union of left-deterministic (resp. right- deterministic unambiguous) monomials.
Example:
The language FIRST b is left-deterministic and therefore definable in [T] In contrast, the language LAST E*h right-deterministic but not left-deterministic and thus not recognizable by LT
C.2 R-trivial monoids
A semigroup is set endowed with associative operator, and monoid is semigroup additionally endowed with an identity element. A canonical example is the set Σ", with string concatenation as the associative operation and the empty string the identity element. A monoid M is said to be R-trivial (resp. C-trivial) for all elements 8, E M. the condition sM = tM (respectively, Mss = Mf) implies
now define an equivalence relation on Σ' known as the syntactic congruence. Given a language L C E" two strings s, t Σ" are syntactically equivalent, written s=,t, if and only if:
Vu,v E E" usv L utv E L.
(64)
The equivalence class of string w is denoted as [w]. The quotient monoid / i.e., the set of cquivalence classes under = is called the syntactic monoid of the language L.
C.3 Partially ordered DFAS
PODFA is introduced in 4 Constructing the DFA for a given language is a useful method for assessing whether the language definable in LTL(P).
Example:
It is non-trivial determine whether certain languages be defined in LTL(P). However, becomes clearer when we consider its corresponding automaton. For instance, consider the type of
language DYCK-(1, 1), written (ab)* in regular expression, the Dyck language parentheses with nesting depth limited to 1. The minimal DFA accepting this language is shown below:
This DFA is not partially ordered, as can revisit both y and go. Therefore, DYCK-(1, is not definable in [P).
29

---

Table 2: Relations between logics, formal languages, monoids, and finite automata.
Temporal logic
First-order logic
Formal language
Monoid
Automata
LTL F.S.U U] LTL T.I.P. F) []
FO FO
Star-free
Aperiodic
Counter-free
Unambiguous polynomial
DA
2-PODFA
PFO
Left-deterministic polynomial
R-trivial
PODFA
C.4 Equivalence
We first show that every PODFA can be defined in LTL.P]-
Lemma C.1. Let A = (2,
q1 8) be a PODFA and w E a string of length N. For every q E Q there exists a formula M9> in LTL(P) such that A is in q upon reading wen and only if w, n F 0gz.
Proof. We first construct a formula -z= for each state E Q, such that w, n - 1 1 10gg if and only if A is in q after reading wen-1, i.e., right before reading wn-1- We proceed by induction the partial order z defined over Q-
Base case. out of qz:
The initial as can be defined by ensuring that prior symbol caused transition
-= AE [=)
PT
(65)
Induction step. Assume that for all d' q with d' o g. the formulas Vz have already been constructed. Then, has entered g at some prior point if:
V
V
P(W=g' A ag)-
(66)
o' d'EQ aE(eló(g' a))=
To define vi ma must ensure that has been entered and it is not exited yet:
-6 viea
-P(tce To).
(67)
Once we obtain vi=g. we can define uug> as follows:
6タ V
V
V= A Ta
(68)
d'EQ (E(=)
Finally, a string w is accepted by A it reaches a final state:
V
(69)
PEF
Now we move on to prove the direction from [P to R-trivial monoid. Our proof is inspired by the proof of Proposition 4 in Diekert al. [T
key characterization of R-trriial monoids is given by Brzozowski and Fich
Proposition C.2 (Brzozowski and Fich 44). is R-trivial if and only if there exists an integer K 0 such that for all t E M,, we have (st)* (st)
Thus, we prove the following lemma as preparation:
Lemma C.3. Let ei be a formula in [P] with operator depth at most and K For every v, E', we have
u(st)* sv sv vb and only if u(st)* v==
(70)
30

---

Proof. The case E trivial, so we assume
Let u(st) sv and w' = =( a subset of positions in w. Define N [w]. We consider position N + to point just beyond the end of w.
v. v. As w' is subsequence of align positions in w/ with
We define a pair (n, n²) E (I,...,,. N 1] as legal if
(n = n' = N 1) V (wn Ww A (n' j(st) Vn' |u(st){
(71)
Next, define the middle block of w as:
B {n |u(st)* <n just))*s}}
(72)
legal pair (n, n() is said to k-close
n=n'
n,n' By.
(73)
We now prove the following inductive claim: Let df be a formula in LTL with operator depth at most k, for some 0 I k S K. For every k-close pair (n, n'), ) we have
w, ト and only if w n' J vb.
(74)
We proceed by induction on
Base case. k = O: In this case, vb is Boolean combination of atomic formulas Ta. (n,, n²) being legal pair implies either n = n' = + or Wn = Wa'' so the claim holds trivially.
Induction step. Assume the claim holds for depth &t 1. Let t/ Poi where & has depth k 1. Suppose w, n = 2/1 Then there exists position m < n such that w, m } th. For w', n - eh to hold, we need to identify position m' n' such that w', m' }= th. By the inductive hypothesis, suffices for m' < n' and for (m, m') to be (A: 1)-close. There are two cases:
. Case 1: m Bg. Then we can set m' m. (m,m') is (k 1)-close by definition. We now need to show that m/ < <n..
Subcase 1.1: n, E Bg. Since m & B& and m < n, we can conclude m S [sst)/| Thus, m' = m nt' because n' E B3,
Subcase 1.2: = n'. Then we have m
n==n n'.
Case 2: m Bg. Then, as B&-1 \ Bd covers all symbols in Bg, there exists m' E Ba-1 \ B& such that Wm Wm. Again, (m, m²) is (k - cl-cl since m, m E BB-11 We need to show that m' n':
Subcase 2.1: n, E Bg. Since m' E BB-1 \ Be and E Bx, we have m' n'. Subcase 2.2: n'. Since m' BB-1 \ B, and m E B2, we have m' < < n = n'.
The converse direction, from w nz } 1b w. - follows analogously.
By applying the claim with &s K, n N and N 1, we conclude that w }= if and
only if w/ 1b.
This result then follows straightforwarddy:
Lemma C.4. Every
language has R-trivial syntactic monoid.
Proof. Lemma C.3 suffices to show that every Leeiii-definable language satisfies the characteriza- tion Proposition
We now have all the pieces in place to prove the main theorem.
Theorem 4.1. Let L. C E* be a regular language, M. be its syntactic monoid, and A be the DFA accepting it. The following assertions are equivalent: (1) T. is a lefe-deteriinistic polynomial, (2) M is R-trivial, (3) A is partially ordered, and (4) L is definable by [PL.P]
31

---

Proof. Brzozowski and Fich 4 showed the equivalence of (1), (2), and (3), To complete the picture. it remains incorporate (4), which follows from Lemma C.1 and Lemma C.4
The relationships between various temporal logics, first-order logics, formal languages, monoids, and finite automata are summarized in Tab. We treat the last row (for LTL(P) this paper. For further details on the other classes (LTL[P, and LTL F, S, U), interested readers can refer to McNaughton and Papert 28 and Tesson and Thérien (45]
D Transformer Language Models
The transformer architecture follows the specification in B. with one modification: the final output
layer is replaced by a language modeling head L: FD F P [UNK]] L is defined as follows:
L(H (wen)) softmax (0' ( (w).
a (w)
(75)
where @¹. x)) and bt E F F///+1 are learnable parameters.
We have laid the groundwork that makes the proofs of the following two theorems straightforward. Theorem 5.1. Every transformer LM can be simulated by PFO [<].
Proof. The mapping L consists of a linear layer followed by a softmax. Since both the linear layer and softmax are definable [FO*[<] as shown in BB22 the result follows directly.
Theorem 5.2. Every PODEA LM can be simulated by a transformer LM.
Proof. Let A = (E, 9r F, be a PODFA, and let PA be its induced LM. By Lemma C.1 for each state E Q, there exists [PT formula vi that characterizes the automaton being in state g. Then, by Theorem 3.3 each such formula can be simulated by dedicated dimension in the hidden state transformer.
Since A is deterministic, at each position, there is exactly one coordinate that takes the value 1, while the rest are Therefore, the final prediction head effectively acts lookup table that maps each dimension to the target distribution 7 induced by A. which depends solely on the state A is in.
E Experiments
In this section, we present additional empirical results that align with our theoretical findings.
E.1
Language recognition
We supplement 6. with detailed descriptions of the experimental setup, tasks, and results.
E.1.1
Experimental setup
Our experimental setup follows Deletang al. [10). Butoi al. [6]. We transformer with soft attention, strict future masking, L = 5 layers, model size = 64, and NoPE. Training strings of length up to 40, while test strings range from length 41 to 500. The model is trained for 1,000,000 steps with a batch size of 128. For evaluation, we generate 512 samples per test length. For comparison, also train long short-term memory (LSTM) 20 with hidden size of 256. Each experiment is run with 5 different random seeds and 3 learning rates (1 x 10 10-4, x 10-4,5 5,5 x 10 10-4).
All experiments were conducted on single GPU with 24 GB of memory, each taking approximately one hour to complete. Our code is adapted from https:t/p//.. /tt:://gttttt com/ google e- deepeeeiii nd/ neural networks chwmsky hierarchy licensed under the Apache License, Version 2.0.
E.1.2 Languages
We consider five language classes, arranged in a strict inclusion hierarchy class proper subset of the one preceding it. For each class, select one more representative languages.
32

---

Counter languages. Counter languages are languages that can be recognized by counter machines finite-state automata augmented by a number of counters [ 30]. In our experiments, we choose one of the simplest counter languages: CNT a a"b", the set of strings consisting of an arbitrary number of as followed by an equal number of bs.
Regular languages. A defining characteristic of non-star-free regular languages is modular count- ing. For instance, PARITY a a"aaa" bab)""""""""" the language of binary strings with even number of bs, is one of the simplest instances of this class.
Star-free languages. Languages that definable in F,S, UJ. We focus three common examples that are not definable [P, F):
DYCK-(1, 2): (b)a")*b)*, the Dyck language (well-balanced parentheses) with 1 pair of parenthe- ses, limited to depth 2.
DYCK-(I, 1): (ab)", the Dyck language with pair of parentheses, limited to depth 1. This is also canonical example of strictly locally testable languages, where string membership depends only on adjacent symbol blocks (28).
LT-2: E' ab with |Σ| 2, the set of strings containing ab substring (symbols appearing contiguously). This is an example of a locally testable language [28].
Unambiguous polynomials. Languages that are definable in LTL.P.P FJ. We are interested in those not definable LTL(P)) i.e., right-deterministic but left-deterministic polynomials. We select two such languages:
RDP-1: (E (bo)) bi))a, simple right-deterministic monomial.
ba,
LAST: b, the language of strings ending with io. It can be seen as the simplest representative of the class.
Left-deterministic polynomials. We now consider languages that definable in LTL[P]. select- ing five examples that serve as contrasts to the previously discussed ones.:
PT-2: E'aE'b" with |Σ| 2, the language of strings that contain ab subsequence. Lan- guages of this type are known as piecewise testable languages [40].
LT-1: E*aE*, the set of strings that contain locally testable and piecewise testable languages.
substring. This is the simplest case in both
LDP-1: (E bo)) a (bi))*, " left-deterministic monomial symmetrical to RDP-1.
Although LDP-1 and RDP-1 symmetrical, the former can be recognized by DFA with only 2 states, whereas the latter requires (see Fig. 3). For a fair comparison, we also include LDP-2 (E)) \ (ai, =bo)==a))lllaa
fay, bı 1 (2(E) {b2) which also requires 3 states.
FIRST: bΣ* the set of strings beginning with
Sample generation. For each language, we construct both positive and negative samples. Some examples are constructed adversarially increase the difficulty of the classification task.:
CNT: Negative samples contain one fewer a or
PARITY: Negative samples contain an odd number of bs.
DYCK-(1, 2), DYCK-(1, 1): One symbol in positive sample is flipped. Since these languages require even-length strings, we only use even-length inputs.
LT-2 and LT-1: Negative samples omit al (resp. a) as substring, Positive samples are constrained to include exactly one such occurrence.
RDP-1, LDP-1, and LDP-2: Negative samples contain a single incorrect symbol.
LAST and FIRST: Negative samples do not end begin with b, respectively.
PT-2: Negative samples lack the subsequence.
33

---

E bo)
E (0),
bi
a
q0
E (a1,
81
Σ b1)
E (12,
bo
q
x {ba}
82
42
(a,
(b) LDP-1
x (b2)
(a) RDP-1
(c) LDP-2
Figure 3: DFAs for the given languages. Nodes represent states, and arrows represent transitions. The imitial state is indicated by an incoming arrow with no source node, and accepting (final) states are shown with double circles.
E.1.3 Results
We compute classification accuracy and report both the maximum and mean values across all runs in Tab. [1. The LSTM achieves perfect accuracy on all tasks, consistent with previous work showing that LSTMs can recognize regular languages [29] and implement counting mechanisms 48 This confirms that the tasks are learnable given the available training data.
Counter languages. While several papers have shown that counting quantifiers can be simulated by Subitrary-rrecision 19 49 or pr-pciiciioon transformers [31], our results indicate that a fixed peeeciioiiionn transformer cannot recognize CNT. The model achieves maximum accuracy of only 83.3%. This finding contrasts with Bhattamishra et al. [3], who report that transformers can recognize a a"b"c". The discrepancy may stem from our evaluation on longer input lengths.
Regular languages. In line with Hahn 17 we find that the transformer completely fails to learn the non-star-free regular language PARITY, reaching most 52.1% accuracy. Although Chiang and Cholak [8] design a transformer with customized positional encodings capable of recognizing PARITY, these encodings are always representable under fixed precision, and the resulting architecture is not learnable under standard training conditions.
Star-free languages. Yang al. [50] show that fixed-precision transformers with UHA recognize exactly the star-free languages. Similarly, Yao et al. [51] demonstrate that transformers with posi- tional encodings of the form n n/N- W/-which
not always representable under fixed precision recognize bounded Dyck languages, a family of star-free languages. In contrast, we prove that trans- formers with soft attention and NoPE cannot recognize even the simplest bounded Dyck languages (DYCK-(1, 2) and DYCK-(1, 1)), nor the locally testable language LT-2. These results are corroborated by our experiments: the transformer fails to learn any of these three languages. The best performance is on DYCK-(1, 1), with a maximum accuracy of 87.7% which still indicates poor generalization, especially considering the simplicity of the task.
Unambiguous polynomials. As predicted by our theory, the transformer fails to learn unambiguous polynomials that are not left-deterministicc The model achieves maximum accuracy of 90.0% RDP-1 and 64.8% on LAST.
Left-deterministic polynomials. Although the transformer cannot learn I.T-2, it achieves perfect accuracy on both PT-2 and LT-1. In contrast to the poor performance on RDP-1 and LAST, the model learns their symmetrical counterparts (LDP-1, LDP-2, and FIRST) with 100% accuracy. Notably, Chiang and Cholak [8] construct unmasked transformer encoders capable of recognizing FIRST, but report difficulty in training such models in practice. Our results show that masked transformer decoders can learn FIRST easily and consistently, suggesting that masking may offer a more robust source of positional information than positional encodings.
Summary The empirical results align fully with our theoretical predictions. Importantly, we use single-precision (32-bit) floating-poit numbers, and the string lengths never exceed the maximum
34

---

Table 3: Language modeling experiments. Maximum and mean per-token accuracies (#: standard deviation) are reported. Exact 100.0% are highlighted in bold.
Language
Max (%)
Mean (%)
RDP-1
98.3
73.6 + 12.5
LDP-1
100.0
98.6 + 2.5
LDP-2
100.0
98.9 + 3.7
attention span of the transformer: That is, attention can uniformly cover all prior positions without numerical underflow or overflow. Yet, despite these favorable conditions, the transformer exhibits no expressive power beyond what is predicted by our formal characterization.
E.2 Language modeling
The DFAs corresponding to the languages used in our experiments are shown in Fig. 3 and their maximum and mean per-token accuracies are reported Tab. 3 As predicted, the transformer language model learns left-deterministic polynomials perfectly but fails on the right-deterministic polynomial.
Additional results
In this section, we present further theoretical results of potential interest.
F.1 Hard attention
Average hard attention (AHA) uniformly attends to positions m < n with the maximum score Sa,m- Formally, Eq. (24) is modified follows:
1 1 n.m = maxien Sn.
O2n.m
Ej 1 [ maxica Sn,i)
(76)
where 1 {-} is the indicator function.
We now show that AHA also definable [F))
Theorem F.1. Every transformer with AHA can be simulated by [<)
Proof. By Proposition
B. PFO [<] can identify the maximum score max Sn,5. The denom-
(76) is a sum of non nog-nieative terms and can therefore be simulated by PFO*[<] via Lemma B.5 As with the soft-attention case in Eq. (24), resulting attention weights may vanish when the number of positions exceeds the model's ss bounded attention span; hence, Lemma B. applies here as well. The remaining steps of the construction follow identically to those in B.2
inator in Eq.
The other direction is straightforward.
Theorem F.2. Every [ormull can be simulated by transformer with AHA.
Proof. Recall that the attention mechanism we constructed in the proof Lemma B. uniformly attends to all positions with the highest score S..m 0, effectively making equivalent to AHA. Therefore, [TL formulas can also be simulated by transformers with AHA.
Now, we turn UHA, another widely studied attention mechanism where each position attends to single position m < n with the highest S,,m- In the case of ties, the rightmost position is selected. Yang et al. [50] prove that transformers with UHA are as expressive F.
Combining the results from above, we have:
Corollary F.3. Trunsformers with AHA are as expressive as those with soft attention, which are strictly less expressive than those with UHA.
35

---

Proof. The equality AHA = soft attention follows directly from Theorems F.1 and
The strict inequality soft attention < UHA follows directly from the fact that L.T. is strictly less expressive than [T, F.S.U)
F.2 Non-strict future masking
Most commonly used transformers adopt non-strict future-masken soft attention, where each position allowed to attend to itself. In this case, Eq. (24) and Eq. (26 become:
def exp(S
Cn
Σ Eisn exp(Sn.i)
(77)
and
A A(H(w)): ).. def Σ an,m V v.
(78)
respectively.
This modification, however, limits the expressiveness of the model.
Theorem F.4. Transformers with non-strict future masking strictly less expressive than those with strict future masking.
Proof. Since we have already established that transformers with striet masking are as expressive as PFO |<] it suffices show that any transformer with non-strict masking is strictly less expressive than [=]
We begin by observing that transformers with non-strict masking can be simulated by PFO [<]. The required modification to Proposition B.4 involves including the current position in the threshold counting quantifiers:
L''y و 2: (0)) (3 < r: o(v)) v v((x).
(79a)
3 $ x: x(v) de (3 < x: < v ((32ly < x: :(v)) ^ A(z)),
(79b)
Next, we construct language that definable in PFO [<] but cannot be recognized by transformer with non-strict masking. Consider the language bb which can be defined in PFO [<] by the following sentence:
3r : (Tz(z) A (3 x: Te (v)) A ^-Ey < x: :m,(y))
(80)
On the other hand, given any transformer H with non-strict masking, and for any string bbE*. we have:
H
w).1 for all layers [l.....,] L}
(81)
This is because, under non-strict masking, position n attends all positions n. including itself. When the prefix consists entirely of identical symbols, each attention pattern and subsequent compu- tation depend solely on the identical sequence of embeddings, resulting identical representations each position. However, differentiating the two leading bs is essential for recognizing bbΣ* as the corresponding DFA will enter different state upon reading the first symbol b.
Empirically, we confirm this limitation by training transformers-one with strict masking and one with non-strict masking-on the language bbΣ*. The results are consistent with our theoretical prediction:
The strictly masked transformer achieves 100.0% maximum accuracy and 96.3% + 5.8% average accuracy.
The non-strictly masked variant reaches only 95.8% maximum accuracy and 74.4% 8.2% average accuracy.
36

---

F.3 Positional encodings
Positional encodings are introduced in Vaswani et al. [46] to inject information about the positions into the transformer. In general, there two categories of positional encodings:
A Asslute positional encoding: This is function p: (1...., N+1] + RD. is typically injected
into the input layer by modifying Eq. (2T) follows:
e(w,)) + p(n), n ,I,...,, N -+N1 +
(82)
Relative positional encoding: This a function p: fI...., 11 x (1...., . - FD.
is typically injected into the attention sublayer by modifying Eq. 23
as follows (39 21:
def Qun K + +Q... p(n,
(83)
VD
In formal logic, a numerical predicate is a predicate that depends solely on the positions in a string, not the symbols in those positions. Numerical predicates that depend on one (resp. two) position(s) are referred as unary (resp. binary) numerical predicates. For instance, the relation < is binary numerical predicate.
We now show that all absolute (resp. relative) positional encodings be simulated by unary (resp. binary) numerical predicates.
Theorem F.5. Let be an absolute (resp. relative) positional encoding and L C E be a regular language. There exists a collection of unary (resp. binary) numerical predicates P such that the following assertions are equivalent:
1. can be recognized by a transformer with positional encoding p-
definable by PFO²|<, (4, PI, i.e., PFO [<] extended with the numerical predicates P.
Proof. Positional encodings, under fixed precision, have finite image. Therefore, for every dimen- sion d 1,.... D and every Moating-point number F, define numerical predicate such that:
r(n)= T if p(n)a= =
(84)
or
(n,m)=T if p(n,m)a= = S.
(85)
The reverse direction and precise logical characterization of commonly used positional encodings, e.g., sinusoidal and rotary [43], are left for future work.
G Related work
The expressivity of transformers in the context of formal methods has been extensively studied in recent literature [42). Various transformer variants have been explored, and different assumptions have been made to enhance the expressivity of transformers.
Chain of thought (CoT). CoT reasoning, which involves generating intermediate steps before arriving at a final answer, has become a popular approach. Pérez et al. [38 demonstrated that transformer with both an encoder and decoder, when allowed a polynomial number intermediate computation steps, is Turing complete. Similarly, Merrill and Sabharwal [33], Nowak et al. [35). Li al. 27 show that the expressivity transformers can improved with various forms CoT reasoning. In this work, along with many others, we do not allow intermediate steps, which restricts expressivity. In such a case, Hao et (18), Merrill et (34), Merrill and Sabharwal 32 Chiang et al. [9), Yang and Chiang 44 have established various upper bounds on expressivity.
37

---

Non-fixed precision. If a transformer is allowed arbitrary precision, or if the precision increases with imput length. Bhattamishra al. [3] proved that it more expressive than simplified and stateless counter machines. Additionally, Chiang et al. [9] and Yang and Chiang [9] showed that transformer with such precision can recognize any language definable by temporal counting logic. In contrast, our work focuses on the scenario where precision is fixed, which imposes more limitations on expressivity.
Bespoke positional encodings. Some prior studies have employed bespoke positional encodings, many of which cannot be represented under fixed precision, to overcome certain limitations of transformers. For cxample, Chiang and Cholak
[8] used the encoding n/N to enable transformers to recognize parity, and Barcelo et al. [2] demonstrated that transformers with a specially designed positional encoding can achieve lower bound of FO <<] with unary numerical predicates. In contrast, our constructions and proof' do not rely on any form positional encoding.
Hard attention. Two forms of hard attention have been explored in the literature. Yang et al. [50] showed that masked fixed- exed-precision transformers with UHA and NoPE recognize exactly the star-free languages. Barcelo et al. [2] established similar lower bound for transformers with AHA and certain positional encodings. Prior to our work, it was unclear, under fixed precision, whether these two hard attention mechanisms soft attention. Surprisingly, we find that UHA is strietly more expressive than soft attention, while AHA is expressive as soft attention.
more less expressive than, comparable to, the standard
H
Limitations
The primary limitation of this work lies in the omission of positional encodings. While we briefly discuss their role as numerical predicates, the exact numerical predicates simulated by commonly used positional encodings remain unknown. We hope to explore this in future work. Nevertheless, we believe is important first understand the expressivity of barebones transformer architecture, as this forms the foundation for systematically incorporating various forms of positional encoding later on.
Another inintation-paaticuulll from an empirical perspective-is is our stringent evaluation criteria for transformer performance. While certain levels of accuracy might be considered successful in empirical studies, we require perfect accuracy. This is motivated by a formal perspective: model (e.g., an automaton or logical formula) either recognizes a language perfection is regarded as failure, suggesting that some form of approximation or shortcut has been employed. We interpret our results as identifying a class of tasks that transformers have the full capacity to solve.
does not; anything short of
38

---

NeurIPS Paper Checklist
The checklist is designed to encourage best practices for responsible machine learning research, addressing issues of reproducibility, transparency, research ethics, and societal impact. Do not remove the checklist: The papers not including the checklist will be desk rejected. The checklist should follow the references and follow the (optional) supplemental material. The checklist does NOT count towards the page limit.
Please read the checklist guidelines carefully for information on how answer these questions. For each question in the checklist:
You should answer [Yes], [No], or [NA].
[NA] means either that the question is Not Applicable for that particular paper or the relevant information Not Available.
Please provide short (1-2 sentence) justification right after your answer (even for NA).
The checklist answers are an integral part of your paper submission. They are visible to the reviewers, area chairs, senior area chairs, and ethics reviewers. You will be asked to also include (after eventual revisions) with the final version of your paper, and its final version will published with the paper.
The reviewers of your paper will be asked use the checklist as one of the factors their evaluation. While "[Yes] is generally preferable to "[No]" ", it is perfectly acceptable to answer "[No] provided proper justification is given (e.g., "error bars are not reported because it would be too computationally expensive" or "we were unable to find the license for the dataset we used"). In general, answering binary way, we
"[No] or "[NA]" is not grounds for rejection. While the questions are phrased acknowledge that the true answer is often more nuanced, please just use your best judgment and write justification to elaborate. All supporting evidence can appear either in the main paper or the supplemental material, provided in appendix. If you answer [Yes] to a question, in the justification please point to the section(s) where related material for the question can be found.
IMPORTANT, please:
Delete this instruction block, but keep the section heading "NeurIPS Paper Checklist",
Keep the checklist subsection headings, questions/answers and guidelines below.
Do not modify the questions and only use the provided macros for your answers.
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: Claims made in abstract and I accurately reflect the paper's contributions and scope.
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. 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 other settings.
is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper.
Limitations
Question: Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
39

---

Justification: SHI
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't t acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set assumptions and complete (and correct) proof?
Answer: [Yes]
Justification:
Assumptions: $5 B.I 3.1 and
proofs: $$ B.2 B.3
D and
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 either appear in the main paper the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proof' provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed reproduce the main experi- mental 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)?
Question:
Answer: [Yes]
Justification: A description of the experimental setup and data generation is provided in $$ B.I.1 and
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 important, regardless of whether the code and data are provided or not.
40

---

If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending the contribution, reproducibility can be accomplished in various ways. For example, the contribution is a novel architecture, deseribing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way 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 large language model), releasing of model checkpoint, other means that appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submissions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution primarily new algorithm, the paper should make clear how reproduce that algorithm.
(b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) If 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 a way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, 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 instructions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification:
Code included in the supplementary material.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (bttps://nlps.cc/pulu for more details.
qui des SCt./Seeeeeiiiee s wwwssooooiiiooo
While we encourage the release 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 a new open-source benchmark).
The instructions should contain the exact command and environment needed to run reproduce the results. See the NeurIPS code and data submission guidelines
guide gjides//odes Suboii ssnnoPoo olicy) 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. If only a 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 is permitted.
Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyperparameters, how they were chosen, type of optimizer, etc.) necessary understand the results?
Answer: [Yes]
Justification:
$ and 6
Guidelines:
41

---

The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of 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, or as supplemental material.
7. Experiment statistical significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [Yes]
Justification:
Standard deviations reported in Tabs. and and
F.2
Guidelines:
The answer NA means that the paper does include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confidence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper. The factors of variability that the error bars are capturing should be clearly stated (for exam- ple, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to 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 the standard error of the mean.
It is OK to report I-sigma error bars, but one should state 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 figures symmetric error bars that would yield results that are out of 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
Question: For each experiment, does the paper provide sufficient information on the computer re- sources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Answer: [Yes]
Justification:
Computer resources are reported in SE.II1
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, 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 the paper (e.g., preliminary or failed experiments that didn't 't make it into the paper).
Code of ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurIPS Code of Ethies htttss::/reurr.ssscc//p/p
de ines
Answer: [Yes]
Justification:
This research conform with the NeurIPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics. the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
42

---

The answer NA means that the paper poses no such risks. The authors should make sure to preserve anonymity (e.g., if there is special consideration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification:
We foresee societal impact of this work.
Guidelines:
The answer NA means that there is no societal impact the work performed. If the authors answer NA No, they should explain why their work has societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious unintended uses (e.g., dis- information, generating fake profiles, surveillance), fairness considerations (e.g.. deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point out. For example, is legitimate to point out that an improvement the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, not needed point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML).
Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data or models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
The paper poses no such risks
Guidelines:
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 access the model 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 take this into account and make a best faith effort.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: Our code is adapted from Deletang et al. 100 The authors are properly credited and the license and terms are explicitly mentioned and properly respected in F.1.1
Guidelines:
43

---

The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL..
The name of the license (e.g., CC-BY 4.0) should included for each asset.
For scraped data from particular source (e.g.. website), the copyright and terms of service of that source should provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, seaperswithcom com/ datasets has curated licenses for some datasets. Their licensing guide help determine the license of a dataset.
For existing datasets that are re- re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
this information is not available online, the authors are encouraged to reach out to the asset's creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification:
This paper does not introduce new assets.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details the dataset/code/mmodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used. At submission time, remember to anonymize your assets (if applicable). You 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 sereenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification:
This research does not involve crowdsourcing.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribution of the paper involves human subjects, then as much detail as possible should be included the main paper. According to the NeurIPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper deseribe 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 the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
This research does not involve human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. you obtained IRB approval, you should clearly state this in the paper.
44

---

for We recognize that the procedures for this may vary sigmificantly between institutions and locations, and expect authors adhere to the NeurIPS Code of Ethies and the guidelines for their institution. * For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Question: Does the paper describe the usage of LLMs if it an important, original, or non-standard component the core methods in this research? Note that the LLM used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, originality of the research, declaration is not required.
Answer: [NA]
Justification: This research does not involve LLMss.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs any important, original, non-standard components. Please refer to our I.LM policy (https: http///euripssee /ptpcccccc/ooooeerrreee///////// what should or should not be described.
45


Reviews:
[{"review_id": "PZZM8y9APq", "reviewer": "Reviewer_4BQ7", "summary": "This paper theoretically analyzes the expressive power of fixed-precision transformers with strict future masking (i.e., every position attends to the left, not to itself), and shows that the class of languages captured by such transformers is precisely the temporal logic LTL[past], for both average hard attention and soft attention.\n\nAs part of the argument, the authors also show a (novel, I think) equivalence between LTL[past] and a 2-variable variant of first order (FO) logic.", "questions": "Nothing in particular, besides what was raised above in the comments.", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 2, "originality": 3, "strengths_and_weaknesses": "The paper has many clear **strengths**, including:\n\n* Technically strong!\n\n* Clear articulation of all concepts and proof ideas; detailed background and proofs in the appendix.\n\n* Novel exact characterization of the considered formal model of transformers, extending the previous characterization of a similar formal model but one that had used *unique* hard attention (which was farther away from practice).\n\n* Length generalization experiments with specific languages, supporting findings.\n\n* Neat idea for simulating the \"past\" operator despite the \"finite attention span\" limitation of soft attention (and also average hard attention?) when using finite-precision.\n\n\nThere are, nonetheless, some aspects that **can use improvement**:\n\n* While I agree with the authors' claim that this work is a step closer to the formalization of real-world transformers (especially compared to prior work analyzing unique hard attention), the current introduction wording has the feel that the formal model used here has closed that gap. But, as noted next, this doesn't quite appear to be the case, and I would thus suggest softening / refining the wording along these lines.\n\n* To give some examples of the above, *strict masking* is not used in practice (though perhaps it should be, given your findings? it does appear odd for a position to not pay attention to itself, especially when operating over natural language, e.g., for coreference resolution), *position encodings* are always used (whereas the authors discuss $bb \\Sigma^*$ not being recognizable without strict masking -- which is true only without position encodings), *layer normalization* discussion is partial (please see below), I don't recall a mention of residual stream, and perhaps more.\n\n* Other reasons to push back against this formal model as the final word on the subject or being the closest to real-world transformers: (1) The finding that, under this model, unique hard attention is more powerful than average or soft attention is counter-intuitive; similarly, that average-hard and soft attention are essentially identical here is also counter-intuitive. (2) While having a fixed set of trained parameters makes complete sense, I don't particularly see an issue with expecting that when solving larger instances of a problem, the model could have access to higher precision arithmetic, or something that scales with input size.\n\n* On that last note, related to the presented length generalization **experiments**, it is possible -- in principle -- that your trained transformer models for the harder languages do, in fact, generalize, it's just that your trained models need to run on larger hardware / higher precision chips in order to solve inputs of size 500. This is a matter of implementation and experimentation, not really answering the question of whether the transformer accurately learned to solve the task.\n\n* In fact, if you take any classic textbook algorithm and implement it on a fixed precision hardware, it will likely fail to solve the problem for large-enough input sizes because of numerical overflow/underflow. Should we then conclude that the textbook algorithm (which has the \"correct\" finite description) is not solving the problem?\n\n* Treatment of layer normalization: it's mentioned somewhat in passing in Prop B.12 in the appendix. There is a \"proof\" but I couldn't quite follow how exactly it works, why the variance is identical across dimensions, etc. It was also unclear how LN comes into picture in the other direction, i.e., when simulating a transformer with LN (vs. without LN) using PFO^2[<]. I'm assuming the fixed-precision assumption let's this work out. Please clarify.\n\n===\n\n**In summary**, I like the paper and I would like to see it published. At the same time, I would appreciate it if the authors could give more thought to their quick opening argument that finite-precision is the \"right\" formal model of transformers. If my arguments above influence their view (especially the one about never being able to experimentally verify arbitrary \"length generalization\" of even a textbook algorithm we know to be correct due to numerical overflow/underflow issues), I would appreciate adjusting the positioning of the work to account for this. The paper is technically a solid contribution, it's just the positioning that I feel should be refined.", "was_revised": true, "final_justification": "I am happy to see the paper accepted, especially after the authors' detailed, thoughtful reply, and their willingness to adjust the wording and expand upon certain aspects to make the paper's content and positioning more clear. I look forward to reading the revised version once published!", "rebuttal": "We thank the reviewer for their thoughtful and constructive feedback, and for their positive assessment of the technical contributions, clarity of exposition, and the paper’s overall value. We are particularly grateful for the recognition of our novel characterization, the simulation of the past operator, and the experimental validation through length generalization. Below, we respond point-by-point to the reviewer’s comments and suggestions.\n\n---\n\n> *While I agree with the authors' claim that this work is a step closer to the formalization of real-world transformers..., the current introduction wording has the feel that the formal model used here has closed that gap.*\n\nWe agree that there is still a gap between our formal model and real-world systems. That’s why we describe our model as an idealization. We thank the reviewer for pointing out that our wording may be misleading. In the final version, we will soften the language to clarify this point.\n\n---\n\n> *It does appear odd for a position to not pay attention to itself... Position encodings are always used... layer normalization discussion is partial... no mention of residual stream...*\n\nThese are valuable observations. We respond to each below:\n\n- **Strict masking**: Due to the residual connections, the current token still has access to itself through the residual stream. This offers intuition for why strict masking does not remove information.\n\n- **Positional encoding**: Together with prior work, we establish that positional encodings largely play the role of numerical predicates in formal logic. Nevertheless, we agree this connection is not sufficient on its own, and we hope to investigate more precisely what numerical predicates commonly used positional encodings correspond to in future work.\n\n- **Residual connection**: Residual connections are present in our model and used critically in the proofs in Appendix B.3. They ensure that earlier logical dimensions are preserved across layers, which is key to simulating complex formulas. We will make this clearer in the main text.\n\n- **Layer normalization**: We now provide a more concrete example to support Proposition B.12:\n\n  Suppose we have two dimensions, encoding $\\\\pi_a$, $\\\\pi_b$, and $\\\\mathbf{P} \\\\pi_a$, respectively. Inputting the string \"ab\" produces:\n  $$\\\\begin{matrix} 1 & 0 \\\\\\\\ 0 & 1 \\\\\\\\ 0 & 1 \\\\end{matrix}$$\n  \n  These column vectors have different means and variances, and applying LN would distort their encoding. To neutralize this, we **introduce a mirror dimension** for each original dimension, giving:\n  $$\\\\begin{matrix} 1 & 0 \\\\\\\\ 0 & 1 \\\\\\\\ 0 & 1 \\\\\\\\ 0 & 1 \\\\\\\\ 1 & 0 \\\\\\\\ 1 & 0 \\\\end{matrix}$$\n  where the last three rows are mirror dimensions. Now, each position (column vector) has mean $0.5$ and variance $0.25$. By setting $\\gamma = \\\\sqrt{0.25 + \\\\epsilon}$ and $\\\\beta = 0.5$, we cancel out LN entirely. This trick ensures that LN is an identity function and has no effect on the content. \n\n  In the reverse direction, simulating transformers using logic, fixed precision makes the simulation of any **positionwise deterministic function** straightforward: we simply enumerate all possible inputs and outputs. Both layer normalization and residual connections fall under this class.\n\n---\n\n> *UHA more powerful than soft or average attention is counter-intuitive; average-hard and soft attention being essentially identical is also counter-intuitive.*\n\nWe agree this may seem counterintuitive. However, there is empirical evidence supporting these theoretical findings:\n\n- **On UHA**, Selim et al. (2025) show that it is specifically **rightmost UHA** that is more expressive than soft attention. This aligns with prior empirical efforts to inject recency bias, where the rightmost token is preferred in case of tie scores, using special attention mechanisms (Alon et al., 2024) or relative positional encodings (Su et al., 2021).\n\n- **On AHA vs. SA**, our preliminary experiments show that if a transformer is trained with SA and annealing, and then tested with AHA, performance often matches or exceeds the performance of models trained and tested with SA. This supports the theoretical equivalence between SA and AHA.\n\n---\n\n> *... it is possible -- in principle -- that your trained transformer models... need to run on larger hardware / higher precision chips in order to solve inputs of size 500.*\n\n> *In fact, if you take any classic textbook algorithm and implement it on a fixed-precision hardware, it will likely fail... Should we then conclude that the textbook algorithm... is not solving the problem?*\n\nOur theory shows that for any language definable in $\\\\textbf{PFO}^2[<]$, we can construct a transformer (textbook algorithm) that computes the correct classification for **every input length**, under fixed precision. In contrast, no such transformer exists for languages outside this class. Our work thus identifies an exact boundary of what **can be reliably encoded and generalized** within a fixed‑precision transformer, distinct from cases where success depends on increasing precision.\n\nThat said, we fully acknowledge that different implementations, precision, or hardware architectures may yield different empirical outcomes. Our results do not preclude the possibility that one could train a transformer to generalize up to length 500. Nevertheless, we find it encouraging that models trained under the standard framework and hyperparameters from Deletang et al. (2023) and Butoi et al. (2025), without any special tuning, task-specific adaptation, or architectural modifications, exhibit generalization behavior that aligns closely with our theoretical predictions.\n\n> *I don't particularly see an issue with ... the model could have access to higher precision arithmetic, or something that scales with input size.*\n\nModels are trained and deployed under fixed precision, and it is infeasible in practice to dynamically increase numerical precision at inference time when longer inputs are encountered. That said, we agree that logarithmic precision or any growing precision is a worthwhile setting to explore. It offers insights into what transformers can recognize when input lengths are constrained, which is often the case in real-world applications. However, interpreting log-precision results in this way implicitly relies on **uniformity assumptions** that a single set of parameters should work for all input lengths below a certain bound. To our knowledge, these questions remain under-explored and represent an exciting direction for future research.\n\n\n---\n\nWe thank the reviewer again for the helpful suggestions and positive evaluation. We will revise the introduction, clarify our assumptions, expand the discussion on residuals and normalization, and incorporate further context to strengthen the positioning of our results. We appreciate the opportunity to improve the paper and clarify its contributions, and we are encouraged by the reviewer’s support for publication.\n\n---\n\n## References\n\n- Selim et al. (2025). *Unique Hard Attention: A Tale of Two Sides.*\n- Alon et al. (2024). *Scaling Stick-Breaking Attention: An Efficient Implementation and In-depth Study.*\n- Su et al. (2021). *RoFormer: Enhanced Transformer with Rotary Position Embedding.*\n- Deletang et al. (2023). *Neural Networks and the Chomsky Hierarchy.*\n- Butoi et al. (2025). *Training Neural Networks as Recognizers of Formal Languages.*"}, {"review_id": "Sc3PvmrKGv", "reviewer": "Reviewer_d6kd", "summary": "This paper investigates the expressive power of real-world transformer models through the lens of formal languages. In particular, it characterizes the capabilities of transformers with fixed numerical precision, soft attention, and strict future masking. The authors prove that such transformers are equivalent in expressivity to a fragment of linear temporal logic and a fragment of first-order logic. These characterizations are then used to construct separation examples that highlight the limitations of transformer models. The paper also presents empirical evidence by training transformers to verify these separations.", "questions": "- Do the separation results demonstrated in the experiments also hold for transformers with positional encoding?", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n+ The paper is clearly written, with well-structured and accessible proofs.\n+ It closes the gap in the literature by providing a precise characterization of practical transformer models.\n+ The empirical evaluation convincingly demonstrates the expressive boundaries of such models, offering valuable insights into their capabilities.\n\nWeaknesses:\n- The treatment of transformers with positional encoding is limited and lacks a thorough theoretical analysis.\n- The study does not consider transformers equipped with Chain-of-Thought (CoT) reasoning, which limits its relevance to state-of-the-art models.", "was_revised": true, "final_justification": "My concerns have been largely addressed. I will maintain my score.", "rebuttal": "We thank the reviewer for their thoughtful and encouraging feedback. We are especially grateful for the recognition of the clarity of our writing, the strength of our theoretical characterization, and the value of the empirical results.\n\nWe agree that both positional encodings and CoT reasoning are important and exciting directions for future work. We believe that our results on barebones transformer models provide a solid foundation for pursuing these lines of research.\n\nRegarding the reviewer's question about positional encodings:\nYes, the separation results do hold even when positional encodings are included. In our preliminary experiments, we explored both absolute (sinusoidal) and relative (rotary) positional encodings. We found that neither variant improved performance on the languages outside $\\\\textbf{PFO}^2[<]$."}, {"review_id": "ETp2AEwwd8", "reviewer": "Reviewer_LVye", "summary": "This paper makes the following contributions: \n1. An exact theoretical characterization of the expressive power of fixed-precision soft-attention transformers as LTL[past], which is obtained by showing two directions:\n\t1. PFO2[<] as an upper bound\n\t2. LTL[past] as a lower bound\n2. Theoretical results showing that LTL[past] is a natural class via several equivalent definitions in terms of automata, logic, etc.\n3. Experiments suggesting transformers can length generalize correctly exactly on those languages that are definable in LTL[past]", "questions": "The PFO2 upper bound proof makes sense at a high level: in fixed precision, summations become simple to simulate compared to log precision. But I'd like some more detail on the following:\n\n> Therefore, it reduces to a sum of a bounded number of terms, which can also be simulated by PFO2 [<] (Lemma B.7).\n\nIf the terms that were being summed were always the same, I'd immediately accept this argument. But in fact, there is a bounded sublist of an unbounded list of terms that needs to be summed. Does this change anything about the argument? The proof needs more detail to clarify this.\n\n\"Uniformly attend to positions m < n where [...]\" State that you can do this because of fixed precision: i.e., if you set the temperature high enough, everything that violates a key/query match condition will go to 0.", "limitations": "As alluded to in weaknesses, the authors should better acknowledge that fixed-precision is one, though not the only, formal model of transformers. There are arguments for other models like log precision.", "rating": 5, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 4, "originality": 3, "strengths_and_weaknesses": "## Strengths\n\n1. Novel theoretical result on expressivity of fixed-precision soft attention that significantly extends past work. In particular, this paper is able to obtain an exact characterization for this model of transformers that is itself a fairly natural class (as evidenced by many converging definitions of this class).\n2. Clever trick and observation used to show that since can be simulated with fixed precision.\n3. Paper is generally well written and presented, and would be of clear interest to the research community working on the expressive power of transformers and other architectures.\n\n## Weaknesses\n\n### On Fixed Precision\n\nIn the title and elsewhere, this paper seems to imply its results hold for all transformer language models, while in reality it characterizes one specific formal model of transformers (fixed-precision, soft-attention transformers). This is not the only reasonable formal model (e.g., log precision is arguably more natural since it allows uniform attention). I would prefer if the title was precise about this fact via inclusion of the term fixed precision. Relatedly, the the following part of the intro brushes under the rug the fact that there are other reasonable models of transformers beyond fixed precision:\n\n> Although these idealizations capture key aspects of transformers, they tend to overestimate 25 the expressive power.\n\nWhat evidence for you have for this? E.g., usually in practice precision is greater than log2 n, so log precision seems reasonable.\n\n### Reconciliation with C-RASP as a Model for Length Generalization\n\nRegarding the claim that the LTL[past] results perfectly predict length generalization, C-RASP, which corresponds to transformers where attention is computed with log precision, also seems to have strong theory/experiment match for length generalization; e.g., see https://openreview.net/forum?id=U49N5V51rU. How do you reconcile your claims with theirs? Are there any languages that test a discrepancy between these formal models of transformers? Or differences in the empirical results between your experiments and theirs?\n\n### Experiments\n\nWhat precision do you use in your experiments?\n\nFor the langauges where the transformer fails but achieves near 100% performance, what does performance look like as a function of sequence length? Is it possible that the transformers are less sample efficient than LSTMs and are just under-trained?\n\nWhy do you only consider 3 languages for the language modeling experiment? Especially because the \"failing\" language still achieves 98.3% accuracy, the evidence here is somewhat weak", "was_revised": true, "final_justification": "Overall, I appreciate the reviewers' comments and maintain my positive score. I hope that, as promised, the authors better highlight the fixed precision assumption (vs. stating their results for \"softmax\" transformers) and also better discuss the differences between their empirical results and similar results for C-RASP.", "rebuttal": "We thank the reviewer for their thoughtful and positive review. We are especially grateful for the recognition of the novelty and significance of our theoretical results, the strength of the proofs, the clarity of the writing, and the potential interest to the broader research community. Below, we address the specific comments and questions raised.\n\n---\n\n> *In the title and elsewhere, this paper seems to imply its results hold for all transformer language models, while in reality it characterizes one specific formal model... I would prefer if the title was precise about this fact via inclusion of the term fixed precision.*\n\nWe agree and appreciate the suggestion. While we refer to \"fixed precision\" throughout the paper, the title and introduction could indeed better reflect the specific model we analyze. We will revise the title and refine the introductory language to make it clear that our results pertain specifically to fixed-precision transformer models.\n\n---\n\n> *What precision do you use in your experiments?*\n\nWe use the default 32-bit floating point precision provided by the standard JAX library for both training and inference.\n\n---\n\n> *What evidence do you have for this? Usually in practice precision is greater than log₂n, so log precision seems reasonable.*\n\nOur empirical results suggest that with 32-bit precision, transformers fail to generalize at input lengths below $500$ on languages outside $\\\\textbf{PFO}^2[<]$, many orders of magnitude smaller than the theoretical bound of $2^{32}$. This suggests that log precision may overestimate real-world transformer capabilities, and motivates our focus on strict fixed precision.\n\n---\n\n> *Regarding the claim that the LTL[past] results perfectly predict length generalization, C-RASP... also seems to have strong theory/experiment match... How do you reconcile your claims with theirs?*\n\nC-RASP **retains fixed precision outside attention** but allows **arbitrary precision within attention**. This effectively augments $\\\\textbf{PFO}^2[<]$ with counting. \n\nExperimentally, the two studies adopt different definitions of success. Our evaluation requires perfect generalization across all input lengths, consistent with formal models such as logic and automata. Huang et al. (2025) adopts a more relaxed criterion, focusing on strong but not perfect generalization. We view the two results as complementary: C-RASP highlights what transformers may learn approximately and generalize well in practice, while our work characterizes what they can reliably and provably generalize without error.\n\n---\n\n> *Is it possible that the transformers are less sample efficient than LSTMs and are just under-trained?*\n\nWe believe this is unlikely. Prior work (Deletang et al., 2023) shows that 1M training steps are sufficient for learning a wide range of formal languages. In our experiments, convergence typically occurs well before this point. Additionally, we find that minor architectural changes (e.g., constraining some attention heads to look only at the previous token) enable the same training setup to achieve perfect generalization on certain tasks outside $\\\\text{PFO}^2[<]$. \n\n---\n\n> *Why do you only consider 3 languages for the language modeling experiment? Especially because the \"failing\" language still achieves 98.3% accuracy*\n\nWe focus on language recognition (LR) because it is a strict subtask of language modeling (LM): to correctly predict the next token, a model must first determine which language the prefix belongs to. Therefore, failure on LR already implies failure on LM. Our LM experiments primarily serve to demonstrate that transformers can correctly track the state of the prefix and generate only permissible symbols.\n\nSince transformers have already been shown to fail at recognizing languages outside $\\\\textbf{PFO}^2[<]$, we do not expect them to model such languages either. Accordingly, we choose the simplest such language, RDP-1, as a counter-example.\n\nNote that some languages, such as $\\\\Sigma^*b$, are unsuitable for language modeling because any next token is valid at any step, making next-token prediction uninformative. \n\nAs for the seemingly high accuracy ($98.3\\\\%$), this is due to the structure of the languages. For instance, in RDP-1 $(\\\\Sigma\\\\setminus\\\\{b\\\\})^* a (\\\\Sigma\\\\setminus\\\\{a,c\\\\})^*$, any symbol except $b$ is correct before the critical $a$ appears. This allows the model to make many \"easy\" correct predictions, inflating its token-level accuracy. However, as with LR, any accuracy short of $100\\\\%$ indicates failure. The key failure mode is clearer when analyzing the model's internal states: on RDP-1, the prefix states are not distinguishable by their representations, in contrast to LDP-1 and LDP-2, where transformers successfully track the DFA states.\n\n---\n\n> *The PFO2 upper bound proof makes sense... but I'd like more detail on the following: \"it reduces to a sum of a bounded number of terms...\" The proof needs more detail.*\n\nThe key is that fixed precision limits the number of non-zero attention weights. This puts a bound on the number of summed terms. Moreover, since each of these terms is drawn from a finite set $\\\\mathbb{F}$, the total number of possible combinations and their resulting sums is also finite. For example, if at most two values from $\\\\mathbb{F} = \\{1,2\\}$ are summed, the possible sums are $1$, $2$, $1+1$, $1+2$, $2+2$, with the last two exceeding the representable range and causing overflow.\n\n> *\"Uniformly attend to positions m < n where [...]\"*\nWe cannot uniformly attend to all $m < n$ satisfying a condition when **too many positions** satisfy it under fixed precision. This is why we need two attention layers in Lemma B.11.\n\n---\n\nWe again thank the reviewer for their careful reading, constructive questions, and generous evaluation. We will incorporate all suggested clarifications to strengthen the presentation and position the work more precisely within the broader landscape.\n\n---\n\n## References\n\n- Huang et al. (2025). *A Formal Framework for Understanding Length Generalization in Transformers.*\n- Deletang et al. (2023). *Neural Networks and the Chomsky Hierarchy.*"}, {"review_id": "o21GhS5Cqt", "reviewer": "Reviewer_v13x", "summary": "It is shown that softmax transformers with ``fixed precision'' (and no positional encoding and strict future masking) recognize precisely languages from a fragment of LTL logic. This logic (containing precisely star-free languages) has been previously shown to be equivalent to unique hard attention transformers with strict future masking and no positional encoding (Yang et al).", "questions": "please see the ``strengths and weaknesses'' section", "limitations": "yes", "rating": 2, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 1, "significance": 1, "originality": 2, "strengths_and_weaknesses": "At the first glance, the result seems interesting, as it is a precise characterization of what languages can softmax (thus, practical!) transformers recognize. However, I believe that fixed-precision assumption does not make sense for the case of softmax transformers.\n\nLet me start by noting that the paper does not formally define ``fixed precision'' transformers (and, in fact, neither do other papers in this area). And this is not as trivial as it seems. Ok, when we only have operations with rational numbers, one can say that precision t means that every number in every computation can be represented as a fraction of two t-bit integers. But when we have softmax and layer norm, it means that we should do rounding. But do we use some specific rounding rule? Or is there ''an adversary'' that can return any rational number, \\epsilon-close to the real output, where log(1/epsilon) is the number of precision bits? And if  we sum up n elements one by one, when do we do rounding -- only in the end, or for each partial sum? If one thinks about it, depending on the answer, fixed precision can turn out to be logarithmic. Hence, fixed precision has to be carefully define.\n\nIn any case, it is hard for me to imagine how the fixed-precision assumption could make sense for softmax transformers. The very basic thing we can do with them is  to take the arithmetic mean of input bits (using attention with uniform weights). But just this operation requires log n bits.\n\nIn that sense, I have a ''counter-example'' to the main result (in quotes because the exact model has not been defined in the paper). Softmax transformers with fixed precision can distinguish binary strings with at most 1/3-fraction ones from strings with at least 2/3-fraction of ones (take the average of input bits and precision enough to distinguish 1/3 from 2/3). This problem is known as Approximate Majority; in [2] of the references of the paper, it is shown that unique hard attention transformers cannot do Approximate Majority while they subsume the LTL logic, which in turns subsumes the logic in the paper, leading to a ``contradiction''.\n\nOf course, there might be no contradiction if authors had in mind another model which is not capable of doing even this simple thing. But then I am not sure to which degree it is fair to call this model ``softmax transformers''.\n\nAdditionally, a speculation that practical transformers use fixed precision, say 32 bits, is not very convincing. Indeed, in that case, why at all let the input length go to infinity? Practical transformers work with inputs that do not exceed some finite number! Of course, the point is that we need to make asymptotic statements because it is not very reasonable to say what can and cannot be done for a fixed input length. Hence, I do not see any problem for such an idealization to have precision growing with n. Note that 32 is significantly larger than the logarithm of the input lengths on which practical transformers are usually run.", "was_revised": true, "final_justification": "I thank authors for their response. I did not understand the precise model from the answer. I am keeping my score as I think if the model cannot compute Approximate Majority, it is not adequate for softmax transformers.", "rebuttal": "We thank the reviewer for engaging deeply with the paper. Below, we respond to the main concerns point by point.\n\n---\n\n> *The paper does not formally define \"fixed precision\"... depending on assumptions, fixed precision can effectively turn into logarithmic precision. Hence, fixed precision has to be carefully defined.*\n\nWe define fixed precision by assuming the existence of a finite set $\\\\mathbb{F}$ of representable numbers, under which the transformer operates. We do not make assumptions about specific rounding rules, or rationality of values, or closeness to ideal real-valued outputs. Instead, we rely on three minimal and realistic properties:\n\n1. **Overflow**: There is a maximum representable number; any computation exceeding it yields overflow.  \n2. **Underflow**: There is a smallest positive number; values below it round to zero.  \n3. **Exponential cutoff**: There exists a sufficiently negative number $x$ such that $\\\\exp(x) = 0$.\n\nAll of these are satisfied by standard numerical libraries (e.g., NumPy, PyTorch, JAX).\n\nWe appreciate the reviewer’s request for precision and will clarify this definition explicitly in the final version, if given the opportunity.\n\n---\n\n> *I have a ''counter-example'' to the main result... Apprxoimate Majority...*\n\nApproximate Majority is not recognizable in our idealization, precisely because uniform attention (and thus averaging inputs) is not always feasible for all input lengths. Therefore, it does not constitute a counterexample.\n\n---\n> *I believe that fixed-precision assumption does not make sense for the case of softmax transformers.*\n\n> *Why let the input length go to infinity? Practical models use 32-bit precision and finite inputs.*\n\nOur experiments show that transformers **fail to generalize well before the theoretical precision limit**. Specifically, under standard 32-bit precision, models fail to generalize on tasks that log-precision models would handle at sequence lengths below 500, far short of $2^{32}$. Notably, length 500 is not large by practical standards either.\n\nWhy real-world models fail so early and appear empirically weaker than log-precision theoretical predictions remains an open question and an exciting direction for future work.\n\nBy contrast, our results align exactly with the fixed-precision model: languages inside $\\\\textbf{PFO}^2[<]$ can be trained to $100\\\\%$ accuracy, while those outside cannot. This suggests that fixed precision provides a realistic and informative lower bound on the class of languages transformers can express reliably and without error, and studying it is far from pointless. \n\nAdditionally, the fixed-precision setting becomes even more relevant as quantized models are increasingly popular in practice. These models operate at significantly lower precision (e.g., 8-bit or 4-bit), making precision constraints even more immediate and our theoretical framework directly applicable. \n\nIn summary, we see the study of fixed precision as **complementary** to other settings, such as logarithmic precision, or mixed precision (e.g., Yang and Chiang, 2024, where attention uses rational arithmetic but other operations remain fixed-precision).\n\n---\n\nWe again thank the reviewer for their time and effort. We hope these clarifications have helped convey the scope and motivation of our work, and we will revise the paper accordingly should we have the chance.\n\n–-\n\n## References\n\n- Yang and Chiang. (2024). *Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers.*"}]

Author rebuttal:

Meta-review: **Scientific claims and findings**:
This paper provides a precise theoretical characterization of the expressive power of transformer language models under a specific formalization: fixed numerical precision, soft attention, and strict future masking. The authors demonstrate that this class of models is exactly as expressive as a fragment of linear temporal logic containing only the "past" operator (LTL[past]). This central result is established by connecting the model to other well-known classes in formal language theory, automata theory, and a two-variable fragment of first-order logic ($PFO^2[<]$).

**Strengths**: The paper's primary strengths are its technical depth and clarity. It delivers a novel and exact characterization for a transformer model that is a step closer to practical implementations compared to prior work that often relied on idealized unique hard attention. The theoretical findings are well-supported by empirical experiments on formal languages, which show that models achieve perfect length generalization on tasks within the identified class but fail on those outside of it. This is not exactly predicted by the expressiveness theory, but provides interesting new insights and perspectives on the length generalization ability of transformers.

**Weakness**: The main weakness, and the source of significant debate, is the "fixed-precision" assumption. Some reviewers argued that this formalization is too restrictive and does not adequately capture the capabilities of real-world softmax transformers, which can perform operations like averaging that require precision that scales with input length. The authors' model, under this assumption, cannot solve problems like Approximate Majority. Other limitations noted include a partial treatment of components like positional encodings and layer normalization in the main text.

**Reason for Accept(Spotlight)**: This paper presents a fundamental and elegant theoretical result that connects a widely used neural architecture, constant-precision softmax transformer with casual masking, to a classic concept in logic and formal languages. The work is technically significant and addresses a key question in the theory of language models. The tight characterization and the clear link between theory and empirical generalization behavior make it a standout contribution.
Decision: Accept (spotlight)