MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident Verification

Abstract

Different from classical computing, quantum program verification (QPV) is a much more challenging task due to the non-duplicability of quantum states and the quantum collapse after measurement. Prior approaches either rely on algebraic reasoning that shows poor scalability or requires exhaustive assertions with huge complexity. In this paper, we propose MorphQPV, a novel methodology to facilitate confident assertion-based verification. Our key insight is to leverage the isomorphism in quantum programs, which suggests an inherent matching between the program input and its runtime states. We first define an assertion statement that consists of assume-guarantee primitives and tracepoint pragma to label the target quantum state. Then, we can characterize the ground-truth relation between states using isomorphism-based approximation, which can effectively get the program states under various inputs while avoiding repeated executions. Finally, the verification is formulated as a constraint optimization problem with a confidence estimation model to enable rigorous analysis. Experiments suggest that MorphQPV reduces the number of program executions by $107.9\times$ times when verifying the 27-qubit quantum lock algorithm and improves the probability of success by $3.3\times$-$9.9\times$ when debugging 5 benchmarks.