Select Page

PL Perspectives

Perspectives on computing and technology from and for those with an interest in programming languages.

Verifying a Quantum Compiler

by Kesha Hietala and Robert Rand on Jun 2, 2021 | Tags: , , , ,

Verifying a Quantum Compiler

Scalable quantum computing is inching ever closer, but progress can be painfully slow. Even as hardware platforms improve in scale and robustness, they still are far from providing the qubit counts needed to run flagship programs like Shor’s prime factoring algorithm; Shor’s needs millions of qubits, while hardware today can provide under a hundred. But hardware solutions alone won’t give us useful quantum computers in the next decade—software solutions are equally critical: if not for software improvements published recently, we would have said “qubit count in the billions” when describing Shor’s.

In sum, even if things go well on the hardware side, quantum algorithms will be executable only through aggressive optimization. Unfortunately, as these optimizations grow in complexity, their implementations will grow increasingly error-prone. For example: Kissinger and van de Wetering [2020] discovered mistakes in the 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. 

How do we address this challenge? We believe that formal verification holds the answer. Following the lead of CompCert, a formally verified C compiler, we set out to verify a cutting-edge quantum compiler.

This post provides a tour of VOQC, a Verified Optimizer for Quantum Circuits, which is the first piece of our verified compiler toolchain. VOQC is the result of a long, careful effort in proof engineering: It took several tries to get all of the pieces right, to best balance expressiveness and ease of proof. One unlocking element was the development of SQIR, our Simple Quantum Intermediate Representation (IR), which has proved useful both as an IR for our compiler and as a source language for verifying quantum programs. Full details about VOQC and SQIR can be found in our Distinguished Paper at POPL 2021, and a follow-on work to appear at ITP 2021.

Optimizing Quantum Circuits Correctly

Quantum programs are typically represented as circuits:

In these circuits, each horizontal wire represents a qubit and boxes on these wires indicate quantum operations, or gates. The circuit above uses two qubits and applies four gates: an X gate, a controlled-not (CNOT) gate (where the small circle represents the control and the large circle the target), and finally a Hadamard (H) gate and concurrent X gate.

The simplest kind of quantum optimization is peephole optimization, a standard pass in traditional classical (i.e. non-quantum) compilers, which involves replacing one small pattern of quantum gates with another. For example, the circuit above can be optimized using X-propagation, which aims to reduce the number of X gates in a circuit to facilitate later optimization:

This optimization relies on the facts that an X followed by a CNOT is equal to a CNOT followed by two Xs, XH is equivalent to HZ, and two X’s cancel. These equivalences are justified by the gates’ underlying matrix representations: 

A single-qubit gate is represented by a 2×2 matrix and a two-qubit gate is represented by a 4×4 matrix. In general, an n-qubit circuit is represented by a 2^n x 2^n matrix, which makes verifying equivalences over many qubits challenging. To get around this, we treat matrices symbolically, which allows us to verify application of equivalences like those above to circuits with an arbitrary number of qubits, while only needing to multiply 2×2 matrices. For instance, a CNOT between the first and last of n qubits can be represented by the matrix expression E_0 \otimes I_{2^{n-2}} \otimes I_2 + E_1 \otimes I_{2^{n-2}} \otimes X, where I_n is the n by n identity matrix (n is symbolic) and E_0 and E_1 are projectors (see our paper for more detail). In addition, an X gate applied to the first of n qubits can be represented by the matrix expression X \otimes I_{2^{n-1}} , so verifying that “an X followed by a CNOT is equal to a CNOT followed by two Xs” (above) requires us to show that the expression (E_0 \otimes I_{2^{n-2}} \otimes I_2 + E_1 \otimes I_{2^{n-2}} \otimes X) (X \otimes I_{2^{n-1}}) is equivalent to (X \otimes I_{2^{n-2}} \otimes X) (E_0 \otimes I_{2^{n-2}} \otimes I_2 + E_1 \otimes I_{2^{n-2}} \otimes X). We accomplish this by automatically converting both terms to a normal form where + and \otimes  appear on the outside. We can then check  smaller 2×2 equivalences, like E_0 X = X E_1, and symbolic identities like I_{n-2} I_{n-2} = I_{n-2}.

Quantum optimizations are not limited to peephole optimizations. For example, the rotation merging optimization introduced by Nam et al. [2018]  is able to combine Rz gates separated by arbitrary subcircuits of Rz and CNOT gates:

In this case, we verify correctness by focusing on circuits’ actions on basis states: For any bits a, b, c (corresponding to the states of the first, second, and third qubits) the action of the circuit on the quantum state \mid abc \rangle is the same before and after merging the Rz gates. Reasoning about basis states proves to be a powerful technique for a broad set of optimizations. 

A Verified Compiler

VOQC is implemented and proved correct in the Coq proof assistant. While developing SQIR and VOQC, we had to think carefully about how to efficiently describe a matrix whose size is dependent on input parameters (we represent matrices symbolically) and how to easily translate a circuit to its corresponding matrix expression (SQIR uses concrete indices in place of proper variables). You can read more about the design decisions behind SQIR and VOQC in our paper.

Ultimately, we were able to produce a verified compiler that is comparable to, and in many cases outperforms, leading compilers like IBM’s Qiskit and CQC’s tket. The results in our paper (summarized below) show that VOQC almost matches the performance of Nam et al. [2018], which was the inspiration for VOQC, and that the optimizations we have implemented and verified are more effective than what is available in Qiskit and tket and on par with the cutting-edge research compiler PyZX. We report compilation time, reduction in total gate count, and reduction in T gate count (where T is expected to be the bottleneck gate for error-corrected computers).

The Road Ahead

There’s much to do before we can claim complete success. For example, VOQC includes a proved-correct mapper that rearranges circuits to fit on a target architecture, but the mapper is far from the state of the art. Moreover, VOQC doesn’t contain much in the way of high-level optimizations, such as those that optimize the quantum implementation of classical functions like modular exponentiation, sometimes up to a reasonable approximation. Such techniques proved key to Gidney and Ekerå’s implementation of Shor’s algorithm. VOQC also does not support compilation from high-level quantum programming languages (like Microsoft’s Q# or the recent Silq language) to low-level SQIR circuits; developing a semantics for high-level languages amenable to formal verification remains an open problem.

VOQC shows that current state-of-the-art optimizations can be verified and, given the difficulty of validating quantum programs and compilers, ought to be verified. We invite the programming languages community to join us in our effort to build a verified quantum toolchain, putting quantum computing on an ever firmer foundation. 

Getting Involved

Our code is all available on GitHub. We welcome contributions and feedback!

  • Our Coq definitions and proofs are available at github.com/inQWIRE/SQIR. The definitions of the SQIR language are in SQIR/SQIR, the definitions for VOQC are in SQIR/VOQC, and our library of verified algorithms (which we are working to expand!) is in SQIR/examples.
  • Our OCaml library (extracted from the verified Coq code) is available at github.com/inQWIRE/mlvoqc and can be installed with the opam package manager (“opam install voqc”). 
  • For interoperability with existing quantum software toolchains, we provide Python bindings for our OCaml library available at github.com/inQWIRE/pyvoqc.
  • SQIR is built on top of the linear algebra and quantum computing libraries available at github.com/inQWIRE/QWIRE. 

Bio: Kesha Hietala is a PhD Candidate at the University of Maryland (College Park) advised by Mike Hicks. Her research focuses on applying formal verification to the domain of quantum computing. Robert Rand is an Assistant Professor of Computer Science at the University of Chicago. He is a co-developer of the QWIRE and SQIR languages and verification tools.

Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.