01742nas a2200169 4500008004100000245004400041210004400085260001500129520128400144100001301428700002301441700001901464700001801483700001501501700001901516856003701535 2021 eng d00aVerified Compilation of Quantum Oracles0 aVerified Compilation of Quantum Oracles c12/13/20213 a

Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the largest components of a quantum algorithm. To ease the construction of efficient, correct oracle functions, this paper presents VQO, a high-assurance framework implemented with the Coq proof assistant. The core of VQO is OQASM, the oracle quantum assembly language. OQASM operations move qubits among three different bases via the Quantum Fourier Transform and Hadamard operations, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM's design enabled us to prove correct VQO's compilers -- from a simple imperative language called OQIMP to OQASM, and from OQASM to SQIR, a general-purpose quantum assembly language -- and allowed us to efficiently test properties of OQASM programs using the QuickChick property-based testing framework. We have used VQO to implement oracles used in Shor's and Grover's algorithms, as well as several common arithmetic operators. VQO's oracles have performance comparable to those produced by Quipper, a state-of-the-art but unverified quantum programming platform.

1 aLi, Liyi1 aVoichick, Finnegan1 aHietala, Kesha1 aPeng, Yuxiang1 aWu, Xiaodi1 aHicks, Michael uhttps://arxiv.org/abs/2112.0670001145nas a2200169 4500008004100000245004600041210004400087260001500131490000600146520069700152100001900849700001700868700001900885700001500904700001900919856003700938 2021 eng d00aA Verified Optimizer for Quantum Circuits0 aVerified Optimizer for Quantum Circuits c11/12/20200 v53 a

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.

1 aHietala, Kesha1 aRand, Robert1 aHung, Shih-Han1 aWu, Xiaodi1 aHicks, Michael uhttps://arxiv.org/abs/1912.0225000982nas a2200157 4500008004100000245006700041210006700108260001500175520050800190100001900698700001700717700001900734700001500753700001900768856003700787 2019 eng d00aVerified Optimization in a Quantum Intermediate Representation0 aVerified Optimization in a Quantum Intermediate Representation c04/12/20193 a

We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum assembly' languages and simplifying the verification process. We demonstrate the power of sqire as an intermediate representation of quantum programs by verifying a number of useful optimizations, and we demonstrate sqire's use as a tool for general verification by proving several quantum programs correct.

1 aHietala, Kesha1 aRand, Robert1 aHung, Shih-Han1 aWu, Xiaodi1 aHicks, Michael uhttps://arxiv.org/abs/1904.06319