一句话：提出 MorphQPV，利用量子程序同构进行基于断言的可信验证，大幅减少执行并提升调试成功率。
量子程序验证因测量后量子态坍缩且不可复制而远比经典验证困难；现有演绎验证可扩展性差，穷举断言又无法保证所有输入正确。MorphQPV 提出基于断言的置信验证方法，核心是利用量子程序中的同构，即运行时状态间的结构保持关系。它通过 tracepoint pragma 标注待验证量子态，并用 assume-guarantee 原语描述状态间期望关系；再用基于同构的近似刻画真实状态关系，在避免重复执行的同时获得不同输入下的程序状态；最终把验证形式化为带置信估计模型的约束优化问题。实验在 27 比特量子锁算法上减少 107.9 倍执行，并在五个调试基准上把成功率提高 3.3–9.9 倍。
Unlike classical computing, quantum program verification (QPV) is much more challenging due to the non-duplicability of quantum states that collapse after measurement. Prior approaches rely on deductive verification that shows poor scalability. Or they require exhaustive assertions that cannot ensure the program is correct for all inputs. In this paper, we propose MorphQPV, a confident assertion-based verification methodology. Our key insight is to leverage the isomorphism in quantum programs, which implies a structure-preserve relation between the program runtime states. In the assertion statement, we define a tracepoint pragma to label the verified quantum state and an assume-guarantee primitive to specify the expected relation between states. Then, we characterize the ground-truth relation between states using an isomorphism-based approximation, which can effectively obtain 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× when verifying the 27-qubit quantum lock algorithm and improves the probability of success by 3.3×-9.9× when debugging five benchmarks.
@inproceedings{TanXLLJCY24,
title = {MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident Verification},
author = {Siwei Tan and Debin Xiang and Liqiang Lu and Junlin Lu and Qiuping Jiang and Mingshuai Chen and Jianwei Yin},
booktitle = {ASPLOS},
year = {2024},
doi = {10.1145/3620666.3651360}
}