A Verified Optimizer for Quantum Circuits
Presented as part of the 2020 HCSS conference.
|
Programming quantum computers will be challenging, at least in the near term. Qubits will be scarce, and gate pipelines will need to be short to prevent decoherence. Fortunately, optimizing compilers can transform a source algorithm to work with fewer resources. Unfortunately, there is a risk that such compilers will operate incorrectly, potentially in a way that is hard to detect; the result could be wrong answers or even security vulnerabilities. In fact, bugs have been found in several state of the art compilers, including IBM's popular Qiskit compiler. |
We present voqc (Figure 1), the rst compiler for quantum circuits fully veried to be correct. Quantum circuits are expressed as programs in a simple, low-level language called sqir, which is deeply embedded in the language of the Coq proof assistant. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of sqir programs. These functions are extracted OCaml by a standard process and then compiled to the nal compiler executable. We evaluate voqc's veried optimizations by running it on a series of benchmarks (written in the standard OpenQASM format). voqc performs comparably to industrial-strength compilers (while being provably bug-free): voqc's optimizations reduce total gate counts on average by 18.4% on a benchmark of 29 circuit programs compared to a 10.7% reduction when using IBM's Qiskit compiler and a 11.2% reduction when using CQC's t|ket> compiler.
VOQC is freely available at https://github.com/inQWIRE/SQIR
Robert Rand is an assistant professor at the University of Chicago with a research specialty in quantum programming. Rand applies techniques from programming languages and formal verification to quantum computation, creating tools for writing, testing, and running reliable software on the quantum computers of today and tomorrow. He co-developed QWIRE, a quantum circuit language, and VOQC, a verified optimizing compiler for quantum programs, and incorporates elements of both in his online textbook, Verified Quantum Computing.