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.”

Related News

More UChicago CS stories from this research area.
No Name

Argonne scientists use AI to identify new materials for carbon capture

Feb 19, 2024
No Name

New research unites quantum engineering and artificial intelligence

Jan 29, 2024
No Name

Group From UChicago CS To Present Four Papers at Most Prestigious International Quantum Conference

Jan 09, 2024
No Name

UChicago Scientists Make New Discovery Proving Entanglement Is Responsible for Computational Hardness In Quantum Systems

Jul 25, 2023
No Name

Virtual Bakery Game Serves Up Both Cupcakes and Quantum Concepts For K-12 Students

Mar 27, 2023
Students posing at competition
No Name

UChicago Undergrad Team Places Second Overall In Regionals For World’s Largest Programming Competition

Mar 17, 2023
Garcia sitting in a jet engine
No Name

Student Spotlight: Gabi Garcia’s Bridge Between CS and Classics

Jan 30, 2023
Professor Fred Chong advising students
No Name

Prof. Fred Chong Reappointed to National Quantum Initiative Advisory Committee

Dec 13, 2022
No Name

Professor Fred Chong Named IEEE Fellow

Dec 09, 2022
No Name

Associate Professor Diana Franklin Named ACM Distinguished Member

Dec 07, 2022
No Name

UChicago’s Parsl Project Pivots to Sustainability and Community with New Grants

Nov 17, 2022
No Name

Alumnus Pranav Gokhale Named to Crain’s 40 Under 40

Nov 07, 2022
arrow-down-largearrow-left-largearrow-right-large-greyarrow-right-large-yellowarrow-right-largearrow-right-smallbutton-arrowclosedocumentfacebookfacet-arrow-down-whitefacet-arrow-downPage 1CheckedCheckedicon-apple-t5backgroundLayer 1icon-google-t5icon-office365-t5icon-outlook-t5backgroundLayer 1icon-outlookcom-t5backgroundLayer 1icon-yahoo-t5backgroundLayer 1internal-yellowinternalintranetlinkedinlinkoutpauseplaypresentationsearch-bluesearchshareslider-arrow-nextslider-arrow-prevtwittervideoyoutube