小规模量子混成系统的验证

Quantum verification is an important assisting method for implementation of quantum computers, and is essential to guarantee reliability and effectiveness of quantum systems. In this project, we study the verification problem for Small-scale Quantum Hybrid Systems (SQHS), as most existing quantum computing systems are of this type. We attempt to build the theoretical framework of the problem solving, and to develop corresponding verification techniques. Specifically, we first propose the formal description of SQHS and their dynamical properties, based on the concept of state transition automata and Birkhoff-von Neumann quantum logic. Then we investigate the reachability problem of the systems to obtain the conditions of undecidable results and decidable results, by problems reduction and other mathematical techniques such as descending chain conditions, respectively. Furthermore, we find efficient algorithms to check important temporal properties such as safety and liveness properties, by optimizing and generalizing the reachability checking algorithms. These results will be applied to practical quantum physical systems for experiments and analysis, in order to assess correctness and reliability of the systems, and thus we can implement automatic assisting tools for designing and developing quantum systems.

量子验证是实现量子计算机的重要辅助手段，对于保证量子系统的可靠性和有效性有着至关重要的作用。本项目结合当前量子计算系统的主要特征，重点研究小规模量子混成系统（SQHS）的验证问题，力图建立起解决这一问题的理论框架，并开发出相关验证技术。项目首先基于状态迁移机的概念以及Birkhoff-von Neumann量子逻辑，给出SQHS及其动态性质的形式化描述。接着对系统的可达性问题进行研究，利用问题归约以及降链条件等数学技巧，分别获得不可判定情形与可判定情形的条件。通过对可达性的判定算法进行扩展与优化，进一步得到验证SQHS安全性、活跃性等关键时序性质的有效算法。项目最后将这些结果应用于真实的量子物理系统进行实验和分析，可以得到系统正确性、可靠性等方面的评价，从而能够实现辅助量子系统设计与开发的自动化工具。

实现多量子比特系统上稳定、精确的纠缠操作，一直是量子计算硬件技术的一个主要难点。当前技术生产的量子芯片仅能对几十个量子比特进行符合性能要求的处理，这意味着现阶段可实现的量子系统仅能包含少量的量子比特。本项目针对实际量子系统的特点，通过形式化方法，研究小规模量子混成系统验证的相关理论与技术，包括量子混成系统及其性质的形式化建模，基本的验证方法与技术，关键性数学问题研究，算法的优化、扩展与应用等方面内容。具体来说，项目的研究成果如下：..1、基于量子Hoare逻辑（QHL）的量子程序正确性证明：1）为了证明量子程序的完全正确性，我们提出了基于LRSM的量子程序终止性分析方法；2）在Isabelle/HOL平台上实现了QHL定理证明器；3）通过综合概率程序的Hoare逻辑和QHL，构建了适用于经典-量子混成程序的Hoare逻辑；4）将QHL进行推广，使之适用于平行量子程序的验证，并证明了逻辑的强可靠性。..2、微分动力系统的验证技术研究：1）基于典型的Schrödinger方程形式，针对可解微分动力系统验证问题进行研究，提出了有效的可达性分析算法；2）提出了可靠的基于仿真的验证方法，实现了对延时微分方程的安全性验证；3）针对非自治多项式动力系统提出了其不变量生成方法。..3、针对更为复杂的连续-离散量子混成系统的有效验证方法，包括：1）将近似互模拟的概念扩展到混成系统的验证当中，通过时间-空间两个方向上的离散化，将复杂的混成系统归约为较为简单的离散程序；2）针对多路径多项式程序的验证展开研究，证明了一定条件下终止性问题的可判定性，并实现了适用于小规模程序的高效算法。..本项目不但产生了丰富的理论成果，同时也对部分验证技术实现了相关工具，它们在量子计算机的软硬件开发中具有广泛的应用前景，特别是在量子系统模拟、量子密码协议的安全性保证、量子软件的开发与调试、量子芯片的设计与测试等方面具备非常明确的使用价值。