Validating Quantum State Preparation Programs (Extended Version)

TL;DR

The paper tackles the challenge of validating quantum state preparation programs by proposing QSV, a framework that combines a high-level PQASM language, a property-based testing validator using Rocq/QuickChick, and a certified compiler to SQIR/VOQC. The key idea is to reduce verification of quantum superposition programs to analysis over a deterministic, non-superposed state by identifying Hadamard-initiated superpositions and testing basis-ket transitions. The authors formalize PQASM with a detailed typing discipline, provide a mechanized type-soundness proof, and connect PQASM to SQIR through correctness theorems, enabling scalable, test-driven validation of state-preparation components. Empirical case studies demonstrate that QSV can validate large-scale state preparations—far beyond what current simulators can handle—while offering meaningful bug-detection insights and practical performance. Overall, the work provides a viable path toward reliable, classically verifiable validation of quantum state preparation routines with potential impact on quantum algorithm design and hardware deployment.

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.

Figures (30)

• Figure 1: The QSV Flow
• Figure 2: State Preparation Circuit
• Figure 3: Preparing Superposition of $n$ Basis-kets
• Figure 5: State syntax. $\overline{S}$: a sequence of $S$. $\ket{c}_{\textcolor{spec}{n+ 1}} \equiv \ket{c[0]}_{\textcolor{spec}{1}}\otimes...\otimes\ket{c[n]}_{\textcolor{spec}{1}}$, as $|c|=n\texttt{+} 1$.
• Figure 6: $\textsc{Pqasm}$ syntax.

Theorems & Definitions (13)

• definition 1: Example $\textsc{Pqasm}$ program $P$ to prepare $n$ superposition states in $\overline{q}$
• definition 2: Well-formed state
• theorem 1
• proof
• theorem 2
• proof
• theorem 3
• proof
• definition 3: Well-formed Oqasm state
• theorem 4