Projection-based runtime assertions for testing and debugging Quantum programs

TLDR

The authors introduce Proq, a runtime assertion framework that uses projection‑based predicates to test and debug quantum programs on quantum hardware, and propose a sound local‑projection simplification for easier implementation. Proq represents assertions as projections in Birkhoff‑von Neumann quantum logic, enabling verification with few projective measurements and adapting the predicates to measurement‑restricted devices through transformation techniques. Theoretical analysis shows that projection‑based assertions can locate bugs or statistically guarantee semantic fidelity, and empirical evaluation on the Harrow‑Hassidim‑Lloyd and Shor algorithms demonstrates Proq’s effectiveness and efficiency compared to existing methods.

Abstract

In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measurements rather than a large number of repeated executions. On the theory side, we rigorously prove that checking projection-based assertions can help locate bugs or statistically assure that the semantic function of the tested program is close to what we expect, for both exact and approximate quantum programs. On the practice side, we consider hardware constraints and introduce several techniques to transform the assertions, making them directly executable on the measurement-restricted quantum computers. We also propose to achieve simplified assertion implementation using local projection technique with soundness guaranteed. We compare Proq with existing quantum program assertions and demonstrate the effectiveness and efficiency of Proq by its applications to assert two sophisticated quantum algorithms, the Harrow-Hassidim-Lloyd algorithm and Shor’s algorithm.