Image: Asst. Professor Robert Rand
outlook more
Photo credit: University of Chicago
Assistant Professor Robert Rand received a grant from the Air Force Office of Scientific Research Young Investigator Research Program, a prestigious early career development award.
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 the ZX calculus can help researchers scale, simulate and optimize quantum calculations. By connecting the system to its mathematical foundations, Rand hopes to improve its use in reliably writing software for this emerging technology.
The research fits Rand’s motto “Quantum hardware is uniquely unreliable, so quantum software must be uniquely reliable” and a complementary version he describes as “Quantum computing is counterintuitive; Therefore, quantum software must be as intuitive as possible.” The ZX calculus, represented by flexible red and green “spider” nodes, offers an alternative to the more traditional circuit model for expressing how quantum computers work and can be manipulated through programming, said he.
“I think all pictorial or graphical quantum computing is just this giant leap beyond 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 computing, and also a really powerful one that breaks the rigidity of the quantum circuit model. Only connectivity matters, it doesn’t matter where your nodes are, reflecting quantum properties.”
To this system, Rand brings his experience in formal verification, the process of mathematically proving that an algorithm does what it intends to do without errors. Quantum computing software developers are already using PyZX, a ZX calculus optimizer written for the Python programming language, but this tool currently lacks direct evidence 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 math library and the Coq proof assistant that connect the category theory of ZX calculus to the underlying quantum mechanics. The work will build on Caldwell and Lehmann’s VyZX, a verified optimizer that enables programmers to write more reliable, elegant, and efficient quantum software using ZX calculus, and work by McGuire and Zweifler on formalizing quantum computing in LEAN and Coq.
“We want to strongly connect the ZX calculus to its mathematical foundations,” Rand said. “So if the optimizer says you can replace A with B, you don’t have to just believe it, 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 comes full circle for his interest in quantum computing, originally sparked by a 2015 AFOSR-funded multi-agency Semantics, Formal Reasoning, and Tool Support for Quantum Programming initiative. Rand participated in this collaboration as a graduate student at the University of Pennsylvania and is honored to continue his work at UChicago CS with a new grant from the agency.
“Over the years, AFOSR has been a strong supporter of this basic research,” Rand said. “They want a deeper understanding of the mathematics behind quantum computers, which will give us a glimpse of what quantum computers are capable of and how to program them. At the same time, this work also has a security aspect, because software is always the easiest target for exploits. So one of our common goals is to develop secure software, where I think the ZX calculus will play a key role. But a larger part of the equation is exploring the fundamentals of quantum computing itself through its rich mathematical structure.”
Disclaimer: AAAS and EurekAlert! are not responsible for the accuracy of the press releases published on EurekAlert! by contributing institutions or for the use of information about the EurekAlert system.
