02180nas a2200181 4500008004100000245003100041210003100072260001200103520171100115100001901826700001301845700001701858700001701875700001701892700001501909700001901924856005501943 2021 eng d00aExpanding the VOQC Toolkit0 aExpanding the VOQC Toolkit c06/20213 a
voqc [Hietala et al. 2021b] (pronounced “vox”) is a compiler for quantum circuits, in the style of
tools like Qiskit [Aleksandrowicz et al. 2019], tket [Cambridge Quantum Computing Ltd 2019],
Quilc [Rigetti Computing 2019], and Cirq [Developers 2021]. What makes voqc different from these
tools is that it has been formally verified in the Coq proof assistant [Coq Development Team 2019].
voqc source programs are expressed in sqir, a simple quantum intermediate representation, which
has a precise mathematical semantics. We use Gallina, Coq’s programming language, to implement
voqc transformations over sqir programs, and use Coq to prove the source program’s semantics
are preserved. We then extract these Gallina definitions to OCaml, and compile the OCaml code to
a library that can operate on standard-formatted circuits.
voqc, and sqir, were built to be general-purpose. For example, while we originally designed sqir
for use in verified optimizations, we subsequently found sqir could also be suitable for writing, and
proving correct, source programs [Hietala et al. 2021a]. We have continued to develop the voqc
codebase to expand its reach and utility.
In this abstract, we present new extensions to voqc as an illustration of its flexibility. These
include support for calling voqc transformations from Python, added support for new gate sets
and optimizations, and the extension of our notion of correctness to include mapping-preservation,
which allows us to apply optimizations after mapping, reducing the cost introduced by making a
program conform to hardware constraints.
As quantum computing steadily progresses from theory to practice, programmers are faced with a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Simon's algorithm, Grover's algorithm, and quantum phase estimation, a key component of Shor's algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.
1 aHietala, Kesha1 aRand, Robert1 aHung, Shih-Han1 aLi, Liyi1 aHicks, Michael uhttps://arxiv.org/abs/2010.0124001145nas a2200169 4500008004100000245004600041210004400087260001500131490000600146520069700152100001900849700001700868700001900885700001500904700001900919856003700938 2021 eng d00aA Verified Optimizer for Quantum Circuits0 aVerified Optimizer for Quantum Circuits c11/12/20200 v53 aWe 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.0225001259nas a2200145 4500008004100000245005700041210005600098490000800154520083800162100001701000700002101017700001701038700002101055856003701076 2019 eng d00aReQWIRE: Reasoning about Reversible Quantum Circuits0 aReQWIRE Reasoning about Reversible Quantum Circuits0 v2873 aCommon quantum algorithms make heavy use of ancillae: scratch qubits that are initialized at some state and later returned to that state and discarded. Existing quantum circuit languages let programmers assert that a qubit has been returned to the |0> state before it is discarded, allowing for a range of optimizations. However, existing languages do not provide the tools to verify these assertions, introducing a potential source of errors. In this paper we present methods for verifying that ancillae are discarded in the desired state, and use these methods to implement a verified compiler from classical functions to quantum oracles.
1 aRand, Robert1 aPaykin, Jennifer1 aLee, Dong-Ho1 aZdancewic, Steve uhttps://arxiv.org/abs/1901.1011800869nas a2200097 4500008004100000245004500041210004500086520058600131100001700717856003700734 2019 eng d00aVerification Logics for Quantum Programs0 aVerification Logics for Quantum Programs3 aWe survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for formal verification of quantum programs" by Yoshihiko Kakutani; and "Floyd-hoare logic for quantum programs" by Mingsheng Ying. We compare the mathematical foundations of the logics, their underlying languages, and the expressivity of their assertions. We also use the languages to verify the Deutsch-Jozsa Algorithm, and discuss their relative usability in practice.
1 aRand, Robert uhttps://arxiv.org/abs/1904.0430400982nas a2200157 4500008004100000245006700041210006700108260001500175520050800190100001900698700001700717700001900734700001500753700001900768856003700787 2019 eng d00aVerified Optimization in a Quantum Intermediate Representation0 aVerified Optimization in a Quantum Intermediate Representation c04/12/20193 aWe 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