Pith. sign in

REVIEW 2 major objections 5 minor 1 cited by

As autoregressive language models, hard-attention transformers express exactly counter-free automata's weighted languages — and probabilistic use splits what Boolean results predict.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

T0 review · deepseek-v4-flash

2026-08-04 07:03 UTC pith:NNEIJL4P

load-bearing objection Genuinely new real-semiring results, but Thm 6.6(b)'s Boolean equivalence proof has a load-bearing bug: the H-operator makes the classifier accept nothing as written. the 2 major comments →

arxiv 2510.27118 v4 pith:NNEIJL4P submitted 2025-10-31 cs.CL

Probability Distributions Computed by Autoregressive Transformers

classification cs.CL MSC 68Q4568Q7003B44
keywords transformer language modelsexpressivityweighted languagescounter-free automatalinear temporal logicunique hard attentionautoregressive generationformal language theory
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Most theory treats transformers as accept/reject recognizers, but practical language models generate strings as probability distributions. This paper asks which such distributions unique-hard-attention transformers can express, and answers it exactly: as state encoders, these transformers are equivalent to linear temporal logic and counter-free deterministic automata. In the Boolean (true/false) setting, classifiers and autoregressive generators define the same weighted languages; in the real-valued (probabilistic) setting, autoregressive generation is strictly more expressive than classification, and equivalences with nondeterministic automata break. The result matters because it delineates what distributions this architectural family can and cannot generate, and shows that classifier-era expressivity results do not automatically transfer to language models.

Core claim

The paper proves that strictly-masked rightmost unique-hard-attention transformers (UHA Ts) — hard, future-masked, position-free attention — are exactly as expressive, as state encoders, as past linear temporal logic (LTL) and counter-free deterministic finite automata (cfDFAs). Consequently, as both classifiers and autoregressive next-symbol predictors, they define the same weighted languages. In the real semiring, LTL classifiers compute exactly the aperiodic step functions, which are strictly weaker than LTL autoregressors: the distribution (1/2 a)* is generatable but not classifiable, while (1a)* is classifiable but not generatable; and weighted counter-free nondeterministic automata def

What carries the argument

The state-encoder equivalence theorem (Theorem 6.1) is the engine: it rests on a finiteness lemma from prior work — every UHA T layer, at every position, outputs a vector from a fixed finite set, so a UHA T can be treated as a finite-state automaton — and then shows LTL formulas and cfDFAs encode exactly the same state sequences. The second piece is a pair of transformations on LTL formulas: a right-derivative operation that removes the final symbol from the language a formula defines, and a prefix operation that converts a formula into the language of all its prefixes. These mediate between classifier and autoregressive readings, giving the Boolean equivalence theorem and explaining why fra

Load-bearing premise

The entire chain of equivalences hangs on a previously established lemma that every unique-hard-attention layer outputs only finitely many distinct vectors per position; if that finiteness ever fails (e.g., under softmax attention or with position embeddings), the claimed equivalence to counter-free automata collapses.

What would settle it

Attempt to construct a strictly-masked rightmost unique-hard-attention autoregressor (with no position embeddings) that assigns positive probability to strings based on the parity of the number of a's; the counter-free barrier predicts no such construction exists, so any working example — or a trained model of that architecture that learns such a distribution — would disprove the paper's central equivalence.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Transformer language models in this class can only express distributions whose weights are counter-free; any distribution requiring unbounded counting (e.g., parity) is impossible regardless of training data or optimization.
  • For Boolean tasks, autoregression adds no expressivity to full LTL, but for the TL[H]/TL[Y] fragments tied to certain transformer variants, next-token prediction recognizes strictly more languages than classification, such as (ab)*.
  • In the probabilistic setting, expressivity depends on task framing: a normalized distribution can be generatable but not classifiable, and vice versa, so classifiers and language models of the same architecture are genuinely different devices.
  • Weighted nondeterministic counter-free automata outrun deterministic ones, meaning the deterministic limitation is real for distributions even within the counter-free class — a fact with no Boolean counterpart.
  • The prefix transformation can be exponential, and constructing it is conditionally intractable (P=PSPACE or P=NP barriers), so even where Boolean equivalence holds, converting a classifier into an autoregressor may be computationally expensive.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the finiteness lemma fails for practical attention (softmax, positional encodings), the counter-free characterization likely breaks; a testable prediction is that adding soft attention or position embeddings should let a transformer LM capture parity-like distributions that violate the theorems.
  • The classifier/autoregressor split suggests a design heuristic: prove expressivity results in the generative framing directly, rather than importing recognizer results, since even the Boolean case diverges for natural fragments.
  • The stutter-invariance criterion behind TL[H] gives a practical litmus test: if a language changes truth when a symbol is repeated, it is outside the class that TL[H]-equivalent transformer variants can generate.
  • One could empirically benchmark a strictly-masked hard-attention LM on (aab)* to see whether it fails exactly as Proposition 6.11 predicts, testing the boundary of what autoregression adds.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper studies expressivity of transformer language models in their practical use as autoregressive probabilistic generators, distinguishing Boolean vs. real semirings and classifiers vs. autoregressors. It defines strictly masked, rightmost unique-hard-attention transformers (UHA Ts) and proves/imports that they, past LTL, and counter-free DFAs define equivalent state encoders (Thm 6.1, App. A). On that basis it derives real-semiring characterizations: LTL classifiers are exactly aperiodic step functions, LTL/UHA T autoregressors are exactly cfDFA autoregressors, and weighted counter-free NFAs are strictly more expressive (Cor 6.2, Prop 6.3, Cor 6.4, Fact 6.5). In the Boolean semiring it claims LTL classifiers and autoregressors are equivalent (Thm 6.6), examines fragments showing that (ab)* is generatable but not classifiable by TL[H] or TL[Y] (Prop 6.10), and proves that (aab)* is not definable by TL[H] classifiers or autoregressors (Prop 6.11). The paper also connects the framework to counting logics and C-RASP in Sec. 6.3.3.

Significance. This paper makes a useful conceptual contribution: it separates classifier and autoregressor expressivity and Boolean vs. real weights, which is directly relevant to how transformers are actually deployed. The framework is clean, and several constructions are explicit and checkable: the Brzozowski-derivative style next transformation (Lem. 6.7), the prefix transformation via the subset DFA (Lem. 6.8), the conditional lower bounds (Prop 6.9), and the bigram/stutter-invariance argument for (aab)* (App. D). If the main results hold, the equivalences for real autoregressors (Cor 6.2), the separation from weighted cfNFAs (Fact 6.5), and the fragment-level separations in Sec. 6.3.2 would be valuable and would clarify when classifier-theoretic expressivity results transfer to language-model practice. However, the submitted proof of the central Boolean equivalence Thm 6.6(b) has serious flaws that are load-bearing for the Boolean-autoregressor side of Fig. 1, so the paper cannot be accepted as is.

major comments (2)
  1. [Appendix B.3, proof of Thm 6.6(b)] The construction φ′ = H(∨_{σ∈Σ∪{EOS}} (Yφ_σ)∧σ) is invalid under the H-semantics of Def. 5.3. Hψ at position i requires ψ at every j≤i, including j=0. At j=0 the disjunction is false: Yφ_σ is false for every σ by (11e) because i>0 fails, no σ∈Σ labels BOS, and EOS is not a symbol occurring in the string. Hence H(...) is false at every position and the classifier accepts no strings. Moreover, even if the BOS off-by-one is repaired, the σ=EOS disjunct is only evaluated where w_i=EOS, which never occurs; the required final condition a(state_n)(EOS)=⊤ is never tested. The theorem may be recoverable with a BOS guard and a final φ_EOS conjunct, but as written the proof does not support it.
  2. [Appendix B.3, same proof] The definition φ_σ = ∧_{h∈B^m} (φ_h ↔ a(h)(σ)) does not express “the current state predicts σ.” For the unique actual state h*, each term with h≠h* evaluates to false ↔ a(h)(σ), i.e. ¬a(h)(σ), so φ_σ is true only when h* is the unique state in the entire automaton with a(h*)(σ)=⊤. If two states both predict σ, φ_σ is false in both. The intended formula is ∨_{h : a(h)(σ)=⊤} φ_h. This is an independent error and also breaks the proof of Thm 6.6(b).
minor comments (5)
  1. [Sec. 6.2] The numbering collides: Theorem 6.1 appears in Sec. 6.1, and then Definition 6.1 appears in Sec. 6.2. Please renumber to avoid confusion.
  2. [Sec. 2] Typo: 'charcaterization' should be 'characterization' in the related-work discussion.
  3. [Sec. 5.2] In the grammar, 'BOSBeginning of string' is a formatting typo; it should be 'BOS — Beginning of string'.
  4. [Sec. 6.1 / App. A] Thm 6.1 relies on the finite-output-set lemma of Yang et al. (2024, Lemma 22) and on the classical LTL↔counter-free correspondence. These are published results, but since the theorem is load-bearing, please state the exact scope (unique-hard attention, rightmost, strict masking, no position embeddings) and cite the finite-trace LTL correspondence (e.g., De Giacomo–Vardi) alongside Schützenberger/McNaughton–Papert/Kamp.
  5. [Fig. 1] The legend 'Key: strict inclusion, equivalence.̸=incomparable.' is garbled; please clean up the formatting.

Circularity Check

0 steps flagged

No significant circularity: the imported UHA T/LTL/cfDFA equivalences are published, proof-bearing results, and the paper's new weighted/autoregressive consequences follow by construction rather than by fitting.

full rationale

The derivation chain starts from Theorem 6.1, which asserts state-encoder equivalence. Its proof imports the finiteness of UHA T states and the per-state LTL translation from Yang et al. (2024, Lemma 22, Thms 1-4, 25), and the LTL/cfDFA correspondence from Schutzenberger, McNaughton-Papert, and Kamp. The Yang et al. results are published, proof-bearing, and parameter-free under the paper's stated architecture (unique-hard attention, strict masking, no position embeddings); they do not assume the present theorem. Under the review rules, such citations are independent support, so the authors' overlap does not make the argument circular. Corollary 6.2 and the real/Boolean characterizations are direct logical consequences of state-encoder equivalence plus output functions, not fitted predictions. No parameter is fitted and then renamed a prediction; no uniqueness theorem is invoked to forbid alternatives; no ansatz is smuggled in via citation. One non-circular correctness concern: the Appendix B.3 proof of Thm 6.6(b) defines phi' = H(vee_{sigma in Sigma union {EOS}} (Y phi_sigma) and sigma), but H ranges over all j <= i including j=0, where the disjunct is false and no sigma in Sigma or EOS holds, so the classifier as written accepts no strings and the final EOS check is not enforced. This is a proof gap, not a circularity, and does not raise the circularity score; a repair (e.g., guarding BOS and conjoining phi_EOS at the end) appears plausible.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 0 invented entities

No fitted or hand-chosen numerical parameters exist in this paper; it is pure theory. The central claims rest on (a) the hard-attention finiteness lemma and the UHA T/LTL equivalence from the authors' own published prior work, (b) standard classical results (Schützenberger, McNaughton–Papert, Kamp, Peled–Wilke, Fionda–Greco, Mohri), and (c) the paper's framework choices about what 'autoregressor' and 'counter-free NFA' mean. No new entities (forces, particles, dimensions) are postulated; the novel objects are roles (classifier vs autoregressor) defined over existing formalisms.

axioms (6)
  • domain assumption UHA T state outputs at every position come from a finite set Q ⊆ R^d; UHA Ts ↔ LTL formulas (Yang et al., 2024, Lem. 22, Thms 1–4, 25)
    Imported from the authors' prior NeurIPS paper to prove Thm 6.1 (App. A); not re-derived here; holds only for hard (not softmax) attention without position embeddings.
  • standard math Classical equivalence: counter-free automata = star-free = LTL (Schützenberger 1965; McNaughton–Papert 1971; Kamp 1968)
    Used in the Thm 6.1 proof (App. A) to connect cfDFAs and LTL; assumed to hold in the paper's finite-trace, BOS-position semantics.
  • standard math TL[H] (= TL[P]) formulas define stutter-invariant languages (Peled–Wilke 1997)
    Load-bearing in Prop 6.10 and in the Appendix D proof of Prop 6.11.
  • standard math Satisfiability of TL[H,Y] is PSPACE-complete; of TL[H] and TL[Y], NP-complete; evaluating a fixed formula on a fixed string is polynomial (Fionda–Greco 2016; De Giacomo–Vardi 2013)
    Basis of the conditional lower bounds in Prop 6.9.
  • domain assumption A weighted automaton is determinizable iff its sibling states are twins (Mohri 1997); the Fig. 2c automaton is counter-free but not determinizable
    Underpins Fact 6.5 (App. C); the paper's counter-free-NFA definition (Def C.2) is one of several non-equivalent analogues (Droste–Gastin 2008), a choice the authors explicitly flag.
  • domain assumption Autoregressor expressivity is defined via normalized distributions (Def 4.2: every conditional sum equals 1; no dead ends or endless loops)
    Framework choice that excludes non-normalized weighted languages from 'expressible by an LM' (used in Cor 6.4).

pith-pipeline@v1.3.0-alltime-deepseek · 15557 in / 31026 out tokens · 266675 ms · 2026-08-04T07:03:04.491390+00:00 · methodology

0 comments
read the original abstract

Most expressivity results for transformers treat them as language recognizers -- devices that accept or reject strings -- rather than as they are used in practice: as language models that generate strings autoregressively and probabilistically. We characterize the probability distributions that transformer language models can express. We show that making transformer language recognizers autoregressive can sometimes increase their expressivity, and that making them probabilistic can break equivalences that hold in the non-probabilistic case. Our overall contribution is to tease apart what functions transformers are capable of expressing in their most common use case as language models.

Figures

Figures reproduced from arXiv: 2510.27118 by Andy Yang, Anej Svete, Anthony Widjaja Lin, David Chiang, Jiaoda Li, Jonathan Rawski, Ryan Cotterell.

Figure 1
Figure 1. Figure 1: In the Boolean semiring, equivalences from the literature (Yang et al., 2024; Jerad et al., [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: (a) A DFA that is counter-free (with k = 2). (b) A DFA that is not counter-free, because for all k, the strings a k and a k+1 have opposite actions. (c) A counter-free weighted NFA that has no equivalent weighted DFA (Fact 6.5). 5.1 FINITE AUTOMATA Definition 5.1 (Deterministic finite automaton). A deterministic finite automaton (DFA) is a tuple M = (Σ, Q, δ, ι), where • Σ is an alphabet • Q is a finite se… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Surprisal Theory is Tautological (without Rational Grounding)

    cs.CL 2026-07 conditional novelty 6.0

    Unconstrained surprisal theory is a tautology: for any non-negative difficulty measure, a language model exists whose surprisal matches it affinely.

Reference graph

Works this paper leans on

24 extracted references · 6 canonical work pages · cited by 1 Pith paper

  1. [1]

    On the ability and limitations of Transformers to recognize formal languages

    Satwik Bhattamishra, Kabir Ahuja, and Navin Goyal. On the ability and limitations of Transformers to recognize formal languages. InProceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 7096–7116,

  2. [2]

    Proof.By induction on the length ofw

    Claim B.2.For anyw,δ(ι,w) ={χ∈cl(ϕ)|w|=χ}. Proof.By induction on the length ofw. Base case:δ(ι, ϵ) =ι={χ|ϵ|=χ}. Inductive step: Assume thatδ(ι,w) ={χ|w|=χ}= Ψ. Then δ(ι,w) =δ(δ(ι,w), σ) =δ(Ψ, σ) ={χ|Ψ σ − →χ} ={χ|wσ|=χ}. Claim B.3.M ϕ defines the same language asϕ. Proof.δ(ι,w)∈Fif and only ifϕ∈ {χ|w|=χ}if and only ifw|=ϕ. 14 Preprint Then make every co-a...

  3. [6]

    Manfred Droste and Dietrich Kuske

    doi:10.4230/LIPICS.MFCS.2019.76. Manfred Droste and Dietrich Kuske. Weighted automata. In Jean- ´Eric Pin, editor,Handbook of Automata Theory, pages 113–150. European Mathematical Society Publishing House, Z ¨urich, Switzerland,

  4. [12]

    org/abs/2505.23623

    URLhttps://arxiv. org/abs/2505.23623. To appear. Eleni Mandrali and George Rahonis. Characterizations of weighted first-order logics over semir- ings. InAlgebraic Informatics: 5th International Conference (CAI), pages 247–259,

  5. [16]

    doi:10.1016/S0020- 0190(97)00133-6. M. P. Sch¨utzenberger. On finite monoids having only trivial subgroups.Information and Control, 8 (2):190–194,

  6. [19]

    Andy Yang and David Chiang

    doi:10.18653/v1/2024.naacl- long.381. Andy Yang and David Chiang. Counting like transformers: Compiling temporal counting logic into softmax transformers. InProceedings of the First Conference on Language Modeling (CoLM),

  7. [20]

    Andy Yang, Micha ¨el Cadilhac, and David Chiang

    URLhttps://proceedings.neurips.cc/paper files/paper/ 2024/hash/13d7f172259b11b230cc5da8768abc5f-Abstract-Conference.html. Andy Yang, Micha ¨el Cadilhac, and David Chiang. Knee-deep in C-RASP: A transformer depth hierarchy. InAdvances in Neural Information Processing Systems (NeurIPS),

  8. [21]

    To appear

    URLhttps: //arxiv.org/abs/2506.16055. To appear. Shunyu Yao, Binghui Peng, Christos Papadimitriou, and Karthik Narasimhan. Self-attention networks can process bounded hierarchical languages. InProceedings of the 59th An- nual Meeting of the Association for Computational Linguistics and the 11th International Joint Conference on Natural Language Processing...

  9. [22]

    11 Preprint A EQUIVALENCE OFSTATEENCODERS Theorem 6.1.UHA Ts,LTL, and cfDFAs define equivalent state encoders

    doi:10.18653/v1/2021.acl-long.292. 11 Preprint A EQUIVALENCE OFSTATEENCODERS Theorem 6.1.UHA Ts,LTL, and cfDFAs define equivalent state encoders. Proof.First we show the equivalence of state sequences defined byUHA TsandLTL, and then equiv- alence ofLTLand cfDFAs. The essential observation (Yang et al., 2024, Lemma

  10. [23]

    So we can think of aUHA Tas a functionT: Σ ∗ →Q ∗

    is that the output at every position of every UHA Tlayer comes from a finite setQ⊆R d. So we can think of aUHA Tas a functionT: Σ ∗ →Q ∗. For eachq∈Q, we can construct anLTLformulaϕ q such thatT(w) i =q⇐ ⇒w, i|=ϕ q (Yang et al., 2024, Theorems 2, 4). So there exists a tuple ofLTLformulas(ϕ q)q∈Q that defines a state encoder equivalent toT. Note that the s...

  11. [25]

    Then, to prove that(aab) ∗ is not definable inTL[H,Y]withY-depth 1, suppose it is definable by ϕ

    noy(Hψ) =H(noy(ψ))noy(Y(Hψ)) =H(noy(Yψ)) noy(σ) = _ σ′∈Σ∪{BOS} (σ′, σ)noy(Yσ) = _ σ′∈Σ∪{EOS} (σ, σ′) noy(BOS) =BOSnoy(YBOS) = _ σ′∈Σ∪{EOS} (BOS, σ′). Then, to prove that(aab) ∗ is not definable inTL[H,Y]withY-depth 1, suppose it is definable by ϕ. By Lem. D.1, there is a formula noy(ϕ)ofTL[H]such that (BOS, a)·(a, a)·(a, b)·(b,EOS)∈ L(noy(ϕ))∩Bigram(Σ ∗)....

  12. [1964]

    Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova

    doi:10.1145/321239.321249. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: Pre-training of deep bidirectional Transformers for language understanding. InProceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (NAACL HLT), pages 4171–4186,

  13. [1965]

    Lena Strobl, William Merrill, Gail Weiss, David Chiang, and Dana Angluin

    doi:10.1016/S0019-9958(65)90108-7. Lena Strobl, William Merrill, Gail Weiss, David Chiang, and Dana Angluin. What formal lan- guages can transformers express? A survey.Transactions of the Association for Computational Linguistics, 12:543–561,

  14. [1968]

    Jiaoda Li and Ryan Cotterell

    URLhttps://www.proquest.com/docview/302320357. Jiaoda Li and Ryan Cotterell. Characterizing the expressivity of transformer language models. In Advances in Neural Information Processing Systems (NeurIPS),

  15. [1997]

    Doron Peled and Thomas Wilke

    URLhttps://aclanthology.org/J97-2003/. Doron Peled and Thomas Wilke. Stutter-invariant temporal properties are expressible without the next-time operator.Information Processing Letters, 63(5):243–246,

  16. [2008]

    Manfred Droste and Paul Gastin

    doi:10.1007/s00224-007- 9064-z. Manfred Droste and Paul Gastin. Aperiodic weighted automata and weighted first-order logic. In Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science,

  17. [2013]

    doi:10.1007/978-3-642-40663-8

  18. [2015]

    Robert McNaughton and Seymour Papert.Counter-Free Automata

    doi:10.14232/actacyb.22.2.2015.1. Robert McNaughton and Seymour Papert.Counter-Free Automata. Number 65 in M.I.T. Press Research Monographs. M.I.T. Press,

  19. [2016]

    Giuseppe De Giacomo and Moshe Y

    doi:10.1609/aaai.v30i1.10104. Giuseppe De Giacomo and Moshe Y . Vardi. Linear temporal logic and linear dynamic logic on finite traces. InProceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI), pages 854–860,

  20. [2019]

    Manfred Droste and Paul Gastin

    doi:10.18653/v1/N19-1423. Manfred Droste and Paul Gastin. On aperiodic and star-free formal power series in partially com- muting variables.Theory of Computing Systems, 42(4):608–631,

  21. [2020]

    Janusz A

    doi:10.18653/v1/2020.emnlp- main.576. Janusz A. Brzozowski. Derivatives of regular expressions.Journal of the Association for Computing Machinery, 11(4):481–494, October

  22. [2021]

    Valeria Fionda and Gianluigi Greco

    doi:10.4171/AUTOMATA-1/4. Valeria Fionda and Gianluigi Greco. The complexity of LTL on finite traces: Hard and easy frag- ments. InProceedings of the AAAI Conference on Artificial Intelligence, volume 30, pages 971– 977,

  23. [2024]

    Anej Svete and Ryan Cotterell

    doi:10.1162/tacl a 00663. Anej Svete and Ryan Cotterell. Transformers can representn-gram language models. InProceedings of the 2024 Conference of the North American Chapter of the Association for Computational Lin- guistics: Human Language Technologies, pages 6845–6881,

  24. [2025]

    Johan Anthony Willem Kamp.Tense Logic and the Theory of Linear Order

    doi:10.18653/v1/2025.acl-short.76. Johan Anthony Willem Kamp.Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles,