量子程序的关系证明

论文信息（正式卷：2020，POPL/PACMPL 4；在线发表：2019 年 12 月）：Gilles Barthe、Justin Hsu、Mingsheng Ying、Nengkun Yu、Li Zhou。DOI；arXiv:1901.05184

工作

本文提出量子程序的关系逻辑，语义基础是概率耦合的量子对应物。关系证明关注两次运行或两段程序之间的性质，而不是只验证单个程序的后置条件。论文用该逻辑分析量子 Bernoulli factory 的均匀性、含噪量子传送、量子一次一密和量子游走等例子。

主要贡献

• 为量子程序建立基于量子耦合的关系证明逻辑。
• 表达程序等价、可靠性和密码安全等跨程序性质。
• 验证量子 Bernoulli factory 的样本均匀性、比特/相位翻转噪声下传态的可靠性、量子一次一密安全性及量子游走等价性。
• 将概率关系证明的思想推广到量子态与量子过程。

局限与适用范围

关系证明依赖耦合构造、关系谓词和量子程序语义；示例成功不等于任意关系性质都能自动证明。噪声模型、测量结果和开放系统边界需要显式建模，逻辑本身也不替代硬件认证或资源性能分析。

与其他工作的关系

它与量子关系 Hoare 逻辑同属关系验证路线，可与量子程序的 Floyd–Hoare 逻辑的单程序断言进行对比。与量子进程的互模拟相比，本文强调耦合与关系谓词，而互模拟强调进程行为等价。

原论文

Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou, Relational Proofs for Quantum Programs, Proceedings of the ACM on Programming Languages 4(POPL), Article 21 (2020), DOI: 10.1145/3371089. arXiv:1901.05184