Validating Quantum State Preparation Programs
摘要
One of the key steps in quantum algorithms is to prepare an initial quantum superposition state with distinct features. These state preparation algorithms are essential to the behavior of quantum algorithms, and complicated state preparation algorithms are difficult to program correctly and effectively. We present QSV: a high-assurance framework implemented with the Rocq proof assistant, permitting the development of quantum state preparation programs and validating them to correctly reflect quantum program behaviors. The key is to reduce the program correctness assurance for a program containing a quantum superposition state to that of the program state without superposition. The reduction enables the development of an effective framework for validating quantum state preparation algorithm implementations on a classical computer — a problem considered hard and without a clear solution until now. We utilize the QuickChick property-based testing framework to validate state preparation programs. We evaluated the effectiveness of our approach across 5 case studies implemented using QSV; these cases are not simulatable on current quantum simulators.