A Practical Quantum Hoare Logic with Classical Variables, I

• URL: http://arxiv.org/abs/2412.09869v1
• Date: Fri, 13 Dec 2024 05:28:19 GMT
• Title: A Practical Quantum Hoare Logic with Classical Variables, I
• Authors: Mingsheng Ying,
• Abstract summary: We present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work. It applies to quantum programs with classical variables that incorporate quantum arrays and parameterised quantum gates.
• Score: 2.789440475527173
• License:
• Abstract: In this paper, we present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work: (1) Enhanced expressivity of the programming language: Our logic applies to quantum programs with classical variables that incorporate quantum arrays and parameterised quantum gates, which have not been addressed in previous research on quantum Hoare logic, either with or without classical variables. (2) Intuitive correctness specifications: In our logic, preconditions and postconditions for quantum programs with classical variables are specified as a pair consisting of a classical first-order logical formula and a quantum predicate formula (possibly parameterised by classical variables). These specifications offer greater clarity and align more closely with the programmer's intuitive understanding of quantum and classical interactions. (3) Simplified proof system: By introducing a novel idea in formulating a proof rule for reasoning about quantum measurements, along with (2), we develop a proof system for quantum programs that requires only minimal modifications to classical Hoare logic. Furthermore, this proof system can be effectively and conveniently combined with classical first-order logic to verify quantum programs with classical variables. As a result, the learning curve for quantum program verification techniques is significantly reduced for those already familiar with classical program verification techniques, and existing tools for verifying classical programs can be more easily adapted for quantum program verification.

Related papers

• Quantum Machine Learning: from physics to software engineering [58.720142291102135]
  We show how classical machine learning approach can help improve the facilities of quantum computers. We discuss how quantum algorithms and quantum computers may be useful for solving classical machine learning tasks.
  arXiv  Detail & Related papers  (2023-01-04T23:37:45Z)
• Anticipative measurements in hybrid quantum-classical computation [68.8204255655161]
  We present an approach where the quantum computation is supplemented by a classical result. Taking advantage of its anticipation also leads to a new type of quantum measurements, which we call anticipative. In an anticipative quantum measurement the combination of the results from classical and quantum computations happens only in the end.
  arXiv  Detail & Related papers  (2022-09-12T15:47:44Z)
• Classical surrogates for quantum learning models [0.7734726150561088]
  We introduce the concept of a classical surrogate, a classical model which can be efficiently obtained from a trained quantum learning model. We show that large classes of well-analyzed re-uploading models have a classical surrogate.
  arXiv  Detail & Related papers  (2022-06-23T14:37:02Z)
• 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)
• Qunity: A Unified Language for Quantum and Classical Computing (Extended Version) [3.5348690973777006]
  We introduce Qunity, a new quantum programming language. Qunity treats quantum computing as a natural generalization of classical computing. We show how Qunity can cleanly express several quantum algorithms.
  arXiv  Detail & Related papers  (2022-04-26T15:34:22Z)
• 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)
• 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)
• 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)
• On the Principles of Differentiable Quantum Programming Languages [13.070557640180004]
  Variational Quantum Circuits (VQCs) are predicted to be one of the most important near-term quantum applications. We propose the first formalization of auto-differentiation techniques for quantum circuits.
  arXiv  Detail & Related papers  (2020-04-02T16:46:13Z)
• From a quantum theory to a classical one [117.44028458220427]
  We present and discuss a formal approach for describing the quantum to classical crossover. The method was originally introduced by L. Yaffe in 1982 for tackling large-$N$ quantum field theories.
  arXiv  Detail & Related papers  (2020-04-01T09:16:38Z)

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.