論文の概要: Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory
- arxiv url: http://arxiv.org/abs/2607.09632v1
- Date: Fri, 10 Jul 2026 17:28:26 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-13 14:47:12.914006
- Title: Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory
- Title（参考訳）: Lean-QIT: 量子情報理論のための形式的基盤を目指して
- Authors: Chengkai Zhu, Ziao Tang, Guocheng Zhen, Yimeng Cao, Yusheng Zhao, Ranyiliu Chen, Xuanqiang Zhao, Lei Zhang, Xin Wang,
- Abstract要約: 量子情報理論(QIT)は、量子情報処理の能力と基本的な限界を特徴づける。
既存の開発には、コード、エラー基準、達成可能なレート、能力を定義する再利用可能な運用層がない。
有限次元QITのためのLean 4ライブラリであるLeanQITを紹介します。
- 参考スコア（独自算出の注目度）: 13.58013986113788
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing, underpinning quantum communication, computation, and error correction. Formalizing its coding theorems requires connecting finite-block protocols, analytic inequalities, and asymptotic limits within a unified machine-checked framework. Existing developments, however, lack a reusable operational layer that defines codes, error criteria, achievable rates, and capacities independently of their information-theoretic characterizations. In this work, we present LeanQIT, a Lean 4 library for finite-dimensional QIT. It provides composable, kernel-checked interfaces for quantum states and channels, source and channel codes, finite-block performance criteria, hypothesis testing, one-shot quantities, and asymptotic rate constructions. Using this infrastructure, we formalize Schumacher's quantum source-coding theorem, the Holevo--Schumacher--Westmoreland classical-capacity theorem, and the entanglement-assisted classical-capacity theorem together with its strong converse. By separating operational definitions from analytic characterizations and exposing reusable achievability, converse, and asymptotic components, Lean-QIT provides a machine-readable foundation for formal QIT and a compositional knowledge substrate for emerging AI-assisted formalization, automated proof search, and agentic reasoning in quantum information and computation.
- Abstract（参考訳）: 量子情報理論(QIT)は、量子情報処理の能力と基本的な限界を特徴づけ、量子通信、計算、誤り訂正の基盤となる。
符号化定理を定式化するには、有限ブロックプロトコル、解析的不等式、および統合されたマシンチェックフレームワーク内の漸近的極限を接続する必要がある。
しかし、既存の開発には、コード、エラー基準、達成可能なレート、能力を定義する再利用可能な運用層がない。
本稿では,有限次元QITのためのLean 4ライブラリであるLeanQITを紹介する。
量子状態とチャネル、ソースコードとチャネルコード、有限ブロック性能基準、仮説テスト、ワンショット量、漸近速度構成のための構成可能なカーネルチェックインターフェイスを提供する。
このインフラを用いて、シューマッハの量子源符号化定理、ホレボ-シューマッハ-ウェストモアランド古典容量定理、およびエンタングルメント支援古典容量定理をその強い逆と共に定式化する。
分析的特徴から運用定義を分離し、再利用可能な達成可能性、逆転、漸近的コンポーネントを公開することにより、Lean-QITは、量子情報と計算におけるAI支援形式化、自動証明探索、エージェント推論を創出するための、形式的QITのための機械可読基盤と構成的知識基盤を提供する。
関連論文リスト
- AQER: a scalable and efficient data loader for digital quantum computers [62.40228216126285]
我々は,ターゲット状態の絡み合いを体系的に低減し,負荷回路を構成するスケーラブルなAQL手法であるAQERを開発した。
我々は、合成データセット、古典画像および言語データセット、最大50キュービットの量子多体状態データセットを用いて、AQERの有効性を評価するための体系的な実験を行う。
論文 参考訳（メタデータ） (2026-02-02T14:39:42Z) - Symbolic Specification and Reasoning for Quantum Data and Operations [5.341843260877702]
量子データと演算に関するシンボリックな仕様と推論を可能にする、Operator Logic $mathbfSOL$と呼ばれる一般的な論理フレームワークを提案する。
このフレームワーク内では、古典的な一階述語論理言語が、量子データと演算を指定するために使われる形式演算子の言語に埋め込まれている。
この埋め込みにより、それらの性質に関する推論は、基礎となる古典的データの選択された理論を変調することができる。
論文 参考訳（メタデータ） (2025-12-26T20:57:42Z) - Quantumness certification via non-demolition measurements [0.0]
量子非破壊測定(QNDM)がこの認証の適切な手段である。
環境との相互作用による量子-古典遷移をQNDMで追跡できるアプリケーションについて論じる。
簡単な実装であるため、QNDMアプローチは量子力学の基礎と量子情報理論の両方に直接的な関係を持つことができる。
論文 参考訳（メタデータ） (2025-12-10T15:15:10Z) - Quantum Machine Unlearning: Foundations, Mechanisms, and Taxonomy [9.347709392900502]
量子マシン・アンラーニングは、計算と信頼できる人工知能をプライバシ保存する量子情報理論の交差において、基礎的な課題として浮上している。
本稿では、検証可能なパラダイム内で、物理的制約のアルゴリズム機構と倫理的ガバナンスを統一する形式的な枠組みを確立することにより、QMUを推し進める。
論文 参考訳（メタデータ） (2025-11-01T05:11:40Z) - Advances in Machine Learning: Where Can Quantum Techniques Help? [0.0]
量子機械学習(QML)は、量子コンピューティングと人工知能の交差点における有望なフロンティアである。
本稿では,従来の機械学習の計算ボトルネックに対処するQMLの可能性について検討する。
論文 参考訳（メタデータ） (2025-07-11T07:47:47Z) - 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) - An operational definition of quantum information scrambling [0.0]
量子情報スクランブル(QIS)は、いくつかの量子系の特徴である。
本稿では,QISの定式化に基づく量子状態の量子化に基づく新しい計算効率のQIS量化器を提案する。
等尺的量子進化によって引き起こされるQISの度合いを反映した最適推定確率が、アクセス可能な最小情報に直接接続されていることを示す。
論文 参考訳（メタデータ） (2023-12-18T19:00:01Z) - Potential and limitations of quantum extreme learning machines [55.41644538483948]
本稿では,QRCとQELMをモデル化するフレームワークを提案する。
我々の分析は、QELMとQRCの両方の機能と限界をより深く理解するための道を開いた。
論文 参考訳（メタデータ） (2022-10-03T09:32:28Z) - Quantum Semantic Communications for Resource-Efficient Quantum Networking [52.3355619190963]
本稿では、量子機械学習と量子意味表現の進歩を活かした新しい量子意味通信(QSC)フレームワークを提案する。
提案手法は,高い量子セマンティック忠実度を達成しつつ,必要な量子通信資源の約50～75%の削減を実現する。
論文 参考訳（メタデータ） (2022-05-05T03:49:19Z) - Using Quantum Metrological Bounds in Quantum Error Correction: A Simple
Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
本稿では、量子誤り訂正符号の品質と、論理ゲートの普遍的な集合を達成する能力とを結びつける、近似したイージン・クニル定理の証明を示す。
我々の導出は、一般的な量子気象プロトコルにおける量子フィッシャー情報に強力な境界を用いる。
論文 参考訳（メタデータ） (2020-04-24T17:58:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。