Proving Quantum Programs Correct
- URL: http://arxiv.org/abs/2010.01240v4
- Date: Tue, 13 Jul 2021 18:50:44 GMT
- Title: Proving Quantum Programs Correct
- Authors: Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li and Michael Hicks
- Abstract summary: 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.
- Score: 3.2513560268591735
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: As quantum computing progresses steadily from theory into practice,
programmers will face a common problem: How can they be sure that their code
does what they intend it to do? This paper presents encouraging results in the
application of mechanized proof to the domain of quantum programming in the
context of the SQIR development. It verifies the correctness of a range of a
quantum algorithms including Grover's algorithm and quantum phase estimation, a
key component of Shor's algorithm. In doing so, it aims to highlight both the
successes and challenges of formal verification in the quantum context and
motivate the theorem proving community to target quantum computing as an
application domain.
Related papers
- Quantum Circuit Ansatz: Patterns of Abstraction and Reuse of Quantum Algorithm Design [3.8425905067219492]
The paper presents a categorized catalog of quantum circuit ansatzes.
Each ansatz is described with details such as intent, motivation, applicability, circuit diagram, implementation, example, and see also.
Practical examples are provided to illustrate their application in quantum algorithm design.
arXiv Detail & Related papers (2024-05-08T12:44:37Z) - Quantum Subroutine for Variance Estimation: Algorithmic Design and Applications [80.04533958880862]
Quantum computing sets the foundation for new ways of designing algorithms.
New challenges arise concerning which field quantum speedup can be achieved.
Looking for the design of quantum subroutines that are more efficient than their classical counterpart poses solid pillars to new powerful quantum algorithms.
arXiv Detail & Related papers (2024-02-26T09:32:07Z) - Efficient Quantum Modular Arithmetics for the ISQ Era [0.0]
This study presents an array of quantum circuits, each precision-engineered for modular arithmetic functions.
We provide a theoretical framework and practical implementations in the PennyLane quantum software.
arXiv Detail & Related papers (2023-11-14T21:34:39Z) - QbC: Quantum Correctness by Construction [4.572433350229651]
We propose Quantum Correctness by Construction (QbC), an approach to constructing quantum programs from their specification in a way that ensures correctness.
We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification.
We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way.
arXiv Detail & Related papers (2023-07-28T16:00:57Z) - 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) - 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) - Optimal Stochastic Resource Allocation for Distributed Quantum Computing [50.809738453571015]
We propose a resource allocation scheme for distributed quantum computing (DQC) based on programming to minimize the total deployment cost for quantum resources.
The evaluation demonstrates the effectiveness and ability of the proposed scheme to balance the utilization of quantum computers and on-demand quantum computers.
arXiv Detail & Related papers (2022-09-16T02:37:32Z) - 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) - Formal Verification of Quantum Programs: Theory, Tools and Challenges [0.0]
Survey aims to be a short introduction into the area of formal verification of quantum programs.
This survey examines some of the challenges that the field may face in the future, namely the development of complex quantum algorithms.
arXiv Detail & Related papers (2021-10-04T11:00:48Z) - On exploring the potential of quantum auto-encoder for learning quantum systems [60.909817434753315]
We devise three effective QAE-based learning protocols to address three classically computational hard learning problems.
Our work sheds new light on developing advanced quantum learning algorithms to accomplish hard quantum physics and quantum information processing tasks.
arXiv Detail & Related papers (2021-06-29T14:01:40Z) - An Application of Quantum Annealing Computing to Seismic Inversion [55.41644538483948]
We apply a quantum algorithm to a D-Wave quantum annealer to solve a small scale seismic inversions problem.
The accuracy achieved by the quantum computer is at least as good as that of the classical computer.
arXiv Detail & Related papers (2020-05-06T14:18:44Z)
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.