Generating Formally Verified Quantum Fourier Transform Algorithms

While quantum computers provide a promising solution to many problems, designing and implementing quantum programs can be difficult due to the probabilistic and nondeterministic nature of quantum mechanics. Combined with the limited, noisy nature of current and near-future quantum hardware, these implementations may require a battery of program transformations in the form of gate decomposition, optimizations, error correction and more. All of this motivates the need to reason about the correctness and other properties of quantum programs. As a consequence of this difficulty, current research efforts have emerged both to reduce the need for human effort via program generation and quantum circuit optimizers and to ensure correctness of quantum programs and optimizations through the use of simulators, equivalence checkers, automated and computer-assisted formal verification, and more. Mixing program generation and formal verification, this paper presents a formally verified approach for generating implementations of the Quantum Fourier Transform (QFT)—a key component of many larger algorithms such as Shor’s Factorization Algorithm—using the Coq Proof Assistant. This approach leverages existing techniques for generating Fast Fourier Transforms for classical computers used by the SPIRAL system. Unitary matrix formulas expressed using domain specific language represent QFT specifications, algorithm components, and quantum gates. Repeated application of a set of verified rewrite rules encoding matrix factorizations transform a specification to one or many implementable algorithms. These algorithms are compiled to an existing formally verified quantum language.