Formally Verifying Graphical Quantum Calculi
Abstract
The ZX-calculus is a powerful new approach to representing quantum computation. Where quantum computing is usually done via the quantum circuit model, which depicts a group of quantum bits traveling along straight wires and through a variety of quantum gates, a ZX-calculus diagram is a simple graph consisting of red and green nodes. Despite its simplicity, a ZX diagram can represent arbitrary quantum computation. In fact, its very simplicity allowed practitioners to develop cutting-edge tools for the ZX-calculus, including a fast quantum simulator and a highly efficient circuit optimizer. Unfortunately, while the ZX-calculus has a mathematically rich foundation and useful tools, these tools are not tightly connected to the theory. As a result, they can fail in the same ways that ordinary software fails, which is particularly damaging in the already error-prone domain of quantum computing. We propose putting both the ZX-calculus and its tools on a firm footing through the use of proof assistants that allow you to prove the correctness of both mathematical theorems and software. Using these tools, we will express and prove correct the mathematical foundations underlying the ZX-calculus, particularly from the discipline of category theory. We will then mechanize the ZX-calculus and show that the graph transformations that characterize it are sound with respect to their quantum mechanical interpretations. Finally, we will use our construction of the ZX-calculus to develop an optimizer that is proven correct and guaranteed not to introduce bugs. This optimizer will be broadly useful to practitioners seeking to reduce the size of their quantum programs. The underlying development will be a significant contribution to the grand project of mechanizing mathematics and deliver a fully verified version of the ZX-calculus for quantum information scientists to use and build upon in their research.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 06, 2024
- Source ID
- FA95502310361
Entities
People
- Robert Rand
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Chicago