A Verified Optimizer for Quantum Circuits. Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks, November 2019.

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.

[ .pdf ]

  AUTHOR = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks},
  TITLE = {A Verified Optimizer for Quantum Circuits},
  YEAR = {2019},
  SUBMITTED = {yes}

This file has been generated by bibtex2html 1.69