| Title | A Verified Optimizer for Quantum Circuits |
| Publication Type | Journal Article |
| Year of Publication | 2021 |
| Authors | Hietala, K, Rand, R, Hung, S-H, Wu, X, Hicks, M |
| Journal | Proceedings of the ACM on Programming Languages |
| Volume | 5 |
| Issue | POPL |
| Date Published | 11/12/2020 |
| 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's verified optimizations on a series of benchmarks, and it performs comparably to industrial-strength compilers. VOQC'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's Qiskit compiler. |
| URL | https://arxiv.org/abs/1912.02250 |
| DOI | 10.1145/3434318 |
