論文の概要: A Machine-Verified Proof of a Quantum-Optimization Conjecture
- arxiv url: http://arxiv.org/abs/2606.29687v1
- Date: Mon, 29 Jun 2026 01:25:40 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-30 18:07:16.017201
- Title: A Machine-Verified Proof of a Quantum-Optimization Conjecture
- Title（参考訳）: 量子最適化の機械検証による証明
- Abstract要約: 量子最適化における10年以上の課題を,マシンで検証した解決法について報告する。
大規模な言語モデルであるClaude Fable 5を用いて証明し,その正しさをエンドツーエンドで検証した。
この研究は、量子情報科学などにおけるオープンな予想を解決するための道を開いた。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We report a machine-verified resolution of a problem open for over a decade in quantum optimization: the Farhi, Goldstone and Gutmann (FGG) conjecture that depth-$p$ Quantum Approximate Optimization Algorithm (QAOA) on the ring of disagrees attains approximation ratio $(2p+1)/(2p+2)$ exactly. We found the proof using a large language model, Claude Fable 5, and verified its correctness end-to-end by the Lean 4 proof assistant. Our methodology includes several ingredients: building on a substantial Lean library of quantum information, we formalized the QAOA components and the known parts of the problem, and reduced the conjecture to a single open mathematical statement. The model was then handed the library and our agentic toolkit, and tasked with closing that gap by constructing a proof in Lean. The resulting process is a feedback loop between the model's natural-language reasoning and Lean's mechanical verification, which converged to a machine-verified proof. Human verification is required only for the structural scaffolding - that the formal statement faithfully encodes the intended claim - while the proof itself is supplied by the model and certified mechanically by Lean. The proof is nevertheless striking - the model uncovered a hidden dynamical symmetry of the problem and exploited it, borrowing tools and machinery from an adjacent field to turn a hard existence problem into an explicit construction. This work paves the way for resolving open conjectures in quantum information science and beyond.
- Abstract（参考訳）: Farhi, Goldstone and Gutmann (FGG) 予想では、不一致環上の深さ-$p$量子近似最適化アルゴリズム (QAOA) は近似比$(2p+1)/(2p+2)$である。
私たちは、大きな言語モデルであるClaude Fable 5を使って証明を見つけ、Lean 4の証明アシスタントによってその正しさをエンドツーエンドで検証しました。
量子情報の実質的なLeanライブラリ上に構築し、QAOAコンポーネントと既知の問題の部品を形式化し、予想を単一のオープンな数学的ステートメントに減らした。
その後、モデルはライブラリとエージェントツールキットを渡され、Leanで証明を構築することでそのギャップを埋めることが義務付けられました。
結果として得られたプロセスは、モデルの自然言語推論とLeanの機械的検証の間のフィードバックループであり、マシン検証された証明に収束した。
証明そのものがモデルによって提供され、リーンによって機械的に認定されるのに対して、人間の検証は構造的足場(構造的足場)のためにのみ必要である。
モデルは問題の隠れた力学対称性を発見し、それを悪用し、隣接する分野から道具や機械を借りて、難解な存在問題を明示的な構成に変えた。
この研究は、量子情報科学などにおけるオープンな予想を解決するための道を開いた。
関連論文リスト
- AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics [0.0]
AxQMは物理学における最大の証明合成ベンチマークである。
タスク数によっては、物理における証明合成のベンチマークとしては最大で4倍である。
論文 参考訳（メタデータ） (2026-09-04T13:58:19Z) - ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
我々は,Olympiadレベルの診断用ベンチマークであるComBenchと,大規模言語モデルの推論機能を紹介する。
ComBenchには、補完的な2つの設定で整理された100の人間注釈の競合レベルの問題が含まれている。
実験の結果、最強モデルはAvg.全体65.4%、Best@4.3%に達した。
論文 参考訳（メタデータ） (2026-06-09T06:50:15Z) - Mathematics with large language models as provers and verifiers [1.1029146548022293]
ChatGPT は6つの IMO 問題のうち5つを解き、[Cohen, Journal of Sequences, 2025] の 6 個の数理論の予想の約3分の1を閉じる。
論文 参考訳（メタデータ） (2025-10-11T20:35:25Z) - A Formalization of the Generalized Quantum Stein's Lemma in Lean [0.0]
我々は、リーン対話的定理証明器において、ハヤシとヤマサキ(2024年)で提示された証明を定式化する。
これは、これまでコンピュータで検証された証明を持つ物理学で最も技術的に要求される定理である。
論文 参考訳（メタデータ） (2025-10-09T17:41:13Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
大型言語モデル(LLM)は厳密な論理的推論と記号的推論を必要とする形式的ドメインと競合する。
本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。
論文 参考訳（メタデータ） (2025-05-20T15:13:32Z) - APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。
エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。
この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
論文 参考訳（メタデータ） (2025-05-09T03:38:31Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - Lyra: Orchestrating Dual Correction in Automated Theorem Proving [63.115422781158934]
Lyraは新しいフレームワークで、ツール補正とConjecture Correctionという2つの異なる補正メカニズムを採用している。
ツール補正は幻覚の緩和に寄与し、それによって証明の全体的な精度が向上する。
Conjecture Correctionは命令で生成を洗練させるが、ペア化された(生成、エラー、改善)プロンプトは収集しない。
論文 参考訳（メタデータ） (2023-09-27T17:29:41Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳（メタデータ） (2022-03-03T10:07:32Z) - Depth-efficient proofs of quantumness [77.34726150561087]
量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。
本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
論文 参考訳（メタデータ） (2021-07-05T17:45:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。