Transformers are Inherently Succinct
Peer-reviewed conference; ICLR 2026 Outstanding Paper, 2026 · paper · AI and machine learning
Studies how compactly transformers can describe languages compared with other formalisms. It proves fixed-precision transformers can be exponentially more succinct than linear temporal logic and recurrent networks, and doubly exponentially more than finite automata, making verification problems EXPSPACE-complete.
Checked: PDF from proceedings.iclr.cc, fetched 5 Oct 2026. Page numbers are those of that PDF.
6 findings
Substance Appendix A.2, Gadget B, Eq. (14e): "B(i) := ▶j [j < i, Q#(j) ∧ ¬B1→0(j) ∧ ¬B+1(j)] 0 : B1→0(i) ∧ B+1(i)". The default joins two mutually exclusive predicates with ∧, so B(L)=0 on every input. This contradicts "Then B(L) = 1 iff the binary blocks count up correctly" and the claim L(P_I) = L_I. The intended connective appears to be ∨.
- p. 15 App. A.2, Gadget B, Eq. (14e)
B(i) := ▶j [j < i, Q#(j) ∧¬B1→0(j) ∧¬B+1(j)] 0 : B1→0(i) ∧B+1(i)
- p. 15 Appendix A.2, Equation (14e), default value
B1→0(i) ∧ B+1(i)
- p. 17 Appendix A.2, concluding correctness claim
L(PI) = LI
- p. 15 App. A.2, Gadget B, Eq. (14e)
0 : B1→0(i) ∧B+1(i)
Only the authors can say what is right here.
Judge's note: Checked Eqs. (14c)–(14e) on the page 15 image; the final connective is clearly ∧. By (14d), whether as value (⋀¬Bk(i)∧Bk(j)) or as default (⋀¬Bk(i)), B1→0(i)=1 requires every Bk(i)=0. By (14c), B+1(i)=1 requires some Bk(i)=1, and its default is 0. So B1→0(i)∧B+1(i) is always 0. Eq. (14e) returns 0 whether an earlier bad # is found or the default is taken, so B(L)=0, Y(L)=0, and the program accepts nothing, even for an encoding of a valid tiling. This contradicts the page 15 claim and the page 17 claim "L(PI) = LI" that underpins Lemma 8. The attention score uses ¬B1→0(j)∧¬B+1(j), i.e. 'neither holds', which points to a disjunction as the intended default. The construction in the proof is wrong as printed, so the proof of Lemma 8 does not go through as written (S1). The fix (∧→∨) appears straightforward.
Second check: another model agreed
Report a problem with this finding
Wording Introduction (p.2) says of EXPSPACE-completeness: "Under standard complexity-theoretic assumptions, this means that no algorithm can solve the problem in less than double exponential time." Under the standard assumption EXP ≠ EXPSPACE, EXPSPACE-completeness rules out only exponential-time algorithms. It gives no doubly-exponential time lower bound.
- p. 2 Introduction, paragraph 'This paper offers a formal result', last sentence
Under standard complexity-theoretic assumptions, this means that no algorithm can solve the problem in less than double exponential time.
- p. 2 Introduction, para. after 'EXPSPACE-complete'
no algorithm can solve the problem in less than double exponential time
Only the authors can say what is right here.
Judge's note: Read on p.2 (crop and full page). Thm. 4 states EXPSPACE-completeness. EXPSPACE ⊆ 2EXP gives doubly-exponential time only as an upper bound. The standard assumption EXP ≠ EXPSPACE excludes time 2^poly, not every time bound below 2^(2^poly). The abstract and Sec. 6 phrase this more cautiously. The sentence states more than the result supports. The authors should decide the wording (e.g. 'more than exponential time').
Second check: another model agreed
Report a problem with this finding
Wording Sec. 2.5 (p.5): "together they pin the gap: C(1) is f-more succinct and has g-bounded expansion over C(2) exactly when the size gap is at least f on a witness family and at most g uniformly." Def. 2 bounds |R(2)| from below by f(|R(1)|). Def. 3 bounds |R(1)| from above by g(|R(2)|). Neither gives an upper bound on how much larger R(2) can be, so the two do not sandwich one gap.
- p. 5 Paragraph after Def. 3
C(1) is f-more succinct and has g-bounded expansion over C(2) exactly when the size gap is at least f on a witness family and at most g uniformly
Only the authors can say what is right here.
Judge's note: Read Def. 2 and Def. 3 on the p.5 page image. Def. 2: |R_n(2)| ≥ f(|R_n(1)|) on a witness family. Def. 3: every R(2) has an R(1) with |R(1)| ≤ g(|R(2)|). Both say that C(1) is not much larger than C(2); they bound ratios in opposite directions. So 'at least f … and at most g' on a single gap does not follow from these definitions. Bounding the same gap from above would need C(2) to have bounded expansion over C(1). The definitions themselves are fine; the gloss misdescribes them.
Second check: another model agreed
Report a problem with this finding
Wording Example 2: Eq. (7) treats C1 as the least significant bit (bits r<k go 1→0, bit k goes 0→1, bits r>k unchanged), yet the text sets "Ck(i) = b^i_k and Ck(j) = b^j_k for all k ∈ [4]" with the words written most significant bit first ("0000a1#0001a2#0010a3"), so the predicate does not check "incremented by 1" as claimed.
- p. 6 Example 2, Eq. (7) and following text
We assume that we already defined Ck(i) = bi k and Ck(j) = bj k for all k ∈[4]
- p. 6 Example 2, specified counter sequence
0000a1#0001a2#0010a3
- p. 6 Equation (7) and the coordinate identification immediately below
Ck(i) = bⁱk and Ck(j) = bʲk
- p. 6 Example 2, Eq. (7) and following text
Ck(i) = bi k and Ck(j) = bj k for all k ∈ [4]
Only the authors can say what is right here.
Judge's note: Checked page 6 image. In Eq. (7), disjunct k requires ¬C_r(i)∧C_r(j) for r<k, C_k(i)∧¬C_k(j), and C_r(i)↔C_r(j) for r>k. That is the increment rule when index 1 is the least significant bit. My own check of the step 0000→0001 with C_k=b_k: C(j)=(0,0,0,0), C(i)=(0,0,0,1). For k=1,2,3 the factor C_k(i) is 0. For k=4 the factor for r=1 needs C_1(j)=1, which fails. So the value is 0 for a correct increment. In the other direction, 0000→1000 satisfies the k=1 disjunct. The appendix version (14a–14c, page 15) is consistent, because there B1 is read as the bit immediately left of the position, i.e. the least significant bit. Reversing the index (C_k = b_{5−k}) would fix the example. This is an illustrative example and the main results do not rely on it, so it is a faulty step and the stated results stand (S3).
Second check: another model agreed
Report a problem with this finding
Wording Appendix A.4, proof of Proposition 12, Part 2: the claim of "integer weights and a bias each of bit-length at most log D (the entries of C scaled by D)" does not hold in general. D is the LCM of the denominators only, so a coefficient p/q scaled by D is p·D/q, whose bit-length also depends on p. The bound "at most 2R · 2^{log D}" therefore does not follow as stated.
- p. 18 Appendix A.4, Part 2: bounding the numerator
with integer weights and a bias each of bit-length at most log D
- p. 18 Appendix A.4, ensuing magnitude bound
at most 2R · 2log D
Only the authors can say what is right here.
Judge's note: Checked page 18 image. Part 1 defines D as the LCM of the denominators of the rationals in the description of T. It sets no limit on the numerators. Scaling a coefficient p/q by D gives p·(D/q), which can have up to about |T| + log D bits, not log D. My check of the reviewer's counterexample: emb(a)=1/2 and C(x)=16x give D=2, so log D = 1, but the scaled coefficient is 16·2 = 32, which needs 6 bits. The per-layer bit-length step is therefore wrong as printed. Proposition 12 still holds: the per-layer increase becomes log R + |T| + log D + O(1), which over at most |T| layers is still polynomial. So the step is faulty and the stated result stands (S3).
Second check: another model agreed
Report a problem with this finding
Wording Proof of Prop. 12, Part 2 (p.18): "integer weights and a bias each of bit-length at most log D (the entries of C scaled by D)". Scaling an entry p/q (q | D) by D gives p·(D/q), whose bit-length can reach b + log D, not log D. So the per-layer factor 2R·2^{log D} and the additive increase log R + log D + O(1) do not hold as printed.
- p. 18 App. A.4, Part 2: bounding the numerator
integer weights and a bias each of bit-length at most log D (the entries of C scaled by D)
Only the authors can say what is right here.
Judge's note: Reworked from the p.18 image. Counterexample: take all coefficients as integers, so D = 1 and log D = 0, with a weight of 5. The scaled weight 5 has bit-length 3 > 0, and the output magnitude 5x exceeds the claimed 2R·2^0·x = 2x for R = 1. The correct per-layer increase is O(log R + |T| + log D), where b ≤ |T|. Iterated over at most |T| layers, this is still polynomial in |T|, so Prop. 12 stands. The step is faulty but the result is not.
Second check: another model agreed
Report a problem with this finding
9 minor (typos and the like; most checked by the judge only)
Wording End of proof of Lemma 8 (p.17): "Each gadget uses O(N) predicates of size polynomial in N and |T|". Gadget C defines one predicate Tt "for all t ∈ T" (15a), so it has |T|+1 predicates, which is O(N+|T|) rather than O(N).
- p. 17 End of proof of Lemma 8
Each gadget uses O(N) predicates of size polynomial in N and |T|
- p. 16 Gadget C, Eq. (15a)
for all t ∈T
Judge's note: Checked (15a) on p.16, which defines Tt for every t ∈ T, and (15b), which defines C. The count O(N) holds only if |T| = O(N), and that is not assumed. The conclusion that |P_I| is polynomial in N and |T| is unaffected.
Second check: another model agreed
Report a problem with this finding
Wording App. A.4 says "a single score value would have bit-length quadratic in its inputs" and "its quadratic bit-length", but a dot product of rationals has bit-length at most linear in the total bit-length of its inputs.
- p. 19 App. A.4, note after Part 2
a single score value would have bit-length quadratic in its inputs
Only the authors can say what is right here.
Judge's note: Page 19 image, top paragraph. My own working: for rationals p1/q1 and p2/q2, the product has numerator and denominator bit-lengths at most the sums of the inputs' bit-lengths. A sum of R such products over a common denominator has bit-length at most about the total input bit-length plus log R. That bound is linear, not quadratic, in the input size. The authors may mean the score is a degree-2 polynomial of its inputs, or may intend 'quadratic' only as a loose upper bound. The step plays no role in the argument, since the score is never forwarded, so the stated result (polynomial bit-length) stands. This is a wording issue for the authors to clarify.
Second check: another model agreed
Report a problem with this finding
Typo Example 2 (p.6): "We show how to construct a B-RASP programs that". The singular article does not agree with the plural noun.
- p. 6 Example 2
We show how to construct a B-RASP programs that
Judge's note: The p.6 page image shows 'a B-RASP programs'.
Second check: none (judge only)
Report a problem with this finding
Typo Sec. 3 (p.6): "with an 2^{O(N)}-sized tape". The article should be 'a', since '2' is read 'two'.
- p. 6 Section 3, first paragraph
with an 2O(N)-sized tape
Judge's note: The p.6 page image shows 'an 2^{O(N)}-sized tape'. This is cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo Lemma 9 (p.7, restated on p.17): "S(j) is a Boolean combinations of P1(j), ..., Pt(j)". This should read 'a Boolean combination'.
- p. 7 Lemma 9 statement
S(j) is a Boolean combinations of
- p. 17 Lemma 9 restated in App. A.3
S(j) is a Boolean combinations of
Judge's note: Both page images (p.7 and the restatement on p.17) show 'a Boolean combinations'.
Second check: none (judge only)
Report a problem with this finding
Typo Footnote 8 (p.8): "For instance, Li and Cotterell’s (2026) demonstration that LTL[P] can not accept {a, b}∗a with EOS-padding, but can without the padding." The sentence is a noun phrase with no main verb.
- p. 8 Footnote 8
For instance, Li and Cotterell’s (2026) demonstration that LTL[P] can not accept {a, b}∗a with EOS-padding, but can without the padding.
Judge's note: The footnote on the p.8 image matches the quote, and the sentence has no predicate. This is a copyedit fragment.
Second check: none (judge only)
Report a problem with this finding
Typo Proof of Thm. 15 (p.9): "gives |φn| ≥ c1·2^{c′ |Tn|^{1/d}} for c′_2 = c2/c0^{1/d}". The constant is written c′ in the bound but defined (and later used in f(m)) as c′_2.
- p. 9 Proof of Thm. 15, first paragraph
gives |φn| ≥c12c′ |Tn|1/d for c′
- p. 9 Proof of Thm. 15, first paragraph
|φn| ≥c12c′ |Tn|1/d for c′ 2 = c2/c1/d 0
Judge's note: The p.9 image shows the exponent with c′ and no subscript, then the definition c′_2 = c2/c0^{1/d} and f(m) = c1·2^{c′_2 m^{1/d}}. The derivation itself is correct: n ≥ (|Tn|/c0)^{1/d}. Only the symbol is inconsistent.
Second check: none (judge only)
Report a problem with this finding
Typo App. A.3 (p.17): "¬(¬Rk(i) ∧ ¬(Rℓ(i))." The outer '¬(' is never closed.
- p. 17 App. A.3, position-wise case
¬(¬Rk(i) ∧¬(Rℓ(i))
Judge's note: The p.17 crop shows '¬(¬R_k(i) ∧ ¬(R_ℓ(i)).'. Apart from the argument parentheses, two parentheses are opened and one is closed, so the outer one is left open.
Second check: none (judge only)
Report a problem with this finding
Typo Proof of Prop. 13 (App. A.5) types the score function as "a score function S: ℚ^{2R} → ℚ^R", but by Eq. (2) S(v_n, v_m) = ⟨A(v_n), B(v_m)⟩ is a scalar, and (26)–(28) compare scores with <, ≥, >; the codomain should be ℚ.
- p. 19 App. A.5, attention with strict masking
a score function S: Q2R →QR, we let
- p. 19 App. A.5, 'Inductive step—attention with strict masking'
a score function S: Q2R →QR
Judge's note: Checked page 19 image: the codomain is printed as ℚ^R (superscript visible), so this is not an extraction artefact. Eq. (2) on p.~4 (text layer, line 209–211) defines the score as a dot product, which is a single rational. Eqs. (26) and (28) order score values (S(u,b) < S(u,a), S(u,b) ≥ S(u,a), S(u,b) > S(u,a)), and that needs a scalar codomain. The intended meaning is clear and the construction is unaffected, so this is a notational slip: minor, with an evident fix.
Second check: none (judge only)