論文の概要: Formal Verification of Continuous-Variable Quantum Programs

• arxiv url: http://arxiv.org/abs/2607.17714v1
• Date: Mon, 20 Jul 2026 09:09:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-21 18:48:37.559555
• Title: Formal Verification of Continuous-Variable Quantum Programs
• Title（参考訳）: 連続可変量子プログラムの形式的検証
• Abstract要約: 連続可変量子コンピューティング(CQC)のための正式なフレームワークを提供する。 CQCはフォトニック量子ハードウェアによってサポートされているが、私たちはCQCの形式的な意味論を知らない。 論理に基づく記号的弱条件CQCを実装した。
• 参考スコア（独自算出の注目度）: 6.925649240526206
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\em unbounded} and have expected values that are defined by an improper integral (or an infinite series), which may not converge. We overcome these challenges to give a formal semantics to a universal programming language for CQC and to provide the first Hoare logic for CQC. The assertions of our logic are built from polynomials over canonical observables. Besides proving relative completeness, we implement a symbolic weakest-precondition calculator for CQC based on our logic. Our tool has successfully verified CQC algorithms from textbooks and calculated their approximation errors for physically realizable implementations, proved the correctness (i.e., equivalence) of gate decompositions for CQC hardware, and computed the resource requirements (i.e., number of photon-number states) for achieving a desired accuracy in the classical simulation of continuous-variable quantum programs.
• Abstract（参考訳）: 連続可変量子コンピューティング(CQC)のための正式なフレームワークを提供する。 CQCはフォトニック量子ハードウェアによってサポートされているが、連続変数量子プログラムの形式的意味論や、その検証のための一意的なホア論理は認識していない。 Discrete-Variable Quantum Computing (DQC) で利用可能な公式なフレームワークのどれでも CQC に拡張するための技術的障害はいくつかある。 最も重要なことに、連続変数の量子プログラムは、無限次元ヒルベルト空間上で作用する;それらの測定結果はしばしば {\em unbounded} であり、不適切な積分(あるいは無限級数)によって定義される期待値を持ち、収束しない。 我々はこれらの課題を克服し、CQCのための汎用プログラミング言語に形式的な意味論を与え、CQCのための最初のHoareロジックを提供する。 私たちの論理のアサーションは、正準可観測子上の多項式から成り立っている。 相対完全性を証明することに加えて、論理に基づくCQCのための記号的最弱条件電卓を実装している。 我々のツールは教科書からCQCアルゴリズムを検証し、物理的に実現可能な実装の近似誤差を計算し、CQCハードウェアのゲート分解の正しさ(等価性)を証明し、連続可変量子プログラムの古典的シミュレーションにおいて所望の精度を達成するためのリソース要件(光子数状態の数)を計算した。

関連論文リスト

• Reasoning about Continuous-Variable Quantum Systems [10.113921654362638]
  連続変数量子コンピューティング(continuous-variable quantum computing, CVQC)は、連続領域上の値を計測する計算パラダイムである。 CVQCは物理量子システムをモデル化するための便利な計算フレームワークであり、量子光学に基づくハードウェアプラットフォームのための優れた抽象化である。 本研究では,コアCV量子プログラミング言語の形式的意味論と,プログラムの正確性検証手法を開発する。
  論文  参考訳（メタデータ） (2026-07-25T10:36:34Z)
• AQER: a scalable and efficient data loader for digital quantum computers [62.40228216126285]
  我々は,ターゲット状態の絡み合いを体系的に低減し,負荷回路を構成するスケーラブルなAQL手法であるAQERを開発した。 我々は、合成データセット、古典画像および言語データセット、最大50キュービットの量子多体状態データセットを用いて、AQERの有効性を評価するための体系的な実験を行う。
  論文  参考訳（メタデータ） (2026-02-02T14:39:42Z)
• Continual Quantum Architecture Search with Tensor-Train Encoding: Theory and Applications to Signal Processing [68.35481158940401]
  CL-QASは連続的な量子アーキテクチャ検索フレームワークである。 振幅のエンコードと変分量子回路の忘れを犠牲にすることの課題を緩和する。 制御可能なロバスト性表現性、サンプル効率の一般化、およびバレンプラトーを使わずに滑らかな収束を実現する。
  論文  参考訳（メタデータ） (2026-01-10T02:36:03Z)
• SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits [13.511470455769482]
  量子プログラムに関する推論は、プログラミングモデルや計算パラダイムに関わらず、根本的な課題である。 本稿では,SAQR-QCと呼ばれる,そのような設定における推論の論理について述べる。 i) 精度のいくつかの(決定的な)損失が組み込まれており、(ii) 推論ステップの列における精度の蓄積の損失を小さく抑えるためのメカニズムを持ち、(iii) 推論をスケーラブルにするためには、すべての推論ステップが局所的である。
  論文  参考訳（メタデータ） (2025-07-18T03:48:36Z)
• Formal Verification of Variational Quantum Circuits [44.06507276521908]
  変分量子回路(VQC)は多くの量子機械学習アルゴリズムの中心的なコンポーネントである。 本稿では,VQCの形式的検証問題に関する基礎的および実践的研究について述べる。
  論文  参考訳（メタデータ） (2025-07-14T12:28:32Z)
• VQC-MLPNet: An Unconventional Hybrid Quantum-Classical Architecture for Scalable and Robust Quantum Machine Learning [50.95799256262098]
  変分量子回路(VQC)は量子機械学習を約束するが、表現性、訓練性、耐雑音性の課題に直面している。 本稿では,VQCが学習中に古典多層パーセプトロンの第一層重みを生成するハイブリッドアーキテクチャであるVQC-MLPNetを提案する。
  論文  参考訳（メタデータ） (2025-06-12T01:38:15Z)
• QbC: Quantum Correctness by Construction [4.068363933090715]
  提案するQuantum Correctness by Construction (QbC) は,その仕様から量子プログラムを構築するための手法である。 プリコンディションとポストコンディションを使用してプログラム特性を規定し、その仕様から量子状態におけるプログラム構築のための音質および完全改善ルールを提案する。 このアプローチは、プログラムの詳細を導出する方法を自然に提案し、その過程で重要な設計上の選択を強調します。
  論文  参考訳（メタデータ） (2023-07-28T16:00:57Z)
• Quantum process tomography of continuous-variable gates using coherent states [49.299443295581064]
  ボソニックモード超伝導回路におけるコヒーレント状態量子プロセストモグラフィ(csQPT)の使用を実証する。 符号化量子ビット上の変位とSNAP演算を用いて構築した論理量子ゲートを特徴付けることにより,本手法の結果を示す。
  論文  参考訳（メタデータ） (2023-03-02T18:08:08Z)
• InQuIR: Intermediate Representation for Interconnected Quantum Computers [0.0]
  InQuIRは、分散量子システム上での通信と計算を表現できる表現である。 デッドロックなどの分散プログラムで発生する問題を説明するために,InQuIRで記述した例を挙げる。 また、InQuIR用のソフトウェアツールを提供し、量子回路の計算コストを評価する。
  論文  参考訳（メタデータ） (2023-02-01T06:19:23Z)
• TeD-Q: a tensor network enhanced distributed hybrid quantum machine learning framework [48.491303218786044]
  TeD-Qは、量子機械学習のためのオープンソースのソフトウェアフレームワークである。 古典的な機械学習ライブラリと量子シミュレータをシームレスに統合する。 量子回路とトレーニングの進捗をリアルタイムで視覚化できるグラフィカルモードを提供する。
  論文  参考訳（メタデータ） (2023-01-13T09:35:05Z)
• 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)
• Using Quantum Metrological Bounds in Quantum Error Correction: A Simple Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
  本稿では、量子誤り訂正符号の品質と、論理ゲートの普遍的な集合を達成する能力とを結びつける、近似したイージン・クニル定理の証明を示す。 我々の導出は、一般的な量子気象プロトコルにおける量子フィッシャー情報に強力な境界を用いる。
  論文  参考訳（メタデータ） (2020-04-24T17:58:10Z)
• On the Principles of Differentiable Quantum Programming Languages [13.070557640180004]
  変分量子回路(VQC)は、最も重要な短期量子応用の1つであると予測されている。 本稿では,量子回路における自己微分法の最初の形式化を提案する。
  論文  参考訳（メタデータ） (2020-04-02T16:46:13Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。