UMD Team to Receive Distinguished Paper Award at POPL 2021

A team of researchers from the University of Maryland will be recognized with a Distinguished Paper Award at an upcoming international forum on programming languages and programming systems.

Their paper, “A Verified Optimizer for Quantum Circuits,” presents the first fully verified optimizer for quantum circuits—called VOQC—implemented within a formal proof management system.

It will be presented at the 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021), scheduled from January 17–22 in an online-only format due to the ongoing COVID-19 pandemic.

The paper is authored by Michael Hicks, a professor of computer science with appointments in the University of Maryland Institute for Advanced Computer Studies (UMIACS) and the Maryland Cybersecurity Center; Xiaodi Wu, an assistant professor of computer science with an appointment in UMIACS and the Joint Center for Quantum Information and Computer Science (QuICS); Kesha Hietala, the paper’s lead author and a fifth-year computer science doctoral student; Shih-Han Hung, a seventh-year computer science doctoral working in QuICS; and Robert Rand, a former Basili Postdoctoral Fellow at UMD who is now an assistant professor of computer science at the University of Chicago. 

In defining their work, the researchers say that 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. However, both approaches will inevitably have bugs. 

Unfortunately, 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 may be impractical due to the indeterminacy of typical quantum algorithms and the substantial expense involved in executing or simulating them. 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 mathematically prove that the actual code that implements an optimization or algorithm always does what it is intended to do. A famous example of this approach is embodied in the CompCert compiler for C programs, which is written and proved correct using the Coq proof assistant. Follow-on work on automated compiler testing found hundreds of bugs in industrial compilers such as GCC and Clang/LLVM but confirmed that no bugs could be found in CompCert.

To apply CompCert’s approach to the quantum setting, the team developed SQIR, a simple, low-level quantum language deeply embedded in Coq, which gives a semantics to quantum programs that is amenable to proof. They implemented optimizations as functions that transform an input SQIR program into an output SQIR program, using Coq to prove that the input and output SQIR code has the same semantics, i.e., that the optimization will always work correctly. 

When applied to a benchmark suite of 28 circuit programs, the researchers found VOQC performed comparably to state-of-the-art compilers, reducing gate counts on average by 17.8 percent compared to 10.1 percent for IBM’s Qiskit compiler, 10.6 percent for Cambridge Quantum Computing Ltd.’s pytket, and 24.8 percent for a cutting-edge research compiler developed in 2018. Notably, none of these prior compilers were proved correct, and indeed some of them exhibited bugs when run on the benchmark programs.

In the future, the researchers plan to incorporate VOQC into a full-featured verified compilation stack for quantum programs, following the vision of a 2018 Computing Community Consortium report. 

—Story by Melissa Brachfeld