A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm

• URL: http://arxiv.org/abs/2204.07112v1
• Date: Thu, 14 Apr 2022 17:02:34 GMT
• Title: A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm
• Authors: Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, Xiaodi Wu
• Abstract summary: We present the first formally certified end-to-end implementation of Shor's prime factorization algorithm. By leveraging our framework, one can significantly reduce the effects of human errors.
• Score: 9.349616752756024
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful 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. With such methods, a programmer writes a mathematical specification alongside their program, and semi-automatically proves the program correct with respect to it. The proof's validity is automatically confirmed -- certified -- by a "proof assistant". Formal methods have successfully yielded high-assurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present the first formally certified end-to-end implementation of Shor's prime factorization algorithm, developed as part of a novel 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.

Related papers

• Towards Classical Software Verification using Quantum Computers [0.0]
  We explore the possibility of accelerating the formal verification of classical programs with a quantum computer. Minimal examples of common errors, like out-of-bounds and overflows, are tested with different solvers and tried on a quantum device.
  arXiv  Detail & Related papers  (2024-04-29T08:43:58Z)
• Quantum Annealing for Single Image Super-Resolution [86.69338893753886]
  We propose a quantum computing-based algorithm to solve the single image super-resolution (SISR) problem. The proposed AQC-based algorithm is demonstrated to achieve improved speed-up over a classical analog while maintaining comparable SISR accuracy.
  arXiv  Detail & Related papers  (2023-04-18T11:57:15Z)
• Fault Tolerant Non-Clifford State Preparation for Arbitrary Rotations [3.47670594338385]
  We propose a postselection-based algorithm to efficiently prepare resource states for gate teleportation. Our algorithm achieves fault tolerance, demonstrating the exponential suppression of logical errors with code distance. Our approach presents a promising path to reducing the resource requirement for quantum algorithms on error-corrected and noisy intermediate-scale quantum computers.
  arXiv  Detail & Related papers  (2023-03-30T13:46:52Z)
• Deep Quantum Error Correction [73.54643419792453]
  Quantum error correction codes (QECC) are a key component for realizing the potential of quantum computing. In this work, we efficiently train novel emphend-to-end deep quantum error decoders. The proposed method demonstrates the power of neural decoders for QECC by achieving state-of-the-art accuracy.
  arXiv  Detail & Related papers  (2023-01-27T08:16:26Z)
• Automatic Implementation and Evaluation of Error-Correcting Codes for Quantum Computing: An Open-Source Framework for Quantum Error Correction [2.1801327670218855]
  Real quantum computers are plagued by frequent noise effects that cause errors during computations. Quantum error-correcting codes address this problem by providing means to identify and correct corresponding errors. We propose an open-source framework that automatically applies error-correcting codes for a given application followed by an automatic noise-aware quantum circuit simulation.
  arXiv  Detail & Related papers  (2023-01-13T19:12:22Z)
• Qafny: A Quantum-Program Verifier [39.47005122712576]
  We present Qafny, an automated proof system for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations. We show how Qafny can efficiently verify important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm.
  arXiv  Detail & Related papers  (2022-11-11T18:50:52Z)
• Quantum circuit debugging and sensitivity analysis via local inversions [62.997667081978825]
  We present a technique that pinpoints the sections of a quantum circuit that affect the circuit output the most. We demonstrate the practicality and efficacy of the proposed technique by applying it to example algorithmic circuits implemented on IBM quantum machines.
  arXiv  Detail & Related papers  (2022-04-12T19:39:31Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  We propose circuit-oriented symmetry verification that are capable of verifying the commutativity of quantum circuits without the knowledge of the quantum state. In particular, we propose the Fourier-temporal stabilizer (STS) technique, which generalizes the conventional quantum-domain formalism to circuit-oriented stabilizers.
  arXiv  Detail & Related papers  (2021-12-27T21:15:35Z)
• Hardware-Efficient, Fault-Tolerant Quantum Computation with Rydberg Atoms [55.41644538483948]
  We provide the first complete characterization of sources of error in a neutral-atom quantum computer. We develop a novel and distinctly efficient method to address the most important errors associated with the decay of atomic qubits to states outside of the computational subspace. Our protocols can be implemented in the near-term using state-of-the-art neutral atom platforms with qubits encoded in both alkali and alkaline-earth atoms.
  arXiv  Detail & Related papers  (2021-05-27T23:29:53Z)
• Proving Quantum Programs Correct [3.2513560268591735]
  It verifies the correctness of a range of quantum algorithms including Grover's algorithm and quantum phase estimation. It aims to highlight both the successes and challenges of formal verification in the quantum context.
  arXiv  Detail & Related papers  (2020-10-03T00:55:41Z)
• Electronic structure with direct diagonalization on a D-Wave quantum annealer [62.997667081978825]
  This work implements the general Quantum Annealer Eigensolver (QAE) algorithm to solve the molecular electronic Hamiltonian eigenvalue-eigenvector problem on a D-Wave 2000Q quantum annealer. We demonstrate the use of D-Wave hardware for obtaining ground and electronically excited states across a variety of small molecular systems.
  arXiv  Detail & Related papers  (2020-09-02T22:46:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.