論文の概要: Long-horizon autoformalization of a core theorem underlying MIP* = RE

• arxiv url: http://arxiv.org/abs/2609.19814v2
• Date: Thu, 24 Sep 2026 02:56:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-25 21:10:09.265164
• Title: Long-horizon autoformalization of a core theorem underlying MIP* = RE
• Title（参考訳）: MIP* = RE を基礎とするコア定理の長い水平自己形式化
• Abstract要約: 本稿では,人間の監督下でAI証明エージェントを協調するシステムであるFormalFlowを紹介する。 共有ブループリントを使用して、ネストした計画、証明、レビューループをガイドする。 我々は,古典的低次検定の量子音響性の,マシンチェックによるLean 4証明を完成させた。
• 参考スコア（独自算出の注目度）: 2.596570510945053
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization. Drawing on software engineering principles and practices, it uses a shared blueprint to guide nested planning, proving and review loops. Agents strengthen verification and review throughout formalization. We completed a machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test, a core theorem underlying MIP* = RE. Developing the proof took 63 days; greater parallelism could further reduce this time. The final library contains 126,367 lines of Lean code, all generated by agents. The formalization corrects side conditions and intermediate errors while preserving the published final error bound under corrected assumptions. This work provides a verified foundation for quantum complexity and demonstrates a route to affordable verification of major research proofs by small teams.
• Abstract（参考訳）: ランドマークの数学的形式化は、完成までに数年を要した。 本稿では,人間の監督下でAI証明エージェントをコーディネートして,長期的定式化における文のドリフトと証明構成に対処するシステムであるFormalFlowを提案する。 ソフトウェアエンジニアリングの原則とプラクティスに基づいて、ネストした計画、証明、レビューループをガイドするために、共有の青写真を使用する。 エージェントは形式化を通して検証とレビューを強化する。 MIP* = REの根底にある中核定理である古典的低次個別度検定の量子音性について,機械チェックしたLean 4の証明を完成させた。 証明の開発には63日を要した。 最後のライブラリには126,367行のリーンコードが含まれており、すべてエージェントによって生成される。 この形式化は、修正された仮定の下で公表された最終エラーを保存しながら、サイド条件と中間エラーを補正する。 この研究は、量子複雑性の検証基盤を提供し、小規模チームによる主要な研究証明を手頃な価格で検証するための道筋を示す。

関連論文リスト

• Multi-agent Autoformalization of Tensor Network Theory [0.21847754147782886]
  我々は、専門的な大規模言語モデルエージェントのチームを構築し、理論物理学における研究レベルの形式化のためのエージェント駆動ワークフローを提示する。 エージェントは、構造化された数学的青写真と定期的な人間のレビューを通して調整し、完全な形式化を自律的にオーケストレーションし実行した。 いくつかの声明では、エージェントは標準的な文献には含まれない新しい証明ルートを探索することができた。
  論文  参考訳（メタデータ） (2026-07-08T18:43:33Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。 最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。 汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-06-30T05:05:03Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。 4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。 我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
  論文  参考訳（メタデータ） (2026-06-03T20:09:39Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium [0.564046562677526]
  本稿では、VML(Vlasov-Maxwell-Landau)システムにおける平衡特性の完全式化について述べる。 プロジェクトはAIによる数学的研究の完全なループを実証する。
  論文  参考訳（メタデータ） (2026-03-16T21:21:53Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)

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

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