論文の概要: Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information
- arxiv url: http://arxiv.org/abs/2607.05492v1
- Date: Mon, 06 Jul 2026 18:00:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-08 21:24:51.291167
- Title: Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information
- Title（参考訳）: Lean-Quantum: 量子情報のAI支援形式化を目指して
- Abstract要約: 理論解析のための再利用可能な形式的基盤として設計された,量子情報のためのLean 4ライブラリを提示する。
有限次元量子系上の正半定値作用素に対するサンドイッチ付きレニイ相対エントロピーのDPIを定式化する。
このライブラリは有限次元量子力学の基底非依存作用素理論フレームワークを提供する。
- 参考スコア（独自算出の注目度）: 4.962621441807053
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Quantum information theory is built on entropic quantities; among them, the sandwiched Rényi relative entropy is a fundamental divergence with various applications, and its data processing inequality (DPI) under quantum channels is a cornerstone result. In this work, we present a Lean 4 library for quantum information, designed as a reusable formal infrastructure for theoretical analysis. As a central demonstration of the library, we formalize the DPI for the sandwiched Rényi relative entropy for positive semidefinite operators on finite-dimensional quantum systems. The library provides a basis-independent operator-theoretic framework for finite-dimensional quantum mechanics compatible with the standard mathematical library Mathlib, including reusable interfaces for finite-dimensional systems, states, channels, tensor products, partial traces, Choi operators, Kraus representations, and Stinespring representations. It also builds infrastructure for noncommutative trace inequalities, including operator monotonicity and convexity via the real continuous functional calculus, block-operator positivity, Hilbert-Schmidt operator spaces, Jensen's operator inequality, generalized perspectives, operator power means, and Lieb-Ando trace inequalities. On top of this framework, we formalize entropy-specific ingredients for the DPI: variational formulas for the sandwiched quasi-entropy via Young and reverse-Young inequalities, tensor-product compatibility of real powers, and Haar measures on unitary groups. Together, these components yield a Lean formalization of the DPI, give strong subadditivity as a corollary, and provide the last missing component needed to complete the Lean formalization of the generalized quantum Stein's lemma. More broadly, the development provides machine-checkable foundations for future formalized and AI-assisted research in quantum information theory.
- Abstract（参考訳）: 量子情報理論はエントロピー量に基づいて構築されており、その中でもサンドイッチ化されたレニイ相対エントロピーは様々な応用と基本的な相違点であり、その量子チャネルにおけるデータ処理の不等式(DPI)は画期的な結果である。
本研究では、量子情報のためのLean 4ライブラリを、理論解析のための再利用可能な形式的インフラストラクチャとして設計する。
図書館の中心的なデモンストレーションとして、有限次元量子系上の正半定値作用素に対するサンドイッチ付きレニイ相対エントロピーのDPIを定式化する。
このライブラリは、標準数学ライブラリMathlibと互換性のある有限次元量子力学の基底非依存の演算子理論フレームワークを提供し、有限次元システム、状態、チャネル、テンソル積、部分トレース、Choi演算子、クラウス表現、スティネスプリング表現の再利用インターフェイスを含む。
また、実連続汎関数計算による作用素の単調性や凸性、ブロック-演算正則性、ヒルベルト・シュミット作用素空間、イェンセン作用素の不等式、一般化された視点、作用素のパワー平均、リーブ・アンドロトレース不等式など、非可換なトレース不等式に対するインフラストラクチャを構築する。
この枠組みの上に, DPI のエントロピー特異的成分として, ヤング不等式とリバースヤング不等式によるサンドイッチ付き準エントロピーの変分式, 実数のテンソル積整合, ユニタリ群におけるハール測度を定式化する。
これらの成分は共に DPI のリーン形式化をもたらし、コローナとして強い部分付加性を与え、一般化された量子シュタインの補題のリーン形式化を完成させるのに必要な最後の欠落成分を与える。
より広範に、この開発は将来の量子情報理論における形式化およびAI支援研究のためのマシンチェック可能な基礎を提供する。
関連論文リスト
- Quantum Information Decoupling Beyond Finite Dimensions [1.2691047660244335]
任意の分離可能で、無限次元のシステムのための枠組みを確立する。
有限次元入力に対しては、操作された系の有限エントロピーを仮定する。
応用として、無限次元の量子状態マージプロトコルを構築する。
論文 参考訳（メタデータ） (2026-07-28T18:00:00Z) - Quantum Reservoir Computing: Recent Advances and Future Directions [34.77938621771246]
量子貯水池計算(QRC)は、時間的およびシーケンシャルな入力を計測された特徴に変換するために、固定または弱調整量子システムの力学を利用する。
その計算力は、しばしば量子系の指数的に大きいヒルベルト空間に起因している。
ハードウェアでは、これらの機能は、有限サンプリング、ハードウェアノイズ、測定バックアクション、観測可能量の推定コストによってさらに制限される。
論文 参考訳（メタデータ） (2026-07-20T22:38:49Z) - Device-independent Quantum Key Distribution in the commuting operator framework [10.668771582679561]
デバイス非依存量子鍵分布(DIQKD)は、安全な量子通信のための金の標準である。
既存の証明技法は、従属的な仮定に依存する傾向があるため、この目標を常に満たすとは限らない。
鍵レートの計算は非可換最適化問題として考えられる。
論文 参考訳（メタデータ） (2026-07-03T19:44:10Z) - Cumulant-based quantum relative Rényi functional [0.0]
我々は、新しい累積型量子相対Rényiを候補量子Rényi分散として導入する。
函数は自然にリー・トロッター積拡大を通じて経路積分的な表現を持つ。
得られた相対量子性量は、基底状態が可換である場合にのみ消滅することを示す。
論文 参考訳（メタデータ） (2026-06-30T06:34:53Z) - Geometric Complexity of Quantum Channels via Unitary Dilations [0.0]
量子チャネルの族として機能する幾何学的複雑性をユニタリディレーションに基づいて導入・解析する。
所定イデアル閉進化に対する幾何学的複雑性の損失を定量化する。
論文 参考訳（メタデータ） (2026-01-02T16:28:36Z) - Performance Guarantees for Quantum Neural Estimation of Entropies [31.955071410400947]
量子神経推定器(QNE)は古典的ニューラルネットワークとパラメトリズド量子回路を組み合わせたものである。
非漸近的エラーリスク境界の形で測定された相対エントロピーのQNEの形式的保証について検討する。
我々の理論は、測定された相対エントロピーに対するQNEの原則的実装を促進することを目的としている。
論文 参考訳（メタデータ） (2025-11-24T16:36:06Z) - Grassmann Variational Monte Carlo with neural wave functions [45.935798913942904]
ヒルベルト空間のグラスマン幾何学の観点から、Pfau et al.citepfau2024accurateによって導入された枠組みを定式化する。
正方格子上のハイゼンベルク量子スピンモデルに対する我々のアプローチを検証し、多くの励起状態に対して高精度なエネルギーと物理観測値を達成する。
論文 参考訳（メタデータ） (2025-07-14T13:53:13Z) - Quantum computer formulation of the FKP-operator eigenvalue problem for probabilistic learning on manifolds [0.0]
本稿では、多様体上の確率論的学習(PLoM)の発展における課題に対処する量子コンピューティングの定式化について述べる。
これは高次元フォッカー・プランク作用素のスペクトル問題を解くことを含む。
ラプラシアンおよびポテンシャルの明示的な公式が導出され、パウリ行列式を用いてキュービットに写像される。
論文 参考訳（メタデータ） (2025-02-20T14:05:16Z) - DimINO: Dimension-Informed Neural Operator Learning [41.37905663176428]
Diminoは次元分析にインスパイアされたフレームワークである。
既存のニューラル演算子アーキテクチャにシームレスに統合することができる。
PDEデータセットで最大76.3%のパフォーマンス向上を実現している。
論文 参考訳（メタデータ） (2024-10-08T10:48:50Z) - Quantum channels, complex Stiefel manifolds, and optimization [45.9982965995401]
我々は、量子チャネルの位相空間と複素スティーフェル多様体の商の間の連続性関係を確立する。
確立された関係は、様々な量子最適化問題に適用できる。
論文 参考訳（メタデータ） (2024-08-19T09:15:54Z) - Quantum tomography of helicity states for general scattering processes [55.2480439325792]
量子トモグラフィーは、物理学における量子系の密度行列$rho$を計算するのに欠かせない道具となっている。
一般散乱過程におけるヘリシティ量子初期状態の再構成に関する理論的枠組みを提案する。
論文 参考訳（メタデータ） (2023-10-16T21:23:42Z) - A Lie Algebraic Theory of Barren Plateaus for Deep Parameterized Quantum Circuits [37.84307089310829]
変分量子コンピューティングスキームは、パラメタライズド量子回路を介して初期状態を送信することで損失関数を訓練する。
彼らの約束にもかかわらず、これらのアルゴリズムの訓練性は不毛の台地によって妨げられている。
十分に深いパラメタライズド量子回路の損失関数の分散を正確に表現する一般リー代数を提案する。
論文 参考訳（メタデータ） (2023-09-17T18:14:10Z) - Noisy Quantum Kernel Machines [58.09028887465797]
量子学習マシンの新たなクラスは、量子カーネルのパラダイムに基づくものである。
消散と脱コヒーレンスがパフォーマンスに与える影響について検討する。
量子カーネルマシンでは,デコヒーレンスや散逸を暗黙の正規化とみなすことができる。
論文 参考訳（メタデータ） (2022-04-26T09:52:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。