连续变量量子程序的形式化验证

我们为连续变量量子计算(CQC)提供了一个形式化框架。虽然CQC得到光子量子硬件的支持，但我们不知道有连续变量量子程序的形式语义，也没有用于其验证的一元Hoare逻辑。将任何可用于离散变量量子计算(DQC)的形式框架扩展到CQC存在几个技术障碍。最重要的是，连续变量量子程序作用于无限维希尔伯特空间；它们的测量结果通常是无界的，其期望值由可能不收敛的反常积分（或无穷级数）定义。我们克服了这些挑战，为CQC的通用编程语言提供了形式语义，并提供了第一个CQC的Hoare逻辑。我们逻辑的断言由规范可观测量上的多项式构成。除了证明相对完备性，我们还基于我们的逻辑为CQC实现了一个符号最弱前条件计算器。我们的工具已成功验证了教科书中的CQC算法，并计算了它们在物理可实现实现中的近似误差，证明了CQC硬件门分解的正确性（即等价性），并计算了在连续变量量子程序的经典模拟中达到所需精度所需的资源（即光子数态的数量）。