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

We present voqc, the first 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. sqir is also sufficiently expressive write source programs and prove them correct. 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 8.4% (and rotation gates on average by 16.1%) on a benchmark of 29 circuit programs compared to a 4.7% reduction (resp, a 8.3% reduction) when using IBM’s Qiskit compiler at optimization level 2.

[ .pdf ]

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

This file has been generated by bibtex2html 1.69