AG-CoT: Verified Algorithmic Traces for LLM Program Synthesis on Clifford Circuits

1 INTRODUCTION

• Executable code can pass parsing and execution yet prepare the wrong quantum state, motivating behavioral rather than surface-level correctness checks.The running example contrasts two valid one-qubit programs, only one of which prepares the requested state.Source: §1 · p. 1, Figure 1 · p. 2
• Clifford state preparation is exactly and inexpensively checkable because signed Pauli generators specify stabilizer states and circuits can be simulated classically.The Aaronson–Gottesman algorithm also provides a step-by-step derivation of a correct circuit for each target.Source: §1 · pp. 1–2
• The framework uses compact signed stabilizer targets, verifier-accepted AG-CoT traces, and verifier-filtered continuation rather than treating exact checks only as scores.A 12-qubit prompt is shortened from roughly 16K to roughly 800 characters.Source: §1 · p. 2
• On 3,661 held-out targets, Qwen solves 201 with AG-CoT SFT versus 33 with circuit-only SFT; Mistral solves 316 versus 71 with Direct SFT.The three Qwen RFT versions solve 213, 215, and 210 targets; Mistral RFT solves 322.Source: §1 · p. 2
• 5.49% versus 0.90% task success for Qwen and 8.63% versus 1.94% for Mistral show higher single-output success with AG-CoT than circuit-only supervision.Verifier-filtered continuation adds a smaller observed increase in all three Qwen versions and in Mistral.Source: §1 · p. 2
• The paper reports syntax validity, Clifford validity, saved-label matching, state equivalence, and finite-budget search coverage separately to expose failures beyond valid code.In the 32B study, supervised models reach approximately 99.9% syntax and Clifford validity, while the strongest direct model prepares the target for 6.14% of prompts.Source: §1 · p. 2

Semantic code evaluation

• Semantic code evaluation moved from textual overlap toward behavioral correctness, executable environments, semantic judgment, and equivalence checking.This paper shares that motivation and uses an exact quantum-domain oracle for training and evaluation.Source: §2 · p. 2

Quantum circuit generation and synthesis

• Quantum circuit work includes classical and generative synthesis, benchmarks of executable and semantic behavior, and language-model systems using fine-tuning, rewards, or search.This paper studies Clifford state preparation from signed stabilizer targets, which permit exact verification after parsing and Clifford-validity checks.Source: §2 · p. 3

Verifier-guided learning and search

• Verifier-guided work uses verifiers for training examples, reward assignment, and candidate selection, while this paper pairs deterministic traces with a matched circuit-only control and verifier-selected continuation.The same verifier checks training completions and generated circuits.Source: §2 · p. 3

3 TASK AND VERIFIER

• A target prompt specifies a state through signed Pauli generators, and the OpenQASM output must prepare it from |0⟩^n.The pipeline parses the program, checks Clifford validity, and compares the prepared state with the target.Source: §3 · p. 3
• A stabilizer state is specified by n independent commuting signed Pauli generators, represented by a tableau containing binary support and sign bits.Different generator bases can describe the same state, so label equality and state equivalence are distinct checks.Source: §3 · p. 3
• Clifford gates update tableau support and signs exactly, letting the verifier compare target states without reconstructing a numerical state vector.Generic state preparation would require a non-stabilizer representation and a predefined fidelity threshold; full unitary synthesis instead needs an equivalence check with numerical tolerance.Source: §3 · p. 3
• The tableau prompt stores a compact exact target representation: the cited 12-qubit example uses approximately 800 characters versus approximately 16,000 for the state-vector representation.The tableau stores 2n^2 + n bits before formatting, compared with 2^n complex amplitudes in a general pure-state vector.Source: §3 · p. 3
• Exact(x, y) requires parsing, Clifford conversion, and equality of signed stabilizer-label sets, whereas StateEq checks equivalence of the represented stabilizer states.StateEq removes generator-basis sensitivity but retains the parsing, Clifford-conversion, and state-preparation boundary.Source: §3 · p. 4
• Pass@N measures the probability of at least one strict success within a candidate budget; StateEq-Pass@N uses state equivalence instead.The study samples 64 candidates per target; observed Pass@64 coverage differs from estimated smaller-budget values and from direct one-output Exact@1.Source: §3 · p. 4

Method overview

• The method pairs AG-CoT supervision with verifier-filtered continuation, using a circuit-only Direct SFT control that omits the synthesis steps.QCircuitBench instances and reference circuits supply the 32B study; Qwen and Mistral use target-conditioned teacher construction.Source: §4 · p. 4

Reference-circuit AG-CoT construction

• For the 32B study, deterministic Aaronson–Gottesman reduction of each reference Clifford is inverted to form the preparation circuit and a trace-plus-circuit completion.Basic AG-CoT records the starting destabilizer row per qubit; Step AG-CoT also records rows after each operation, and the accepted corpus contains 38,940 examples.Source: §4 · p. 4

Target-conditioned AG-CoT construction

• For Qwen and Mistral, the target-conditioned teacher completes signed stabilizer generators to a full tableau, reduces and inverts it, compiles to {h, s, cx}, and verifies the program.The source QASM is used only to confirm that it prepares the recorded target state.Source: §4 · p. 4

4 TARGET-CONDITIONED SUPERVISION AND VERIFIER-FILTERED TRAINING

• Figure 2 presents the verified teacher, paired supervision, accepted-response dataset, and correct single outputs on the same 3,661 test targets.Its three Qwen RFT versions are shown separately.Source: Figure 2 · p. 5

Paired supervision and training objective

• The paired circuit-only and AG-CoT records share the prompt and teacher circuit, while AG-CoT additionally supervises the algorithmic trace.Basic traces use one line per qubit; Step AG-CoT adds intermediate destabilizer-row states after each reduction operation.Source: §4 · pp. 5–6

Verifier-filtered supervised continuation

• RFT samples model responses, keeps only completions accepted by the verifier, and continues supervised training on the fixed accepted dataset.Acceptance requires a complete formatted response and QASM program that parses, is Clifford-valid, uses {h, s, cx}, has the requested qubit count, and passes StateEq.Source: §4 · p. 6

5 EXPERIMENTAL SETUP

• Evaluations use QCircuitBench random-circuit state-preparation instances, where exact stabilizer-tableau verification is available.Prompt and decoding settings are recorded in Appendix E.Source: §5 · p. 6
• The controlled Qwen and Mistral test set contains 3,661 distinct targets with no canonical identity shared with training or development targets.Each model generates one greedy completion per target without retries or program repair; success requires state equivalence, gate-set, header, and output-length compliance.Source: §5 · p. 6
• The complementary 32B study evaluates six Qwen2.5-Coder-32B-Instruct systems on 3,894 held-out prompts, including a separate verifier-selected Best-of-64 variant.The direct variants include zero-shot, two AG-CoT formats, GRPO, and verifier-filtered RFT.Source: §5 · p. 6
• Reported metrics distinguish syntax and Clifford validity, exact saved-label matching, state equivalence, and single-output versus multi-candidate success.Controlled comparisons report StateEq-based task success with additional output requirements.Source: §5 · p. 6

6.1 CONTROLLED TRAINING COMPARISONS

• 201 versus 33 Qwen targets succeed with AG-CoT SFT versus Direct SFT, a 4.59 percentage-point gain; AG-CoT is higher at every tested size from 3 to 12 qubits.The paired comparison has 170 AG-CoT-only successes and 2 Direct-SFT-only successes; the exact McNemar p value is 4.97 × 10^-48.Source: §6.1 · p. 7, Table 1 · p. 7, Figure 4 · p. 7
• 210–215 Qwen targets succeed across the three RFT versions, exceeding AG-CoT SFT by 9–14 outputs; mean task success reaches 5.81%, up 0.32 percentage points.The additional gain appears in all three versions; the verifier supplies fixed successful model completions for supervised continuation.Source: §6.1 · p. 7
• 322 versus 71 Mistral targets succeed after AG-CoT SFT versus Direct SFT, a gain of 245 targets; continuation adds 6 more successes.The trace-supervision gain appears in a second model family, while the continuation increase is smaller.Source: §6.1 · pp. 7–8

6.2 COMPLEMENTARY 32B RESULTS

• Near-saturated syntax and Clifford validity do not ensure target matching: most valid 32B circuits still prepare the wrong state.The 32B study evaluates direct results on 3,894 prompts.Source: §6.2 · p. 8
• 6.14% is the highest reported 32B direct StateEq@1, achieved by RFT-v1; its strict saved-label Exact@1 is 3.13%.Neither Step AG-CoT nor GRPO-v2 exceeds Basic AG-CoT on either direct target-match metric.Source: §6.2 · p. 8, Table 3 · p. 8
• 10.07% versus 4.42% is the observed Basic AG-CoT Pass@64 under StateEq versus strict saved-label equality on the same candidates, a 2.28× coverage increase.The 10.07% result is finite-budget search coverage, not a direct-generation rate; the RFT pool separately reaches observed saved-label Pass@64 of 5.19%.Source: §6.2 · pp. 8–9, Table 4 · p. 8

6.3 ERROR ANALYSIS

• 7.77% of valid state-incorrect AG-CoT outputs lack at most two independent target constraints, versus 4.09% for Direct SFT; RFT versions reach 8.02–8.18%.These distributions use each model’s own valid-error set, not a common set of failed targets.Source: §6.3 · p. 9, Table 5 · p. 9
• 112 of 961 valid 32B RFT-v1 errors at five to eight qubits lack at most two independent target constraints, versus 8.84 expected for random programs preserving gate types and order.The deficit counts missing independent target constraints, not gates needed for circuit repair.Source: §6.3 · p. 9

7 CONCLUSION

• Algorithmic traces and exact verification together improve semantic correctness in language-model Clifford circuit synthesis.The conclusion also reports gains from verifier-filtered continuation and higher proportions of near-correct outputs among remaining valid errors.Source: §7 · p. 9
• Across the 3,661-target evaluations, AG-CoT SFT raises Qwen correct outputs from 33 to 201 and Mistral outputs from 71 to 316.Verifier-filtered continuation yields 210–215 correct outputs across Qwen RFT versions and 322 for Mistral.Source: §7 · p. 9
• In the complementary 32B study, RFT reaches the highest direct StateEq@1 at 6.14%, while GRPO-v2 does not improve strict saved-label correctness.Verifier-selected search finds additional correct circuits, with coverage reflecting multiple candidates per target.Source: §7 · p. 9

AI USE STATEMENT

• The authors report that they used a large language model to polish manuscript language and verified the claims, proofs, formulations, and reported values against implementation and results.They take responsibility for the manuscript.Source: AI USE STATEMENT · p. 10

A FORMAL TASK AND VERIFIER

• Targets are stabilizer states specified by n independent commuting signed Pauli generators, represented by a tableau containing binary X/Z support and generator signs.The task prompts provide signed generators and ask for an OpenQASM 3.0 program preparing the target from |0⟩^n.Source: A FORMAL TASK AND VERIFIER · p. 13
• The verifier parses each program, checks Clifford convertibility, applies exact tableau updates, then compares the prepared tableau with the target.Strict Exact uses saved-label equality; StateEq instead checks state equivalence, while controlled task success also applies gate, qubit, header, and completion requirements.Source: A FORMAL TASK AND VERIFIER · p. 14
• The verifier separates syntax success, Clifford validity, and state correctness, so a valid circuit can still fail the target-state comparison.Strict Exact requires the saved stabilizer labels to match; StateEq uses tableau equivalence after the same initial stages.Source: A FORMAL TASK AND VERIFIER · p. 14
• Exact@1 averages strict correctness over one candidate per target, whereas Pass@N estimates whether a sampled set of N candidates contains any exact success.The search estimates reuse pools of 64 candidates per target; StateEq-Pass@N substitutes state equivalence for saved-label equality.Source: A FORMAL TASK AND VERIFIER · pp. 14–15
• Conditional exact rate measures saved-label matches among outputs that already pass parsing and Clifford validity.The verifier applies stages in a fixed order, and the first failed stage determines the failure label.Source: A FORMAL TASK AND VERIFIER · pp. 14–15

B DATASET AND PREPROCESSING PROTOCOL

• The 32B split groups duplicate QASM strings, uses a seeded 90/10 train-test split, and has no validation split.The full accepted AG-CoT dataset contains 38,940 examples; the training split has 35,046 and the held-out test set has 3,894 prompts.Source: B DATASET AND PREPROCESSING PROTOCOL · pp. 15–16, Table 8 · p. 16, Table 9 · p. 16
• For Clifford instances, preprocessing converts reference circuits into signed Pauli stabilizer generators while preserving the target representation.A 500-case check compared saved target labels with states prepared by reference circuits; the universal-circuit task retains state-vector targets and is outside this exact-tableau evaluation.Source: B DATASET AND PREPROCESSING PROTOCOL · p. 15
• For 12 qubits, the tableau prompt is roughly 800 characters, compared with roughly 16K characters for the state-vector target.The tableau stores 2n^2 + n bits before text formatting, versus 2^n complex amplitudes for a state-vector target.Source: B DATASET AND PREPROCESSING PROTOCOL · p. 15

C AG-COT ALGORITHM DETAILS

• The construction pairs each emitted circuit with its row-reduction trace; single-qubit instances instead use direct Clifford synthesis without a per-operation reduction trace.The trace records reduction steps, while the preparation circuit runs in the opposite direction.Source: C AG-COT ALGORITHM DETAILS · p. 16
• Verifier filtering retains completions whose circuits pass parsing, Clifford-family checking, and exact target-tableau matching.The accepted 32B AG-CoT dataset contains 38,940 examples with no observed generation failures.Source: C AG-COT ALGORITHM DETAILS · p. 17
• The row-reduction implementation was validated on 1,000 random Clifford tests, but model-generated traces are not separately checked at every intermediate step.Evaluation runs through the emitted program, so verifier acceptance establishes correctness of the final circuit, not every learned trace step.Source: C AG-COT ALGORITHM DETAILS · pp. 17–18
• The target-conditioned recipe builds a deterministic full Clifford tableau from prompted stabilizers, reduces it to identity, then inverts the reduction to synthesize a preparation circuit.Auxiliary destabilizer rows complete the symplectic frame but are not prompt fields or additional target-state constraints.Source: C AG-COT ALGORITHM DETAILS · pp. 16, 18

• GRPO-v2 forms group-relative advantages from 32 sampled outputs per prompt, using verifier-derived rewards rather than SFT’s conditional-likelihood objective.The reward distinguishes exact saved-label matches, other Clifford-valid outputs, non-Clifford outputs, and invalid outputs; partial label overlap receives a fractional reward.Source: D TRAINING AND SEARCH INTERPRETATION · p. 18
• For GRPO-v2, the reward uses the fraction of saved target labels also present in the generated label set as a partial-overlap signal.The reward passage assigns 0.8 times this fraction to Clifford-valid outputs without exact label equality.Source: D TRAINING AND SEARCH INTERPRETATION · p. 18
• Held-out strict saved-label Exact@1 is 2.21% for GRPO-v2, versus 2.62% for Basic AG-CoT SFT, despite rising mean training reward.Mean training reward increases from 0.088 early in epoch 1 to 0.197 late in epoch 3.Source: D TRAINING AND SEARCH INTERPRETATION · p. 18
• The reported 32B RFT training set contains sampled target-output pairs only when the strict saved-label verifier returns Exact(x, y) = 1.This strict filter differs from the 3B continuation’s StateEq-based task-success rule.Source: D TRAINING AND SEARCH INTERPRETATION · p. 18
• Best-of-N applies verifier selection at inference rather than updating model parameters, and RFT reaches observed Pass@64 of 5.19%.Pass@64 measures finite-budget search coverage, not reliable direct generation.Source: D TRAINING AND SEARCH INTERPRETATION · p. 18

E DECODING AND EVALUATION SETTINGS

• The prompt represents each target with stabilizer generators and requests an OpenQASM 3.0 circuit using H, S, and CNOT gates to prepare that state from |0>^n.Evaluation parses outputs without repairing invalid or incomplete programs; StateEq@1 and strict Exact@1 use different success criteria.Source: E DECODING AND EVALUATION SETTINGS · p. 19

F REPRODUCIBILITY DETAILS

• The reproducibility materials identify evaluation inputs, verifier and data-construction artifacts, run records, and software versions needed to reproduce the 32B study.The records include decoding settings and data-manifest details such as split policy, record counts, and checksums.Source: F REPRODUCIBILITY DETAILS · pp. 19–20, Table 10 · p. 20, Table 11 · p. 20

F.1 REPLICATION ACROSS INFERENCE ENVIRONMENTS

• Across inference environments, all 201 AG-CoT successes on A6000 also succeed on H200, which solves one additional target, while RFT version 1 solves the same 213 targets in both.Generated QASM differs across environments, so matching task success does not imply identical output text.Source: §F.1 · p. 20, Table 12 · p. 20

G.1 MATCHED MISTRAL TRAINING

• The matched Mistral study holds prompts, target identities, teacher circuits, and training settings fixed, while AG-CoT completions include additional trace tokens.Continuation retains 983 verifier-accepted responses; the final comparison uses fixed checkpoints and no retries or output repair.Source: §G.1 · p. 21
• AG-CoT gains 246 successes and loses 1 against Direct SFT on matched Mistral targets (p = 2.19 × 10^-72); RFT’s six additional successes are not statistically established (p = 0.441).The comparison uses one greedy completion per target on 3,661 test targets.Source: §G.1 · p. 21

G.2 PAIRED TARGET LEVEL ANALYSIS

• AG-CoT succeeds on 170 Qwen targets missed by Direct SFT, while Direct SFT succeeds on 2 targets missed by AG-CoT; version 2 remains significant after Holm adjustment.The Direct SFT-to-AG-CoT comparison has 172 discordant targets.Source: §G.2 · p. 21

G.3 TASK SUCCESS BY QUBIT COUNT

• At twelve qubits, Qwen Direct SFT solves 2 of 841 targets and AG-CoT solves 40, with AG-CoT solving more targets at every qubit count.Each size group includes all test targets, including invalid or incomplete outputs.Source: §G.3 · p. 21

G.4 CONSTRAINT DEFICITS IN VALID ERRORS

• AG-CoT and RFT versions have lower mean constraint deficits among remaining valid errors than Direct SFT.The passage describes this as consistent with the median and low-deficit proportions discussed in Section 6.3.Source: §G.4 · p. 21

• Direct SFT raises TaskSuccess@1 from 0 to 41 (1.12%) for Qwen2.5-3B-Instruct and from 0 to 78 (2.13%) for Mistral-7B-Instruct-v0.3.Both use the same 35,046 target-to-QASM training instances and one greedy completion with a 2,048-token generation cap and strict no-repair evaluation.Source: §G.5 · pp. 21–22, Table 14 · p. 22
• For 32B RFT, observed Pass@64 is 5.19%, compared with estimated Pass@1 of 3.18% from the same candidate pool.For Basic AG-CoT, state equivalence yields 2.28 times the measured 64-candidate coverage of saved-label equality, while 89.93% of prompts remain uncovered.Source: §G.5 · p. 22, Table 15 · p. 23
• The 64-sample budget has its highest coverage for two-qubit prompts, a bucket containing only 30 prompts, so the stratification is diagnostic rather than a scaling law.Source: §G.5 · p. 22
• The 32B Best-of-64 evaluation verifies 249,216 candidates over 3,894 prompts and takes 9 h 52 min 49 s of wall-clock time.This timing is for the Best-of-64 evaluation, not average generation or verifier latency.Source: §G.5 · p. 22, Table 16 · p. 23
• The exploratory QASM-only SFT run has an 83% truncation rate under its 2,048-token cap, making it a format-and-budget diagnostic rather than a directly comparable method ranking.Its output-extraction and verifier rules are unchanged.Source: §G.5 · p. 23, Table 17 · p. 23

H TARGET CONSTRAINT RETENTION IN 32B ERRORS

• Among five-to-eight-qubit RFT-v1 errors, 112 outputs have deficit at most two, versus 8.84 expected (reference SD 2.45), or 12.7 times the reference count.The length-matched reference preserves gate types and order while randomizing operands; larger-system comparisons apply only to retained outputs after character-limit exclusions.Source: H TARGET CONSTRAINT RETENTION IN 32B… · pp. 23–24, Table 18 · p. 24
• At fixed unsigned overlap across 2,581 valid errors, the sign reference predicts 1,639.2 conflicts (SD 16.5), compared with 1,335 observed.The reference assigns independent fair relative signs to a basis of the shared stabilizer subspace.Source: H TARGET CONSTRAINT RETENTION IN 32B… · p. 24, Table 18 · p. 24

H.1 COMPLETE ERROR DISTRIBUTION

• Nonzero overlap occurs in 1,246 of 2,581 valid state-incorrect outputs (48.28%); across all errors, median squared overlap is 0 and median constraint deficit is 7.Among zero-fidelity outputs, 170 (12.7%) lack at most two independent constraints, although most differ in more than two.Source: §H.1 · p. 24, Table 20 · p. 26

I FAILURE TAXONOMY

• Saved-label mismatches account for more than 96% of held-out prompts across the three 32B direct-verifier rows, despite rare syntax failures and no non-Clifford valid parses.The strict categories are distinct from the state-equivalence and constraint analyses of RFT-v1 errors.Source: I FAILURE TAXONOMY · pp. 24–25, Table 21 · p. 26

I.1 DEPTH SENSITIVITY

• GRPO-v2 Exact@1 is 74.5% for 47 one-to-two-layer targets and 0.7% for 142 targets with 15–20 layers; there are no matches among 664 targets with 21–50 layers.The group with more than 50 layers has one strict match among 2,743 targets.Source: §I.1 · p. 26, Table 22 · p. 26

I.2 UNCERTAINTY AND SEARCH OUTCOMES

• A search miss means none of a prompt’s 64 sampled candidates passed exact verification; the appendix reports uncertainty intervals and strict saved-label search coverage.Source: §I.2 · pp. 26–27, Table 25 · p. 27