arXiv · quant-ph· Yuanjie (Collin), Ren, Zhicheng Zhang, Junyi Liu, Jinzheng Li, Yidi Qi, Mingsheng Ying·· 1 天前
QEDIA：Lean 4中的量子程序验证框架
QEDIA: Quantum Program Verification in Lean
arXiv:2610.17708v1阅读论文 PDF ↗
仅依据论文摘要整理；未读取全文，实验条件、证明与基准细节请核对原文。
作者：Yuanjie (Collin), Ren, Zhicheng Zhang, Junyi Liu, Jinzheng Li, Yidi Qi, Mingsheng Ying
研究任务与主要进展
作者提出QEDIA，用于在Lean 4中验证包含经典变量的量子程序，并在论文摘要中称其底层开放库形式化了量子Hoare逻辑QHL+，覆盖量子力学、程序语法与语义、规范及证明规则，同时论证了偏正确性和全正确性的可靠性。研究还介绍了由人类监督、使用LLM证明代理构建库和程序证明的流程，并验证了量子傅里叶变换、相位估计、repeat-until-success电路和Hamiltonian模拟等程序。
阶段、条件与复现 · 深读核对
- 任务输出与输入访问模型是什么？
- 在什么假设、规模与资源条件下成立？
- 与哪种经典基线比较，是否计入编码与读出？
这些是阅读核对问题；材料未说明的条件保留未知。请结合上方论文版本、资料范围与原文核验。
来源：arXiv · quant-ph · arxiv.org