AutoQ 2.0：从量子电路验证到量子程序验证（技术报告）
计算机科学中的逻辑
2026-05-08 v2 形式语言与自动机理论
摘要
我们提出了一个名为 AutoQ 2.0 的量子程序验证器。量子程序通过经典控制流结构扩展了量子电路（AutoQ 1.0 的领域），使用户能够以形式化且精确的方式描述高级量子算法。这种扩展极不平凡，因为我们需要同时应对理论挑战（如测量处理、归一化问题，以及将带循环的经典程序验证提升技术推广到量子领域）和工程问题（如扩展输入格式以支持指定循环不变量）。我们已成功使用 AutoQ 2.0 验证了两类无法仅用量子电路表达的高级量子程序：重复直到成功（RUS）算法和基于弱测量的 Grover 搜索算法版本。AutoQ 2.0 能高效验证所有基准：所有 RUS 算法瞬间完成验证，而对于基于弱测量的 Grover 搜索，我们能在约 20 分钟内处理 100 量子比特的情况。
引用
@article{arxiv.2411.09121,
title = {AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)},
author = {Yu-Fang Chen and Kai-Min Chung and Min-Hsiu Hsieh and Wei-Jia Huang and Ondřej Lengál and Jyun-Ao Lin and Wei-Lun Tsai},
journal= {arXiv preprint arXiv:2411.09121},
year = {2026}
}
备注
regular tool paper submitted to TACAS 2025