Verification in Quantum Computing

经典计算机可能需要很长时间才能解决一些问题。有了量子计算机的能力，这些问题可以更快地解决。人们对开发专门的算法非常感兴趣，这些算法可以在量子计算机上运行，用于各种不同的领域，包括化学和机器学习。然而，由于量子物理的性质，量子计算机天生就有噪音，因此容易出错。量子计算机上运行的程序也存在不正确的风险。此外，量子计算机也有可能返回不正确的结果。这意味着程序的不正确结果可能会受到任何或所有这些因素的影响。因此，减少这些设备的硬件和软件中的错误是很重要的。虽然许多公司都在努力减少硬件中的错误，但需要开发可用于验证量子计算机将运行的程序的工具。由于量子计算机可以提供加速，因此调查这些设备是否可以为当前的系统提供验证方法将是有益的。随着系统变得越来越大，验证这些系统是否会进入错误状态变得更加困难。目前的计算方法虽然有效，但随着系统的少量增长，速度会变得慢得多。然而，量子计算机可以提供一种手段来加快目前无法实现的验证过程。这个项目旨在考察量子计算中的这两个验证领域。第一个研究领域是开发一种工具，可以用来验证量子程序的正确性。第二个研究领域是用于验证大系统的量子算法的发展。SMT(满足性模理论)求解器是用于自动验证经典程序的常用工具。SMT解算器的一种变体牺牲了一些具体性来换取速度，从而允许更快地验证程序。该项目的第一部分旨在为量子程序开发这种SMT解算器的变体。这将涉及定义用于复杂算术的SMT解算器的变体，将其实施到软件中，并将软件配置为量子编程语言，以便可以验证该语言中的程序。一旦完成，就可以对一些(可能复杂的)量子程序进行一些案例研究。对于项目的第二部分，验证工具所基于的问题需要重新定义。这是因为量子计算机以一定的概率返回正确的结果。一旦问题的重新定义完成，就可以开发一种算法来解决问题。这个项目的结果将为量子程序的验证和大型经典系统的量子验证提供新的有效工具。通过研究量子计算机的验证，这些设备可能会被用于需要验证的大型复杂系统中，例如发电厂或航天器。

Classical computers can take a long time to solve some problems. With the power of quantum computers, these problems can be solved much faster. There is a large amount of interest in developing specialized algorithms that can run on quantum computers for a variety of different fields, including chemistry and machine learning.However, due to the nature of quantum physics, quantum computers are inherently noisy and so prone to error. There is also a risk of the programs that are run on quantum computers are incorrect. Further, quantum computers have a chance of returning the incorrect result as well. This means that an incorrect result from a program can be influenced by any or all these factors. Therefore, it Is important to reduce the error within the hardware and software of these devices. Whilst various companies are working on reducing error in hardware, there is a need to develop tools that can be used to verify the programs that quantum computers will run.With the speedups that quantum computers can provide though, it would be beneficial to investigate whether these devices can provide a method of verification for current systems. As systems become larger and larger, it becomes harder to verify if these systems can enter an erroneous state or not. Current computing methods, while efficient, become much slower as the system grows by a small amount. However, quantum computers can provide a means of speeding up the verification process that is currently unachievable.This project aims to inspect these two areas of verification within quantum computing. The first area of research is the development of a tool that can be used to verify the correctness of a quantum program. The second area of research is the development of quantum algorithms to be used to verify large systems.An SMT (Satisfiability Modulo Theories) solver is a common tool that is used to automatically verify classical programs. A variation of SMT solvers sacrifices some concreteness for speed, allowing programs to be verified faster. The first part of the project aims to develop this variation of SMT solver for quantum programs. This will involve defining the variation of SMT solver for complex arithmetic, implementing this into software and configuring the software to a quantum programming language so that programs within that language can be verified. Once this is complete, some case studies can be performed on some (potentially complex) quantum programs.For the second part of the project, the problem that verification tools are based on needs to be redefined. This is because quantum computers return the correct result with some probability. Once the redefinition of the problem is completed, then an algorithm can be developed to solve the problem. It will be necessary to explain how the algorithm works, how fast the algorithm can be run and with what probability does the algorithm return the right result.The results of this project will be new efficient tools for the verification of quantum programs and the quantum verification of large classical systems. By studying the verification of quantum computers, these devices can potentially be used within large complex systems that need to be verifiable, such as within power plants or spacecraft.