Equivalence Checking of Quantum Circuits by Model Counting

• URL: http://arxiv.org/abs/2403.18813v1
• Date: Wed, 27 Mar 2024 17:58:20 GMT
• Title: Equivalence Checking of Quantum Circuits by Model Counting
• Authors: Jingyi Mei, Tim Coopmans, Marcello Bonsangue, Alfons Laarman,
• Abstract summary: This paper gives a Turing reduction of the (universal) quantum circuits equivalence problem to weighted model counting (WMC) With an open-source implementation, we demonstrate that this novel approach can outperform a state-of-the-art equivalence-checking tool based on ZX calculus and decision diagrams.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verifying equivalence between two quantum circuits is a hard problem, that is nonetheless crucial in compiling and optimizing quantum algorithms for real-world devices. This paper gives a Turing reduction of the (universal) quantum circuits equivalence problem to weighted model counting (WMC). Our starting point is a folklore theorem showing that equivalence checking of quantum circuits can be done in the so-called Pauli-basis. We combine this insight with a WMC encoding of quantum circuit simulation, which we extend with support for the Toffoli gate. Finally, we prove that the weights computed by the model counter indeed realize the reduction. With an open-source implementation, we demonstrate that this novel approach can outperform a state-of-the-art equivalence-checking tool based on ZX calculus and decision diagrams.

Related papers

• Equivalence Checking of Quantum Circuits via Intermediary Matrix Product Operator [4.306566710489809]
  Equivalence checking plays a vital role in identifying errors that may arise during compilation and optimization of quantum circuits. We introduce a novel method based on Matrix Product Operators (MPOs) for determining the equivalence of quantum circuits.
  arXiv  Detail & Related papers  (2024-10-14T18:00:00Z)
• Equivalence Checking of Parameterised Quantum Circuits [13.796569260568939]
  We propose a novel compact representation for PQCs based on tensor decision diagrams. We present an algorithm for verifying PQC equivalence without the need for instantiation.
  arXiv  Detail & Related papers  (2024-04-29T06:25:00Z)
• Lightcone Bounds for Quantum Circuit Mapping via Uncomplexity [1.0360348400670518]
  We show that a minimal SWAP-gate count for executing a quantum circuit on a device emerges via the minimization of the distance between quantum states. This work constitutes the first use of quantum circuit uncomplexity to practically-relevant quantum computing.
  arXiv  Detail & Related papers  (2024-02-01T10:32:05Z)
• 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)
• Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation of Variational Quantum Algorithms [3.610459670994051]
  Variational quantum algorithms have been introduced as a promising class of quantum-classical hybrid algorithms. It is essential to verify that parameterized quantum circuits have been compiled correctly. No methodology capable of handling circuits with parameters has been proposed yet.
  arXiv  Detail & Related papers  (2022-10-21T18:00:04Z)
• Quantum circuit debugging and sensitivity analysis via local inversions [62.997667081978825]
  We present a technique that pinpoints the sections of a quantum circuit that affect the circuit output the most. We demonstrate the practicality and efficacy of the proposed technique by applying it to example algorithmic circuits implemented on IBM quantum machines.
  arXiv  Detail & Related papers  (2022-04-12T19:39:31Z)
• Numerical Simulations of Noisy Quantum Circuits for Computational Chemistry [51.827942608832025]
  Near-term quantum computers can calculate the ground-state properties of small molecules. We show how the structure of the computational ansatz as well as the errors induced by device noise affect the calculation.
  arXiv  Detail & Related papers  (2021-12-31T16:33:10Z)
• 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)
• Realization of arbitrary doubly-controlled quantum phase gates [62.997667081978825]
  We introduce a high-fidelity gate set inspired by a proposal for near-term quantum advantage in optimization problems. By orchestrating coherent, multi-level control over three transmon qutrits, we synthesize a family of deterministic, continuous-angle quantum phase gates acting in the natural three-qubit computational basis.
  arXiv  Detail & Related papers  (2021-08-03T17:49:09Z)
• QUANTIFY: A framework for resource analysis and design verification of quantum circuits [69.43216268165402]
  QUANTIFY is an open-source framework for the quantitative analysis of quantum circuits. It is based on Google Cirq and is developed with Clifford+T circuits in mind. For benchmarking purposes QUANTIFY includes quantum memory and quantum arithmetic circuits.
  arXiv  Detail & Related papers  (2020-07-21T15:36:25Z)
• 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.