A Verified Optimizer for Quantum Circuits
arXiv:1912.02250 · doi:10.1145/3434318
Abstract
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.
arXiv commentThis paper supercedes arXiv:1904.06319; version 2 includes additional results and improved formatting; version 3 is the final draft with additional formatting improvements and some restructuring
References in corpus (23)
- Quantum Computing in the NISQ era and beyond
- Quantum cryptography: Public key distribution and coin tossing
- ProjectQ: An Open Source Software Framework for Quantum Computing
- tket : A Retargetable Compiler for NISQ Devices
- Resource-Aware Quantum Programming with General Recursion and Quantum Control
- Interacting Quantum Observables: Categorical Algebra and Diagrammatics
- Polynomial-time T-depth Optimization of Clifford+T circuits via Matroid Partitioning
- Concrete Categorical Model of a Quantum Circuit Description Language with Measurement
- Automated optimization of large quantum circuits with continuous parameters
- Synthesis of Quantum Circuits for Linear Nearest Neighbor Architectures
- Reducing T-count with the ZX-calculus
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- PyZX: Large Scale Automated Diagrammatic Reasoning
- QWIRE Practice: Formal Verification of Quantum Circuits in Coq
- On the CNOT-complexity of CNOT-PHASE circuits
- Verified compilation of space-efficient reversible circuits
- ReQWIRE: Reasoning about Reversible Quantum Circuits
- Optimising Clifford Circuits with Quantomatic
- Next Steps in Quantum Computing: Computer Science's Role
- Formalization of Quantum Protocols using Coq
- Proving Quantum Programs Correct
- CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler
- Sized Types for low-level Quantum Metaprogramming
Cited by in corpus (30)
- Bugs in Quantum Computing Platforms: An Empirical Study
- A Deductive Verification Framework for Circuit-building Quantum Programs
- Synthesizing Quantum-Circuit Optimizers
- NetQASM -- A low-level instruction set architecture for hybrid quantum-classical programs in a quantum internet
- Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
- Reducing 2-QuBit Gate Count for ZX-Calculus based Quantum Circuit Optimization
- Proving Quantum Programs Correct
- Symbolic Execution for Quantum Error Correction Programs
- Efficient Formal Verification of Quantum Error Correcting Programs
- SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation
- On the need for effective tools for debugging quantum programs
- A Case for Synthesis of Recursive Quantum Unitary Programs
- The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation
- Quantum Control Machine: The Limits of Control Flow in Quantum Programming
- Linear and non-linear relational analyses for Quantum Program Optimization
- Near-optimal quantum circuit construction via Cartan decomposition
- Unitary Synthesis of Clifford+T Circuits with Reinforcement Learning
- Formal Methods for Quantum Programs: A Survey
- Verifying Quantum Phase Estimation (QPE) using Prove-It
- Automating Equational Proofs in Dirac Notation
- Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs
- Gleipnir: Toward Practical Error Analysis for Quantum Programs (Extended Version)
- The Quantum Monadology
- Symbolic Verification of Quantum Circuits
- A Practical Quantum Hoare Logic with Classical Variables, I
- Type-Based Verification of Connectivity Constraints in Lattice Surgery
- ViCAR: Visualizing Categories with Automated Rewriting in Coq
- POPQC: Parallel Optimization for Quantum Circuits (Extended Version)
- Hybrid Path-Sums for Hybrid Quantum Programs
- QUANTIFY: A framework for resource analysis and design verification of quantum circuits