論文の概要: Symbolic Specification and Reasoning for Quantum Data and Operations

• arxiv url: http://arxiv.org/abs/2512.22383v1
• Date: Fri, 26 Dec 2025 20:57:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-30 22:37:30.020798
• Title: Symbolic Specification and Reasoning for Quantum Data and Operations
• Title（参考訳）: 量子データと演算のシンボリック仕様と推論
• Authors: Mingsheng Ying,
• Abstract要約: 量子データと演算に関するシンボリックな仕様と推論を可能にする、Operator Logic $mathbfSOL$と呼ばれる一般的な論理フレームワークを提案する。 このフレームワーク内では、古典的な一階述語論理言語が、量子データと演算を指定するために使われる形式演算子の言語に埋め込まれている。 この埋め込みにより、それらの性質に関する推論は、基礎となる古典的データの選択された理論を変調することができる。
• 参考スコア（独自算出の注目度）: 5.341843260877702
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time, they are essential for ensuring the scalability and efficiency of automated reasoning and verification tools for quantum algorithms and programs. However, a formal theory for symbolic specification and reasoning about quantum data and operations is still lacking, which significantly limits the practical applicability of automated verification techniques in quantum computing. In this paper, we present a general logical framework, called Symbolic Operator Logic $\mathbf{SOL}$, which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into $\mathbf{SOL}$ is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.
• Abstract（参考訳）: 量子情報と計算研究において、記号的手法は量子状態や演算に関する人間の仕様や推論に広く用いられている。 同時に、量子アルゴリズムやプログラムの自動推論と検証ツールのスケーラビリティと効率を確保するためには、これらが不可欠である。 しかし、量子データと演算に関する記号的仕様と推論に関する公式な理論はいまだに欠けており、量子コンピューティングにおける自動検証技術の実践的適用性を著しく制限している。 本稿では,シンボリック演算子$\mathbf{SOL}$という,量子データと演算のシンボリック仕様と推論を可能にする一般的な論理フレームワークを提案する。 このフレームワーク内では、古典的な一階述語論理言語が、再帰的定義を含む量子データと演算を指定するために使われる形式演算子の言語に埋め込まれている。 この埋め込みにより、それらの性質について、基礎となる古典的データ(例えばブール代数や群論)の選択理論を変調し、古典的計算のために開発された既存の自動検証ツールを活用することができる。 古典的な一階述語論理を$\mathbf{SOL}$に埋め込むことは、まさにシンボリックメソッドを可能にするものであることを強調すべきである。 我々は,このフレームワークが,Lean,Coq,関連システムなどの証明アシスタントにおいて,量子計算と情報を証明する形式的検証と自動定理の基盤となることを想定する。

関連論文リスト

• Quantum algorithms for equational reasoning [0.0]
  シンボリックな表現を解析するための量子計算フレームワークである量子正規化(quantum normal form reduction)を導入する。 テンソルネットワークシミュレーションを用いて量子インスパイアされたアルゴリズムを実演する。 このフレームワークは、量子回路設計からデータ圧縮まで、領域における量子記号計算の道を開く。
  論文  参考訳（メタデータ） (2025-08-28T18:00:06Z)
• QCircuitBench: A Large-Scale Dataset for Benchmarking Quantum Algorithm Design [63.02824918725805]
  量子コンピューティングは、量子アルゴリズムによる古典的コンピューティングよりも大幅にスピードアップされていることが認識されている。 QCircuitBenchは、量子アルゴリズムの設計と実装におけるAIの能力を評価するために設計された最初のベンチマークデータセットである。
  論文  参考訳（メタデータ） (2024-10-10T14:24:30Z)
• Efficient Learning for Linear Properties of Bounded-Gate Quantum Circuits [62.46800898243033]
  量子学習理論の最近の進歩は、様々な古典的な入力によって生成された測定データから、大きな量子ビット回路の線形特性を効率的に学習できるのか? 我々は、小さな予測誤差を達成するためには、$d$で線形にスケーリングするサンプルの複雑さが必要であることを証明し、それに対応する計算複雑性は、dで指数関数的にスケールする可能性がある。 そこで本研究では,古典的影と三角展開を利用したカーネルベースの手法を提案し,予測精度と計算オーバーヘッドとのトレードオフを制御可能とした。
  論文  参考訳（メタデータ） (2024-08-22T08:21:28Z)
• Qafny: A Quantum-Program Verifier [39.47005122712576]
  本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。 我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
  論文  参考訳（メタデータ） (2022-11-11T18:50:52Z)
• Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs [1.1878820609988696]
  量子変数を持つ一階述語論理は、量子プログラムの様々な性質を特定し、推論するためのアサーション言語として必要とされる。 本稿では,Birkhoff-von Neumann量子論理を量子変数上の普遍的および存在的量子化器を用いて一階拡張する。
  論文  参考訳（メタデータ） (2022-05-04T08:57:44Z)
• No-signalling constrains quantum computation with indefinite causal structure [45.279573215172285]
  我々は、不定因果構造を持つ量子計算の定式化を開発する。 我々は高階量子マップの計算構造を特徴付ける。 計算的および情報理論的な性質を持つこれらの規則は、量子システム間のシグナル伝達関係のより物理的概念によって決定される。
  論文  参考訳（メタデータ） (2022-02-21T13:43:50Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  本稿では,複合量子システムにおける情報フローの推論のための動的論理形式について紹介する。 本稿では,この論理の文法,関係意味論,音響証明システムについて述べる。 アプリケーションとしては,テレポーテーションプロトコルと標準量子秘密共有プロトコルに対して,正式な正当性を与えるために,我々のシステムを利用する。
  論文  参考訳（メタデータ） (2021-10-04T12:20:23Z)
• The Logic of Quantum Programs [77.34726150561087]
  本稿では,量子プログラムにおける情報フローの論理計算について述べる。 特に、複素量子系における量子測定、ユニタリ進化、絡み合いを扱うことができる動的論理を導入する。
  論文  参考訳（メタデータ） (2021-09-14T16:08:37Z)
• Quantum Hoare logic with classical variables [3.1181601933418897]
  古典変数と量子変数の両方を含む簡単な時相言語に対して量子ホア論理を提案する。 古典量子状態とそれに対応するアサーションの新たな定義により、論理体系は非常に単純であり、古典的プログラムの伝統的なホア論理と類似している。
  論文  参考訳（メタデータ） (2020-08-15T23:56:18Z)

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

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