Proving Quantum Programs Correct

TL;DR

This paper demonstrates the application of mechanized proof techniques to verify the correctness of quantum programs, including key algorithms like Grover's and quantum phase estimation, highlighting progress and challenges in quantum formal verification.

Contribution

It introduces formal verification methods for quantum programs within the SQIR framework, showcasing verified implementations of important quantum algorithms.

Findings

Successfully verified Grover's algorithm and quantum phase estimation.

Highlights both successes and challenges in quantum formal verification.

Motivates further research in theorem proving for quantum computing.

Abstract

As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Grover's algorithm and quantum phase estimation, a key component of Shor's algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.