論文の概要: Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information
- arxiv url: http://arxiv.org/abs/2607.21533v1
- Date: Thu, 23 Jul 2026 17:19:21 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-24 18:26:25.496151
- Title: Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information
- Title（参考訳）: 量子アルゴリズムと量子情報における定理証明のためのベンチマークエージェント
- Abstract要約: Lean-QuantumAlg-BenchとLean-QIT-Benchは、量子アルゴリズムと量子情報理論のための36と40の定理補完タスクを含む2つのLean 4ベンチマークである。
GPT-5.5,Kim K3,DeepSeek V4-Pro,MiniMax M3の4つのモデルを評価する。
難易度の高いスコアは、量子アルゴリズムベンチマークで100点中60.4点、量子情報ベンチマークで100点中59.6点である。
- 参考スコア（独自算出の注目度）: 13.46344583931603
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal verification is becoming increasingly practical for quantum computing, yet the ability of AI agents to construct machine-checkable proofs in this domain remains unmeasured. We introduce Lean-QuantumAlg-Bench and Lean-QIT-Bench, two Lean 4 benchmarks containing 36 and 40 theorem-completion tasks for quantum algorithms and quantum information theory, respectively. Every task compiles in a fixed environment and is evaluated by deterministic proof checking and targeted semantic review, with difficulty weights assigned before model execution. We evaluate four models-GPT-5.5, Kimi K3, DeepSeek V4-Pro, and MiniMax M3-within a common theorem-proving framework under two settings: a task-only baseline and library-augmented deduction (LAD), which additionally provides access to a verified domain library. The highest difficulty-weighted scores are 60.4 out of 100 on the quantum-algorithm benchmark and 59.6 out of 100 on the quantum-information benchmark. LAD improves both score and completion rate in all eight model-benchmark comparisons, with gains of up to 15.9 points, providing evidence that verified libraries can strengthen domain-specific proof agents. The results reveal recurring weaknesses of agentic proving in areas such as quantum simulation, quantum learning, quantum information measures, and entanglement theory. Monetary and wall-clock costs per score point also vary substantially across models, highlighting important capability-efficiency trade-offs. We expect these benchmarks to establish a reproducible baseline for developing more capable and reliable proof agents, and to pave the way toward self-evolving AI scientists for advancing quantum information science.
- Abstract（参考訳）: 形式的検証は量子コンピューティングではますます実用的になっているが、この領域で機械チェック可能な証明を構築するAIエージェントの能力は依然として測定されていない。
Lean-QuantumAlg-BenchとLean-QIT-Benchは、量子アルゴリズムと量子情報理論のための36と40の定理補完タスクを含む2つのLean 4ベンチマークである。
各タスクは固定された環境でコンパイルされ、決定論的証明チェックとターゲットセマンティックレビューによって評価される。
我々は,GPT-5.5,Kim K3,DeepSeek V4-Pro,MiniMax M3の4つのモデルを評価する。
難易度の高いスコアは、量子アルゴリズムベンチマークで100点中60.4点、量子情報ベンチマークで100点中59.6点である。
LADは8つのモデルベンチマーク比較のスコアと完了率を改善し、最大15.9ポイントのゲインを得て、検証済みライブラリがドメイン固有の証明エージェントを強化することができることを示す。
その結果, 量子シミュレーション, 量子学習, 量子情報測度, 絡み合い理論などの領域において, エージェント証明の弱点が繰り返し現れることがわかった。
スコアポイント当たりの通貨と壁時計のコストもモデルによって大きく異なり、重要な能力と効率のトレードオフが浮き彫りになっている。
これらのベンチマークは、より有能で信頼性の高い証明エージェントを開発するための再現可能なベースラインを確立し、量子情報科学を進化させるための自己進化型AI科学者への道を開くことを期待しています。
関連論文リスト
- QuantumMind: Constraint-Grounded Agentic Reasoning for Speedup Analysis in Quantum Computing [30.648434508009988]
我々は、量子加速仮説の生成と保守的なスクリーニングのための監査可能なエージェントワークフローであるQuantumMindを提案する。
公的なタスクを形式化し、構造と古典的なボトルネックを分析し、スコープ化された候補スキームを構築する。
我々は,タスク適応型7つのプロンプトとエージェント制御に対するQuantumMindの評価を行った。
論文 参考訳（メタデータ） (2026-08-07T20:21:13Z) - Qiskit QuantumKatas: Adapting Microsoft's Quantum Computing exercises for LLM evaluation [1.2891210250935148]
我々は、MicrosoftのQuantumKatas量子コンピューティングカリキュラムに、体系的LLM評価のための評価フレームワークをパッケージ化する。
その結果得られたベンチマークは、26のカテゴリにわたる350のタスクで構成され、高度なアルゴリズムを通じて基本的なゲートにまたがる。
各タスクは、自然言語プロンプト、標準解、古典回路シミュレーションによる決定論的テスト検証を含む。
論文 参考訳（メタデータ） (2026-05-26T16:02:08Z) - QuanBench+: A Unified Multi-Framework Benchmark for LLM-Based Quantum Code Generation [39.32132630606808]
Qiskit、PennyLane、Cirqにまたがる統一ベンチマークであるQuanBench+を紹介します。
我々は,機能テストの実行可能なモデルの評価を行い,Pass@1およびPass@5を報告する。
フレームワーク全体で、最強のワンショットスコアはキズキットで59.5%、サークルで54.8%、ペニーレーンで42.9%に達した。
論文 参考訳（メタデータ） (2026-03-25T20:51:21Z) - AQER: a scalable and efficient data loader for digital quantum computers [62.40228216126285]
我々は,ターゲット状態の絡み合いを体系的に低減し,負荷回路を構成するスケーラブルなAQL手法であるAQERを開発した。
我々は、合成データセット、古典画像および言語データセット、最大50キュービットの量子多体状態データセットを用いて、AQERの有効性を評価するための体系的な実験を行う。
論文 参考訳（メタデータ） (2026-02-02T14:39:42Z) - On-Chip Verified Quantum Computation with an Ion-Trap Quantum Processing Unit [0.5497663232622965]
本稿では、量子コンピューティングの検証とベンチマークのための新しいアプローチを提示し、実験的に実証する。
従来の情報理論的にセキュアな検証プロトコルとは異なり、我々のアプローチは完全にオンチップで実装されている。
我々の結果は、短期量子デバイスにおけるよりアクセスしやすく効率的な検証とベンチマーク戦略の道を開いた。
論文 参考訳（メタデータ） (2024-10-31T16:54:41Z) - QCircuitBench: A Large-Scale Dataset for Benchmarking Quantum Algorithm Design [63.02824918725805]
量子コンピューティングは、量子アルゴリズムによる古典的コンピューティングよりも大幅にスピードアップされていることが認識されている。
QCircuitBenchは、量子アルゴリズムの設計と実装におけるAIの能力を評価するために設計された最初のベンチマークデータセットである。
論文 参考訳（メタデータ） (2024-10-10T14:24:30Z) - QKSAN: A Quantum Kernel Self-Attention Network [53.96779043113156]
量子カーネル法(Quantum Kernel Methods, QKM)のデータ表現能力とSAMの効率的な情報抽出能力を組み合わせた量子カーネル自己認識機構(Quantum Kernel Self-Attention Mechanism, QKSAM)を導入する。
量子カーネル自己保持ネットワーク(QKSAN)フレームワークは,DMP(Dederred Measurement Principle)と条件測定技術を巧みに組み込んだQKSAMに基づいて提案されている。
4つのQKSANサブモデルはPennyLaneとIBM Qiskitプラットフォームにデプロイされ、MNISTとFashion MNISTのバイナリ分類を実行する。
論文 参考訳（メタデータ） (2023-08-25T15:08:19Z) - Quantum circuit architecture search on a superconducting processor [56.04169357427682]
変分量子アルゴリズム(VQA)は、ファイナンス、機械学習、化学といった様々な分野において、証明可能な計算上の優位性を得るための強力な証拠を示している。
しかし、現代のVQAで利用されるアンザッツは、表現性と訓練性の間のトレードオフのバランスをとることができない。
8量子ビット超伝導量子プロセッサ上でVQAを強化するために,効率的な自動アンサッツ設計技術を適用した最初の実証実験を実証する。
論文 参考訳（メタデータ） (2022-01-04T01:53:42Z) - On exploring the potential of quantum auto-encoder for learning quantum systems [60.909817434753315]
そこで我々は,古典的な3つのハードラーニング問題に対処するために,QAEに基づく効果的な3つの学習プロトコルを考案した。
私たちの研究は、ハード量子物理学と量子情報処理タスクを達成するための高度な量子学習アルゴリズムの開発に新たな光を当てています。
論文 参考訳（メタデータ） (2021-06-29T14:01:40Z) - QUANTIFY: A framework for resource analysis and design verification of
quantum circuits [69.43216268165402]
QUINTIFYは、量子回路の定量的解析のためのオープンソースのフレームワークである。
Google Cirqをベースにしており、Clifford+T回路を念頭に開発されている。
ベンチマークのため、QUINTIFYは量子メモリと量子演算回路を含む。
論文 参考訳（メタデータ） (2020-07-21T15:36:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。