A formally certified end-to-end implementation of Shor’s factorization algorithm

What is it about?

Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but it is useful only if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors—“bugs.” Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. To demonstrate its feasibility, we present a formally certified end-to-end implementation of Shor’s prime factorization algorithm, developed as part of a framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way.

Featured Image

Photo by Michael Dziedzic on Unsplash

Photo by Michael Dziedzic on Unsplash

Why is it important?

While hardware errors have garnered significant attention as the major obstacle to quantum computing, the error due to human factors in the implementation is less recognized. This paper identifies human programming errors as another important source of errors, whereas most existing techniques from the classical domain fail to transfer at scale to quantum programming. The adaptation of formal methods to quantum programming is proposed as a solution that circumvents quantum unique challenges and leads to the high-assurance implementation of large-scale quantum applications in a principle way. As a demonstration of the feasibility, this paper presents a formally certified end-to-end implementation of Shor’s prime factorization algorithm due to its complexity and importance.

Perspectives