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.
Garcia sitting in a jet engine
UChicago CS News

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

Jan 30, 2023
Professor Fred Chong advising students
UChicago CS News

Prof. Fred Chong Reappointed to National Quantum Initiative Advisory Committee

Dec 13, 2022
UChicago CS News

Professor Fred Chong Named IEEE Fellow

Dec 09, 2022
UChicago CS News

Associate Professor Diana Franklin Named ACM Distinguished Member

Dec 07, 2022
UChicago CS News

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

Nov 17, 2022
In the News

Alumnus Pranav Gokhale Named to Crain’s 40 Under 40

Nov 07, 2022
UChicago CS News

Prof. Diana Franklin Discusses Quantum Computing Education on Entangled Things Podcast

Nov 03, 2022
UChicago CS News

Civic Tech Pioneer James Turk Joins UChicago CS to Teach in MPCS, CAPP

Oct 06, 2022
UChicago CS News

UChicago/Argonne Computer Scientist Ian Foster Receives ACM/IEEE Ken Kennedy Award

Sep 07, 2022
UChicago CS News

High School Students in College Prep Program Visit UChicago CS

Aug 23, 2022
UChicago CS News

UChicago Hosts NSF Workshop on Frontiers of Quantum Advantage

Aug 15, 2022
In the News

Bill Fefferman Comments on New Standards for Quantum-Proof Cryptography

Jul 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