Assistant Professor Robert Rand Receives Air Force Young Investigator Grant

Assistant Professor Robert Rand received a grant from the Air Force Office of Scientific Research Young Investigator Research Program, an esteemed award for early career development.

The three-year, $450,000 grant will fund Rand’s work on formal verification of the ZX-calculus, a graphical system for representing quantum programs. Tools based on ZX-calculus can help researchers scale, simulate, and optimize quantum computations. By connecting the system with its mathematical foundations, Rand hopes to enhance its use in reliably writing software for this emerging technology.

The research fits Rand’s motto of “Quantum hardware is uniquely unreliable, so quantum software needs to be uniquely reliable,” as well as a complementary version he describes as “quantum computing is unintuitive; therefore, quantum software needs to be as intuitive as possible.” The ZX-calculus, depicted through flexible red and green “spider” nodes, offers an alternative to the more traditional circuit model for expressing how quantum computers function and can be manipulated through programming, he said.

“I think that the whole pictorial or graphical quantum calculus is just this giant leap above the quantum circuit model, because you can see the flow of quantum information through these diagrams,” Rand said. “It’s an incredibly elegant way of representing quantum computation, and also a really powerful one, that takes away the rigidity of the quantum circuit model. Only connectivity matters, it doesn’t matter where your nodes are, which reflects quantum properties.”

To this system, Rand brings his experience in formal verification, the process of mathematically proving that an algorithm does what it is intended to do without error. Quantum computing software developers already use PyZX, a ZX-calculus optimizer written for the Python programming language, but currently this tool lacks direct proofs of its validity.

Rand and his student collaborators – including Benjamin Caldwell, Adrian Lehmann, Quarrie McGuire, and Jake Zweifler – will add formalized proofs to the LEAN mathematics library and the Coq proof assistant that connect the category theory of ZX-calculus to its underlying quantum mechanics. The work will build upon Caldwell and Lehmann’s VyZX, a verified optimizer that allows programmers to write more reliable, elegant, and efficient quantum software using ZX-calculus, and McGuire and Zweifler’s work on formalizing quantum computing in LEAN and Coq.

“We want to strongly connect ZX-calculus to its mathematical foundations,” Rand said. “So if the optimizer says that you can replace A with B, you don’t have to just take its word for that, it’s mathematically proven. And then we can explore what kind of new rules we can figure out for optimization and simulation if we have a sufficient mathematical library.”

For Rand, the Air Force Office of Scientific Research award is full circle for his interest in quantum computing, originally sparked by a multi-institutional “Semantics, Formal Reasoning, and Tool Support for Quantum Programming” initiative funded by AFOSR in 2015. Rand participated in that collaboration as a PhD student at the University of Pennsylvania, and is honored to continue his work at UChicago CS under a new grant from the agency.

“Over the years, AFOSR has strongly supported this basic research,” Rand said. “They want a deeper understanding of the mathematics behind quantum computation, which will give us insight into what quantum computers are capable of and how to program them. At the same time, there is a security angle to this work, because software is always the easiest target for exploits. So one of our shared goals is building secure software, where I think the ZX-calculus will play a key role. But a bigger part of the equation is exploring the fundamentals of quantum computing itself through its rich mathematical structure.”