Verification in 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.