Paper deep dive
On the Ability of Transformers to Verify Plans
Yash Sarrof, Yupei Du, Katharina Stein, Alexander Koller, Sylvie Thiébaux, Michael Hahn
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 95%
Last extracted: 3/23/2026, 12:10:09 PM
Summary
The paper investigates the theoretical limits of transformer-based models in verifying AI planning tasks, specifically focusing on length generalization. The authors introduce C*-RASP, an extension of the C-RASP framework, to analyze generalization when both sequence length and vocabulary size (number of objects) increase. They prove that transformers can provably learn to verify plans in delete-free and well-formed classical planning domains, while general STRIPS and conditional effect domains remain outside the scope of guaranteed length generalization.
Entities (4)
Relation Signals (4)
C*-RASP → extends → C*-RASP
confidence 100% · we introduce C*-RASP, an extension of C-RASP
Delete-free planning → isexpressiblein → C*-RASP
confidence 90% · Plan verification is in C*-RASP if it is delete-free
STRIPS → notexpressiblein → C*-RASP
confidence 90% · Full STRIPS plan verification is not in C*-RASP
Transformers → performs → Plan Verification
confidence 90% · analyzing the ability of decoder-only models to verify whether a given plan correctly solves a given planning instance
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Transformers have shown inconsistent success in AI planning tasks, and theoretical understanding of when generalization should be expected has been limited. We take important steps towards addressing this gap by analyzing the ability of decoder-only models to verify whether a given plan correctly solves a given planning instance. To analyse the general setting where the number of objects -- and thus the effective input alphabet -- grows at test time, we introduce C*-RASP, an extension of C-RASP designed to establish length generalization guarantees for transformers under the simultaneous growth in sequence length and vocabulary size. Our results identify a large class of classical planning domains for which transformers can provably learn to verify long plans, and structural properties that significantly affects the learnability of length generalizable solutions. Empirical experiments corroborate our theory.
Tags
Links
- Source: https://arxiv.org/abs/2603.19954v1
- Canonical: https://arxiv.org/abs/2603.19954v1
Trouble viewing inline? Open PDF directly →
Full Text
215,964 characters extracted from source content.
Expand or collapse full text
On the Ability of Transformers to Verify Plans Yash Sarrof𝅘𝅥 Yupei Du♫ Katharina Stein♫ Alexander Koller Sylvie Thiébaux Michael Hahn Abstract Transformers have shown inconsistent success in AI planning tasks, and theoretical understanding of when generalization should be expected has been limited. We take important steps towards addressing this gap by analyzing the ability of decoder-only models to verify whether a given plan correctly solves a given planning instance. To analyse the general setting where the number of objects – and thus the effective input alphabet – grows at test time, we introduce C*-RASP, an extension of C-RASP designed to establish length generalization guarantees for transformers under the simultaneous growth in sequence length and vocabulary size. Our results identify a large class of classical planning domains for which transformers can provably learn to verify long plans, and structural properties that significantly affects the learnability of length generalizable solutions. Empirical experiments corroborate our theory. Machine Learning, ICML 1 Introduction Transformer based Large Language Models (LLMs) have demonstrated remarkable capabilities, but their success in the field of AI planning has been mixed. Planning involves computing a sequence of actions to transform an initial state into a desired goal state. To circumvent combinatorial explosion, planning state spaces are represented symbolically, typically using variants of the STRIPS formalism as standardized in the PDDL planning definition language (Fikes and Nilsson, 1971; Haslum et al., 2019). LLMs have made considerable strides in solving planning problems through apt prompting, fine tuning, and programmatic plan or heuristic generation (Yao et al., 2023; Stein et al., 2025; Pallagani et al., 2022; Silver et al., 2024; Chen et al., 2025a; Aghzal et al., 2025), but there is also evidence pointing to their inability to reliably solve planning problems, e.g. under the slogan “LLMs still can’t plan” (Valmeekam et al., 2022, 2024). On many benchmarks, transformers tend to lose track of the world state, propose inapplicable actions, or stop before reaching the goal – especially as plans grow longer (Huang et al., 2025a; Fritzsche et al., 2026). The analysis of LLM planning failures in the literature is almost exclusively empirical and a clear theoretical analysis is lacking. Problem class Fixed Universe Variable Universe Delete-free C-RASP[Pos]C-RASP[Pos] C*-RASP[Pos]C*-RASP[Pos] Well-formed C-RASP[Pos]C-RASP[Pos] C*-RASP[Pos]C*-RASP[Pos] STRIPS ∉C-RASP[Pos] -RASP[Pos] ∉C*-RASP[Pos] *-RASP[Pos] Conditional effects not star-free, ∉C-RASP[Pos] -RASP[Pos] ∉C*-RASP[Pos] *-RASP[Pos] Figure 1: Overview of our results This paper contributes to the theoretical understanding of why transformers succeed on certain planning tasks and fail on others. We focus specifically on plan verification, which decides for a given planning instance and a given plan whether the plan correctly solves the instance. Furthermore, we focus on the question of length generalization: can a transformer learn to verify long plans if it is trained only on short plans? If not, then they cannot fully learn to verify plans from any finite amount of training data. A key technical challenge in understanding how transformers generalize on plan verification is that existing techniques for length generalization are limited to the case where the token vocabulary at training and inference time is the same. In this case, a recent line of work has established a theoretically principled framework for predicting length generalization of transformers based on the expressiveness of the C-RASP language (Yang and Chiang, 2024; Huang et al., 2025b; Yang et al., 2025; Jobanputra et al., 2025; Jiang et al., 2025; Chen et al., 2025b) and its variant C-RASP[Pos]C-RASP[Pos]111Huang et al. (2025b) call it C-RASP[periodic,local]C-RASP[periodic,local]. (Huang et al., 2025b; Jobanputra et al., 2025). It is known that transformers can length-generalize on problems that can be expressed in C-RASP[Pos]C-RASP[Pos], and that they empirically tend not to length-generalise otherwise. We use the C-RASP framework to analyze plan verification for the case where the planning instances at training and test time contain the same objects (Fixed Universe); but of course an even more interesting question is whether transformer can generalize to instances with a larger set of objects (Variable Universe). This case is out of reach of a C-RASP[Pos]C-RASP[Pos]-based analysis. We therefore introduce C*-RASP, which extends C-RASP with the ability to handle increasing alphabets during test time, and provides length generalization guarantees under a formal learning model inspired by Huang et al. (2025b). This is a nontrivial technical result with ramifications beyond plan verification. Using our frameworks, we establish the following results (Overview in Figure 1). Plan verification is in C*-RASP if it is delete-free (i.e. actions only have positive effects) or well-formed (i.e. each of their effects necessarily changes the state). Full STRIPS plan verification is not in C*-RASP, nor is plan verification with conditional effects. This implies that certain structural properties – such as well-formedness which holds of a large class of classical planning domains – can enable the learning of length generalizable solutions, whereas the latter is intractable for unconstrained plan verification with transformers. We confirm our theoretical findings experimentally on a number of planning domains. 2 Background & Task Definition 2.1 Planning Planning involves finding a path from an initial to a goal state in a huge transition system where we transition between possible states of the world with actions. This problem is compactly represented in terms of a domain (predicates representing states and action schemas describing state transitions) and an instance that describes the particular set of objects present in the world, the initial state, and goal. A planning domain is a pair =⟨,⟩ D= P, A where 1. P is a finite set of predicates. A predicate p∈p∈ P has the form p(x1,…,xnp)p(x_1,…,x_n_p) where xix_i are arguments p takes. 2. A is a finite set of action schemas. Each a∈a∈ A is a triplet ⟨args(a),pre(a),eff(a)⟩ (a),pre(a),eff(a) where args(a)args(a) are arguments, eff(a)=[Ci(a)⊳effi(a)]i=1k(a)eff(a)=[C_i(a) _i(a)]_i=1^k(a) are conditional effects, and pre(a)pre(a), effi(a)eff_i(a), and Ci(a)C_i(a) are sets of literals over P with arguments taken from args(a)args(a). They represent the preconditions of a, and its effects under various mutually exclusive and exhaustive conditions, respectively. Figure 2 presents an example, a variant of a well-known domain which we call Heavy Grippers, where a robot must relocate balls within a set of rooms. The robot can move between rooms, pick, drop and carry balls using its grippers. Some balls are heavy. Dropping balls and picking heavy balls discharges the battery, whereas moving recharges it. Predicates: room(r),ball(b),gripper(g),free(g),heavy(b),room(r),ball(b),gripper(g),free(g),heavy(b), charged, atRobby(r),at(b,r),carry(b,g)charged, atRobby(r),at(b,r),carry(b,g) Action move(r1,r2)move(r_1,r_2): Pre: room(r1),room(r2),atRobby(r1)\room(r_1),room(r_2),atRobby(r_1)\ Eff: charged,atRobby(r2),¬atRobby(r1)\charged,atRobby(r_2), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 atRobby(r_1)\ Action pick(b,r,g)pick(b,r,g): Pre: ball(b),room(r),gripper(g),atRobby(r),at(b,r),\ball(b),room(r),gripper(g),atRobby(r),at(b,r), free(g),chargedfree(g),charged\ Eff: ¬heavy(b)⊳carry(b,g),¬free(g),¬at(b,r)\ [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 heavy(b)\ [rgb]0.1796875,0.48828125,0.1953125 [named]pgfstrokecolorrgb0.1796875,0.48828125,0.1953125 \carry(b,g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 free(g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 at(b,r)\ heavy(b)⊳carry(b,g),¬free(g),¬at(b,r),¬charged\heavy(b)\ [rgb]0.1796875,0.48828125,0.1953125 [named]pgfstrokecolorrgb0.1796875,0.48828125,0.1953125 \carry(b,g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 free(g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 at(b,r), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 charged\ Action drop(b,r,g)drop(b,r,g): Pre: ball(b),room(r),gripper(g),atRobby(r),carry(b,g)\ball(b),room(r),gripper(g),atRobby(r),carry(b,g)\ Eff: at(b,r),free(g),¬carry(b,g),¬charged\at(b,r),free(g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 carry(b,g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 charged\ Figure 2: Heavy Grippers domain. We omit the empty condition sets for the effects in movemove and dropdrop which are unconditional. A planning instance Π=⟨,O,I,G⟩ = D,O,I,G , has a domain D, set of objects O, initial state I, and goal G. Figure 3: Valid plan for a Heavy Grippers instance with 1 gripper, 2 balls and 2 rooms. The goal G=at(B1,RoomB),at(B2,RoomA)G=\at(B1,RoomB),at(B2,RoomA)\ is to swap the balls in our rooms. Ball B1 is heavy and requires charge, making moving the only legal action in I. The robot then picks B2 from RoomB, moves, drops it in RoomA. It needs charge so it moves back and forth before picking B1, moving and dropping it in RoomB A proposition p(o1,…,oarity(p))p(o_1,…,o_arity(p)) is a ground instance of a predicate p∈p∈ P obtained by substituting the arguments of p with objects from O; we write P for the sets of all propositions. A state is a set of propositions under the closed world assumption, i.e. this set contains exactly those propositions that hold in the state. The goal G is represented by a set of ground literals. In the following, we partition sets of literals L into: L+L^+ containing all propositions appearing positively in L, and L−L^- containing propositions whose negation appears in L. L is satisfied in state S, written S⊧LS L, iff L+⊆SL^+ S and L−∩S=∅L^-∩ S= . S is a goal state iff S⊧GS G. Actions represent one-step transitions in the state space of the planning instance. An action a(o1,…,oarity(a))a(o_1,…,o_arity(a)) is a ground instance of an action schema a∈a∈ A, where arguments of a are substituted with objects from O in its preconditions, conditions and effects; we write A for the set of actions. An action a∈Aa∈ A is applicable in a state S iff its preconditions are satisfied (i.e. S⊧pre(a)S (a)), in which case the successor state is obtained by removing (resp. adding) the propositions made false (resp. true) by a: i.e. succ(S,a)=(S∖effi(a)−)∪effi(a)+succ(S,a)=(S eff_i(a)^-)∪eff_i(a)^+ where S⊧Ci(a)S _i(a). A plan is a sequence of actions π=[a1,…,an]π=[a_1,…,a_n], and is valid for the planning instance Π iff all actions are applicable and it reaches the goal. That is, π induces a sequence of states s1,…,sn+1s_1,…,s_n+1 such that s1=Is_1=I, si+1=succ(si,ai)s_i+1=succ(s_i,a_i) and sn+1⊧Gs_n+1 G. Figure 3 shows a valid plan for a small instance of the Heavy Grippers domain, where the robot must swap the balls in the rooms. In the following, we say that a state S is reachable iff there exists a valid plan for the planning instance ⟨,O,I,S⟩ D,O,I,S . 2.2 Planning Subclasses & Our Generalization Setting Our results distinguish the following subclasses of planning instances, listed from the least restrictive to the most: Conditional Effects: no restrictions are applied. STRIPS: no action has conditional effects. Thus, for all a∈Aa∈ A, k(a)=1k(a)=1 and C1(a)=∅C_1(a)= . Hence eff(a)eff(a) simplifies to a single literal set and we write STRIPS actions in this simplified form in the rest of the paper (e.g. see move and drop in Figure 2). Well-Formed: a STRIPS instance where each proposition listed in the effects of an action strictly changes value whenever the action is applied. Formally, for all reachable states S, all actions a∈Aa∈ A, and all l∈eff(a)l (a) we have that S⊧pre(a)⟹S⊧¬lS (a) S l. Delete-Free: a STRIPS instance where actions only have positive effects, i.e. for all a∈Aa∈ A eff(a)−=∅eff(a)^-= . We say that a planning domain falls into one of the above classes if all instances of interest for this domain do.222Planning domain formulations normally assume a set of implicit constraints that all states must satisfy, and which hold in the initial state and are preserved by actions; the instances of interest are those for which I and G satisfy these constraints. This is only relevant to Well-Formedness, since the other three properties only depend on the domain. STRIPS is the standard formalism to describe planning problems. Conditional effects are a useful feature when modeling real-world problems, and are strictly more expressive than STRIPS (Nebel, 2000). Many classical planning benchmarks are well-formed according to our definition. The Delete-Free class captures the most well-known relaxation of STRIPS, and is commonly used when computing cost-to-goal heuristics estimates to guide the search of planners (Helmert and Domshlak, 2009). Our primary focus is to study a transformer’s capability to length generalize: training on valid plans of a limited length and testing on longer plans. We study two generalization settings, providing both theoretical and experimental results for each. The domain =⟨,⟩ D= P, A is fixed throughout, and the task is to decide if a given plan π is valid. 1. Fixed Universe: The set of objects O is fixed, but I and G can vary per input sample. The model must learn to validate longer plans for unseen pairs of (I,G)(I,G). 2. Variable Universe: The set of objects O,I,GO,I,G can all vary across samples. Thus at test time, longer plans might also have many more objects than ever seen during training. Note that both the fixed and variable universe settings are widely used in the planning literature, see e.g. (Arfaee et al., 2011; Ferber et al., 2022; Rossetti et al., 2024; Toyer et al., 2020; Ståhlberg et al., 2022; Huang et al., 2025a). 2.3 C-RASP Understanding and predicting transformers’ generalization behavior has been of great interest (e.g. Zhou et al., 2024; Golowich et al., 2025; Izzo et al., 2025). Recently, expressiveness in the C-RASP (Counting RASP) language (Yang and Chiang, 2024) and its variant C-RASP[Pos]C-RASP[Pos] (Huang et al., 2025b; Jobanputra et al., 2025) has been used to establish a theoretically principled and empirically predictive framework for predicting length generalization of transformers (Huang et al., 2025b; Yang et al., 2025; Jobanputra et al., 2025; Jiang et al., 2025; Chen et al., 2025b). If a task can be defined by a program in C-RASP[Pos]C-RASP[Pos], then decoder-only transformers with absolute positional encodings (APE) provably generalize to longer inputs under a specific formal model of training (Theorem 7 in Huang et al. (2025b)). Huang et al. (2025b) show that this result unifies a range of prior empirical observations. Tasks exhibiting length generalization can be programmed in C-RASP[Pos]C-RASP[Pos], whereas tasks provably outside this class empirically fail to generalize. For instance, Huang et al. (2025b) proved that the Flipflop language L=Σ∗be∗L= ^*be^* (over Σ=a,b,e =\a,b,e\) and the PARITY language L=b∗(ab∗ab∗)∗L=b^*(ab^*ab^*)^* cannot be expressed in C-RASP[Pos]C-RASP[Pos]. Languages reducible to either Flipflop or PARITY, are therefore predicted to and have been empirically observed to not length generalize (Liu et al., 2023; Hahn and Rofin, 2024; Huang et al., 2025b; Jobanputra et al., 2025). Thus, we obtain positive generalization results via membership in C-RASP[Pos]C-RASP[Pos], and negative results via reduction to PARITY or Flipflop. 3 Theoretical Results 3.1 Generalization over a Fixed Universe Figure 4: Example from the Colors domain (Fig. 8), where actions add balls of a given color to a bag or remove all balls of a given color from a bag. (a) Well-Formed: balls of the same color cannot be added if already present, and can’t be removed if not in the bag. Such alternation allows the truth of “Is a color in the bag?” to be determined by simply counting add versus remove actions from the initial state. (b) STRIPS: In general STRIPS, determining the truth value requires identifying the last action that actually changed the state, making it equivalent to solving the FlipFlop language. Theorem 3.1 (Fixed Universe). Let D be a planning domain and O a fixed set of objects. Consider the language L,OL_ D,O consisting of all sequences ⟨I,π,G⟩ I,π,G where π is a valid plan for the planning instance ⟨,O,I,G⟩ D,O,I,G . 1. (Delete-Free & Well-Formed) If D is delete-free or well-formed, then L,O∈C-RASP[Pos]L_ D,O -RASP[Pos]. 2. (STRIPS) There exist STRIPS domains and object sets such that L,O∉C-RASP[Pos]L_ D,O -RASP[Pos]. 3. (Conditional Effects) There exist domains with conditional effects such that L,OL_ D,O is neither star-free nor in C-RASP[Pos]C-RASP[Pos]. Proof Sketch. (Full proof in Appendix A.1) These results imply that transformers can learn to verify delete-free and well-formed plans in the fixed universe setting with perfect length generalization. They also show that there are more general instances where, even with a fixed set of objects, transformers cannot length generalize. Statement 1: C-RASP highlights how a transformer using uniform attention can count over its context window. For delete-free, a proposition is true if it was initially present or the count of actions listing it as an effect is >0>0. For well-formed, the truth value of a proposition toggles (See Figure 4a). We can count the number of actions adding a proposition (+1 if initially present) and the ones deleting it. Thus all validity checks (action preconditions and goal) can be done through such counts, which allows us to write C-RASP[Pos]C-RASP[Pos] programs to prove our positive results. For our negative results, we construct a planning instance Π for a given ,O D,O, and show that even the language of valid plans of a fixed Π : L(Π)∉C-RASP[Pos]L( ) -RASP[Pos]. Statement 2: Lin and Bercher (2022) already showed that L(Π)L( ) when Π is a STRIPS instance, is a strict subset of star free regular languages. We construct a STRIPS instance Π such that L(Π)=Σ∗be∗L( )= ^*be^*, where Σ=a,b,e =\a,b,e\, the FlipFlop language. Thus L(Π)∉C-RASP[Pos]L( ) -RASP[Pos]. As shown in Figure 4, ascertaining the truth value of a proposition in STRIPS might require figuring out the last action that affected it. Statement 3: We define an instance in the Lights Out planning domain with conditional effects. We show that L(Π)L( ) in such a case can be reduced to PARITY, making L(Π)∉C-RASP[Pos]L( ) -RASP[Pos] (Huang et al., 2025b). ∎ 3.2 Generalization over a Variable Universe Motivation for a new Framework: Planning might require reasoning over a larger number of objects at test time than seen at train time. For transformers, this corresponds not only to generalization in sequence length, but also to generalization over an effectively larger alphabet. Since C-RASP assumes a fixed and finite alphabet Σ , it is not suitable to analyze such settings. To address this limitation, we expand on several key ideas from Huang et al. (2025b) and introduce C*-RASP, an extension of C-RASP designed to establish length generalization guarantees for transformers under simultaneous growth in sequence length and vocabulary size. Huang et al. (2025b) framed length generalization as the asymptotic convergence of a sequence of transformers – trained on increasing lengths – to the same underlying algorithm, formalized as a Limit Transformer, that would thus work at arbitrarily longer lengths than training (Huang et al., 2025b; Izzo et al., 2025). We adopt the same view, but consider asymptotic convergence of a sequence of transformers – trained on not just increasing lengths but also on increasing vocabulary – to the same underlying algorithm, which we refer to as a Symbolic Limit Transformer (Formal definition in Appendix C.5). Huang et al. (2025b) used C-RASP as a more human readable interface to prove tasks representable in a Limit Transformer. We will do the same with C*-RASP and Symbolic Limit Transformers. Split Alphabet: The key observation underlying our extension is that, in planning domains, not all symbols play the same role. Action names and predicate names are drawn from a fixed, finite set, while object identifiers are not. We therefore view the input alphabet (say Ω ) as partitioned into two parts: Σ∪ , Σ is a fixed alphabet of domain-level symbols (actions, predicates, delimiters), and C is a countably increasing alphabet (isomorphic to natural numbers) used to represent object identities. Product Functions: To formalize this, we parameterize transformers using product functions (Huang et al., 2025b). These functions express the internal computations of a transformer—such as attention scores and MLP activations—as inner products of learnable parameters mediated by the model’s matrices (keys, queries, values, and feedforward layers; see Definition C.1 for the full formalization). They can either reflect pairwise interactions or products that depend on only a single token or position. Pairwise interactions are those between different tokens, arising for instance from self attention or with the unembedding matrix. An example is a token-token interaction ciTWcjc_i^TWc_j, where W is the product of several parameter matrices throughout the transformer, and ci,cjc_i,c_j are embeddings for tokens i,j∈i,j . Product functions affected by single token/position capture products formed because of the MLPs. Along the lines of Huang et al. (2025b), for a transformer to generalize to increasing lengths and alphabets, its internal ‘algorithm’ cannot depend on absolute position values or object identifiers, which is formalized via the following constraints: 1. Translation Invariance: Interactions must depend only on relative differences, not absolute indices. Crucially, we apply this to the alphabet C and not just positions: a token-token interaction must satisfy f(i,j)=f(i+δ,j+δ)f( c_i, c_j)=f( c_i+δ, c_j+δ). Interactions between unrelated types (e.g., Position-Token) and those involving just one token or one position must collapse to constants. 2. Locality: Interactions must vanish when the relative distance exceeds a finite bandwidth Δ , ensuring the algorithm relies only on local context. Practically, invariance can be brought about during training via the offset trick: For APE, offsets are used to train positional embeddings beyond the maximum train length. For example, if the maximum training length was 100, but generalization to length 200 was desired, during training, positions are randomly shifted to [1+o,…100+o][1+o,… 100+o] such that 0≤o≤1000≤ o≤ 100. This discourages reliance on absolute positions, promoting invariance (Huang et al., 2025b). We can apply the same idea to our extended characters, and despite having access to a limited vocabulary during training, we can shift object identities with offsets to train embeddings beyond what is seen during training. The Learning Model: Symbolic Limit Transformer is essentially an algorithm of a transformer that satisfies these constraints over an infinite context and alphabet. To prove that finite training can actually lead to this solution, we define a learning model along the lines of Huang et al. (2025b): 1. Hypothesis Class (Θn _n): We restrict the search space to transformers that already satisfy translation invariance, and where any parameter is specified at fixed precision (finite number of bits used to represent any parameter). 333In infinite precision setups one cannot hope to identify algorithms implemented by transformers from finite data, notwithstanding the choice of the regularizer (Huang et al., 2025b). 2. Regularizer (ℛR): A regularizer penalizes model complexity (depth, norms) and non-local interactions, forcing the inference procedure to select ‘algorithms’ that are local. Our regularizer simplifies the one used by Huang et al. (2025b). 3. Inference Procedure: We model learning as an idealized selection of the T∈ΘnT∈ _n minimizing ℛ(T)R(T) while matching the target function on all inputs of length n/2n/2 (Huang et al., 2025b). Crucially, these inputs are restricted to use only a contiguous subset of the extended alphabet of size at most n/2n/2. This forces the model to infer rules that are invariant to token identities. Our main result shows that this procedure converges: by selecting the simplest local algorithm on short data, the model effectively identifies the unique Symbolic Limit Transformer, guaranteeing generalization to length n.444In doing so, we improve on the treatment of the Unique Copy task compared to Huang et al. (2025b). See Remark C.6. Guaranteed Length Generalization: We show that expressibility by a Symbolic Limit Transformer is the necessary and sufficient condition for length generalization in our framework. Informally our result is the following, Theorem 3.2 (Informal version of Theorem C.9). A task is expressible by a Symbolic Limit Transformer iff our Inference Procedure generates a sequence of transformers TnT_n that eventually generalize: there exists a threshold N0N_0 such that for all m>N0m>N_0, the model TmT_m (selected on length m/2m/2) correctly computes f on all inputs up to length m. Proof Sketch (Detailed Proof in Appendix C.9) Our inference procedure generates an infinite sequence of distinct transformers T1,T2,…T_1,T_2,…, but translation invariance and locality ensure that they traverse only a finite set of underlying algorithms. The regularizer bounds the structural complexity (depth, precision), while the invariance constraints ensure that the number of product functions is finite. Thus, as n→∞n→∞, the procedure sequentially rules out algorithms that would not have generalized. Since the set of candidate algorithms is finite, there must be a N0N_0 after which only the correct one remains. ∎ C*-RASP: Huang et al. (2025b) used C-RASP as a human-readable interface to establish expressibility results for Limit Transformers. We will do the same for Symbolic Limit Transformers and C*-RASP. We define the following logical predicate that acts over our extended alphabet C, which is used to refer to object IDs. Since generally these objects IDs are numbered, we assume that ≅ℕC . Definition 3.3 (Match Predicate). A Match Predicate χ(i,j)χ(i,j) is a conjunction of equality checks between tokens in the neighborhoods of i and j: χ(i,j):=⋀k=1K(j−δk=i−γk+τk)χ(i,j):= _k=1^K( c_j- _k= c_i- _k+ _k), where δk,γk∈ℕ _k, _k and τk∈ℤ _k are constants and cic_i refers to the token at position i. This predicate evaluates to True if the token at position j−δkj- _k has the same value as the token ((shifted by τk _k)) at i−γki- _k for all k. Such a match predicate can match tokens based on local constants δ,γ,τδ,γ,τ, without memorizing identities of any token from C. The algorithms represented by this predicate correspond to simple pattern matching operations in local neighborhoods throughout our context window. As an example, if we wish to check whether for an action pick(b,r,g)pick(b,r,g), its precondition at(b,r)at(b,r) was in the initial state, the following match predicate can help us check that they refer to the same set of objects (i,ji,j denote the end of the action and the proposition respectively) χ(i,j):=(ci−2=cj−1)∧(ci−3=cj−2)χ(i,j):=(c_i-2=c_j-1) (c_i-3=c_j-2). This predicate is our sole addition (in green) to C-RASP. Definition 3.4 (C*-RASP). Let Σ∪ be an alphabet, where Σ is finite, and C is an increasing alphabet. Let Ψ be a set of binary relations ψ:ℕ×ℕ→0,1ψ:N×N→\0,1\. A C*-RASP program P is defined as a sequence P1,…,PkP_1,…,P_k of operations, where each operation is either Boolean-valued or count-valued, and can be formed according to the rules listed in Table 1. Boolean-Valued Operations Initial P(i):=Qσ(i)P(i):=Q_σ(i) for σ∈Σσ∈ Boolean P(i):=¬P1(i)P(i):= P_1(i) P(i):=P1(i)∧P2(i)P(i):=P_1(i) P_2(i) Constant P(i):=⊤P(i):= Comparison P(i):=C1(i)≤C2(i)P(i):=C_1(i)≤ C_2(i) Count-Valued Operations Counting C(i):=#[j≤i,ψ(i,j)]P(j)C(i):= \# [j≤ i,ψ(i,j) ]\;P(j) for ψ∈Ψ∪⊤ψ∈ ∪\ \ Match C(i):=#[j≤i,χ(i,j)]C(i):= \# [j≤ i,χ(i,j) ]\; Conditional C(i):=P(i)?C1(i):C2(i)C(i):=P(i)\;?\;C_1(i)\;:\;C_2(i) Addition C(i):=C1(i)+C2(i)C(i):=C_1(i)+C_2(i) Subtraction C(i):=C1(i)−C2(i)C(i):=C_1(i)-C_2(i) Constant C(i):=1C(i):=1 Table 1: Operations allowed in a C*-RASP program. It should be noted that only symbols from the fixed alphabet Σ may be accessed via unary queries QσQ_σ, while symbols from the extended alphabet C can only be compared through the match predicate.555Compared to C-RASP[Pos]C-RASP[Pos] as defined by (Huang et al., 2025b), we omit operations performing modular counting on positions. These play no role in our results; we discuss technical issues about their representation in Appendix C.6 Counting operations return the number of positions j≤ij≤ i where P(j)P(j) and ψ(i,j)ψ(i,j) which represents functions such as i=j+δi=j+δ, for a fixed δ, thus acting as a local relation (δ cannot be arbitrarily large) for checking things in local neighborhoods. As in C-RASP, if a C*-RASP program is run on input w with final operation L, then we accept w if and only if L(|w|)L(|w|) is true. We also write C*-RASP for the class of all languages accepted by some C*-RASP program. Any C*-RASP program can be simulated by a Symbolic Limit Transformer. Hence, by Theorem 3.2, the existence of a C*-RASP program for a task implies a guarantee of length generalization for APE transformers on that task, allowing us to prove positive length generalization results. If no ψ∈Ψψ∈ is used and all constants of the type σk,δk _k, _k are 0, then length generalization would be guaranteed even for NoPE transformers. Thus we make a distinction between C*-RASP and C*-RASP[Pos]C*-RASP[Pos] to denote the necessity of positional encodings. On the other hand, we show that the difficulty of FlipFlop and PARITY carries over even to C*-RASP: Theorem 3.5. Consider the alphabet Σ=a,b,e =\a,b,e\. Then, PARITY:=b∗(ab∗ab∗)∗∉C*-RASPPARITY:=b^*(ab^*ab^*)^* *-RASP. and Flip flop :=Σ∗be∗∉C*-RASP:= ^*be^* *-RASP . Proof sketch. If the input alphabet Ω=Σ∪ = is finite, then C*-RASP reduces to C-RASP[Pos]C-RASP[Pos], as the match predicate can then be simulated by the syntax of C-RASP[Pos]C-RASP[Pos] itself (Detailed Proof in Appendix, Lemma C.22). Thus, existence of a program for FlipFlop or PARITY in C*-RASP would imply existence of a program in C-RASP[Pos]C-RASP[Pos], which Huang et al. (2025b) showed to be impossible. ∎ Theorem 3.6. Let D be a planning domain. Consider the language L_ D consisting of all possible sequences ⟨I,π,G⟩ I,π,G where π is a valid plan for some planning instance ⟨,O,I,G⟩ D,O,I,G . 1. (Delete-Free / Well-Formed) If D is delete-free or well-formed, then L∈C*-RASPL_ D *-RASP. In particular, generalization from both limited number of objects and plan lengths during training to a increased number of objects and plan lengths is expected. 2. (STRIPS / Conditional Effects) There exists STRIPS domains as well as domains with conditional effects for which L∉C*-RASPL_ D *-RASP. Generalization to instances with longer plans or increased number of objects is thus not expected. In particular, there are domains where L_ D subsumes FlipFlop or PARITY. Detailed Proof is in Appendix B.1. To show our positive results, we construct C*-RASP programs along the same lines as for Theorem 3.1. The crucial difference is the use of the match predicate to match actions to propositions, without relying on specific object identities. Since STRIPS and domains with conditional effects have instances with Flip-Flop and PARITY like signatures, Theorem 3.5 applies. ∎ 4 Experiments 4.1 Planning Domains and Datasets Construction We develop three domains to empirically validate our predictions regarding the learnability of different planning subclasses. For each dataset we generate correct and incorrect plans, where the incorrect plans are constructed to be either incomplete (where the goal is not fully satisfied) or non-executable (where an action’s preconditions are violated).666For some domains, like the standard Colors, since all actions are applicable, invalid plans can only be incomplete. Details of our domain design, data generation, and setups are in Appendix D. Heavy Grippers. We modify the Heavy Grippers domain (Figure 2), and create well-formed and delete-free variants. First, we eliminate the conditional effects by separating pick into two actions and remove charged from the preconditions of picking up not heavy balls. Second, we create the well-formed variant by extending the preconditions and the delete-free variant by removing the delete effects. Colors. This domain involves placing colored balls into bags, where actions add or remove a color from a specific bag, and goals specify which colors each bag should contain. We design well-formed and standard STRIPS variants that differ in handling redundant operations: the well-formed variant enforces that a color can be added or removed only if it is absent or present in the bag, respectively, while the standard STRIPS formulation treats these as no-ops. Lights Out. We formalize the Lights Out game as our final domain. It consists of lights (on/off) on a 5×55× 5 grid where pressing a light toggles it and its neighbors. The goal is to turn all lights off. We consider two variants: one with conditional effects and a well-formed variant. In the conditional effects variant, the post-press states of the pressed light and its neighbors depend on their states before pressing; the well-formed variant uses separate actions for pressing each light under every possible combinations of its and its neighbors’ states. For example, pressing the corner light L_00 yields 232^3 different actions, corresponding to the states combinations of L_00 and its neighbors L_10 and L_01. 4.2 Experimental Setup & Results Figure 5: ID (100-bucket) OOD (110-200, 10-bucket) accuracy for our domains. We compare the well-formed variant to a minimal pair: delete-free for Grippers, STRIPS for Colors, and conditional effects for Lights Out. Well-formed and delete-free has good accuracy even at higher lengths, accuracy for STRIPS drops with plan length and performance for conditional effects is chance level. Our detailed results are in Figure 12. Setup: We use the GPT-2 architecture with APE and pre-layer normalization, and train it with the standard causal language modeling objective. The initial state, plan, goal, and a verdict token indicating plan validity (‘correct’/‘incorrect’), each separated by a custom delimiter form our inputs: <init>I<plan>π<goal>G<verdict>V, <init>I\; <plan>π\; <goal>G\; <verdict>V, where V refers to the verdict label. We train on plans of 11–100 actions and validate on 101–200 actions (length here refers to the number of actions in π, not tokens). The numbers of objects in Colors and Heavy Grippers grow with plan length, whereas Lights Out has a fixed number of objects. We use a fixed number of objects for Lights Out to show that our negative result regarding conditional effects holds even in the setting described in Theorem 3.1, whereas the increased number of objects in the other domains helps validate the positive results regarding well-formedness and being delete-free, as described in Theorem 3.6. We use four random seeds and select the best checkpoint on a held out validation set. At test time, the verdict token is omitted for the model to generate it. We evaluate on both in-distribution (ID, lengths 11–100) and out-of-distribution (OOD, lengths 101–200) test sets. Results: Our experiments (Figure 5) are consistent with our theory. For Lights Out, we observe a sharp contrast: the conditional effects formulation yields chance-level performance even on a fixed set of objects, whereas the well-formed variant generalizes perfectly despite having an exponential action space, corroborating Theorem 3.1. Furthermore, our models successfully generalize to longer plans and more objects in Heavy Grippers and Colors as predicted by Theorem 3.6. Specifically, the well-formed variants of both domains—as well as the delete-free variant of Heavy Grippers (all in ∈C*-RASP *-RASP)—achieve high accuracy, while for the STRIPS variant of Colors (∉C*-RASP *-RASP), the performance dips. Overall, generalization succeeds where C*-RASP membership holds and fails otherwise.777Our code is available at: https://github.com/coli-saar/transformers_plan_verification 5 Discussion 5.1 Implications Our results establish a sharp divide in the learnability of plan verification by transformers: generalization in delete-free and well-formed instances is possible; but for unconstrained STRIPS domains it is not, with conditional effects making it even harder. Our negative results highlights why transformers have had inconsistent success in planning tasks. Conversely, our positive results are significant given that a broad class of practical planning problems are well-formed. For instance, 70% of the domains from the Learning Track 2023 (Taitler et al., 2024), and a lot of domains in the International Planning Competition (IPC) (McDermott, 2000) come with benchmark problem generators that can only produce well-formed instances. We achieve this breadth through a “semantic” definition of well-formedness in terms of the actual dynamics of the actions and states; much more permissive than the syntax-based definition of Gösgens et al. (2025), which is rarely satisfied by planning benchmarks. We also find that the exact formulation of the planning task matters: for instance, the Lights Out game when formulated with conditional effects does not generalize, but a compilation of this domain into a well-formed one does. This confirms that the structural complexity of the planning problem, rather than just the number of actions or objects, drives the ability of transformers to learn it. Thus, if one can reformulate the problem structure, transformers could have marked improvement in performance. It is also worth noting that the ramifications of Theorem 3.2 (More Formal Statement C.9), and C*-RASP which establishes a framework to give length generalization guarantees for transformers with growing alphabets at test time, are far beyond plan verification. For instance, they open up the possibility to reason about how powerful can transformers with a growing index hint vocabulary be, as even a limited set of index hints have shown to help improve generalization in transformers (Zhou et al., 2024). 5.2 Related Work Transformers have been applied extensively to planning tasks (Yao et al., 2023; Silver et al., 2024; Stein et al., 2025; Hirsch et al., 2024; Pallagani et al., 2022; Fritzsche et al., 2026; Chen et al., 2025a). While LLMs can generate plans when test data instances are of the same size as training (Rossetti et al., 2024), they struggle on larger instances (Huang et al., 2025a; Fritzsche et al., 2026). A recurrent observation is a sharp performance degradation on longer plans (Stein et al., 2025; Valmeekam et al., 2025; Hirsch et al., 2024; Pallagani et al., 2023; Hazra et al., 2024), underscoring the need to better evaluate length generalization in planning (Chiari et al., 2025). Comparatively, plan verification has only been studied by a few (Stechly et al., 2025; Valmeekam et al., 2023). Stechly et al. (2025) found that LLMs struggle to verify self generated plans, while Valmeekam et al. (2023) found LLMs to be better at verification than generation for a STRIPS domain, but overall performance remained low. Prior work has also tried to connect computational complexity of classical planning (Bylander, 1994) to formal language theory (Höller et al., 2016; Lin and Bercher, 2022), albeit not in the context of transformer expressiveness. In contrast, a rich line of research has looked into transformers expressiveness through the lens of formal language theory and computational complexity. This includes the design of formalisms that capture transformer computations, such as RASP (Weiss et al., 2021), B-RASP (Yang et al., 2024), C-RASP (Yang and Chiang, 2024) and results linking models to complexity classes such as TC0TC^0 (Merrill and Sabharwal, 2023; Strobl, 2023). Zhou et al. (2024) conjectured that only programs expressible in RASP-L exhibit length generalization, a notion formalized by Huang et al. (2025b) using the C-RASP formalism (Yang and Chiang, 2024). The C-RASP length generalization framework has since seen substantial success, with results demonstrated at scale (Jobanputra et al., 2025), quantitative bounds on training length (Izzo et al., 2025), and even predictions of the model depth required to solve certain problems (Yang et al., 2025). More broadly, length generalization remains an active area of research, with approaches exploring scratchpads, positional embeddings, and synthetic data generation (Anil et al., 2022; Abbe et al., 2023; Zhou et al., 2024; Golowich et al., 2025; Hou et al., 2024; Xiao and Liu, 2025; Press et al., 2022; He et al., 2024; Cho et al., 2024; Lee et al., 2025; Chen et al., 2025b). Our work is most closely related to Núñez-Molina et al. (2025), who show that plan verification for propositional STRIPS is expressible in B-RASP, and thus realizable by a restricted class of transformers (Yang et al., 2024). We differ in two key respects: we study generalization in learning rather than expressivity, and we consider generalization not only across plans for a fixed instance, but also across instances with unbounded numbers of objects. 5.3 Limitations & Future Work Our theoretical results on length generalization apply to standard transformers without scratchpads (no chain of thought). However, our results are still relevant, as chain of thought is expensive and knowing what is possible without Chain of thought is important. Much like C-RASP, our theory also only applies to APE and NoPE encodings, extending our theory to cover Rotary Positional embeddings is a natural next step. Finally, our focus was on verification and not plan generation. As Stechly et al. (2025) mentions, their respective computational complexity (P vs PSPACE-complete for STRIPS) should not be expected to translate to relative transformer performance. Thus generalizing our findings to plan generation is non-trivial. Our proofs rely on the existence of valid plans containing loops, whereas optimal plans could be much shorter. Thus, while our results serve as a foundational step, characterizing the learnability of plan generation remains exciting grounds for future work. 6 Conclusion We presented a formal analysis of the ability of transformers to verify plans, focusing on the challenge of length generalization. To address the setting where the number of objects grows at test time, we introduced C*-RASP, a novel extension of the C-RASP framework that characterizes learnability under simultaneous growth of sequence length and vocabulary size. Our results indicate that the specific formulation of a planning problem—rather than only the number of objects or actions—is a decisive factor in learnability. These findings take steps toward explaining inconsistent performance of transformers on planning tasks, opening new avenues for characterizing their capabilities in planning. Impact Statement This paper presents work whose goal is to advance the field of Machine Learning. There are many potential societal consequences of our work, none of which we feel must be specifically highlighted here. Acknowledgments Katharina Stein was funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under the project number 232722074 – SFB 1102. We gratefully acknowledge the stimulating research environment of the GRK 2853/1 “Neuroexplicit Models of Language, Vision, and Action”, funded by the Deutsche Forschungsgemeinschaft under project number 471607914. Sylvie Thiébaux’s work was funded by the Australian Research Council (ARC) under the Discovery Project grant DP220103815 and by the Artificial and Natural Intelligence Toulouse Institute (ANITI) under the grant agreement ANR-23-IACL-0002. We thank Chaahat Jain for insightful discussions. Contributions YS drafted the paper, contributed Theorem 3.1, 3.6 and their corresponding proofs (Appendix A, B) with inputs from ST and MH, and coordinated the experiments with KS and YD. YS and MH jointly developed the learning framework, symbolic limit transformer translation, C*-RASP formulation (Section 3.2 and Appendix C). YD developed the training and evaluation pipeline, trained all models, implemented the Colors domain dataset in use, and contributed substantially to the design and development of the other two domain datasets. KS led the development of the datasets and contributed substantially to their designs. She conducted the implementation and generation of the Grippers Heavy and Lightsout datasets, and contributed to the writing. AK advised on the research direction and narrative framing, supervised the experimental work, and contributed to the writing of the paper. ST contributed to the research framing, to the identification of the generalisable planning classes, to the formulation of theorems 3.1 and 3.6, and proposed the Color domain. She drafted section 2 and provided feedback and corrections on every section except Appendix C. MH contributed to the research framing and to the identification of the generalisable planning classes, and jointly developed the learning framework, limit transformers, and C*-RASP formulation with YS. References E. Abbe, S. Bengio, A. Lotfi, and K. Rizk (2023) Generalization on the unseen, logic reasoning and degree curriculum. In Proceedings of the 40th International Conference on Machine Learning, ICML’23. Cited by: §5.2. M. Aghzal, E. Plaku, G. J. Stein, and Z. Yao (2025) A survey on large language models for automated planning. External Links: 2502.12435, Link Cited by: §1. C. Anil, Y. Wu, A. Andreassen, A. Lewkowycz, V. Misra, V. Ramasesh, A. Slone, G. Gur-Ari, E. Dyer, and B. Neyshabur (2022) Exploring length generalization in large language models. Advances in Neural Information Processing Systems 35, p. 38546–38556. Cited by: §5.2. S. J. Arfaee, S. Zilles, and R. C. Holte (2011) Learning heuristic functions for large state spaces. Artif. Intell. 175 (16-17), p. 2075–2098. Cited by: §2.2. T. Bylander (1994) The computational complexity of propositional strips planning. Artificial Intelligence 69 (1-2), p. 165–204. Cited by: §5.2. D. Z. Chen, J. Zenn, T. Cinquin, and S. McIlraith (2025a) Language models for generalised pddl planning: synthesising sound and programmatic policies. In Proceedings of the 18th European Workshop on Reinforcement Learning (EWRL), Cited by: §1, §5.2. T. Chen, T. Ma, and Z. Li (2025b) Non-asymptotic length generalization. In Forty-second International Conference on Machine Learning, External Links: Link Cited by: §1, §2.3, §5.2. D. Chiang and P. Cholak (2022) Overcoming a theoretical limitation of self-attention. In Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2022, Dublin, Ireland, May 22-27, 2022, S. Muresan, P. Nakov, and A. Villavicencio (Eds.), p. 7654–7664. External Links: Link, Document Cited by: §C.1. M. Chiari, L. Putelli, N. Rossetti, I. Serina, and A. E. Gerevini (2025) On planning through llms. In Proceedings of the International Conference on Automated Planning and Scheduling, Vol. 35, p. 377–385. Cited by: §5.2. H. Cho, J. Cha, P. Awasthi, S. Bhojanapalli, A. Gupta, and C. Yun (2024) Position coupling: improving length generalization of arithmetic transformers using task structure. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, External Links: Link Cited by: §5.2. G. Cybenko (1989) Approximation by superpositions of a sigmoidal function. Mathematics of control, signals and systems 2 (4), p. 303–314. Cited by: §C.1. B. L. Edelman, S. Goel, S. Kakade, and C. Zhang (2022) Inductive biases and variable creation in self-attention mechanisms. In International Conference on Machine Learning, p. 5793–5831. Cited by: §C.1. P. Ferber, F. Geißer, F. W. Trevizan, M. Helmert, and J. Hoffmann (2022) Neural network heuristic functions for classical planning: bootstrapping and comparison to other methods. In Proceedings of the 32nd International Conference on Automated Planning and Scheduling (ICAPS), p. 583–587. Cited by: §2.2. R. Fikes and N. J. Nilsson (1971) STRIPS: A new approach to the application of theorem proving to problem solving. Artif. Intell. 2 (3/4), p. 189–208. Cited by: §1. M. Fritzsche, E. Gestrin, and J. Seipp (2026) Symmetry-aware transformer training for automated planning. In Proceedings of the Fortieth AAAI Conference on Artificial Intelligence (AAAI 2026), C. Jenkins and M. Taylor (Eds.), Cited by: §1, §5.2. N. Golowich, S. Jelassi, D. Brandfonbrener, S. M. Kakade, and E. Malach (2025) The role of sparsity for length generalization in transformers. arXiv preprint arXiv:2502.16792. Cited by: §2.3, §5.2. J. Gösgens, N. Jansen, and H. Geffner (2025) Learning lifted strips models from action traces alone: a simple, general, and scalable solution. In Proceedings of the 35th International Conference on Automated Planning and Scheduling (ICAPS), p. 189–197. Cited by: §5.1. M. Hahn and M. Rofin (2024) Why are sensitive functions hard for transformers?. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), p. 14973–15008. Cited by: §2.3. P. Haslum, N. Lipovetzky, D. Magazzeni, and C. Muise (2019) An introduction to the planning domain definition language. Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan & Claypool Publishers. Cited by: §1. R. Hazra, P. Zuidberg Dos Martires, and L. De Raedt (2024) SayCanPay: heuristic planning with large language models using learnable domain knowledge. Proceedings of the AAAI Conference on Artificial Intelligence 38 (18), p. 20123–20133. External Links: Link, Document Cited by: §5.2. Z. He, G. Feng, S. Luo, K. Yang, L. Wang, J. Xu, Z. Zhang, H. Yang, and D. He (2024) Two stones hit one bird: bilevel positional encoding for better length extrapolation. In Proceedings of the 41st International Conference on Machine Learning, ICML’24. Cited by: §5.2. M. Helmert and C. Domshlak (2009) Landmarks, critical paths and abstractions: what’s the difference anyway?. In Proceedings of the 19th International Conference on Automated Planning and Scheduling, ICAPS, Cited by: §2.2. E. Hirsch, G. Uziel, and A. Anaby-Tavor (2024) What’s the plan? evaluating and developing planning-aware techniques for llms. CoRR abs/2402.11489. External Links: Link, Document, 2402.11489 Cited by: §5.2. D. Höller, G. Behnke, P. Bercher, and S. Biundo (2016) Assessing the expressivity of planning formalisms through the comparison to formal languages. In Proceedings of the International Conference on Automated Planning and Scheduling, Vol. 26, p. 158–165. Cited by: §5.2. K. Hou, D. Brandfonbrener, S. M. Kakade, S. Jelassi, and E. Malach (2024) Universal length generalization with turing programs. CoRR abs/2407.03310. External Links: Link, Document, 2407.03310 Cited by: §5.2. S. Huang, T. Cohn, and N. Lipovetzky (2025a) Chasing progress, not perfection: revisiting strategies for end-to-end llm plan generation. In Proceedings of the 35th International Conference on Automated Planning and Scheduling (ICAPS), p. 204–212. Cited by: §1, §2.2, §5.2. X. Huang, A. Yang, S. Bhattamishra, Y. Sarrof, A. Krebs, H. Zhou, P. Nakkiran, and M. Hahn (2025b) A formal framework for understanding length generalization in transformers. In The Thirteenth International Conference on Learning Representations, Cited by: §A.1, §A.1, §A.1, §A.1, §C.1, §C.1, §C.1, §C.1, §C.1.1, §C.1.2, §C.1.2, §C.2, §C.2, §C.2, §C.2, §C.3, §C.3, §C.3, §C.3, §C.3, §C.3, §C.3, §C.3, §C.4, §C.5, §C.5, §C.5, §C.6, §C.6, §C.6, §C.6, §C.6, §C.6, Remark C.3, §1, §1, §2.3, §3.1, §3.2, §3.2, §3.2, §3.2, §3.2, §3.2, §3.2, §3.2, §5.2, footnote 1, footnote 12, footnote 13, footnote 3, footnote 4, footnote 5. Z. Izzo, E. Nichani, and J. D. Lee (2025) Quantitative bounds for length generalization in transformers. In High-dimensional Learning Dynamics 2025, External Links: Link Cited by: §C.1, §C.6, §2.3, §3.2, §5.2. H. Jiang, M. Hahn, G. Zetzsche, and A. W. Lin (2025) Softmax transformers are turing-complete. arXiv preprint arXiv:2511.20038. Cited by: §1, §2.3. M. Jobanputra, Y. Veitsman, Y. Sarrof, A. Bakalova, V. Demberg, E. Pavlick, and M. Hahn (2025) Born a transformer–always a transformer? on the effect of pretraining on architectural abilities. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, Cited by: §1, §2.3, §5.2. A. Kazemnejad, I. Padhi, K. Natesan Ramamurthy, P. Das, and S. Reddy (2023) The impact of positional encoding on length generalization in transformers. Advances in Neural Information Processing Systems 36, p. 24892–24928. Cited by: §C.1. N. Lee, Z. Cai, A. Schwarzschild, K. Lee, and D. Papailiopoulos (2025) Self-improving transformers overcome easy-to-hard and length generalization challenges. In Forty-second International Conference on Machine Learning, Cited by: §5.2. S. Lin and P. Bercher (2022) On the expressive power of planning formalisms in conjunction with ltl. Proceedings of the International Conference on Automated Planning and Scheduling 32 (1), p. 231–240. External Links: Link, Document Cited by: §A.1, §3.1, §5.2. B. Liu, J. Ash, S. Goel, A. Krishnamurthy, and C. Zhang (2023) Exposing attention glitches with flip-flop language modeling. Advances in Neural Information Processing Systems 36, p. 25549–25583. Cited by: §2.3. D. McDermott (2000) The 1998 ai planning systems competition. AI Magazine 21 (2), p. 35–35. Cited by: §5.1. W. Merrill and A. Sabharwal (2023) The parallelism tradeoff: limitations of log-precision transformers. Transactions of the Association for Computational Linguistics 11, p. 531–545. Cited by: §5.2. B. Nebel (2000) On the compilability and expressive power of propositional planning formalisms. J. Artif. Intell. Res. 12, p. 271–315. Cited by: §2.2. C. Núñez-Molina, V. Gómez, and H. Geffner (2025) From next token prediction to (strips) world models – preliminary results. External Links: 2509.13389, Link Cited by: §5.2. V. Pallagani, B. Muppasani, K. Murugesan, F. Rossi, L. Horesh, B. Srivastava, F. Fabiano, and A. Loreggia (2022) Plansformer: generating symbolic plans using transformers. CoRR abs/2212.08681. Cited by: §1, §5.2. V. Pallagani, B. Muppasani, K. Murugesan, F. Rossi, L. Horesh, B. Srivastava, F. Fabiano, and A. Loreggia (2023) Plansformer: generating symbolic plans using transformers. In NeurIPS 2023 Workshop on Generalization in Planning, External Links: Link Cited by: §5.2. O. Press, N. Smith, and M. Lewis (2022) Train short, test long: attention with linear biases enables input length extrapolation. In International Conference on Learning Representations, External Links: Link Cited by: §5.2. N. Rossetti, M. Tummolo, A. E. Gerevini, L. Putelli, I. Serina, M. Chiari, and M. Olivato (2024) Learning general policies for planning through GPT models. In Proceedings of the Thirty-Fourth International Conference on Automated Planning and Scheduling, ICAPS, p. 500–508. Cited by: §2.2, §5.2. T. Silver, S. Dan, K. Srinivas, J. B. Tenenbaum, L. Kaelbling, and M. Katz (2024) Generalized Planning in PDDL Domains with Pretrained Large Language Models. Proceedings of the AAAI Conference on Artificial Intelligence 38 (18), p. 20256–20264. External Links: ISSN 2374-3468, Document Cited by: §1, §5.2. S. Ståhlberg, B. Bonet, and H. Geffner (2022) Learning Generalized Policies without Supervision Using GNNs. In Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning (KR), p. 474–483. Cited by: §2.2. K. Stechly, K. Valmeekam, and S. Kambhampati (2025) On the self-verification limitations of large language models on reasoning and planning tasks. In The Thirteenth International Conference on Learning Representations, External Links: Link Cited by: §5.2, §5.3. K. Stein, D. Fišer, J. Hoffmann, and A. Koller (2025) Automating the generation of prompts for llm-based action choice in pddl planning. In Proceedings of the 35th International Conference on Automated Planning and Scheduling (ICAPS), p. 250–259. Cited by: §1, §5.2. L. Strobl (2023) Average-hard attention transformers are constant-depth uniform threshold circuits. arXiv preprint arXiv:2308.03212. Cited by: §5.2. A. Taitler, R. Alford, J. Espasa, G. Behnke, D. Fišer, M. Gimelfarb, F. Pommerening, S. Sanner, E. Scala, D. Schreiber, J. Segovia-Aguas, and J. Seipp (2024) The 2023 International Planning Competition. AI Magazine 45 (2), p. 280–296. External Links: Document Cited by: §5.1. S. Toyer, S. Thiébaux, F. W. Trevizan, and L. Xie (2020) ASNets: deep learning for generalised planning. J. Artif. Intell. Res. 68, p. 1–68. Cited by: §2.2. K. Valmeekam, M. Marquez, A. Olmo, S. Sreedharan, and S. Kambhampati (2023) Planbench: an extensible benchmark for evaluating large language models on planning and reasoning about change. Advances in Neural Information Processing Systems 36, p. 38975–38987. Cited by: §5.2. K. Valmeekam, A. Olmo, S. Sreedharan, and S. Kambhampati (2022) Large language models still can’t plan (a benchmark for LLMs on planning and reasoning about change). In NeurIPS 2022 Foundation Models for Decision Making Workshop, External Links: Link Cited by: §1. K. Valmeekam, K. Stechly, A. Gundawar, and S. Kambhampati (2025) A systematic evaluation of the planning and scheduling abilities of the reasoning model o1. Transactions on Machine Learning Research. Note: External Links: ISSN 2835-8856, Link Cited by: §5.2. K. Valmeekam, K. Stechly, and S. Kambhampati (2024) LLMs still can’t plan; can lrms? A preliminary evaluation of openai’s o1 on planbench. CoRR abs/2409.13373. Cited by: §1. G. Weiss, Y. Goldberg, and E. Yahav (2021) Thinking like transformers. In International Conference on Machine Learning, p. 11080–11090. Cited by: §5.2. C. Xiao and B. Liu (2025) Generalizing reasoning problems to longer lengths. In The Thirteenth International Conference on Learning Representations, Cited by: §5.2. A. Yang, M. Cadilhac, and D. Chiang (2025) Knee-deep in c-RASP: a transformer depth hierarchy. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, External Links: Link Cited by: §1, §2.3, §5.2. A. Yang, D. Chiang, and D. Angluin (2024) Masked hard-attention transformers recognize exactly the star-free languages. Advances in Neural Information Processing Systems 37, p. 10202–10235. Cited by: §5.2. A. Yang and D. Chiang (2024) Counting like transformers: compiling temporal counting logic into softmax transformers. In First Conference on Language Modeling, Cited by: §1, §2.3, §5.2. S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. R. Narasimhan, and Y. Cao (2023) ReAct: synergizing reasoning and acting in language models. In The Eleventh International Conference on Learning Representations, External Links: Link Cited by: §1, §5.2. H. Zhou, A. Bradley, E. Littwin, N. Razin, O. Saremi, J. M. Susskind, S. Bengio, and P. Nakkiran (2024) What algorithms can transformers learn? A study in length generalization. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024, External Links: Link Cited by: §2.3, §5.1, §5.2. Appendix A Proofs on Plan Verification A.1 Proofs about Generalization over a Fixed Object Universe We restate Theorem 3.1 and then prove it. Theorem A.1. Let D be a planning domain and O a fixed set of objects. Consider the language L,OL_ D,O consisting of all sequences ⟨I,π,G⟩ I,π,G where π is a valid plan for the planning instance ⟨,O,I,G⟩ D,O,I,G . 1. (Delete-Free & Well-Formed) If D is delete-free or well-formed, then L,O∈C-RASP[Pos]L_ D,O -RASP[Pos]. 2. (STRIPS) There exist STRIPS domains and object sets such that L,O∉C-RASP[Pos]L_ D,O -RASP[Pos]. 3. (Conditional Effects) There exist domains with conditional effects such that L,OL_ D,O is neither star-free nor in C-RASP[Pos]C-RASP[Pos]. Proof of Statement 1. In this setting, the domain D and the set of objects O are fixed and finite. However, the initial state I and the goal state G are provided as part of the input sequence, and can vary per sample. Given this setting, all possible instances will have the set of all possible ground propositions P, and the same set of all possible ground actions A, where both P,AP,A are finite as well. Because of this we can directly refer to the necessary P, which is all the set of possible propositions, and A which is the entire set of ground actions (i.e. after the object names have been substituted into the predicates and action schemas taken from P and A respectively). The initial state I⊆PI P, and the goal state G are as defined in Section 2.1. We now give a recipe for constructing a C-RASP[Pos]C-RASP[Pos] program for any such input, where the given plan π is a valid action sequence and upon starting from I and taking all the actions in π all the goal conditions listed in G are met. We assume that the input sequence is as follows w=$I@π@G@w= I@π@G@. where, I=p1,po1,1,…,po1,pk1,p2,po2,1,…,po2,pk2,…I=p_1,po_1,1,…,po_1,pk_1, p_2,po_2,1,…,po_2,pk_2, … π=α1,o1,1,…,o1,k1,α2,o2,1,…,o2,k2,…π= _1,o_1,1,…,o_1,k_1, _2,o_2,1,…,o_2,k_2, … G=g1,go1,1,…,go1,gk1,g2,go2,1,…,go2,gk2,…G=g_1,go_1,1,…,go_1,gk_1, g_2,go_2,1,…,go_2,gk_2, … Thus, in the I block, the token ptp_t represents a predicate name, followed by pktpk_t (arity of the predicate) objects representing its arguments, Thus pt,pot,1…pot,pkt∈Pp_t,po_t,1… po_t,pk_t∈ P. Similarly, in the the token π block, αt _t is an action schema name, followed by ktk_t object tokens representing its arguments, and αt,ot,1…ot,kt∈A _t,o_t,1… o_t,k_t∈ A Finally the G block is also similar to the I block and therefore gt,got,1…got,gkt∈Pg_t,go_t,1… go_t,gk_t∈ P. We need to verify the plan by tracking the state of every ground proposition in P, making sure that all preconditions of a given action was always satisfied and also checking that all the goal conditions were indeed met by the end of the w. 1. We must identify which part of the input a token belongs to, using cumulative counts of separator tokens. CountSep(i):=#[j≤i]Q@(j)CountSep(i):= \# [j≤ i ]\;Q_@(j) Using this, we define the section selectors: • InInit(i):=(CountSep(i)==0)InInit(i):=(CountSep(i)==0) • InPlan(i):=(CountSep(i)==1)InPlan(i):=(CountSep(i)==1) • InGoal(i):=(CountSep(i)==2)InGoal(i):=(CountSep(i)==2) • End(i):=(CountSep(i)==3)End(i):=(CountSep(i)==3) The ==== syntax is equivalent to checking (CountSep(i)≤k)∧(CountSep(i)≥k)(CountSep(i)≤ k) (CountSep(i)≥ k). 2. We first identify, at any index i, whether an action has just completed and what that action is. Let a∈Aa∈ A be a specific ground action, defined by schema α and argument objects u1,…,uku_1,…,u_k. The action a ends at index i if the sequence of tokens ending at i matches the signature of a: token at i=uk,token at i−1=uk−1,…,token at i−k=αtoken at i=u_k, at i-1=u_k-1, …, at i-k=α In C-RASP, we can implement lookbacks using the query relation ψ(i,j)≡(i=j+Δ)ψ(i,j)≡(i=j+ ). For each ground action a, we define a boolean selector sequence Occursa(i)Occurs_a(i) that is true iff the action a ends at i: OccursActiona(i):=((#[j≤i,i=j+k]Qα(j)==1)∧⋀m=1k(#[j≤i,i=j+m]Qum(j)==1)∧InPlan(i))OccursAction_a(i):= (( \# [j≤ i,i=j+k ]\;Q_α(j)==1) _m=1^k( \# [j≤ i,i=j+m ]\;Q_u_m(j)==1) (i) ) This expression verifies the action schema name at offset k and every object argument umu_m at the correct offset. Since there are finitely many ground actions, we define one such line for every a∈Aa∈ A. Thus at every position i, at most only 1 ground action can ever be true. We do the same thing for every p∈Pp∈ P to match propositions listed in the initial and the goal state. (u1,…uku_1,… u_k representing the arguments of the proposition p, k the arity of the proposition). OccursInitialp(i):=((#[j≤i,i=j+k]Qp(j)==1)∧⋀m=1k(#[j≤i,i=j+m]Qum(j)==1)∧InInit(i))OccursInitial_p(i):= (( \# [j≤ i,i=j+k ]\;Q_p(j)==1) _m=1^k( \# [j≤ i,i=j+m ]\;Q_u_m(j)==1) (i) ) OccursGoalp(i):=((#[j≤i,i=j+k]Qp(j)==1)∧⋀m=1k(#[j≤i,i=j+m]Qum(j)==1)∧InGoal(i))OccursGoal_p(i):= (( \# [j≤ i,i=j+k ]\;Q_p(j)==1) _m=1^k( \# [j≤ i,i=j+m ]\;Q_u_m(j)==1) (i) ) 3. For every ground proposition p∈Pp∈ P, we identify the set of ground actions that add it, TPpTP_p, where TPp=a∈A|p∈eff(a)+TP_p=\a∈ A|p∈eff(a)^+\. These sets will be fixed and known a priori, given our fixed objects and domain. We define the cumulative count of additions for p at step i: MadeTruep(i):=(∑a∈TPp#[j≤i]OccursActiona(j))MadeTrue_p(i):=( _a∈ TP_p \# [j≤ i ]\;OccursAction_a(j)) We do the same for the set of actions that delete it FPp=a∈A|p∈eff(a)−FP_p=\a∈ A|p∈eff(a)^-\. MadeFalsep(i):=(∑a∈FPp#[j≤i]OccursActiona(j))MadeFalse_p(i):=( _a∈ FP_p \# [j≤ i ]\;OccursAction_a(j)) 4. Now, we define the truth value of a proposition p at step i. • Well-Formed: Because of well-formedness, the truth value of a proposition toggles (False → True → False). We compute the net flow (adds minus deletes) for each proposition at every step. If the proposition was in the initial state, then the net flow has to be 0, and if it was not then this net flow should be 11. Netp(i):=MadeTruep(i)−MadeFalsep(i)Net_p(i):=MadeTrue_p(i)-MadeFalse_p(i) Validp(i):=(OccursInitialp(i)∧Netp(i)==0)∨(¬OccursInitialp(i)∧Netp(i)==1)Valid_p(i):=(OccursInitial_p(i) _p(i)==0) ( _p(i) _p(i)==1) • Delete-Free: The proposition is true, if it was either already true (as it was in the initial state) or at least one action made it true. Validp(i):=OccursInitialp(i)∨(MadeTruep(i)≥1)Valid_p(i):=OccursInitial_p(i) (MadeTrue_p(i)≥ 1) 5. For every ground action a, let pre(a)+pre(a)^+, pre(a)−pre(a)^- define the list of positive and negative ground propositions for a given action. We need to check that all the preconditions are satisfied before the action effect takes place. We check the state of preconditions at i−1i-1 (the state before the effects of the action took place). If any of the preconditions are not met, we mark this position as invalid. PreCondPasseda(i):=⋀p∈pre(a)+(#[j≤i,i=j+1]Validp(j)⋀p∈pre(a)−(#[j≤i,i=j+1]¬Validp(j)PreCondPassed_a(i):= _p∈pre(a)^+( \# [j≤ i,i=j+1 ]\;Valid_p(j) _p∈pre(a)^-( \# [j≤ i,i=j+1 ]\; _p(j) InvalidActiona(i):=OccursActiona(i)∧¬PreCondPasseda(i)InvalidAction_a(i):=OccursAction_a(i) _a(i) The count of invalid actions by the end of w should be 0. AllActionsValid(i):=(∑a∈A#[j≤i]InvalidActiona(j)==0)AllActionsValid(i):=( _a∈ A \# [j≤ i ]\;InvalidAction_a(j)==0) 6. Finally, we need check if every goal condition is satisfied. We iterate over our ground propositions. For every proposition, either it does not appear in the goal or it is valid. GoalSat(i):=⋀p∈P¬OccursGoalp(i)∨Validp(i)GoalSat(i):= _p∈ P _p(i) _p(i) At the end token, we need to check, that all goals were met. AllGoalsMet(i):=End(i)∧AllActionsValid(i)∧(#[j≤i]¬GoalSat(i)==0)AllGoalsMet(i):=End(i) (i) ( \# [j≤ i ]\; (i)==0) Note that, in case negative goal conditions are present, we can check for invalidity of the underlying proposition, however the logic remains the same. Since A and P are finite, this program has a finite number of lines and operations. At the last position of our sequence, our program outputs True if the given input sequence was valid else not for any possible sequence in L,OL_ D,O. Hence, for both delete-free and well-formed, L,O∈C-RASP[Pos]L_ D,O -RASP[Pos]. ∎ For our negative results, we will show that there exist instances Π=⟨,O,I,G⟩ = D,O,I,G , where the language of all valid plans of just that instance L(Π)L( ) (therefore subsets of the full language L,OL_ D,O) are not contained in C-RASP[Pos]C-RASP[Pos]. Consequently, the language L,OL_ D,O itself is not in C-RASP[Pos]C-RASP[Pos]. Proof of Statement 2. Lin and Bercher (2022) showed that L(Π)L( ) when Π=⟨,O,I,G⟩ = D,O,I,G represents a STRIPS instance belongs to a strict subset of star free languages. Here we will show that there could be a STRIPS instance Π , where L(Π)∉C-RASP[pos]L( ) -RASP[pos]. Huang et al. (2025b) had rigorously showed that the star free language Σ∗be∗ ^*be^* (Σ=a,b,e =\a,b,e\), also known as the flipflop language is not in C-RASP[pos]C-RASP[pos]. Thus, we will now create a STRIPS instance Πff _f where L(Πff)=Σ∗be∗L( _f)= ^*be^*, which will thus prove our claim. Let the planning domain be ff=⟨,⟩ D_f= P, A where =active P=\active\, arity(active)=1arity(active)=1 and =a,ab,ae A=\a_a,a_b,a_e\. All three schemas share the argument set args()=xargs()=\x\ and empty preconditions pre()=∅pre()= . Their effects are: eff(a)=¬active(x)eff(a_a)=\ (x)\, eff(ab)=active(x)eff(a_b)=\active(x)\, eff(ae)=∅eff(a_e)= . Now we define the planning instance to be Πff=⟨ff,,∅,active()⟩ _f= D_f,\ k\, ,active( k) . This planning instance is a STRIPS instance, as by construction we did not violate any rules of being in STRIPS. The ground actions correspond directly to the alphabet Σ : a=a()a=a_a( k), b=ab()b=a_b( k), and e=ae()e=a_e( k). Note that since the preconditions are empty, all actions are applicable in every state. Let π∈Σ∗π∈ ^* be a sequence of actions π=σ1…σnπ= _1… _n. We track the state Si=succ(I,σ1…σi)S_i=succ(I, _1… _i). The ground proposition set is simply active()\active( k)\. Thus, there are only two possible states: ∅ (which we call OFF) and active()\active( k)\ (which we call ON). Since I=∅I= , the system starts in the OFF state. Based on the definitions of the ground actions each action regardless of the previous state acts as follows – a: eff(a)−=active()eff(a)^-=\active( k)\ removes the proposition, setting the state to off, b: eff(b)+=active()eff(b)^+=\active( k)\ adds the proposition, setting the state to on, e: eff(e)=∅eff(e)= acts as the identity function, leaving the state unchanged. A plan π is valid iff Sn⊧GS_n G, which means active()∈Snactive( k)∈ S_n (i.e., the final state is on). Consider the last occurrence of a non-e symbol in w. If w contains no a or b (i.e., w∈e∗w∈ e^*), the state remains I (off). The goal is not satisfied. If the last non-e symbol is a, the state becomes off at that step. Any subsequent e actions maintain the off state. The goal is not satisfied. If the last non-e symbol is b, the state becomes ON at that step. Any subsequent e actions maintain the ON state. The goal is satisfied. Therefore, w∈L(Πff)w∈ L( _f) if and only if w contains at least one b, and no a occurs after the last b. This corresponds exactly to the regular expression Σ∗be∗ ^*be^*. ∎ Proof of Statement 3. PARITYPARITY is the non star free regular language L=b∗(ab∗ab∗)∗L=b^*(ab^*ab^*)^* where Σ=a,b =\a,b\. Thus, a string w∈Lw∈ L, if it contains an even number of a’s. Huang et al. (2025b) rigorously showed that PARITY∉C-RASP[Pos]PARITY -RASP[Pos]. We will here show that the Lights Out domain, when defined with conditional effects (explained in Section D.1), can be reduced to PARITY, thus proving our claim. We begin by first defining a Lights Out planning instance. Definition A.2 (Lights Out with conditional effects). Let LO=(V,E)LO=(V,E) be a lights out board represented as a graph where V=v1,…,vnV=\v_1,…,v_n\ represents the set of cells (vertices) and E defines the connectivity (edges between the vertices). For any v∈Vv∈ V, let N[v]=u∈V∣(v,u)∈E∪vN[v]=\u∈ V (v,u)∈ E\∪\v\ be the closed neighborhood of v. Given an initial configuration of cells I⊆VI V that are on, we define the corresponding planning instance ΠLO=⟨,O,I,G⟩ _LO= D,O,I,G as follows: • The domain is =⟨,⟩ D= P, A . – The set of objects is empty, O=∅O= . – The predicates are propositional (arity 0), representing the state of each cell: =oni∣vi∈V P=\on_i v_i∈ V\ – The action schema correspond to pressing specific cells. Since the logic depends on the fixed graph topology, we define a schema for each cell: G=a1,…,an A_G=\a_1,…,a_n\ For each cell vk∈Vv_k∈ V, the schema aka_k is defined by: * args(ak)=∅args(a_k)= * pre(ak)=∅pre(a_k)= (actions are always applicable) * The effects eff(ak)eff(a_k) toggle the cell and its neighbors. For every vj∈N[vk]v_j∈ N[v_k], we include the following pair of conditional effects:888For compactness, we factorize conditions, with the semantics that all conditions that are true in the current state trigger their effects and that consistent sets of conditions must lead to consistent effect sets. This does not affect our results. onj \on_j\ ⊳¬onj \ _j\ ¬onj \ _j\ ⊳onj \on_j\ • The initial state is defined by the set of cells that are initially on: I=oni∣vi∈II=\on_i v_i∈ I\ • The goal is to switch all lights off: G=¬on1,…,¬onnG=\ _1,…, _n\ Algebraic Formulation of the State Space: To analyze the structure of the language L(ΠLO)L( _LO), we reformulate the state space algebraically. The specific structure of the conditional effects, which toggle the truth value of literals (flipping on to off and vice versa) motivates the use of a vector space over the finite field of two elements, 2=(0,1,+,⋅)F_2=(\0,1\,+,·). Let n=|V|n=|V|. We define an isomorphism ϕ:ℙ()→2nφ:P( P) _2^n where the k-th component is 1 if onk∈Son_k∈ S, and 0 otherwise. The initial state I maps to a vector b=ϕ(I)b=φ(I), and the goal state maps to 0→ 0. Recall that for each cell vkv_k, the action schema aka_k toggles the values of propositions in N[vk]N[v_k]. In 2F_2, toggling corresponds to addition by 1. Let uk∈2nu_k _2^n be the effect vector for action aka_k, where the j-th component is 1 if vj∈N[vk]v_j∈ N[v_k] and 0 otherwise. Thus the transitions in our lights out instance succ(S,ak)succ(S,a_k) are isomorphic to vector addition: ϕ(succ(S,ak))=ϕ(S)+ukφ(succ(S,a_k))=φ(S)+u_k. Definition A.3 (Plan Homomorphism). Let (Σ∗,⋅)( ^*,·) be the free monoid on Σ with the operation of string concatenation. Let (2n,+)(F_2^n,+) be the additive group of state vectors. We define a function h:Σ∗→2nh: ^* _2^n that maps a sequence of actions to its total effect vector: h(w=a1…ak)=∑m=1kumh(w=a_1… a_k)= _m=1^ku_m The function h(w)h(w) is a monoid homomorphism. Let w1,w2∈Σ∗w_1,w_2∈ ^*. The concatenation w1w2w_1w_2 is the sequence of actions in w1w_1 followed by the sequence of actions in w2w_2. The total effect vector is the sum of the effect vectors of all actions in the concatenated sequence. Since vector addition in 2nF_2^n is associative and commutative, this sum is equal to the sum of the effects of w1w_1 and the sum of the effects of w2w_2. Thus, h(w1w2)=h(w1)+h(w2)h(w_1w_2)=h(w_1)+h(w_2). Periodicity of the Solution Language: A plan w is a solution if, starting from state b, it reaches state 0→ 0. The final state is b+h(w)b+h(w). The condition for a valid plan is therefore b+h(w)=0→b+h(w)= 0, which in 2F_2 is equivalent to h(w)=bh(w)=b. Therefore, the language of valid plans L is precisely the preimage of the singleton set containing the initial state vector, b\b\: L=h−1(b)=w∈Σ∗∣h(w)=bL=h^-1(\b\)=\w∈ ^* h(w)=b\ The structure of L is determined by the kernel of the homomorphism h. Definition A.4 (Kernel). The kernel of the homomorphism h is the preimage of the identity element of the target group (2n,+)(F_2^n,+), which is the zero vector 0→ 0. ker(h)=h−1(0→)=w∈Σ∗∣h(w)=0→ (h)=h^-1( 0)=\w∈ ^* h(w)= 0\ The kernel is the sublanguage of all action sequences that have no net effect on the board state. Proposition A.5. For any action ai∈Σa_i∈ , the sequence aiai∈ker(h)a_ia_i∈ (h). Proof. Let uiu_i be the effect vector for action aia_i. By the homomorphism property, h(aiai)=h(ai)+h(ai)=ui+uih(a_ia_i)=h(a_i)+h(a_i)=u_i+u_i. In any vector space over 2F_2, for any vector v, v+v=0→v+v= 0. Therefore, h(aiai)=0→h(a_ia_i)= 0, which by definition means aiai∈ker(h)a_ia_i∈ (h). ∎ The existence of this non-trivial kernel proves that the solution language is periodic and not star-free. The syntactic monoid of the language contains non-trivial groups. For any action aia_i, the element represented by aia_i in the monoid has order 2, since applying it twice returns to the start. A monoid containing non-trivial group elements is, by definition, not aperiodic. This implies that the language of Lights Out plans is not star-free. Reduction from PARITY: Now, that we have established that L is not star free, we will further show that L(ΠLO)∉C-RASP[pos]L( _LO) -RASP[pos]. The proof proceeds by contradiction. Assume that the language of valid L(ΠLO)∈C-RASP[pos]L( _LO) -RASP[pos]. Consider the specific instance where the initial state is all lights off (I=∅I= ). The corresponding initial state vector is b=0→b= 0. The language of valid plans for this instance, L(ΠLO)L( _LO), is the kernel of the homomorphism h: L(ΠLO)=w∈Σ∗∣h(w)=0→=ker(h)L( _LO)=\w∈ ^* h(w)= 0\= (h) Our initial assumption implies L(ΠLO)∈C-RASP[pos]L( _LO) -RASP[pos], as it is simply a specific instance of the general problem. Let us fix three distinct actions: α,β,γ∈Σα,β,γ∈ . Let their effect vectors be eα,eβ,eγe_α,e_β,e_γ. We can always choose these actions such that eγ+eβ≠0→e_γ+e_β≠ 0. Consider the regular language RinterR_inter defined as: Rinter=((αα)∗(γβ)∗)∗R_inter=((α)^*(γβ)^*)^*. This language consists of all strings formed by concatenating blocks of (αα)(α) and (γβ)(γβ). As already established, applying an action twice leads to no action. Hence (αα)(α) is simply the identity and by construction (γβ)(γβ) does not map to the zero vector. Hence Rinter≡(ab)∗R_inter≡(ab)^* which is known to be in C-RASP[pos]C-RASP[pos] (Huang et al., 2025b). Since, C-RASP is closed under intersection and L(ΠLO)∈C-RASP[pos]L( _LO) -RASP[pos], we have R=L(ΠLO)∩Rinter∈C-RASP[pos]R=L( _LO)∩ R_inter -RASP[pos] i.e. R∈C-RASP[pos]R -RASP[pos]. The PARITY language over a,b\a,b\ can be written as a∗(ba∗b)∗a∗a^*(ba^*b)^*a^*. We link R to PARITY using an inverse homomorphism. Define ψ:a,b∗↦α,β,γ∗ψ:\a,b\^* \α,β,γ\^* as: ψ(a)=ααψ(a)=α, ψ(b)=γβψ(b)=γβ. The inverse homomorphism ψ−1(R)ψ^-1(R) is the set of all strings in a,b∗\a,b\^* that map into R under ψ. This language is precisely the set of strings over a,b\a,b\ with an even number of b’s. Note that ψ−1(R)=a∗(ba∗b)∗a∗=PARITYψ^-1(R)=a^*(ba^*b)^*a^*=PARITY. Now Lemma 42 in Huang et al. (2025b) shows that C-RASP[pos]C-RASP[pos] is closed under inverse images of morphisms where each symbol is mapped to a word of the same length 999This is precisely why we needed two actions γβγβ, as our identity action has two actions αα. This applies to ψ, because it maps both a and b to length-2 words. Thus since we have shown that R∈C-RASP[pos]R -RASP[pos], it implies that PARITY ∈C-RASP[pos] -RASP[pos]. However, Huang et al. (2025b) formally proved that PARITY is not in C-RASP[pos]C-RASP[pos]. This is a direct contradiction. ∎ Appendix B Proofs about Generalization over a Planning instances with growing number of objects We restate Theorem 3.6 and then prove it. Theorem B.1. Let D be a planning domain. Consider the language L_ D consisting of all possible sequences ⟨I,π,G⟩ I,π,G where π is a valid plan for some planning instance ⟨,O,I,G⟩ D,O,I,G . 1. (Delete-Free / Well-Formed) If D is delete-free or well-formed, then L∈C*-RASPL_ D *-RASP. In particular, generalization from both limited number of objects and plan lengths during training to a increased number of objects and plan lengths is expected. 2. (STRIPS / Conditional Effects) There exists STRIPS domains as well as domains with conditional effects for which L∉C*-RASPL_ D *-RASP. Generalization to instances with longer plans or increased number of objects is thus not expected. In particular, there are domains where L_ D subsumes FlipFlop or PARITY. We start by proving Statement 1 Proof. We represent a planning instance and plan as a sequence of tokens w. Along the same lines as Theorem A.1, the sequence is composed of the initial state I, and action names obtained by grounding action schemas from the finite set A and object names O per sample taken from the potentially infinite alphabet C, and the goal G. We will define A as follows. Each α∈α∈ A has the form nα(x1,…xarity(α))n_α(x_1,… x_arity(α)) where nαn_α is the name of the action schema, and and the xi∈args(α)x_i (α) refer to the placeholder objects. This set can be constructed from the action schemas A set by ignoring the schemas’ preconditions and effects, with a one to one mapping between A and A. It should be noted that we are constructing this set just for notational convenience and to avoid ambiguity. We write it as w=$I@π@G@w= I@π@G@. where, I=np1,po1,1,…,po1,pk1,p2,po2,1,…,po2,pk2,…I=n_p_1,po_1,1,…,po_1,pk_1, p_2,po_2,1,…,po_2,pk_2, … π=nα1,o1,1,…,o1,k1,α2,o2,1,…,o2,k2,…π=n_ _1,o_1,1,…,o_1,k_1, _2,o_2,1,…,o_2,k_2, … G=ng1,go1,1,…,go1,gk1,g2,go2,1,…,go2,gk2,…G=n_g_1,go_1,1,…,go_1,gk_1, g_2,go_2,1,…,go_2,gk_2, … In the I block, the token nptn_p_t represents a predicate name, followed by pktpk_t (arity of the predicate) objects representing its arguments. Thus each npt,pot,1…pot,pktn_p_t,po_t,1… po_t,pk_t represents a ground proposition where the proposition name and object structure are taken from P, and each object that has been instantiated is taken from O. The key difference here is that P, the set of all ground propositions is now infinite, and hence cannot be used. Similarly, in the π block, nαtn_ _t is an action schema name, followed by ktk_t object tokens representing its arguments. Therefore, nαt,ot,1…ot,ktn_ _t,o_t,1… o_t,k_t follows the structure of an nαt(x1,…,xarity(αt))∈n_ _t(x_1,…,x_arity( _t))∈ A. Finally the G block is also similar to the I block and therefore ngt,got,1…got,gktn_g_t,go_t,1… go_t,gk_t. For nαtn_ _t, nptn_p_t and ngtn_g_t, the objects that follow it are taken from the infinite pool of objects O. Thus, in addition to the ground propositions, the number of ground actions are also infinite. We will be constructing C*-RASP[Pos]C*-RASP[Pos] programs to verify action preconditions and goals for our positive cases. Note that unlike in C-RASP, here we will not be able to use object names inside the QσQ_σ operator to check for the presence of a specific object at the current position (owing to the increased number of objects), and will instead rely on the match predicate to help us resolve our issue. 1. Section Identification: we must identify which part of the input a token belongs to, using cumulative counts of separator tokens. CountSep(i):=#[j≤i]Q@(j)CountSep(i):= \# [j≤ i ]\;Q_@(j) • InInit(i):=(CountSep(i)==0)InInit(i):=(CountSep(i)==0) • InPlan(i):=(CountSep(i)==1)InPlan(i):=(CountSep(i)==1) • InGoal(i):=(CountSep(i)==2)InGoal(i):=(CountSep(i)==2) • End(i):=(CountSep(i)==3)End(i):=(CountSep(i)==3) The ==== syntax is not explicitly listed in C*-RASP[Pos]C*-RASP[Pos], but it is equivalent to checking (c(i)≤1)∧(c(i)≥1)(c(i)≤ 1) (c(i)≥ 1). 2. Precalculated Sets based on D: Since our D is fixed, we can precalculate the following sets for every predicate p∈p and thus have them be plugged into our program whenever we want: • TPpTP_p: The subset of action names along with placeholder object arguments α in A that have p in their add-effects (eff(α)+eff(α)^+). • FPpFP_p: The set of action names along with placeholder object arguments α∈α∈ A that have p in their delete-effects (eff(α)−eff(α)^-). • PrepPre_p: The set of action names along with placeholder arguments α∈α∈ A with p in their preconditions. 3. Check presence of Action/Predicate: To check the presence of a specific action/ predicate, we can use our local function from j. Currα(i)=#[j≤i,i=j+arity(α)]Qnα(j)≥1Curr_α(i)= \# [j≤ i,i=j+arity(α) ]\;Q_n_α(j)≥ 1 Currp(i)=#[j≤i,i=j+arity(p)]Qnp(j)≥1Curr_p(i)= \# [j≤ i,i=j+arity(p) ]\;Q_n_p(j)≥ 1 We can still use Q here as the number of predicates and action names are taken from our fixed alphabet. 4. Match predicate: We have to determine if two different subsequences refer to the same ground proposition, and since our object universe is variable, object names cannot be directly compared against a fixed list. Thus, we compare them exclusively through their positions relative to the object names. Consider a mapping function μα,β,p:1,…,kα→1,…,kβ _α,β,p:\1,…,k_α\→\1,…,k_β\, where α∈α∈ A has p∈p∈ P listed as a precondition and β∈β∈ A has p∈p∈ P listed in its effects. So μα,β,p(m)=n _α,β,p(m)=n implies that we want to map the m-th argument of α with the n-th argument of β to check how each of these map their arguments to p. We need this, as the mapping of the arguments of the underlying predicate to α and β could be different. We define the match predicate χα,β,p(i,j) _α,β,p(i,j) to be true if the ground action nα,o1,…,okαn_α,o_1,…,o_k_α ending at index i and action nβ,o1,…,okβn_β,o_1,…,o_k_β ending at index j match on the arguments of p. Since we only have access to the full argument list at the end of the action span due to causal masking, we define the offsets relative to i and j: χα,β,p(i,j):=Currα(i)∧Currβ(j)∧⋀m=1arity(p)(ci−kα+m=cj−kβ+n) _α,β,p(i,j):=Curr_α(i) _β(j) _m=1^arity(p)(c_i-k_α+m=c_j-k_β+n) where n=μα,β,p(m)n= _α,β,p(m). We note that all such offsets m,nm,n pairs will be constant and fixed according to a domain and can thus be plugged into our C*-RASP[Pos]C*-RASP[Pos] program. We can similarly define χα,Init,p(i,j) _α,Init,p(i,j) to be true, if the ground action nα,o1,…,okαn_α,o_1,…,o_k_α ending at i with a ground proposition np,o1,…,oarity(p)n_p,o_1,…,o_arity(p) ending at position j is listed in the initial state. χα,Init,p(i,j):=Currα(i)∧Currp(j)∧⋀m=1arity(p)(ci−kα+m=cj−kp+n) _α,Init,p(i,j):=Curr_α(i) _p(j) _m=1^arity(p)(c_i-k_α+m=c_j-k_p+n) With such match predicates, we will be able to match grounded actions and propositions, irrespective of the exact identities of the underlying objects. Thus, we will henceforth in the proof, be able to directly reason and interact with grounded actions and propositions listed in our w. We will be using α,pα,p in our indexing, but those C*-RASP variables will be true for every ground instance of the corresponding α,pα,p. 5. Precondition Check at every action: For a specific action instance α at i and a specific precondition p of α, we compute three values: (a) Provided by Init: Does the initial state contain the required ground proposition? Vinit,α,p(i):=#[j<i](InInit(j)∧χα,Init,p(i,j))V_init,α,p(i):= \# [j<i ]\; (InInit(j) _α,Init,p(i,j) ) The check for being in initial is required, so as to not match with propositions listed in G. (b) Provided by Plan (Adds): How many times has this proposition been added by previous actions? Vadd,α,p(i):=∑β∈TPp#[j<i,χα,β,p(i,j)]V_add,α,p(i):= _β∈ TP_p \# [j<i, _α,β,p(i,j) ]\; (c) Removed by Plan (Deletes): How many times has this proposition been deleted? Vdel,α,p(i):=∑β∈FPp#[j<i,χα,β,p(i,j)]V_del,α,p(i):= _β∈ FP_p \# [j<i, _α,β,p(i,j) ]\; We combine these to check if precondition p is satisfied for action α at step i: • Case A: Delete-Free. In a delete-free domain, FPp=∅FP_p= , so Vdel(i)=0V_del(i)=0. The precondition is satisfied if the proposition was ever established: Satisfiedα,p(i):=(Vinit,α,p(i)+Vadd,α,p(i)≥1)Satisfied_α,p(i):=(V_init,α,p(i)+V_add,α,p(i)≥ 1) • Case B: Well-Formed. In a well-formed domain, the truth value of a proposition toggles cleanly. A proposition is true if it was in Init and not net-deleted, or not in Init and net-added. The current truth value is: CurrentValα,p(i):=Vinit,α,p(i)+Vadd,α,p(i)−Vdel,α,p(i)CurrentVal_α,p(i):=V_init,α,p(i)+V_add,α,p(i)-V_del,α,p(i) Since the domain is well-formed, this sum will always be either 0 (False) or 1 (True). Thus: Satisfiedα,p(i):=(CurrentValα,p(i)==1)Satisfied_α,p(i):=(CurrentVal_α,p(i)==1) We note that for negative precondition requirements, the satisfaction check above would be changed to the value to be equal to 0. Whether a precondition requirement is positive or negative is known apriori as well, and hence one can aptly set 0 (for negative precondition) or 1 (positive precondition) here. We mark an action as valid, if all the preconditions are satisfied. Validα(i)=⋀p∈pre(α)Satisfiedα,p(i)Valid_α(i)= _p (α)Satisfied_α,p(i) We check at the final token of the entire input sequence, that we are indeed at the end and that we found no invalid actions so far. AllActionsValid(i):=End(i)∧⋀α∈(#[j≤i]¬Validα(j)==0)AllActionsValid(i):=End(i) _α∈ A( \# [j≤ i ]\; _α(j)==0) 6. Finally, we check if all goal conditions are met. We iterate over all predicates p∈p∈ P. For each predicate p, we perform validity checks at every position in the block where the goal proposition is of the type p (each such proposition may have different objects). We can construct a similar match predicate as before, χGoal,β,p(i,j) _Goal,β,p(i,j) to match a goal requirement at i with an action β at j (where j≤ij≤ i). We can also construct χGoal,Init,p(i,j) _Goal,Init,p(i,j), here in fact the entire proposition to be matched will be listed in the same way in the goals as in the initial state. For a specific goal proposition at index i (the index denotes the end of that goal proposition), we compute its validity: (a) Initial Status: Ginit,p(i):=#[j≤i,χGoal,Init,p(i,j)]G_init,p(i):= \# [j≤ i, _Goal,Init,p(i,j) ]\; (b) Added: Gadd,p(i):=∑β∈TPp#[j≤i,Currβ(j)∧χGoal,β,p(i,j)]G_add,p(i):= _β∈ TP_p \# [j≤ i,Curr_β(j) _Goal,β,p(i,j) ]\; (c) Deletes: Gdel,p(i):=∑β∈FPp#[j≤i,Currβ(j)∧χGoal,β,p(i,j)]G_del,p(i):= _β∈ FP_p \# [j≤ i,Curr_β(j) _Goal,β,p(i,j) ]\; The goal ending at i is satisfied if: GoalSatp(i):=(Ginit,p(i)+Gadd,p(i)−Gdel,p(i)==1)GoalSat_p(i):=(G_init,p(i)+G_add,p(i)-G_del,p(i)==1) (Or ≥1≥ 1 for Delete-Free). If i is not a goal token for p, we define GoalSatp(i)GoalSat_p(i) to be by default true (or ignore it in the final count). We note that for negative goal conditions, the conditions for satisfaction above would be flipped to equating with 0 (for both well-formed and delete-free). We explicitly mark goals that were unsatisfied: UnsatisfiedGoal(i):=InGoal(i)∧⋁p∈(Currp(i)∧¬GoalSatp(i))UnsatisfiedGoal(i):=InGoal(i) _p∈ P(Curr_p(i) _p(i)) At the final token, we verify that the total count of unsatisfied goal tokens is zero. AllGoalsMet(i):=End(i)∧(#[j≤i]UnsatisfiedGoal(j)==0)AllGoalsMet(i):=End(i) ( \# [j≤ i ]\;UnsatisfiedGoal(j)==0) The final program output is Φvalid:=AllActionsValid∧AllGoalsMet _valid:=AllActionsValid . ∎ We next proceed to proving Statement 2 Proof. Statements 2, 3 of Theorem 3.1 already showed that even the set of objects is fixed, universe domains with STRIPS and domains with conditional effects have instances where the language of valid plans is isomorphic to the FlipFlop and Parity language. As Theorem 3.5 showed both FlipFlop and Parity cannot be expressed in C*-RASP. Thus, the current statement falls out as a corollary based on these facts established already. ∎ Appendix C Learning Framework C.1 Model of the transformer with Extended Alphabet Parameterization Our parameterization and setup closely follows Huang et al. (2025b), with the crucial distincition being in the way we allow an extended alphabet (to account for the increase of objects during test). We focus on transformers with causal masking. We assume the transformer T is parameterized by the following; • A finite alphabet Σ and a token embedding matrix for the finite alphabet ∈ℝ|Σ|×d E ^| |× d. • Width of the transformer being d∈ℕd . • A context width N(T)∈ℕ∪+∞N(T) ∪\+∞\. • Positional encodings t∈ℝd:1≤t<N(T)+1\ p_t ^d:1≤ t<N(T)+1\. • An extended embedding collection k∈ℝd:1≤k<N(T)+1∈ℕ\c_k ^d:1≤ k<N(T)+1 \ representing the learnable embeddings for the extended alphabet. Note that while indexed by integers similar to positions, these are distinct parameters from the positional encodings. • Depth L, heads H, and layer matrices l,h,l,h,l,h,l,l,l\ K_l,h, Q_l,h, V_l,h, A_l, B_l, b_l\ as standard. • An unembedding matrix ∈ℝ|Ω|×d U ^| |× d Input Structure, Embeddings & Positional Embedding We define the vocabulary as the disjoint union Ω=Σ∪$ = ∪\ \, where $ is a special reserved start symbol. Thus, a input string w is a sequence w=(w1,…,wn)w=(w_1,…,w_n), where the first token is the special start symbol, w1=$w_1= , and the rest of the sequences can be either a σ∈Σσ∈ or a symbol c∈c . Similar to Huang et al. (2025b), we study NoPE (No Positional Encoding) and Absolute Positional Encodings (APE) that has learned per-position embedding vectors 1,…,N p_1,…, p_N. We encode an input x of length |x|=k≤N|x|=k≤ N using positional encodings 1+o,…,k+o p_1+o,…, p_k+o where o is an offset such that k+o≤Nk+o≤ N, and require that the transformer correctly performs the task independently of the offset o≥0o≥ 0. The offsets try to mimic the fact that language models typically need to solve tasks appearing at aribitrary positions in a long context. Positions outside of the input are considered empty. Computation of Initial State Let w be an input sequence of length n such that n≤N(T)n≤ N(T). We consider two kinds of offset again, where op,oc≥0\o_p,o_c\≥ 0 are the positional offsets and the character offsets such that n+op≤N(T)n+o_p≤ N(T) and n+oc≤N(T)n+o_c≤ N(T) as well (ensuring the sequence fits within the context window when shifted). The input to the first transformer layer, denoted as i(0)∈ℝdy_i^(0) ^d for the token at position i (where 1≤i≤n1≤ i≤ n), is defined as the sum of the token’s embedding and its positional encoding: i(0)=wi+i+opif wi∈Σ(Finite Token)k+oc+i+opif wi∈ and wi has value k(Extended Token)y_i^(0)= casesE_w_i+p_i+o_p&if w_i∈ (Finite Token)\\ c_k+o_c+p_i+o_p&if w_i and w_i has value k (Extended Token) cases (1) The motivation for training the extended alphabet with offsets is to enable reasoning over the increasing alphabet and still be able to fit everything in the same context window, akin to the motivation of using offsets for absolute positional encodings. Attention logits, at query position i and key position j are computed as ai,j(l,h)=(j(l−1))Tl,hTl,hi(l−1)for 1≤j≤i≤|x|;l=1,…,L;h=1,…,Ha_i,j^(l,h)=( y_j^(l-1))^T K_l,h^T Q_l,h y_i^(l-1)\ \ for\ 1≤ j≤ i≤|x|;\ l=1,…,L;\ h=1,…,H (2) We assume standard softmax attention, but incorporate scaling with log|x| |x| following prior work finding it necessary to theoretically represent sparse functions and circumvent theoretical limitations of soft attention (Chiang and Cholak, 2022; Edelman et al., 2022): i(l):=i(l−1)+∑h=1H∑j=1iexp(log|x|⋅ai,j(l,h))l,hj(l−1)∑j=1iexp(log|x|⋅ai,j(l,h)) Y_i^(l):= y_i^(l-1)+ _h=1^H _j=1^i ( |x|· a^(l,h)_i,j ) V_l,h y_j^(l-1) _j=1^i ( |x|· a^(l,h)_i,j ) (3) After each attention block, the activations are passed through a one-layer MLP: i(l):=i(l)+l⋅ψl(li(l)+l) y_i^(l):= Y_i^(l)+ B_l· _l( A_l Y_i^(l)+ b_l) (4) where we allow similar to Huang et al. (2025b) the activation function ψl _l to be, in each coordinate, either ReLU or Heaviside. In addition, we also allow the activation function f(x)=1/x+ϵf(x)=1/x+ε, where ϵε is a small constant to avoid division by 0. Owing to the universal approximation theorem (Cybenko, 1989), such non-linear activations can be approximated arbitrarily closely by ReLU MLPs. We do this to use to have an MLP that could invert values akin to the strategy in Theorem 1 of Kazemnejad et al. (2023).101010The prevalent use of the Universal Approximation theorem notwithstanding, precisely understanding how such functions are learned on the basis of more commonly used activation functions such as ReLU in MLPs inside transformers is largely an open and highly challenging question, which we leave to future work. To keep our model close to Huang et al. (2025b), we also omit layer norm as they do and also assume an infinite-precision setup for the activations, with the restriction that attention logits (2) and the output of the exp(⋅) (·) function are both rounded to p fractional bits of precision before further processing. This mild restriction was put in Huang et al. (2025b) to prevent tiny changes in attention patterns to potentially snowball into large changes in the output due to infinite precision; it is also adopted in Izzo et al. (2025). A transformer T maps strings x (|x|≤N(T)|x|≤ N(T)) to vectors of next-token prediction logits, T(x,op,oc)∈ℝ|x|×|Ω|T(x,o_p,o_c) ^|x|×| |, where T(x,op,oc)i=i(L)T(x,o_p,o_c)_i= U y_i^(L) (i=1,…,|x|i=1,…,|x|) for the unembedding matrix ∈ℝ|Ω|×d U ^| |× d, and op,oco_p,o_c are the offsets. Let ℱ(Ω)F( ) be the set of all maps f mapping x to f(x)∈ℝ|x|×|Ω|f(x) ^|x|×| |. C.1.1 Product Functions Our theory extends the framework for length generalization of transformers with absolute positional encodings, where the width may grow with the input length, to account for cases where transformers also reason based on token identities from an unbounded vocabulary. Similar to Huang et al. (2025b), we cannot view the ground-truth function as realized by a single transformer. Even if one assigned such a transformer an infinite number of positional encodings, it would effectively only distinguish between a bounded number of positions because the width of the model is bounded. Analogously, even if we equip the transformer with an increasing number of token embeddings, a single finite-width transformer can only act on this infinite alphabet in a limited fashion—primarily by matching identities of token symbols rather than memorizing infinite arbitrary features. Thus, just as Huang et al. (2025b) derived a parameterization to convert sequences of transformers operating on longer sequences into a single limiting object, we derive a similar parameterization to unify sequences of transformers equipped with increasing alphabet sizes. We reuse the key technical idea to reparameterize the transformer in terms of product functions—inner products of parameter vectors mediated by parameter matrices. However, in our setting, we explicitly distinguish between pairwise interactions (α) and single-site potentials (β). The pairwise interactions (α) capture operations operations where two kinds of embedding interact (either position-position, position-token, or token-token).For instance in attention scores or with the use of Input-Output predictions (Token-Token): iT1,hT1,hj p_i^T K_1,h^T Q_1,h p_j σT1,hT1,hτ E_σ^T K_1,h^T Q_1,h E_τ (5) iT2,hT2,h1j p_i^T K_2,h^T Q_2,h V_1 p_j τT31σ U_τ^T V_3 V_1 E_σ Meanwhile, the single-site potentials (β) capture interactions where such two kinds of embeddings do not interact. For instance while considering MLP operations: (1)s,⋅Ti ( A_1)_s,·^T p_i (1)s,⋅Tσ ( A_1)_s,·^T E_σ (6) τT(1)⋅,s U_τ^T( B_1)_·,s τT2(1)⋅,s U_τ^T V_2( B_1)_·,s Definition C.1 (Product Parameterization). More formally, this parameterization is defined as follows: For l=1,…,Ll=1,…,L,: start= _start= i:i∪ω:ω∈Ω \ p_i:i\∪\ E_ω:ω∈ \ l= _l= (l)⋅,s:s=1,…,d \( B_l)_·,s:s=1,…,d\ ℐl= _l= (l)s,⋅:s=1,…,d \( A_l)_s,·:s=1,…,d\ = = ω:ω∈Ω \ U_ω:ω∈ \ = = start∪⋃l=1Ll _start∪ _l=1^LVO_l ℐ= = ⋃l=1Lℐl _l=1^LVI_l = = Vl1,h1,…,Vlk,hk: 0≤k≤L;l1<⋯<lk; 1≤hi≤H \\V_l_1,h_1,…,V_l_k,h_k\\ \ :\ \ 0≤ k≤ L;\ \ l_1<…<l_k;\ \ 1≤ h_i≤ H\ Given a transformer T, define the Pairwise Interaction Potentials (α) and Single-Site Potentials (β): αl,h,1,2,,attn:= α^attn_l,h,S_1,S_2, v, w:= T(∏S∈1S)Tl,hTl,h(∏S∈2S)∈ℝ v^T ( _S _1S )^T K_l,h^T Q_l,h ( _S _2S ) w for 1≤l≤L; 1≤h≤H;,∈;1,2∈ for 1≤ l≤ L;\ \ 1≤ h≤ H;\ \ v, w ;\ \ S_1,S_2 α,,unembed:= \ α^unembed_S, u, w:= T(∏S∈S)∈ℝ u^T ( _S S ) w for ∈;∈start;∈ for u ;\ \ w _start;\ \ S β,,mlp:= \ β^mlp_S, v, w:= T(∏S∈S)∈ℝ v^T ( _S S ) w for ∈ℐ;∈;∈ for v ;\ \ w ;\ \ S β,,unembed:= \ β^unembed_S, u, w:= T(∏S∈S)∈ℝ u^T ( _S S ) w for ∈;∈ℐ;∈ for u ;\ \ w ;\ \ S where the matrix product over a set ∈S ∏S∈S _S S (7) is computed in descending order of layers; with the S associated with the lowest layer at the right. For instance, ∏S∈V1,h,V3,h′,V4,h′S=V4,h′V3,h′V1,h _S∈\V_1,h,V_3,h ,V_4,h \S=V_4,h V_3,h V_1,h (8) Remark C.2. Here, we exemplify the Product Parameterization. α1,h,∅,∅,i,σattn= α^attn_1,h, , , p_i, E_σ= iT1,hT1,hσ p_i^T K_1,h^T Q_1,h E_σ α2,h,1,h′,∅,i,jattn= α^attn_2,h,\ V_1,h \, , p_i, p_j= iT1,h′T2,hT2,hj p_i^T V_1,h ^T K_2,h^T Q_2,h p_j α3,h′,1,h,τ,σunembed= α^unembed_\ V_3,h , V_1,h\, U_τ, E_σ= τT3,h′1,hσ U_τ^T V_3,h V_1,h E_σ β∅,(1)s,⋅,imlp= β^mlp_ ,( A_1)_s,·, p_i= (1)s,⋅Ti ( A_1)_s,·^T p_i β1,h,(3)s,⋅,σmlp= β^mlp_\ V_1,h\,( A_3)_s,·, E_σ= (3)s,⋅T1,hσ ( A_3)_s,·^T V_1,h E_σ β3,h′,2,h,τ,(1)⋅,sunembed= β^unembed_\ V_3,h , V_2,h\, U_τ,( B_1)_·,s= τT3,h′2,h(1)⋅,s U_τ^T V_3,h V_2,h( B_1)_·,s Remark C.3. For ease of notation, we have not restricted the layers from which different vector parameters are taken in the definition of α and β; hence, they will also include products that are not relevant to actual computations, such as iT2,hT1,h′T1,h′3,h′j p_i^T V_2,h^T K_1,h ^T Q_1,h V_3,h p_j (9) where a vector of the form V3,h′jV_3,h p_j cannot actually feed into the computation of queries in the first layer. This is simply for simplicity of notation; such products will not impact results and is consistent with the parameterization used in Huang et al. (2025b). C.1.2 Symbolic Limit Transformers We define locality and translation invariance by generalizing the notions from (Huang et al., 2025b) beyond positional encodings to also cover token embeddings: Definition C.4 (Locality & Translation Invariance). For any embedding types ,∈,x,y∈\ p, c\, if the product functions obey the following, then the transformer is said to be local and translation invariant: 1. Locality & Translation Invariance for Related Types: When inputs share a type (Pos-Pos or Tok-Tok), then their interactions vanish if the distance exceeds a bandwidth Δ∈ℕ 111111… implies that the rest of the parameters are the same on both sides : |k−m|>Δ⟹α…,k,m=0|k-m|> _…,x_k,x_m=0 (10) Translation Invariance implies that for all shifts δ, the behaviour remains the same: α…,k,m=α…,k+δ,m+δ _…,x_k,x_m= _…,x_k+δ,x_m+δ (11) 2. Translation Invariance for Unrelated Types: When inputs differ in type (Pos-Tok) or act singly (MLP-Pos), the interaction cannot pick out specific absolute indices from a structure it is unrelated to. Thus, the interaction collapses to a Constant. For any kx_k, if the other term is of a different type or fixed: β…,k=Candα…,k,m=C _…,x_k=C _…,x_k,y_m=C (12) We will use the parameterization just defined to translate sequences T1,T2,T3,…T_1,T_2,T_3,… of transformers running on inputs of length 1,2,3,…1,2,3,… to limiting transformer-like objects that are applicable at all input lengths, while keeping width d bounded even if the widths of TnT_n, and thus the allowed number of tokens diverge to infinity. We will define this limit transformer like object as follows: Definition C.5. A Symbolic Limit Transformer is a transformer T where: 1. N(T)=+∞N(T)=+∞ 2. Positional encodings tt∈ℕ\ p_t\_t and extended alphabet embeddings kk∈\ c_k\_k have globally bounded norms in ℋH. There exists Cemb>0C_emb>0 such that: supt∈ℕ‖t‖≤Cembandsupk∈‖k‖≤Cemb _t \| p_t\|≤ C_emb _k \| c_k\|≤ C_emb (13) 3. All weight matrices ∈l,h,l,h,l,h,l,l, W∈\ K_l,h, Q_l,h, V_l,h, A_l, B_l, U\ are bounded linear operators on ℋH, where their spectral norms are bounded. 4. For every layer l, the MLP projects to a finite-dimensional subspace. There exists dff∈ℕd_f such that l:ℋ→ℝdff A_l:H ^d_f and l:ℝdff→ℋ B_l:R^d_f . 5. The behavior of this transformer is governed by the set of scalar product functions defined earlier (Definition C.1). Each product function must evaluate to a number in p-bit precision, for some fixed p∈ℕp . Crucially, these functions must satisfy the Locality and Translation Invariance Constraints defined in Definition C.4 Length generalization will be linked to expressibility by Symbolic Limit Transformers. A Limit Transformer, as defined in Huang et al. (2025b) could use positional information through bounded-width and bounded-precision positional encodings i p_i, and additionally through potentially more complicated functions ϕl,h _l,h, where a function f:ℕ×ℕ→ℝf:N×N would be “translation-invariant” if f(i,j)=f(i+τ,j+τ),∀i≤j,∀τ≥0f(i,j)=f(i+τ,j+τ),∀ i≤ j,∀τ≥ 0, and “local” if there is τ such that f(i,j)=0f(i,j)=0 when j>i+τj>i+τ. Symbolic Limit Transformers use positional information in the same way. However since now they have access to an infinite character vocabulary, we put some restrictions in the ways in which these character tokens can interact with each other. Thus we can perform operations like checking the equality of character tokens, or check the equality of character tokens that lie near each other in their embedding spaces. The other points in the definition are simply to keep the outputs of each of the operations be finite, and representable in finite precision.d The parameterization in terms of inner products permits a translation from a transformer T to a bounded-width Symbolic Limit Transformer (Statement 3 of Proposition C.12 in the Appendix). C.2 Definition of Inference Procedure To define the inference procedure, we specify the following hypothesis class at each input length n: Definition C.6 (Hypothesis Class). For each n=1,2,3,…n=1,2,3,…, define the hypothesis class Θn _n as the set of transformers T (as defined in Section C.1) where (1) N(T)=nN(T)=n, (2) each parameter vector and matrix of T is represented at p bits of precision, for some p∈ℕp , (3) each product function involving only positional encodings is translation-invariant. (4) each product function involving only the extended character alphabet is also translation-invariant. Note that the width d of the transformers T∈ΘnT∈ _n is unconstrained. We keep the requirement of Huang et al. (2025b) of wanting the contributions of positional encodings i p_i (that vary with position) to the transformer’s computations to be offset-independent. This is a stronger requirement than for the input-output behavior to be offset-independent: we ask for the transformer’s “algorithm” itself to be the same across offsets. We extend this logic to the character alphabet in requirement (4). Here, the goal is to prevent the model from overfitting to specific absolute values of the extended tokens. By enforcing translation invariance on the embeddings k c_k, we ensure that the model only ever uses relative differences between token indices (to do operations like local matching or exact equality checks). This effectively restricts the transformer to learning algorithms based on pattern matching—such as identifying when a current token matches one from the past—without allowing it to attach arbitrary semantics to specific tokens in the infinite sequence. Our inference procedure will use a regularizer ℛR favoring simpler hypotheses. It should be noted that while our extension of Limit Transformers is more complex than in Huang et al. (2025b), the regularizer we will use would be simpler. It should be noted that this trades off a complexity in a theoretical mathematical construct – that is just a tool for proving statements about standard transformers – with an increase in simplicity in the conditions of the regularizer we use in the idealized model of learning. The following will be sufficient: Definition C.7 (Regularizer). Let T∈ΘnT∈ _n, thus N(T)=nN(T)=n. Define ℛ(T)R(T) as the sum of (1) L+HL+H; (2) the precision p used in Definition C.6; the precision p used for rounding attention logits and the output of exp(⋅) (·) (Section C.1); (3) maxl,h‖l,hTl,h‖ _l,h\| K_l,h^T Q_l,h\|; maxl,h‖l,h‖ _l,h\| V_l,h\|; maxl‖l‖F _l\| A_l\|_F, ‖l‖F\| B_l\|_F; ‖\| U\|; (4) maxi‖i‖2 _i\| p_i\|_2, maxσ‖σ‖2 _σ\| E_σ\|_2, maxl‖l‖2 _l\| b_l\|_2; (5) the term: ζ(T)=∑l=1L∑h=1H∑1,2∈(∑j=1N(T)|αl,h,1,2,1,jAttn|2+∑k=1|Ω||αl,h,1,2,1,kAttn|2)+∑∈∑k=1|Ω||α,1,kunembed|2ζ(T)= _l=1^L _h=1^H _S_1,S_2 ( _j=1^N(T) |α^Attn_l,h,S_1,S_2, p_1, p_j |^2+ _k=1^| | |α^Attn_l,h,S_1,S_2, E_1, E_k |^2 )+ _S _k=1^| | |α^unembed_S, U_1, E_k |^2 (14) We note that this regularizer omits a term rank(l,h)rank( V_l,h) used in Huang et al. (2025b); we do not need it and can thus simplify by removing it. As in Huang et al. (2025b), the idea of (14) is to discourage accidental attention between far-away positions and interactions between character token embeddings that do not appear together during training, which could hamper length generalization. These form a subset of the product functions formally defined earlier (Definition C.1). Due to translation invariance, such a term entails a bound on products for all pairs i,j p_i, p_j (i≤ji≤ j) and i,j c_i, c_j) entering causal attention. While such a regularizer is not part of standard training, standard initialization tends to lead to bounded values for (14) when d is large. As shown in Huang et al. (2025b), it thus captures an implicit bias of standard initialization and training. Additionally, by removing the bounded rank constraint on the regularizer, we enforce lesser restrictions on it, making it a more plausible estimate of standard initialization and training compared to what was used in Huang et al. (2025b). Importantly, the width d does not explicitly enter ℛR; as a consequence, for any sufficiently large C, the number of transformers Tn∈ΘnT_n∈ _n with ℛ(Tn)≤CR(T_n)≤ C is infinite, simply because d is not constrained. Nonetheless, this regularizer will be sufficient for identification under our idealized inference procedure, which observes the input-output behavior of the target function f on inputs of length ≤n2≤ n2 and selects a transformer T with maximal context window n, T∈ΘnT∈ _n that exactly fits that input-output behavior while minimizing the regularizer ℛ(T)R(T). At inference time, when the transformer TnT_n processes input lengths up to n, it may encounter extended tokens k c_k that were effectively unseen during the “training” phase (which is restricted to smaller indices). This can be thought of as adding random embeddings at test time. However, these tokens would be constrained by the translation invariance and locality conditions of the hypothesis class Θn _n, and the algorithm learned by the transformer would not be able to rely on the specific identity of these new tokens, and instead would have to use the same relative algorithms learned on the smaller alphabet (such as checking for equality i=j c_i= c_j or local proximity). This setup models the transformer’s ability to generalize simpler algorithmic primitives (like pattern matching) to completely novel vocabulary items. The inference procedure is then defined in analogy to Huang et al. (2025b): Definition C.8 (Inference Procedure). Given a function f∈ℱ(Ω)f ( ), the Inference Procedure obtains a sequence of transformers T1∈Θ1,T2∈Θ2,…T_1∈ _1,T_2∈ _2,… as follows. Define UnU_n as the set of T∈ΘnT∈ _n matching the behavior of f on the restricted domains of inputs constrained in the following ways relative to n. 1. The sequence length of any input x is |x|≤n2|x|≤ n2. 2. The extended character tokens ck\c_k\ appearing in x fall within a range of size at most n2 n2. Specifically, if Kx=k∈ℕ∧k∈[1,n]∣ck appears in xK_x=\k k∈[1,n] c_k appears in x\ is the set of indices in input x, then max(Kx)−min(Kx)≤n2 (K_x)- (K_x)≤ n2. Then choose Tn∈UnT_n∈ U_n such that ℛ(Tn)≤1n+infT∈Unℛ(T)R(T_n)≤ 1n+ _T∈ U_nR(T) (15) Importantly, we only ask TnT_n to match the behavior of f up to length n2 n2 with context window sizes of the character embeddings involved also restricted to n2 n2, formalizing the idea of training on shorter inputs and testing on longer ones; our identifiability guarantee will provide conditions under which TnT_n will end up matching f correctly up to length n – representing length generalization. In (15), we do not simply ask for minimizing the regularizer, as the set of elements of UnU_n with ℛ(T)R(T) smaller than a given value need not be finite and thus a minimum need not be attained by any TnT_n. As in (Huang et al., 2025b), we take the testing length to be twice the training length, but the analysis works whenever the training length diverges to infinity. C.3 Main Result: Convergence of Inference Procedure Our main result asymptotically characterizes length generalization under the inference procedure from Definition C.8. For functions representable by Symbolic Limit Transformers, we guarantee that any run of the Inference Procedure will ultimately achieve length generalization, so that transformers with context length n and access to a vocabulary range of n from C chosen to fit the target function on inputs with length ≤n2≤ n2 and vocabulary range of n/2n/2 from C will, when n is sufficiently large, also perform correctly at all lengths ≤n≤ n. Formally, we obtain the following analogue of Theorem 7 in Huang et al. (2025b): Theorem C.9 (Guaranteed Length Generalization in the Limit). Let f∈ℱ(Ω)f ( ). Then the following are equivalent: 1. f is expressible by a Symbolic Limit Transformer. 2. (Guaranteed Length Generalization) Applying the Inference Procedure from Definition C.8 to f generates a sequence T1,T2,…T_1,T_2,… with supn=1,2,3,…ℛ(Tn)<∞ _n=1,2,3,…R(T_n)<∞, for which there is some N0N_0 such that, for all m>N0m>N_0, TmT_m matches f on all inputs of any length k≤mk≤ m. Remark C.10. We note that a Symbolic limit transformer T∞T_∞ representing f need not itself be offset-invariant. It is sufficient to have T∞(x,0)=f(x)T_∞(x,0)=f(x) (16) Statement 2 of Proposition C.12 shows that such a function has a sequence of transformers Tn∈ΘnT_n∈ _n which are offset-invariant, even without assuming T∞T_∞ to be offset-invariant. High-Level Proof Sketch Our proof here tracks the proof of Theorem 7 of Huang et al. (2025b) really closely. The core logic of both ours and theirs is the same, and the difference primarily lies in the fact that our learning setting has different definitions for the regularizer, our limiting object, inference procedure etc. The core idea is that if f is expressible by a Symbolic Limit Transformer satisfying then, even though the Inference Procedure produces infinitely many distinct transformers T1,T2,…T_1,T_2,… (with increasing numbers of position and token embeddings), these can only traverse a finite set of underlying algorithms, each described by some Symbolic Limit Transformer. The property of translation invariance and locality ensure that the parameter count effectively remains finite, as its position-related parameters as well as the extended character related parameters can be fully specified in terms of finite product functions. The regularizer bounds the complexity of the symbolic Limit Transformers as well, thus keeping the set of algorithms traversed finite. For 1⇒ 2, given a sequence generated by the Inference Procedure, we show that ℛR stays bounded and use the compactness property to show that a subsequence exhibits behavior equivalent to f. To show that, in fact, all possible sequences TnT_n generated by the Inference Procedure ultimately exhibit behavior equivalent to f, when n is large, we show that subsequences failing to length-generalize would exhibit increasing attention scores between far-away positions and between characters whose embeddings are far apart, as input length increases. Due to the penalty on such scores in ℛR, any such sequence would, for large n, need to have a higher value of ℛR than sequences avoiding such an increase. For 2⇒ 1, we obtain the Symbolic Limit Transformer from the compactness property applied to the sequence generated by the Inference Procedure. The penalty on pairwise interactions enforces that the transformer satisfy the locality property, and as noted in the Remark C.10, offset invariance is not necessary for T∞T_∞. Preliminaries and Formal Proof For our formal proof, we will set up some definitions that will help provide translations between ordinary transformers and Symbolic Limit Transformers. It will be useful to define a complexity metric applicable to Symbolic Limit Transformers. Definition C.11. For a Limit Transformer T∞T_∞, define ℛ∞(T∞)R_∞(T_∞) as the sum of 1. The number of layers and heads (L+HL+H) 2. dMLPd_MLP 3. the precision p used for expressing the output of any product function, and the precision p used for rounding attention logits and the output of exp(⋅) (·) (Section C.1). 4. The total L2 norm of the pairwise product functions. This corresponds to the limit (N(T)→∞N(T)→∞) of the ζ(T)ζ(T) term in Definition C.7: ζ(T∞)= ζ(T_∞)= ∑l=1L∑h=1H∑1,2∈(∑j=1∞|αl,h,1,2,1,jAttn|2+∑k=1∞|αl,h,1,2,1,kAttn|2) _l=1^L _h=1^H _S_1,S_2 ( _j=1^∞ |α^Attn_l,h,S_1,S_2, p_1, p_j |^2+ _k=1^∞ |α^Attn_l,h,S_1,S_2, E_1, E_k |^2 ) +∑∈∑k=1∞|α,1,kunembed|2 + _S _k=1^∞ |α^unembed_S, U_1, E_k |^2 Proposition C.12. The following are true. 1. Specification by Product functions: The input-output behavior of a (symbolic-limit or normal) transformer is fully specified by its product functions. Thus, for any choice of product functions that respects translation invariance and locality, there is a corresponding symbolic-limit transformer, and also (restricting to any N(T)N(T)) a corresponding transformer implementing these. 2. Symbolic Limit Transformer to a standard Transformer: For any symbolic-limit transformer T∞T_∞ and any context window length N0N_0, there is a corresponding transformer T∈ΘN0T∈ _N_0 with N(T)=N0N(T)=N_0 that exactly matches the product functions of T∞T_∞ restricted to inputs up to size N0N_0. Furthermore, ℛ(T)≤ℛ∞(T∞)R(T) _∞(T_∞). 3. Standard Transformer to a Symbolic Limit Transformer: For any transformer T, there is a corresponding symbolic limit transformer T∞T_∞ that has the same product functions up to N(T)N(T), and R∞(T∞)R_∞(T_∞) is bounded in terms of R(T)R(T). 4. Let C>0C>0 be a constant. There is a finite set of symbolic limit transformers denoted CQ_C, such that any T∞T_∞ with R∞(T∞)<CR_∞(T_∞)<C agrees with an element of CQ_C on all product functions except possibly those representing pairwise interactions between embeddings of related types (Position-Position, Token-Token, etc.). Proof. 1. This directly follows from the definition of our Product Parameterization (Defintion C.1). Since the output of the model is a composition of scalar products, specifying those products specifies the model. 2. We can simply construct T to evaluate the product functions of the Symbolic Limit Transformer for indices i,j≤N0i,j≤ N_0. Since ℛ∞(T∞)R_∞(T_∞) is the sum of squared norms over the infinite domain, and ℛ(T)R(T) is the sum over the finite domain N0N_0, non-negativity of the terms involved implies ℛ(T)≤ℛ∞(T∞)R(T) _∞(T_∞). 3. We construct T∞T_∞ from T as follows: • For the product functions terms involving unrelated types or involving just a single position or single character from the extended set, we extend the values observed in T constantly to infinity (because of our assumption of locality). • For pairwise terms (related types), since the product functions are translation invariant, we take all available distances from T and use that to fill in the values of our product functions wherever the relative distance between the terms is smaller than the available distances, and set the other product functions to 0 i.e. when the relative distance was not observed in T. This extension thus, also ensures the infinite sum of squares converges, keeping ℛ∞(T∞)R_∞(T_∞) bounded by the finite sum ℛ(T)R(T). 4. We focus on the product functions excluded from our exception. More specifically the single-site β terms, or the α terms where Position-Token interactions happen. By the definition of the Symbolic Limit Transformer, these functions must satisfy the Locality constraint. Thus, they must evaluate to a constant value K everywhere to ensure the limit object is well-defined. Additionally, since ℛ∞(T∞)<CR_∞(T_∞)<C: 1. The contribution of such product functions to the regularizer would be |K|2|K|^2. Thus, |K|2≤ℛ∞(T∞)<C|K|^2 _∞(T_∞)<C, which implies |K|<C|K|< C. 2. Since the precision p is fixed, K must be a multiple of 2−p2^-p. There are only finitely many discrete multiples of 2−p2^-p in the bounded interval [−C,C][- C, C]. Since the transformer has a fixed, finite number of layers and heads, there are only finitely many such constant product functions to assign. Thus, the set of possible configurations for these components, CQ_C, is finite. ∎ The following definitions will be used: Definition C.13. If T∈ΘiT∈ _i, then define ℛ−(T)R_-(T) to be ℛ(T)R(T) minus the term in Eq. (14). That is, ℛ(T)=ℛ−(T)+ζ(T)R(T)=R_-(T)+ζ(T) (17) where ζ(T)=∑l=1L∑h=1H∑1,2∈[∑j=1N(T)|αl,h,1,2,1,jAttn|2+∑k=1|Ω||αl,h,1,2,1,kAttn|2]+∑∈∑k=1|Ω||α,1,kunembed|2ζ(T)= _l=1^L _h=1^H _S_1,S_2 [ _j=1^N(T) |α^Attn_l,h,S_1,S_2, p_1, p_j |^2+ _k=1^| | |α^Attn_l,h,S_1,S_2, E_1, E_k |^2 ]+ _S _k=1^| | |α^unembed_S, U_1, E_k |^2 The following lemma will be used for both directions of our main theorem C.9, and is an adaptation of Lemma 17 from Huang et al. (2025b). The proof technique is the same, the main thing that changes is that the terms in the derivation refer to our framework. We try to keep our notation and argumentation similar to theirs to enable quick readability for a reader familiar with Huang et al. (2025b). For readers unfamiliar with Huang et al. (2025b), the following set of proofs are still self contained, and our remarks are meant to simply acknowledge that the following proof argument style is not novel, and is simply an application of it in our context. Lemma C.14. Let T1,T2,…T_1,T_2,…, where Tn∈ΘnT_n∈ _n, be a sequence generated by the Inference Procedure based on the functional behavior of a function f∈ℱf , and such that supn=1,2,3,…ℛ(Tn)<∞ _n=1,2,3,…R(T_n)<∞ (18) Then f is expressible by a Symbolic Limit Transformer and there is some N0N_0 such that, for all m>N0m>N_0, TmT_m matches f on all inputs of length k≤mk≤ m. Proof. We will refer to all sets of pariwise functions α with related types with Φrelated _related. We will use a superscript Φrelated(T) _related^(T), to indicate the symbolic limit transformer whose relevant product functions of this type are being talked about. We can use statement 3 of Proposition C.12 to get Limit Transformers T~1,T~2,… T_1, T_2,… such that supiℛ∞(T~i)<∞ _iR_∞( T_i)<∞ for the sequence of transformers T1,T2,…T_1,T_2,… generated by our Inference Procedure. In similar vein to Huang et al. (2025b), we thus get, T~i(x,o)=Ti(x,o),∀i,o,x;|x|+o≤i T_i(x,o)=T_i(x,o),\ \ \ \ ∀ i,o,x;|x|+o≤ i (19) and, each T~i T_i possesss the same set of pairwise product functions as TiT_i up to length i, which means Φrelated(T~i)=Φrelated(Ti) _related^( T_i)= _related^(T_i) Each T~i T_i has (i) the collection of its constant product functions (single site potentials and cross-type interactions) (i) the collection of pairwise decaying product functions. We will write (T~i) P( T_i) for the collection of the constant product functions T~i T_i. Let A:=supiℛ∞(T~i)<∞A:= _iR_∞( T_i)<∞. Then (T~):ℛ∞(T~)≤A\ P( T):R_∞( T)≤ A\ and by Proposition C.12 (Statement 4) only a finite number of Symbolic Limit Transformer parameter settings (T~i) P( T_i) will be traversed as i→∞i→∞. If each product function involved in Φrelated(T~i) _related^( T_i) also traversed a finite set of distinct functions as i→∞i→∞, then the number of T~i T_i itself is finite would have been finite. Each of these functions are local according to definition; however, a priori, they might not be local for any single finite τ (where τ is the distance beyond which product functions evaluate to 0) across the different T~i T_i. We will now show that all such functions are in fact local for a single finite τ. For any given n, ℛ(Tn)∈[infT∈Un(ℛ(T)),1n+infT∈Un(ℛ(T))]R(T_n)∈ [ _T∈ U_n(R(T)), 1n+ _T∈ U_n(R(T)) ] Again similar to Huang et al. (2025b), here, our infT∈Unℛ(T) _T∈ U_nR(T) is bounded and monotonically increasing in n, and thus it converges to some limit, say R~ R. As 1/n→01/n→ 0, the interval width tends to 0, and therefore the squeeze theorem gives ℛ(Tn)→R~R(T_n)→ R. For each τ and each n, we consider Dn(τ) D_n(τ) =∑f∈Φrelated(T~n)∑i=1min(n,τ)|f(T~n)(1,i)|2≤ℛ(Tn) = _f∈ _related^( T_n) _i=1 (n,τ)|f^( T_n)(1,i)|^2≤R(T_n) The f(T~n)(1,i)f^( T_n)(1,i) refers to every single product function, where the interactions happen between a term i and a term 11. Therefore for positional attention terms (piT…pjp_i^T… p_j), this implies interactions between p1p_1 and pip_i, for extended alphabet attention terms it implies interaction between c1c_1 and cic_i, and for unembedding terms it implies interactions between some U1U_1 and EiE_i. Each such f has precision bounded in terms of ℛ(Tn)R(T_n), and thus Dn(τ):n∈ℕ\D_n(τ):n \ is a discrete set. Consequently, every accumulation point of the sequence (Dn(τ))n∈ℕ(D_n(τ))_n must be attained for infinitely many values of n. Having established this, we now look at ℛ−(Tn)R_-(T_n) from Equation 17. The following derivation (Equation 20 to Equation 26) are verbatim the same as Huang et al. (2025b), with the key difference being in the interpretation of the terms here. Let R0:=lim infn→∞ℛ−(Tn)R_0:= _n→∞R_-(T_n) (20) and let ν1,ν2,ν3,… _1, _2, _3,… be such that limi→∞ℛ−(Tνi)=R0 _i→∞R_-(T_ _i)=R_0 (21) Then, for some D0D_0, limi→∞Dνi(νi)=D0 _i→∞D_ _i( _i)=D_0 (22) and R~=limn→∞ℛ(Tn)=limi→∞ℛ(Tνi)=R0+D0 R= _n→∞R(T_n)= _i→∞R(T_ _i)=R_0+D_0 (23) Indeed, D0=lim supn→∞Dn(n)D_0= _n→∞D_n(n) (24) because121212As noted by (Huang et al., 2025b), if an+bna_n+b_n converges and an,bna_n,b_n are bounded, then the limit lim(an+bn) (a_n+b_n) equals lim supan+lim infbn a_n+ b_n. For, assume lim supan+lim infbn>lim(an+bn) a_n+ b_n> (a_n+b_n) (similar if >> is replaced by <<). Then let i(n)i(n) be a subsequence such that ai(n)→lim supana_i(n)→ a_n. Then lim(an+bn)=lim(ai(n)+bi(n))=lim supan+limbi(n)≥lim supan+lim infbn>lim(an+bn) (a_n+b_n)= (a_i(n)+b_i(n))= a_n+ b_i(n)≥ a_n+ b_n> (a_n+b_n), contradiction. D0+R0=limn→∞(ℛ−(Tn)+Dn(n))=lim infn→∞ℛ−(Tn)+lim supn→∞Dn(n)D_0+R_0= _n→∞(R_-(T_n)+D_n(n))= _n→∞R_-(T_n)+ _n→∞D_n(n) (25) Define, for each τ∈ℕτ , D∞(τ)=lim infi→∞Dνi(τ)D_∞(τ)= _i→∞D_ _i(τ) (26) Because all functions in Φrelated _related have bounded precision in terms of ℛ(Tn)R(T_n), and our function above is monotonically increasing, there must be τ∞ _∞ such that D∞(τ∞)=limτ→∞D∞(τ)D_∞( _∞)= _τ→∞D_∞(τ). We now define a sequence Tn′T_n where for each n, lim infj→∞Dνj(n)=D∞(n)≤D∞(τ∞) _j→∞D_ _j(n)=D_∞(n)≤ D_∞( _∞) As all functions in Φrelated _related have bounded precision, there are infinitely many νi _i such that Dνi(n)=lim infj→∞Dνj(n)D_ _i(n)= _j→∞D_ _j(n). Hence, we can select i(n)∈ℕi(n) such that νi(n)≥n _i(n)≥ n and Dνi(n)(n)=lim infj→∞Dνj(n) D_ _i(n)(n)= _j→∞D_ _j(n) For each n, let Tn′T_n be the restriction of Tνi(n)T_ _i(n) to positions up to n. Since Tνi(n)T_ _i(n) agrees with f up to length νi(n)/2≥n/2 _i(n)/2≥ n/2, it follows that Tn′T_n also agrees with f up to length n/2n/2. Once again, the derivation from here till the point where we show that D∞(τ∞)=D0D_∞( _∞)=D_0 are verbatim the same as Huang et al. (2025b). Then lim supn→∞ℛ(Tn′)= _n→∞R(T_n )= lim supn→∞ℛ−(Tn′)+Dνi(n)(n) _n→∞R_-(T_n )+D_ _i(n)(n) = = lim supn→∞ℛ−(Tνi(n))+D∞(τ∞) _n→∞R_-(T_ _i(n))+D_∞( _∞) = = R0+D∞(τ∞) R_0+D_∞( _∞) Since TnT_n was created by the Inference Procedure, we have lim supn→∞ℛ(Tn′)≥limn→∞ℛ(Tn) _n→∞R(T_n )≥ _n→∞R(T_n) (27) On the other hand, since ℛ(Tn′)≤ℛ(Tνi(n))R(T_n ) (T_ _i(n)), we also have lim supn→∞ℛ(Tn′)≤limn→∞ℛ(Tn) _n→∞R(T_n )≤ _n→∞R(T_n) (28) giving lim supn→∞ℛ(Tn′)=limn→∞ℛ(Tn)=D0+R0 _n→∞R(T_n )= _n→∞R(T_n)=D_0+R_0 (29) Hence, R0+D∞(τ∞)= R_0+D_∞( _∞)= lim supn→∞ℛ(Tn′) _n→∞R(T_n ) = = limn→∞ℛ(Tn) _n→∞R(T_n) = = R0+D0 R_0+D_0 and D∞(τ∞)=D0D_∞( _∞)=D_0. Now assume there are infinitely many n such that the functions in as each function in Φrelated(Tn) _related^(T_n) are not τ∞ _∞-local, hence, infinitely many n such that Dn(n)≥Dn(τ∞)+2−2pD_n(n)≥ D_n( _∞)+2^-2p. Then: D0= D_0= lim supn→∞Dn(n) _n→∞D_n(n) ≥ ≥ lim supn→∞Dn(τ∞)+2−2p _n→∞D_n( _∞)+2^-2p ≥ ≥ lim infi→∞Dνi(τ∞)+2−2p _i→∞D_ _i( _∞)+2^-2p = = D0+2−2p D_0+2^-2p This is a contradiction. The first inequality follows from Dn(n)≥Dn(τ∞)D_n(n)≥ D_n( _∞) whenever n≥τ∞n≥ _∞, as for every n, Dn(⋅)D_n(·) is monotonically increasing. The second holds because (νi)i∈ℕ( _i)_i is a subsequence of (n)n∈ℕ(n)_n ; hence a limsup over the larger sequence gives an upper bound of liminf over the subsequence. Thus with this, we can claim that all the functions in Φrelated(T~n) _related^( T_n) have to be local for a uniform τ∞ _∞. The remainder of the proof follows Huang et al. (2025b); we repeat it here for self-containedness. The attention product functions involving only positions or only extended characters have products bounded by (R0)4(R_0)^4, and are bounded in absolute value by ≤‖i‖2‖l,hT‖‖l,h‖‖j‖2≤(R0)4≤\| p_i\|_2\| K_l,h^T\|\| Q_l,h\|\| p_j\|_2≤(R_0)^4 or ≤‖i‖2‖l,hT‖‖l,h‖‖j‖2≤(R0)4≤\| c_i\|_2\| K_l,h^T\|\| Q_l,h\|\| c_j\|_2≤(R_0)^4. The unembedding terms are in fact bounded by a smaller polynomial ‖Ui‖‖Ej‖≤(R0)2\|U_i\|\|E_j\|≤(R_0)^2, therefore each function value is expressed at precision bounded by a polynomial in R0R_0. There are only a finite set of functions that satisfy these properties and are are local for this τ∞ _∞. We had already shown that the constant components of T~ T are from a finite set, and now we have also shown that the pairwise product functions are also from a finite set. Hence, we know that, :=T~i:i∈ℕQ:=\ T_i:i \ is finite. Let ∞⊆Q_∞ be the set of Limit Transformers that equal T~i T_i for infinitely many different i. By definition of the Inference Procedure, every element of ∞Q_∞ is functionally equivalent to f at all input lengths. Because Q is finite, there is N0N_0 such that T~i∈∞ T_i _∞ for each i≥N0i≥ N_0. Hence, TiT_i is functionally equivalent to f at all lengths ≤i≤ i as soon as i exceeds the threshold N0N_0. ∎ We now prove the theorem. Proof of the Theorem. With Lemma C.14, now both directions of the theorem are just corollaries. 2⇒ 1: This directly follows from Lemma C.14. 1⇒ 2: By Statement 2 of Proposition C.12, there exists a standard normal transformer T^i∈θi T_i∈ _i which can be derived from the ground truth Symbolic Limit Transformer T~∞ T_∞ for each i=1,2,3,…i=1,2,3,…, such that ℛ(T^i)R( T_i) is uniformly bounded, i.e. lim supi→∞ℛ(Ti)≤lim supi→∞ℛ(T^i)<∞ _i→∞R(T_i)≤ _i→∞R( T_i)<∞ (30) where TiT_i refers to the sequence generated by Inference Procedure in Lemma C.14. Lemma C.14 now provides a threshold N0>0N_0>0 such that the sequence of inferred transformers stablise to some Symbolic Limit Transformer, which we define as computing a function g. Now for all m>N0m>N_0, TmT_m computes g on inputs of length ≤m≤ m. However, by construction of the inference procedure, TmT_m is also constrained to match the ground truth function f on inputs of length ≤m≤ m. Therefore for all m>N0m>N_0, and all inputs x, such that |x|≤m|x|≤ m, we have g(x)=Tm(x)=f(x)g(x)=T_m(x)=f(x). Since this holds for arbitrarily large m, we conclude that g≡fg≡ f. Thus, for all m>N0m>N_0, the inferred transformer TmT_m matches f. ∎ C.4 Result for NoPE Transformers As in (Huang et al., 2025b), we obtain an analogous result for NoPE transformers: Corollary C.15. For ease of the reader, we mark the differences to Theorem C.9 in green font. Let f∈ℱ(Ω)f ( ). Then the following are equivalent: 1. f is expressible by a Symbolic Limit Transformer where all i≡0 p_i≡ 0 2. (Guaranteed Length Generalization) Consider the inference procedure from Definition C.8 applied to f with ℛR while constraining all i≡0 p_i≡ 0, generating a sequence T1,T2,…T_1,T_2,…. For any such sequence, there is some N0N_0 such that, for all m>N0m>N_0, TmT_m matches f on all inputs of any length k≤mk≤ m, and supn=1,2,3,…ℛ(Tn)<∞ _n=1,2,3,…R(T_n)<∞. Proof. The statement 2 of Proposition C.12 still stands, but instead when translating a Symbolic Limit Transformer to an ordinary transformer, since the positional encodings are taken to be zero, i≡0 p_i≡ 0, the product functions involving these positions become 0. Similarly in the statement 3 of Proposition C.12 also stands, but when i≡0 p_i≡ 0 in a transformer, the resulting Symbolic Limit Transformer also has zero positional encodings and zero outputs for all associated positional product functions. Specifically, the pairwise product functions restricted to position-position interactions will be identically zero, and the single site potentials or the cross related types will have fewer product functions. The finiteness and compactness arguments in Lemma C.14 then rely solely on the interactions between extended alphabet characters (Token-Token interactions) and the remaining constant components. Since these are a subset of the components bounded in the general proof, the convergence and finiteness arguments apply equally. The proof of Theorem C.9 thus applies directly to show Corollary C.15. ∎ C.5 Statement of Main Theorem for Arbitrary Training Lengths Analogous to how Huang et al. (2025b) extended their generalization results from length n/2n/2 to n to arbitrary scaling of train vs test lengths, we do the same. Definition C.16. A training length is a function t:ℕ→ℕt:N satisfying limt→∞t(n)=+∞ _t→∞t(n)=+∞ and t(n)≤nt(n)≤ n for all n. If t(n)t(n) is a training length, then the t(n)t(n)-Inference Procedure determines Tn∈Θ(n)T_n∈ (n) to match f at all inputs of lengths ≤t(n)≤ t(n) while minimizing ℛ(Tn)R(T_n) up to 1n 1n. The special case of t(n)=n2t(n)= n2 is the Inference Procedure from Definition C.8. The definition above is an adaptation of Definition 22 from Huang et al. (2025b), except the inference procedure and regularizer mentioned in the definition will refer to the versions we defined earlier. With this, we can state the following. Theorem C.17. Let f∈ℱ(Ω)f ( ). The following are equivalent: 1. f is expressible by a Symbolic Limit Transformer. 2. Let t(n)t(n) be any training length. Then the t(n)t(n)-Inference Procedure will output solutions T1,T2,…T_1,T_2,… such that, for some N0N_0, for all m>N0m>N_0, TmT_m matches f at all lengths ≤m≤ m. Intuitively, this says that, when selected to fit the behavior of f on sufficiently long inputs of length t(n)t(n), the output of the Inference Procedure will generalize to unboundedly longer inputs of length n, where n can be arbitrarily larger than t(n)t(n). Corollary C.18. Assume f∈ℱ(Ω)f ( ) is not expressible by a Symbolic Limit Transformer. Then, for some training length t(n)t(n), the t(n)t(n)-Inference Procedure outputs a sequence TnT_n where infinitely many TnT_n fail to match f at length n. The proof here tracks the proof of Theorem 23, Corollary 24 & Remark 25 from Huang et al. (2025b) which are applicable directly here, with the difference being that the terms refer to our learning model. We restate it for completeness. Remark C.19. Theorem C.17 differs from Theorem C.9 in the following aspects. • Here, we talk about length generalization for all arbitrary training lengths t(n)t(n), not specifically n2 n2. • We do not ask for supiℛ(Ti)<∞ _iR(T_i)<∞, but ask for TnT_n to ultimately length generalize. Proof of Theorem C.17. 1⇒ 2 The proof of Theorem C.9 remains valid in this direction without any changes, as we never used the fact that training length was half the context size. 2⇒ 1 We will show that if f is not expressible by a Symbolic Limit Transformer, then generalization would not happen. Thus, assume f is not expressible by a Symbolic Limit Transformer. We use the same arguments as in Lemma C.14. Consider any sequence Tn∈ΘnT_n∈ _n that matches f and has lim infn→∞ℛ(Tn)<∞ _n→∞R(T_n)<∞. This sequence need not be generated by our Inference procedure. If we translating each of these to a Symbolic Limit Transformer we once again will get a sequence where, except the pairwise product functions, only a finite number of settings will be traversed. Now, as in the proof of Lemma C.14, we use D∞(τ)D_∞(τ) to construct a sequence of Symbolic Limit Transformers that are local for a single τ. Now since f is not expressible by a Symbolic Limit transformer, lim infn→∞ℛ(Tn)=∞ _n→∞R(T_n)=∞ († ) for any sequence Tn∈ΘnT_n∈ _n that matches f. Because if this was not true, then by Lemma C.14, we would get a Symbolic Limit Transformer. We will now construct a sequence of failure points nkn_k and and a training length t(n)t(n). Let k∈ℕk represent a target training length. For any such fixed k, it is possible to match f on inputs of length ≤k≤ k with a finite regularization cost. Let UkU_k be an upper bound on this regularization cost required to fit f on inputs of length k, considering any transformer of any size n>kn>k. We set UkU_k such that for any n>kn>k, there exists a transformer in θn _n, matching f on the prefix k with cost ≤Uk≤ U_k. Because the cost to match f at length n diverges to infinity (as established above), for any fixed k, we can find a nkn_k sufficiently large such that any transformer T∈θnkT∈ _n_k that matches f at the full length nkn_k must have a regularization cost strictly greater than Uk+1U_k+1. We construct this sequence nkn_k inductively ensuring nk>nk−1n_k>n_k-1. We now define the training length function t(n)t(n) based on these intervals: t(n)=maxk:nk≤nt(n)= \k:n_k≤ n\. This function is a step function, for n∈[nk,nk+1)n∈[n_k,n_k+1), the training length is constant at t(n)=kt(n)=k. Note that t(n)→∞t(n)→∞ as n→∞n→∞. Consider the behavior of the Inference Procedure at specific test lengths n=nkn=n_k. The procedure receives a training constraint of length t(nk)=kt(n_k)=k. It seeks to minimize ℛ(T)R(T) subject to matching f on length k. By definition of UkU_k, there exists a transformer T∗∈ΘnkT^*∈ _n_k that matches f on length k with ℛ(T∗)≤Uk+ϵR(T^*)≤ U_k+ε. However, by our choice of nkn_k, any transformer that matches f on the full length nkn_k requires a cost >Uk+1>U_k+1. Since the Inference Procedure minimizes cost, it will prefer T∗T^* (cost ≈Uk≈ U_k) over any solution that generalizes to nkn_k (cost >Uk+1>U_k+1). Thus, the inferred transformer TnkT_n_k will match the training data (length k) but fail to match the target function f at the test length nkn_k. Since this occurs for infinitely many k, the inference procedure fails to length generalize ∎ C.6 Length Generalization for C-RASP Any C*-RASP or C*-RASP[Pos]C*-RASP[Pos] program can be translated to a Symbolic Limit Transformer. If the positional functions ψ(i,j)ψ(i,j) and all the constants of the type δk,γk _k, _k from our Match predicate (definition 3.3) are not used (τk _k can still be used), then then length generalization will be guaranteed even without positional embeddings. If any of them are required to be used, then length generalization is only guaranteed with the use of absolute positional embeddings. We say a Symbolic Limit Transformer T accepts an input if the value in the last dimension in the last position of the output is greater than 0, and rejects otherwise. Theorem C.20. For every C*-RASP program P with local functions Ψ , there exists a Symbolic Limit Transformer T∞T_∞ such that for all w∈Σ∗w∈ ^*, P accepts w iff T∞T_∞ accepts $w w. Furthermore: 1. If P uses neither local positional relations ψ(i,j)ψ(i,j) nor spatial offsets in Match Predicates (i.e., δk=γk=0 _k= _k=0 for all matches, though τk≠0 _k≠ 0 is allowed), then T∞T_∞ requires no positional encodings (NoPE), and length generalization is guaranteed for NoPE transformers. 2. If P uses local positional relations ψ(i,j)ψ(i,j) or non-zero spatial offsets (δk≠0 _k≠ 0 or γk≠0 _k≠ 0), then T∞T_∞ utilizes absolute positional encodings, and length generalization is guaranteed for APE transformers. As a consequence, the Inference Procedure will ultimately length-generalize on inputs from a function f expressible by a C*-RASP[Pos]C*-RASP[Pos] program. If the C-RASP program requires no positional functions as said above, then length generalization will succeed even with NoPE transformers. Remark C.21. We note that the Symbolic Limit Transformer T∞T_∞ provided by the proof of Theorem C.20 emulates the C-RASP program P at zero offset: That is, P accepts w iff a predetermined entry in the last output dimension of T∞($w,0)T_∞( w,0) is above some threshold. In principle, its computations may not be offset-invariant, i.e., for the constructed T∞T_∞, the output T∞($w,o)T_∞( w,o) may depend on o. Importantly, the proof of Theorem C.9 does not require a Symbolic Limit Transformer computing f to be offset-invariant, but just requires it to compute f when the offset is zero. This is because Statement 2 of Proposition C.12 ensures that, for any Symbolic Limit Transformer T∞T_∞, even if it is not offset-invariant, there are transformers Tn∈ΘnT_n∈ _n whose behavior matches T∞(⋅,0)T_∞(·,0). Proof. We will also show that a Symbolic Limit Transformer T∞T_∞ simulates a C*-RASP program P if for every operation PkP_k of P there is a dimension dkd_k in T such that when Pk(i)P_k(i) when run on w is true iff T∞($w)i+1,dk=1T_∞( w)_i+1,d_k=1 (and 0 otherwise) for Boolean operation and Pk(i)=cP_k(i)=c iff T∞($w)i+1,k=ci+1T_∞( w)_i+1,k= ci+1 for count operations. We will use induction on the length of P. All boolean cases and all but one counting case are identical to Huang et al. (2025b). The only distinct operation which still needs proving is the match predicate. We restate the proof of the case when C(i):=#[j≤i,ψ(i,j)]P(j)C(i):= \# [j≤ i,ψ(i,j) ]\;P(j) from Huang et al. (2025b) when ψ is a local function of the following form ψ(i,j)=1j=i−ℓ0elseψ(i,j)= cases1&j=i- \\ 0&else cases We are doing this, as we will re-use a key idea here to implement our match predicate. Thus, in this C(i)C(i) will either be 11 or 0 depending if P(i−ℓ)P(i- ) is true or false. If we set the query and key matrices to 0 we get sij=logN⋅ψ(i,j)s_ij= N·ψ(i,j) We assume the log is base 2, but the argument is similar for others. Then we can have attention compute ci,k=∑j≤iexp(logN⋅ψ(i,j))⋅P(j)∑j≤iexp(logN⋅ψ(i,j))=∑j≤iN(ψ(i,j)ln2)⋅P(j)∑j≤iN(ψ(i,j)ln2)c_i,k= _j≤ i ( N·ψ(i,j) )· P(j) _j≤ i ( N·ψ(i,j) )= _j≤ iN ( ψ(i,j) 2 )· P(j) _j≤ iN ( ψ(i,j) 2 ) If P(i−ℓ)P(i- ) and ¬P(j) P(j) for j≠i−ℓj≠ i- , then we have a lower bound: N(1ln2)N(1ln2)+i−1≤ci,k N ( 1 2 )N ( 1 2 )+i-1≤ c_i,k If ¬P(i−ℓ) P(i- ) and P(j)P(j) for j≠i−ℓj≠ i- then we have an upper bound: ci,k≤i−1N(1ln2)+i−1c_i,k≤ i-1N ( 1 2 )+i-1 Since N1ln2≥iN 1 2≥ i, and we know that P(i−ℓ)⇔ci,k≥12P(i- ) c_i,k≥ 12, we can construct an MLP that computes the correct value. It will output either 0i+1 0i+1 or 1i+1 1i+1, in the dimension reserved for Pk+1(i)P_k+1(i), for instance by using a conditional operation (allowed in the syntax of the language) that checks that the output of the attention layer ci+1,k≥12c_i+1,k≥ 12. Now, when C(i):=#[j≤i,χ(i,j)]C(i):= \# [j≤ i,χ(i,j) ]\;, where χ(i,j)≡⋀k=1K(j−δk=i−γk+τk)χ(i,j)≡ _k=1^K( c_j- _k= c_i- _k+ _k). The c here refers to integers representing the elements of the extended alphabet, whereas everywhere else before in this proof, we were referring to c as counts. Similarly k here refers to the constants in this specific condition. Just for this proof, we will use σ to refer to characters to avoid confusion, and r. Hence, we want to prove that C(i):=#[j≤i,χ(i,j)]C(i):= \# [j≤ i,χ(i,j) ]\;, where χ(i,j)≡⋀r=1R(σj−δr=σi−γr+τr)χ(i,j)≡ _r=1^R( _j- _r= _i- _r+ _r). Note that all the γr,τr,δr _r, _r, _r are constants and help in looking around in the neighborhood, and the total number of such conditions R is also bounded. We reserve 2R2R spots in our residual stream. We use the same process defined earlier in computing our local ψ(i,j)ψ(i,j) functions, except in the attention computation, we use the value matrices to pass the value of the character embeddings at offsets to be transferred to the current position. We take the value matrix to be the identity matrix I 131313Allowed now, as the rank constraint on V matrices is no longer there, unlike in Huang et al. (2025b). Therefore, the only change would be that we use σj _j instead of P(j) in our derivation above. Thus, 2R2R spots out of all will now store each of our values of σi−γr _i- _r, σi−δr _i- _r. We can assume that the σi _i here are be one-hot vectors representing the corresponding integers. Adding a constant τ corresponds to a linear shift such that τσi=σi+τR_τ _i= _i+τ. So, τR_τ can be implemented as a shifted-diagonal matrix. Note that this is just one way in which this could happen. There could be other ways of this being true. We just want to be able to go from one character’s embedding to another with a linear transformation. Thus, we can hardcode these shifts in the KQ parameter matrices doing the retrievals of σi−γr _i- _r. Thus, instead of KQ=0KQ=0, they implement such a shift. Therefore we will already have the values of σi−γr+τr _i- _r+ _r in R positions. Thus, with these many attention heads, now we have all the information in our residual stream, and we need to actually compute the equality and the ∧ condition. We construct an attention head for this. We use the key and query matrices to concatenate the respective slots that hold all the R σi−δr _i- _r vectors and all the R σi−γr+τr _i- _r+ _r vectors respectively, and the product between these will be maximum when all the sets of R vectors match, which is what we want. Additionally, the key query matrices also scale up all the one hot vectors by a factor of 2. Thus now, we note that if χ(i,j)χ(i,j) is true, then the score is 2R2R, and ≤2(R−1)≤ 2(R-1) if even one condition fails. Therefore to verify a full match (and avoid confusion with partial matches), the attention score to the $ is always 2R2R. The value matrix at $ holds the value 11, and the value matrix at all other positions hold the value 0. Let Mi=j≤i|χ(i,j)=TrueM_i=\j≤ i|χ(i,j)=True\ and m=|Mi|m=|M_i| be the count we wish to compute. Based on our construction of Q and K, the attention scores sijs_ij satisfy: sij=2Rif j=$ (Start Token)2Rif j satisfies the match requirements)≤2(R−1)if j Mismatchs_ij= cases2R&if j= (Start Token)\\ 2R&if j satisfies the match requirements)\\ ≤ 2(R-1)&if j Mismatch cases (31) The output of the attention head at position i therefore hi h_i =∑j≤iexp(logN⋅sij)V(j)∑j≤iexp(logN⋅sij) = _j≤ i ( N· s_ij)V(j) _j≤ i ( N· s_ij) =exp(logN⋅si$)⋅1+∑j≠$exp(logN⋅sij)⋅0exp(logN⋅si$)+∑j∈Miexp(logN⋅sij)+∑j∉Mi∪$exp(logN⋅sij) = ( N· s_i )· 1+ _j≠ ( N· s_ij)· 0 ( N· s_i )+ _j∈ M_i ( N· s_ij)+ _j∉ M_i∪\ \ ( N· s_ij) Dividing both the numerator and the denominator by exp(logN⋅2R) ( N· 2R), and substituting the score values, we obtain: hi h_i =11+∑j∈Miexp(logN⋅2R)exp(logN⋅2R)+∑j∉Mi∪$exp(logN⋅sij)exp(logN⋅2R) = 11+ _j∈ M_i ( N· 2R) ( N· 2R)+ _j∉ M_i∪\ \ ( N· s_ij) ( N· 2R) =11+m⋅1+∑j∉Mi∪$exp(sij−logN⋅2R) = 11+m· 1+ _j∉ M_i∪\ \ (s_ij- N· 2R) We analyze the error term caused by mismatches. Since sij≤logN⋅2(R−1)s_ij≤ N· 2(R-1) for mismatches, the exponent is bounded by −2logN-2 N. There are at most i such mismatching terms (bounded by context length N). Thus: ∑j∉Mi∪$exp(sij−logN⋅2R)≤N⋅exp(−2logN)=N⋅N−2=1N _j∉ M_i∪\ \ (s_ij- N· 2R)≤ N· (-2 N)=N· N^-2= 1N Therefore, the output of the attention head is: hi=11+m+O(N−1)h_i= 11+m+O(N^-1) (32) As Izzo et al. (2025) argued, because of the restriction that attention logits and the output of the exp(⋅) (·) operation be rounded p fractional bits of precision, the O(1/N)O(1/N) terms gets rounded to 0. Thus our value converges strictly to 11+m 11+m. This is f As m is an integer bounded by N, the values 11,12,…,1N+1\ 11, 12,…, 1N+1\ are well-separated. We use our activation function f(x)=1/xf(x)=1/x to invert this value to recover m (or compute mi+1 mi+1 as required by the count operation) with arbitrary precision. ∎ Lemma C.22. C*-RASP[Pos]C*-RASP[Pos] where the input alphabet Ω is finite, is equivalent to C-RASP[Pos]C-RASP[Pos]. Proof. The syntax of C*-RASP[Pos]C*-RASP[Pos] closely tracks the syntax of C-RASP. The only additional operation in C*-RASP is that of the match predicate χ(i,j)χ(i,j). The class C*-RASP extends C-RASP solely through the addition of the Match operation. We show that when Σ is finite, any function defined by a Match operation can be simulated by a finite sequence of standard C-RASP operations. Recall the definition of the Match operation for a specific neighborhood structure defined by constants vectors δ,γ∈ℕKδ,γ ^K and τ∈ℤKτ ^K: Cmatch(i):=#[j≤i,χ(i,j)]C_match(i):= \# [j≤ i,χ(i,j) ]\; (33) where χ(i,j)≡⋀k=1K(j−δk=i−γk+τk)χ(i,j)≡ _k=1^K( c_j- _k= c_i- _k+ _k). Since Σ is finite, we know all pairs of (σ, σ+τσ+τ) we are looking for. Let us say that we enumerate each of these as (ak,bk)(a_k,b_k), where k∈[1,K]k∈[1,K]. The number of such pairs is equal to the size of the alphabet Σ , as every character from Σ can only be at a fixed distance τ to one other character from Σ . Thus, the whole match predicate boils down to a couple of steps. The first step is finding a j in the past, which has the symbol bkb_k stored at δk _k distance away from it. This local operation can be encoded as following in C-RASP[local]C-RASP[local]. Ppast(i):=⋀k=1K(#[j≤i,j+δk=i]Qbk(j)>0)P_past(i):= _k=1^K( \# [j≤ i,j+ _k=i ]\;Q_b_k(j)>0) The second step is to check whether the current position also has symbols aka_k stored at a distance of γk _k distance from it. This is fairly similar to the previous check, and can use similar commands. Pcurrent(i):=⋀k=1K(#[j≤i,j+γk=i]Qak(j)>0)P_current(i):= _k=1^K( \# [j≤ i,j+ _k=i ]\;Q_a_k(j)>0) The final step is counting the number of past positions where step 1 holds, and also making sure that step 2 holds at the current position. Thus, Cmatch(i):=#[j≤i]Ppast(j)∧Pcurrent(i)C_match(i):= \# [j≤ i ]\;P_past(j) P_current(i) Although once we know either of aka_k or bkb_k, we can get the other character in the pair. Apriori, we do not know the identity of the current position. In case of the infinite alphabet, the key was that the program could perform the matching without relying on the exact identity of the symbol. To simulate the same, instead of the predicates QakQ_a_k or QbkQ_b_k, we need to replicate the whole 3 steps for all possible pairs in Σ at every step k. Thus, the 33 lines of program are repeated |Σ|| | times, each time with a different (ak,bk)(a_k,b_k) combination assigned to each k. Since, we can simulate the only extra command in C*-RASP[Pos]C*-RASP[Pos] using commands of C-RASP[local]C-RASP[local], when the alphabet is finite, the two are equivalent. ∎ We restate Theorem 3.5 and prove it. Theorem C.23. Consider the alphabet Σ=a,b,e =\a,b,e\. Then, PARITY:=b∗(ab∗ab∗)∗∉C-RASP[∞,local]PARITY:=b^*(ab^*ab^*)^* -RASP[∞,local]. and Flip flop :=Σ∗be∗∉C-RASP[∞,local]:= ^*be^* -RASP[∞,local] . Proof. The proof of both of the languages above is analogous. We represent the corresponding language as L, and both PARITYPARITY or Flip-Flop can be substitued in place of L in our forthcoming arguments. We assume that there exists a program C*-RASP[Pos]C*-RASP[Pos] , P for L. Since, P works for L, it can work for L with bounded alphabet as well, as the Σ of L is simply Σ=a,b,e =\a,b,e\. However as per theorem C.22, such a P can be simulated in C-RASP[local]C-RASP[local]. That would imply that L∈C-RASP[periodic,local]L -RASP[periodic,local], which was proven to be impossible in Lemma 11 of Huang et al. (2025b). Thus, our initial assumption that such a program exists must be wrong. Hence, the corollary stands. ∎ Remark on Periodic Relations: Huang et al. (2025b) introduce C-RASP[periodic,local], which includes both local relations (ψ in the counting operation), and periodic relations ϕ(i,j)φ(i,j) checking if i≡k(modm)i≡ k\ (modm). In our new framework, we omit such periodic relations. In Huang et al. (2025b), accounting for these relations necessitated the assumption that the regularizer penalizes the rank of V matrices. In our present framework, we instead only penalize the spectral norm of these matrices, for two reasons: (i) first, because a norm penalty is better motivated as a proxy for standard learning methods than a rank penalty, (i) second, because penalizing the rank of V matrices would preclude moving information about object names across adjacent positions, which in fact is important for verifying plan validity. In Huang et al. (2025b), periodic relations were important for explaining APE length generalization on certain formal languages such as (aa)∗(a)^*, which are definable in [Reg] FO[Reg] but not [<] FO[<]. Such languages are not directly relevant to our present results, as they are not star-free but empirically easier for transformers than PARITY/FlipFlop. In particular, including such relations would not change Theorems 3.1 and 3.6. We leave to future work to better understand the role of periodic relations in length generalization. Remark on Unique Copying Task: Unique copying is the task of copying a string that is composed of distinct tokens. Huang et al. (2025b) showed that that task of unique copying is in C-RASP. However such kind of copying would require an increase of vocabulary during test time, and thus actually creates a challenge for rigorously treating the task using the results of Huang et al. (2025b), which assumes a fixed alphabet. Huang et al. (2025b) addressed this problem by formalizing Unique Copy as repeating a string unboundedly often with a fixed alphabet. However, formalizing the task in our new framework becomes much more principled and more true to the original formulation of the task. Essentially, the following lines of program are enough to detect that unique copying was successful: OnlyOneMatch(i):=(#[j≤i,cj−1=ci]==1)OnlyOneMatch(i):=( \# [j≤ i,c_j-1=c_i ]\;==1) UniqueCopySuccessful(i):=(#[j≤i]¬OnlyOneMatch(i)==0)UniqueCopySuccessful(i):=( \# [j≤ i ]\; (i)==0) Appendix D Experimental Details D.1 Domains and Dataset Generation For the generation of our training and test datasets, we use custom generators instead of existing problem generators and symbolic planners in order to control the lengths of the generated plans and get more variation. The generation of correct plans is mostly based on randomly selecting applicable action sequences but varies slightly depending on the domain. We first describe the shared set-up and then provide the domain-specific details below. Table 2 provides an overview over the characteristics of the six datasets we generate (see Table 3 for information about size and train/test splits). Note that the initial state of the Colors planning instances is fixed in the sense that all bags are empty initially. However, the part of the initial state that defines which objects are colors and bags varies depending on O. All datasets contain the same number of valid and invalid plans. In particular, we generate a set of planning instances Πi=⟨,Oi,Ii,Gi⟩ _i= D,O_i,I_i,G_i and for each Πi _i we create a plan π=[a1,…,ak,…,an]π=[a_1,…,a_k,…,a_n] such that π induces a state sequence from s1=Is_1=I to sn+1s_n+1 such that sn+1⊧Gs_n+1 G, i.e. π is a valid plan. Additionally, we generate an invalid plan π′π for each Πi _i and add ⟨Πi,π⟩ _i,π and ⟨Πi,π′⟩ _i,π to the dataset. We consider two ways of constructing invalid plans: converting the valid plan into an incomplete plan or a non-executable plan. To obtain the incomplete plans, the valid plan π=[a1,…,ak,…,an]π=[a_1,…,a_k,…,a_n] is converted into an invalid plan π′=[a1,…,ak′,…,am′]π =[a_1,…,a_k ,…,a_m ] inducing a sequence of states s1,…,sm+1′s_1,…,s_m+1 where s1=Is_1=I and sm+1′⊧̸Gs_m+1 G. The incomplete plans are created such that exactly one (in the case of Heavy Grippers, Colors) or at least one (Lights Out) of the literals in the goal is not satisfied. For Lights Out and Colors, π′π contains exactly the same number of actions as π. For Heavy Grippers, the number of actions is similar but some of the invalid plans are slightly shorter. For Heavy Grippers, we additionally generate a dataset with non-executable plans. To obtain a non-executable plan π′π , the valid plan is converted into an action sequence π′=[a1,…,am−1,am′]π =[a_1,…,a_m-1,a_m ] such that [a1,…,am−1][a_1,…,a_m-1] induces a sequence of states s1,…,sm′s_1,…,s_m and sm′⊧̸pre(am′)s_m (a_m ). We then combine the datasets with the incomplete plans and non-executable plans into the final dataset. In the STRIPS Colors domain and the Lights Out domain with conditional effects all actions are always applicable. Therefore, we cannot generate a dataset with non-executable plans here and only consider incomplete ones. The valid and invalid plans for the Colors and Lights Out domains are minimal pairs, differing only by single action. The same applies to the valid and non-executable plans in the Heavy Grippers datasets. However, some of the incomplete plans differ slightly more due to the specific characteristics of the domain and might have a slightly different plan length than their valid counterparts. Domain Domain variant Object set O Fixed states Invalid plans Heavy Grippers well-formed varying number and names none incomplete + non-executable Heavy Grippers delete-free varying number and names none incomplete + non-executable Colors well-formed varying number and names initial I incomplete Colors STRIPS varying number and names initial I incomplete Lights Out well-formed fixed goal G incomplete Lights Out conditional effects fixed goal G incomplete Table 2: Overview over the datasets generated for our experiments. Heavy Grippers. The Gripper domain is a well-known planning domain from the IPC benchmarks. Here, we create a variant of it that introduces two new aspects to the domain, namely that balls can be heavy and that the robot has a charge that affects how it can pick and drop balls (see Section 2.1 and Figure 2). We create a well-formed and a delete-free variant of our Heavy Grippers domain shown in Figure 2. First, we eliminate the conditional effects by separating pick into two actions, pickpick and pickHeavypickHeavy, and remove charged from the preconditions of pickpick. Second, we create the well-formed variant by extending the preconditions and the delete-free variant by removing the delete effects, resulting in the two domains shown in Figure 6. Predicates: room(r),ball(b),gripper(g),free(g),heavy(b),room(r),ball(b),gripper(g),free(g),heavy(b), charged, atRobby(r),at(b,r),carry(b,g)charged, atRobby(r),at(b,r),carry(b,g) Action move(r1,r2)move(r_1,r_2): Pre: room(r1),room(r2),atRobby(r1),¬atRobby(r2),¬charged\room(r_1),room(r_2),atRobby(r_1), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 atRobby(r_2), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 charged\ Eff: charged,atRobby(r2),¬atRobby(r1)\charged,atRobby(r_2), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 atRobby(r_1)\ Action pick(b,r,g)pick(b,r,g): Pre: ball(b),room(r),¬heavy(b),gripper(g),atRobby(r),\ball(b),room(r), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 heavy(b),gripper(g),atRobby(r), free(g),at(b,r),¬carry(b,g)free(g),at(b,r), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 carry(b,g)\ Eff: carry(b,g),¬free(g),¬at(b,r)\carry(b,g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 free(g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 at(b,r)\ Action pickHeavy(b,r,g)pickHeavy(b,r,g): Pre: ball(b),room(r),heavy(b),gripper(g),atRobby(r),\ball(b),room(r),heavy(b),gripper(g),atRobby(r), free(g),charged,at(b,r),¬carry(b,g)free(g),charged,at(b,r), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 carry(b,g)\ Eff: carry(b,g),¬free(g),¬at(b,r),¬charged\carry(b,g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 free(g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 at(b,r), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 charged\ Action drop(b,r,g)drop(b,r,g): Pre: ball(b),room(r),gripper(g),atRobby(r),carry(b,g)\ball(b),room(r),gripper(g),atRobby(r),carry(b,g), charged,¬at(b,r),¬free(g)charged, [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 at(b,r), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 free(g)\ Eff: at(b,r),free(g),¬carry(b,g),¬charged\at(b,r),free(g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 carry(b,g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 charged\ Predicates: room(r),ball(b),gripper(g),free(g),heavy(b),room(r),ball(b),gripper(g),free(g),heavy(b), charged, atRobby(r),at(b,r),carry(b,g)charged, atRobby(r),at(b,r),carry(b,g) Action move(r1,r2)move(r_1,r_2): Pre: room(r1),room(r2),atRobby(r1)\room(r_1),room(r_2),atRobby(r_1)\ Eff: charged,atRobby(r2)\charged,atRobby(r_2)\ Action pick(b,r,g)pick(b,r,g): Pre: ball(b),room(r),gripper(g),atRobby(r),at(b,r),\ball(b),room(r),gripper(g),atRobby(r),at(b,r), free(g),¬heavy(b)free(g), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 heavy(b)\ Eff: carry(b,g)\carry(b,g)\ Action pickHeavy(b,r,g)pickHeavy(b,r,g): Pre: ball(b),room(r),gripper(g),atRobby(r),at(b,r),\ball(b),room(r),gripper(g),atRobby(r),at(b,r), free(g),charged,heavy(b)free(g),charged,heavy(b)\ Eff: carry(b,g)\carry(b,g)\ Action drop(b,r,g)drop(b,r,g): Pre: ball(b),room(r),gripper(g),atRobby(r),carry(b,g)\ball(b),room(r),gripper(g),atRobby(r),carry(b,g)\ Eff: at(b,r),free(g)\at(b,r),free(g)\ Figure 6: The well-formed (left) and delete-free (right) variants of the Heavy Grippers domain used in our experiments. Variants were obtained from the variant shown in Figure 2. For the generation of the planning instances we fix the number of grippers to 2 (the standard number for the IPC Gripper variant), but vary the number of balls and rooms. In particular, when generating a plan of length N, we sample the number of balls nbn_b from the range [0.6∗N,0.85∗N][0.6*N,0.85*N]. The number of heavy balls and rooms is selected by sampling from [0.45∗nb,0.85∗nb][0.45*n_b,0.85*n_b] and range [0.2∗nb,0.5∗nb][0.2*n_b,0.5*n_b] respectively. This sampling strategy results in different combinations of plan lengths and number of objects while modeling that more objects tend to correlate with larger plans, which is the standard in planning datasets. We randomly assign a name to each object sampled from a fixed set of possible names. This set contains object names ranging from Object0 to ObjectM, where M is at least as large as the maximum number of objects within one instance in our dataset. For the initial state I, the initial locations of the robot and all balls are randomly assigned. We then sample a sequence of applicable actions until reaching the target length and make sure that in the resulting state each ball is located in a room, i.e. not carried anymore. The goal G consists of the locations of all balls obtained after applying the sampled sequence of applicable actions. For the delete-free variant, part of the actions of the sequence are sampled from all actions applicable under the delete-free variant and some are sampled from the smaller set of actions applicable under the well-formed variant. This mixture increases the probability that balls are actually dropped again which is important for getting reasonable goal states. The non-executable plans are obtained by replacing the last action of the valid plan with an action for which the preconditions are not valid at that step in the action sequence. This action is sampled at random from the non-executable move and drop actions. Pick actions are not considered because valid plans never end with pick actions, and this type of mistake could be easily identified without actually reasoning over the planning instance and plan. For the generation of incomplete plans, it is not possible to simply replace a single action. We select one ball and modify the plan such that the last step at which that ball is dropped does not drop the ball in the goal room anymore, which requires also changing the movements of the robot. Figure 7 shows a small example planning instance from the Heavy Grippers domain, with plans that are valid (π), incomplete (π1′ _1 ) and non-executable (π2′ _2 ) under the well-formed domain variant. Under the delete-free variant, both π and π2′ _2 are valid plans, but π1′ _1 is also incomplete. O=_,_,_,_,_,_,_,_,_O=\ object\_237, object\_223, object\_100, object\_154, object\_280, object\_113, object\_94, object\_7, object\_76\ I=at-robby(_),gripper(_),gripper(_),free(_),free(_),I=\at-robby( object\_280),gripper( object\_237),gripper( object\_223),free( object\_237),free( object\_223), room(_),room(_),room(_),room(_),room( object\_100),room( object\_154),room( object\_280),room( object\_113), ball(_),ball(_),ball(_),heavy(_),ball( object\_94),ball( object\_7),ball( object\_76),heavy( object\_94), at(_,_),at(_,_),at(_,_)at( object\_94, object\_100),at( object\_7, object\_154),at( object\_76, object\_280)\ G=at(_,_),at(_,_),at(_,_)G=\at( object\_94, object\_280),at( object\_7, object\_154),at( object\_76, object\_154)\ π=[pick(_,_,_),move(_,_),pick_heavy(_,_,_),π=[pick( object\_76, object\_280, object\_223),move( object\_280, object\_100),pick\_heavy( object\_94, object\_100, object\_237), move(_,_),drop(_,_,_),move(_,_),move( object\_100, object\_154),drop( object\_76, object\_154, object\_223),move( object\_154, object\_280), drop(_,_,_),move(_,_)]drop( object\_94, object\_280, object\_237),move( object\_280, object\_113)] π1′=[pick(_,_,_),move(_,_),pick_heavy(_,_,_), _1 =[pick( object\_76, object\_280, object\_223),move( object\_280, object\_100),pick\_heavy( object\_94, object\_100, object\_237), move(_,_),drop(_,_,_),move(_,_)¯,move( object\_100, object\_154),drop( object\_76, object\_154, object\_223), move( object\_154, object\_113), drop(_,_,_)¯] drop( object\_94, object\_113, object\_237)] π2′=[pick(_,_,_),move(_,_),pick_heavy(_,_,_), _2 =[pick( object\_76, object\_280, object\_223),move( object\_280, object\_100),pick\_heavy( object\_94, object\_100, object\_237), move(_,_),drop(_,_,_),move(_,_),move( object\_100, object\_154),drop( object\_76, object\_154, object\_223),move( object\_154, object\_280), drop(_,_,_),drop(_,_,_)¯]drop( object\_94, object\_280, object\_237), drop( object\_76, object\_280, object\_223)] Figure 7: An example planning instance from the well-formed Heavy Grippers domain with a valid plan π, an incomplete plan π1′ _1 and a non-executable plan π2′ _2 . The actions by which the invalid plans differ from the valid one are underlined. Colors. This domain involves placing colored balls into bags, where actions add or remove a color from a specific bag, and goals specify which colors each bag should contain. We design a standard STRIPS and a well-formed variant of the domain as shown in Figure 8. The variants differ in how they handle redundant operations, i.e. adding a color that is already in a bag or removing one that is not. The well-formed variant enforces that a color can be added or removed only if it is absent or present in the bag, respectively, while the standard STRIPS does not have this restriction. For all planning instances, we define the initial state as one in which no color is in any bag. We choose the number of colors and bags as a function of the target plan length: we set the total number of bag–color pairs (i.e., #colors × #bags) to approximately one quarter of the plan length, and we make the numbers of colors and bags as close as possible. We randomly assign a name to each object sampled from a fixed set of possible names. This set contains object names ranging from Object0 to ObjectM, where M is at least as large as the maximum number of objects within one instance in our dataset. Valid plans are generated by randomly sampling applicable actions until reaching the target length. The goal is then defined as the set of all hasColor facts that hold in the resulting state. In order to obtain the incomplete plans, we randomly substitute an action in the plan with another applicable action, and verify that this substitution leads to a different end state, failing the original goals. Figure 9 shows a small example planning instance from the Colors domain where the goal is to have color object3 in bag object5 and color object8 in bag object6. The figure shows a valid and an incomplete plan for the well-formed variant and a valid and an incomplete plan for the standard STRIPS. For both cases, the invalid plans are obtained by replacing a single action that has the effect that object3 will not be in object5 in the end. Note that the valid plan for the STRIPS variant is invalid under the well-formed variant but the well-formed valid plan would also be valid under the standard STRIPS domain. Predicates: bag(b),color(c),hasColor(b,c)bag(b),color(c),hasColor(b,c) Action remove(c,b)remove(c,b): Pre: bag(b),color(c)\bag(b),color(c)\ Eff: ¬hasColor(b,c)\ [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 hasColor(b,c)\ Action add(c,b)add(c,b): Pre: bag(b),color(c)\bag(b),color(c)\ Eff: hasColor(b,c)\hasColor(b,c)\ Predicates: bag(b),color(c),hasColor(b,c)bag(b),color(c),hasColor(b,c) Action remove(c,b)remove(c,b): Pre: bag(b),color(c),hasColor(b,c)\bag(b),color(c),hasColor(b,c)\ Eff: ¬hasColor(b,c)\ [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 hasColor(b,c)\ Action add(c,b)add(c,b): Pre: bag(b),color(c),¬hasColor(b,c)\bag(b),color(c), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 hasColor(b,c)\ Eff: hasColor(b,c)\hasColor(b,c)\ Figure 8: The standard (left) and well-formed (right) variants of the Colors domain. Well-formed variant O=_,_,_,_O=\ object\_5, object\_6, object\_3, object\_8\ I=bag(_),bag(_),color(_),color(_)I=\bag( object\_5),bag( object\_6),color( object\_3),color( object\_8)\ G=hasColor(_,_),hasColor(_,_)G=\hasColor( object\_5, object\_3),hasColor( object\_6, object\_8)\ π1=[add(_,_),add(_,_),remove(_,_), _1=[add( object\_3, object\_5),add( object\_8, object\_5),remove( object\_3, object\_5), add(_,_),add(_,_)¯,remove(_,_)]add( object\_8, object\_6), add( object\_3, object\_5),remove( object\_8, object\_5)] π1′=[add(_,_),add(_,_),remove(_,_), _1 =[add( object\_3, object\_5),add( object\_8, object\_5),remove( object\_3, object\_5), add(_,_),add(_,_)¯,remove(_,_)]add( object\_8, object\_6), add( object\_3, object\_6),remove( object\_8, object\_5)] Standard variant O=_,_,_,_O=\ object\_5, object\_6, object\_3, object\_8\ I=bag(_),bag(_),color(_),color(_)I=\bag( object\_5),bag( object\_6),color( object\_3),color( object\_8)\ G=hasColor(_,_),hasColor(_,_)G=\hasColor( object\_5, object\_3),hasColor( object\_6, object\_8)\ π2=[remove(_,_),add(_,_),add(_,_), _2=[remove( object\_3, object\_5),add( object\_8, object\_5),add( object\_8, object\_5), add(_,_)¯,remove(_,_),remove(_,_)] add( object\_8, object\_6),remove( object\_8, object\_5),remove( object\_3, object\_6)] π2′=[remove(_,_),add(_,_),add(_,_), _2 =[remove( object\_3, object\_5),add( object\_8, object\_5),add( object\_8, object\_5), remove(_,_)¯,remove(_,_),remove(_,_)] remove( object\_8, object\_5),remove( object\_8, object\_5),remove( object\_3, object\_6)] Figure 9: A small planning instance of the Colors domain with a valid plan π1 _1\ and an incomplete plan (π1′ _1 ) for the well-formed variant and a valid (π2 _2) and incomplete (π2′ _2 ) plan for the standard STRIPS. The actions by which the valid and invalid plans differ are underlined. Lights Out. While the well formed variants of Heavy Grippers and Colors domains serve as positive cases to show generalization over variable objects, we will use Lights Out to show negative results. It is important to note that this restriction does not undermine the validity of our evaluation. On the contrary, since conditional effects of Lights Out represents a negative result, the failure to generalize even for a fixed set of objects matches our predictions from Theorem 3.1. Lights Out is a puzzle consisting of lights arranged in a square grid. Each light is either on or off, and pressing a light toggles the state of itself and of each of the adjacent lights. The goal is to have all the lights off. We consider two formalizations of this domain, one with conditional effects and one that is well-formed. We use the standard 5x5 in all our Lights Out datasets with lights named 00 L_00, 01 L_01, … 44 L_44 according to their positions in the grid. The variant with conditional effects includes only a single action schema for pressing a light as shown in Figure 10 (left). There are no preconditions for pressing a light and the effect on each of the affected lights (i.e. the pressed light and the adjacent lights) is conditioned on the current status of that light. The well-formed variant has separate actions for pressing each light and for each possible combination of the state of that light and the adjacent lights. Figure 10 (right) shows two action schemas from the well-formed domain. The shown action schemas are two of the schemas for pressing the light in the upper left corner (00 L_00) which has two adjacent lights, 10 L_10 and 01 L_01. The other action schemas for pressing 00 L_00 cover all the remaining possible 232^3 on/off-combinations of 00 L_00, 10 L_10 and 01 L_01. Overall, the domain consists of 512 action schemas. There could be many other ways of defining this, we choose one for our convenience. All Lights Out planning instances have the same goal, i.e. all lights need to be off. In order to generate the initial states and valid plans, we start from the goal state and sample actions up to the target plan length. The resulting state becomes then the initial state and the valid plan is obtained by inverting the action sequence. The incomplete plans are obtained by replacing the last action with a different, applicable action which is guaranteed to result in a state where at least one light is turned on. Predicates: on(l),out(l),adj(l1,l2)on(l),out(l),adj(l_1,l_2) Action press(l1)press(l_1): Pre: ∅ Eff: out(l1)\out(l_1)\ ⊳ on(l1),¬out(l1)\on(l_1), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 out(l_1)\ on(l1)\on(l_1)\ ⊳ out(l1),¬on(l1)\out(l_1), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 on(l_1)\ ∀l2.adj(l1,l2),on(l2)∀ l_2.\adj(l_1,l_2),on(l_2)\ ⊳ out(l2),¬on(l2)\out(l_2), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 on(l_2)\ ∀l2.adj(l1,l2),out(l2)∀ l_2.\adj(l_1,l_2),out(l_2)\ ⊳ on(l2),¬out(l2)\on(l_2), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 out(l_2)\ Constants: ,,,,,,,… L_00, L_01, L_02, L_03, L_04, L_10, L_11,… Predicates: on(l),out(l)on(l),out(l) Action press-00-1: Pre: out(),out(),on(),¬on(),¬on(),¬out()\out( L_00),out( L_01),on( L_10), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 on( L_00), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 on( L_01), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 out( L_10)\ Eff: on(),on(),out(),¬out(),¬out(),¬on()\on( L_00),on( L_01),out( L_10), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 out( L_00), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 out( L_01), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 on( L_10)\ Action press-00-2: Pre: on(),out(),on(),¬out(),¬on(),¬out()\on( L_00),out( L_01),on( L_10), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 out( L_00), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 on( L_01), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 out( L_10)\ Eff: out(),on(),out(),¬on(),¬out(),¬on()\out( L_00),on( L_01),out( L_10), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 on( L_00), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 out( L_01), [rgb]0.77734375,0.15625,0.15625 [named]pgfstrokecolorrgb0.77734375,0.15625,0.15625 on( L_10)\ Figure 10: Left: the Lights Out domain with conditional effects and universal quantification over adjacent lights. Right: an excerpt of the well-formed variant of Lights Out. The complete well-formed domain consists of 512 action schemas. D.2 Training and evaluation Dataset Variant Train Val-ID Val-OOD Test-ID Test-OOD Color Bags Well-formed 1,720,000 12,000 13,333 24,000 26,667 Color Bags STRIPS 1,720,000 12,000 13,333 24,000 26,667 Grippers Well-formed 360,000 18,000 20,000 18,000 20,000 Grippers Delete-free 360,000 18,000 20,000 18,000 20,000 Lights-Out Well-formed 180,000 6,000 6,666 12,000 13,334 Lights-Out Conditional effects 180,000 6,000 6,666 12,000 13,334 Table 3: Number of instances per dataset, variant, and split. Setup. Unless otherwise specified, we use a decoder-only Transformer based on the GPT-2 architecture, with 8 layers, hidden size 768, and 12 attention heads. We use trainable absolute positional embeddings (APE) and pre-layer normalization, and optimize it using the standard causal language modeling objective. Inputs are tokenized with a domain-specific vocabulary that includes delimiter tokens, action tokens, argument and object tokens, the verdict tokens, along with other special tokens. Each example is constructed using delimiter tokens that separate the initial conditions I, the plan action sequence π, the goal G, and a final verdict token V∈correct,incorrectV∈\ correct, incorrect\: <init>I<plan>π<goal>G<verdict>V. <init>\,I\; <plan>\,π\; <goal>\,G\; <verdict>\,V. Tokenization. We tokenize plans at the level of action primitives and their arguments, with domain-specific schemes: (i) Lights Out (conditional-effect version): actions of the form press(lij) press(l_ij) are tokenized as <press> <i> <j>. (i) Lights Out (well-formed version): there are multiple distinct actions for pressing a specific light; we therefore tokenize these as <press> <i> <j> <k>. (i) Colors and Heavy Grippers: actions such as add(objecti,objectj) add( object_i, object_j) and pick(objecti,objectj,objectk) pick( object_i, object_j, object_k) are tokenized as <add> <object_i> <object_j> and <pick> <object_i> <object_j> <object_k>. Moreover, we only include tokens that are different for different instances. For example, for Colors, because all instances share the same initial state, i.e., all bags are empty, we omit the initial state from the input sequence. Data splits. For all three domains, we generate planning instances and correct plans of lengths 11 up to 200, and their invalid counterparts. We train only on the dataset instances with a plan length of up to 100 and test on the complete range of plans. All datasets are balanced, with the same number of valid and invalid plans. Evaluation. We train on plans of length 11–100 actions (ID) and validate on both 11–100 actions (ID) and 101–200 actions (OOD) datasets; here, “length” refers to |π||π|, instead of the total number of input tokens, which also increases monotonically with |π||π|. We run four random seeds and pick the checkpoint with the best validation performance.141414For the not-well-formed variant of Colors, we exclude the results of a random seed, because it failed to converge to a high ID performance. The phenomenon is consistent with our observation regarding the in-distribution learnability analysis in Figure 11. Then we report both ID and OOD accuracy scores on held-out test sets. At inference time, we provide the prefix up to <verdict> and compare only the logits of the two verdict tokens at the last prompt position; the prediction is the one with the larger logit. Instance packing. To improve training throughput while preserving instance boundaries, we concatenate multiple variable-length instances into fixed-length blocks of length B=4096B=4096 tokens, without splitting any instance across blocks. If an instance does not fit in the remaining space, we start a new block. For Colors and Heavy Grippers allowing cross-instance attention leads to unstable optimization with large loss spikes, so we prevent tokens from different instances in the same block from attending to each other, i.e., attention is restricted to the tokens from the same instance, in addition to the standard causal mask. Instances are shuffled between each epoch to avoid memorization. Optimization. Across all domains, we use a per-device batch size of 88 blocks. Our pilot shows that a larger block, e.g., 16 or 32, achieves similar performance; we therefore stick to 8 for efficiency. We train for 50,00050,000 steps for all runs, and validate them every 1000 steps. We use AdamW with a linear learning-rate schedule, with warmup over the first 10%10\% of training steps, weight decay 0.10.1, and gradient clipping to max norm 0.50.5. We train in bfloat16 on a single A100 or H100 GPU per run. We performed a learning-rate sweep over 2×10−5,5×10−5,1×10−4,3×10−4,6×10−4,1×10−3,2×10−3\2× 10^-5,5× 10^-5,1× 10^-4,3× 10^-4,6× 10^-4,1× 10^-3,2× 10^-3\ and selected the best setting per domain; this yields the following fixed learning rates: (i) Lights Out 2×10−52× 10^-5, (i) Colors 3×10−43× 10^-4, (i) Heavy Grippers 6×10−46× 10^-4. Appendix E Additional Empirical Results Figure 11: In-distribution test accuracy during the learning process (seed 0). Figure 12: Accuracy scores for each 10-length bucket. This is an extended version of results in Figure 5. Extended main empirical results. We first present an extended version of our main empirical results in Figure 12, i.e., the generalization accuracy across different plan lengths. Results are bucketed into 10-length intervals; for example, the point at x=20x=20 reports the accuracy over lengths 11–20. Besides the average accuracy scores, we also show the best seed and the standard deviation across all four seeds. In-distribution learnability. We also compare the ID learnability of different planning variants, by plotting the curve of ID test accuracy during the training process in Figure 11. We use one random seed as an example here, and our observations are consistent across different seeds. Model failure on Lights Out with conditional effects. Lights Out with conditional effects is the only setting in which models remain at chance-level accuracy. while others achieve near-perfect ID accuracy. This suggests that conditional-effect Lights Out is substantially more challenging, and highlights the massive benefit of the well-formed reformulation, which introduces an exponential (in grid size) number of actions and yields near-perfect accuracy for both ID and OOD lengths. Well-formed is easier than STRIPS. For Colors, although both the well-formed and STRIPS variants achieve near-perfect ID accuracy, the well-formed variant is learned substantially earlier, again suggesting the benefit of well-formed actions. Delete-free vs well-formed. For Heavy Grippers, the delete-free variant is learned slightly earlier than the well-formed variant, but variants do eventually converge.