PaperlayerView exact revision on arXiv

Source-linked AI summary

ConQEC: Concolic Testing for Quantum Error-Correcting Code Implementations

Zihao Li, Ji Guan, Mingsheng Ying

arXiv:2610.31443v1quant-phcs.SE

TL;DR

QECC testing needs to generate concrete faults while explaining where an implementation’s repair path diverges, rather than reporting only a final failure. ConQEC combines symbolic repair-path constraints with paired replay to produce FSDR witnesses. It detects the seeded bug in every evaluated case and reports replay-valid, fault-localizing witnesses across generated and public QECC artifacts with up to thousands of qubits.

  • Problem

    QECC implementations combine syndrome extraction, decoder dispatch, recovery, and logical checks, yet developers lack a scalable workflow that generates concrete faults and identifies the first repair-path divergence.

    Source: §I · p. 1

  • Method

    ConQEC uses symbolic constraints over Pauli faults and repair-path behavior to propose tests, then replays each fault against the implementation and reference contract to produce staged evidence.

    Source: §I · p. 2, A. Evidence Contract and Bug Classes · p. 3, B. Symbolic Repair-Path Model · p. 4

  • Results

    On generated QECC families and public artifacts with up to thousands of qubits, ConQEC detects every seeded bug and reports a replay-valid, fault-localizing FSDR witness for each.

    Source: §I · p. 2

  • Takeaways & Limitations

    The evaluation shows that the same replay-backed evidence contract can be instantiated on generated QECC implementations and public artifacts.

    Source: §VII · p. 11

    The seeded localization study measures generation and localization of exposed repair-path bugs, not their natural prevalence; broader Tesseract coverage requires structured REPEAT-block handling, and temporal-history bugs require history predicates.

    Source: B. RQ1: Replay-Backed Fault Localization · p. 8, §V · p. 11

Abstract

from arXiv · show

Quantum error-correcting code (QECC) implementations are hybrid software-control systems: measured syndromes drive decoder dispatch, recovery actions, and logical checks. Existing QECC verification techniques can prove formal obligations, and general quantum testing can expose final failures, but developers still lack a scalable testing workflow that generates concrete faults and explains where a QECC repair path first diverges. This paper presents ConQEC, to our knowledge the first concolic testing framework for QECC implementations. By combining concrete (Pauli) fault replay with symbolic repair-path constraints, ConQEC generates tests that expose not only final logical failures but also fault--syndrome--decoder--recovery (FSDR) diagnostics: the injected fault, observed syndrome, decoder decision, recovery action, oracle result, and earliest divergent stage. Its symbolic encoding of Pauli faults, syndrome predicates, decoder and recovery relations, and oracle checks enables this diagnostic workflow to scale beyond exponentially increasing amplitude-level quantum-state reasoning. We implemented ConQEC and evaluated it on generated source-level QECC families and public QECC artifacts with up to thousands of qubits. ConQEC detects the seeded bug in every experimental case and reports a replay-valid, fault-localizing FSDR witness for each.

I. INTRODUCTION

QECC implementations combine syndrome measurement, decoder dispatch, recovery, and logical checks, so a failed final check alone may not identify where repair diverged. ConQEC combines symbolic repair-path generation with paired replay to produce concrete, fault-localizing witnesses.

I. INTRODUCTION

  • A QECC implementation can diverge through a wrong measurement bit, decoder branch, recovery case, or correction location even when the code theorem is correct.Source: §I · p. 1
  • A useful bug report records the fault, syndrome, decoder decision, recovery action, oracle result, and earliest divergent stage, supporting inspection, minimization, and regression testing.Source: §I · p. 1
  • Existing formal-verification tools primarily check correctness obligations, while general quantum concolic testing uses amplitude-based constraints that are difficult to scale to large QECC implementations.Source: §I · pp. 1–2
  • ConQEC models tests as FSDR repair paths and accepts a bug witness only after actual/reference replay localizes the earliest divergence.Source: §I · p. 2
  • Symbolic constraints over Pauli faults, syndromes, decoder and recovery relations, and oracle checks avoid amplitude-level state reasoning while targeting thousand-qubit QECC behaviors.Source: §I · p. 2
  • Across generated QECC families and public artifacts with up to thousands of qubits, ConQEC detects every seeded bug and reports a replay-valid, fault-localizing FSDR witness for each.Source: §I · p. 2

A. Quantum Error-Correcting Code

A QECC repair path extracts syndrome bits, maps them to a decoder correction, and applies recovery. The motivating example shows how concolic testing can identify a decoder divergence that a final failure alone cannot localize.

A. Quantum Error-Correcting Code

  • A syndrome-based repair path uses parity-check measurements to produce classical bits, a decoder to select a correction, and recovery to restore intended logical behavior.Source: A. Quantum Error-Correcting Code · p. 2

B. Concolic Testing

  • Concolic testing combines concrete execution with constraint solving, changing path conditions to generate inputs that exercise different behavior; in QECC, the input is a Pauli fault and the path is the repair sequence.Source: B. Concolic Testing · p. 2

C. Motivating Example

  • For fault X@q0, the syndrome is (1, 0), but the implementation chooses X@q1 while the reference chooses X@q0, making the decoder the first divergent stage.Source: Figure 2 · p. 3, C. Motivating Example · p. 3
  • A final logical-check failure does not identify whether syndrome extraction, decoder choice, recovery, or the final check caused the divergence.Source: C. Motivating Example · p. 3

III. CONQEC DESIGN

  • ConQEC separates candidate generation from evidence: symbolic constraints propose Pauli faults, and paired replay against a reference contract determines coverage credit and whether to accept a debugging witness.Source: §III · p. 3

A. Evidence Contract and Bug Classes

ConQEC treats a test as a replayed repair-path execution and requires comparison with reference behavior before reporting a bug witness. The witness records observable implementation and reference behavior, with classification based on the earliest exposed divergence.

A. Evidence Contract and Bug Classes

B. Symbolic Repair-Path Model

ConQEC models repair paths with compact constraints over legal Pauli faults, syndrome predicates, and available decoder and recovery behavior. The model generates targeted candidate faults without enumerating the concrete fault space or using an amplitude-level quantum state vector; paired replay supplies concrete testing evidence.

B. Symbolic Repair-Path Model

  • Legal fault atoms receive Boolean indicators, while ΦF encodes the declared fault domain, including weight bounds and allowed injection sites.An indicator is 1 when its corresponding fault atom is selected.Source: B. Symbolic Repair-Path Model · p. 4
  • Each check-like predicate is represented as an affine parity expression, so it flips when an odd number of selected faults touch its support.The predicate values induce the symbolic syndrome or detector vector.Source: B. Symbolic Repair-Path Model · p. 4
  • When available to the generator, decoder behavior is represented as a relation between syndrome and decoder decision, and recovery behavior as a relation from syndrome and decision to recovery result.Unavailable decoder or recovery internals are observed during paired replay rather than invented by the symbolic generator.Source: B. Symbolic Repair-Path Model · p. 5
  • The symbolic repair-path model represents many concrete Pauli fault patterns at once, enabling targeted solving without fault-space enumeration or an amplitude-level state vector.Paired replay turns selected candidates into concrete testing evidence.Source: B. Symbolic Repair-Path Model · pp. 4–5

C. Objectives and Candidate Generation

ConQEC selects solver objectives over reachable repair-path behavior, including measurement outcomes, stabilizer conditions, transitions, and likely implementation–reference divergences. It materializes objective-constrained candidate faults and credits coverage or accepts witnesses only after replay.

C. Objectives and Candidate Generation

  • Coverage targets reachable measurement outcomes, stabilizer conditions, and transition sequences, while failure-directed objectives target likely implementation–reference divergences.The coverage denominator is repair-path behavior rather than merely source branches.Source: C. Objectives and Candidate Generation · pp. 5–6
  • Stabilizer-condition objectives record how many selected fault atoms touch a check, distinguishing how a measurement outcome was reached.For the example, one fault touching σ0 covers µσ0 = 1; a two-fault model can test µσ0 = 2.Source: C. Objectives and Candidate Generation · p. 5
  • Transition-sequence objectives cover ordered links from stabilizer conditions to decoder decisions, syndromes to decoder decisions, and decoder decisions to recovery results.A replayed test covers an obligation when its repair path contains the corresponding ordered pair.Source: C. Objectives and Candidate Generation · pp. 5–6
  • Coverage reports count obligations covered by at least one replayed fault for each layer.OL(T) is the subset of obligations in OL covered by the replayed test set T.Source: C. Objectives and Candidate Generation · p. 6
  • Each candidate query combines the legal fault domain and syndrome equations with a constraint for the selected objective, such as a measurement value, stabilizer condition, transition, or stage disagreement.Satisfying assignments become concrete Pauli faults, then paired replay validates them; unused variables are ignored during materialization.Source: C. Objectives and Candidate Generation · p. 6

D. Concolic Loop with Paired Replay

ConQEC alternates between solver-guided fault generation and paired replay, which determines coverage progress and whether a bug witness is accepted. A witness is accepted for an oracle failure or a first repair-path divergence, including divergences whose final oracle result is masked.

D. Concolic Loop with Paired Replay

  • A bug witness is accepted when replay finds either an oracle failure or a nonempty first-divergence stage.The divergence marks the earliest FSDR stage where paired replay violates the reference contract, even if the final oracle is masked.Source: D. Concolic Loop with Paired Replay · p. 6
  • For the motivating at-most-one-X-fault bug, replay of X@q0 yields syndrome (1, 0), different implementation and reference decoder decisions, and a decoder-stage divergence.The observed oracle result is FAIL, so the candidate is accepted as an FSDR bug witness.Source: D. Concolic Loop with Paired Replay · p. 6
  • The loop initializes a symbolic repair-path model and clean replay, then repeatedly solves for an unseen fault targeting an uncovered objective and validates it by paired replay.Replay updates coverage and records implementation and reference traces, oracle result, and first divergence.Source: D. Concolic Loop with Paired Replay · pp. 6–7

IV. EVALUATION

The evaluation is organized around replay-backed fault localization, semantic coverage, scale and cost, and applicability to public QECC artifacts.

IV. EVALUATION

  • RQ1 asks whether ConQEC localizes repair-path faults as actionable FSDR witnesses at thousand-qubit scale.Source: §IV · p. 7
  • RQ2 compares repair-path semantic guidance with strong valid-input random testing on hard stabilizer obligations.Source: §IV · p. 7
  • RQ3 investigates source-level QECC-family scaling and which phase dominates the cost.Source: §IV · p. 7
  • RQ4 asks whether supported adapters let ConQEC operate on recognized public QECC artifacts.Source: §IV · p. 7

A. Experimental Setup

ConQEC is implemented as a testing layer over the QSE symbolic-stabilizer backend, using adapters to expose QECC-specific objects. Evaluation covers generated source-level subjects and public artifacts, with experiments run in an isolated Docker environment.

A. Experimental Setup

  • Adapters export each subject’s Pauli fault model, exposed predicates, optional decoder or recovery relations, and paired replay entry points.ConQEC builds semantic objectives from these objects and credits coverage or bug evidence only after replay.Source: A. Experimental Setup · p. 7
  • The evaluation spans generated repetition, surface/toric, Tanner/LDPC-style, color-code, and small-block subjects, plus supported Tesseract Stim artifacts and a PyMatching regression.RQ2 uses a repetition-code scale ladder; RQ3 reports source-scale frontiers on repetition, surface/toric, and Tanner/LDPC rows.Source: A. Experimental Setup · p. 7
  • Experiments ran as isolated Docker jobs on an AMD EPYC 7702 server with 128 physical cores and 2.0 TiB memory.The environment used Ubuntu 24.04.4 LTS, Docker 29.4.3, Julia 1.10.10, QuantumSE, and Z3 4.12.4.Source: A. Experimental Setup · p. 7

B. RQ1: Replay-Backed Fault Localization

ConQEC localizes seeded repair-path faults through replay-backed witnesses, including at thousand-qubit scale. Its results measure localization capability and generation effort for seeded faults, not the natural frequency of bug classes.

B. RQ1: Replay-Backed Fault Localization

  • The 195-mutant campaign applies 15 fixed source-level mutations to each of 13 configurations across five repair-stage bug classes.The five classes cover syndrome extraction, measurement-register use, decoder dispatch, unhandled syndromes, and recovery-contract violations.Source: B. RQ1: Replay-Backed Fault Localization · p. 7
  • Mutation operators are fixed and applied uniformly; generation receives no mutation location, trigger, class, wrong target, or expected witness.The campaign therefore tests localization without revealing the seeded mutation’s details to the generator.Source: B. RQ1: Replay-Backed Fault Localization · p. 7
  • 156/195 seeded repair-path faults are localized by B = 2 and all 195 by B = 4; branch-order search finds none and random testing averages 15.7/195 at B = 4.With equal elapsed-time budgets, random leads slightly at 1 s, while ConQEC leads by 10 s and reaches 195/195 by 60 s.Source: B. RQ1: Replay-Backed Fault Localization · p. 8, Table III · p. 8
  • The first four repair-path bug classes yield witnesses at B = 2, while recovery contract violations first yield them at B = 4.The two earlier failure-directed objectives for recovery contract violations are unsatisfiable.Source: B. RQ1: Replay-Backed Fault Localization · p. 8
  • Accepted witnesses span five QECC families, reaching 1500 physical qubits and 1499 checks; the largest non-repetition witness has 1058 qubits and 1058 checks.The largest sparse-check witness reaches 1000 qubits and 1000 checks.Source: B. RQ1: Replay-Backed Fault Localization · p. 8, Table V · p. 8
  • Every accepted row is a replayed debugging artifact, so the campaign measures seeded-fault localization and generation effort rather than natural bug-class frequency.Witnesses are not merely solver-produced candidates.Source: B. RQ1: Replay-Backed Fault Localization · p. 8

C. RQ2: Semantic Coverage Analysis

RQ2 compares QECC semantic coverage under ConQEC and valid-input random testing on a repetition-code scale ladder. ConQEC covers hard local obligations and repair-path transitions more effectively, while random testing remains competitive on shallow outcomes.

C. RQ2: Semantic Coverage Analysis

  • Measurement-outcome coverage tracks both Boolean outcomes of exposed predicates; stabilizer-condition coverage distinguishes the number of selected fault atoms in each check’s support.The declared fault model determines which atom counts are reachable; pair-mask coverage is a representative hard sublayer of stabilizer-condition coverage.Source: C. RQ2: Semantic Coverage Analysis · p. 8, Figure 4 · p. 9
  • Transition-sequence coverage records ordered syndrome-to-decoder and decoder-to-recovery transitions when explicit decoder and recovery relations are available.A transition is credited only when paired replay confirms it.Source: C. RQ2: Semantic Coverage Analysis · p. 8
  • The controlled ladder uses repetition codes with n = 10, 100, and 1000 qubits and legal weight-2 X faults; both methods share the fault domain and paired-replay acceptance rule.Random samples legal fault pairs uniformly without replacement, and both methods start from the same clean seed included in budget B.Source: C. RQ2: Semantic Coverage Analysis · p. 8
  • At the ends of the campaigns, ConQEC reaches full stabilizer-condition coverage at all three scales, while random testing falls behind as n grows; transition-sequence coverage also separates at larger n.Measurement-outcome coverage remains an area where random testing is competitive.Source: C. RQ2: Semantic Coverage Analysis · p. 9, Figure 4 · p. 9
  • At B = n/2, ConQEC covers 44.4%, 49.5%, and 49.9% of pair-mask obligations; random testing covers 8.89%, 0.61%, and 0.10% for n = 10, 100, and 1000.In this ladder, a legal weight-2 fault can cover at most one pair-mask obligation, so full coverage requires at least n −1 non-clean tests, or B = n including the clean seed.Source: C. RQ2: Semantic Coverage Analysis · p. 9
  • ConQEC solves directly for local objectives of the form µc(F) = 2, while uniform sampling must select both fault atoms in a check support.Across the criteria, ConQEC covers hard local activations and repair-path transitions more effectively, while random remains competitive on shallow outcomes.Source: C. RQ2: Semantic Coverage Analysis · p. 9

D. RQ3: Scale and Cost

RQ3 finds that source-level campaigns reach thousand-qubit scales, with repeated objective generation and solver/backend search setting the larger-campaign boundary rather than replay. RQ4 instantiates replay-backed evidence on public artifacts through detector-adapter execution and wrapper-level decoder-regression replay.

D. RQ3: Scale and Cost

  • Full campaigns complete through repetition n = 3000 and surface/toric d = 41; single-objective runs reach n = 5000 and d = 51.At the largest rows, full campaigns hit the timeout after writing 24 and 5 SMT queries, respectively; Tanner/LDPC is limited by source-generator capability.Source: D. RQ3: Scale and Cost · p. 10, Table VII · p. 10
  • Solver/backend time dominates completed runs, while paired replay takes 0.194ms median and 0.553ms p95.Replay accounts for 0.0016% of median and 0.0038% of p95 wall-clock time; the phase-cost split is shown in Figure 5.Source: D. RQ3: Scale and Cost · p. 10, Figure 5 · p. 10

E. RQ4: Public Artifact Applicability

V. DISCUSSION AND THREATS TO VALIDITY

The discussion bounds ConQEC’s claims by its replay evidence, subject interfaces, and evaluation settings. The related-work comparison distinguishes its repair-path constraints from amplitude-based quantum concolic testing, and the conclusion reports results across generated and public QECC artifacts.

V. DISCUSSION AND THREATS TO VALIDITY

  • RQ1 measures localization of seeded repair-path bugs, not their natural prevalence; RQ3 reports empirical scale under the configured backend and timeout, not an asymptotic bound.RQ2 evaluates semantic coverage on repetition codes with legal weight-2 faults against uniform sampling; other code families or fault models may stress different layers.Source: §V · p. 11
  • ConQEC’s generation targets depend on exposed subject semantics: transition objectives require explicit decoder and recovery relations, and broader Tesseract coverage requires structured REPEAT handling.New interfaces require reference relations and manual replay mappings; temporal-history bugs require history predicates.Source: §V · p. 11

VI. RELATED WORK

  • Unlike amplitude-based QCT, ConQEC encodes QECC repair-path behavior compactly and reports replay-valid witnesses across families reaching thousands of qubits.QCT’s reported branch-coverage evaluation focuses on programs with fewer than five qubits.Source: §VI · p. 11

VII. CONCLUSION

  • Across generated source-level families and public artifacts, ConQEC detects every seeded bug and reports a replay-valid, fault-localizing FSDR witness for each.The conclusion also reports improved hard repair-path coverage, replay not being the scale bottleneck, and evidence-contract instantiation on public artifacts.Source: §VII · p. 11
Loading 2610.31443v1…