{"id":"ea440d21-6273-4cc6-876d-8fd10b58d492","arxiv_id":"2603.19954","paper_version":2,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.5,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Decoder-only transformers provably length-generalize on verifying plans in delete-free/well-formed domains via C*-RASP membership, but fail on general STRIPS and conditional effects.","lead":"Transformers can length-generalize on plan verification for delete-free and well-formed classical planning domains, but not for unrestricted STRIPS or conditional effects. The paper introduces C*-RASP to prove this under growing object alphabets, explaining mixed LLM planning results.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"Bounded-width Symbolic Limit Transformers cannot realize exact Match predicates over unbounded alphabets, undermining C*-RASP simulation for variable-universe plan verification.","rationale":"The reader's weakest-assumption call on the Inference Procedure (Thm C.9) is correct and related, yet secondary: even if the selection procedure is granted, the premise that plan-verification languages lie in the class of functions expressible by some Symbolic Limit Transformer already fails for any program that uses Match, by the elementary rank obstruction above. Fixed-universe results (Thm 3.1) and the negative reductions remain intact, as does the empirical dichotomy; only the novel C* variable-universe positive claims are affected. Clarifying whether the Limit Transformer is permitted infinite-dimensional residual streams, or whether the theory is only approximate, would restore the guarantee; until then the strongest claim holds only conditionally on a fixed (or slowly growing) object bound.","tokens_in":28514,"tokens_out":596,"duration_ms":129961,"concrete_test":"Check Appendix C for the explicit simulation of Match: does it construct (or assume existence of) fixed-d embeddings whose Tok-Tok products equal the equality indicator on every finite initial segment of C? If the construction either (a) lets d grow with |C| or (b) treats the products as abstract oracles not realized by any finite-d family, the positive variable-universe theorems are unsupported; if a fixed-d realization is claimed, recompute the rank of the resulting Gram matrix for M = d+1 to obtain an immediate contradiction.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The positive half of the central claim (Thm 3.6.1 / B.1) rests on every C*-RASP program (incl. those using the Match predicate of Def 3.3 for object-argument equality) being simulable by a Symbolic Limit Transformer (Def C.5). That object has fixed finite width d, bounded-norm embeddings {e_k} in R^d (or H of dim d), and product functions α that are local+translation-invariant. Implementing Match requires Tok-Tok products realizing (a p-bit version of) the equality indicator 1_{k=m} so that attention can count matching groundings exactly. The Gram matrix of those products on any set of M labels then has rank M, but is realized as E^\top A E and therefore has rank ≤ d. For every fixed d this is impossible once M > d. Consequently no single bounded-d Limit Transformer can compute the required exact Match counts on all finite inputs. The simulation claim therefore fails for the variable-universe setting, and the length+alphabet generalization guarantee does not follow from C*-RASP membership.","agreement_with_reader":"partial"},"referee_report":{"model":"grok-4.5","summary":"The paper analyzes length generalization of decoder-only transformers on plan verification (deciding whether a given plan solves a given classical planning instance). It distinguishes fixed-universe (fixed objects) and variable-universe (growing objects/alphabet) settings, and subclasses of domains (delete-free, well-formed, unrestricted STRIPS, conditional effects). For fixed universe it shows membership of the valid-plan language in C-RASP[Pos] for delete-free/well-formed domains (hence length-generalizable) and non-membership for some STRIPS and conditional-effect instances via reductions to Flip-Flop and PARITY. For variable universe it introduces C*-RASP (C-RASP plus a Match predicate for object-argument equality) and Symbolic Limit Transformers, claims that C*-RASP programs are simulated by the latter, and thereby obtains analogous positive/negative results (Theorems 3.1, 3.2, 3.5, 3.6). Empirics on Heavy Grippers, Colors and Lights Out variants corroborate the predicted generalization pattern.","tokens_in":28815,"tokens_out":1208,"duration_ms":61880,"significance":"If the claims hold, the work supplies the first theoretically grounded account of when transformers can length-generalize on plan verification, identifies a broad and practically relevant class of domains (well-formed, covering many IPC/Learning-Track benchmarks) for which this is possible, and introduces a reusable extension of the C-RASP framework to growing alphabets. The explicit C*-RASP programs, the reductions to known hard languages, the idealized but fully formalized learning model, and the matching empirical results (including code) are concrete strengths that would advance both the planning-with-LLMs literature and the length-generalization theory of transformers.","major_comments":[{"comment":"The positive variable-universe claim (Thm. 3.6.1 / B.1) rests on every C*-RASP program, including those that use the Match predicate (Def. 3.3) to test object-argument equality, being simulable by a Symbolic Limit Transformer (Def. C.5). The latter object is required to have bounded residual dimension (the paper explicitly states that width d stays bounded while alphabet size diverges) together with bounded-norm embeddings {e_k} and local translation-invariant product functions α. Realizing exact equality indicators 1_{k=m} (needed for the exact counts that decide preconditions and goals) produces a Gram matrix of rank equal to the number of distinct objects M. That matrix is realized as E^\top AE and therefore has rank ≤ d. For every fixed d the construction is impossible once M > d. Consequently no single bounded-d Limit Transformer correctly evaluates Match-based counts on all finite i","section":null},{"comment":"The same rank obstruction appears inside the learning model (Sec. 3.2 / App. C). The Inference Procedure is claimed to converge to a unique Symbolic Limit Transformer because translation invariance + locality + the regularizer R leave only finitely many candidate algorithms (Thm. C.9). For any program that uses Match, however, exact agreement with the target on all length-n/2 inputs that employ a contiguous alphabet of size n/2 already requires residual dimension Ω(n). Either the hypothesis class Θ_n must allow d \to ∞ (contradicting the bounded-d Limit) or, if R penalizes large d, no hypothesis matches the target for large n. In either case the finiteness argument and the claimed convergence fail for the very programs used in the positive proofs of Thm. 3.6.1.","section":null}],"minor_comments":[{"comment":"The informal statement of Thm. 3.2 and the surrounding prose (p. 5) repeatedly assert that C*-RASP membership yields a length-generalization guarantee for APE transformers; after the simulation gap is repaired this claim should be restated with the precise hypotheses under which the guarantee holds.","section":null},{"comment":"Figure 1 and the overview paragraph of Sec. 1 list “STRIPS \notin C-RASP[Pos]” while the body (Thm. 3.1.2) only shows existence of some STRIPS instances outside the class; a one-sentence clarification would avoid over-statement.","section":null},{"comment":"Appendix C.1.2 defines product functions over a Hilbert space H that is never declared finite- or infinite-dimensional; an explicit sentence would remove ambiguity about whether the rank argument can be circumvented.","section":null},{"comment":"In the experimental section the growth rate of the object set with plan length is not quantified; a short table or plot would make the “variable-universe” claim fully transparent.","section":null}],"recommendation":"major_revision","confidential_remarks":"The fixed-universe half and the empirical corroboration are solid and would be publishable on their own. The variable-universe theory is the paper’s main technical novelty; the rank obstruction is fatal to the claims as written but appears fixable (e.g., by allowing slowly growing width, by moving to approximate Match, or by redefining the Limit object). I therefore recommend major revision rather than rejection. The idealized Inference Procedure is already acknowledged as a modelling choice in the C-RASP literature, so I do not treat it as an independent flaw."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The useful takeaway is a clean structural split: delete-free and well-formed plan verification sit in C*-RASP (hence length-and-alphabet generalizable under their model), while unrestricted STRIPS and conditional effects can encode Flip-Flop or PARITY and sit outside. That organizes a lot of the mixed LLM-planning empirics and is immediately usable for the many IPC domains that already produce well-formed instances.\n\nWhat is new is C*-RASP itself: the split alphabet, the Match predicate for object-argument equality without memorizing IDs, and the Symbolic Limit Transformer that extends Huang et al. (2025b) to simultaneous growth of length and vocabulary. The positive proofs are explicit counting programs that track proposition truth by net counts of matching actions; the negatives are concrete reductions. Empirics on three minimal-pair domains (Heavy Grippers, Colors, Lights Out) line up with the theory, including the sharp well-formed vs conditional-effects contrast on Lights Out even with fixed objects. Citations and self-citations to the C-RASP line look appropriate.\n\nThe soft spot is the one the stress-test flags. A fixed finite width d cannot realize exact equality indicators over an unbounded object alphabet via Tok-Tok products (Gram rank argument). The paper never spells out how Match is approximated or how the p-bit product functions evade this; the simulation claim for variable-universe C*-RASP is therefore incomplete as written. That is a genuine gap in Appendix C, not a minor omission. It does not erase the fixed-universe results or the empirical pattern, and the idealized inference procedure is the same style of assumption already used in the prior C-RASP literature, but it does mean the strongest variable-universe guarantee needs more work.\n\nThis is for people who care about length generalization of transformers or about when LLMs can be expected to verify plans. The math and data are careful enough that a serious referee should see it. I would engage, cite the dichotomy and the C*-RASP idea, and push on the Match simulation in review.","headline":"Solid dichotomy for plan verification plus a real C-RASP extension; the stress-test rank objection is real but does not kill the paper.","tokens_in":29414,"tokens_out":503,"would_cite":true,"duration_ms":7370,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"Transformers can learn to verify long plans when domains are delete-free or well-formed, but not for general STRIPS.","keywords":["transformers","plan verification","length generalization","C-RASP","C*-RASP","classical planning","STRIPS","well-formed domains"],"falsifier":"Train an APE transformer on short plans drawn from a well-formed domain (e.g., the well-formed Heavy Grippers or Colors variants) with a limited object set, then measure accuracy on much longer plans with many more objects; if accuracy collapses while the corresponding delete-free or well-formed C*-RASP program exists, the central claim fails.","tokens_in":29420,"feed_emoji":"🧩","tokens_out":714,"duration_ms":6557,"temperature":0.7,"pith_summary":"Transformers succeed inconsistently on AI planning, and theory has been scarce on when length generalization should occur. This paper studies plan verification: given an instance and a candidate plan, decide whether the plan is valid. The hard case is when the number of objects (hence the input alphabet) can grow at test time. The authors introduce C*-RASP, an extension of C-RASP that gives length-generalization guarantees for transformers under simultaneous growth of sequence length and vocabulary. They prove that for delete-free and well-formed classical planning domains the verification language belongs to C*-RASP and is therefore learnable with perfect length generalization; unrestricted STRIPS and domains with conditional effects fall outside and can encode Flip-Flop or PARITY, which are known not to length-generalize. Experiments on Heavy Grippers, Colors, and Lights Out confirm the predicted split. The result matters because many practical planning benchmarks are well-formed, so the structural form of a domain, not merely size, decides whether transformers can reliably verify long plans.","feed_headline":"Transformers verify long plans only when domains are well-formed","feed_subtitle":"Delete-free and well-formed domains lie in C*-RASP; general STRIPS and conditional effects do not","key_machinery":"C*-RASP: an extension of C-RASP that adds a Match Predicate allowing object identities drawn from a growing alphabet to be compared only via local equality checks, without memorizing absolute identifiers; expressibility in C*-RASP is necessary and sufficient for length generalization of APE transformers under the idealized Inference Procedure that selects the minimal regularizer translation-invariant finite-precision model.","core_discovery":"Plan verification for delete-free or well-formed domains lies in C*-RASP (and C-RASP[Pos] when the object set is fixed), so absolute-positional-encoding transformers length-generalize under the Symbolic Limit Transformer learning model; unrestricted STRIPS and conditional-effect domains lie outside C*-RASP and can encode Flip-Flop or PARITY, so length generalization is not expected.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Transformers verify long plans in well-formed domains via C*-RASP","Delete-free domains let transformers length-generalize plan checks","Unrestricted STRIPS plan verification falls outside C*-RASP","Well-formed domains enable transformer plan verification growth","C*-RASP shows when transformers can verify growing object plans"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"Learning is idealized as selecting, among all translation-invariant finite-precision transformers that match the target on short inputs using only a contiguous alphabet subset, the single model of lowest regularizer; that selection is assumed to converge to the unique Symbolic Limit Transformer that works at every length.","fun_headline_variants_meta":{"raw":{"variants":["Transformers verify long plans in well-formed domains via C*-RASP","Delete-free domains let transformers length-generalize plan checks","Unrestricted STRIPS plan verification falls outside C*-RASP","Well-formed domains enable transformer plan verification growth","C*-RASP shows when transformers can verify growing object plans"]},"model":"grok-4.5","effort":"low","cost_usd":0.003926,"raw_usage":{"total_tokens":1175,"prompt_tokens":685,"num_sources_used":0,"completion_tokens":69,"cost_in_usd_ticks":39260000,"prompt_tokens_details":{"text_tokens":685,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":421,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":685,"tokens_out":69,"duration_ms":3680,"temperature":1.0,"reasoning_tokens":421,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-13T21:45:57.227253+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Train an APE transformer on short plans drawn from a well-formed domain (e.g., the well-formed Heavy Grippers or Colors variants) with a limited object set, then measure accuracy on much longer plans with many more objects; if accuracy collapses while the corresponding delete-free or well-formed C*-RASP program exists, the central claim fails.","supporting_citations":[],"review_version":1}