Fugu-MT 論文翻訳(概要): symQV: Automated Symbolic Verification of Quantum Programs

論文の概要: symQV: Automated Symbolic Verification of Quantum Programs

arxiv url: http://arxiv.org/abs/2212.02267v1
Date: Mon, 5 Dec 2022 13:46:27 GMT
ステータス: 処理完了
システム内更新日: 2023-01-09 20:20:35.834774
Title: symQV: Automated Symbolic Verification of Quantum Programs
Title（参考訳）: symQV:量子プログラムのシンボリック検証の自動化
Authors: Fabian Bauer-Marquart, Stefan Leue, Christian Schilling
Abstract要約: 本稿では,量子計算を記述・検証するためのシンボリックな実行フレームワークであるsymQVを提案する。 symQVは、量子プログラムが一階の仕様に準拠していることを自動的に検証することができる。
参考スコア（独自算出の注目度）: 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).
Abstract（参考訳）: 量子回路モデルで量子計算を記述・検証するためのシンボリック実行フレームワークであるsymqvを提案する。 symQVは、量子プログラムが一階の仕様に準拠していることを自動的に検証することができる。我々は正式に記号量子プログラムモデルを導入する。これにより、検証問題をSMT式にエンコードし、デルタ完全決定手順でチェックすることができる。また,検証プロセスを高速化するための抽象化手法を提案する。実験結果から,24量子ビット(2^24次元状態空間)の量子プログラムに対して,symQVのスケーラビリティを桁違いに向上することが示された。

関連論文リスト

Automated Verification of Silq Quantum Programs using SMT Solvers [0.0]
SilVerは、Silqで記述された量子プログラムの動作を検証する自動化ツールである。我々は,SilqプログラムとSMT証明義務のインターフェースとして,量子RAMスタイルのコンピュータをベースとしたプログラミングモデルを提案する。
論文参考訳（メタデータ） (2024-06-05T10:12:47Z)
A Case for Synthesis of Recursive Quantum Unitary Programs [9.287571320531457]
量子プログラムは、量子プログラミングに関連する直感的な量子知識のために、コーディングと検証が難しいことで知られている。本稿では、新しい帰納的量子プログラム言語を含む、最初の量子プログラム合成フレームワークであるQ Synthを紹介する。 Q Synthは量子加算器回路、量子固有値反転回路、量子フーリエ変換を含む10個の量子ユニタリプログラムをうまく合成する。
論文参考訳（メタデータ） (2023-11-20T03:01:36Z)
Decision Diagrams for Symbolic Verification of Quantum Circuits [14.715027770125335]
本稿では,シンボルオブジェクトを動作させ,量子回路をシンボル項で検証するための最初の決定図法を提案する。我々のシンボリックテンソル決定図(シンボリックTDD)は、3分で160量子フーリエ変換回路の機能を検証することができる。
論文参考訳（メタデータ） (2023-08-01T10:35:04Z)
Quantum process tomography of continuous-variable gates using coherent states [49.299443295581064]
ボソニックモード超伝導回路におけるコヒーレント状態量子プロセストモグラフィ(csQPT)の使用を実証する。符号化量子ビット上の変位とSNAP演算を用いて構築した論理量子ゲートを特徴付けることにより,本手法の結果を示す。
論文参考訳（メタデータ） (2023-03-02T18:08:08Z)
Delegated variational quantum algorithms based on quantum homomorphic encryption [69.50567607858659]
変分量子アルゴリズム(VQA)は、量子デバイス上で量子アドバンテージを達成するための最も有望な候補の1つである。クライアントのプライベートデータは、そのような量子クラウドモデルで量子サーバにリークされる可能性がある。量子サーバが暗号化データを計算するための新しい量子ホモモルフィック暗号(QHE)スキームが構築されている。
論文参考訳（メタデータ） (2023-01-25T07:00:13Z)
Qafny: A Quantum-Program Verifier [39.47005122712576]
本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
論文参考訳（メタデータ） (2022-11-11T18:50:52Z)
Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
本稿では,量子状態の知識を必要とせず,量子回路の可換性を検証する回路指向対称性検証を提案する。特に、従来の量子領域形式を回路指向安定化器に一般化するフーリエ時間安定化器(STS)手法を提案する。
論文参考訳（メタデータ） (2021-12-27T21:15:35Z)
Variational quantum process tomography [12.843681115589122]
我々は、未知のユニタリ量子プロセスを比較的浅い深さパラメトリック量子回路に符号化する量子機械学習アルゴリズムを提唱した。その結果、これらの量子プロセスは高い忠実度で再構成可能である一方で、必要な入力状態の数は、標準量子プロセストモグラフィーで要求されるよりも少なくとも2ドル以下であることがわかった。
論文参考訳（メタデータ） (2021-08-05T03:36:26Z)
Tensor Network Quantum Virtual Machine for Simulating Quantum Circuits at Exascale [57.84751206630535]
本稿では,E-scale ACCelerator(XACC)フレームワークにおける量子回路シミュレーションバックエンドとして機能する量子仮想マシン(TNQVM)の近代化版を提案する。新バージョンは汎用的でスケーラブルなネットワーク処理ライブラリであるExaTNをベースにしており、複数の量子回路シミュレータを提供している。ポータブルなXACC量子プロセッサとスケーラブルなExaTNバックエンドを組み合わせることで、ラップトップから将来のエクサスケールプラットフォームにスケール可能なエンドツーエンドの仮想開発環境を導入します。
論文参考訳（メタデータ） (2021-04-21T13:26:42Z)
Facial Expression Recognition on a Quantum Computer [68.8204255655161]
量子機械学習手法を用いて表情認識の可能な解を示す。適切に定義された量子状態の振幅に符号化されたグラフの隣接行列を操作する量子回路を定義する。
論文参考訳（メタデータ） (2021-02-09T13:48:00Z)
Quantum walk processes in quantum devices [55.41644538483948]
グラフ上の量子ウォークを量子回路として表現する方法を研究する。提案手法は,量子ウォークアルゴリズムを量子コンピュータ上で効率的に実装する方法である。
論文参考訳（メタデータ） (2020-12-28T18:04:16Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。