Automated Verification of Silq Quantum Programs using SMT Solvers

• URL: http://arxiv.org/abs/2406.03119v1
• Date: Wed, 5 Jun 2024 10:12:47 GMT
• Title: Automated Verification of Silq Quantum Programs using SMT Solvers
• Authors: Marco Lewis, Paolo Zuliani, Sadegh Soudjani,
• Abstract summary: 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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present SilVer (Silq Verification), an automated tool for verifying behaviors of quantum programs written in Silq, which is a high-level programming language for quantum computing. The goal of the verification is to ensure correctness of the Silq quantum program against user-defined specifications using SMT solvers. We introduce a programming model that is based on a quantum RAM-style computer as an interface between Silq programs and SMT proof obligations, allowing for control of quantum operations using both classical and quantum conditions. Additionally, users can employ measurement flags within the specification to easily specify conditions that measurement results require to satisfy for being a valid behavior. We provide case studies on the verification of generating entangled states and multiple oracle-based algorithms.

Related papers

• 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)
• ADAPT-QSCI: Adaptive Construction of Input State for Quantum-Selected Configuration Interaction [0.0]
  We present a quantum-classical hybrid algorithm for calculating the ground state and its energy of the quantum many-body Hamiltonian. We numerically illustrate that our method, dubbed textitADAPT-QSCI, can yield accurate ground-state energies for small molecules.
  arXiv  Detail & Related papers  (2023-11-02T09:15:50Z)
• Schrödinger as a Quantum Programmer: Estimating Entanglement via Steering [3.187381965457262]
  We develop a quantum algorithm that tests for and quantifies the separability of a general bipartite state by using the quantum steering effect. Our findings provide a meaningful connection between steering, entanglement, quantum algorithms, and quantum computational complexity theory.
  arXiv  Detail & Related papers  (2023-03-14T13:55:06Z)
• 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)
• symQV: Automated Symbolic Verification of Quantum Programs [0.0]
  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.
  arXiv  Detail & Related papers  (2022-12-05T13:46:27Z)
• 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)
• QSAN: A Near-term Achievable Quantum Self-Attention Network [73.15524926159702]
  Self-Attention Mechanism (SAM) is good at capturing the internal connections of features. A novel Quantum Self-Attention Network (QSAN) is proposed for image classification tasks on near-term quantum devices.
  arXiv  Detail & Related papers  (2022-07-14T12:22:51Z)
• 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)
• On exploring the potential of quantum auto-encoder for learning quantum systems [60.909817434753315]
  We devise three effective QAE-based learning protocols to address three classically computational hard learning problems. Our work sheds new light on developing advanced quantum learning algorithms to accomplish hard quantum physics and quantum information processing tasks.
  arXiv  Detail & Related papers  (2021-06-29T14:01:40Z)
• 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)
• A MLIR Dialect for Quantum Assembly Languages [78.8942067357231]
  We demonstrate the utility of the Multi-Level Intermediate Representation (MLIR) for quantum computing. We extend MLIR with a new quantum dialect that enables the expression and compilation of common quantum assembly languages. We leverage a qcor-enabled implementation of the QIR quantum runtime API to enable a retargetable (quantum hardware agnostic) compiler workflow.
  arXiv  Detail & Related papers  (2021-01-27T13:00:39Z)

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.