Transformers are Inherently Succinct
Authors: Pascal Bergsträßer
Ryan Cotterell
Anthony Widjaja Lin
Venue: ICLR 2026 Oral (2026)
Keywords: Transformers
complexity
expressivity
automata
LTL
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: We propose succinctness as a measure of expressive power of a transformer in describing a concept. To this end, we prove that transformers are highly expressive in that they can represent formal languages substantially more succinctly than standard representations of formal languages like finite automata and Linear Temporal Logic (LTL) formulas. As a by-product of this expressivity, verifying even simple properties of transformers is shown to be provably intractable (i.e. EXPSPACE-complete).

Published as a conference paper at ICLR 2026
TRANSFORMERS ARE INHERENTLY SUCCINCT
Paseal Bergsträßer
Ryan Cotterell
RPTU Kaiserslautem-Landdaa
ETH Zürich
Kaiserslauter,, Germany
Zürich, Switzerland
bergstraesser0cs uni-k1..
ryan. syan.cotterell@ing wtwz..eehzcc.
Anthony W. Lin
RPTU Kaiserslautem-LLanda and MPI-SWS
Kaiserslautern, Germany
1in0cs.
wanncssuni-kk.eee. uni-k1.de
ABSTRACT
We propose succinctness as a measure of the expressive power of transformer in describing a concept. To this end, we prove that transformers are highly ex- pressive that they can represent formal languages substantially more succinctly than standard representations of formal languages like finite automata and Linear Temporal Logic (LTLL) formulas. a by-product of this expressivity, we show that verifying properties of transformers is provably intractable (i.e. EXPSPACE- complete).
INTRODUCTION
Transformers (Vaswani et al., 2017) the underlying model behind the recent success of Large Language Models (LLMs). The past few years saw a large amount of theoretical development explaining the expressive power transformers (Strobl et al., 2024; Barceló al., 2024; Yang al., 2024; Hahn, 2020; Pérez et al., 2021; Chiang & Cholak, 2022; Jerad et al., 2025), their trainability and length generalizability (Zhou al., 2024; Huang et al., 2025; Chiang & Cholak, 2022), and the extent to which one can formally verify them (Sälzer et al., 2025). Interestingly, it is known that transformers with fixed (finite) precision (Yang et al., 2024: Barceló et al., 2024; Jerad et al., 2025; Li & Cotterell, 2025) recognize well-known subclass of regular languages called star-free languages. Fixed-precision transformers are especially pertinent to real-world transformers, which implemented hardware with fixed (finite) precision.
Star-free languages form rather small subclass of regular languages. More precisely, a star-free regular expression allows the intersection and complementation operators instead of the Kleene star.
For this reason, the regular language a is star-free because it can be defined as 0.b.a.0. On the other hand, it is known that regular languages like (aa)* not star-free (ef. see (Straubing, 1994))- This is in contrast to Recurrent Neural Networks (RNN), which can recognize all regular languages (Siegelmann & Sontag, 1995; Merrill et al., 2020). Thus, expressivity language recognizers per se is perhaps not the most useful criterion for an LLM architecture.
In this paper, we propose succinctness transformers. More precisely, the succinctness of a language L with respect to a class of language recognizers (e.g. transformers, automata, etc.) measures the smallest (denotational) size of T that recognizes L, i.c., how many symbols are used to describe T. Succinetness has been studied in logic in computer science (e.g. (Grohe & Schweikardt, 2004; Stockmeyer, 1974)) as an alternative (and more computational) measure of expressiveness, and has direct consequence in how computa- tionally difficult is to analyze certain expression. For example, Linear Temporal Logic (LTL) (Pnueli, 1977) is expressively equivalent to star-free regular languages (e.g. see (Libkin, 2004)), as well as a subclass of deterministic finite automata called counter-free automata (McNaughton & Papert, 1971) l). Despite this, it is known that LTL can be exponentially more succinet than finite au- tomata (Sistla & Clarke, 1985). In other words, certain concepts can described considerably more succinctly by LTI. formulas as by finite automata. This has various consequences, e.g., analyzing
alternative angle in understanding the "expressivity" of

---

Published as a conference paper at ICLR 2026
LTL formulas (e.g. checking whether they describe trivial concept) is provably computationally more difficult than analyzing finite automata (Sistla & Clarke, 1985).
Contributions. Our main result can be summarized as follows:
Transformers can describe concepts extremely succinetly.
More precisely, we show that transformers can be exponentially more succinct than LTL and RNN (so including offte-of-the-art State-Space Models (SSMs), e.g., (Gu & Dao, 2023; Merrill al., 2024)), and doubly exponentially more succinct than finite automata. This means that, with the same descriptional size, transformers can encode complex patterns that require exponentially (resp. dou- bly exponentially) larger descriptional sizes for LTL and RNN (resp. automata). As a by-product of this expressivity, one may surmise that analyzing transformers must be computationally challenging. We show this to be the case. That is, verifying simple properties about transformers (c.g. whether recognizes a trivial language) is computationally difficult: EXPSPACE-comple standard time.
That is, with assumptions, this cannot be done in better than double exponential
In fact, we also show matching upper bound on the succinctness gap for LTL (exponential) and automata (double exponential). That is, we provide a translation from redd-precisoon transformers to exponential-sized LTI. formulas. This significantly improves the previously shown doubly ex- ponential translation by Yang et al. (2024). As a consequence, for any precision transformer, there is LTL formula (resp, finite automaton) of (doubly) exponential size recognizing the same language.
In proving our succinctness results, show how transformers count from up 2 .i.., the so-called "(doubly exponentially) large counters". This requires subtle encoding of large coun- ters using attention. We then prove that the resulting languages using LTL and RNN (resp. finite automata) require exponentially (resp. doubly exponentially) larger description.
What assumptions do (finite) precision. This assumption is faithful to real-world implementations, which use only fixed- precision arithmetics. In this paper, we use Unique-Hard Attention Transformers (UHATss model, which is a simple and popular abstraction of self-attention (cf. (Yang et al., 2024; Jerad et al., 2025; Strobl et al., 2024; Hao al., 2022; Li & Cotterell, 2025; Hahn, 2020: Barceló et al., 2024; Bergsträßer et al., 2024)). In particular, recent works by Jerad et al. (2025) show that expressivity bounds on UHAT's entail bounds on realistic softmax transformers with a fixed precision.
in our results? We assume that transformers and RNN of fixed
Organization. We recall some formal concepts (transformers, automata, and logic) in Section 2. We show in Section 3 how transformers can encode an exponential tiling problem. We show in Section 4 how this implies succinetness of UHATs relative to other representations. Applications of our results for reasoning about transformers are discussed in Section 5. We conclude the paper in Section 6.
PRELIMINARIES
We often denote vectors by boldface letters and for vector v (v1,..., Ud) write v[i,j] (Vi....,?) for all 1 < j S d and if i = j. we simply write vi). We also write n for a number denote vector (n, (m....,7) r1) of appropriate dimension.
An alphabet a finite set Σ of symbols (a.k.a. tokens). We write Σ" for the set of all words (a.ka. sequences, strings) of the form di ..... Un. where n 2 0 and a; Σ for all E [1,n]. We write E for the set of all non-empty words. A language is a subset L C Σ". We assume familiarity with basic concepts in formal language theory and complexity theory (see e.g. (Kozen, 1997; Sipser, 1997)). In particular, we will deal with finite automata. We will also use the following complexity classes:
P C NP C PSPACE S EXP C NEXP C EXPSPACE.
The complexity classes P and NP correspond to problems solvable in polynomial (resp. nondeter- minsitic polynomial) time, and are well-known. The complexity classes EXP and NEXP are similar to P and NP, but we allow the algorithm to exponential time. The complexity classes PSPACE
2

---

Published as a conference paper at ICLR 2026
and EXPSPACE correspond to problems solvable in polynomial (resp. exponential) space. The above inclusions are well-known (cf. (Sipser, 1997)).
2.1 LINEAR TEMPORAL LOGIC
formula in Linear Temporal Logic (LTL) over the finite alphabet has the following syntax:
9 == T T Qf all Σ) (p A y v -p 40
4 U p
We define satisfaction of an LTL formula yp on a word w = a1 an E E at position i E [1, written wc i = 4p inductively (omitting T (true) and 1. (false)):
Qo
iff
a,
(for all a 2))
W, = 81 A P2
iff
w, = P1 and w, - 422
W; $1 V PP2
iff
w,i = (P1 w, - 42
w. = 7PP
iff
w, i of 40
w,i $1 S 4P2
iff
for some with 1 S j < we have w.j F P2 and
for all k with j < k < we have w, k } 91
iff
for some j with i <
have w.j - y22 and
for all & with i < k < j we have w, k F p
Moreover, we define the shortcuts
P = TS TU:=
Xp:=
An LTL formula recognizes the language [(p) of all words Et such that w, k += ip, where k either or |w| depending on whether the first or last position is regarded the output position of s. Example 1. The star-free language (ab)+ be defined in LTL
Qa A AGG. + XQx) A G((Q& A AT) + XQa).
In words, the first letter is and at any a-position, the next letter is b. At any b-position that has successor, the next letter is a.
2.2 MASKED UNIQUE HARD-ATTENTIO TRANSFORMERS
Let E be finite alphabet of tokens. A token embedding is function cmb: E - Q for some d > 0. token embedding naturally extends to a homomorphism E* (DA)), where emb(a1.... an) = emb(ai) ... embea. (a..) for di,..., , On Σ.
Remark 2. In the following we define transformers over arbitrary rational numbers since our upper bounds even hold this setting. We remark that all of our results also hold for the special case of fixed precissin real numbers, i.e. with a constant number of bits for fixed transformer regardless of the input length. In fact, the lower bounds already hold for integers of fixed precision.
Attention layer. A masked unique hard-attention (UHA) layer of width >> 0 is defined by
three affine transformations A, B: Q Q and C: Qer Q" with rational valued coefficients (i.e., each is of the form Qx b where matrix Q and vector have only rational entries),
mask predicate M: N N + [J, which is defined by (i. := T (no masking), (i.jj) = (j < i) (strict future masking), or M (i.j) = (j > i) (strict past masking), and
tie- bie-breaking function 7 selecting element of finite non con-empty subset of N. which is either defined as min (leftmost tie- breakiik or max (rightmost breakink
We show how UHA layer works sequence Ui,-.., Un function is defined as the dot product S(v; 11) == (A(u;), B(U,)) for all i E [1, n]. For E [1, let U. = ti E [1, (i.j) } be the of unmasked positions and B, lj U; Vj' U:: S(v, v,) S(v, } be the set of unmasked positions that maximize the score function. We define the attention vector position
Q" with n
The score
[1. as a; : U+(P.) if U, * and a, otherwise. The layer outputs the sequence C(v), (101,a)).. 01), C(v,: a.))

---

Published as a conference paper at ICLR 2026
ReLU layer. A ReLU layer of width 0 on imput ......, Un E Q" applies for some & E [1,r] the ReLU function to the k-th coordinate of each Vú, ie., it outputs the sequence vi...., 2n where o/ [o,[11, 1I, max(0, v, (k)), vi(k + 1, nl). [Equivalently, forward network at the end an encoder layer (see (Hao et al., 2022; Barceló et al., 2024)).]
could instead allow a feed-
Transformer. A masked unique hard-attention transformer (UHAT) tion T: Σ + (Q+)+ defined by application of a token embedding followed by application of fixed sequence of UHA layers and ReLU layers of matching width.
func-
(Q+)+ language recognizer, we assume that T is given together with an acceplance vector t E Q The recognized language L(T) is then the set of words on which T outputs a sequence ",...., Un Q with (t, vz) O, where k E [1, n2] is either I or n depending on whether the first or last position is regarded the output position of
Languages accepted by UHATs. To view UHAT T
2.3 BOOLEAN RASP
As intermediate step prove EXPSPACE-hardmen for UHATs, use Boolean RASP (B-RASP) as introduced by Yang et al. (2024), who showed that B-RASP is expressively equiv- alent to UHATs. A B-RASP program is defined follows. Let 01 -.- On E Σ be input word. For every a E Y there is an initial Boolean vector Qu E {0, 13"h with Qu for all i [1, We number the initial vectors and call them PI..... . Px. We now describe how vector pr+1 can be defined from vectors Pl..... P. for Σ
1 iff
Position-wise operation. The vector Pet can be defined by Pi+1(1) R(i) for some Boolean combination R(i) of
Attention operation.
The vector Pi+1 be defined by either of
(i) (M(..)) V(i,)) D())
P1+1(1) (M( ((1)
where
indicates leftmost tie-breaking and indicates rightmost tie- seebbreaknng,
(i.j) is mask predicate in the definition of a UHAT,
ji and Vii.j) are Boolean combinations of (f), (RO)) ... P(()), called score predicate and value predicate, respectively,
D(i) is Boolean combination of (P) ...., P()),, called default value predicate.
The semantics of an attention operation is follows. For every E [1, m), let
M(i,j) and S(i,j) = 1}, for j. = max E [1.n] [ (i.jj and S(i,j) = 1}, for
min(j e [1, n]
We then define Pi+1 (1) Vii.i.) if je exists and (1) = D(i) otherwise.
B-RASP program is given by an alphabet Σ and a sequence position- wise and attention opera- tions. We can view B-RASP program
language recognizer by designating one Boolcan vector as the output vector and either the first or last position as the output position. Then an input word 01 ... On is accepted if and only if (k) 1, where k is the output position, i.e., k 1 or n.
2.4 RECURRENT NEURAL NETWORKS (RNN)
We use RNN as language acceptors, as in the work of Merrill et al. (2020); Weiss et al. (2024; 2018). In particular, Recurrent Neural Network (RNN) M can be viewed as a function g (R+ x xE) - Rdd
As in the case of transformers. E is also mapped into Rdd (for some d') through token embedding
4

---

Published as a conference paper at ICLR 2026
function emb (e.g. one-hot encoding) and the function actually has domain R x R We have an input vector žy E R and a final function f : R - {Acc, Rej), to decide whether a vector I E Rd is accepting. The semantics of acceptance is the same as that of automata, i.c. given w = 01 ... an E Σ", we compute d-vectors T1,- T1....,ān such that g(Ti, ax+1) = I:41 for each i 0, .0. 1. The string is accepted by M if f(T)) Acc.
f
As computational model, it realistic to assume RNNs with a fixed precision, i.e., computation is always done over real numbers that can be represented with constant k number of bits. The details of the actual representation are not important for our analysis. Therefore, the state-space Q of the above RNN can be mapped d-vectors over {0, 1] (instead of R.. The following proposition is now immediate.
Proposition An RNN g (R' x Σ) + Rdd with fixed precision k can be represented by a finite aulomaton with kd many states.
2.5 SIZE MEASURES AND SUCCINCTNESS
Let R be finite representation of a language, i.e., in our case a UHAT, LTL formula, finite au- tomaton, RNN, or B-RASP program. We define the size of R, denoted by [R]. as the length of its usual binary encoding. also as part of the size measure; since do not want compare transformer that uses fixed precision k and allow an RNN that uses a fixed precision 2*, Let C1, C2 be classes of finite rep- resentations of languages. We say that C₁ can be exponentially more succinct than C2 if for every function 20(n) there is an R1 C1 such that any R2 C2 representing the same language as R1 has size [R2] > I() Similarly, we define doubly exponentially more succinct using functions f E 22"(n) instead. Intuitively, this means that any translation from C₁ C2 incurs, in the worst-case, an (doubly) exponential increase in size.
measuring succinctness of RNN, we put the precision k unary
3 SIZE OF SMALLEST WITNESS VIA NON-EMPTINESS PROBLEM
In this section we consider the problem of checking whether the language recognized by a UHAT or B-RASP program is non-empty. In particular, the technique is essentially simulation of a Turing machine with an 20(")-sized tape (for given n)). As we will see later, there are Turing machines such that the smallest (i.e. shortest) accepted string by the constructed UHAT is of length at least 22
Example To illustrate the idea, we describe B-RASP program that accepts strings of the form
0000a, #0000,
#11llar
where a, E ba.b.c} such that (aj, (0j)) E for all 1 J 2 Here, H == Ua, (b, (b, (b, (c, is a set of constraints specifying which symbols can be next to each other. For simplicity, we concentrate on the two main conditions: (i) checking that the bit counter incremented and (ii) checking that the successive symbols are in H. To check (i), we use the following attention operation:
k-1 (A - AC(0)A
C+1 1
CÂ ++0+++++))) r=k+1
Assume is a #-position. Attention selects the rightmost # A--ooiition j left of position i. Let bf ..... and b/...b', by be the bit strings directly left of position i and j. respectively. We assume that we already defied Cx(i) bj and Cx(i) = by for all l [1,4]. 4). Then the above value predicate checks that the binary number bj ...bb,, by, the number 17 ... incremented by I. check (ii), we can use the attention operation
M (i) = ij<iQ
V Qx() (1) (K.))H
5

---

Published as a conference paper at ICLR 2026
i is a position of a symbol 0g attention picks the rightmost position of symbol aj to the left of i and checks with the value predicate that (aj. E H.
This allows us succinctly recognize language whose smallest string has length exponential in the number of bits of the binary counter. In the following we describe how to extend this idea such that can reduce an EXPSPACE-compiet! problem non-emptiness of certain B-RASP programs. Intuitively, we place multiple such strings as above on top of each other, creating multiple rows and columns (separated by #). Moreover, we introduce vertical constraints, i.e., between rows, in addition to the horizontal constraints H. Using this technique, we will see in Theorem 15 how B-RASP programs can even succinetly recognize languages whose smallest string has doubly exponential length.
We prove the following precise complexity bounds:
Theorem 5. The non-emptiness problem for UHATs and B-RASP programs is EXPSPACE- complete.
We start with the lower bound and show it first for B-RASP programs. Proposition The non-emptiness problem for B-RASP programs EXPSPACE-hard.
For the proof we use the techniques illustrated in Example 4 and reduce from a so-called tiling problem. A tile is a quadruple & Ny. where we write (teft(t), up(t), right(t), down(t)). The 2 -illing problem is defined as follows:
Given: An integer n > 0 in unary, a finite set of tiles, and a tile tfn E ET
Question: Do there exist m > and a function T: (l....,
{l....,ml m} + T such that
1. T(2", m) tim
2. doun(r(i, 1)) (p(r(i, = 0 for all 1 i 2",
3. left(r(1,j)) right(r(2",,)) 0 for all 1 m,
4. right(r(i,j)) left(T(i for all < 2n and j S m, and
5. up( = doum(r(i,j + 1)) for all i 2 and 1 S j m?
Note that an instance of the 2 -tilinnig problem consists of the number n. in unary, set of available tiles, and a dedicated final tile. A configuration of tiles, i.e., candidate for the function т, places tiles in an arbitrary number of rows and 2" columns. That is, given 2"-tiling problem instance, configurations have a fixed number of columns but an unbounded number rows.
The following is shown as Theorem 5 in (Schwarzentruberr, 2019) (by choosing k 1): Proposition 7. The 2" -tlling problem is EXPSPACE-complete
To proof Proposition 6, we construct a B-RASP program of size polynomial in n that accepts an encoding of a configuration of tiles as a sequence of strings, which are of a similar form as in Example 4, if and only if the configuration is solution of the given 2"-tiling problem instance. The key observation is that strict future masking with rightmost tie-breaking enables us to check conditions between successive tiles in row (condition 4) but also between the current tile and the tile at the most recent past occurrence of the same counter value, i.e., in the same column of the previous row, (condition 5). The proof of the next lemma can can be found in Appendix A.
Lemma 8. Given a 2" -tiling problem instance, one can construct in time polynomial in n a B-RASP program, whose language non-empty if and only if the 2 -tiling problem instance has a solution.
Lemma 8 reduces the 2""tiling problem to the non-emptiness problem for B-RASP programs. Thus, together with Proposition 7, it implies Proposition 6.
We observe that the B-RASP program constructed in Lemma 8 is of special form, which allows for a polynomial- Lemma 9, Given a B-RASP program Pı..... Pm where every attention operation is of the form
translation to UHAT.
(1) =
[M(i.)). S(j) A A Pa(i) + Pa(i) V(i.)) D(1).
AEK
where

---

Published as a conference paper at ICLR 2026
Σ f
S(j) is a Boolean combinations of (Pi())..... ... .(O)) and
K Kl
one can construct in polynomial time a UHAT that recognizes the same language.
Proof sketch. Note that Boolean operations can easily be simulated using affine transformations and ReLU. For the attention operations we use an attention layer. The value predicates (i., can be simulated by copying the required components of the j-th vector, that was selected by attention, to the i-th vector using the affine transformation whose result is forwarded and computing the result of the Boolean combination with additional ReLU layers. The part (i)) of the score predicates that only depends on j can be simulated using an additional preliminary layer that already computes the result of (j)) every position j. For the part A (i( (i) that checks equality of two binary numbers, we provide a score function that maximizes the attention score if the two binary numbers are equal. The full proof can be found Appendix
Combining Proposition 7 and Lemmas 8 and 9 yields the EXPSPACE lower bound for UHAT. Proposition 10. The non-emptiness problem for UHAT is EXPSPACE-hard.
We observe that the B-RASP program constructed in Lemma 8 only uses strict future masking and rightmost tie-breaking (and can be adapted to only use strict past masking and leftmost tie- breaking). Moreover, the UHAT in Lemma 9 preserves the mask predicate and tie- bi-bbrekking. Thus, the EXPSPACE lower bound already holds for UHAT's that only use strict future masking and right- most tie- bie-breaking (similar for strict past masking and leftmost tre-breaking).
Corollary 11. The non-emptiness problem for UHATs, where every layer uses strict future mask- ing and rightmost tie-breaking (resp. strict past masking and leftmost tie tie-breaking), is already EXPSPACE- -hadd.
We now prove the upper bounds in Theorem 5. To this end, we first note that any B-RASP program can be converted in exponential time into an LTL formula using the construction from (Yang al., 2024). In Proposition 13 we prove that the same is true for UHAT's which improves the doubly exponential construction in (Yang et al., 2024) that translates UHATs B-RASP programs first. This suffices to prove the exponential-space upper bounds in Theorem 5 since non-emptiness of languages given by LTL formulas can be checked in polynomial space (Sistla & Clarke, 1985).
For the translation from UHAT to LTL, we first have to make the crucial observation that the values occurring during the computation of UHAT are not "too large".
Proposition 12. The values occurring in the computation of a UHAT T can be represented with only polynomial number of bits in the size T. Thus, rational numbers with fixed precision, that polynomial in the size of are sufficient.
Proof. Clearly, ReLU layers do not increase the amount of bits needed since only the maximum with 0 is taken. Since our UHAT model is defined over rational numbers, we can represent each value with binary number for the numerator and binary number for the denominator. By taking the LCM, we can further assume that the denominators of the numbers in emb(E) are all equal. Note that the LCM of linearly many numbers of linear bit size can be represented with polynomially many bits. Similarly, for each attention layer we can assume that the denominators of all coefficients of the affine transformation, whose result is forwarded, are equal. This ensure that in the input sequence and after each layer the values have the same denominator. Next we argue that the numerators and denominators of all values that occur in the computation can be represented with a polynomial number of bits. The output of attention layer is an affine transformation involving two input vectors. Here, the input values are only multiplied with constants, i.e., the values in the output only depend linearly with coefficients are all equal, addition does not incur an increase in bit length of the denominators. Therefore, repeated application of linearly many attention layers can only lead numerators and
input values. Since the denominators of the values after multiplication
7

---

Published as a conference paper at ICLR 2026
denominators whose values are at most exponential in the number of layers, i.e., can be represented with polynomially many bits. For the score function we observe that the dot product after an affine transformation only involves two input vectors. Thus, the number of bits needed to represent the result of the score function is still polynomial. A crucial observation is that the results after applying the score function are not forwarded to the next layer, which would introduce an exponential increase in size in the number of layers.
By Proposition 12, we can already compute the results of the affine transformations and score func- tions during the construction of the LTL formula. This means that the LTL formula only has to simulate the position-wis behavior of attention layers, i.e, masking and selecting the position of the attention vector, but not the actual computation of values. The proof of the following proposition can be found in Appendix A.
Proposition 13. Given UHAT that recognizes a language L, one can construct in exponential time an formula recognizing L.
We remark that if we start with a UHAT, where every attention layer uses strict future masking and leftmost re-bbraking (resp. strict past masking and rightmost tie-breaking), then the LTL formula constructed in the proof of Proposition 13 only uses the (resp. F) operator. It was shown in (Sistla & Clarke, 1985) that the non-emptiness problem for the fragments of LTL that only allow P or F is NP-complete. Thus, we obtain an improved complexity upper bound for such restricted UHATs.
Corollary 14. The non con-emmtssess problem for UHATs, where every attention layer uses strict future masking and leftmost tie-breaking (resp. strict past masking and rightmost tie-breaking). is in NEXP.
Note that it was already shown in (Jerad et al., 2025) that such restricted UHAT's are equally expres- sive as the LTL fragment with only P (resp. F). However, the construction by Jerad et al. (2025) from UHAT to the LTL fragments incurs a doubly exponential blow-up, opposed to our singly exponential translation.
4 SUCCINCTNESS AGAINST OTHER REPRESENTATIONS OF LANGUAGES
We now study how succinctly transformers can represent languages compared to standard models from formal language theory.
We first compare transformers to LTL. One indication that transformers may be more succinet than LTL comes from Theorem 5, which shows that the non-emptiness problem for UHATs is EXPSPACE-complete. whereas for LTL. the corresponding problem is known to be PSPACE- complete. The following result shows that this exponential gap also manifests in terms of suc- cinctness.
Theorem 15. UHAT's can be exponentially more succinct than LTI.
Proof. We give family [12 of languages such that Ln is recognized by UHAT of size polynomial in n but any LTL. formula recognizing I., has size exponential in n. Let M,, be a (de- terministic) Turing machine that implements a binary counter with 2" bits, i.c., when initialized with 0²", it increments the binary number until it has written 1 on its tape and accepts. In particular, Mn first checks that it has 2n many O's written on its tape using an additional n-bit counter. To increment the -it counter, M,, traverses the counter from left to right while flipping every 1 to until it encounters the first O, which is then flipped to 1. For the initial check, Mn uses linear number of states in and incrementing can be done with constant-sized Turing machine. More- over, Mn uses an exponential number of tape cells in n and the unique accepting run has length at least 22". In (van Emde Boas, 1997) a reduction from Turing machines to tiling problem instances is presented that encodes configurations of Turing machines in its rows and a correct tiling corresponds to a valid execution the Turing machine. We observe that the 2p(n) 20(n)-tiling problem instance I,, for some polynomial p. constructed from Mn has size polynomial in and it has the property that the smallest correct tiling has at least 22" many rows. We showed Lemmas 8 and 9 that there is UHAT Tn of size polynomial in the size of In that recognizes encodings of correct tilings of I, Thus, Tn is of size polynomial in n and the smallest accepted word has length at least 2?" We let T., be the language recognized by T... Let pn be an L.T. formula that recognizes T.p. Since
8

---

Published as a conference paper at ICLR 2026
the smallest accepted word by any LTL formula has length at most exponential in the formula size (using an exponential conversion from LTL to finite automata similar to (Vardi & Wolper, 1994)), follows that the size of fn, is at least exponential in
show that there is language than can be represented by LTL significantly more succinct than by UHATs. Thus, we may even say that UHATs are exponentially more succinct than L.T...
Conversely,
Proposition 16. Given an LTL formula y, one can construct in polynomial time UHAT that recognizes the same language as sp
Proof sketch. From yp we construct UHAT that on input w outputs a dedicated component at position sis |w|] 1 if w. F o and 0 otherwise. Then the claim can be proven by induction. If o is an atomic formula or a Boolean combination, we can easily define T. If y = f 9p2, we assume by induction hypothesis that we already computed the truth value of (1 and (P2 every position, which we use to compute the truth value -41 V (22 We then use an attention layer with strict future masking and rightmost tie-breaking to get for every position i the maximal position j < i where P V holds and output at position i the truth value of (o2 from position j. The case where 9 10 U y22 is similar using strict past masking and leftmost tie-breaking.
We show next that compared finite automata, UHAT's be even doubly exponentially more succinct. To see this, take the UHAT T, from the proof of Theorem 15 that is of size polynomial in n and the smallest accepted word has length least 2 Since any automaton recognizing non-empty language accepts a word of length at most linear in the automaton size, the smallest automaton that recognizes the same language as Tn has size least doubly exponential in n.
Theorem 17. UHATS can be doubly exponentially more succinct than finite automata.
Conversely, the best known construction from counter-free automata (that are equally expressive as LTL) to LTL incurs an exponential blow-up (Maler & Pnueli, 1990). Thus, together with Proposi- tion 16, we obtain an exponential-tine translation from counter-free free automata to UHATs. Note that also the translation in (Yang et al., 2024) from counter-free automata to UHAT's increases the size exponentially, when using the results by Maler & Pnueli (1990).
Finally, we combine Theorem 17 and Proposition 3 to obtain the following succinctness gap between UHAT's and RNNs.
Corollary 18. UHAT's can be exponentially more succinct than RNNs.
Since RNNs recognize all regular languages, whereas UHATs only recognize the strict subclass of star-free languages, RNNs are strictly more expressive than UHATs. Thus, suceinetness in the above corollary should be interpreted with respect to star-free languages.
5 APPLICATIONS
As consequence of our results, we show that reasoning about languages of UHATs (e.g. cquivalence, emptiness, universality, etc.) is provably intractable. Contrast this to deterministic finite automata, where all these problems be done in polynomial time (ef. (Kozen, 1997)). In the following, we show the precise complexity for the equivalence problem, i.e., the problem of checking whether two given UHATs recognize the same language. That the universality problem is EXPSPACE-complees can be proven similarly.
Theorem 19. Equivalence of UHAT's is EXPSPACE -copppetcco..ee.....
Proof. To prove the lower bound, we reduce from the non-emptiness problem for UHATs, which by Theorem 5 is EXPSPACE-cooplett To this end, let T be given UHAT and fix UHAT To that recognizes the empty language. Then we have that T and To are equivalent and only if T recognizes the empty language.
For the upper bound let the UHATs Ti and Tz be given. We apply Proposition 13 to turn Ti and To in exponential time into LTL formulas yo and yo2, respectively. Now, Ti and Tz equivalent if and

---

Published as a conference paper at ICLR 2026
only if (p1 and (2 are equivalent. The latter can be decided in polynomial space (Sistla & Clarke, 1985), which results in an exponential -space algorithm in total.
6 CONCLUDING REMARKS
Related work. Our work was inspired by the works of Yang et al. (2024); Barceló et al. (2024); Jerad et al. (2025); Li & Cotterell (2025), which exhibit close connection between unique-hard attention transformers and star-free regular languages. In particular, these works also exploited the connection to LTL. However, none of these results investigated neither the issue of succinctness nor computational complexity of verification, which we establish in this paper.
Sälzer et al. (2025) investigated the issue of verifying transformers of various precisions. In partic- ular, it was shown that transformers of fixed precision are at least NEXP-hard (i.e. hard for the class of problems solvable by nondeterministic algorithms that run in exponential time). The technique there implies that transformers can be (singly) exponentially more succinet than finite automata. However, no conclusion can be derived to their succinctness relative representations like LTL or RNN. Our result substantially improve this by showing that transformers can be doubly exponen- tially more succinct than automata, and exponentially more succinct than LTL and RNN. In addition, our work assumes a much simpler model in comparison to the results in (Sälzer et al., 2025). In par- ticular, we use unique-hard attention, whereas in (Sälzer et al., 2025) combination of softmax and hardmax is employed. Finally, our results use positional masking (as employed in (Yang et al., 2024; Jerad et al., 2025; Li & Cotterell, 2025))- as a simple class of Positional Embeddings (PEs) in contrast to (Sälzer et al., 2025), which admits arbitrary PEs of fixed precision. It was recently shown in Sälzer et al. (2026) that non-fixed finite precision average- hard attention and softmax attention transformers have undecidable verification, even without PEs.
Succinetness has also been studied in the context of linguistics. For example, according to Zipf's law of abbreviation (Zipf, 1935), frequently occuring concepts tend to have a succinet description. In particular, Hindu-Arabic numeral system - which evolves into our modern numeral system allows an exponentially more succinet description than the Roman numeral system. According to Zipf's law, the former potentially enables mathematics and computer science as we see today.
Future work. We mention the challenge of developing an automatic tool for analyzing, verifying, and explaining transformers. More broadly, this is an important problem for explainable AI, as thor- oughly described in the survey (Huang et al., 2020). In particular, lots of practical advances have been made on verifying feed-forward neural networks (but not transformers) and some practical tools have been developed in the last decade (see also the results of the most recent annual VNN compe- tition (Brix et al., 2024)). Despite the rather high complexity (EXPSPACE-come) complete). we pose as a challenge to exploit techniques from automated verification (Clarke et al., 2018) (e.g. symbolic techniques, simulation, etc.) to verify transformers in practice. Similarly, since our EXPSPACE- hardness proof requires transformers that encode large counters, another research avenue is to study subclasses of transformers, which cannot encode these and potentially allow a lower complexity of verification. Another key open question concerns the learnability of succinet transformers, which is at the moment still unclear in the light of existing empirical results, e.g., see (Garg et al., 2022; Naim et al., 2025; Huang et al., 2025)). Finally, we note that our results constitute a first step to- ward understanding how succinct transformers can represent languages compared to other language acceptor models, e.g., fixed finite precision softmax transformers Li & Cotterell (2025), which are overapproximated by UHAT. We leave the study of succinctness of fixed finite precision softmax and average-hard attention transformers future work. See (Yang al., 2026) for an initial attempt.
ACKNOWLEDGMENTS
We thank David Chiang, Marco Sälzer, Andy Yang and anonymous reviewers for their helpful feed- back. Pascal Bergsträßerr and Anthony W. Lin are supported by Deutsche Forschungsgemeinscaattt (ERC, LASD, 101089343).
(grant number 522843867) and European Union'
Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the Furopean Research Council Executive Agency. Neither the Furopean Union nor the granting authority can he held responsible for them.
10

---

Published as a conference paper at ICLR 2026
REFERENCES
Pablo Barceló, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir V. Podolskii. Logical languages accepted by transformer encoders with hard attention. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. OpenRe- view.net, 2024. URL httpt: httttpp:://ppnzeevieee net /
Pascal Bergsträßer, Chris Köcher, Anthony Widjaja Lin, and Georg Zetzsche. The power of hard attention transformers data sequences: A formal language theoretic perspec- tive. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Pa- quet, Jakub M. Tomczak, and Cheng Zhang (eds.), Advances in Neural Information Pro- cessing Systems 38: Anmual Conference on Neural Information Processing Systems 2024, NeurlPS 2024, Vancouver, BC, Canada, December 10 15, 2024, 2024. doi: 10.52202/ 079017-3067. URL https:
htctps://proceediie poroceedings.o neurips cc/ cc/ hwtp:/aperrpaeeeee forrr_flllsse wiless/ppeeprrrr (ct7538866c4444440 210.:f/lleaaffaa38881115577222.1 3e oe Cow.arreerrroeeeeeeee.eeoee pdf.
Christopher Brix, Stanley Bak, Taylor T. Johnson, and Haoze Wu. The fifth international verification of neural networks competition (ynn-comp 2024): Summary and results, 2024. URL https:
/ //arr //arxivv.rrg wrw.varrgaaae abs//ba///// / 2412. 19855.
David Chiang and Peter Cholak. Overcoming theoretical limitation of self-attention. In Smaranda Muresan, Preslav Nakov, and Aline Villavicencio (eds.), Proceedings of the 60th Annual Meet- ing of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2022, Dublin, Ireland, May 22-27, 2022, pp. 7654-7664. Association for Computational Linguistics, 2022. doi: 10. 2022.ac1- ac1-longllnn 527.
URL /tttpp:://oi..rg//........ 18653//11
F.M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith. Model Checking, second edition. Cyber Physical Systems Series. MIT Press, 2018. ISBN 9780262038836. URL https://
books.googla det.ookseoooooeeeeoooo.o MAAAN
Shivam Garg, Dimitris Tsipras, Percy Liang, and Gregory Valiant. What can transformers learn in-context? A case study of simple function classes. In Sanmi Koyejo, S. Mo- hamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances Neural Information Processing Systems 35: Annual Conference on Neural Information Process- ing Systems 2022, NeurlPS 2022, New Orleans, LA, USA, November 28 December 9, 2022, 2022. URL http: http://apprr.sssee nips. cc/paperpppppeeeceeecceeeeee..ee wttppppeeeiillleepppppeeeeeeeeee fttpes//ppppee2222/aaaaaasa c52 9dba0 8a1 1 (wwraaddcf7155eee980
Abstract- html.
Martin Grohe and Nicole Schweikardt. The succinctness of first-order logic on linear orders. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pp. 438-447, IEEE Computer Society, 2004. doi: 10. 2111099/
URL https:/ doi. org /000//01.00 1tt//11111111 11w.11199/CCC 2004 1319638.
Albert Gu and Tri Dao. Mamba: Linear-time sequence modeling with selective state spaces. CoRR, abs/2312.00752,, 2023. doi: 1044850/ARXXW.2312.00733 URL https: /ttp://o..oooo/// org/10. 48550/arXiv 2tt.:x...31....7..
Michael Hahn. Theoretical limitations of self-attention in neural sequence models. Trans. Assoc.
Comput. Linguistics, 171, 2020. doi: 10.1162/TACL 000006. A.00366 URL https://dol.
Yiding Hao, Dana Angluin, and Robert Frank. Formal language recognition by hard attention transformers: Perspectives from circuit complexity. Trans. Assoc. Comput. Linguistics, 10:800- 810, 2022. doi: 10.116/TACLLA 00490.
URL https: http//do.oo//// wtt.e/.ogg/1...../tttaa.....
Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu, and Xinping Yi. A survey of safety and trustworthiness of deep neural networks: Ver- ification, testing, adversarial attack and defence, and interpretability. Computer Science Re- view, 37:100270, 2020. ISSN 1574-0137. doi: 10.10169..cxre222000.00777 URL https: // //www. www.nciieeeeee rect. com http://ccc..cccccaaaaaaa//a////a

---

Published as a conference paper at ICLR 2026
Xinting Huang, Andy Yang, Satwik Bhattamishra, Yash Raj Sarrof, Andreas Krebs, Hattie Zhou, Preetum Nakkiran, and Michael Hahn. A formal framework for understanding length gen- eralization in transformers. In The Thirteenth International Conference Learning Repre- sentations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net, 2025. URL https: //openreview. net. forum? d=14 9N5V51
Selim Jerad, Anej Svete, Jiaoda Li, and Ryan Cotterell. Unique hard attention: A tale of two sides. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar (eds.), Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), ACL. 2025, Vienna, Austria, July 27 August I, 2025, pp. 977-996. Association for Computational Linguistics, 2025. doi: http///o........o////o////// 180.1118633/// wtt.:///......5////005555...5... short 76,
URL
Dexter Kozen. Automata and computabilitty Undergraduate texts in computer science. Springer, 1997. ISBN 978-0-337-994907-..
doi: 00.1007/978-1-4412-18444
Jiaoda Li and Ryan Cotterell. Characterizing the expressivity of transformer language models. CoRR, 0bb/22055.26223 2025. doi: 10.4550AARXIV.5052263... URL https: http::://doo.oooo 10. 48504 arriv 2505 23623.
Leonid Libkin. Elements of finite model theory, volume 41. Springer, 2004.
Oded Maler and Amir Pnueli. Tight bounds the complexity of cascaded decomposition of automata. In 31st Annual Symposium on Foundations of Computer Science, St. Louis, Mis- souri, USA, October 22-24, 1990, Volume II, pp. 672-682. IEEE Computer Society, 1990. doi: D0.1109/FSCS.1990 1990.89589. URL https: doi. org/ 100 110111199//0 /CS.///SCC.... wtt.0/////S.1..........
Robert McNaughton and Seymour Papert. Counter-free Automata. M.I.T. Press, Cambridge, Mass., 1971. ISBN 0262130766
William Merrill, Gail Weiss, Yoav Goldberg, Roy Schwartz, Noah A. Smith, and Eran Yahav, A formal hierarchy of RNN architectures. In Dan Jurafsky, Joyce Chai, Natalie Schluter, and Joel R. Tetreault (eds.), Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, ACL 2020, Online, July 5-10, 2020, pp. 443-459. Association for Computational Linguisties, 2020. doi: 110.6555122200AAAAMMMAI 18653/vll 2200222022222 acl -main. 43.
URL https: pestps:/Aa / //w.///////////////////.. org/10.
William Merrill, Jackson Petty, and Ashish Sabharwal. The illusion of state in state-space mod- els. In Forty-first International Conference Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024. OpenReview.net, 2024. URL https:////// wwwp/rwpeeeew..e/////p/.. net forum?ide Q7go9JZpIq.
Omar Naim, Jerome Bolte, and Nicholas Asher. Analyzing limits for in-context learning, 2025. URL
03503.
Jorge Pérez, Pablo Barceló, and Javier Marinkovic. Attention is turing-complete. J. Mach. Learn. html.
Res., 22:75:1-75:35, 2021. URL https:t///// jmmrr http://.tt..//eeeeeeee/ee http:/ppppesv//22/peppp
Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46-57, 1977. doi: 10.1109/SFCS.1977.33 URL https: //doi. wrwpi.oorg/1..... 1ttg///..119/SCCCC TwT.EECC......... 1977.32.
Marco Sälzer, Eric Alsmann, and Martin Lange. Transformer encoder satisfiability: Complex- ity and impact formal reasoning. In The Thirteenth International Conference Learn- ing Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net, 2025. URL htttss://cpenreee http://www..a......ooooooaaaaaaa
net wtt.://mdd..-.
Marco Sälzer, Chris Köcher, Alexander Kozachinskiy, Georg Zetzsche, and Anthony Widjaja Lin. The counting power of transformers. In The Fourteenth International Conference on Learning Representations, 2026. URL https: h//p//ppeeviiieeee/ee/eeeeeeeeee /ttpttts//peeneeeeiee net/ /t///oormmiiii// wttp://wwwweeeeeteeeaaeaae--eaee
François Schwarzentruber. The complexity of tiling problems. CoRR, abs/ 0ttbb//99000002.. 2019. URL http://arxiie wwt.t//orgg////////////oo/ss//es .01102
12

---

Published as a conference paper at ICLR 2026
Hava T. Siegelmann and Eduardo D. Sontag. On the computational power of neural nets. Comput. Syst. Sci., 50(1):132-150 1995. doi: 10.1006/JCCSS.1955.113. URL https: /tt.///o.///a/////// .org/ 1tt...99...111
10.1006/ joss.
Michael Sipser. Introduction to the theory of compulation. PWS Publishing Company, 1997. ISBN 978-0-534-94728-6
A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. doi: 10.1145/3828.387.. URL attps:t////... :/tpss:///c../// org/ otg//0..1100 10..144/ 3.228.8880 3837.
Larry Joseph Stockmeyer. The complexity of decision problems automata theory and logic. Phl) thesis, Massachusetts Institute of Technology, 1974.
Howard Straubing. Finite Automata, Formal Logic, and Circuit Complexity. Progress in Theoretical Computer Science. Birkhäuser Boston, MA, I edition, 1994. ISBN 978-0-8176-3719-4 doi: 10. 1007/978-
1-6-12-028-2-9 1007/97--1-461--28889 URL /doiip httpss//////ttt//////tt/ org/ 1111111111007911--151100
Lena Strobl, William Merrill, Gail Weiss, David Chiang, and Dana Angluin. What formal languages can transformers express? A survey. Trans. Assoc. Comput. Linguistics, 12:543-561, 2024. doi: 111162/TTCCLAL0000 URL https::///// http:/ii..gg..gg//// www.//.......oo..oooooooo/.../.o wtt.:o.111/tttaaaeeeeaeeaeaa 00666.
Peter van Emde Boas. The convenience of tilings. In Complexity, Logic, and Recursion Theory, pp. 331-363. CRC Press, 1997. doi: 10.1201/97804291874990 URL https: //to:///ooooo org/10. 1201/ 0011//78042918449
Moshe Vardi and Pierre Wolper. Reasoning about infinite computations. Inf. Comput., 115(1): 1-37, 1994. doi: 10.1006/NC0.1199..099 URL https: /tt:://doi..ooo http://i...g/0.1000///1 00t.//....00/1111 inco. 1092.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (eds.), Advances in Neural Information Processing Systems 30: Anmual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp. 5998-6008, 2017. URL https: http:///cccccccc..e///////o wwwpeediiinnnn.eniiieeeeeeeeeeie wwtpp/ppp//1//////eeeapppe 2tt/2/217hhhh///// 3f5ee2435 (t1.554/7/ee11111eeeeeeeeee1
Abstract html.
Gail Weiss, Yoav Goldberg, and Eran Yahav. On the practical computational power of finite precision mns for language recognition.
Iryna Gurevych and Yusuke Miyao (eds.), Pro- ceedings of the 56th Annual Meeting of the Association for Computational Linguistics, ACL 2018, Melbourne, Australia, July 15-20, 2018, Volume 2: Short Pupers, pp. 740-745, As- sociation for Computational Linguistics, 2018. doi: 10. (0.18653N1/P18-2117. URL https: //aclanthology. www.hhooooyy..../.eeo crg/p18 2117/. 2117/
Gail Weiss, Yoav Goldberg, and Eran Yahav. Extracting automata from recurrent neural net- works using queries and counterexamples (extended version). Mach. Learn., 113(5):2877- 2919, 2024. doi: 10. 00.1007//119994-222-006666 s10994- 0209944--22--0 0000--0663-22-
URL https:/ /tts:///do.... www.///..1..... http:///oo.orrg....o
Andy Yang, David Chiang. and Dana Angluin. Masked hard-attention transformers recog- nize exactly the star-free languages. In Amir Globersons, Lester Mackey, Danielle Bel- grave, Angela Fan, Ulrich Paquet, Jakub M. Tomezak, and Cheng Zhang (eds.), Advances in Neural Information Processing Systems 38: Annual Conference on Neural Informa- tion Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, December 10 15, 2024, 2024. URL /tap::://papps....e nips capps.c//pan
/////sh/////// html.
Andy Yang, Pascal Bergsträßer, Georg Zetzsche, David Chiang, and Anthony Lin. Length general- ization bounds for transformers, 2026. Under submission (preprint: https: zzeodo. org/ records /1800700).
13

---

Published as a conference paper at ICLR 2026
Hattie Zhou, Arwen Bradley, Etai Littwin, Noam Razin, Omid Saremi, Joshua M. Susskind, Samy Bengio, and Preetum Nakkiran. What algorithms can transformers learn? A study in length gener- alization. In The Twelfth International Conference Learning Representations, ICLR 2024, Vi- enna, Austria, May 7-11, 2024. OpenReview.net, 2024. URL https: htt.https://ppeeeee /tppreeeeeeeeeeeeeeeeeeeeeeeeeee net/ forum? id-aadddsssss TuHnHHX
George Kingsley Zipf. The Psychobiology of Language: An Introduction to Dynamic Philology. Houghton Mifflin, Boston, MA, 1935.
A PROOFS FROM SECTION
A.1 PROOF OF LEMMA 8
Let 2"-tiling problem instance with in unary, of tiles T, and final tile Lin T be given. We encode configuration of tiles, i.c., candidate for the function in the 2"-tiling problem definition, as word over the alphabet == TU, 1, #}. We define enc, {l...., 2 x (1.....m} m] - E" such that
enc, (i,j) = (i - ()#
for all E [1, 2 and j E m]] where (i - 1) denotes the binary encoding of with bits and most significant bit first. Then
enc(r) == enc, (1, 1) enc- (2", 1) enc, (2, 1) enc, (nc,(m, 2")
construct a B-RASP program that accepts enc(T) if and only if satisfies the conditions above.
The B-RASP program first checks whether the input is word from (10, 4)) using the follow- ing Boolean vectors:
Ar(1)=
(1 V v+(i): :0
tET Ac,( : j,< v vQ()): :0
Ac.(1i = Ac=x(())
for k = ......
(i) =- > []<<,,1]
A+)(1)= = (b<
for k = ...... +1 "
Aeno(1) = (Q (1) + Ar(i)) ^ ((V 2+(1) - Ac,((i) A Amn+(())
TET
We use the vector
A(1)
< end (j) 0 Aeme(1) (1)
to check that (inc(i) the length of the input. Note that we still have to check that the symbol at position & is # But consecutive binary numbers separated by the encoded
every position i, which is the case if and only if A(e) = 1 where č
before that, ensure that for every value increases by or is set to 2" - is reached.
(1) = J < i, Qo(5) v Q10) Q10) 0 Ck(1)= = > (j<i) v 2101 C :
for k = 2....,
" k-1
C+1(1)= , [ V (A -C(0AGG)) ACK() -C0AAC-)))AAAAMCCCCC AC(()
A +(0+0))) :0
r=#
C1-0(1) b 1+((,2(()) A -ca()AC.)) A -C,(1)
C(i) 1)(iQ0(() A-- A
14

---

Published as a conference paper at ICLR 2026
Now, C(E) if and only if the binary numbers required.
Next, we check that the input ends with f' #
(i) = < i V Qr) Q.0)::
for E T
MET
F(1) == Q mm (1) A C2()
Then F(t) = if and only if the input ends with t.
We continue by verifying conditions 2 and 3 of r.
(1()) := <( Cx(1) + C.0)1:
V
B,(i)
1=
TET: down(t)=
ET(1): = ; 10 < (+))))) (( V
B(JI A -C(OM)
V
B(O)) A
1ET: xp(1)
BET: up(c)=0
V B((1)) :0
tET: up((==
(1) ^ -c(())
V
B((1)
k=1
1ET: 1ef(()=0
B4(1) = A Cx(1)) + V
B((i))
k=1
1ET: right())-
E() 1 < ( (EE(i) E-(j) E-())) E1()))))))))) A
Now, conditions 2 and 3 hold if and only if E()) 1.
Finally, we ensure that conditions and 5 are satisfied.
M((1) = )b<ū A A C&( ++ C&O)
V
B((1) A Be()) :1
Gr'T: (oum(()=up()))
(1) = bbb ( V Cx(1)) +
V
Bi(i) B+ :1
k=1
GUET: left())=righc)))
M(1) = < i (
M-) M1(1) M. (1)
Then (f) if and only if conditions and hold.
Thus, we define the output vector to be the conjunction
(()) = A(i) A C(1) A (() A E() A M(i)
and say that the B-RASP program accepts if and only if Y 1, then the B-RASP program rec- ognizes the set of all enc(T) where satisfies the conditions above. Hence, the language recognized by the B-RASP program is non-empty if and only the 2" 2"-tiling problem has solution.
A.2 PROOF OF LEMMA 9
Let PI,...,Pr Pm.. be B-RASP program over the alphabet Σ {a),..... } where P; is the initial vector Qo, for all 1 < E We construct a UHAT over Σ that recognizes the same language as the B-RASP program. We use one-hot token embedding emb: Σ + {0. 10 i.e., emb(a;) := e, for all < f < Σ), where e, denotes the f-th unit vector. Then (i( coincides with the t-th component of the i-th input vector of the UHAT after the token embedding is applied. The UHAT will preserve these components in each layer and will gradually add new components to store the value of (i) for all | < & So assume already defined the layers of the UHAT that
15

---

Published as a conference paper at ICLR 2026
compute the vector layers whose output will be
position i for | S m. We now define additional
We first consider the case where Pt-1 is position-wise operation, i.c. Pi+1(i) is defined by Boolean combination of {Pi (())).,.,,PP(();; We define UHAT layers to compute the result of that Boolean combination bottom-up. Assume we already defined layers that output (R) (i)...... ..... where & 2 t and R, (i)..... (i)
(i)), contain Pi (.)....., (i) and the results of previously computed subformulas. To compute the result of -RR (i) for some & E s]. add an attention layer that just forwards - R& (i) at position in an additional component while leaving the first 8 components unchanged. To compute (t) (i) for some k, é E [1. we first use an attention layer to in an additional component followed by ReLU layer that forwards the result of max (0, (x) + Re(1) -1} in this additional component, again leaving the first s components unchanged. We do not have to deal with R& (i) V Re()), since it can be rewritten as ((-R{(()A-(R((() After computing the results of all subformulas, we add an additional attention layer to only forward (Pi (i),... ..... 1 (i)), i.e. removing the intermediate results. Observe that Boolean combination has only linearly many subformulas.
forward (2) + (i)
Let us now consider the case where Pi+1 is an attention operation of the form
(i+1(1)=
(M() A Px()) PR(O) V(I.)) D(i)
kEK
as in the statement of Lemma 9. We first use additional layers as in the case of position- wise operations to compute the result of -i at every position i an additional component to output (i) Pc()), S(i)). Next we use an attention layer to add the result of 1 (x for all K every position in additional components. We then add an attention layer that uses mask predicate M, tie-breaking according to and attention score
Σ (Pa(1)PaL)) (1 Px(0) --000000----000---0-0-00--00--)- -PGGI)) KEK
(1-)
which is equal to 1 K| (x(() PaO)) (1 -(i)) since
Pa(1) + (1 P((O)(1 Pa(O)) ={1,
[1. if Px Pa())
otherwise.
Thus, the score is maximized (equal [K]) if (t) P)) for all E K and S(j) 1. For every position let js be the position of the vector that maximizes the attention score w.r.t. i. The attention layer forwards the vector (P). (i))), Pi Pi(),, ... P..k).,,,.( S(())) position i. We now compute the result of
R(1) = S(j) A PAO0 + ((0
KEK
at every position as in the case of position-wise operations and forward the vector P(())...... Po(j.), R(i)). Finally, we compute
(R(1) A V v (-R(I)A(())
by again using additional layers as in the case of position-wise operations, whose result is exactly (1). We then forward (Pi (i). Ptt
It remains to describe when the UHAT accepts. If P. is the output vector of the B-RASP program, then we stop the construction of the UHAT after the layers to compute P, are constructed. The acceptance vector of the UHAT is then defined as et, i.c., the t-th unit vector, and the output position is the same as the output position of the B-RASP program (i.e., the first or last position of the sequence). This means that the UHAT accepts if and only if (e,, (k). holds if and only if (k) = 1.
0, which
We observe that the resulting UHAT only has polynomially many layers since the result of each operation P. can be computed using an additional number of layers that is linear in the description size of Pt.
16

---

Published as a conference paper at ICLR 2026
A.3 PROOF OF PROPOSITION 13
Let T be a UHAT that recognizes a language L C Σ+ and F be set of binary representations of rational numbers that may oceur during the computation of from Proposition 12. Our goal is to define for the E-th layer of 'T and every vector v E Fs, where is the output dimension of layer f, an LTL formula & such that if is applied on input w Σ, then the ε-th layer outputs at position i E [1, |w]] the vector v if and only if w, - Ge. We define this formula inductively on the layer number f. Let emb: - (Qrd)" be the token embedding of TT For all E Fd let
Vagemb ((0) Qa, if emb emb (v)) + 1
otherwise.
We now define the formula for layer E 2+11 1. In case of a Rel.U layer of width that applies ReL.U to the k-th coordinate, we can simply define
Pe
MEF: (ax(00x)=
for all E PT. layer + an attention layer with strict future masking and rightmost tie- breaking defined by the affine transformation C: Q Q and score function S: Q Q" let
E+1 Fr
V
Pu A
V BEF S(u.b)<SSu..a)
xb) (
V
vb)
BEF
C(u,a)=v
S(n,b)>-S(u.a)
for all v F To account for the special case, where the set of unmasked positions is empty, take the disjunction of the previous formula and (-PT) urP:: C(u,0)== F We omit this special case in the following. If the layer uses leftmost tie-breaking, we adapt the formula as follows:
pu (P(v' A-
(b)) (-P
V
+())
U.OEF
BEF ((u.))25(u.a)
BEFT S(M.D)>-Su..)
C(u.a)=
The case of strict past masking is similar, where we use U instead of S and F instead of the layer uses no masking and rightmost tie-breaking, we distinguish three situations: the attention vector is at the current position, the attention vector is strictly to the left of the current position, the attention vector strictly to the right of the current position. For the situation, where the attention vector is at the current position,
P A(P
V BER"
4
(-F
9
BE S(u.b)2S(u.cu
C(u.u)=v
8(u,b)>S(u.u
For the situation, where the attention vector strictly to the left of the current position, we use
V
pu ^ (-F
V
sbb
F.
BE
S(u.b)2S(uu
V
(b)
(pp
P
V
DEF": S(u.b)<S(u.a)
S(u.b)>S(u.a)
Similarly, for the situation, where the attention vector is strictly to the right of the current position, use
A
(-P
V
W.FE (A
BEP
S(u,b)
(3)
(F(p2
-F
A(F
V DEFT s(u.b)>S(u.a)
v6))
DEFT. S(u.b)2S(u.a)
Thus, in the case of masking and rightmost bre-brea,ing, define oft1 the disjunction of Equations (1) to (3). The case where the layer uses no masking and leftmost tie- breaking is analogous.
17

---

Published as a conference paper at ICLR 2026
Finally, if there are layers, where the last layer outputs vectors of dimension s, and è Q is the acceptance vector T, we define the formula
VEF* (6,))
Then k F yo if and only if w E L, where k is the output position of
remains to argue that y can computed in exponential time. By Proposition 12, |F is exponential in the size of T and every representation in F is of polynomial size. Moreover, can be computed in exponential time. The formulas of+1 at every layer e + 1 of width depends on [F((() many formulas from layer f. Moreover, F can be computed time polynomial in | 17], since we only have to compute affine transformations polynomial in [T The formulas oe the last layer depend layer 0, where r' is the maximum width of all layers. Thus, P has size exponential in [T] and can be computed in exponential time. Therefore, also yp can be computed in exponential time.
vectors from F", where each component is of size
| ()O(r'm) many formulas from
18


Reviews:
[{"review_id": "lQ6ANaltMP", "reviewer": "Reviewer_aJWw", "summary": "This paper proposes *succinctness* as an alternative measure of the expressivity of the transformer architecture used in most LLMs. It goes on to prove that transformers (with finite precision, UHAT attention) can in fact be exponentially more succinct than LTL formulas and can be doubly-exponentially more succinct than traditional RNNs. They point out interesting corollaries, such as it being EXPSPACE-hard to solve the non-emptiness problem for UHAT transformers and for B-RASP programs; they do this by constructing languages whose shortest string is of (doubly-)exponential length in the size of the transformer / program.\n\nWhile the idea of studying succinctness is creative and the results intriguing, diving deeper into the paper, I found many places where either the argument is not structured as clearly as it should have been, or where basic (but key) concepts are not described in clear detail, or where some leaps are made that need further justification.\n\nThus, while I am really excited to see this work be published, I feel it needs a careful pass by the authors to improve various aspects in order to make the paper more coherent and technically accurate. (see specific points below in the weaknesses section)", "questions": "Please see the lengthy discussion above, especially around the proof of Theorem 14 (which builds upon subtleties in the proofs of Prop 6 and the definition the tiling problem considered here). I am willing to raise my score if the authors are able to address these concerns clearly during the rebuttal phase.", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "* The proposal of using \"succintness\" of representation as a way of measuring expressivity is novel in the study of the transformer architecture. It seem very interesting to pursue.\n\n* The results (but see caveats below in the weaknesses section) are quite intriguing, showing how transformers can represent certain counting and tiling problems vastly more succinctly than LTL formulas and RNNs.\n\n* The authors clearly identify the architectural assumptions (more like choices) early on in the paper, which helps place this work in the context of several alternatives that have been analyzed in the past few years. (but again see caveat in the weaknesses section below)", "weaknesses": "* While the paper makes it clear that the architectures use finite precision and unique rightmost hard attention, the authors don't mention other key aspects that seem important and consequential. E.g., the B-RASP program construction in the proof of Proposition 6 (tiling) uses $\\Theta(n)$ predicates at each position $i$, which allows each # position to have access to the entire counter value represented by the previous $n$ positions, which then allows checking \"locally\" for increment by $1$. This is fine, but it also means the vectors represented in the transformer construction that simulates this program (in the proof of Theorem 14) need $\\Theta(n)$ width vectors at each position. Besides making the studied transformer model non-uniform, it also means that when reconstructing the $\\Theta(n)$ predicates at each # position, one needs $\\Theta(n)$ attention \"heads\" to retrieve the past $n$ values into a single position, again adding to the non-uniform description of the transformer. Is this accurate? If so, it would be valuable to mention this early on -- that the transformer model (for the lower bound) will use linearly many attention heads and linear width. It should also be mentioned in section 2.2 where $d$ is introduced -- presumable $d$ isn't a constant, it's a linear function of $n$ in the constructions in this paper.\n\n* In a similar vein, Proposition 11 seems to assume there is no *layer norm* or non-linearity like *sigmoid* or *inverse-tan* in the transformer architecture. Is this correct? If so, it would be good to note it somewhere.\n\n* Some statements should be described more carefully. E.g., at the top of page 2 (line 54), it's not that transformers *are* exponentionally more succinct, it's that they *can be*, for certain problems (shown here for the $2^n$-tiling problem). \n\n* Proposition 7 states that the $2^n$-tiling problem is EXPSPACE-complete, citing Schwarzentruber (2019). There is, however, no direct analog of this in the reference, from what I can tell. The closest I see is Theorem 5, which states that TILING$(2^n, n)$ is PSPACE-complete. The problem definition in that paper, however, has $n$ specified in **unary**. Are you deducing that, if $n$ were instead specified in **binary** (like you do), then TILING$(2^n, n)$ will become EXPSPACE-complete? This can use some clarification, also about the difference in the 2nd argument of the tiling problem. What you have appears closest to TILING$(2^n, *)$ in the notation of Schwarzentruber, and isn't a perfect match with a specific theorem of Schwarzentruber.\n\n* The proof of Theorem 14 (arguably the main result) is confusing, to say the least:\n\n* (a) The proof starts with a Turing machine $M_n$ that implements a binary counter with $2^n$ bits. It's stated that this machine has $poly(n)$ size without saying why. It seems that *given* a $2^n$ bit string, incrementing it needs only a fixed size Turing machine -- one just has to identify the rightmost $0$ and change it to $1$. The only complication is when the string looks like $0...01...1$, in which case the machine needs to detect that there are no $1$s to the left of the rightmost $0$, and change all $1$s to $0$s, which also seems doable without any machine size dependence on $n$. Is the $poly(n)$ size needed to write down $0^{2^n}$ at the very start?\n\n* **[most critical issue]** (b) The proof says that the tiling problem instance $I_n$ constructed from $M_n$ has size $poly(n)$. Since the authors' definition of the $2^N$-tiling problem specifies the input $N$ in *binary* for tilings with $2^N$ rows (which means an instance with $2^N$ tiling rows has size $\\log N$), this sounds correct with $N = 2^n$: input size is $O(n)$ and the tiling has $2^{2^n}$ rows, as the authors state. However, they then state that the proof of Prop 8 showed that there is a UHAT of size polynomial in the size of $I_n$, i.e., a UHAT of size $poly(n)$. First, the statement of Prop 8 is really about the non-emptiness problem being hard, not about the size of a UHAT; the latter is presumably buried inside the proof and should be brought out as a lemma that can be directly referenced in the proof of Theorem 14. Second, the proof of Prop 8 actually provides a polynomial time simulation of the B-RASP construction in the proof of Prop 6. So the size claim is actually coming from the proof of Prop 6 (again, the statement of Prop 6 can't be pointed to; one has to dig into its proof to find support for the $poly(n)$ size claim in the proof of Thm 14). This is where it seems to me that there is possibly a serious issue -- the B-RASP construction in the proof of Prop 6 constructs a program that has $\\Theta(n)$ predicates at each position (as also noted above in my review), and, importantly, this is for an instance of the tiling problem of size $O(\\log n)$. Specifically, when $n$ is provided as binary, the B-RASP program constructs at each position $i$ predicates $C_1, C_2, ..., C_n$. In other words, a tiling problem input with size $\\log n$ requires B-RASP programs of size $\\Theta(n)$ in Prop 6. So the tiling problem $I_n$, which has size $poly(n)$, will presumably require a B-RASP program of size $exp(n)$ by Prop 6, which implies UHATs of size $exp(n)$ by Prop 8, which conflicts with the argument presented in support of a $poly(n)$ size UHAT claim in Theorem 14 in lines 398-401.\n\nThis last part -- the proof of Theorem 14 -- is in the best case confusing and in the worst case incorrect. Again, I like where this paper is going and it's possible that the results are actually correct. But the current way the arguments are presented is confusing and, to be honest, somewhat sloppy in places. Having clear statements of \"nuggets\" of proofs that are cited and used later would have been much better, rather than indirections through multiple proofs.\n\n\n* Clarification: in section 2.5 (size measures), why is succinctness not defined directly as $|R_2(n)| = 2^{\\Omega(|R_1(n)|)}$? Does one have to go through every $f \\in 2^{o(n)}$? (this might be true, would help to explain if so)\n\n* The paragraph at the bottom of Example 4 (\"This allows us to succinctly ...\") is unclear when it talks about \"stacking multiple such strings vertically... double exponential length\". Please clarify what this means and how this will be used later in the paper.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "TEyJI4DQAP", "reviewer": "Reviewer_cqAR", "summary": "This paper studies the class of languages expressible by Uniform Hard Attention Transformers (UHAT) with fixed precision.\n\nPreviously, it has been shown that UHATs can recognize exactly the class of star-free languages, which is a subset of regular expressions. This is not as expressive as other classes, such as RNNs, which can recognize any regular language.\n\nIn order to understand potential benefits of UHATs over other classes of recognizers (such as Linear Temporal Logics (LTLs) and finite-state automata), this paper studies the succintness of this class. I.e., what languages can be recognized with polynomial-size UHATs.\n\nThe main results are:\n(1) Determining whether a UHAT can recognize some string is EXPSPACE-complete.\n(2) There is an exponential-time reduction from UHATs to LTLs.\n(3) In fact, the above reduction is tight, in the sense that there are UHATs that require an exponentially-larger LTL to recognize the same language. And also any LTL can be reduced to a UHAT with a poly-time reduction.\n(4) There are UHATs that require doubly-exponential size automata to recognize the same language. Therefore, they require exponentially larger RNNs to recognize the same language.", "questions": "* See weaknesses.", "limitations": "", "rating": 8, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "* This paper provides a rigorous and clear analysis of a special case of transformer models (UHATs). Upper bounds have complementary matching bounds. These help build a growing literature analyzing transformer architectures via a complexity-theoretic lens.\n\n* The paper demonstrates that even though RNNs are more expressive than UHATs, there are languages that UHATs can recognize that would require an exponentially larger RNN to recognize. This is interesting, since it is a neat demonstration that expressivity is not the end of the story for comparing Transformer architectures to RNN architectures. Instead, the picture is more subtle once one studies what can be expressed efficiently (in poly-size).\n\n* In my mind, this paper gives more motivation for hybrid architectures that incorporate both UHAT layers and RNN layers, getting the best of both worlds in terms of succinctness & expressivity.", "weaknesses": "* It is shown that UHATs are shown to have more succinct representations than RNNs for some languages. However, it is also known that RNNs are more expressive than UHATs. Therefore, in terms of succinctness of representations the two classes are incomparable. Thus, the title \"Transformers are inherently succinct\" is a little misleading, because RNNs are also \"inherently succinct\" at other languages that Transformers are not succinct at. A sentence acknowledging this (e.g. in the discussion or after Corollary 17) could go a long way.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "mBTbSDapp0", "reviewer": "Reviewer_rC5n", "summary": "The paper investigates the computational complexity of the emptiness problem for Unique Hard-Attention Transformer Models (UHAT). The authors show:\n\n1. Non-Emptiness of UHATs is $\\textsf{EXPSPACE}$-complete.\n   They show the lower bound via an reduction from the $\\textsf{EXPSPACE}$-complete $2^n$-Tiling problem.  The upper bound using a new translation from UHAT to LTL of single-exponential size, improving prior double-exponential constructions.\n2. They show several succinctness results. Explicitly they show that UHATs can be exponentially more succinct than RNNs and LTL and doubly exponentially more succinct than finite automata.\n\nAs a consequence, several basic reasoning tasks (non-emptiness, equivalence, universality) for UHATs are $\\textsf{EXPSPACE}$-complete.", "questions": "1. It is interesting that for future-masking and left-most tiebreak (resp. past-masking and right-most tiebreak) the problem is in $\\textsf{NEXP}$. The cause might be the lack of real positional information, right? Because after the maximum score was reached once, you will always attend to the first position which reached the score.\n2. Lemma 9 shows equality checking of two binary strings via attention. In the proof of Proposition 6, value predicates check both equality and $Q_{\\\\#}(j)$. Is this covered by Lemma 9, or is an additional modification needed?\n3. Can the authors include the explicit construction (or layer count) needed to simulate the B-RASP program of Prop. 8 as an UHAT? In particular, how do you avoid an exponential blow-up when translating Boolean expressions (e.g., no hidden DNF expansion as it was done in Yang et al. (2024))?\n\n**Minor Comments**:\n\n- In Section 2.4, the symbol $k$ is used both for embedding dimension and precision. Using distinct symbols would avoid confusion.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The results enrich our understanding of the attention mechanism in general and complement recent theoretical results on UHAT as well as on the emptiness problem for transformers with other attention mechanisms.\n- The succinctness results and EXPSPACE bounds are technically non-trivial.\n- Despite heavy theory, the paper is readable and provides good intuition", "weaknesses": "- UHAT is an intentionally minimal transformer abstraction. The paper would benefit from a discussion of how the results transfer to *practical architectures* (e.g., softmax attention, non-unique ties) and how much of the succinctness phenomenon is specific to UHAT\n- The $\\textsf{EXPSPACE}$-hardness construction (Prop. 6 & 8) relies on several non-trivial translations but omits the concrete UHAT layer-level construction. Without at least an appendix-level sketch (including an explicit bound on number of layers / parameters), the claimed polynomial reduction is difficult to verify.\n\nThis paper provides meaningful theoretical advances and improves important prior bounds. If the authors add a detailed construction of the EXPSPACE hardness reduction (Prop. 6/8), the contribution will be significantly stronger and easier to verify.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "ojVQG1vGQO", "reviewer": "Reviewer_TYFS", "summary": "This paper gives a formal analysis of a certain class of transformers and shows that they can have very efficient codings for formal languages.  In particular, they can represent complex linguistic patterns that formal languages like LTL or neural models like RNNs require exponentially longer representations to express.", "questions": "How does this result for UHATrelate to pushdown automata or stack automata for some of which the emptiness problem is PSPACE complete?  Can we place the UHAT class of transformers somewhere in this hierarchy?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "This is an important result that advances our understanding of the capacities of certain classes of transformers.   One upshot of this paper is that verifying equivalence of transformers, even relatively weak kinds, can be very difficult and computationally intractable.  This raises an interesting question for interpretability and explainability.   It its provably intractable to show that two transformers are equivalent, then we can't hope to get a computationally tractable method for determining whether a transformer is equivalent to some other model say expressed as an LTL formula.", "weaknesses": "When the authors give a lower bound for their result (theorem 5), they set it up following example 4.  Example 4 is interesting in this light: In that example we constructing a language L with s \\in L and an attention layer that recognizes s.  Thus, example 4 provides a particular encoding and a particular attention layer set up.  What they show then is that transformers of the simple variety they define can accept a language for which the nonemptiness problem is EXSPACE hard. \n\nWhy is this important?  Well because of the implication the authors draw from this proof---namely that proving properties about transformers is computationally intractable.  Perhaps they simply mean \"can be intractable\", in which case there is no problem.  But transformers typically don't have such complex encodings (we know because we make those encodings when we do ICL and pretraining) and typically they are used to solve much easier problems.  Thus transformers can have high complexity but that doesn't mean that they do.  IFor instance, suppose you use a very simple transformer to learn something like the induction head phenomenon of Olsson et al 2022.  The attention layer structure may be quite simple and it can be straightforward to prove equivalence with other transformers or other models.  Thus, theorem 5 doesn't entail that proving properties of transformers is necessarily intractable.  \n\nIt's also very unclear that transformers can actually learn the structure given in example 4 or the even more complex one that underpins theorem 5.  t will really depend on the task to which they are put.   What it does show, however, is that we don't have a tractable general method for proving properties for transformers.\n\nA possible problem has to do here with the encoding of large numbers.  Transformers can have difficulty in doing even simple tasks given with large number or high vector norm inputs, inputs much larger than those seen in training, as work on in context learning has shown (Naim and Asher 2025).  If the authors could comment on this, it would be much appreciated.\n\nMinor weaknesses:\nIt would help the reader to use the definition in Hao et al 2022 of these transformers as string accepters.  \n\ntypos: show matching upper bound on ---> show a matching upper bound on\n\nthe first or last ---> the first or last\n\nPlease explain the black triangle notation when you introduce it in the specification of the Attention operation.\n\nIn example 4, Q I don't believe is defined.\n\n\n\nOlsson, Catherine and Elhage, Nelson and Nanda, Neel and Joseph, Nicholas and DasSarma, Nova and Henighan, Tom and Mann, Ben and Askell, Amanda and Bai, Yuntao and Chen, Anna and others, arXiv:2209.11895, 2022\n\nNaim, Omar and Asher,Nicholas. Analyzing limits of icl https://arxiv.org/pdf/2502.03503, 2025", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: This decision has been updated in view of AC clarifying their decision.
Decision: Accept (Oral)