Verification of Nondeterministic Quantum Programs
- URL: http://arxiv.org/abs/2302.07973v1
- Date: Wed, 15 Feb 2023 22:37:23 GMT
- Title: Verification of Nondeterministic Quantum Programs
- Authors: Yuan Feng and Yingte Xu
- Abstract summary: 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.
- Score: 1.9302781323430196
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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. It supports the stepwise refinement of programs, a method that
has proven useful in software development. Nondeterminism has also been
introduced in quantum programming, and the termination of nondeterministic
quantum programs has been extensively analysed. In this paper, we go beyond
termination analysis to investigate the verification of nondeterministic
quantum programs where properties are given by sets of hermitian operators on
the associated Hilbert space. Hoare-type logic systems for partial and total
correctness are proposed, which turn out to be both sound and relatively
complete with respect to their corresponding semantic correctness. To show the
utility of these proof systems, we analyse some quantum algorithms, such as
quantum error correction scheme, the Deutsch algorithm, and a nondeterministic
quantum walk. Finally, a proof assistant prototype is implemented to aid in the
automated reasoning of nondeterministic quantum programs.
Related papers
- Refinement calculus of quantum programs with projective assertions [5.151896714190243]
This paper introduces a refinement calculus tailored for quantum programs.
We first study the partial correctness of nondeterministic programs within a quantum.
We also present their semantics in transforming a postcondition to the weakest liberal postconditions.
arXiv Detail & Related papers (2023-11-23T22:12:57Z) - 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 Conformal Prediction for Reliable Uncertainty Quantification in
Quantum Machine Learning [47.991114317813555]
Quantum models implement implicit probabilistic predictors that produce multiple random decisions for each input through measurement shots.
This paper proposes to leverage such randomness to define prediction sets for both classification and regression that provably capture the uncertainty of the model.
arXiv Detail & Related papers (2023-04-06T22:05:21Z) - Design by Contract Framework for Quantum Software [1.9988400064884826]
We propose a design-by-contract framework for quantum software.
It provides assertions on the input and output states of all quantum circuits built by certain procedures.
Our framework has sufficient expressive power to verify the whole procedure of quantum software.
arXiv Detail & Related papers (2023-03-31T00:21:28Z) - Quantum process tomography of continuous-variable gates using coherent
states [49.299443295581064]
We demonstrate the use of coherent-state quantum process tomography (csQPT) for a bosonic-mode superconducting circuit.
We show results for this method by characterizing a logical quantum gate constructed using displacement and SNAP operations on an encoded qubit.
arXiv Detail & Related papers (2023-03-02T18:08:08Z) - 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) - 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) - Characterizing quantum instruments: from non-demolition measurements to
quantum error correction [48.43720700248091]
In quantum information processing quantum operations are often processed alongside measurements which result in classical data.
Non-unitary dynamical processes can take place on the system, for which common quantum channel descriptions fail to describe the time evolution.
Quantum measurements are correctly treated by means of so-called quantum instruments capturing both classical outputs and post-measurement quantum states.
arXiv Detail & Related papers (2021-10-13T18:00:13Z) - Preparation of quantum superposition using partial negation [1.911678487931003]
The speed of the preparation process and the accuracy of the prepared superposition has a special importance to the success of any quantum algorithm.
The proposed method can be used to prepare the required quantum superposition in $mathcalO(n)$ steps.
arXiv Detail & Related papers (2021-09-29T11:57:44Z) - 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.