Formal Modeling and Verification of Grover's Algorithm
H. Sun, Z. Shi, S. Chen, G. Wang, X. Li, Y. Guan, Q. Zhang, Z. Shao
TL;DR
This work addresses the challenge of validating quantum algorithms, specifically Grover's search, by providing a fully formal HOL Light model and machine-checked proofs. It formalizes quantum states, unitary evolution, measurement, and the Grover circuit, yielding exact state evolutions and probability expressions such as p_t = sin^2((2t+1)θ) with θ = arcsin(1/sqrt(N)). The authors prove the unitarity of the oracle and diffusion operators, derive the optimal iteration count t ≈ π/(4 arcsin(1/√N))−1/2, and establish a monotonic increase up to the optimum followed by a decrease, all within a rigorous two-dimensional subspace framework. A factorization case study demonstrates the approach's practicality, underscoring the method's potential to provide reliable, scalable guarantees for quantum algorithms and informing the design of more complex quantum systems and protocols.
Abstract
Grover's algorithm relies on the superposition and interference of quantum mechanics, which is more efficient than classical computing in specific tasks such as searching an unsorted database. Due to the high complexity of quantum mechanics, the correctness of quantum algorithms is difficult to guarantee through traditional simulation methods. By contrast, the fundamental concepts and mathematical structure of Grover's algorithm can be formalized into logical expressions and verified by higher-order logical reasoning. In this paper, we formally model and verify Grover's algorithm in the HOL Light theorem prover. We focus on proving key properties such as the unitarity of its oracle and diffusion operators, the monotonicity of the success probability with respect to the number of iterations, and an exact expression for the optimal iteration count. By analyzing a concrete application to integer factorization, we demonstrate the practicality and prospects of our work.