論文の概要: LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification

• arxiv url: http://arxiv.org/abs/2610.17697v1
• Date: Tue, 13 Oct 2026 04:23:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:15.505266
• Title: LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
• Title（参考訳）: LeanPRM: 自然言語証明のためのリーンを取り巻くプロセススーパービジョン
• Abstract要約: LeanPRMは、Leanの証明アシスタントを使用して、自然言語の証明のためのステップレベルのラベルを作成するフレームワークです。 LeanPRMでトレーニングされたQwen3-4B検証器は、同じベースモデルがRM800Kでトレーニングされた場合の60.3とは対照的に、48.2から74.7までの200の証明の保持されたセットに対して正確なステップラベルの精度を上げる。
• 参考スコア（独自算出の注目度）: 12.305232086450287
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI systems now write long and difficult mathematical proofs, and checking their step-by-step validity is becoming a bottleneck. A learned verifier could check proofs cheaply, but training one requires a correctness label on every step, and such labels are hard to obtain for open-ended proofs. Existing methods take them from human annotators, which is costly, or derive them from final answers, which proofs do not have, and formalizing each proof in Lean requires expert effort. We introduce LeanPRM, a framework that uses the Lean proof assistant to create step-level labels for natural-language proofs. A model writes a natural-language proof together with a paired formal proof, without feedback from Lean. Lean then labels every step, and a second model discards failures caused only by the formal syntax, so that the negative labels mark errors in the mathematics. LeanPRM contains 10,634 proofs with 152K labeled steps and no human annotation. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on a held-out set of 200 proofs (LeanPRM-Bench) from 48.2 to 74.7, as opposed to 60.3 when the same base model is trained on PRM800K. It also selects better proofs in best-of-N selection on IMO-level problems, and outperforms the PRM800K-trained verifier on three of four external verification benchmarks. Training on LeanPRM improves verifiers at every size from 0.6B to 8B parameters on LeanPRM-Bench, Hard2Verify and IMO-GradingBench. Given the labels need no human annotation, LeanPRM can grow with the supply of formal statements, offering a path to step-level feedback on AI-generated proofs that are hard for humans to check.
• Abstract（参考訳）: AIシステムは、長くて難しい数学的証明を記述し、ステップバイステップの妥当性をチェックすることがボトルネックになっている。 学習した検証者は、証明を安くチェックできるが、トレーニングするには各ステップに正当性ラベルが必要である。 既存のメソッドは、コストがかかる人間のアノテーションから、あるいは証明が持たない最終回答から、それらを取り除き、リーンでそれぞれの証明を形式化するには、専門家の努力が必要です。 LeanPRMは、Leanの証明アシスタントを使用して、自然言語の証明のためのステップレベルのラベルを作成するフレームワークです。 モデルは、リーンからのフィードバックなしに、自然言語による証明とペアの形式的な証明を書きます。 リーンはすべてのステップをラベル付けし、第二のモデルは形式的な構文によってのみ発生する失敗を捨て、負のラベルは数学の誤りを示す。 LeanPRMには10,634の証明と152Kのラベル付きステップがあり、人間のアノテーションはない。 LeanPRMでトレーニングされたQwen3-4B検証器は、同じベースモデルがPRM800Kでトレーニングされた場合の60.3に対して、200の証明(LeanPRM-Bench)の保持されたセット(LeanPRM-Bench)の正確なステップラベル精度を48.2から74.7に引き上げる。 また、IMOレベルの問題に対するNの最良の選択の証明も選択し、4つの外部検証ベンチマークのうち3つでPRM800Kで訓練された検証器よりも優れている。 LeanPRMのトレーニングでは,LeanPRM-Bench, Hard2Verify, IMO-GradingBenchの各サイズの検証項目が0.6Bから8Bに改善されている。 ラベルが人間のアノテーションを必要としないことを考えると、LeanPRMは形式的なステートメントの提供によって成長し、人間がチェックしづらいAI生成の証明に対するステップレベルのフィードバックを提供する。

関連論文リスト

• Pseudo-Formalization for Automatic Proof Verification [17.612188352560494]
  証明の信頼性検証は、厳密な数学的推論に基づくAIシステムのトレーニングと評価のボトルネックとして依然として残っている。 Pseudo-Formalization (PF) は形式的証明のモジュラリティと精度をキャプチャする証明形式である。 今後の研究を支援するため,研究レベルの検証ベンチマークArxivMathGradingBenchをリリースする。
  論文  参考訳（メタデータ） (2026-05-19T22:08:51Z)
• ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations [14.748476989228214]
  Proofrは、人間の監督を必要とせず、リーンの証明を単純化するために訓練された最初の言語モデルです。 Provrは専門家の反復と強化学習を通じてトレーニングされ、リーンを使って単純化の検証とトレーニング信号を提供する。 Provrは、最先端のRL訓練プローバーが標準ベンチマークで生成した証明を実質的に圧縮する。
  論文  参考訳（メタデータ） (2025-10-17T14:45:30Z)
• LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs [7.468772576199917]
  本稿では,Large Language Model(LLM)に基づく算数証明学習システムであるLeanTutorを紹介する。 LeanTutorは自然言語で学生と対話し、Leanで学生が書いた数学の証明を正式に検証し、次のステップを正しく生成し、適切な指導指導を提供する。 本システムを評価するために,自然数ゲームから派生した人文データセットであるPeanoBenchを紹介した。
  論文  参考訳（メタデータ） (2025-06-10T01:12:36Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems [0.0]
  リーンの残りのIMO問題に対する完全な、オリジナルの公式な証明を書いています。 この取り組みは,5,880行のリーン証明を作成することで,現在パブリックドメインにある証明の可用性を拡大するものだ。
  論文  参考訳（メタデータ） (2024-11-28T02:50:42Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)

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

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