EAGER: Formal Verification For Quantum Software: 1,000 Qubits and Beyond

Quantum computing offers the potential for exponential speedup in solving complex problems, such as optimization, cryptography, and simulation, by leveraging quantum superposition and entanglement to process vast amounts of information simultaneously. Many applications of quantum computing are safety-critical and security-critical, i.e., errors or security breaches in quantum software can lead to catastrophic failures and/or harm of human life. The goal of this project is to develop scalable formal verification methods for quantum software. Formal verification provides a rigorous mathematical framework to prove that quantum programs behave as intended under all possible conditions, which is especially important given the difficulty of detecting and correcting quantum errors through traditional testing methods. The significance of this project lies in developing scalable formal verification methods for quantum software to ensure the correctness and reliability of safety-critical and security-critical quantum applications, where errors or vulnerabilities could lead to catastrophic outcomes. Success will be extremely beneficial as it will be an important step towards widespread utility of quantum computers. The project will also benefit students in North Dakota, a geographically underrepresented area in computing and quantum information science and engineering.

The significant challenge in verifying quantum software is that quantum operations are modeled in Hilbert space (complex vector space), and existing verification tools are not very scalable for Hilbert space. Our central hypothesis is that abstractions can be used to reduce the verification problem from Hilbert space to bit-vector space, for which verification tools are orders-of-magnitude more efficient and scalable. This hypothesis is based on preliminary investigation with two abstractions: (1) rotational abstraction that exploits the rotational behavior of quantum operations; and (2) superposition abstraction that abstracts the superposition behavior of quantum programs. The goals of the project are to generalize rotational and superposition abstraction, develop a unified abstraction framework that incorporates both, develop algorithms and tooling to apply the abstractions automatically, and study the applicability of the abstractions to implementations of many quantum algorithms that have potential for real-world applications.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

Award Number: 2513276
Principal Investigator: Sudarshan Srinivasan
Funds Obligated: $119,159
State: ND