A Verified Optimizer for Quantum Circuits
Abstract
We present VOQC, the first fully verified compiler for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, 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. We evaluate VOQC&⋕39;s verified optimizations on a series of benchmarks, and it performs comparably to industrial-strength compilers. VOQC&⋕39;s optimizations reduce total gate counts on average by 17.7% on a benchmark of 29 circuit programs compared to a 10.7% reduction when using IBM&⋕39;s Qiskit compiler.
Publication Details
- Authors
- Publication Type
- Journal Article
- Year of Publication
- 2021
- Journal
- Proceedings of the ACM on Programming Languages
- Volume
- 5
- Date Published
- 01/2021