Validating Quantum State Preparation Programs (Extended Version)

TL;DR

This paper introduces Pqasm, a Coq-based framework for certifying quantum state preparation programs, enabling effective testing of complex algorithms that are hard to simulate with current quantum simulators.

Contribution

The paper presents Pqasm, a novel high-assurance framework that reduces quantum program correctness to classical verification, facilitating testing of complex quantum state preparation algorithms.

Findings

Successfully tested 5 case studies with Pqasm

Validated correctness of quantum state preparation programs

Demonstrated effectiveness on non-simulatable cases

Abstract

One of the key steps in quantum algorithms is to prepare an initial quantum superposition state with different kinds of features. These so-called state preparation algorithms are essential to the behavior of quantum algorithms, and complicated state preparation algorithms are difficult to develop correctly and effectively. This paper presents Pqasm: a high-assurance framework implemented with the Coq proof assistant, allowing us to certify our Pqasm tool to correctly reflect quantum program behaviors. The key in the framework is to reduce the program correctness assurance of a program containing a quantum superposition state to the program correctness assurance for the program state without superposition. The reduction allows the development of an effective testing framework for testing quantum state preparation algorithm implementations on a classical computer - considered to be a hard problem with no clear solution until this point. We utilize the QuickChick property-based testing framework to test state preparation programs. We evaluated the effectiveness of our approach over 5 case studies implemented using Pqasm; such cases are not even simulatable in the current quantum simulators.