量子线路的经验证优化器
A Verified Optimizer for Quantum Circuits
Hietala 等人用 Coq 验证 VOQC 优化器，并以 SQIR 的符号矩阵语义证明线路变换正确。
论文信息（2021，POPL/PACMPL）：Kesha Hietala、Robert Rand、Shih-Han Hung、Xiaodi Wu、Michael Hicks。DOI；预印本；论文条目
工作
本文提出 VOQC，一个用 Coq 编写并验证的量子线路优化器。线路在 SQIR（simple quantum intermediate representation）中表示，优化和变换是 Coq 函数，并相对于 SQIR 的复矩阵语义证明正确。通过符号处理矩阵，系统可以为任意数量的量子比特表达和验证优化。
主要贡献
- 提出第一个完整验证的量子线路优化器 VOQC。
- 在 Coq 中深度嵌入 SQIR，并定义线路矩阵语义。
- 证明多类优化和完整线路变换的语义保持性。
- 提供自动化支持，使前沿优化器的变换也能进入验证范围。
局限与适用范围
证明针对 SQIR 语义和已形式化的优化函数；没有被编码和证明的编译阶段、硬件噪声和性能特性仍在信任边界外。符号矩阵语义提供正确性依据，但不自动证明优化后的电路在所有设备上更快或更省资源。
与其他工作的关系
VOQC 将大规模量子线路功能验证的功能等价方向落实到经验证优化器，并可与OpenQASM和Quipper的线路表示对接。它也把验证方法与工具中的定理证明器信任边界具体化为 Coq 内核和 SQIR 语义。
原论文
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks, A Verified Optimizer for Quantum Circuits, Proceedings of the ACM on Programming Languages 5(POPL), Article 37 (2021), DOI: 10.1145/3434318. 预印本