symQV: Automated Symbolic Verification of Quantum Programs

• URL: http://arxiv.org/abs/2212.02267v1
• Date: Mon, 5 Dec 2022 13:46:27 GMT
• Title: symQV: Automated Symbolic Verification of Quantum Programs
• Authors: Fabian Bauer-Marquart, Stefan Leue, Christian Schilling
• Abstract summary: We present symQV, a symbolic execution framework for writing and verifying quantum computations. symQV can automatically verify that a quantum program complies with a first-order specification.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a symbolic quantum program model. This allows to encode the verification problem in an SMT formula, which can then be checked with a delta-complete decision procedure. We also propose an abstraction technique to speed up the verification process. Experimental results show that the abstraction improves symQV's scalability by an order of magnitude to quantum programs with 24 qubits (a 2^24-dimensional state space).

Related papers

• Quantum-Chiplet: A Novel Python-Based Efficient and Scalable Design Methodology for Quantum Circuit Verification and Implementation [5.727672509269657]
  We propose a new quantum representation (QPR) to facilitate the analysis of massively parallel quantum computation. For the verification of quantum circuits, we introduce Quantum-Chiplet, a hierarchical quantum behavior modeling methodology. A quantum amplitude estimation example demonstrates that this method significantly improves the design process, with more than 10x speed-up compared to IBM Qiskit at 14 qubits.
  arXiv  Detail & Related papers  (2025-03-13T05:12:41Z)
• Automated Verification of Silq Quantum Programs using SMT Solvers [0.0]
  SilVer is an automated tool for verifying behaviors of quantum programs written in Silq. We introduce a programming model that is based on a quantum RAM-style computer as an interface between Silq programs and SMT proof obligations.
  arXiv  Detail & Related papers  (2024-06-05T10:12:47Z)
• A Case for Synthesis of Recursive Quantum Unitary Programs [9.287571320531457]
  Quantum programs are notoriously difficult to code and verify due to unintuitive quantum knowledge associated with quantum programming. We present Q Synth, the first quantum program synthesis framework, including a new inductive quantum programming language. Q Synth successfully synthesizes ten quantum unitary programs including quantum adder circuits, quantum eigenvalue inversion circuits and Quantum Fourier Transformation.
  arXiv  Detail & Related papers  (2023-11-20T03:01:36Z)
• Decision Diagrams for Symbolic Verification of Quantum Circuits [14.715027770125335]
  This paper proposes the first decision-diagram approach for operating symbolic objects and verifying quantum circuits with symbolic terms. Our symbolic tensor decision diagrams (symbolic TDD) could verify the functionality of the 160-qubit quantum Fourier transform circuit within three minutes.
  arXiv  Detail & Related papers  (2023-08-01T10:35:04Z)
• 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)
• Delegated variational quantum algorithms based on quantum homomorphic encryption [69.50567607858659]
  Variational quantum algorithms (VQAs) are one of the most promising candidates for achieving quantum advantages on quantum devices. The private data of clients may be leaked to quantum servers in such a quantum cloud model. A novel quantum homomorphic encryption (QHE) scheme is constructed for quantum servers to calculate encrypted data.
  arXiv  Detail & Related papers  (2023-01-25T07:00:13Z)
• 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)
• Variational quantum process tomography [12.843681115589122]
  We put forward a quantum machine learning algorithm which encodes the unknown unitary quantum process into a relatively shallow depth parametric quantum circuit. Results show that those quantum processes could be reconstructed with high fidelity, while the number of input states required are at least $2$ orders of magnitude less than required by the standard quantum process tomography.
  arXiv  Detail & Related papers  (2021-08-05T03:36:26Z)
• 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)
• 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)
• Quantum walk processes in quantum devices [55.41644538483948]
  We study how to represent quantum walk on a graph as a quantum circuit. Our approach paves way for the efficient implementation of quantum walks algorithms on quantum computers.
  arXiv  Detail & Related papers  (2020-12-28T18:04:16Z)

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.