{"id":"094f7e8b-809b-40cb-9e1c-ff0729011b86","arxiv_id":"2510.27118","paper_version":4,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Autoregressive hard-attention transformers express exactly the weighted languages of counter-free DFAs, and probabilistic generation is strictly stronger than Boolean classification in some fragments.","lead":"This paper pinpoints which probability distributions transformer language models can express, treating them as autoregressive generators of the next symbol rather than as accept/reject classifiers. It shows that making transformers probabilistic and autoregressive can add power and can break equivalences that hold for Boolean recognizers.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Thm 6.6(b) construction is invalid as written: the H-operator includes position 0, where the disjunct is false, so the classifier defines the empty language; the EOS check is never evaluated.","rationale":"The paper's central contribution is a map of transformer-based weighted languages, with Thm 6.6 as the central bridge between Boolean classifiers and autoregressors. The proof of 6.6(b) as written is internally inconsistent with the paper's own semantics: H quantifies over position 0, where the disjunct is false, making the constructed classifier identically empty; and the EOS transition is never checked. This is not a matter of outside consensus; the construction fails under the paper's definitions. The theorem may be repairable, but the submitted proof does not support it. The reader's weakest_assumption focused on the imported finiteness lemma; while that is also a genuine dependency, the proof bug is more immediately load-bearing because it is an internal defect. I agree with the reader's CONDITIONAL verdict: the defect is concrete yet likely fixable, so the paper should not be rejected outright but the proof must be corrected. Other parts (6.6(a), and real-semiring Cor 6.4 with an easy normalization patch) appear sound on inspection.","tokens_in":16142,"tokens_out":9303,"duration_ms":92506,"concrete_test":"Instantiate the proof of Thm 6.6(b) with the Boolean TL[∅] autoregressor for L={a}: state after ε predicts a; state after a predicts EOS. Construct φ' from the recipe in §B.3. Evaluate C(w) for w=a under Def 5.3: at position 0 the inner disjunction is false, so H(inner) is false at position 1, so C rejects a. Equivalently, compute φ' at the initial position of any string; because H includes j=0, C is identically false. If the authors replace φ' with a corrected formula, re-check that it accepts a and rejects aa.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The proof of Thm 6.6(b) in Appendix B.3 does not establish that every TL[O] Boolean autoregressor is equivalent to a TL[O∪{Y,H}] classifier. As written, define φ' = H(∨_{σ∈Σ∪{EOS}} (Yφ_σ)∧σ). Under Def 5.3, Hψ at position i requires ψ true at every j≤i, including j=0. At j=0, Yφ_σ is false for every σ because Yϕ requires i>0, and no σ∈Σ is true at BOS; EOS is not in Σ. Hence the inner disjunction is false at position 0, so H(...) is false at every position, and the classifier accepts nothing. Moreover, even if one ignored the BOS off-by-one, the disjunction never tests φ_EOS at the end of the string, because σ ranges over symbols that occur at positions 1..|w|, and EOS never occurs there; the required final EOS prediction a(state_n)(EOS) is not enforced. Thus the claimed Boolean classifier/autoregressor equivalence (Thm 6.6, and hence the Boolean-autoregressor UHA T side of Fig. 1) is unsupported by the submitted proof. The flaw is in the proof, not necessarily the theorem — a repair such as adding BOS to the H-guard and conjoining φ_EOS seems plausible — but until that repair is written, the central equivalence should be treated as unproved.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":16424,"tokens_out":11486,"duration_ms":134744,"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":[{"comment":"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.","section":"Appendix B.3, proof of Thm 6.6(b)"},{"comment":"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).","section":"Appendix B.3, same proof"}],"minor_comments":[{"comment":"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.","section":"Sec. 6.2"},{"comment":"Typo: 'charcaterization' should be 'characterization' in the related-work discussion.","section":"Sec. 2"},{"comment":"In the grammar, 'BOSBeginning of string' is a formatting typo; it should be 'BOS — Beginning of string'.","section":"Sec. 5.2"},{"comment":"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.","section":"Sec. 6.1 / App. A"},{"comment":"The legend 'Key: strict inclusion, equivalence.̸=incomparable.' is garbled; please clean up the formatting.","section":"Fig. 1"}],"recommendation":"major_revision","confidential_remarks":"The flaw in Thm 6.6(b) is in the proof, not necessarily the theorem: a BOS guard and a final φ_EOS conjunct appear to repair the H construction, and a disjunctive definition of φ_σ repairs the state-prediction formula. I therefore recommend major revision rather than rejection. The authors should also re-check all corollaries that depend on Thm 6.6, since the current Fig. 1 Boolean-autoregressor column is unsupported by the submitted proof. The imported finiteness lemma is acceptable given the stated model class, but it should be foregrounded as a scope condition."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's my take. The paper gives a genuinely new framework for asking what transformer language models can express — separating classifiers from autoregressors and Boolean from real-weighted computation — and it produces real results in the real-semiring setting: LTL classifiers are the aperiodic step functions, real LTL autoregressors are strictly stronger, and weighted counter-free NFAs outrun cfDFA autoregressors. The explanation of the Yang et al. depth discrepancy via the absence of 'yesterday' is a nice payoff. The constructions for next/prefix via Brzozowski derivatives and the subset DFA check out, and the proof of Prop 6.11 via the bigram/stutter trick is clean. I also think the framework itself is useful for future work.\n\nBut there is a load-bearing flaw in the Boolean section. The proof of Thm 6.6(b) in Appendix B.3 defines φ' = H(∨_{σ∈Σ∪{EOS}} (Yφ_σ)∧σ). Under the paper's own semantics (Def 5.3), Hψ at position i requires ψ true at every j ≤ i, including j = 0. At position 0, Yφ_σ is false for every σ, and no σ ∈ Σ is true at BOS; EOS is not in Σ by stipulation. So the disjunction is false at position 0, H(...) is false at every position, and the classifier accepts nothing. Even if you ignored that off-by-one, the disjunction never tests φ_EOS at the end of the string, because σ ranges over symbols that occur at positions 1..|w| and EOS never occurs there. So the required final EOS check is not enforced. Thm 6.6(b) — and with it the Boolean-autoregressor side of Fig. 1 — is unsupported by the submitted proof. The theorem may still be true; a repair that guards H with BOS and conjoins φ_EOS looks plausible. But the paper needs to actually write that proof.\n\nTwo lesser issues. Cor 6.4 glosses over the normalization requirement in Def 4.2 — the (1/2 a)* example needs the distribution to sum to one over all continuations, which the statement doesn't address; that's patchable. And Thm 6.1 leans on the finiteness lemma from Yang et al. 2024 rather than reproving it; that's fine since it's published, but the paper should make the dependency explicit in the main text, not just in the appendix.\n\nVerdict: if the 6.6(b) proof is fixed, this is a solid, citable contribution. As it stands, the real-semiring results stand on their own, but the Boolean equivalence should be treated as unproved. Send it to a serious referee with instructions to focus on the theorem 6.6 proof — this is exactly the kind of paper that deserves review rather than desk rejection, and the authors are likely to fix it quickly.","headline":"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.","tokens_in":17059,"tokens_out":2919,"would_cite":true,"duration_ms":24150,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q70","03B44"],"pacs":[],"model":"deepseek-v4-flash","headline":"As autoregressive language models, hard-attention transformers express exactly counter-free automata's weighted languages — and probabilistic use splits what Boolean results predict.","keywords":["transformer language models","expressivity","weighted languages","counter-free automata","linear temporal logic","unique hard attention","autoregressive generation","formal language theory"],"falsifier":"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.","tokens_in":15913,"feed_emoji":"🎲","tokens_out":8619,"duration_ms":70909,"temperature":0.7,"pith_summary":"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.","feed_headline":"Autoregressive hard-attention LMs match counter-free automata","feed_subtitle":"Probability distributions, not accept/reject verdicts, change what these transformers can express — and the Boolean-era equivalences split.","key_machinery":"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","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Autoregressive transformers match counter-free automata in distribution","Transformers as probability generators match counter-free automata","Autoregressive LMs equal counter-free automata expressivity","Probability distributions of transformers align with counter-free automata","Autoregressive transformers: distributions match counter-free automata"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Autoregressive transformers match counter-free automata in distribution","Transformers as probability generators match counter-free automata","Autoregressive LMs equal counter-free automata expressivity","Probability distributions of transformers align with counter-free automata","Autoregressive transformers: distributions match counter-free automata"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00057,"raw_usage":{"total_tokens":2474,"prompt_tokens":625,"completion_tokens":1849,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":369,"completion_tokens_details":{"reasoning_tokens":1769}},"tokens_in":369,"tokens_out":1849,"duration_ms":14344,"temperature":1.0,"reasoning_tokens":1769,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T07:03:04.491390+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}