論文の概要: StepFun-Prover Preview: Let's Think and Verify Step by Step
- arxiv url: http://arxiv.org/abs/2507.20199v1
- Date: Sun, 27 Jul 2025 09:38:32 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-29 16:23:57.260777
- Title: StepFun-Prover Preview: Let's Think and Verify Step by Step
- Title（参考訳）: StepFun-Proverのプレビュー: ステップバイステップの検証と検討
- Authors: Shijie Shang, Ruosi Wan, Yue Peng, Yutong Wu, Xiong-hui Chen, Jie Yan, Xiangyu Zhang,
- Abstract要約: 本稿では,ツール統合推論による形式定理証明のための大規模言語モデルであるStepFun-Prover Previewを提案する。
提案手法は,実時間環境フィードバックに基づく証明を反復的に精錬することにより,人間的な問題解決戦略をエミュレートすることを可能にする。
miniF2F-testベンチマークでは、StepFun-Proverがパス@1成功率70.0%$を達成した。
- 参考スコア（独自算出の注目度）: 14.896796588073725
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: We present StepFun-Prover Preview, a large language model designed for formal theorem proving through tool-integrated reasoning. Using a reinforcement learning pipeline that incorporates tool-based interactions, StepFun-Prover can achieve strong performance in generating Lean 4 proofs with minimal sampling. Our approach enables the model to emulate human-like problem-solving strategies by iteratively refining proofs based on real-time environment feedback. On the miniF2F-test benchmark, StepFun-Prover achieves a pass@1 success rate of $70.0\%$. Beyond advancing benchmark performance, we introduce an end-to-end training framework for developing tool-integrated reasoning models, offering a promising direction for automated theorem proving and Math AI assistant.
- Abstract（参考訳）: 本稿では,ツール統合推論による形式定理証明のための大規模言語モデルであるStepFun-Prover Previewを提案する。
ツールベースのインタラクションを組み込んだ強化学習パイプラインを使用することで、StepFun-Proverは、最小限のサンプリングでLean 4の証明を生成する上で、強力なパフォーマンスを実現することができる。
提案手法は,実時間環境フィードバックに基づく証明を反復的に精錬することにより,人間的な問題解決戦略をエミュレートすることを可能にする。
miniF2F-testベンチマークでは、StepFun-Proverがパス@1成功率70.0\%$を達成した。
ベンチマークパフォーマンスの向上に加えて、ツール統合推論モデルを開発するためのエンドツーエンドのトレーニングフレームワークを導入し、自動定理証明とMath AIアシスタントのための有望な方向性を提供します。
関連論文リスト
- Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning [38.4246156415702]
Kimina-Proverは、形式的定理証明のための新しい推論駆動探索パラダイムを開拓した大きな言語モデルである。
Qwen2.5-72Bから大規模な強化学習パイプラインでトレーニングされたKimina-Proverは、Lean 4の証明生成において、強力なパフォーマンスを示している。
Kimina-Prover は miniF2F ベンチマークに新しい最先端をセットし、pass@8192 で 80.7% に達した。
論文 参考訳（メタデータ） (2025-04-15T16:23:44Z) - R1-VL: Learning to Reason with Multimodal Large Language Models via Step-wise Group Relative Policy Optimization [86.32257216965229]
そこで本稿では,MLLMの自己改善を支援するオンライン強化学習フレームワークを提案する。
StepGRPOは、Step-wise Reasoning Accuracy Reward (StepRAR)とStep-wise Reasoning Validity Reward (StepRVR)の2つの新しいルールベースの推論報酬を導入した。
提案するStepGRPOでは,ステップバイステップ推論に優れた機能を持つMLLMのシリーズであるR1-VLを紹介する。
論文 参考訳（メタデータ） (2025-03-17T08:51:44Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - AdaptiveStep: Automatically Dividing Reasoning Step through Model Confidence [29.551802573731305]
本稿では,モデルが次の単語を予測する自信に基づいて推論ステップを分割する手法であるAdaptiveStepを提案する。
数理推論およびコード生成タスクにおいて,AdaptiveStep-trained PRMを用いた実験により実効性を示す。
論文 参考訳（メタデータ） (2025-02-19T18:35:55Z) - BRiTE: Bootstrapping Reinforced Thinking Process to Enhance Language Model Reasoning [78.63421517563056]
大規模言語モデル(LLM)は複雑な推論タスクにおいて顕著な機能を示した。
本稿では,新しいグラフィカルモデルを用いてLLM推論を定式化する統一確率的フレームワークを提案する。
本稿では,Bootstrapping Reinforced Thinking Process (BRiTE)アルゴリズムについて述べる。
論文 参考訳（メタデータ） (2025-01-31T02:39:07Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - Step-KTO: Optimizing Mathematical Reasoning through Stepwise Binary Feedback [94.25162866972077]
Step-KTOは、プロセスレベルと結果レベルのバイナリフィードバックを組み合わせたトレーニングフレームワークである。
実験の結果,Step-KTOは最終回答の精度と中間推論の質の両方を著しく向上させることがわかった。
論文 参考訳（メタデータ） (2025-01-18T15:38:03Z) - Enhancing Deployment-Time Predictive Model Robustness for Code Analysis and Optimization [4.374023944113174]
本稿では,予測モデルの堅牢性と性能を高めるオープンソースライブラリであるPromを紹介する。
Promは、統計的アセスメントを使用して、誤った予測をしがちなテストサンプルを識別する。
評価の結果,Promは平均96%(最大100%)の誤予測を識別できることがわかった。
論文 参考訳（メタデータ） (2024-12-31T06:17:03Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Let's reward step by step: Step-Level reward model as the Navigators for
Reasoning [64.27898739929734]
Process-Supervised Reward Model (PRM)は、トレーニングフェーズ中にステップバイステップのフィードバックをLLMに提供する。
LLMの探索経路を最適化するために,PRMからのステップレベルのフィードバックを応用した欲求探索アルゴリズムを提案する。
提案手法の汎用性を探るため,コーディングタスクのステップレベル報酬データセットを自動生成する手法を開発し,コード生成タスクにおける同様の性能向上を観察する。
論文 参考訳（メタデータ） (2023-10-16T05:21:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。