A Verified Optimizer for Quantum Circuits

Kesha Hietala; Robert Rand; Shih-Han Hung; Xiaodi Wu; Michael Hicks

Source-linked AI summary

A Verified Optimizer for Quantum Circuits

Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks

arXiv:1912.02250v3Dec 4, 2019cs.PLcs.ETcs.LOquant-ph

TL;DR

Quantum-circuit optimizers need correctness guarantees, but testing them is difficult because quantum execution and simulation can be costly or impractical. VOQC addresses this gap with Coq-verified transformations over SQIR's symbolic semantics, achieving competitive reductions on benchmark circuits while retaining explicit trust and scope boundaries.

Problem
Quantum optimizers can contain bugs, while direct correctness testing is often impractical because quantum algorithms are indeterminate and expensive to execute or simulate.
Method
VOQC expresses circuit transformations as Coq functions over SQIR and proves that their output semantics are equivalent to those of the input circuits.
Results
On 28 benchmarks, VOQC reduced total gate count by 17.8% on average and T-gate count by 41.4% on average, while supporting a range of verified optimizations.
Takeaways & Limitations
SQIR's symbolic semantics and proof automation make it possible to verify full-circuit transformations in addition to local optimization rules.
Takeaways & Limitations
The extracted optimizer trusts OCaml implementations of some data types, and its OpenQASM translation and Coq-to-OCaml extraction are not formally verified.

Abstract

from arXiv · show

We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.

1 INTRODUCTION

Quantum-circuit optimization is valuable but difficult to validate because quantum resources are scarce and direct testing is often impractical. VOQC applies Coq-based formal verification to general quantum programs, using SQIR and verified transformations while achieving competitive benchmark performance.

1 INTRODUCTION: Formal verification addresses optimization bugs and testing barriers caused by quantum indeterminacy, execution expense, scarce resources, and constrained qubit connectivity.The paper motivates proof-based correctness because optimized and source programs may be impractical to execute or simulate for direct comparison.
1 INTRODUCTION: SQIR is a Coq-embedded quantum language whose semantics and proof automation support reasoning about global quantum states and verified circuit transformations.Its design uses indexed qubits and separate semantics for general programs and unitary programs to simplify proofs involving linear algebra.
1 INTRODUCTION: VOQC expresses optimizations as Coq functions and proves that each output circuit preserves the input circuit's semantics.The framework also includes verified circuit mapping for target-architecture interaction constraints.
1 INTRODUCTION: 17.8% average total-gate reduction on 28 benchmarks, versus 10.1% for Qiskit, 10.6% for t|ket⟩, and 24.8% for Nam et al.VOQC also reduced T-gate count by 41.4% on average, matching Nam et al. and exceeding Amy et al.'s 39.7%.
1 INTRODUCTION: VOQC is presented as the first fully verified optimizer for general quantum programs.Unlike prior tools limited to reversible circuits, Clifford circuits, local equivalences, or concrete-state validation, VOQC targets general programs with symbolic matrices.
1 INTRODUCTION: VOQC and SQIR are positioned as steps toward a full-scale verified compiler toolchain, including future higher-level translations and noise-oriented optimizations.The paper identifies these as next steps rather than completed capabilities.

2 OVERVIEW

The overview introduces quantum circuits and the verification challenges posed by exponentially sized, globally entangled states. It then presents SQIR and VOQC as a Coq-based representation and optimizer whose transformations are proved semantics-preserving.

2.1 Quantum Programs: An n-qubit state requires a vector of length 2^n, while n-qubit operators require 2^n × 2^n matrices, making the state space exponentially large.Entanglement prevents some states from being decomposed into independently described qubits.
2.2 Quantum Circuits: Quantum programs are circuit descriptions in which wires represent qubits and boxes represent unitary or non-unitary gates such as measurement.High-level frameworks can construct circuits and transform them for gate count, depth, qubit usage, and hardware connectivity.
2.3 sqir: A Small Quantum Intermediate Representation Supporting Verification: The overview frames verification around proving that parameterized circuit programs produce mathematically specified quantum states for arbitrary numbers of qubits.This requires formal states, a program language with semantics, and mechanical reasoning about the resulting matrices.
2.3 sqir: A Small Quantum Intermediate Representation Supporting Verification: SQIR is a small circuit-oriented language deeply embedded in Coq, with syntax, semantics, quantum-state properties, and proof automation defined in its host language.Its libraries support complex numbers and matrices, while isolating unitary subprograms from measurement-dependent density-matrix reasoning.
2.4 voqc: A Verified Optimizer for Quantum Circuits: VOQC optimizations are Coq functions over SQIR circuits proved to preserve the semantics of their inputs.This framework supports verified optimization passes and circuit mapping to satisfy target-architecture constraints.
2.4 voqc: A Verified Optimizer for Quantum Circuits: VOQC differs from translation validation by proving transformations against explicit SQIR semantics, enabling global optimizations beyond peephole equivalences.SQIR's unitary-core design and proof automation support these full-circuit correctness proofs.

3 SQIR: A SMALL QUANTUM INTERMEDIATE REPRESENTATION

SQIR is a small quantum intermediate representation whose unitary programs have matrix semantics designed to simplify verified reasoning. Its concrete qubit indices, explicit typing conventions, and proof-oriented matrix design support scalable circuit-equivalence proofs and source-program verification.

3.2 Semantics: Unitary SQIR programs denote matrices, while full SQIR programs use functions over density matrices; the matrix semantics simplifies proofs of unitary optimizations.Sequential composition is represented by matrix multiplication, with the later program matrix multiplying the earlier one.
3.1 Unitary sqir: Syntax: SQIR programs are sequences of one- and two-qubit gate applications over natural-number indices into a fixed global register.A program is parameterized by a gate set and global-register size, represented in Coq as ucom g n.
3.2 Semantics: Ill-typed programs denote the zero matrix, avoiding repeated well-typedness assumptions in semantic theorems and proofs.Well-typedness requires in-bounds, nonrepeated qubit indices; the latter enforces linearity consistent with the no-cloning theorem.
3.2 Semantics: The semantics maps each local gate to a full-register operation by tensoring its matrix with identity matrices on untouched qubits.The apply1 and apply2 functions embed one- and two-qubit operations into the global dimension d.
3.3 Design for Proofs: SQIR uses concrete qubit indices and phantom matrix dimensions to make disjointness, matrix operations, and proof automation easier to manage.Concrete indices make commuting disjoint gates straightforward to state, while external well-formedness predicates carry most matrix-bound obligations.
3.4 Source-program Proofs: The framework supports verified circuit optimizations and also source-program proofs, illustrated by a correctness proof for GHZ state preparation.The paper notes ongoing efforts to prove more sophisticated algorithms correct in SQIR.

4 OPTIMIZING UNITARY SQIR PROGRAMS

VOQC optimizes unitary SQIR programs through semantics-preserving transformations, including propagation, cancellation, circuit replacement, and connectivity mapping, with correctness supported by Coq automation.

VOQC applies each optimization only when the output is guaranteed equivalent to the input program, including under global phase.Soundness is quantified over any gate set, qubit count, and program, with occasional well-typedness preconditions.
The framework combines replacement with propagate-cancel transformations that commute gates until adjacent gates cancel, then removes the resulting pattern.Supporting library functions operate on flattened instruction lists and are themselves verified for intended behavior.
VOQC’s unitary optimizer uses the universal gate set {H, X, R_z, CNOT}, with rational rotation parameters that support Coq pattern matching and symbolic reasoning.The gate set is translated into SQIR’s base gates for denotational semantics and matches Nam et al.’s set except for the rotation-parameter type.
4.2 voqc Optimization Overview: Not propagation moves X gates through commuting circuits to expose cancellations, but may introduce extra X gates at circuit ends or Z gates internally.Subsequent cancellation and rotation-merging passes are expected to remove some extra gates, while moving X gates can help rotation merging succeed.
4.3 Optimization by Propagation and Cancellation: The verified propagate function returns a propagated gate to its original position when cancellation fails, and is sound given valid commutation and cancellation rules.This general function underlies single- and two-qubit gate cancellation.
4.5 Proving Low-Level Circuit Equivalences: Gridify automates most low-level equivalence proofs, while larger-qubit equivalences such as rotation merging rely on matrix-simplification automation instead.Small equivalences cover patterns of at most five gates on up to three qubits; rotation merging is handled without applying gridify directly.
4.6 Scheduling: The optimizer orders not propagation, Hadamard reduction, gate cancellation, and rotation merging so earlier reductions enable later passes; single-qubit cancellation and rotation merging were most effective experimentally.The ordering follows Nam et al., who did not prove it optimal.
4.7 Mapping: VOQC also verifies mappings from arbitrary circuits to connectivity-constrained architectures, including Tenerife, LNN, LNN ring, and 2D-grid settings.The framework is intended to extend to more sophisticated placement and routing strategies.

5 FULL SQIR: ADDING MEASUREMENT

Full SQIR extends unitary circuits with branching measurement and density-matrix semantics, supporting verified reasoning about non-unitary programs. The section illustrates these ideas with a formally verified quantum-teleportation program and measurement-aware optimizations.

5.1 Syntax and Semantics: Branching measurement extends unitary SQIR so a program can execute one of two subprograms based on a measured qubit.The command meas q P1 P2 branches on the measurement result; non-branching measurement and reset are defined from it.
5.1 Syntax and Semantics: Figure 9 gives non-unitary programs density-matrix semantics, mapping input density matrices to output density matrices.Density matrices represent arbitrary quantum states, including mixed states.
5.2 Example: Quantum Teleportation: Quantum teleportation is encoded as Bell-pair preparation, Alice’s measurements, and Bob’s classically controlled corrections followed by resets.Bob’s controls use the post-measurement classical states of the first two qubits.
5.2 Example: Quantum Teleportation: For every well-formed input density matrix ρ, the verified teleportation program transfers ρ to Bob while resetting the first two qubits to zero.The stated correctness property maps ρ⊗|0⟩⟨0|⊗|0⟩⟨0| to |0⟩⟨0|⊗|0⟩⟨0|⊗ρ.
5.2 Example: Quantum Teleportation: The teleportation proof is fixed-size, whereas arbitrary-dimension density-matrix proofs are more difficult because symbolic states must be multiplied by large matrices.Unitary equivalence proofs avoid carrying a symbolic input density matrix.
5.3 Optimizations for Non-Unitary Programs: VOQC verifies measurement-aware optimizations including removing pre-measurement Z rotations and propagating known classical states through later operations.Propagation can remove controlled-NOT gates, replace them with X gates, select branches, and stop when a qubit becomes non-classical.

6 EXPERIMENTAL EVALUATION

VOQC is evaluated against verified and unverified quantum optimizers on Clifford+T circuit benchmarks using total gate count and T-gate count. It achieves competitive reductions while retaining formally verified transformations, though performance depends on the implemented optimization set and trusted components.

Total Gate Count: 17.8% average total-gate reduction places VOQC ahead of Qiskit’s 10.1% and tket’s 10.6%, but behind Nam et al.’s 24.8% heavy optimization.VOQC outperforms or matches Qiskit and tket on all but one benchmark and beats Nam et al. in 8 of 28 cases.
Comparison with Prior Optimizers: VOQC’s gap from Nam et al. largely reflects missing transformations, especially Toffoli decomposition and floating-Rz-related capabilities.VOQC’s simpler decomposition can sometimes produce more cancellations than Nam et al.’s heuristics, but Nam et al.’s special-purpose decomposition also enables cancellations unavailable to VOQC.
T-Gate Count: 41.4% average T-gate reduction matches Nam et al. and exceeds Amy et al.’s 39.7%, while PyZX reaches 42.6%.VOQC matches Nam et al. on all but two benchmarks; one lower-T result from Nam et al. was later found inequivalent.
Runtime: Runtime is generally competitive with existing tools, although scaling differs and some larger-benchmark cases can be substantially slower.The reported largest benchmark has VOQC at 27.4 seconds versus Qiskit at 31.6 seconds; broader results note that some cases are much worse than Nam et al.
Trusted Code: VOQC’s benchmark results rely partly on trusted OCaml primitives and unverified translations from OpenQASM to SQIR and from Coq to OCaml.The authors explicitly trust consistency between the OCaml implementations and Coq.

7 RELATED WORK

Related work spans verified compilation, translation validation, ZX-calculus optimization, and verified quantum programming. VOQC differs by proving optimizer correctness against SQIR semantics while supporting broad, including full-circuit, transformations.

Verified Quantum Compilation: Prior certified compilers handled reversible circuits or lacked optimization, whereas VOQC targets general quantum programs with verified optimizations.Amy et al. verified compilation from Boolean expressions to reversible circuits, while Rand et al. handled quantum circuits without optimizations.
ZX-Calculus Compilation: PyZX combines ZX-calculus rewriting with translation validation, but its validator is not guaranteed to succeed for every pair of equivalent circuits.ZX-calculus provides a small, well-studied equational theory, but PyZX is not verified in Coq.
Verified Quantum Compilation: Translation-validation approaches can incur compile-time overhead and may fail to identify latent optimizer bugs, while VOQC proves transformations against explicit SQIR input/output semantics.This semantic proof style also supports more flexible optimization expressions.
Verified Quantum Compilation: Smith and Thornton use QMDD equivalence checking, but their optimizations are simpler and the approach scales poorly with increasing qubit count.VOQC’s optimizations are verified for arbitrary dimension.
Verified Quantum Programming: SQIR shares with Qbricks a simplified language and semantics designed to make quantum-program verification more direct.SQIR primarily serves VOQC’s verified optimizations but can also support verified source programming.

8 CONCLUSIONS AND FUTURE WORK

VOQC combines a Coq-embedded SQIR language with proofs that optimization passes preserve program semantics, and its benchmark performance is comparable to state-of-the-art compilers. Future work aims to extend these guarantees into a complete verified compilation stack.

Conclusions: VOQC’s Coq-proved optimizations achieve comparable benchmark performance to leading compilers while reducing total and T-gate counts substantially.Across 28 programs, VOQC reduces gate count by 17.8% and T-gate count by 41.4% on average.
Conclusions: SQIR provides the low-level, proof-friendly semantics that let VOQC verify local equivalences, cancellation, rotation merging, and other transformations.Optimization passes are expressed as Coq functions proved to preserve SQIR program semantics.
Future Work: Future work targets a verified compilation stack from high-level languages through validated parsers and translations into SQIR circuits.The planned stack includes compilation from languages with formal semantics and verified OpenQASM translation.

A ADDITIONAL BENCHMARK RESULTS

Additional benchmarks show that VOQC often matches Nam et al.'s results, while remaining less effective or slower where transformations are missing or implementations differ. The SQIR design also simplifies verification by avoiding typed quantum-data composition issues and supporting direct decomposition and rewriting.

Benchmark results: VOQC matches Nam et al.'s results on QFT, QFT-based adder, and product-formula circuits, but is slightly less effective elsewhere because some transformations are unimplemented.The missing transformations include Toffoli decomposition and floating R_z gates.
Benchmark results: VOQC's runtime is often under one second, but can be four orders of magnitude slower than Nam et al.'s in the worst case.The longer runtimes occur for benchmarks with more than 1000 two-qubit gates, which the authors describe as beyond current quantum hardware.
Benchmark setup: The additional benchmark suite covers arithmetic, Toffoli, QFT, adder, and product-formula circuits spanning tens to hundreds of thousands of gates and up to 4096 qubits.Results are reported in Tables 4–7, with the arithmetic and Toffoli suite alone ranging from 45 to 346,533 gates and 5 to 489 qubits.
Benchmark results: On all 40 product-formula benchmarks, VOQC matches Nam et al.'s results, with H reductions of 62.5%–75% and non-Clifford z-axis-rotation reductions of 0%–28.6%.CNOT reductions range from 0% to 33%, while optimization runtimes range from 0.01s to 406.93s.
Representation and verification: SQIR avoids composition burdens caused by quantum data structures and typed circuits, which can require intermediate identity gadgets and explicit qubit-to-register mappings.SQIR also does not support dynamic lifting, whose semantics depend on the host language.
Representation and verification: SQIR's concrete qubit indices and arbitrary nesting make programs easier to flatten, decompose, and rewrite than QWire circuits with abstract variables and right-associated structure.The paper reports that proving SQIR's inPar correctness took hours, whereas the corresponding QWire proof remained incomplete after many months, although the comparison is not entirely fair.