Pith. sign in

REVIEW 3 major objections 5 minor 13 references

Comparison of different Unique hard attention transformer models by the formal languages they can recognize

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Unique hard attention transformers come in variants that recognize different formal languages, and this survey places them in a strict hierarchy running from first-order definable languages up to constant-depth circuits.

desk verdict A useful survey with three modest new results, but the proof of the headline inclusion F-UHAT subset F-MUHAT has a gap that should be fixed before the diagram is trusted. read the letter →

arxiv 2506.03370 v1 pith:YFJ7YUBN submitted 2025-06-03 cs.LG cs.CLcs.FL

Leonid Ryvkin This is my paper
classification cs.LGcs.CLcs.FL MSC 68Q4568Q1968T07
keywords uniquehardattentiontransformersformallanguagesmaskedfirst-orderlogiccircuitcomplexitystar-freeURASPseparable
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This note surveys what unique hard attention transformer encoders can recognize as formal languages, comparing masked versus unmasked attention, finite-image versus unbounded position encodings, and general versus bilinear score functions. The paper's central claim is a hierarchy: finite-image masked transformers recognize exactly the first-order definable languages with unary numerical predicates; finite-image unmasked transformers are strictly weaker; and general unmasked transformers sit inside $\mathrm{AC}^0$ while missing languages like approximate majority. It also argues that for finite image encoders masking helps, that general scores collapse to bilinear ones, and that for unmasked general transformers adding layers strictly increases expressive power. If the diagram is right, the note gives a clear boundary for which simple formal languages hard-attention transformers can compute.

What carries the argument

The paper works in URASP, a restricted sequence programming language equivalent to unique hard attention transformers, and normalizes attention layers to the form $\blacktriangleleft_j[\top, s(j)]v(j) : D(i)$ in the finite-image setting. The load-bearing new notion is separable attention, a score function expressible as a finite sum of products $f_i(x)g_i(y)$; separability is shown to be equivalent to bilinearity and automatic for finite image embeddings, which explains why the GUHAT/UHAT distinction disappears there. The inclusion $\mathrm{F\text{-}UHAT} \subseteq \mathrm{F\text{-}MUHAT}$ runs through BRASP and a four-layer masked construction (BOS, L1, L2, L3) that is intended to simulate each unmasked attention step using strict future and past masking.

What would settle it

Run the four-layer simulation on a finite-image F-UHAT program at position 0 where no earlier position has score 1, and check whether the final value matches the unmasked program's value at that position; if it does not, a language whose membership depends on that position would break the claimed inclusion $\mathrm{F\text{-}UHAT} \subseteq \mathrm{F\text{-}MUHAT}$.

Watch

Extended reading notes

Core claim

Section 4.4's inclusion diagram is the note's central assertion. It claims $\mathrm{F\text{-}MUHAT} = \mathrm{FO}_<(\mathrm{Mon})$, that the finite-image general and bilinear variants coincide ($\mathrm{F\text{-}GUHAT} = \mathrm{F\text{-}UHAT}$ and $\mathrm{F\text{-}MGUHAT} = \mathrm{F\text{-}MUHAT}$), that $\mathrm{F\text{-}UHAT}$ is properly contained in $\mathrm{F\text{-}MUHAT}$, that $\mathrm{GUHAT}$ lies inside $\mathrm{AC}^0 \cap \text{strongly }\epsilon\text{-fixable}$ while approximate majority lies outside it, and that $\mathrm{F\text{-}MUHAT}$ is properly contained in $\mathrm{UHAT}$. A separate contribution is Theorem 3.1: for every depth bound $D$ there is a language recognizable by a GUHAT with more layers but not by any $D$-layer GUHAT, proved by combining all the DYCK-(1,n) languages into one construction and deriving recognition of DYCK-1.

Load-bearing premise

The proof that finite unmasked transformers can be simulated by masked ones assumes that at the very first position the default value still reproduces the attended value, while under strict past masking that default is zero, so the simulation as written is not established for the boundary position.

Editorial extensions

If this is right

  • Finite-image masked transformers recognize exactly the class $\mathrm{FO}_<(\mathrm{Mon})$, equivalently the star-free languages.
  • Finite-image unmasked transformers are strictly weaker than finite-image masked ones, with DYCK-(1,2) as a witness language.
  • In the finite-image setting, general attention scores give no extra power over bilinear scores.
  • General unmasked transformers cannot recognize all of $\mathrm{AC}^0$; approximate majority is the separating language.
  • For every layer bound $D$, a GUHAT with sufficiently many more layers recognizes a language no $D$-layer GUHAT recognizes.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If Theorem 4.11's position-0 gap is repaired, then the strictness of the finite masked/unmasked hierarchy rests on the boundary case of the simulation, and the choice of default value at the first position may be the real source of the difference.
  • The separability equivalence suggests that any genuine separation between GUHAT and UHAT must come from a non-separable score function built on an unbounded positional encoding; a concrete such language would settle the open questions in the paper's diagram.
  • The depth-hierarchy construction imports bracket-depth languages, so a natural extension is to test whether the same encoding trick yields a depth hierarchy for the masked or bilinear variants, not just for general unmasked transformers.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The manuscript is a survey of unique hard attention transformer encoders (UHATs) and their variants, organized around the classes GUHAT, UHAT, masked analogues, and finite-image restrictions. It recalls known results on epsilon-fixability, AC^0 upper bounds, and first-order definability, and it presents three observations claimed to be potentially new: a depth hierarchy for GUHATs (Theorem 3.1), a notion of separable attention used to identify finite-image GUHATs with finite-image UHATs (Corollary 4.7), and a proof that finite-image UHATs are contained in finite-image masked UHATs (Theorem 4.11). The paper closes with an inclusion diagram summarizing the known and new relations.

Significance. If the new proof in Theorem 4.11 is repaired, the paper gives a useful and clearly organized map of the known landscape, and the separable-attention viewpoint is a helpful conceptual addition. The survey function is valuable, especially because it collects results from [2], [6], [7], and [12] and flags exactly which arguments are new. However, the main original proof, Theorem 4.11, is not correct as written, and since that theorem is load-bearing for the strict inclusion F-UHAT subset F-MUHAT in the Section 4.4 diagram, the manuscript needs substantive revision before the central diagram can be accepted.

major comments (3)
  1. [Section 4.3, Theorem 4.11] The four-layer simulation of an unmasked F-UHAT attention step does not handle the case in which the normalized binary score s(j) is 0 for every position. In the original normalized layer, all attention scores are then equal, so the leftmost-hard tie-breaking selects position 0 and outputs v(0). In the proposed simulation, L1(i) = leftmost_j [i<j, s(j)]v(j) : 0 cannot see position 0 when i=0, because the mask i<j excludes j=0. If there is some later position, the leftmost tied masked position is j=1, so L1(0)=v(1); if n=1, the masked set is empty and L1(0) uses the default 0. In either case L2(0) is v(1) or 0, not v(0). Thus the simulated output at every position, after L3 propagates L2(0), can differ from the original output whenever v(0) differs from v(1). The proof's statement that 'since there is no masking, D(i) is never used' concerns the original unmasked layer; in the replacement L1 the default is relevant, and setting it to 0 is not always correct. A repair would need to make position 0 visible to the computation at position 0, for example by using a non-strict mask i<=j or by arranging the score so that the all-zero case is treated differently, but the written proof does not do this. The inclusion F-UHAT subset F-MUHAT is therefore not established as written.
  2. [Section 4.2, Theorem 4.9] The direct proof that F-MUHAT is contained in UHAT does not specify how the default value at position 0 is realized in the unmasked simulation. In a strict-future-masked layer, position 0 has an empty candidate set and outputs the default D(0); in the modified unmasked attention function sbar, all scores at position 0 are negative and the maximum is attained at j=0, so the unmasked layer attends to position 0 itself. The proof says that 'the default value should be used' at the first position, but no default mechanism exists in the unmasked URASP definition, and the activation function is not described. Because this theorem is cited from [2,12], the inclusion itself is not in doubt, but the presented direct proof is incomplete and should either be completed or marked as a proof sketch.
  3. [Section 4.3, Example 4.12] The strictness argument for F-UHAT subset F-MUHAT is only a sketch, and it depends on the same normalization used in Theorem 4.11. The sentence 'Since the column at k will always coincide with the column at i or j' assumes a precise invariant about how the normalized attention layers treat identical positional encodings under leftmost-hard tie-breaking, but that invariant is not stated or proved. Because this example supplies the properness of the inclusion in the Section 4.4 diagram, it should be expanded into a formal argument rather than left as a brief remark.
minor comments (5)
  1. [Section 1.2 and Section 4.4] The shorthand 'F - M(G)UHAT' is used to mean both F-MGUHAT and F-MUHAT; this notation should be defined explicitly before it is used in the diagram and in the text.
  2. [Section 4.1, Definition 4.1 and Example 4.2] The summation in Definition 4.1 should run from i=1 to k, not i=0, and the display of Example 4.2 has garbled superscripts and subscripts that make the separability decomposition hard to read.
  3. [Section 2.2, Example 2.14] The condition 'i < n-1 2' appears to be a typographical error; it should presumably be 'i < (n-1)/2'.
  4. [Section 4.4] The inclusion diagram is typeset as a vertical list of classes with arrows, not as an actual commutative diagram; a properly drawn diagram with all labels would make the inclusions and strictness claims much easier to verify.
  5. [Section 3, Theorem 3.1] The proof of Theorem 3.1 assumes that each V[i] contains a designated value 0; this can be arranged by adding a dummy element, but the assumption should be stated explicitly.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the survey's inclusions are imported from external cited theorems or proved by explicit constructions, not by fitting, self-citation, or definitional equivalence.

full rationale

The note is a survey whose load-bearing inclusions are either quoted from independent prior papers ([2], [6], [7], [12]) or proved in the text by direct simulation and separability arguments. There is no self-citation loop: reference [12] is by Yang, Chiang, and Angluin, [2] by Barcelo et al., [6] by Hahn, and [7] by Hao et al., none overlapping with the author. Theorem 3.1's new depth argument constructs a hypothetical D-layer transformer for DYCK-1 from a uniform family of D-layer transformers for DYCK-(1,D') and derives a contradiction from the known non-recognizability of DYCK-1; it does not presuppose the hierarchy claim. Section 4.1's separability lemma is a direct algebraic construction, and Theorem 4.9's proof constructs separable scores with explicit inequalities rather than fitting a parameter to the target class. Theorem 4.11 is an explicit four-layer masked simulation of an unmasked attention step; its reliance on the BRASP normalization of [12] is an external lemma, not a restatement of F-UHAT subseteq F-MUHAT. The possible gap at position 0 when no later position has score 1 is a correctness concern about the simulation, not a circular reduction of the theorem to its conclusion. No self-definitional, fitted-input, self-citation load-bearing, uniqueness-imported, or ansatz-smuggling step was found, so the circularity score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No empirical parameters are fitted. The constants in Theorem 4.9's attention function are explicit proof constants, not tunable model parameters. The paper's claims rest on cited formal-language characterizations, which are stated but not reproved.

assumptions (5)
  • domain assumption GUHAT languages are strongly epsilon-fixable (Hahn [6])
    Used as an upper bound in Section 4.4 and Appendix A.1; not reproved in this note.
  • domain assumption GUHAT languages are contained in AC^0 (Hao, Angluin, Frank [7])
    Used in Section 4.4 and in Corollary A.10 to exclude DYCK-1; imported from the literature.
  • domain assumption F-MUHAT languages are exactly FO_<(Mon), equivalently LTL(Mon) (Yang, Chiang, Angluin [12])
    Central characterization used in Sections 4.2 and 4.3 and Theorem A.17; the proof relies on the BRASP equivalence from [12].
  • domain assumption FO_<(Mon) languages are contained in UHAT (Barcelo et al. [2])
    Used to prove F-MUHAT subset UHAT in Theorem 4.9 and in the summary diagram.
  • domain assumption URASP programs may be nonuniform in input length n, since the initialization En and all score and activation functions can see n
    Definition 2.1 and Remark 2.5; this is the mechanism that makes the depth hierarchy proof in Theorem 3.1 work.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Comparison of different Unique hard attention transformer models by the formal languages they can recognize." pith.science (2026). https://pith.science/paper/YFJ7YUBN

@misc{pith2026250603370,
  author       = {Pith},
  title        = {Pith review of: Comparison of different Unique hard attention transformer models by the formal languages they can recognize},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YFJ7YUBN}},
  note         = {Machine review of arXiv:2506.03370}
}
read the original abstract

This note is a survey of various results on the capabilities of unique hard attention transformers encoders (UHATs) to recognize formal languages. We distinguish between masked vs. non-masked, finite vs. infinite image and general vs. bilinear attention score functions. We recall some relations between these models, as well as a lower bound in terms of first-order logic and an upper bound in terms of circuit complexity.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages

  1. [2]

    Logical Languages Accepted by Transformer Encoders with Hard Attention, October 2023

    Pablo Barcelo, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir Podolskii. Logical Languages Accepted by Transformer Encoders with Hard Attention, October 2023

    work page 2023

  2. [6]

    Theoretical limitations of self-attention in neural sequence models.Transactions of the Asso- ciation for Computational Linguistics, 8:156–171, 2020

    Michael Hahn. Theoretical limitations of self-attention in neural sequence models.Transactions of the Asso- ciation for Computational Linguistics, 8:156–171, 2020

    work page 2020

  3. [7]

    Formal Language Recognition by Hard Attention Transformers: Perspectives from Circuit Complexity, April 2022

    Yiding Hao, Dana Angluin, and Robert Frank. Formal Language Recognition by Hard Attention Transformers: Perspectives from Circuit Complexity, April 2022

    work page 2022

  4. [12]

    Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages, May 2024

    Andy Yang, David Chiang, and Dana Angluin. Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages, May 2024

    work page 2024

  5. [1]

    A theorem on probabilistic constant depth computations

    Miklos Ajtai and Michael Ben-Or. A theorem on probabilistic constant depth computations. InProceedings of the 16th Annual ACM Symposium on Theory of Computing (STOC ’84), pages 11–19. ACM, 1984

    work page 1984

  6. [3]

    Brzozowski and R

    J.A. Brzozowski and R. Knast. The dot-depth hierarchy of star-free languages is infinite.Journal of Computer and System Sciences, 16(1):37–55, 1978

    work page 1978

  7. [4]

    First-order definable languages

    Volker Diekert and Paul Gastin. First-order definable languages. InLogic and Automata. History and Perspec- tives. Dedicated to Wolfgang Thomas on the Occasion of His Sixtieth Birthday., pages 261–306. Amsterdam: Amsterdam University Press, 2008

    work page 2008

  8. [5]

    Computing approximate majority in ac0, 2023

    Oded Goldreich. Computing approximate majority in ac0, 2023. Accessed: 2024-11-03

    work page 2023

Show all 13 references
  1. [8]

    Logical languages accepted by transformer encoders with hard attention, 2023

    Alexander Kozachinskiy. Logical languages accepted by transformer encoders with hard attention, 2023. [On- line; accessed 4-Nov-2024]

    2023

  2. [9]

    Temporal logic with past is exponentially more succinct, concurrency column.Bull

    Nicolas Markey. Temporal logic with past is exponentially more succinct, concurrency column.Bull. EATCS, 79:122–128, 2003

    2003

  3. [10]

    William Merrill, Ashish Sabharwal, and Noah A. Smith. Saturated transformers are constant-depth threshold circuits, 2021

    2021

  4. [11]

    Thinking Like Transformers

    Gail Weiss, Yoav Goldberg, and Eran Yahav. Thinking Like Transformers

  5. [13]

    Self-attention networks can process bounded hierarchical languages

    Shunyu Yao, Binghui Peng, Christos Papadimitriou, and Karthik Narasimhan. Self-attention networks can process bounded hierarchical languages. In Chengqing Zong, Fei Xia, Wenjie Li, and Roberto Navigli, editors, Proceedings of the 59th Annual Meeting of the Association for Comp...

    2021

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.