論文の概要: ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization

• arxiv url: http://arxiv.org/abs/2609.34960v1
• Date: Mon, 28 Sep 2026 11:45:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-03 01:29:59.432384
• Title: ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
• Title（参考訳）: ProofLoom:研究レベル確率最適化の自動化のための証明駆動理論の構築
• Abstract要約: 本稿では,ProofLoomを紹介した。Proof-Obligation-Driven Theory Constructionのための,完全に自動化されたLLMエージェントシステムである。 ProofLoomは、公開されたアルゴリズム、ターゲット定理、およびソース証明を与えられた後、リーンモデルとサポート理論を自律的に構築する。 33の開発で、490,693行のアルゴリズムローカルなリーンコードを生成する。
• 参考スコア（独自算出の注目度）: 5.053793874612475
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formalizing research-level stochastic optimization in Lean requires both an algorithm model and domain theory connecting foundational libraries to convergence proofs. Revising a model to restore provability can change the mathematical claim. We introduce ProofLoom, a fully automated LLM-agent system for Proof-Obligation-Driven Theory Construction. Given a published algorithm, target theorem, and source proof, ProofLoom autonomously constructs the Lean model and supporting theory. Open proof obligations drive the development of definitions, interfaces, lemmas, and proof plans. Signature contracts record evidence and obligations for model revisions; an independent Judge rejects unsupported assumptions and weakened conclusions. Planner expands the published argument into intermediate claims, and Audit checks whether the Lean proof follows it. Across tasks, SOptLib accumulates verified mathematics and construction experience: reusable results are extracted, generalized, and verified, while modeling decisions and failed proof routes are recorded. Later tasks retrieve these results and records and contribute new developments, forming a cycle of construction, accumulation, and reuse. On fifteen textbook and research-paper tasks, ProofLoom obtains mean human ratings of 6.3/7 and 6.4/7, compared with 4.9/7 and 5.0/7 for the strongest of six baselines. Across 33 developments, it produces 490,693 lines of algorithm-local Lean code with no sorry. The formalizations also expose 28 incorrect formulas, proof gaps, and algorithm-analysis mismatches in published sources across 22 developments, each with checked evidence.
• Abstract（参考訳）: リーンにおける研究レベルの確率的最適化の形式化には、アルゴリズムモデルと、基礎ライブラリと収束証明を結合するドメイン理論の両方が必要です。 改善性を取り戻すためのモデルを修正することは、数学的クレームを変えることができる。 本稿では,ProofLoomを紹介した。Proof-Obligation-Driven Theory Constructionのための,完全に自動化されたLLMエージェントシステムである。 ProofLoomは、公開されたアルゴリズム、ターゲット定理、およびソース証明を与えられた後、リーンモデルとサポート理論を自律的に構築する。 オープンな証明義務は、定義、インターフェース、補題、証明計画の開発を促進する。 署名契約は、モデル修正の証拠と義務を記録する。 Planner氏は公表された議論を中間的な主張に拡張し、Audit氏はリーンの証明がそれに従うかどうかをチェックする。 再利用可能な結果が抽出され、一般化され、検証され、モデリング決定と失敗する証明経路が記録される。 その後のタスクは、これらの結果と記録を取得し、新しい開発に貢献し、建設、蓄積、再利用のサイクルを形成する。 15の教科書と研究論文のタスクで、ProofLoomは6.3/7と6.4/7の平均人間格付けを6つのベースラインで最強の4.9/7と5.0/7と比較する。 33の開発で、490,693行のアルゴリズムローカルなリーンコードを生成する。 公式化はまた、22の展開にまたがって、28の不正な公式、証明のギャップ、アルゴリズム分析のミスマッチを公開し、それぞれがチェックされた証拠を持っている。

関連論文リスト

• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
  LLMは難解な解答作業に対処できるが、幻覚や不可解なステップの誤りを生じやすい。 創造性と数学的厳密性の両方を保ちながら、どのように解答-構成問題を解決するか? 本稿では,パターン駆動型推論と形式的定理証明を統合したニューロシンボリックな手法であるLLM-Conjecture-Prove(ECP)フレームワークを紹介する。 ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、公式な数学的推論を前進させる可能性を示している。
  論文  参考訳（メタデータ） (2025-05-24T03:52:25Z)
• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
  我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。 我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。 この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
  論文  参考訳（メタデータ） (2025-02-16T06:20:39Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)

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

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