論文の概要: Solving Formal Math Problems by Decomposition and Iterative Reflection

• arxiv url: http://arxiv.org/abs/2507.15225v1
• Date: Mon, 21 Jul 2025 03:56:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-22 20:51:32.248814
• Title: Solving Formal Math Problems by Decomposition and Iterative Reflection
• Title（参考訳）: 分解と反復反射による形式数学問題の解法
• Authors: Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, Haocheng Wang, Luong Trung, Rong Ye, Phan Nhat Hoang, Huishuai Zhang, Peng Sun, Hang Li,
• Abstract要約: textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
• 参考スコア（独自算出の注目度）: 30.54275542622631
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: General-purpose Large Language Models (LLMs) have achieved remarkable success in intelligence, performing comparably to human experts on complex reasoning tasks such as coding and mathematical reasoning. However, generating formal proofs in specialized languages like Lean 4 remains a significant challenge for these models, limiting their application in complex theorem proving and automated verification. Current approaches typically require specializing models through fine-tuning on dedicated formal corpora, incurring high costs for data collection and training. In this work, we introduce \textbf{Delta Prover}, an agent-based framework that orchestrates the interaction between a general-purpose LLM and the Lean 4 proof environment. Delta Prover leverages the reflection and reasoning capabilities of general-purpose LLMs to interactively construct formal proofs in Lean 4, circumventing the need for model specialization. At its core, the agent integrates two novel, interdependent components: an algorithmic framework for reflective decomposition and iterative proof repair, and a custom Domain-Specific Language (DSL) built upon Lean 4 for streamlined subproblem management. \textbf{Delta Prover achieves a state-of-the-art 95.9\% success rate on the miniF2F-test benchmark, surpassing all existing approaches, including those requiring model specialization.} Furthermore, Delta Prover exhibits a significantly stronger test-time scaling law compared to standard Best-of-N proof strategies. Crucially, our findings demonstrate that general-purpose LLMs, when guided by an effective agentic structure, possess substantial untapped theorem-proving capabilities. This presents a computationally efficient alternative to specialized models for robust automated reasoning in formal environments.
• Abstract（参考訳）: 汎用大規模言語モデル(LLM)は、コーディングや数学的推論といった複雑な推論タスクにおいて、人間の専門家と相容れない性能を発揮した。 しかしながら、Lean 4のような専門言語で形式的な証明を生成することは、これらのモデルにとって重要な課題であり、複雑な定理の証明と自動検証の応用を制限する。 現在のアプローチでは、データ収集とトレーニングのコストが高くなるため、専用の形式コーパスを微調整することでモデルを専門化する必要がある。 本稿では,汎用LLMとLean 4の実証環境とのインタラクションをオーケストレーションするエージェントベースのフレームワークである,‘textbf{Delta Prover}’を紹介する。 Delta Proverは、汎用LLMのリフレクションと推論機能を活用して、Lean 4で形式的な証明を対話的に構築する。 その中核となるのは、リフレクティブ分解と反復的証明修復のためのアルゴリズムフレームワークと、リーン4に基づいて構築された、サブプロブレム管理の合理化のためのカスタムドメイン特化言語(DSL)である。 \textbf{Delta Prover は miniF2F-test ベンチマークで 95.9 % の成功率を達成した。 さらに、Delta Proverは標準的なBest-of-N証明戦略に比べて、テスト時間スケーリングの法則がかなり強い。 本研究は, 汎用LSMが有効なエージェント構造で導かれると, 未解決の定理証明能力を有することを示した。 これは、フォーマルな環境での堅牢な自動推論のための特殊モデルに代わる計算効率の良い代替となる。

関連論文リスト

• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• ProofCompass: Enhancing Specialized Provers with LLM Guidance [6.757964026033364]
  本稿では,計算効率を向上する新しいハイブリッド手法であるProofを紹介する。 DeepSeek-Prover-v1.5-RL (DSP-v1.5) のような既存の特殊な証明手法をLLM (Large Language Model) で戦略的にガイドする。 miniF2F ベンチマークでは、Proof は DSP-v1.5 (54.9% rightarrow 55.3%$) を上回っ、25 個の試行 (3200 rightarrow 128$) を使用する。
  論文  参考訳（メタデータ） (2025-07-18T19:28:01Z)
• ProtoReasoning: Prototypes as the Foundation for Generalizable Reasoning in LLMs [54.154593699263074]
  ProtoReasoningは、大規模推論モデルの推論能力を高めるフレームワークである。 ProtoReasoningは問題を対応するプロトタイプ表現に変換する。 ProtoReasoningは論理的推論に基づくベースラインモデルよりも4.7%改善されている。
  論文  参考訳（メタデータ） (2025-06-18T07:44:09Z)
• Teaching Large Language Models to Maintain Contextual Faithfulness via Synthetic Tasks and Reinforcement Learning [80.27561080938747]
  本研究では,人間のアノテーションを使わずに,大規模言語モデル(LLM)の短文および長文生成タスクにおける忠実度を改善するための体系的フレームワークであるCANOEを提案する。 また,ルールに基づく強化学習手法であるDual-GRPOを提案する。 実験結果から,CANOEは11の下流タスクにまたがるLLMの忠実度を大幅に向上し,最も先進的なLLMよりも優れていた。
  論文  参考訳（メタデータ） (2025-05-22T10:10:07Z)
• General-Reasoner: Advancing LLM Reasoning Across All Domains [64.70599911897595]
  強化学習(RL)は近年,大規模言語モデル(LLM)の推論能力の向上に強い可能性を示している。 本稿では,多分野にわたるLSM推論能力の向上を目的とした,新たなトレーニングパラダイムであるGeneral-Reasonerを提案する。 私たちは一連のモデルをトレーニングし、物理学、化学、金融、電子工学など幅広い分野をカバーする幅広いデータセットでそれらを評価します。
  論文  参考訳（メタデータ） (2025-05-20T17:41:33Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving [30.112351299773632]
  この問題を解決するために,我々はLean4定理の包括的なフレームワークを提案する。 一般的なNLの認識タスクを完全防御生成と証明修正のための誤り解析に分離する。 我々のフレームワークは、MiniF2F-TestデータセットのLean4バージョンにおいて**61.07%*の精度を達成する。
  論文  参考訳（メタデータ） (2025-03-05T05:50:31Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Reference Trustable Decoding: A Training-Free Augmentation Paradigm for Large Language Models [79.41139393080736]
  大規模言語モデル(LLM)は急速に進歩し、印象的な機能を示している。 In-Context Learning (ICL) など。 効率的なファインチューニング(PEFT)は、現在2つの主要な拡張方法である。 下流タスクへのLLM。 我々は、モデルが微調整なしで新しいタスクに迅速に適応できるパラダイムである参照信頼復号(RTD)を提案する。
  論文  参考訳（メタデータ） (2024-09-30T10:48:20Z)
• Improving Retrieval Augmented Language Model with Self-Reasoning [20.715106330314605]
  本稿では,ALMの信頼性とトレーサビリティ向上を目的とした,新たな自己推論フレームワークを提案する。 このフレームワークは、関連性を認識したプロセス、エビデンスを認識した選択プロセス、軌跡解析プロセスの3つのプロセスで自己推論軌道を構築することを含む。 提案手法の優位性を示すため,4つの公開データセットにまたがるフレームワークの評価を行った。
  論文  参考訳（メタデータ） (2024-07-29T09:05:10Z)
• Large Language Model Agent as a Mechanical Designer [7.136205674624813]
  本研究では、FEMモジュールと協調して事前訓練された大規模言語モデル(LLM)を利用して、構造設計を自律的に生成、評価、洗練するフレームワークを提案する。 LLMはドメイン固有の微調整なしで動作し、設計候補を提案し、FEMから派生した性能指標を解釈し、構造的な音響修正を適用する。 NSGA-II (Non-Sorting Genetic Algorithm II) と比較して,本手法はより高速に収束し,より少ないFEM評価を実現する。
  論文  参考訳（メタデータ） (2024-04-26T16:41:24Z)

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

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