Synthesis and Verification of Transformer Programs

1 Introduction*

Transformers [Vaswani et al., 2017] are the underlying neural network architectures behind Large Language Models (LLMs), using attention to aggregate information in the input sequence. Although transformers are expressive and at the same time efficiently parallelizable [Barcel´o et al., 2024; Huang et al., 2025; Yang and Chiang, 2024; Yang et al., 2024; Strobl et al., 2024], they are rather tricky to analyze. In particular, verifying transformers is undecidable [S¨alzer et al., 2025; S¨alzer et al., 2026]. Moreover, equipped with Chain of Thoughts (i.e. scratchpads for doing intermediate computation), they become Turing-complete [P´erez et al., 2021; Merrill and Sabharwal, 2024; Jiang et al., 2026b].

To better understand the behavior of transformers, researchers developed declarative languages which enjoy precisely defined semantics and at the same time faithfully capture the behavior of transformers. In 2021 Weiss et al. [Weiss et al., 2021] proposed the influential RASP (Restricted Access Sequence Processing Language) paradigm.

* An extended version of the paper, including appendices, is available at arXiv:2602.16473.

Essentially, RASP is a programming language that operates on sequences via operations like selection, aggregation, and simple position-wise arithmetic operations. Over the years the RASP paradigm has been instantiated and formally proven to model specific classes of transformers.

C-RASP (Counting RASP) [Yang and Chiang, 2024] is the most recent variant of RASP that has been shown (both theoretically and experimentally) by [Huang et al., 2025] to capture real-world transformers. C-RASP is essentially a refinement of Counting Linear Temporal Logic [Barcel´o et al., 2024], but without features that are not expressible by realworld transformers. More precisely, C-RASP allows a term of the form #φ, which counts the number of positions j to the left of the current position i where the formula φ holds. In this way, the Dyck-1 language of balanced parentheses over the alphabet {[, ]} is expressible in C-RASP; more on this in Section 2. In addition, C-RASP can express languages like MAJORITY (i.e. the input string contains more a's than b's), but cannot express the flip-flop language [Liu et al., 2023] - essentially, the regular language Σ∗ be∗ , for some letters b, e in the alphabet Σ - as well as PARITY (i.e. the number of a's in the input string is even), both of which are not trainable by transformers. [Huang et al., 2025] showed that C-RASP is captured by length-generalizable transformers (in that a transformers can learn a target language, given a finite training dataset). In particular, C-RASP is conjectured by [Huang et al., 2025] to capture all length-generalizable transformer languages; this is a formal version of the so-called RASP-L conjecture [Zhou et al., 2024].

Despite tight connections between C-RASP and transformers, the role of C-RASP has mostly been to help understand the expressivity of transformers. Here, we study the role of C-RASP as an interpretable surrogate model of transformers. "Interpretability" is a general concept in AI (e.g. see [Krishnan et al., 2024]), but for C-RASP (which has a formally defined semantics) it is best understood as the existence of an automatic method to analyze C-RASP programs. In particular, this is consistent with the term "interpretability" and "explainability" in FXAI (Formal eXplainable AI) [Marques-Silva and Ignatiev, 2023] and investigations in the formal aspects of AI (e.g. [Okudono et al., 2020; Barcel´o et al., 2020; Weiss et al., 2024; Hong et al., 2025; Arenas et al., 2021]). To this end, there are two main challenges. The first concerns automatic verification, since hitherto no automatic method to analyze C-RASP exists. In fact, checking whether a given C-RASP recognizes a trivial language is undecidable [Yang et al., 2026]. The second concerns synthesis, since there is no known method to actually learn a C-RASP program (from examples, or otherwise).

Contributions. We develop the first techniques that address both the verification and synthesis of C-RASP programs. We have implemented them and shown their efficacy on an assortment of benchmarks from the literature [Huang et al., 2025; Yang et al., 2025], in relation to the following applications: (1) transformer program minimization, and (2) constrained learning of transformer programs.

Our first contribution is the first automatic method for verifying C-RASP programs. In particular, we provide a reduction to the verification of Lustre, which is a synchronous datastream language with precise syntax and semantics. Since Lustre is supported by highly optimized model checkers (e.g. Kind2 Model Checker [Champion et al., 2016] with plugins to fast SMT solvers like CVC5 and Z3), we obtain an automatic method for verifying C-RASP programs against properties like language equivalence, inclusion, and emptiness.

Our second contribution is the first automatic method for synthesizing C-RASP programs from positive and negative examples. The method exploits local search in the form of simulated annealing. This is orthogonal to stochastic gradient descent for training transformers, which yields no implementable translation since the current translations (e.g. see [Yang and Chiang, 2024; Yang et al., 2025]) work only from a specific class of idealized transformers.

We have implemented both methods and demonstrate their efficacy against two applications: (i) C-RASP minimization (given a C-RASP, construct a smaller C-RASP) and (ii) constrained learning of C-RASP from a partial specification. In particular, we have tested our verifier against existing CRASP benchmarks in the literature (e.g. [Huang et al., 2025; Yang et al., 2025]), and show highly promising experimental results (see Table 1). In summary, our tool uses for both synthesis and verification of each benchmark a total of at most 300 seconds. In contrast, transformer training (e.g., GPT2) using the HuggingFace transformer library in PyTorch for some of these benchmarks alone could take up to several hours to achieve the correct language!

Organization. We define C-RASP and provide examples in Section 2. In Section 3, we define Lustre and a reduction from C-RASP to Lustre. Our synthesis algorithm is in Section 4. Experimental results and applications are in Section 5. We conclude with discussion and related work in Section 6.

We refer the reader to the technical report [Jiang et al., 2026a] and the artifact [Hongjian et al., 2026] for implementation and benchmark details.

2 Preliminaries

Before giving the full definition of C-RASP, we begin with an example. Let Σ be a finite nonempty alphabet and Σ+ denote nonempty words † a1 . . . an. Let ⊤ and ⊥ denote the Boolean values true and false. C-RASP programs are given by a sequence of rules that are evaluated over each position of an input word from Σ+. Rules may evaluate to Boolean or integer values, referred to as Boolean and counting rules, respectively. The C-RASP program below recognizes the Dyck(- 1) language; that is, the language of words over Σ = {[, ]} where each [ is matched by an ] in a well-nested fashion. For example [], [[]], and [[][]] are Dyck words, []] and ][ are not.

† We use "words" and "strings" synonymously in the paper, as as is standard in formal language theory.

Example 1. The following C-RASP program contains four rules and recognizes Dyck words. It is explained below.

The counting rules rule C[ and C] count the number of [ and ] characters respectively. We use the Boolean rule V to detect violations of well-nestedness. That is, V is true at a position of the input word if the number of [ characters is less than the number of ] characters. Finally, D is true only at the end of a Dyck word. It requires that the word contains no violations of the well-nested property and ultimately has the same number of [ and ]. The table below shows the full execution of the program over the word [[][]]][] which is not a Dyck word.

A word is accepted if the value of the last rule (D) is ⊤ at the final position of the word.

In the sequel, we follow closely the definition of C-RASP from [Huang et al., 2025], which also allows local and periodic positional encodings.

Definition 2.1 (C-RASP). A C-RASP program P over a finite alphabet Σ is a finite sequence of rules P = (R1, . . . ,Rk) where each Ri is either a Boolean rule or a Count rule of the form B := BExp or C := CExp respectively. B and C are the names of the rules. To recognize

languages, Rk is a Boolean rule that determines acceptance.

Definition 2.2 (Boolean Expressions). The syntax of Boolean expressions is given by the following grammar, in which a ∈ Σ is an atomic letter predicate, B is the name of a Boolean rule, ⋄ ∈ {∧, ∨} denotes Boolean conjunction and disjunction, ▷◁ ∈ {=,≤,<} denotes a comparison between counting expressions, and o < m ∈ N:

The semantics of Boolean expressions is as expected; in particular, B evaluates to the value of the referenced rule and m%o is true at positions j satisfying j modm = o.

Definition 2.3 (Counting Expressions). The syntax of counting expressions is defined inductively as follows, where k ∈ N, C is the name of a counting rule, and rs < re ∈ N:

CExp ::= k | C | #(BExp) | #rs,re (BExp) | CExp +CExp | CExp -CExp | min(CExp, CExp) | max(CExp, CExp) | BExp ? CExp : CExp.

Here, at position j, #(BExp) denotes the number of positions satisfying the Boolean expression at or before position j. The expression #rs,re (BExp) is a variant that only counts positions occurring between rs and re positions before the current position. The conditional expression eb ? e1 : e2 evaluates to e1 if the Boolean expression eb holds and to e2 otherwise. Constants k ∈ N denote fixed integer values and C evaluates to the value of the referenced rule.

Counting expressions thus provide numerical summaries of Boolean rules, which can be compared in Boolean expressions to form complex logical conditions. The expressions m%o and #rs,re are extensions of C-RASP to handle LOCAL and PERIODIC positional predicates [Huang et al., 2025].

C-RASP programs are evaluated over words. Given a word w = a1 . . . an ∈ Σ+ we inductively define the value of expressions. Let each rule be of the form Ri = V := eV , that is, eV is the expression associated to the rule named V . We define νw : (BExp × {1, . . . , n} → {⊤,⊥}) ∪ (CExp × {1, . . . , n} → Z) to be the value of the expression at position j in the word. Here we show only a selection of interesting cases, the full definition is given in the extended version.

A word w = a1 . . . an ∈ Σ+ is accepted by a C-RASP program (R1, . . . ,Rk) if νw(B, n) = ⊤ where Rk = B := e. [Remark: for simplicity, we do not allow an empty input, but this is easy to handle, e.g., by allowing an end-of-string symbol (see [Yang and Chiang, 2024]).]

3 Verification of C-RASP Programs

We verify properties of C-RASP programs via a translation to the synthronous dataflow language Lustre [Caspi et al., 1987], which is tailored to implementing embedded systems. Properties of Lustre programs can be checked by highly optimized tools such as Kind2 [Champion et al., 2016].

3.1 Lustre

We do not present Lustre in full, but show a fragment that is sufficient to show how C-RASP can be simulated. We will begin with an example to show how Lustre programs can recognize Dyck words. The program operates in a similar way to the C-RASP program of Example 1.

In the full definition, a Lustre program contains a set N1, . . . ,Nn of nodes. For simplicity of presentation we will use a single node. Intuitively, nodes can be used to define functions that are reusable and aid readability. Each node has input, output, and local variables. Our node will have one input variable (the input word) and no output variables. We use two types: BOOL and INT. Each variable represents an infinite stream of values of the declared type and will broadly correspond to a single C-RASP rule.

Local and output variables are defined using standard mathematical and Boolean combinations of variables and constants. For example X := ¬Y means that at position i in the stream, X takes the negation of the value of Y at position i. The pre operator accesses the value of a variable at the previous position. The → operator can be used to replace the initial value of a stream. A typical example of these two operators is X := 1 → pre(X)+1, which defines the sequence 1, 2, 3, . . . where 1 replaces the initial (undefined) value of pre(X) +1. Kind2 supports a check keyword to verify that a given Boolean expression evaluates to true at all positions.

Example 2. The following Lustre program recognizes Dyck words. It has an input variable I of type INT and local variables Nl, Cl, Nr, Cr, NV , and CV of type INT and V and D of type BOOL. D is designated as an output variable. For this example we will make the simplifying assumption that I only takes integer values 0 or 1 (corresponding to [ and ]). Our full encoding will need to enforce this assumption and use end of stream markers. The equations defining each variable are shown below and then explained.

node DyckCounters(I: int) returns (D: bool); var Nl, Nr, Cl, Cr, Nv, Cv : int; V : bool; let Nl = if I = 0 then 1 else 0; Nr = if I = 1 then 1 else 0; Cl = (0 -> pre(Cl)) + Nl; Cr = (0 -> pre(Cr)) + Nr; V = Cl < Cr; Nv = if V then 1 else 0; Cv = (0 -> pre(Cv)) + Nv; D = (Cv = 0) and (Cl = Cr); tel

Adding a check statement check¬(Cr = 3) ∨ D would require the property that whenever three ] characters have been seen, then the word so far is a Dyck word. This property is true of the stream above, but not true of all input streams.

Definition 3.1 (Lustre (fragment)). A Lustre program in our fragment is a node with: one input variable I of type INT; local variables B1, . . . ,Bmb of type BOOL; local variables C1, . . . ,Cmc of type INT; one equation for each local variable; and a check statement.

Let B = {B1, . . . ,Bmb } and C = {I,C1, . . . ,Cmc } denote the Boolean and integer variables. Boolean variables are defined using equations B := LBExp and integer variables with C := LIExp where

with C ∈ C, ⋄b ∈ {+,-,mod} and k ∈ Z. The check statement is of the form check LBExp.

Variables hold infinite streams of integers or Booleans. Let ν : (B × N → {⊤,⊥}) ∪ (C × N → Z) be a valuation of the Boolean and integer variables. That is ν(V, i) is the value of the ith position of the stream assigned to the variable V . We generalize ν to expressions e. Interesting cases are given below and full generalization refers to the extended version.

Each equation V := e means V takes a value such that ν(V, i) = ν(e, i) for all i. An assertion check e is violated if there exists some assignment ν consistent with the equations of the program such that for some i we have ν(e, i) = ⊥. We say a Lustre program is valid if no check statement is violated by any value of the input variable I.

While the semantics is largely straightforward, it is worth considering some examples of pre and →. An expression 1 → 2 defines a stream 1, 2, 2, 2, . . .. However, notice that the expression 1 → (1 → 2) also defines 1, 2, 2, 2, . . . as → only changes the first value. To define a stream 1, 2, 3, 4, 4, 4, . . . we use 1 → pre(2 → pre(3 → 4)).

3.2 C-RASP to Lustre

We encode a C-RASP program (R1, . . . , Rk) over an alphabet Σ into Lustre as follows. An outline of the translation can be seen by comparing Example 1 and Example 2. Consider the C-RASP expression #V . This is simulated in Lustre by introducing new variables NV and CV with

The expression #V is then translated directly to CV . Most other C-RASP constructs allow almost direct translations, with some additional subtlety for the counting operators.

We also need to bridge the gap between C-RASP operating over finite words and Lustre over infinite streams of integers. The translations are given below.

Representing the Input Word

We introduce two fresh symbols # (end of stream) and Ω (eternity). Let Σ′ = Σ ∪ {#, Ω}. Choose any injective map ι : Σ′ → Z. A finite word a1 . . . an will be encoded by an infinite stream ι(a1) . . . ι(an)ι(#)ι(Ω)ι(Ω)ι(Ω) . . ..

For convenience, let I ∈ S for a set S ⊆ Σ′ denote ∨a∈S I = ι(a). Similarly I = a denotes I = ι(a).

We introduce a new Boolean Lustre variable BI and assign it the following Boolean expression that checks at each position i if I is a correct input word. It asserts that each position encodes a character. Then, it asserts that the first symbol is not Ω and Ω is the only character seen after #. Let RI =

We introduce a second variable Bˆ I to track whether BI was false at any point in the word. Let Rˆ I = Bˆ I := BI → (BI ∧ pre(Bˆ I )). Finally, let RI = {RI,Rˆ I }.

Translating C-RASP Rules

Let (R1, . . . ,Rk) be a C-RASP program. For each Boolean rule Ri = B := e, introduce a Lustre variable VB that is of type BOOL. Similarly, introduce a variable VC of type INT for each counting rule Ri = C := e. For each C-RASP rule Ri = X := e we define T(Ri) to be a set of equations including the rule VX := T(e) and possibly some auxiliary equations. We define T (e) in full in the extended version(e.g. T(¬e) := ¬T(e)). Interesting cases are shown here. For Boolean expressions (recall that I = a denotes I = ι(a))

where P is a fresh integer variable encoding the current position. It uses an auxiliary equation P := 0 → pre(P) + 1. C#(e), C#rs,re (e), Ce1 , and Ce2 are fresh integer variables defined via the auxiliary equations.

The auxiliary equations of T(Ri) for the examples shown are as follows. For each instance of C#(e) we create a fresh a integer variable Ce that is 0 when e is false and 1 when e is true. We add the equations

For C#rs,re (e) we use the shorthand prei to define a "safe" i-fold application of pre that evaluates to 0 if there are fewer than i previous positions. That is pre0 (e) = e and prei (e) = 0 → prei-1 (e) when i > 0. We also create a fresh integer variable Ce defined as above. We then add

Checking Properties of C-RASP

We can verify a number of properties of C-RASP programs by translation to Lustre. We show here how to check language inclusion. A similar encoding can check equality

Given two C-RASP programs P1 = (R1 1 , . . . ,R1k1 ) and P2 = (R2 1 , . . . , R2k2 ) we can check whether P1 only accepts words that are also accepted by P2. We assume that P1 and P2 have disjoint rule names and translate P1 and P2 to Lustre. The only shared variable between the programs is the input variable I. Suppose V1 and V2 are the variables corresponding to the output equations of the two programs. Notice that, in C-RASP, at least one character is needed to determine the value of the output equations. The following check constraint asserts that after the first position, either the input I is incorrect, the end of the streammarker has not been reached, or P2 accepts whenever P1 does.

If the property does not hold, Kind2 reports a witnessing trace of I. This trace gives counter-example word after applying the inverse of ι and removing # and Ω.

We define T⊆(P1, Pw) to be the Lustre program with the equations RI ∪⋃i T (R1 i )∪⋃i T (R2 i ) and the check statement defined above.

Proposition 3.2. Take C-RASP programs P1 and P2. P1 accepts only words accepted by P2 if T⊆(P1, P2) is valid.

The translation from C-RASP to Lustre is polynomial except for #rs,re . To translate #rs,re we use prei (Ce) for each re ≤ i ≤ rs. If rs and re are encoded in binary, the translation is exponential. Hence, we assume that rs and re are given in unary. We do not need a similar restriction for m%o.

Proposition 3.3. Take C-RASP programs P1 and P2. Assume each rs and re appearing in the #rs,re operators is encoded in unary. The Lustre program T⊆(P1, P2) is of size polynomial in the size of P1 and P2.

4 Synthesis of C-RASP Programs

We synthesize C-RASP programs with a local search procedure based on simulated annealing [Kirkpatrick et al., 1983; Henderson et al., 2003]. It starts from an initial program and repeatedly proposes a neighboring program obtained by applying syntactic mutations. Given a set of words labeled as positive and negative samples, we aim to synthesize a program that is consistent with the samples while remaining small and structurally simple.

State Space. A C-RASP program over an alphabet Σ is written as a finite sequence P = (R1, . . . ,Rk) where each Ri is either a Boolean rule or a Count rule, and Rk is the distinguished Boolean rule that determines language acceptance.

To bias the search toward a concise and interpretable model, we restrict the search to programs of a fixed program shape. Formally, a shape is a tuple

where Nb and Nc are the number of Boolean and Counting rules, respectively, and K bounds the range of numeric constants that may appear in Counting expressions. Only programs that satisfy these bounds are considered during search.

Let Pσ denote the set of all well-formed C-RASP programs over Σ that contain exactly Nb Boolean rules and Nc counting rules and use only constants from {0, . . . ,K}. The local search explores the finite state space Pσ.

Mutation Operator and Neighborhood. Local search proceeds by repeatedly modifying the current program using a stochastic mutation operator. The mutation operator induces the neighborhood relation explored by simulated annealing. The mutation operator defines a Markov transition

mapping each program P to a distribution Mutate(P) over the successor programs; we require Mutate(P )(P ′ ) ≥ 0 and ∑P ′∈Pσ Mutate(P )(P ′ ) = 1 for all P, P ′ ∈ Pσ. The neighborhood of a program P is defined as

Each neighbour differs from P by a single conservative rewrite of the right-hand side of one rule. Although individual mutations are local, the neighborhood is sufficiently rich that any two programs of the same program shape can be connected by a finite sequence of mutations.

At each iteration, the mutator selects either a Boolean rule or a Counting rule in a program P, rewrites the right-hand side of the rule, and removes rules that are unreachable from the final Boolean expression Rk. All mutations preserve wellformedness and acyclicity by construction.

Boolean Rule Mutation. Boolean rules are mutated by resampling or locally modifying their right-hand sides. The mutation operator only uses a non-nested fragment of expressions to bias the search toward simple programs. In particular, Boolean expressions are limited to expressions in which logical connectives and negation may be applied only to Boolean atoms, and nesting of Boolean operators is disallowed. This restriction ensures that the program remains simple, while more complex behavior can still be expressed through dependencies between expressions.

A Boolean atom occurring in the right-hand side of a Boolean rule Bi may be one of the following: an alphabet test a ∈ Σ; a reference to an earlier Boolean rule Bj with j < i; a position-period predicate m%o, where m ∈ N and o < m; or a comparison CExp1 ▷◁ CExp2, where ▷◁∈ {=,≤,<}.

In addition to full resampling, we allow micro-mutations that preserve expression depth while modifying only a local syntactic feature. Examples include swapping ∧ and ∨, toggling negation, flipping the strictness of a comparison, or resampling a single leaf atom. These micro-mutations define small, incremental moves in the neighborhood.

Counting Rule Mutation. As with Boolean expressions, we work with a shallow fragment of the syntax defined in Definition 2.3. During mutation, the right-hand side of each counting rule is required to have syntactic depth at most 2. Counting expressions are therefore built from count atoms using at most one arithmetic operator or one conditional expression. A new right-hand side is either resampled entirely or modified using a micro-mutation. Resampled Counting expressions are drawn from the grammar

where x, y are count atoms and op ∈ {+, -, min, max}.

Count atoms are drawn from a finite, type-directed pool: integer constants k ∈ N; references to earlier counting rules Cj with j < i; or count of PERIODIC predicate #(ϕ) or LOCAL predicate #rs,re (ϕ). The predicate ϕ is a Boolean atom that does not contain comparisons or equalities. For LOCAL predicates, bounds are normalized so that rs ≤ re.

Objective Function. Each candidate program P is evaluated on a fixed set of labeled examples D = D+ ∪ D-. The primary objective is to minimize the number of misclassified samples:

Here, I[·] is the indicator function, equal to 1 if P misclassifies x and 0 otherwise. Among programs with equal classification behavior, we prefer simpler programs. We penalize on expressions unreachable from Rk in the dependency graph, and the total size of the abstract syntax tree. The resulting scoring function is

where λmis ≫ 1. This demands that the search first minimizes mis(P ) and, among programs with equal misclassified count, prefers structurally simpler programs.

Annealing Dynamics. At each iteration, the algorithm maintains a current program P and proposes a neighbouring program P ′ . Let ∆ = E(P ′ ) - E(P). If ∆ ≤ 0, the new programP ′ is always accepted. Otherwise, it is acceptedwith probability exp(- ∆T ), where T > 0 is the current temperature. The temperature is initialized to T0 and decreased using geometric cooling. To mitigate premature convergence, we optionally apply periodic reheating.

The complete simulated-annealing synthesis procedure is presented in Algorithm 1, which maintains the current program and the best program encountered so far, applies mutation-based proposals, and accepts or rejects them according to the probability above. Note that if ∆ ≤ 0, then exp(-∆/T) ≥ 1 and the new program P ′ is accepted with probability 1 in line 7. Termination occurs when the iteration budget is exhausted or when no further improvement is observed under a sufficiently low temperature.

As a refinement (not shown in Algorithm 1), once a program with mis(P) = 0 is discovered, the search may continue under a hard constraint that forbids reintroducing misclassification, while increasing structural penalties to accelerate simplification.

5 Experiments

We implement a unified Scala framework integrating C-RASP synthesis and verification within a single modular toolchain. The framework - combining example-driven local search with verification - consists of three core components:

1. C-RASP synthesis based on simulated annealing,
2. a lightweight C-RASP evaluator for fast scoring on finite datasets, and

Algorithm 1 Simulated-Annealing Synthesis for C-RASP Programs

1: Input: initial program P0; sample set D; temperature parameters (T0, α, K, ρ); iteration budget N 2: Output: best program P ⋆ 3: P ←P0, P ⋆ ←P, T ← T0 4: for i = 0 to N -1 do 5: Pick P ′ according to distribution Mutate(P) 6: Pick r ∈ [0, 1] uniformly at random 7: if r ≤ exp(-(E(P ′ ) - E(P ))/T ) then 8: P ←P ′ 9: end if 10: if E(P) < E(P ⋆ ) then 11: P ⋆ ←P 12: end if 13: T ←α · T 14: if K > 0 and (i + 1) mod K = 0 then 15: T ← ρ · T 16: end if 17: end for 18: return P ⋆

1. a verification back-end that translates C-RASP programs to Lustre and checks properties using Kind2.

Building on this integration, our framework supports two verification-guided synthesis applications: 1) Transformer Program Minimization and 2) Constraint Learning.

1. Given a specification program Pspec, the goal is to synthesize a program P such that L(P) = L(Pspec) while minimizing structural complexity. The procedure alternates between local search and equivalence checking; when equivalence fails, Kind2 provides a counterexample trace that is added to the trace set to guide further search. The process terminates once equivalence is established or a predefined limit is reached.
2. Given labeled examples D = D+ ∪ D- and a partial specification program Pspec, constraint learning aims to synthesize a program P that fits all examples and satisfies L(P) ⊆ L(Pspec). Local search is guided by D and each candidate is checked for inclusion; if the check fails, the resulting counterexample is added to D as a negative example and synthesis continues.

We evaluate on a benchmark suite of regular, countingbased, and context-free-style languages. For each task, synthesis is trained on 1000 balanced examples with string lengths in [ℓmin, 100], where ℓmin is the minimum valid length for the target language, using an 80%-20% train/test split to report both train accuracy (TA) and evaluation accuracy (EA). The objective function is parameterized with λmis = 1000, λU = 200, and λS = 100. Simulated annealing runs a budget of 105 iterations. The temperature (initially T0 = 1.0) is cooled exponentially with rate α = 0.9995, and reheated every 4000 iterations by a factor of 1.2.

SL Synthesis is the backbone of both applications and achieves high accuracy across benchmarks, including those requiring non-trivial counting (Table 1). Consistent with the known expressivity theory [Huang et al., 2025; Yang et al.,

2025], languages beyond C-RASP's expressive power (Parity, Tomita 3, Tomita 5, etc.) could not be learned with a sufficiently high accuracy; within the alloted time, the best training accuracy is below 80%. Full results and the corresponding transformer training comparisons can be found in the technical report.

ProgramMinimization and Constraint Learning are correct by construction: a candidate is accepted only after Kind2 discharges the equivalence (resp. inclusion) checked against Pspec, and every failed check is recycled as a counterexample. Accuracy is therefore 100% on all inputs whenever the loop succeeds, so the table reports only refinement rounds and synthesis/verification time. In ProgramMinimization, local search quickly finds correct but non-minimal programs, while verification dominates the runtime by driving structural simplification, especially for richer counting structures. In Constraint Learning, refinement rounds are typically few since the labeled examples restrict the hypothesis space; verification cost stays low, while synthesis grows under tighter semantic constraints.

6 Discussion and RelatedWork

Formal models of transformers. The intricacy of formally modeling transformers arises from the following features (among others): precision (polynomial, logarithmic, and fixed), attention mechanisms (hardmax/softmax attention), positional encodings (periodic, local, relative, etc.), and uniformity (a uniform description independent of the input length). These gave rise to a number of different formal models (e.g. see [Strobl et al., 2024]). Over the years, experimental results concerning learnability revealed that several variants of softmax transformers [Huang et al., 2025; Yang et al., 2025] that are tightly related to C-RASP capture concepts that are learnable by transformers. [Huang et al.,

2025] proposed a formal version of the RASP-L conjecture [Zhou et al., 2024] that C-RASP captures precisely languages that are expressible by length-generalizable transformers.

RASPs. [Friedman et al., 2023] proposed learning a RASP by pre-restricting the architecture and parameters for transformer training. The difficulty with this approach (especially for C-RASP) is to find the right "restriction" so that a CRASP can be extracted; we are not aware of such work. Our synthesis algorithm directly finds a C-RASP without going through a transformer, which we showed to be competitive with transformer training on our benchmarks.

B-RASP [Yang et al., 2024] is a version of RASP, which supports manipulations of bit sequences. B-RASP can express languages that are not efficiently learnable (see [Huang et al., 2025]), including the flip-flop language [Liu et al., 2023], which makes it not a suitable model for real-world transformers. The model overapproximates concepts expressible by fixed-precision transformers [Li and Cotterell, 2025].

Verification of neural networks. Suchworks (e.g. [Katz et al., 2022; Huang et al., 2020; Liu et al., 2021; Huang et al., 2017]) focus mostly on verifying neural networks with a fixed number of input nodes. Yearly competition (e.g. see [Brix et al., 2024]) is now held on such verification tasks. Here, the verification problem is decidable (in fact, NP-complete), which is not the case for transformers [S¨alzer et al., 2025].

Future Work. Numerous open problems lie ahead including the extension of our methods to other properties, e.g., "robustness". This is a common property in neural networks verification (e.g. [Brix et al., 2024]), but the right formulation (that is motivated by practical applications) for sequential models is yet to be explored, e.g., perhaps via metrics on strings like hamming/edit distances. Since practical transformers use "Chain of Thoughts (CoTs)" [Jiang et al., 2026c], another direction is to incorporate CoTs in our framework.

Acknowledgments

This material is based in part upon work supported by the Eu(ERC, LASD, 101089343, https://doi. org/10.3030/101089343) and by the Swedish Research Coun-

ropean Union ‡ cil through grants 2021-06327 and 2025-06185.