Fugu-MT 論文翻訳(概要): Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving

論文の概要: Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving

arxiv url: http://arxiv.org/abs/2605.11905v1
Date: Tue, 12 May 2026 10:18:28 GMT
ステータス: 翻訳完了
システム内更新日: 2026-05-13 21:48:56.791623
Title: Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving
Title（参考訳）: スーパービジョンの粒度を再考する: LLMに基づく理論証明のためのセグメントレベル学習
Authors: Shuo Xu, Jiakun Zhang, Junyu Lai, Chun Cao, Jingwei Xu,
Abstract要約: リーン4における大きな言語モデルで証明された自動定理は、一般的に、木探索によるステップレベルの戦術予測と、全体的な防御生成を通じてアプローチされる。これら2つのパラダイムは、教師付きトレーニングデータを構築するための反対の粒度を表す。本稿では,訓練方針モデルのための局所的コヒーレントな証明セグメントを抽出する訓練データ構築戦略であるセグメントレベルの監視を提案する。
参考スコア（独自算出の注目度）: 8.420305724549603
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Automated theorem proving with large language models in Lean 4 is commonly approached through either step-level tactic prediction with tree search or whole-proof generation. These two paradigms represent opposite granularities for constructing supervised training data: the former provides dense local signals but may fragment coherent proof processes, while the latter preserves global structure but requires complex end-to-end generation. In this paper, we revisit supervision granularity as a training set construction problem over proof trajectories and propose segment-level supervision, a training data construction strategy that extracts locally coherent proof segments for training policy models. We further reuse the same strategy at inference time to trigger short rollouts for existing step-level models. When trained with segment-level supervision on STP, LeanWorkbook, and NuminaMath-LEAN, the resulting policy models achieve proof success rates of 64.84%, 60.90%, and 66.31% on miniF2F, respectively, consistently outperforming both step-level and whole-proof baselines. Goal-aware rollout further improves existing step-level provers while reducing inference costs. It increases the proof success rate of BFS-Prover-V2-7B from 68.77% to 70.74% and that of InternLM2.5-StepProver from 59.59% to 60.33%, showing that appropriate supervision granularity better aligns model learning with proof structure and search. Code and models are available at https://github.com/NJUDeepEngine/SEG-ATP.
Abstract（参考訳）: リーン4における大きな言語モデルで証明された自動定理は、一般的に、木探索によるステップレベルの戦術予測と、全体的な防御生成を通じてアプローチされる。これらの2つのパラダイムは、教師付きトレーニングデータを構築するための反対の粒度を表しており、前者は密集した局所信号を提供するが、後者はグローバルな構造を保ちながら複雑なエンドツーエンド生成を必要とする。本稿では,実証軌道上での訓練セット構築問題としての監督的粒度を再考し,訓練方針モデルのための局所的一貫性のある証明セグメントを抽出する訓練データ構築戦略であるセグメントレベルの監督手法を提案する。さらに、推論時に同じ戦略を再利用して、既存のステップレベルのモデルに対する短いロールアウトをトリガーします。 STP、LeanWorkbook、NuminaMath-LEANのセグメンテーションレベルの監督で訓練された結果、それぞれが64.84%、60.90%、66.31%の証明成功率を達成した。ゴール対応ロールアウトは、推論コストを削減しつつ、既存のステップレベルのプロバーをさらに改善する。 BFS-Prover-V2-7Bの証明成功率は68.77%から70.74%に増加し、InternLM2.5-StepProverは59.59%から60.33%に増加した。コードとモデルはhttps://github.com/NJUDeepEngine/SEG-ATPで入手できる。

関連論文リスト

GRPO-VPS: Enhancing Group Relative Policy Optimization with Verifiable Process Supervision for Effective Reasoning [48.32628338889922]
グループ相対政策最適化は中間段階の無差別な信用割当に苦しむ。モデルフリーで検証可能なプロセス監視を,モデルが正しい回答を信じているかどうかを判断することによって導入する。このアプローチにより、よりターゲット的でサンプル効率の良いポリシー更新が可能になる。
論文参考訳（メタデータ） (2026-04-22T15:08:58Z)
Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification [34.98335927187393]
大規模言語モデル(LLM)は可塑性コードを生成することができるが、正確性には限界がある。本稿では,Lean4における自動コード検証のための階層的証明検索フレームワークを提案する。 Goedel-Code-Prover-8Bは、分解と完了の両方のための単一の統一ポリシーです。
論文参考訳（メタデータ） (2026-03-18T18:42:04Z)
ProRAG: Process-Supervised Reinforcement Learning for Retrieval-Augmented Generation [54.071574153853994]
ProRAGは、学習段階の監視をオンライン最適化ループに統合するために設計されたプロセス教師付き強化学習フレームワークである。本フレームワークは,(1)構造化推論形式でモデルを初期化するための監視されたポリシーワームアップ,(2)中間推論品質を定量化するためのMCTSベースのプロセスリワードモデル(PRM)の構築,(3)細粒度プロセスの好みに合わせてポリシーを調整するためのPRM誘導推論リファインメント,(4)プロセススーパービジョン強化学習と2つのグラニュラリティー・アドバンテージ・メカニズムの4段階から構成される。
論文参考訳（メタデータ） (2026-01-29T16:04:59Z)
DiRL: An Efficient Post-Training Framework for Diffusion Language Models [54.405206032785706]
Diffusion Language Models (dLLMs) はAuto-Regressive(AR)モデルに代わる有望な代替品として登場した。既存の手法は、訓練と推論の間の計算の非効率性と客観的なミスマッチに悩まされている。我々は,FlexAttention-accelerated blockwise trainingとLMDeploy-timized inferenceを密接に統合した,効率的なポストトレーニングフレームワークであるDiRLを紹介した。
論文参考訳（メタデータ） (2025-12-23T08:33:19Z)
SPARK: Stepwise Process-Aware Rewards for Reference-Free Reinforcement Learning [39.1720897614261]
密度の高いステップレベルのフィードバックを提供するプロセス報酬モデル(PRM)は、強化学習の可能性を示している。筆者らはSPARK(SPARK)という3段階のフレームワークを提案し、第1段階ではジェネレータモデルが多様な解を生成し、検証器モデルがそれらを評価する。ステップレベルで複数の独立した検証を集約することで、根底的な結果管理を超越したプロセス報酬モデルのトレーニングデータが得られることを示す。
論文参考訳（メタデータ） (2025-12-02T21:30:47Z)
CLGRPO: Reasoning Ability Enhancement for Small VLMs [4.551310348498266]
SVLM(Small Vision Language Models)は、一般にパラメータサイズが2B未満のモデルを指す。本稿では,SVLMの推論能力を高めるために,インクリメンタルトレーニング戦略(Incrmental Training Strategy)と呼ばれるポストトレーニング後の最適化パラダイムを提案する。実験により,本手法は1B SVLMの推論能力を大幅に向上することが示された。
論文参考訳（メタデータ） (2025-06-22T14:32:15Z)
TemplateRL: Structured Template-Guided Reinforcement Learning for LLM Reasoning [56.250782426571526]
強化学習(Reinforcement Learning, RL)は, モデル推論の強化に有効なパラダイムとして登場した。本稿では、明示的なテンプレートガイダンスによってポリシー最適化を向上する構造化テンプレート誘導型RLフレームワークを提案する。提案手法はまず, MCTS を用いて小さなシードセット上に問題解決テンプレートライブラリを構築し, この高レベルの構造化ガイダンスを RL トレーニングにシームレスに統合する。
論文参考訳（メタデータ） (2025-05-21T16:06:10Z)
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)
Efficient Stagewise Pretraining via Progressive Subnetworks [53.00045381931778]
一般的な見方では、レイヤのドロップのような段階的なドロップ戦略は、スタック方式のアプローチと比べて効果がない。本稿では, 適切な設計で, 戦略の廃止は, 積み重ね手法よりも競争力があることを示すことによって, この概念に挑戦する。本稿では,各ステップでランダムサブネットワークのみを選択し,訓練し,段階的に拡大するランダムパートトレーニング(RAPTR)を提案する。
論文参考訳（メタデータ） (2024-02-08T18:49:09Z)

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

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