A Verified Optimizer for Quantum Circuits
A Verified Optimizer for Quantum Circuits
Hietala and colleagues verify the VOQC optimizer in Coq using SQIR's symbolic matrix semantics.
Paper information (2021, POPL/PACMPL) — Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. DOI; preprint; paper entry
Work
The paper presents VOQC, a quantum-circuit optimizer written and verified in Coq. Circuits are represented in SQIR (simple quantum intermediate representation); optimizations and transformations are Coq functions whose correctness is proved against SQIR's complex-matrix semantics. Symbolic matrices let the system reason about circuits with an arbitrary number of qubits.
Contributions
- A fully verified quantum-circuit optimizer, VOQC.
- A deeply embedded SQIR language and matrix semantics in Coq.
- Semantic-preservation proofs for many optimizations and full-circuit transformations.
- Automation that brings transformations from state-of-the-art optimizers into the verified framework.
Limits
The proofs cover SQIR semantics and optimization functions that have been encoded and verified; compiler stages outside that model, hardware noise, and performance remain outside the trust boundary. Symbolic matrix semantics supports correctness reasoning but does not prove that an optimized circuit is faster or cheaper on every device.
Connections
VOQC turns the functional-equivalence direction of Towards Large-Scale Functional Verification of Universal Quantum Circuits into a verified optimizer, and can connect to circuit representations such as OpenQASM and Quipper. It also makes the theorem-prover trust boundary in Verification Methods and Tools concrete through Coq's kernel and SQIR semantics.
Original paper
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks, A Verified Optimizer for Quantum Circuits, Proceedings of the ACM on Programming Languages 5(POPL), Article 37 (2021), DOI: 10.1145/3434318. Preprint