A formally certified end-to-end implementation of Shor’s factorization algorithm
AI Breakdown
Get a structured breakdown of this paper — what it's about, the core idea, and key takeaways for the field.
Abstract
Significance 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.