迈向通用量子线路的大规模功能验证

论文信息（正式版本：2019，EPTCS 287，pp. 1–21；预印本：2018）：Matthew Amy。DOI；arXiv:1805.06908

工作

本文提出基于费曼路径积分的量子线路形式化规格与验证框架。量子操作被表示为多项式函数的指数和，便于描述尤其是经典函数的量子实现；带自由变量的重写系统支持线路与规格或参考线路的比较。框架覆盖 Clifford 层级，并在实验中验证了百量子比特和数千 T 门规模的线路与算法。

主要贡献

• 用指数和和多项式函数建立量子线路的结构化功能语义。
• 通过带自由变量的重写系统验证规格、参考线路和线路等价性。
• 给出 Clifford 群线路等价检查的多项式时间判定过程。
• 展示对大规模 Clifford+T 线路和量子算法的自动验证实验。

局限与适用范围

验证效率和可处理规模依赖线路片段、重写系统和规格表示；实验规模不等于所有通用线路都能同样高效验证。该方法证明的是理想线路的功能性质，不自动覆盖噪声、编译器实现、硬件校准或资源最优性。对非适用门集和更复杂控制结构仍需额外扩展。

与其他工作的关系

本文把验证方法与工具中的线路等价检查推进到大规模功能验证，也可与 Clifford+T 量子力学 ZX 演算的完备公理化 对照：前者以指数和和算法验证为中心，后者以图形等式完备性为中心。它与 OpenQASM 和 Quipper 形成从线路表示到验证的链条。

原论文

Matthew Amy, Towards Large-Scale Functional Verification of Universal Quantum Circuits, EPTCS 287, 1–21 (2019), DOI: 10.4204/EPTCS.287.1. arXiv:1805.06908