論文の概要: Process-Verified Reinforcement Learning for Theorem Proving via Lean

• arxiv url: http://arxiv.org/abs/2606.20068v1
• Date: Thu, 18 Jun 2026 10:40:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-19 18:23:39.802227
• Title: Process-Verified Reinforcement Learning for Theorem Proving via Lean
• Title（参考訳）: リーンによる定理証明のためのプロセス検証強化学習
• Authors: Minsu Kim, Se-Young Yun,
• Abstract要約: リーン証明アシスタント自体が、象徴的なプロセスのオラクルとして機能できることを示します。 LeanLeanとDeepSeek-V1.5の実験によると、戦術レベルの監視は、ほとんどの設定で結果のみのベースラインを上回っている。
• 参考スコア（独自算出の注目度）: 47.294932573003756
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While reinforcement learning from verifiable rewards (RLVR) typically has relied on a single binary verification signal, symbolic proof assistants in formal reasoning offer rich, fine-grained structured feedback. This gap between structured processes and unstructured rewards highlights the importance of feedback that is both dense and sound. In this work, we demonstrate that the Lean proof assistant itself can serve as a symbolic process oracle, supplying both outcome-level and fine-grained tactic-level verified feedback during training. Proof attempts are parsed into tactic sequences, and Lean's elaboration marks both locally sound steps and the earliest failing step, yielding dense, verifier-grounded credit signals rooted in type theory. We incorporate these structured rewards into a GRPO-style reinforcement learning objective with first-error propagation and first-token credit methods that balances outcome- and process-level advantages. Experiments with STP-Lean and DeepSeek-Prover-V1.5 show that tactic-level supervision outperforms outcome-only baselines in most settings, delivering improvements on benchmarks such as MiniF2F and ProofNet. Beyond empirical gains, our study highlights a broader perspective: symbolic proof assistants are not only verifiers at evaluation time, but can also act as process-level reward oracles during training. This opens a path toward reinforcement learning frameworks that combine the scalability of language models with the reliability of symbolic verification for formal reasoning.
• Abstract（参考訳）: 検証可能な報酬(RLVR)からの強化学習は、通常、単一のバイナリ検証信号に依存するが、形式的推論における記号的証明アシスタントは、リッチできめ細かい構造化されたフィードバックを提供する。 構造化プロセスと非構造化報酬の間のこのギャップは、密度と音の両方のフィードバックの重要性を強調します。 この研究では、リーン証明アシスタント自体が、トレーニング中に結果レベルと詳細な戦術レベルの両方を検証したフィードバックを提供する、象徴的なプロセスのオラクルとして機能できることを実証します。 証明の試みは戦術的な順序に解析され、リーンの発見は局所的な音のステップと最も初期の失敗のステップの両方を示し、型理論に根ざした密集した検証済みの信用信号を生み出す。 我々は、これらの構造化報酬を、第1次エラー伝播と結果とプロセスレベルの利点のバランスをとる第1次クレジット手法を備えたGRPO型強化学習目標に組み込む。 STP-LeanとDeepSeek-Prover-V1.5の実験によると、戦術レベルの監視は、ほとんどの設定において結果のみのベースラインよりも優れており、MiniF2FやProofNetなどのベンチマークで改善されている。 象徴的証明アシスタントは、評価時に検証者であるだけでなく、トレーニング中にプロセスレベルの報酬オーラクルとして機能する。 これは、言語モデルのスケーラビリティと、形式的推論のための記号的検証の信頼性を組み合わせた強化学習フレームワークへの道を開く。

関連論文リスト

• Verifiable Process Rewards for Agentic Reasoning [21.195739597726142]
  検証可能な報酬(RLVR)による強化学習は、大規模言語モデル(LLM)の推論能力を向上させる。 既存のアプローチのほとんどは、少ない結果レベルのフィードバックに依存しています。 本稿では,これらのオーラクルを強化学習のための高密度なターンレベルの監視に変換するフレームワークであるVerifiable Process Rewards (VPR)を提案する。
  論文  参考訳（メタデータ） (2026-05-11T10:30:53Z)
• Discovering Process-Outcome Credit in Multi-Step LLM Reasoning [3.584086358722852]
  強化学習(RL)は、大規模言語モデル(LLM)における推論能力を高めるための強力なパラダイムとして機能する。 本稿では,連続的な報酬信号を提供するための新しいフレームワークを提案する。 本モデルでは, 予測できない, 難解な推論タスクに対して, ゼロショット転送能力を実証し, より優れた配当性を示す。
  論文  参考訳（メタデータ） (2026-02-01T05:44:09Z)
• Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
  本稿では,Refinement Provenance Inference (RPI)監査タスクをRefinement Provenance Inference (RPI)として定式化する。 本稿では,ロジットレベルの信号で教師が強制する可能性機能を融合させるロジットベースのフレームワークであるReProを提案する。 トレーニング中、ReProはシャドウファインチューニングを通じて転送可能な表現を学び、訓練データアクセスなしで、見えない犠牲者の証明を推測するために軽量のリニアヘッドを使用する。
  論文  参考訳（メタデータ） (2026-01-05T10:16:41Z)
• Look As You Think: Unifying Reasoning and Visual Evidence Attribution for Verifiable Document RAG via Reinforcement Learning [55.232400251303794]
  Look As You Think (LAT)は、モデルをトレーニングし、一貫した帰属性を持った検証可能な推論パスを生成するための強化学習フレームワークである。 LATはシングルイメージとマルチイメージの両方でバニラモデルを一貫して改善し、平均ゲインは8.23%、IoU@0.5では47.0%となる。
  論文  参考訳（メタデータ） (2025-11-15T02:50:23Z)
• Veri-R1: Toward Precise and Faithful Claim Verification via Online Reinforcement Learning [53.05161493434908]
  大規模言語モデル(LLM)によるクレーム検証は、その強力な推論能力と透過的な検証プロセスのため、近年注目を集めている。 我々は、LLMが検索エンジンと対話し、その計画、検索、推論行動を明確に形作る報酬信号を受け取ることができるオンライン強化学習フレームワークであるVeri-R1を紹介した。 実験の結果、Veri-R1は最大30%の精度で関節の精度を向上し、エビデンススコアを2倍にし、より大きなモデルを上回ることが示されている。
  論文  参考訳（メタデータ） (2025-10-02T11:49:48Z)
• Learning a Dense Reasoning Reward Model from Expert Demonstration via Inverse Reinforcement Learning [50.20267980386502]
  我々は、専門家によるデモンストレーションから直接、プロセスの監督のための密集したトークンレベルの報酬モデルを学びます。 学習された推論報酬は、2つの補完的な役割を果たす: (i)訓練中の推論ポリシーを最適化するためのステップレベルのフィードバックを提供する。
  論文  参考訳（メタデータ） (2025-10-02T09:55:26Z)
• AURORA: Augmented Understanding via Structured Reasoning and Reinforcement Learning for Reference Audio-Visual Segmentation [113.75682363364004]
  AURORAは、参照音声視覚セグメント化における真の推論と言語理解を強化するために設計されたフレームワークである。 AURORAはRef-AVSベンチマークの最先端性能を達成し、非参照セグメンテーションに効果的に一般化する。
  論文  参考訳（メタデータ） (2025-08-04T07:47:38Z)
• Reinfier and Reintrainer: Verification and Interpretation-Driven Safe Deep Reinforcement Learning Frameworks [36.730973051834376]
  本稿では,信頼性の高いDRLモデルを開発するために,検証駆動型ループ内解釈フレームワークReintrainerを提案する。 各イテレーションにおいて、このフレームワークは、トレーニング中のモデルと事前定義されたプロパティの間のギャップをフォーマルな検証を使って測定する。 Reinfierは、簡潔な制約エンコーディング言語DRLPに関連する、ブレークポイント検索と検証駆動型解釈を備えている。
  論文  参考訳（メタデータ） (2024-10-19T15:03:26Z)

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

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