論文の概要: Automated Verification of Silq Quantum Programs using SMT Solvers
- arxiv url: http://arxiv.org/abs/2406.03119v1
- Date: Wed, 5 Jun 2024 10:12:47 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-06 18:59:55.878139
- Title: Automated Verification of Silq Quantum Programs using SMT Solvers
- Title（参考訳）: SMTソルバを用いたシルク量子プログラムの自動検証
- Authors: Marco Lewis, Paolo Zuliani, Sadegh Soudjani,
- Abstract要約: SilVerは、Silqで記述された量子プログラムの動作を検証する自動化ツールである。
我々は,SilqプログラムとSMT証明義務のインターフェースとして,量子RAMスタイルのコンピュータをベースとしたプログラミングモデルを提案する。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: 我々は、Silqで記述された量子プログラムの動作を検証する自動化ツールであるSilVer(Silq Verification)を紹介する。
この検証の目的は、SMTソルバを用いたユーザ定義仕様に対するSilq量子プログラムの正当性を保証することである。
我々は、SilqプログラムとSMT証明義務のインターフェースとして量子RAMスタイルのコンピュータをベースとしたプログラミングモデルを導入し、古典的条件と量子的条件の両方を用いて量子演算の制御を可能にする。
さらに、ユーザは仕様内で測定フラグを使用して、測定結果が有効な振る舞いであるために必要な条件を簡単に指定することができる。
本稿では,絡み合った状態と複数のオラクルベースのアルゴリズムの検証事例について述べる。
関連論文リスト
- A Case for Synthesis of Recursive Quantum Unitary Programs [9.287571320531457]
量子プログラムは、量子プログラミングに関連する直感的な量子知識のために、コーディングと検証が難しいことで知られている。
本稿では、新しい帰納的量子プログラム言語を含む、最初の量子プログラム合成フレームワークであるQ Synthを紹介する。
Q Synthは量子加算器回路、量子固有値反転回路、量子フーリエ変換を含む10個の量子ユニタリプログラムをうまく合成する。
論文 参考訳（メタデータ） (2023-11-20T03:01:36Z) - ADAPT-QSCI: Adaptive Construction of Input State for Quantum-Selected
Configuration Interaction [0.0]
量子多体ハミルトンの基底状態とそのエネルギーを計算するための量子古典ハイブリッドアルゴリズムを提案する。
提案手法はtextitADAPT-QSCI と呼ばれ,小分子に対して正確な基底状態エネルギーが得られることを示す。
論文 参考訳（メタデータ） (2023-11-02T09:15:50Z) - Schrödinger as a Quantum Programmer: Estimating Entanglement via Steering [3.187381965457262]
我々は、量子ステアリング効果を用いて、一般的な二部状態の分離性をテストし、定量化する量子アルゴリズムを開発した。
我々の発見は、ステアリング、絡み合い、量子アルゴリズム、量子計算複雑性理論の間の有意義な関係を提供する。
論文 参考訳（メタデータ） (2023-03-14T13:55:06Z) - Delegated variational quantum algorithms based on quantum homomorphic
encryption [69.50567607858659]
変分量子アルゴリズム(VQA)は、量子デバイス上で量子アドバンテージを達成するための最も有望な候補の1つである。
クライアントのプライベートデータは、そのような量子クラウドモデルで量子サーバにリークされる可能性がある。
量子サーバが暗号化データを計算するための新しい量子ホモモルフィック暗号(QHE)スキームが構築されている。
論文 参考訳（メタデータ） (2023-01-25T07:00:13Z) - symQV: Automated Symbolic Verification of Quantum Programs [0.0]
本稿では,量子計算を記述・検証するためのシンボリックな実行フレームワークであるsymQVを提案する。
symQVは、量子プログラムが一階の仕様に準拠していることを自動的に検証することができる。
論文 参考訳（メタデータ） (2022-12-05T13:46:27Z) - Qafny: A Quantum-Program Verifier [39.47005122712576]
本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。
Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。
我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
論文 参考訳（メタデータ） (2022-11-11T18:50:52Z) - QSAN: A Near-term Achievable Quantum Self-Attention Network [73.15524926159702]
SAM(Self-Attention Mechanism)は機能の内部接続を捉えるのに長けている。
短期量子デバイスにおける画像分類タスクに対して,新しい量子自己注意ネットワーク(QSAN)を提案する。
論文 参考訳（メタデータ） (2022-07-14T12:22:51Z) - Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
本稿では,量子状態の知識を必要とせず,量子回路の可換性を検証する回路指向対称性検証を提案する。
特に、従来の量子領域形式を回路指向安定化器に一般化するフーリエ時間安定化器(STS)手法を提案する。
論文 参考訳（メタデータ） (2021-12-27T21:15:35Z) - On exploring practical potentials of quantum auto-encoder with
advantages [92.19792304214303]
量子オートエンコーダ(QAE)は、量子物理学で遭遇する次元の呪いを和らげるための強力なツールである。
我々はQAEを用いて固有値を効率的に計算し、高次元量子状態の対応する固有ベクトルを作成できることを証明した。
低ランク状態の忠実度推定,量子ギブス状態準備,量子メトロジーの課題を解決するために,QAEに基づく効果的な3つの学習プロトコルを考案した。
論文 参考訳（メタデータ） (2021-06-29T14:01:40Z) - Facial Expression Recognition on a Quantum Computer [68.8204255655161]
量子機械学習手法を用いて表情認識の可能な解を示す。
適切に定義された量子状態の振幅に符号化されたグラフの隣接行列を操作する量子回路を定義する。
論文 参考訳（メタデータ） (2021-02-09T13:48:00Z) - A MLIR Dialect for Quantum Assembly Languages [78.8942067357231]
量子コンピューティングにおけるMLIR(Multi-Level Intermediate Representation)の有用性を実証する。
我々は、共通量子集合言語の表現とコンパイルを可能にする新しい量子方言でMLIRを拡張した。
我々はQIR量子ランタイムAPIのqcor対応実装を活用して、再ターゲット可能な(量子ハードウェアに依存しない)コンパイラワークフローを実現する。
論文 参考訳（メタデータ） (2021-01-27T13:00:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。