Model Checking for Verification of Quantum Circuits

• URL: http://arxiv.org/abs/2104.11359v1
• Date: Fri, 23 Apr 2021 00:43:37 GMT
• Title: Model Checking for Verification of Quantum Circuits
• Authors: Mingsheng Ying
• Abstract summary: We will describe a framework for assertion-based verification of quantum circuits. Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks.
• Score: 1.1878820609988696
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In this talk, we will describe a framework for assertion-based verification (ABV) of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which: (i) Noiseless and noisy quantum circuits are modelled as operator- and super-operator-valued transition systems, respectively, both of which can be further represented by tensor networks. (ii) Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Their semantics is defined based on the design decision: they will be used in verification of quantum circuits by simulation on classical computers or human reasoning rather than by quantum physics experiments (e.g. testing through measurements); (iii) Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks. We observe that many optimisation techniques for computing relational products used in BDD-based model checking algorithms can be generalised for contracting tensor networks of quantum circuits.

Related papers

• Efficient Learning for Linear Properties of Bounded-Gate Quantum Circuits [63.733312560668274]
  Given a quantum circuit containing d tunable RZ gates and G-d Clifford gates, can a learner perform purely classical inference to efficiently predict its linear properties? We prove that the sample complexity scaling linearly in d is necessary and sufficient to achieve a small prediction error, while the corresponding computational complexity may scale exponentially in d. We devise a kernel-based learning model capable of trading off prediction error and computational complexity, transitioning from exponential to scaling in many practical settings.
  arXiv  Detail & Related papers  (2024-08-22T08:21:28Z)
• Mapping quantum circuits to shallow-depth measurement patterns based on graph states [0.0]
  We create a hybrid simulation technique for measurement-based quantum computing. We show that groups of fully commuting operators can be implemented using fully-parallel, i.e., non-adaptive, measurements. We discuss how such circuits can be implemented in constant quantum depths by employing quantum teleportation.
  arXiv  Detail & Related papers  (2023-11-27T19:00:00Z)
• Peptide Binding Classification on Quantum Computers [3.9540968630765643]
  We conduct an extensive study on using near-term quantum computers for a task in the domain of computational biology. We perform sequence classification on a task relevant to the design of therapeutic proteins, and find competitive performance with classical baselines of similar scale. This work constitutes the first proof-of-concept application of near-term quantum computing to a task critical to the design of therapeutic proteins.
  arXiv  Detail & Related papers  (2023-11-27T10:32:31Z)
• Decomposition of Matrix Product States into Shallow Quantum Circuits [62.5210028594015]
  tensor network (TN) algorithms can be mapped to parametrized quantum circuits (PQCs) We propose a new protocol for approximating TN states using realistic quantum circuits. Our results reveal one particular protocol, involving sequential growth and optimization of the quantum circuit, to outperform all other methods.
  arXiv  Detail & Related papers  (2022-09-01T17:08:41Z)
• Quantum variational learning for entanglement witnessing [0.0]
  This work focuses on the potential implementation of quantum algorithms allowing to properly classify quantum states defined over a single register of $n$ qubits. We exploit the notion of "entanglement witness", i.e., an operator whose expectation values allow to identify certain specific states as entangled. We made use of Quantum Neural Networks (QNNs) in order to successfully learn how to reproduce the action of an entanglement witness.
  arXiv  Detail & Related papers  (2022-05-20T20:14:28Z)
• Theory of Quantum Generative Learning Models with Maximum Mean Discrepancy [67.02951777522547]
  We study learnability of quantum circuit Born machines (QCBMs) and quantum generative adversarial networks (QGANs) We first analyze the generalization ability of QCBMs and identify their superiorities when the quantum devices can directly access the target distribution. Next, we prove how the generalization error bound of QGANs depends on the employed Ansatz, the number of qudits, and input states.
  arXiv  Detail & Related papers  (2022-05-10T08:05:59Z)
• 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)
• Quantum algorithms for quantum dynamics: A performance study on the spin-boson model [68.8204255655161]
  Quantum algorithms for quantum dynamics simulations are traditionally based on implementing a Trotter-approximation of the time-evolution operator. variational quantum algorithms have become an indispensable alternative, enabling small-scale simulations on present-day hardware. We show that, despite providing a clear reduction of quantum gate cost, the variational method in its current implementation is unlikely to lead to a quantum advantage.
  arXiv  Detail & Related papers  (2021-08-09T18:00:05Z)
• Tensor Network Quantum Virtual Machine for Simulating Quantum Circuits at Exascale [57.84751206630535]
  We present a modernized version of the Quantum Virtual Machine (TNQVM) which serves as a quantum circuit simulation backend in the e-scale ACCelerator (XACC) framework. The new version is based on the general purpose, scalable network processing library, ExaTN, and provides multiple quantum circuit simulators. By combining the portable XACC quantum processors and the scalable ExaTN backend we introduce an end-to-end virtual development environment which can scale from laptops to future exascale platforms.
  arXiv  Detail & Related papers  (2021-04-21T13:26:42Z)
• A Tensor Network based Decision Diagram for Representation of Quantum Circuits [8.36229449571485]
  This paper proposes a decision diagram style data structure, called TDD, for principled and convenient applications of tensor networks. By exploiting circuit partition, the TDD of a quantum circuit can be computed efficiently. It is expected that TDDs will play an important role in various design automation tasks related to quantum circuits.
  arXiv  Detail & Related papers  (2020-09-06T00:12:31Z)

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.