AlchemQ: Proof-Carrying Quantum Circuit Optimization with Per-Result Equivalence Certificates

AI summary

Overview

Research area: Quantum compilation and circuit optimization, specifically proof-carrying compilation — attaching machine-checkable equivalence evidence to each optimized circuit rather than trusting the optimizer.

Technical level: Advanced. The paper assumes familiarity with quantum circuits, the ZX-calculus, OpenQASM, T-count/two-qubit-count/depth metrics, and fuzzy t-norms.

Scope (one sentence): The paper describes and evaluates AlchemQ v0.5, a small proof-of-concept optimizer–certifier system whose every returned circuit ships with a self-contained, versioned, tamper-evident certificate of equivalence-up-to-global-phase, and reports benchmarks, two certification case studies, and a first hardware experiment on IBM Heron r2.

What This Paper Is About

Quantum circuit optimizers rewrite circuits with no per-result guarantee, so an optimizer bug can silently corrupt every circuit it touches — and the paper cites formal-verification work (CertiQ, Giallar) that found real bugs in Qiskit passes, plus recent audits of compiler defects. AlchemQ separates the untrusted optimizer from a trusted certification layer: a beam search proposes rewrites, and an independent certifier must prove each candidate equivalent to the original (up to global phase) before it can be returned. The goal is not a faster optimizer but a contract: every emitted circuit pair comes with a machine-verifiable artifact a third party can re-check offline.

Key Contributions

1. An open certification protocol for circuit pairs (version 0.2.0). Certificates are self-contained JSON artifacts carrying a canonical gate-canon-v1 hash, an artifact byte hash, a declared equivalence method, tri-state verdicts (certified / rejected / inconclusive), measured residuals, versioned phase-note schemas (phase-note-v1, phase-note-v2), a rewrite_log_hash, and a 128-bit protocol-tagged cert_id, plus a strict migration path from protocol 0.1.1 (migrate_cert_v1_to_v2).

2. A reference certifier and standalone verifier. Equivalence up to global phase is proved by ZX-calculus full reduction, with a numeric tensor fallback for circuits of at most six qubits that estimates relative phase by the optimal Hilbert–Schmidt overlap φ* = arg⟨t₀,t₁⟩ rather than a single pivot element. The verifier is released separately under Apache-2.0; the optimization engine remains proprietary.

3. A toy search agent with structural safety guarantees. Under three fuzzy t-norms (Gödel, product, Łukasiewicz), the agent is structurally incapable of returning an uncertified circuit, never scores below the PyZX-based baseline, and since v0.4 guarantees no componentwise regression against the original circuit — not merely aggregate non-inferiority.

4. A gated empirical evaluation and two diagnostic case studies. A 100-circuit benchmark with gates G0, G1, G2 passed, mutation testing, cross-platform reproduction, and two root-caused certification failures (one upstream in PyZX, one in the authors' own phase notes).

Main Findings

• All optimizations certified, none failed: All 400 optimizations (100 circuits × baseline plus three t-norms) terminate without errors or timeouts, and every returned circuit is certified equivalent.
• Certificates validate cross-platform: All three artifact sets — 400 legacy V1, 400 historical V2, and 400 fresh V2 certificates, plus a determinism audit — validate 400/400 on both Linux/Python 3.12 and macOS/Python 3.14.
• The test suite passes on two platforms: a 2998-test suite passes on both platforms in approximately 80 s.
• Mutation testing catches everything: every mutation is detected, the certifier being sound in practice on the tested pairs (Gate G1 reports 100/100 and 100/100 on 200 constructed pairs).
• The baseline is strong, and the agent matches or beats it: the PyZX-based baseline reduces T-count by 21.4% on average over the 82 circuits with nonzero T-count. Recomputed under the current zero-baseline score semantics, the agent is never worse than the baseline anywhere and is strictly better on 9/100 circuits under the Gödel and product norms (8/100 under the semantics of the archived run).
• The choice of t-norm barely matters on standard circuits: the three norms return identical final circuits on all 100 standard benchmark circuits, diverging only on 4/38 and 3/38 instances of an adversarial 38-circuit ablation suite.
• Case study 1 — an upstream false negative: a certifier rejection of variational_n4 was root-caused to a pivot-normalization bug in PyZX's compare_tensors (pivot amplitude 4.7×10⁻⁹, noise amplification ~2×10⁸); the optimal-overlap residual for the same pair is 7.4×10⁻¹¹. A correct optimization had been made to look unverifiable.
• Case study 2 — a portability bug in the authors' own artifacts: eight v0.4 certificates were rejected on macOS; the root cause was BLAS-dependent raw floats recorded in phase_note. Both defects are reported fixed.
• Componentwise regression was real but aggregate-invisible: the baseline itself regresses some objective on 74/100 benchmark circuits, and in the archived pre-v0.4 run all 42/100 componentwise-regressing agent outputs sat at aggregate 0, because the score clamp forces a regressing candidate to 0 under all three norms.
• First hardware experiment (IBM Heron r2, ibm_kingston): compiled to the native gate set, the certified-optimized benchmark circuit is 78% shallower with 65% fewer two-qubit gates than the original. Point estimates favor the optimized circuit on all three output-quality metrics, but differences are not statistically significant at 1024 shots per arm.
• Illustrative per-circuit result (simon_n6, transpiled): T-count 14 → 0, two-qubit count 14 → 4, depth 33 → 7, gate count 56 → 15, certified by zx-full-reduce with measured phase 0.0 and residual 0.0.

Methodology in Plain English

The system treats optimization and verification as separate concerns joined by a contract. An untrusted beam search proposes local rewrites — gate merging, commutation pushes, inverse cancellation, and a PyZX full_reduce-plus-extraction pass — with each suggestion a deterministic function of the current circuit and a seeded random generator.

Before any candidate may enter the beam, it must pass a certification hard gate. The certifier parses both circuits from OpenQASM 2.0, checks qubit counts match, converts both to ZX diagrams, and interleaves full_reduce with normalize; if the result is a bare identity diagram, the circuits are equal exactly and the surviving graph scalar supplies the relative phase. If ZX is inconclusive and the circuit has at most six qubits, a numeric fallback computes dense tensors and picks the global phase that minimizes the Frobenius distance between them, deciding on the phase-aligned tensors and a normalized residual (≤ 2×10⁻⁶ in protocol 0.2.0; atol = rtol = 10⁻⁹ in 0.1.1). Everything else — too many qubits, non-unitary records like measure, unstable round-trips, degenerate or orthogonal tensors — yields inconclusive rather than a guess, and an inconclusive certificate is explicitly "evidence of nothing".

Candidates are ranked lexicographically by (aggregate, ¬regresses, sum of scores, −steps, gate count, canonical form), with the aggregate computed by a t-norm over clamped per-objective improvement scores. A persistent best-by-rank tracker sits outside the beam so truncation cannot lose it, and a final componentwise re-check replaces the winner with the original circuit if any objective regressed.

The evaluation uses 100 circuits: 62 real circuits (26 native and 25 transpiled QASMBench small-category circuits, 11 Feynman unitaries) plus 38 generated Clifford+T instances (QFT, adders, QAOA MaxCut, VQE ansätze, Grover, Toffoli decompositions, random symplectic circuits), with fixed seed 42. Non-unitary content was stripped to the unitary kernel in 51 circuits. Three gates guard the claims: G0 compares metrics against an independent hand-written QASM parser; G1 measures certifier completeness and soundness on constructed equivalent and inequivalent pairs; G2 is reported as passed. (The paper text supplied here is truncated inside the G1 description, so the detailed G1 protocol text and the G2 criteria and numbers beyond "passed" are not available in the content provided.) Verification of a certificate re-does everything from the file alone: schema and trust-boundary checks, hash recomputation, QASM re-parsing, re-execution of the declared method, phase-note validation, metric recomputation, and residual reproduction.

Why This Matters

Impact on research. The paper reframes compiler trust as an evidentiary problem rather than a code-provenance problem. Verified compilers (VOQC, CertiQ, QBlue) prove the compiler correct once and for all but cover only what the compiler does; AlchemQ's per-artifact contract lets any optimizer — including a learned or third-party one — sit behind the same gate. The two case studies are the concrete argument: a certification layer that fails loudly exposed a numerical bug in a widely used library (PyZX) and a cross-platform reproducibility defect in the authors' own artifacts, both of which a bare "trust me" claim would have hidden.

Real-world applications:

• Fault-tolerant pipeline planning, where T-count and two-qubit count dominate the cost of magic-state distillation and routing.
• Validating third-party or vendor-supplied compiled circuits before they run on expensive hardware, without re-running the original optimizer.
• Auditing learned or heuristic optimizers (RL-based rewriters, LLM-generated circuit transformations) by wrapping them in a certify-or-discard gate.
• Regression testing of compiler releases: mutation testing and hash-chained certificates as a CI artifact rather than a log line.

Industry relevance. Production compilers ship long rewrite sequences with no per-result guarantee, and the paper cites Qiskit issue numbers, SQbricks audits reporting seventeen bugs across four platforms, and a documented false "equivalent" verdict by QCEC under phase shifts. A self-contained, engine-agnostic certificate format with tri-state verdicts is directly usable as an acceptance criterion in a compilation service. The authors are explicit that the release is split: certificate specification and reference verifier under Apache-2.0, optimization engine proprietary.

Future Directions

• Independent verifier engine. The verifier currently shares its ZX implementation with the certifier, so an upstream ZX bug could in principle affect both sides; a separately implemented or externally validated engine would close that gap.
• Cross-validation against established checkers. Verifying AlchemQ certificates with QCEC (or an MPO-based engine emitting the same artifact under a different method tag) is named as future work and would test the format's engine-agnostic claim.
• Scaling the certification bottleneck. The ZX path is acknowledged as the bottleneck in both coverage (it may be inconclusive on large non-Clifford circuits) and runtime, with the tensor fallback capped at six qubits; extending coverage is the main route to certifying larger circuits.
• Hardware-aware optimization under certified equivalence. The planned noise-aware layer would treat calibration data as a risk-adjusted, uncertainty-bearing signal while preserving certified equivalence — a combination the authors say they have not found in the literature — and an RL policy could be added later provided it inherits the same hard gate.

Target Audience

Researchers and engineers building practical, trustworthy quantum compilation pipelines: compiler and toolchain developers who want per-result correctness evidence, formal-methods researchers interested in lightweight per-artifact certification as an alternative to whole-compiler verification, and quantum software teams who need to validate optimized circuits before spending hardware time. Readers wanting implementation details of the proprietary search agent, or a competitive performance comparison against industrial passes, will not find them here — the paper positions itself as a bounded pilot study and states its limitations in full in its Section 12.

Authors’ abstract

We present AlchemQ v0.5, a proof-of-concept system that couples an untrusted beam-search optimizer with a machine-checkable per-result certification layer and a versioned certificate protocol (0.2.0), so that every optimized circuit ships with a verifiable artifact rather than a bare claim. The certifier proves equivalence up to global phase by ZX-calculus full reduction, with a numeric-tensor fallback based on the optimal Hilbert-Schmidt overlap. Certificates are self-contained and tamper-evident: canonical gate-canon-v1 hashes, measured residuals, tri-state verdicts (certified/rejected/inconclusive), and versioned phase-note schemas for cross-platform reproducibility. The agent aggregates three fuzzy t-norms, cannot return an uncertified circuit, and since v0.4 guarantees no componentwise regression against the original. On a benchmark of 100 circuits, all 400 optimizations terminate without error, every returned circuit is certified, every mutation is detected, and a 2998-test suite passes on two platforms. The PyZX baseline is strong (21.4% mean T-count reduction over 82 circuits) and the agent is strictly better on 9/100; the three t-norms return identical circuits on all 100 standard instances, diverging only on 4/38 of an adversarial suite. Two case studies are new: a false negative root-caused to a pivot-normalization bug in PyZX's compare_tensors (pivot 4.7e-9; the optimal-overlap residual is 7.4e-11), and eight certificates rejected on macOS due to BLAS-dependent floats in phase_note. Both were fixed; all artifact sets validate 400/400 on both platforms. A pilot run on IBM Heron r2 gives a certified circuit 78% shallower with 65% fewer two-qubit gates; output quality favors it on all three metrics but is not significant at 1024 shots. We release the certificate specification and a standalone reference verifier (Apache-2.0) with data and scripts; the engine is proprietary.