使用量子 Hoare 逻辑形式化验证量子算法
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic
Liu 等人将量子 Hoare 逻辑、交互式定理证明与量子算法验证结合起来。
论文信息（2019，CAV，LNCS，pp. 187–207）：Junyi Liu、Bohua Zhan、Shuling Wang、Shenggang Ying、Tao Liu、Yangjia Li、Mingsheng Ying、Naijun Zhan。DOI
工作
本文在 Isabelle/HOL 中形式化量子 Hoare 逻辑的程序语法、语义及部分正确性证明系统，并机械化证明该系统的可靠性与完备性。工作将量子断言和算法规格连接到可检查的证明脚本，用于证明形式化模型中的算法性质。
主要贡献
- 在 Isabelle/HOL 中形式化 QHL 的程序语法和语义。
- 机械化证明部分正确性系统的可靠性与完备性。
- 用该框架开展非平凡量子算法的形式化验证。
- 将程序逻辑的元理论与算法规格证明连接起来。
局限与适用范围
结论针对形式化的规格、输入前提与程序模型；参数化证明可以覆盖其量化范围内的所有输入，但不自动覆盖其他实现或硬件。证明脚本构造和循环不变量仍需要人工推理。本文不能与 2016 年使用外部 Python oracle 的原型混为一谈。
与其他工作的关系
本文把量子程序的 Floyd–Hoare 逻辑推进到 Isabelle/HOL 中的元理论和算法验证，并与量子关系 Hoare 逻辑的成对程序推理形成对照。验证方法与工具介绍如何区分规格、证明与实现的保证范围。
原论文
Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan, Formal Verification of Quantum Algorithms Using Quantum Hoare Logic, in CAV 2019, LNCS, 187–207, DOI: 10.1007/978-3-030-25543-5_12.