A Verified Optimizer for Quantum Circuits

<jats:p>
We present
<jats:sc>voqc</jats:sc>
, the first verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called
<jats:sc>sqir</jats:sc>
, a small quantum intermediate representation, 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
<jats:sc>sqir</jats:sc>
programs.
<jats:sc>sqir</jats:sc>
programs denote complex-valued matrices, as is standard in quantum computation, but we treat matrices symbolically to reason about programs that use an arbitrary number of quantum bits.
<jats:sc>sqir</jats:sc>
’s careful design and our provided automation make it possible to write and verify a broad range of optimizations in
<jats:sc>voqc</jats:sc>
, including full-circuit transformations from cutting-edge optimizers.
</jats:p>
<jats:p />