并行与分布式量子程序的形式化验证

One of the major difficulties in quantum computer hardware technology is to stably and precisely implement entangled operations on multi-qubit systems. Quantum chips based on current technology can only satisfactorily manipulate dozens of qubits. Thus most experts believe that there will be a long time to implement practical universal quantum computers based on classical architecture. On the other hand, based on current physical technology, a mount of small scale quantum computing nodes can be connected by quantum communication network, and then form a distributed quantum computing cluster. This direction has attracted a lot of attention, and becomes a new topic in the leading research of quantum computation..In this program, we will use formal method to investigate the software system of such quantum computing cluster, including their modelling, semantics, reasoning, analysis and verification. Specifically, the research contains the following topics: (1) Semantics and correctness proof for Parallel quantum programs; (2) Communication, concurrency and synchronization between quantum programs; (3) Model checking on Parallel and distributed quantum programs; (4) Implementation and Case Study.

实现多量子比特系统上稳定、精确的纠缠操作，一直是量子计算硬件技术的一个主要难点。当前技术生产的量子芯片仅能对几十个量子比特进行符合性能要求的处理。因此，专家们普遍预测，基于经典架构的可实用化通用量子计算机依然需要相当长的一段时间才有可能实现。而另一方面，依托于现有物理技术，人们可以通过量子通讯网络，将多个小规模的量子计算结点连接起来，实现一个分布式架构下的量子计算集群。这一方向引起了科学家们的广泛兴趣，是当前量子计算研究前沿的新方向。.本项目将采用形式化方法，对上述量子计算集群上的软件系统进行研究，探讨其建模、语义、推理、分析、验证等问题。具体而言，本研究包括以下内容：（1）并行量子程序的形式语义和正确性证明；（2）量子程序间的通信、并发与时间同步；（3）并行与分布式量子程序的模型检测技术；（4）工具实现与实例研究

基于当前的技术，通过量子通信网络将一系列小规模量子计算结点相连接，构成一个分布式量子计算集群，在物理上是可实现的。这是当前量子计算领域的前沿方向，吸引了大量关注。本项目中，我们通过形式化方法，对这类量子计算集群的软件系统进行研究，主要探索其建模、语义、推理、分析与验证等问题. 具体来说，我们的成果包括：.1、通过在量子while程序语言中加入描述并行程序的结构，并定义其操作与指称语义，我们建立起了并行量子程序理论研究的基础。.2、为构建一个一般的并行量子程序正确性证明方法，我们推广了已有的量子Hoare逻辑（QHL），引入了适用于并行复合的推理规则，使得并行程序的正确性可以由各子程序的正确性推导获得，并进一步证明了该规则的强可靠性。.3、我们专门探讨了分布式量子程序的几个相关问题，包括量子耦合，量子关系Hoare逻辑，以及延时量子控制系统等。.4、我们在Isabelle/HOL平台上实现了QHL定理证明器，从而使得实际量子算法（例如Grover量子搜索算法）的正确性可以通过交互式的定理证明器得到证明，较之以往的手工证明，其可靠性大为提高。.可以看出，这些成果丰富了现有的量子程序理论。我们相信它们会对量子软件的开发与量子计算机的实现起到启发与推动作用。