Verification in Quantum Computing

量子计算验证

• 批准号: 2442289
• 金额: --
• 依托单位: Newcastle University
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2442289
• 关键词: Verification; Quantum; Computing

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.

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