Qafny: A Quantum-Program Verifier
- URL: http://arxiv.org/abs/2211.06411v5
- Date: Mon, 8 Jul 2024 16:28:26 GMT
- Title: Qafny: A Quantum-Program Verifier
- Authors: Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu,
- Abstract summary: 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.
- Score: 39.47005122712576
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny's automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm.
Related papers
- Verification of Recursively Defined Quantum Circuits [7.042810171786408]
We present a proof system for formal verification of the correctness of quantum circuits.
A series of application examples are given, including (multi-qubit) controlled gates, a quantum circuit generating (multi-qubit) GHZ.
arXiv Detail & Related papers (2024-04-09T01:35:13Z) - Local Reasoning about Probabilistic Behaviour for Classical-Quantum
Programs [3.871660145364189]
We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour.
We show that the proof rules in the logic are sound with respect to a denotational semantics.
We formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms.
arXiv Detail & Related papers (2023-08-09T07:23:22Z) - 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) - quAssert: Automatic Generation of Quantum Assertions [5.263910852465185]
We propose automated generation and placement of quantum assertions based on static analysis and random sampling of quantum circuits.
We uncover special properties of a quantum circuit, such as purely classical states, superposition states, and entangled states using statistical methods.
We demonstrate the effectiveness of the generated assertions in error detection using a suite of quantum benchmarks.
arXiv Detail & Related papers (2023-03-02T18:49:14Z) - Verification of Nondeterministic Quantum Programs [1.9302781323430196]
Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations.
Nondeterminism has also been introduced in quantum programming, and the termination of nondeterministic quantum programs has been extensively analysed.
arXiv Detail & Related papers (2023-02-15T22:37:23Z) - Delegated variational quantum algorithms based on quantum homomorphic
encryption [69.50567607858659]
Variational quantum algorithms (VQAs) are one of the most promising candidates for achieving quantum advantages on quantum devices.
The private data of clients may be leaked to quantum servers in such a quantum cloud model.
A novel quantum homomorphic encryption (QHE) scheme is constructed for quantum servers to calculate encrypted data.
arXiv Detail & Related papers (2023-01-25T07:00:13Z) - 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) - Efficient criteria of quantumness for a large system of qubits [58.720142291102135]
We discuss the dimensionless combinations of basic parameters of large, partially quantum coherent systems.
Based on analytical and numerical calculations, we suggest one such number for a system of qubits undergoing adiabatic evolution.
arXiv Detail & Related papers (2021-08-30T23:50:05Z) - Depth-efficient proofs of quantumness [77.34726150561087]
A proof of quantumness is a type of challenge-response protocol in which a classical verifier can efficiently certify quantum advantage of an untrusted prover.
In this paper, we give two proof of quantumness constructions in which the prover need only perform constant-depth quantum circuits.
arXiv Detail & Related papers (2021-07-05T17:45:41Z) - Facial Expression Recognition on a Quantum Computer [68.8204255655161]
We show a possible solution to facial expression recognition using a quantum machine learning approach.
We define a quantum circuit that manipulates the graphs adjacency matrices encoded into the amplitudes of some appropriately defined quantum states.
arXiv Detail & Related papers (2021-02-09T13:48:00Z)
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.