Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs

• URL: http://arxiv.org/abs/2308.04741v2
• Date: Wed, 6 Sep 2023 01:49:15 GMT
• Title: Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
• Authors: Yuxin Deng, Huiling Wu, Ming Xu
• Abstract summary: 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.
• Score: 3.871660145364189
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms.

Related papers

• BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
  We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations. We develop a quantum BI-style logic that includes interpretations for separating implication. We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs.
  arXiv  Detail & Related papers  (2024-09-16T10:34:45Z)
• A refinement of the argument of local realism versus quantum mechanics by algorithmic randomness [0.0]
  In quantum mechanics, the notion of probability plays a crucial role. In modern mathematics, probability theory means nothing other than measure theory. We present a refinement of the Born rule, called the principle of typicality, for specifying the property of results of measurements in an operational way.
  arXiv  Detail & Related papers  (2023-12-20T18:22:42Z)
• 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)
• 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)
• Entanglement and coherence in Bernstein-Vazirani algorithm [58.720142291102135]
  Bernstein-Vazirani algorithm allows one to determine a bit string encoded into an oracle. We analyze in detail the quantum resources in the Bernstein-Vazirani algorithm. We show that in the absence of entanglement, the performance of the algorithm is directly related to the amount of quantum coherence in the initial state.
  arXiv  Detail & Related papers  (2022-05-26T20:32:36Z)
• Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs [1.1878820609988696]
  A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties of quantum programs. In this paper, we introduce a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables.
  arXiv  Detail & Related papers  (2022-05-04T08:57:44Z)
• 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)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  This paper introduces a dynamic logic formalism for reasoning about information flow in composite quantum systems. We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness for the Teleportation protocol and for a standard Quantum Secret Sharing protocol.
  arXiv  Detail & Related papers  (2021-10-04T12:20:23Z)
• Logical Credal Networks [87.25387518070411]
  This paper introduces Logical Credal Networks, an expressive probabilistic logic that generalizes many prior models that combine logic and probability. We investigate its performance on maximum a posteriori inference tasks, including solving Mastermind games with uncertainty and detecting credit card fraud.
  arXiv  Detail & Related papers  (2021-09-25T00:00:47Z)
• The Logic of Quantum Programs [77.34726150561087]
  We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems.
  arXiv  Detail & Related papers  (2021-09-14T16:08:37Z)
• 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)
• Error mitigation and quantum-assisted simulation in the error corrected regime [77.34726150561087]
  A standard approach to quantum computing is based on the idea of promoting a classically simulable and fault-tolerant set of operations. We show how the addition of noisy magic resources allows one to boost classical quasiprobability simulations of a quantum circuit.
  arXiv  Detail & Related papers  (2021-03-12T20:58:41Z)
• A Quantum Interpretation of Bunched Logic for Quantum Separation Logic [22.507329566323982]
  We develop a program logic where pre- and post-conditions are BI formulas describing quantum states. We exercise the logic for proving the security of quantum one-time pad and secret sharing.
  arXiv  Detail & Related papers  (2021-01-30T22:24:36Z)
• Secure Two-Party Quantum Computation Over Classical Channels [63.97763079214294]
  We consider the setting where the two parties (a classical Alice and a quantum Bob) can communicate only via a classical channel. We show that it is in general impossible to realize a two-party quantum functionality with black-box simulation in the case of malicious quantum adversaries. We provide a compiler that takes as input a classical proof of quantum knowledge (PoQK) protocol for a QMA relation R and outputs a zero-knowledge PoQK for R that can be verified by classical parties.
  arXiv  Detail & Related papers  (2020-10-15T17:55:31Z)
• Quantum Hoare logic with classical variables [3.1181601933418897]
  We propose a quantum Hoare logic for a simple while language which involves both classical and quantum variables. With novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs.
  arXiv  Detail & Related papers  (2020-08-15T23:56:18Z)
• Using Quantum Metrological Bounds in Quantum Error Correction: A Simple Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
  We present a proof of the approximate Eastin-Knill theorem, which connects the quality of a quantum error-correcting code with its ability to achieve a universal set of logical gates. Our derivation employs powerful bounds on the quantum Fisher information in generic quantum metrological protocols.
  arXiv  Detail & Related papers  (2020-04-24T17:58:10Z)

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.