論文の概要: Reap: Uncovering Monte Carlo proof search with a lightweight model
- arxiv url: http://arxiv.org/abs/2611.02678v1
- Date: Mon, 02 Nov 2026 07:33:28 GMT
- ステータス: 情報取得中
- システム内更新日: 2026-11-03 19:54:41.374433
- Title: Reap: Uncovering Monte Carlo proof search with a lightweight model
- Title（参考訳）: モンテカルロの証明を軽量モデルで発見
- Abstract要約: Reapは、Lean4でポリシーに価値のあるMonte Carlo Tree Searchを直接実装している。
政策価値モデルであるReaper-1を、継続事前学習、教師付き戦術学習、反復探索に基づく強化学習を通じて訓練する。
最終システムは、pass@32でのminiF2F-testの79.9%を解決し、同等サイズのオープンプロデューサ間の最先端のパフォーマンスを確立する。
- 参考スコア（独自算出の注目度）: 13.056755987121308
- License:
- Abstract: We present Reap, an open framework for learning and analyzing formal proof search in Lean4. Reap implements policy-value-guided Monte Carlo Tree Search directly in Lean, sharing proof-state transitions, AND-OR search, and replay verification between inference and training rollouts. Structured action logs expose how neural predictions and tactic execution interact during search. Using this framework, we train Reaper-1, a 1.7B-parameter policy-value model, through continued pre-training, supervised tactic learning, and iterative search-based reinforcement learning. Using a separate premise selector, the final system solves 79.9% of miniF2F-test at pass@32, establishing state-of-the-art performance among open provers of comparable size while remaining competitive with substantially larger models. Beyond improved solve rates, our results suggest that RL strengthens the prover's ability to organize proofs around useful intermediate results, favoring substantial advances over repeated local adjustments. This more directed proof construction is accompanied by increasingly elaborate tactic programs: fewer explicit search decisions are needed, while more work is performed within each decision. The resulting trade-off between search effort and tactic execution cost provides insight into how learning changes the prover's problem-solving strategy.
- Abstract（参考訳）: Lean4で公式な証明検索を学習し分析するためのオープンなフレームワークであるReapを紹介します。
Reapは、ポリシーに価値を付与されたMonte Carlo Tree Searchを直接リーンで実装し、証明状態遷移を共有し、AND-OR検索を行い、推論とトレーニングのロールアウト間の検証をリプレイする。
構造化されたアクションログは、検索中に神経予測と戦術実行がどのように相互作用するかを明らかにする。
このフレームワークを用いて、継続事前学習、教師付き戦術学習、反復探索に基づく強化学習を通じて、1.7Bパラメータポリシー値モデルであるReaper-1を訓練する。
異なる前提セレクタを使用して、最終システムはpass@32でminiF2F-testの79.9%を解決し、相当サイズのオープンプロバーの間で最先端のパフォーマンスを確立しながら、かなり大きなモデルと競合する。
以上の結果から,RLは有効な中間結果に関する証明を整理する能力を強化し,局所的な調整の繰り返しよりもかなりの進歩を期待できることが示された。
このより指示された証明構築には、より精巧な戦術プログラムが伴う。
探索努力と戦術実行コストのトレードオフによって、学習が証明者の問題解決戦略をどのように変えるかが分かる。
関連論文リスト
- Retrieval, Reward, and Training Protocols: What Matters in Training Search Agents? [15.605151408619895]
本稿では,探索エージェント訓練の3つの未探索次元を分離する制御的実証的研究について述べる。
まず、広く使われているWikipedia 2018コーパスにおける重要なデータカバレッジの問題を特定し、それを修正するだけで、トレーニングアルゴリズムの違いよりも大きな利益が得られることを示す。
第2に、結果に基づく報酬法とプロセスに基づく報酬法を3つのベースモデルで体系的に比較し、最も単純な結果に基づくアプローチが、ほとんどの設定において、競争力や優れたパフォーマンスを達成することを発見した。
第三に、トレーニングデータの多様性、非政治データ利用、検索予算のスケーリングを分析し、効果的な検索エージェントの訓練のための実践的ガイドラインを精査する。
論文 参考訳（メタデータ） (2026-05-27T03:04:36Z) - CoSearch: Joint Training of Reasoning and Document Ranking via Reinforcement Learning for Agentic Search [51.911048955965136]
CoSearchは多段階推論エージェントと生成ドキュメントランキングモデルを共同でトレーニングするフレームワークである。
この結果から, 推論エージェントと検索システムの協調訓練は, 実現可能であり, 性能も高いことが示唆された。
論文 参考訳（メタデータ） (2026-04-19T17:48:17Z) - PRAISE: Prefix-Based Rollout Reuse in Agentic Search Training [28.912613644535668]
本稿では,エージェント検索訓練におけるデータ効率向上のためのフレームワークPRAISEを提案する。
本手法は,検索ポリシー学習とプレフィックス応答評価の両方に,単一の共有モデルを用いる。
マルチホップQAベンチマークの実験では、PRAISEは強いベースラインよりも一貫してパフォーマンスを改善している。
論文 参考訳（メタデータ） (2026-04-04T10:23:46Z) - OThink-SRR1: Search, Refine and Reasoning with Reinforced Learning for Large Language Models [27.82040547996176]
OThink-SRR1は、強化学習を通じてトレーニングされた反復的なサーチ-リファイン-推論プロセスで大きなモデルを強化するフレームワークである。
その中核となるRefineステージは、回収された文書を推論する前に簡潔で関連する事実に蒸留する。
4つのマルチホップQAベンチマーク実験により,提案手法はより少ない検索ステップとトークンを用いながら,強いベースラインよりも優れた精度が得られることが示された。
論文 参考訳（メタデータ） (2026-03-27T03:06:29Z) - Thinking Forward and Backward: Multi-Objective Reinforcement Learning for Retrieval-Augmented Reasoning [137.33138614095435]
Retrieval-augmented Generation (RAG) は、大規模言語モデルにおける幻覚の緩和に有効であることが証明されている。
近年、検索に基づく対話をRAGに組み込んで、リアルタイム検索による反復推論を可能にしている。
提案するBi-RARは,各中間ステップを前方方向と後方方向の両方で共同で評価する,新たな検索拡張推論フレームワークである。
論文 参考訳（メタデータ） (2025-11-12T08:29:39Z) - VAR: Visual Attention Reasoning via Structured Search and Backtracking [49.427842994857635]
構造化された検索としてグラウンドド推論をリキャストするフレームワークであるVisual Attention Reasoningを紹介する。
VARは、推論プロセスを2つの重要な段階に分解する。
我々は、我々の7BモデルであるVAR-7Bが、幻覚と安全性のベンチマークの包括的なスイートに新しい最先端を設定していることを示します。
論文 参考訳（メタデータ） (2025-10-21T13:18:44Z) - Walk Before You Run! Concise LLM Reasoning via Reinforcement Learning [10.255235456427037]
大規模言語モデル(LLM)における簡潔推論を実現するための簡易かつ効果的な2段階強化学習フレームワークを提案する。
最初の段階は、より多くのトレーニングステップを使用して、グループ相対ポリシー最適化を通じてモデルの推論能力をインセンティブ化することを目的としています。
第2段階は、より少ないトレーニングステップを使用して、簡潔さを明示的に実施し、Longth-aware Group Relative Policy Optimizationを通じて効率を向上させる。
論文 参考訳（メタデータ） (2025-05-27T13:29:51Z) - SEM: Reinforcement Learning for Search-Efficient Large Language Models [26.075903427834838]
大きな言語モデル(LLM)は、推論だけでなく、外部ツールの呼び出しでもその能力を実証している。
既存の強化学習アプローチは、しばしば冗長な探索行動を引き起こす。
本研究では,学習後強化学習フレームワークであるSEMを提案する。
論文 参考訳（メタデータ） (2025-05-12T09:45:40Z) - ReSearch: Learning to Reason with Search for LLMs via Reinforcement Learning [74.65632662894086]
本稿では,強化学習を通じてLLMをReason with Searchに学習するフレームワークであるReSearchを提案する。
提案手法では,検索操作を推論チェーンの不可欠な要素として扱う。
分析によると、ReSearchは自然にリフレクションや自己訂正のような高度な推論機能を引き出す。
論文 参考訳（メタデータ） (2025-03-25T09:00:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。