AI 中文总结
研究为连续变量量子计算提供形式框架，克服技术障碍给出形式语义与首个霍尔逻辑，实现符号最弱前置条件计算器，成功验证算法、证明门分解正确性并计算资源需求。
AI 中文摘要
我们为连续变量量子计算（CQC）提供了一个形式框架。尽管CQC受光子量子硬件支持，但我们不知道连续变量量子程序的形式语义，也不知道用于其验证的一元霍尔逻辑。将离散变量量子计算（DQC）的任何形式框架扩展到CQC存在几个技术障碍。最重要的是，连续变量量子程序作用于无限维希尔伯特空间；其测量结果通常是无界的，期望值由反常积分（或无穷级数）定义，可能不收敛。我们克服了这些挑战，为CQC的通用编程语言给出了形式语义，并提供了首个用于CQC的霍尔逻辑。我们逻辑的断言由规范可观测量上的多项式构建。除了证明相对完备性，我们还基于我们的逻辑实现了一个用于CQC的符号最弱前置条件计算器。我们的工具已成功验证了教科书中的CQC算法，并计算了其物理可实现实现的近似误差，证明了CQC硬件门分解的正确性，以及计算了在连续变量量子程序的经典模拟中达到所需精度的资源需求（即光子数态的数量）。
英文摘要
We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\em unbounded} and have expected values that are defined by an improper integral (or an infinite series), which may not converge. We overcome these challenges to give a formal semantics to a universal programming language for CQC and to provide the first Hoare logic for CQC. The assertions of our logic are built from polynomials over canonical observables. Besides proving relative completeness, we implement a symbolic weakest-precondition calculator for CQC based on our logic. Our tool has successfully verified CQC algorithms from textbooks and calculated their approximation errors for physically realizable implementations, proved the correctness (i.e., equivalence) of gate decompositions for CQC hardware, and computed the resource requirements (i.e., number of photon-number states) for achieving a desired accuracy in the classical simulation of continuous-variable quantum programs.
