AI 中文总结
本文针对真实有噪声硬件上的量子程序，开发噪声感知量子霍尔逻辑，实现特定硬件量子程序的有界验证与噪声最优无循环量子程序综合，经IBM Qiskit评估，发现经典概率分支是量子编程最优的必要条件。
AI 中文摘要
尽管大多数量子编程研究采用理想化、无噪声的量子程序语义，本文针对在真实有噪声硬件上执行的量子程序展开研究。我们采用量子硬件厂商发布的误差模型，为量子程序提供依赖于硬件的语义。本研究对噪声感知量子编程进行了全面探究，涵盖从逻辑基础到自动验证与综合的各个方面。我们开发了噪声感知量子霍尔逻辑（quantum Hoare logic），并利用其推导特定硬件上量子程序有界验证的算法方法，以及噪声最优无循环量子程序的自动综合方法。通过这种方式，我们综合了量子算法中常见的依赖硬件的子例程，如奇偶校验、量子态制备和量子态鉴别。我们在IBM Qiskit工具包提供的硬件规格上对方法进行评估，除了为不同噪声模型找到不同的最优子例程外，我们的综合工具还表明，经典概率分支是量子编程达到最优所需的。
英文摘要
While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hardware. We consider the error models published by quantum hardware vendors to give a hardware-dependent semantics to quantum programs. This work presents a comprehensive study of noise-aware quantum programming, ranging from logical foundations to automated verification and synthesis. We develop a noise-aware quantum Hoare logic, and use it to derive algorithmic methods for the bounded verification of quantum programs on specific hardware, and for the automatic synthesis of noise-optimal loop-free quantum programs. In this way, we synthesize hardware-dependent subroutines that commonly occur in quantum algorithms, such as parity checks, quantum state preparation, and quantum state discrimination. We evaluate our method on the hardware specifications provided by the IBM Qiskit toolkit. Besides finding different optimal subroutines for different noise models, our synthesis tool also shows that classical probabilistic branching is needed for optimality in quantum programming.
