Jan. 22, 2021 — If programmers want to use quantum computers today or in the near future, they’re going to have to get the most out of small, error-prone machines. Fortunately, they have a helpful tool at hand: the compiler. The translators of the programming stack, compilers convert human-readable code to the explicit instructions that computing machinery, classical or quantum, need to operate. Some can even improve that code along the way, making it faster and more reliable.

A new compiler that does all of the above for today’s early quantum computers received one of seven Distinguished Paper awards this month at the 2021 Symposium on Principles of Programming Languages (POPL), one of the top conferences in programming languages research. VOQC, developed by UChicago CS assistant professor Robert Rand and collaborators at the University of Maryland, is the first verified quantum optimizer — a tool for rewriting programs to make them faster while guaranteeing that the program’s meaning is preserved.

The ecosystem of quantum compilers is still small, and new arrivals can produce a large impact in this young field. The ability of VOQC to not only get the most out of the current generation of quantum computers but also prevent errors provides a huge boost to programmers working in an exciting new paradigm.

“We need an optimizing compiler for quantum computing because the hardware is in its infancy. It is incredibly limited, and we need to take advantage of literally every single qubit on the hardware,” Rand said. “Furthermore, these machines are incredibly error-prone, and quantum programs are very difficult to write. So whenever we plug a potential source of error, it’s a big step towards being able to write and execute correct programs and pinpoint the source of programmer or machine errors.”

VOQC, pronounced “vox,” gains its unique abilities through the use of formal verification, methods that convert a computer program or algorithm to a mathematical proof in order to rigorously confirm that its outputs are correct. The project was inspired by CompCert, a verified compiler built for the C language that used the Coq proof assistant to optimize code and prevent bugs. But formal verification could be even more critical for quantum computing, where the underlying physics of the hardware and the possibility of applications that can’t be performed or confirmed on a classical computer create additional uncertainty.

To help VOQC work its magic, Rand and his team developed a quantum intermediate language called SQIR (“squire”). Programmers can write code in a high-level quantum programming language — including QWIRE, a mathematically-grounded language co-developed by Rand — and then convert their program to SQIR, a language closer to the actual instructions for the quantum hardware. With UChicagoCS PhD student Kartik Singhal, Rand is currently working on a verified SQIR translator for IBM’s OpenQASM standard, and hope to build similar tools for popular quantum languages like Q# and Silq.

These projects are part of Rand’s overall goal of building up the quantum programming stack and installing formal verification at every step of the process. While CompCert only appeared after decades of C programming, VOQC arrives in the early days of quantum computing, with the potential to help shape the field as it grows. Given the unreliability of today’s hardware and the inherent complexities of quantum physics and computing, the extra layer of validation will help the field move past its awkward stage as quickly as possible and move on to unprecedented feats of computation.

“In general, what we want to do is set a high standard for quantum programming languages and quantum computing,” Rand said. “We want to apply lessons from decades of classical computing research right at the beginning, and compilers were a major success story case for formal verification.”

The paper, “A Verified Optimizer for Quantum Circuits,” was presented online at POPL 21 on January 20th. In addition to Rand, co-authors include Kesha Hietala, Shih-Han Hung, Xiaodi Wu, and Michael Hicks, all of University of Maryland. For more on the project and the award, see the University of Maryland news article. You can also watch the POPL 21 talk and Q&A here.

---

Source: The University of Chicago Department of Computer Science