{"id":"29a61145-9136-4475-b5a6-224152ed31f7","arxiv_id":"2506.03370","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper maps known and new inclusion and separation results for unique hard attention transformer variants into one diagram, with new proofs for a depth hierarchy, separable attention in finite-image models, and masked simulation.","lead":"This note surveys very simple attention-based transformer models and compares which formal languages they can recognize, from first-order logic to constant-depth circuits. It consolidates known inclusion results and adds a few new proofs about depth, separability, and masked attention.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 4.11's four-layer simulation of an unmasked F-UHAT attention step omits the case where no later position has score s(j)=1, so the claimed inclusion F-UHAT ⊆ F-MUHAT is not established as written.","rationale":"The reader's weakest assumption identifies the same gap in Theorem 4.11: the simulation at position 0 fails when no later position has s(j)=1, so the exact simulation of F-UHAT by F-MUHAT is not established. This is the most load-bearing concern because Theorem 4.11 is one of the paper's claimed new proofs and supports the strict inclusion F-UHAT ⊂ F-MUHAT in the central diagram. The rest of the diagram mostly imports known characterizations from [2], [6], [7], and [12], so a survey reader can treat those as cited background. The depth hierarchy proof in Theorem 3.1 is a separate new argument and appears coherent, though it also depends on Example A.19's layer count. The concern is substantial but repairable: either [12]'s normalization can be shown to guarantee a true score in every normalized layer, or the four-layer construction can be modified to handle the all-zero case explicitly. Since the paper is a survey with useful exposition and the gap is in a new proof rather than in the overall research program, the correct response remains the reader's conditional verdict rather than outright rejection.","tokens_in":14369,"tokens_out":9868,"duration_ms":114469,"concrete_test":"Run Theorem 4.11's construction on the simplest normalized layer L(i) = ◀j [⊤, s(j)] v(j) with s(j)=0 for all j and v(0)=1, v(j)=0 for j>0, on a length-1 input. The original layer, by leftmost tie-breaking over all positions, outputs 1 at the single position. The simulated BOS/L1/L2/L3 sequence outputs L2(0)=0 at every position. If this mismatch reproduces, the proof as written is incorrect; a repair must either prove that [12]'s normalization never produces an all-zero s(j), or modify the simulation (e.g., by using the default value D(0) instead of 0 when no later position has score 1).","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 4.11 is the paper's new proof that F-UHAT ⊆ F-MUHAT, a load-bearing edge in the Section 4.4 diagram. After normalizing each unmasked attention layer to the form ◀j [⊤, s(j)] v(j), with boolean s(j) and leftmost tie-breaking, the proof replaces it by the masked sequence BOS, L1, L2, L3 and asserts that L2(0) equals the original value at every position. This needs the global leftmost selected position to be visible at position 0. The simulation handles s(0)=1 and handles a later position j>0 with s(j)=1, since L1(0) can see it. It does not handle the case s(j)=0 for all j. In the original unmasked attention, all scores tie at 0, so leftmost tie-breaking selects position 0 and outputs v(0). In the masked simulation, L1(0) uses the default 0 because the strict mask i<j leaves no candidates; then L2(0) = ¬s(0) ∧ L1(0) = 0. If v(0)=1, the simulated layer outputs 0 at every position while the original outputs 1. The proof's statement that 'since there is no masking, D(i) is never used' is therefore not sufficient: an unmasked layer always has candidates, but the boolean predicate s(j)=1 can be false everywhere, and then the leftmost tied position, not the default, is selected. Unless the normalization from [12, Proposition 11 and Lemma 2] is shown to guarantee at least one true s(j) per layer, the four-layer construction does not exactly simulate the original layer, and the claimed inclusion is unproved.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":14710,"tokens_out":15001,"duration_ms":178263,"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":[{"comment":"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.","section":"Section 4.3, Theorem 4.11"},{"comment":"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.","section":"Section 4.2, Theorem 4.9"},{"comment":"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.","section":"Section 4.3, Example 4.12"}],"minor_comments":[{"comment":"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.","section":"Section 1.2 and Section 4.4"},{"comment":"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.","section":"Section 4.1, Definition 4.1 and Example 4.2"},{"comment":"The condition 'i < n-1 2' appears to be a typographical error; it should presumably be 'i < (n-1)/2'.","section":"Section 2.2, Example 2.14"},{"comment":"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.","section":"Section 4.4"},{"comment":"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.","section":"Section 3, Theorem 3.1"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is essentially a survey with three advertised new observations, and the main new proof, Theorem 4.11, is not correct as written. Since the same theorem is the primary original contribution, the revision needs to repair the all-zero-score case or else reclassify the inclusion as relying entirely on cited results. I would be willing to review a revised version."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This is an honest survey that does a real service: it consolidates known expressiveness results for hard-attention transformers into one diagram and adds three small but genuine pieces - the depth hierarchy proof, explicit separable attention, and the formal claim that finite UHAT is included in finite MUHAT. The paper is clearly written, credits prior work carefully, and is candid about what is new and what is imported. The depth hierarchy argument is a nice diagonalization; separable attention is a useful conceptual lens.\n\nThe soft spot is Theorem 4.11, the proof that F-UHAT subset F-MUHAT. The four-layer simulation replaces an unmasked leftmost attention layer with BOS, L1, L2, L3. The gap is at position 0 when no later position has s(j)=1. In the original unmasked layer, all scores tie at 0, so leftmost tie-breaking selects position 0 and outputs v(0). In the simulation, L1(0) uses the default 0 because strict mask leaves no candidate, and L2(0)=0. If v(0)=1, simulated layer outputs 0 everywhere while original outputs 1. The proof says D(i) is never used because there is no masking, but that is about the original layer, not about L1's default. Unless normalization from [12, Proposition 11 and Lemma 2] guarantees at least one true s(j) per layer, which the paper does not show, simulation does not go through. This is not fatal to survey's value, but it is a load-bearing edge in the diagram.\n\nOther soft spot is heavy reliance on unproved results from [2], [6], [7], [12]. Standard for a survey, not problem per se, but diagram strong only as citations. Paper is transparent.\n\nWho should read: anyone working on formal-language expressiveness of hard-attention transformers. It is not breakthrough, but reliable synthesis.\n\nRecommendation: send to peer review, but ask author to repair Theorem 4.11. Inclusion likely true and probably fixable, but as written proof incomplete. With fix, accept. If not fixable, survey useful without that edge, mark claim open or conjecture.","headline":"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.","tokens_in":726,"tokens_out":1441,"would_cite":true,"duration_ms":55454,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q19","68T07"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["unique hard attention transformers","formal languages","masked attention","first-order logic","circuit complexity","star-free languages","URASP","separable attention"],"falsifier":"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}$.","tokens_in":14156,"feed_emoji":"🔤","tokens_out":9301,"duration_ms":92416,"temperature":0.7,"pith_summary":"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.","feed_headline":"Finite-image masked transformers match first-order logic","feed_subtitle":"A survey ranks masked, finite, and bilinear attention variants in a strict language hierarchy.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the characterization $\\mathrm{F\\text{-}MUHAT} = \\mathrm{FO}_<(\\mathrm{Mon})$, the BRASP equivalence, and the leftmost binary-score normalization used in Theorem 4.11.","marker":"[12]"},{"why":"Gives the lower bound $\\mathrm{FO}_<(\\mathrm{Mon}) \\subseteq \\mathrm{UHAT}$, the approximate-majority counterexample, and the strictness observations involving PALINDROMES.","marker":"[2]"},{"why":"Provides the upper bound $\\mathrm{GUHAT} \\subseteq \\mathrm{AC}^0$ and the non-membership of DYCK-1 used in the depth hierarchy proof.","marker":"[7]"},{"why":"Establishes strong $\\epsilon$-fixability of GUHAT languages, one of the upper bounds in the inclusion diagram.","marker":"[6]"},{"why":"Introduces the RASP programming language adapted here as URASP, the framework carrying all the constructions.","marker":"[11]"},{"why":"Supplies the equivalence $\\mathrm{FO}_< = \\mathrm{LTL} = \\mathrm{PLTL} = \\mathrm{FLTL}$ behind the logical characterizations.","marker":"[4]"},{"why":"Provides the bounded hierarchical language construction cited in the proof of the GUHAT depth hierarchy.","marker":"[13]"}],"fun_headline_variants":["Survey: finite masked attention equals first-order logic","UHAT survey: masked finite variants match FO(Mon)","Attention hierarchy: finite masked = FO(Mon)","Survey: finite masked attention hits FO(Mon)","Deep attention gains: more layers beat fixed-depth GUHAT"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Survey: finite masked attention equals first-order logic","UHAT survey: masked finite variants match FO(Mon)","Attention hierarchy: finite masked = FO(Mon)","Survey: finite masked attention hits FO(Mon)","Deep attention gains: more layers beat fixed-depth GUHAT"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000462,"raw_usage":{"total_tokens":2254,"prompt_tokens":833,"completion_tokens":1421,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":449,"completion_tokens_details":{"reasoning_tokens":1345}},"tokens_in":449,"tokens_out":1421,"duration_ms":12884,"temperature":1.0,"reasoning_tokens":1345,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T11:05:28.845940+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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}$.","supporting_citations":[{"cited_title":"Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages, May 2024","cited_arxiv_id":null,"evidence_quote":"Supplies the characterization $\\mathrm{F\\text{-}MUHAT} = \\mathrm{FO}_<(\\mathrm{Mon})$, the BRASP equivalence, and the leftmost binary-score normalization used in Theorem 4.11."},{"cited_title":"Logical Languages Accepted by Transformer Encoders with Hard Attention, October 2023","cited_arxiv_id":null,"evidence_quote":"Gives the lower bound $\\mathrm{FO}_<(\\mathrm{Mon}) \\subseteq \\mathrm{UHAT}$, the approximate-majority counterexample, and the strictness observations involving PALINDROMES."},{"cited_title":"Formal Language Recognition by Hard Attention Transformers: Perspectives from Circuit Complexity, April 2022","cited_arxiv_id":null,"evidence_quote":"Provides the upper bound $\\mathrm{GUHAT} \\subseteq \\mathrm{AC}^0$ and the non-membership of DYCK-1 used in the depth hierarchy proof."},{"cited_title":"Theoretical limitations of self-attention in neural sequence models.Transactions of the Asso- ciation for Computational Linguistics, 8:156–171, 2020","cited_arxiv_id":null,"evidence_quote":"Establishes strong $\\epsilon$-fixability of GUHAT languages, one of the upper bounds in the inclusion diagram."},{"cited_title":"Thinking Like Transformers","cited_arxiv_id":null,"evidence_quote":"Introduces the RASP programming language adapted here as URASP, the framework carrying all the constructions."},{"cited_title":"First-order definable languages","cited_arxiv_id":null,"evidence_quote":"Supplies the equivalence $\\mathrm{FO}_< = \\mathrm{LTL} = \\mathrm{PLTL} = \\mathrm{FLTL}$ behind the logical characterizations."},{"cited_title":"Self-attention networks can process bounded hierarchical languages","cited_arxiv_id":null,"evidence_quote":"Provides the bounded hierarchical language construction cited in the proof of the GUHAT depth hierarchy."}],"review_version":1}