University of Chicago Assistant Professor Rob

Assistant Professor Robert Rand

Image: Asst. Professor Robert Rand
see more

Credit: University of Chicago

Assistant Professor Robert Rand has received a prestigious award for early career development from the Air Force Science Laboratory’s Young Investigator Research Program.

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

The study follows Rand’s motto, “Quantum hardware is uniquely unreliable, so quantum software must be uniquely reliable” and “Quantum computing is non-intuitive. So quantum software should be as intuitive as possible.” ZX-calculus, depicted through flexible red and green “spider” nodes, offers an alternative to more traditional circuit models for expressing how quantum computers can operate and be manipulated through programming, he said.

“I think full picture or graphical quantum calculus is a huge leap beyond the quantum circuit model, because you can see the flow of quantum information through these diagrams,” said Rand. “It’s a very elegant way to express quantum computation, and it’s also a really powerful way to remove the rigidity of quantum circuit models. Only the connectivity matters, not the location of the nodes that reflect quantum properties.”

To this system, Rand brings his experience with formal verification, the process of mathematically proving that an algorithm does what it is intended to do without errors. Quantum computing software developers are already using PyZX, a ZX-calculus optimizer written for the Python programming language, but currently this tool 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 Coq proof helpers that link the category theory of ZX-calculus to fundamental quantum mechanics. . This work includes Caldwell and Lehmann’s VyZX, a proven optimizer that allows programmers to write more reliable, elegant, and efficient quantum software using ZX-calculus, and McGuire and Zweifler’s work on formulating quantum computing in LEAN and Coq. based on.

“We want to strongly connect ZX-calculus to mathematical foundations,” Rand said. “So if the optimizer says that A can be substituted for B, he doesn’t have to take it literally. It is mathematically proven. Then, if you have enough mathematical libraries, you can explore what kind of new rules you can come up with for optimization and simulation.”

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

“Over the years, AFOSR has strongly supported this basic research,” said Rand. “They want a deeper understanding of the mathematics behind quantum computation that will provide insight into what quantum computers can do and how they can be programmed. At the same time, there is a security aspect to this task as software is always the easiest target for exploitation. So one of our common goals is to build secure software where ZX-calculus will play a key role. But a bigger part of the equation is exploring the fundamentals of quantum computing itself through rich mathematical constructs.”

disclaimer: AAAS and EurekAlert! We take no responsibility for the accuracy of press releases posted on EurekAlert! Contributing Organizations or Use of Information Through the EurekAlert System.


Also Read :  HPC-Powered Simulation Helps Engineers See into the Future

Leave a Reply

Your email address will not be published.