論文の概要: FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models

• arxiv url: http://arxiv.org/abs/2605.10141v1
• Date: Mon, 11 May 2026 07:51:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-12 23:28:50.617887
• Title: FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
• Title（参考訳）: FormalRewardBench: 回帰モデルを証明する形式理論のベンチマーク
• Authors: Zeynel A. Uluşan, Burak S. Akbudak, Can S. Erer, Gözde Gül Şahin,
• Abstract要約: 我々はtextbfFormalRewardBenchを紹介します。これはLean 4.0で証明された形式的定理で報酬モデルを評価するための最初のベンチマークです。 その結果,フロンティア LLM は最高性能 (59.8%) を達成し,特殊定理証明器は最低性能 (24.4%) を達成した。 textbfFormalRewardBenchを公開し、形式数学における報酬モデルの開発についてさらなる研究を奨励する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent neural theorem provers use reinforcement learning with verifiable rewards (RLVR), where proof assistants provide binary correctness signals. While verifiable rewards are cheap and scalable without reward hacking issues, they suffer from sparse credit assignment: models receive no learning signal from difficult problems where partial progress goes unrewarded. This motivates learned reward models that can evaluate proof quality beyond binary verification. However, comparing reward models is challenging since it typically requires expensive RL training ablations. To address this, we introduce \textbf{FormalRewardBench}, the first benchmark for evaluating reward models in formal theorem proving with Lean 4. Our benchmark consists of 250 preference pairs where correct proofs are paired with incorrect variants generated through five expert curated error injection strategies: forced mistakes, minimal single-point variations, verbose incorrect proofs, natural language justification, and Python code injection. We evaluate frontier LLMs (e.g., Claude Opus 4.5), judge LLMs (e.g., CompassJudger-1-14B), general-purpose LLMs (e.g., Qwen2.5-72B-Instruct), and specialized theorem proving models (e.g., DeepSeek-Prover-V2-7B). Our results reveal that frontier LLMs achieve the highest performance (59.8\%) while specialized theorem provers perform the worst (24.4\%), suggesting that theorem proving ability does not transfer to proof evaluation. We provide further insights on various error injection mechanisms, highlighting the challenging nature of most injection mechanisms. We release \textbf{FormalRewardBench} publicly to encourage more research on developing reward models in formal mathematics.
• Abstract（参考訳）: 最近のニューラル定理証明者は、証明アシスタントが二項正当性信号を提供する検証可能な報酬(RLVR)を用いた強化学習を使用する。 検証可能な報酬は、ハッキングの問題なく安価でスケーラブルだが、十分なクレジットの割り当てに悩まされている。 これは、バイナリ検証を超えて証明品質を評価することができる、学習された報酬モデルへの動機付けである。 しかしながら、報酬モデルの比較は、通常、高価なRLトレーニングアブリケーションを必要とするため、難しい。 これを解決するために、私たちは、Lean 4.0で証明された形式的定理で報酬モデルを評価するための最初のベンチマークである \textbf{FormalRewardBench} を紹介します。 我々のベンチマークは250の選好ペアで構成されており、そこでは正しい証明が5つの専門家がキュレートしたエラーインジェクション戦略(強制ミス、最小限の単一ポイントのバリエーション、冗長な不正確な証明、自然言語の正当性、Pythonコードインジェクション)によって生成される誤った変種とペアリングされる。 我々は、フロンティア LLMs (e g , Claude Opus 4.5), judge LLMs (e g , CompassJudger-1-14B), general-purpose LLMs (e g , Qwen2.5-72B-Instruct), and special theorem proving model (e g , DeepSeek-Prover-V2-7B)を評価する。 その結果、フロンティア LLM は最高性能 (59.8 %) を達成する一方、特殊定理証明器は最悪の性能 (24.4 %) を達成し、定理証明能力が証明評価に移行しないことが示唆された。 我々は,多くのインジェクション機構の難易度を強調し,様々なエラーインジェクション機構に関するさらなる知見を提供する。 我々は、形式数学における報酬モデルの開発に関するさらなる研究を促進するために、公然と \textbf{FormalRewardBench} をリリースする。

関連論文リスト

• SPARK: Stepwise Process-Aware Rewards for Reference-Free Reinforcement Learning [39.1720897614261]
  密度の高いステップレベルのフィードバックを提供するプロセス報酬モデル(PRM)は、強化学習の可能性を示している。 筆者らはSPARK(SPARK)という3段階のフレームワークを提案し、第1段階ではジェネレータモデルが多様な解を生成し、検証器モデルがそれらを評価する。 ステップレベルで複数の独立した検証を集約することで、根底的な結果管理を超越したプロセス報酬モデルのトレーニングデータが得られることを示す。
  論文  参考訳（メタデータ） (2025-12-02T21:30:47Z)
• Hilbert: Recursively Building Formal Proofs with Informal Reasoning [38.36481253622752]
  大規模言語モデル(LLM)は、驚くべき数学的推論能力を示しているが、そのソリューションには自動検証できないエラーが含まれていることが多い。 非公式な推論と形式的検証の相補的な強みを組み合わせたエージェントフレームワークであるHilbertを紹介する。 我々のシステムは4つのコンポーネントを編成する: 数学的推論に優れる非公式のLLM、リーン4の戦術に最適化された特殊なLLM、形式検証器、意味定理検索器。
  論文  参考訳（メタデータ） (2025-09-26T18:24:23Z)
• Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening [36.81125165911328]
  強化学習は、言語モデルの推論能力を改善する主要な要因として現れています。 本稿では,現在の強化学習アルゴリズムが,すでに解いている問題に関するベースモデルの分布を単に研ぎ澄ましているだけかどうかを考察する。 差分報酬はランクバイアスを緩和し、合成定理と実定理の両方の証明設定において、多種多様な$N$でpass@N$を改善することを示す。
  論文  参考訳（メタデータ） (2025-06-03T01:15:15Z)
• Exploring the Limit of Outcome Reward for Learning Mathematical Reasoning [65.2421542320293]
  推論能力は汎用知能の重要な構成要素である。 OpenAIのoシリーズモデルなどのプロプライエタリ企業による最近の進歩は、推論タスクに顕著な進歩をもたらした。 本稿では、数学的推論タスクのための textbfOutcome textbfREwtextbfArd ベースの強化 textbfLearning により達成できる性能限界を追求する新しい RL フレームワーク OREAL を提案する。
  論文  参考訳（メタデータ） (2025-02-10T18:57:29Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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