A Verified Optimizer for Quantum Circuits
KESHA HIETALA, University of Maryland, USA ROBERT RAND, University of Chicago, USA SHIH-HAN HUNG, University of Maryland, USA XIAODI WU, University of Maryland, USA MICHAEL HICKS, University of Maryland, USA
We present voqc, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called sqir, a simple 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 sqir programs. sqir uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. sqir’s careful design and our provided automation make it possible to write and verify a broad range of optimizations in voqc, including full-circuit transformations from cutting-edge optimizers.
CCS Concepts: • Hardware → Quantum computation; Circuit optimization; • Software and its engineering → Formal software verification.
Copyright By PowCoder代写 加微信 powcoder
Additional Key Words and Phrases: Formal Verification, Quantum Computing, Circuit Optimization, Certified Compilation, Programming Languages
ACM Reference Format:
, , Shih- , Xiaodi Wu, and . 2021. A Verified Optimizer for Quantum Circuits. Proc. ACM Program. Lang. 5, POPL, Article 37 (January 2021), 29 pages. https://doi.org/10. 1145/3434318
1 INTRODUCTION
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. Where compilers fall short, programmers can optimize their algorithms by hand.
Of course, both compiler and by-hand optimizations will inevitably have bugs. As evidence of the former, Kissinger and van de Wetering [2020] discovered mistakes in the optimized outputs produced by the circuit optimizer of Nam et al. [2018], and Nam et al. themselves found that the optimization library they compared against (Amy et al. [2013]) sometimes produced incorrect results. Likewise, Amy [2018] discovered an optimizer they had recently developed produced buggy results [Amy et al. 2018]. Making mistakes when optimizing by hand is also to be expected: as put well by Zamdzhiev [2016], quantum computing can be frustratingly unintuitive.
Authors’ addresses: , University of Maryland, USA, , University of Chicago, USA, Shih- , University of Maryland, USA, Xiaodi Wu, University of Maryland, USA, , University of Maryland, USA,
© 2021 Copyright held by the owner/author(s). 2475-1421/2021/1-ART37 https://doi.org/10.1145/3434318
Proc. ACM Program. Lang., Vol. 5, No. POPL, Article 37. Publication date: January 2021.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, Tcohnistawctorthkeisolwicneenrs/eadutuhnodre(sr)a. Creative Commons Attribution 4.0 International License.
37:2 K. Hietala, R. Rand, S. Hung, X. Wu & M. , the very factors that motivate optimizing quantum compilers make it difficult to test their correctness. Comparing runs of a source program to those of its optimized version is often impractical due to the indeterminacy of typical quantum algorithms and the substantial expense involved in executing or simulating them. Indeed, resources may be too scarce, or the qubit connectivity too constrained, to run the program without optimization!
An appealing solution to this problem is to apply rigorous formal methods to prove that an optimization or algorithm always does what it is intended to do. For example, CompCert [Leroy 2009] is a compiler for C programs that is written and proved correct using the Coq proof assis- tant [Coq Development Team 2019]. CompCert includes sophisticated optimizations whose proofs of correctness are verified to be valid by Coq’s type checker.
In this paper, we apply CompCert’s approach to the quantum setting. We present voqc (pro- nounced “vox”), a verified optimizer for quantum circuits. voqc takes as input a quantum program written in a language we call sqir (“squire”). sqir is designed to be a small quantum intermediate representation, but it is suitable for source-level programming too: it is not very different from lan- guages such as Quil [Smith et al. 2016] or OpenQASM [Cross et al. 2017], which describe quantum programs as circuits. sqir is deeply embedded in Coq, similar to how Quil is embedded in Python via PyQuil [Rigetti Computing 2019a], allowing us to write sophisticated quantum programs. voqc applies a series of optimizations to sqir programs, ultimately producing a result that is compatible with a specified quantum architecture. For added convenience, voqc provides translators between sqir and OpenQASM. (Section 2.)
We designed sqir to make it as easy as possible to reason about the semantics of quantum programs, which are significantly different from the semantics of classical programs. For example, while in a classical program one can reason about different variables independently, the phenomenon of quantum entanglement requires us to reason about a global quantum state, typically represented as a large vector or matrix of complex numbers. This means that reasoning about quantum states involves linear algebra, and often trigonometry and probability too. As a result, existing approaches to program proofs in Coq tend not to apply in the quantum setting. Indeed, we first attempted to build voqc using Qwire [Paykin et al. 2017], which is also embedded in Coq and more closely resembles a classical programming language, but found proofs of even simple optimizations to be non-trivial and hardly scalable.
To address these challenges, sqir’s design has several key features (Section 3). First, it uses natural numbers in place of variables so that we can naturally index into the vector or matrix state. Using variables directly (e.g., with higher-order abstract syntax [Pfenning and Elliott 1988], as in Qwire and Quipper [Green et al. 2013]) necessitates a map from variables to indices, which we find confounds proof automation. Second, sqir provides two semantics for quantum programs. We express the semantics of a general program as a function between density matrices, as is standard (e.g., in QPL [Selinger 2004] and Qwire), since density matrices can represent the mixed states that arise when a program applies a measurement operator (Section 5). However, measurement typically occurs at the end of a computation, rather than within it, so we also provide a simpler unitary semantics for (sub-)programs that do not measure their inputs. In this case, a program’s semantics corresponds to a restricted class of square matrices. These matrices are often much easier to work with, especially when employing automation. Other features of sqir’s design, like assigning an ill-typed program the denotation of the zero-matrix, are similarly intended to ease proof. Pleasantly, unitary sqir even turns out to be effective for proving quantum programs correct. This paper presents a proof of correctness of GHZ state preparation [Greenberger et al. 1989]; in concurrent work [Hietala et al. 2020a], we have proved the correctness of implementations of Quantum Phase Estimation (a key component of Shor’s prime factoring algorithm [1994]), Grover’s search algorithm [1996], and Simon’s algorithm [1994].
Proc. ACM Program. Lang., Vol. 5, No. POPL, Article 37. Publication date: January 2021.
A Verified Optimizer for Quantum Circuits 37:3
At the core of voqc is a framework for writing transformations of sqir programs and verifying their correctness. To ensure that the framework is suitably expressive, we have used it to develop verified versions of a variety of optimizations. Many are based on those used in an optimizer developed by Nam et al. [2018], which is the best performing optimizer we know of in terms of total gate reduction (per experiments described below). We abstract these optimizations into a couple of different classes, and provide library functions, lemmas, and automation to simplify their construction and proof. We have also verified a circuit mapping routine that transforms sqir programs to satisfy constraints on how qubits may interact on a specified target architecture. (Section 4.)
We evaluated the quality of the optimizations we verified in voqc, and by extension the quality of our framework, by measuring how well it optimizes a set of benchmark programs, compared to Nam et al. and several other optimizing compilers. The results are encouraging. On a benchmark of 28 circuit programs developed by Amy et al. [2013] we find that voqc reduces total gate count on average by 17.8% compared to 10.1% for IBM’s Qiskit compiler [Aleksandrowicz et al. 2019], 10.6% for CQC’s t∣ket⟩ [Cambridge Quantum Computing Ltd 2019], and 24.8% for the cutting-edge research optimizer by Nam et al. [2018]. On the same benchmarks, voqc reduces T -gate count (an important measure when considering fault tolerance) on average by 41.4% compared to 39.7% by Amy et al. [2013], 41.4% by Nam et al., and 42.6% by the PyZX optimizer. Results on an even larger benchmark suite (detailed in the full version of this paper [Hietala et al. 2020b]) tell the same story. In sum, voqc and sqir are expressive enough to verify a range of useful optimizations, yielding performance competitive with standard compilers. (Section 6.)
voqc is the first fully verified optimizer for general quantum programs. Amy et al. [2017] de- veloped a verified optimizing compiler from source Boolean expressions to reversible circuits and Fagan and Duncan [2018] verified an optimizer for ZX-diagrams representing Clifford cir- cuits; however, neither of these tools handle general quantum programs. In concurrent work, Shi et al. [2019] developed CertiQ, which uses symbolic execution and SMT solving to verify circuit transformations in the Qiskit compiler. CertiQ is limited to verifying correct application of local equivalences and does not provide a way to describe general quantum states (a key feature of sqir), which limits the types of optimizations that it can reason about. This also means that it cannot be used as a tool for verifying general quantum programs. Smith and Thornton [2019] presented a compiler with built-in translation validation via QMDD equivalence checking [Miller and Thornton 2006]. However, QMDDs represent quantum state concretely, which means that the validation time will increase exponentially with the number of qubits in the compiled program. In contrast to these, sqir represents matrices symbolically, which allows us to reason about arbitrary quantum computation and verify interesting, non-local optimizations, independently of the number of qubits in the optimized program. (Section 7.)
Our work on voqc and sqir are steps toward a broader goal of developing a full-scale verified compiler toolchain. Next steps include developing certified transformations from higher-level quantum languages to sqir and implementing optimizations with different objectives, e.g., that aim to reduce the probability that a result is corrupted by quantum noise. All code we reference in this paper can be found online at https://github.com/inQWIRE/SQIR.
2 OVERVIEW
We begin with a brief background on quantum programs, focusing on the challenges related to formal verification. We then provide an overview of voqc and sqir, summarizing how they address these challenges.
Proc. ACM Program. Lang., Vol. 5, No. POPL, Article 37. Publication date: January 2021.
37:4 K. Hietala, R. Rand, S. Hung, X. Wu & M. Hicks
2.1 Preliminaries
Quantum programs operate over quantum states, which consist of one or more quantum bits (a.k.a. qubits).Asinglequbitisrepresentedasavectorofcomplexnumbers⟨α,β⟩suchthat∣α∣2+∣β∣2 =1. The vector ⟨1, 0⟩ represents the state ∣0⟩ while vector ⟨0, 1⟩ represents the state ∣1⟩. A state written ∣ψ ⟩ is called a ket, following Dirac’s notation. We say a qubit is in a superposition of ∣0⟩ and ∣1⟩ when both α and β are non-zero. Just as Schrodinger’s cat is both dead and alive until the box is opened, a qubit is only in superposition until it is measured, at which point the outcome will be 0 with probability ∣α∣2 and 1 with probability ∣β∣2. Measurement is not passive: it has the effect of collapsing the state to match the measured outcome, i.e., either ∣0⟩ or ∣1⟩. As a result, all subsequent measurements return the same answer.
Operators on quantum states are linear mappings. These mappings can be expressed as matrices,
and their application to a state expressed as matrix multiplication. For example, the Hadamard
operator H is expressed as a matrix √1 ( 1 1 ). Applying H to state ∣0⟩ yields state ⟨ √1 , √1 ⟩, also 1 −1
written as ∣+⟩. Many quantum operators are not only linear, they are also unitary—the conjugate transpose (or adjoint) of their matrix is its own inverse. This ensures that multiplying a qubit by the operator preserves the qubit’s sum of norms squared. Since a Hadamard is its own adjoint, it is also its own inverse: hence H ∣+⟩ = ∣0⟩.
A quantum state with n qubits is represented as vector of length 2n . For example, a 2-qubit state is represented as a vector ⟨α,β,γ,δ⟩ where each com- ⎛1 0 ponent corresponds to (the square root of) the probability of measuring ∣00⟩, ⎜0 1 ∣01⟩, ∣10⟩, and ∣11⟩, respectively. Because of the exponential size of the com- ⎜0 0 plex quantum state space, it is not possible to simulate a 100-qubit quantum ⎝0 0 computer using even the most powerful classical computer!
n-qubit operators are represented as 2n × 2n matrices. For example, the
CNOT operator over two qubits is expressed as the matrix shown at the right. It expresses a controlled not operation—if the first qubit (called the control) is ∣0⟩ then both qubits are mapped
to themselves, but if the first qubit is ∣1⟩ then the second qubit (called the target) is negated, e.g., CNOT ∣00⟩ = ∣00⟩ while CNOT ∣10⟩ = ∣11⟩.
n-qubit operators can be used to create entanglement, which is a situation where two qubits
cannot be described independently. For example, while the vector ⟨1, 0, 0, 0⟩ can be written as
⟨1,0⟩⊗⟨1,0⟩where⊗isthetensorproduct,thestate⟨√1 ,0,0, √1 ⟩cannotbesimilarlydecomposed. 22
We say that ⟨√ ,0,0, √ ⟩ is an entangled state. 22
An important non-unitary quantum operator is projection onto a subspace. For example, ∣0⟩⟨0∣ (in matrix notation ( 1 0 )) projects a qubit onto the subspace where that qubit is in the ∣0⟩ state.
Projections are useful for describing quantum states after measurement has been performed. We sometimes use ∣i⟩q⟨i∣ as shorthand for applying the projection ∣i⟩⟨i∣ to qubit q and an identity operation to every other qubit in the state.
2.2 Quantum Circuits
Quantum programs are typically expressed as circuits, as shown in Figure 1(a). In these circuits, each horizontal wire represents a qubit and boxes on these wires indicate quantum operators, or gates. Gates can either be unitary operators (e.g., Hadamard, CNOT) or non-unitary ones (e.g., measurement). In software, quantum circuit programs are often represented using lists of instructions that describe the different gate applications. For example, Figure 1(b) is the Quil [Smith et al. 2016] representation of the circuit in Figure 1(a).
In the QRAM model [Knill 1996] quantum computers are used as co-processors to classical computers. The classical computer generates descriptions of circuits to send to the quantum
Proc. ACM Program. Lang., Vol. 5, No. POPL, Article 37. Publication date: January 2021.
A Verified Optimizer for Quantum Circuits
∣0⟩ H ● ∣0⟩ ● ∣0⟩
(a) Quantum Circuit
H0 CNOT01 CNOT12
def ghz_state(qubits):
program = Program()
program += H(qubits[0])
for q1,q2 in zip(qubits, qubits[1:]):
program += CNOT(q1, q2) return program
(c) PyQuil (arbitrary number of qubits) Fig. 1. Example quantum program: GHZ state preparation
computer and then processes the measurement results. High-level quantum programming languages are designed to follow this model. For example, Figure 1(c) shows a program in PyQuil [Rigetti Computing 2019a], a quantum programming framework embedded in Python. The ghz_state function takes an array qubits and constructs a circuit that prepares the Greenberger-Horne- Zeilinger (GHZ) state [Greenberger et al. 1989], which is an n-qubit entangled quantum state of the form
∣GHZn ⟩ = √1 (∣0⟩⊗n + ∣1⟩⊗n ). 2
Calling ghz_state([0,1,2]) returns the Quil program in Figure 1(b), which produces the quantum state√1 (∣000⟩+∣111⟩).Thehigh-levellanguagemayprovidefacilitiestooptimizeconstructed
circuits, e.g., to reduce gate count, circuit depth, and qubit usage. It may also perform transforma- tions to account for hardware-specific details like the number of qubits, available set of gates, or connectivity between physical qubits.
What if we want to formally verify that ghz_state, when passed an array of indices [0, …,n − 1], returns a circuit that produces the quantum state ∣GHZn ⟩? What steps are necessary?
First, we need a way to formally define quantum states as matrices of complex numbers. Indeed, we need a way to define indexed families of states—∣GHZn ⟩ is a function from an index n to a quantum state. Second, we need a formal language in which to express quantum programs; to this language we must ascribe a mathematical semantics in terms of quantum states. A program like ghz_state is a function from an index (a list of length n) to a circuit (of size n), and this circuit’s denotation is its equivalent (unitary) matrix (of size 2n ). Finally, we need a way to mechanically reason that, for arbitrary n, the semantics of ghz_state([0,1,…,n − 1]) applied to the zero state (∣0⟩⊗n ) is equal to the state ∣GHZn ⟩.
We designed sqir, a small quantum intermediate representation, to do all of these things. sqir is a simple circuit-oriented language deeply embedded in the Coq proof assistant in a manner similar to how Quil is embedded in Python via PyQuil. We use sqir’s host language, Coq, to define the syntax and semantics of sqir programs and to express properties about quantum states. We developed a library of lemmas and tactic-based automation to assist in writing proofs about quantum programs; such proofs make heavy use of complex numbers and linear algebra. These proofs are aided by isolating sqir’s unitary core from primitives for measurement, which require consideration of probability distributions of outcomes (represented as density matrices); this means that (sub- )programs that lack measurement can have simpler proofs. Either way, in sqir we perform reasoning symbolically. For example, we can prove that every circuit generated by the sqir-equivalent of ghz_state produces the expected state ∣GHZn ⟩ when applied to input lists of length n, for any n.
Proc. ACM Program. Lang., Vol. 5, No. POPL, Article 37. Publication date: January 2021.
2.3 sqir: A Small Quantum Intermediate Representation Supporting Verification
K. Hietala, R. Rand, S. Hung, X. Wu & M. OQC
source circuit
target circuit
source program
VOQC optimizers, circuit mapper
VOQC optimizers, circuit mapper
source SQIR circuit
target SQIR circuit
Fig.2. Thevoqcarchitecture.InputcircuitscanbedescribedinOpenQASM,OCaml,orCoq
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com