論文の概要: Expected Value Alignment for Generative Reward Modeling in Formal Mathematics Verification

• arxiv url: http://arxiv.org/abs/2606.01160v1
• Date: Sun, 31 May 2026 11:06:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-02 21:34:29.289158
• Title: Expected Value Alignment for Generative Reward Modeling in Formal Mathematics Verification
• Title（参考訳）: 形式的数学検証における生成的リワードモデリングのための期待値アライメント
• Authors: Shihao Ji, Haotao Tan, Zihui Song, Mingyu Li,
• Abstract要約: 本稿では,モデルのトークン分布から連続的なスコアを抽出しながら,表面出力を離散的に維持する報奨モデルである期待値アライメント(EVA)を紹介する。 リーン4の形式検証のための報酬モデルであるtextitLeibnizでEVAをインスタンス化し、ゼロショットと報酬モデリングのベースラインに対して評価します。
• 参考スコア（独自算出の注目度）: 12.08180258890855
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large Language Models (LLMs) are increasingly used with formal interactive theorem provers such as Lean 4. Scaling these systems with reinforcement learning or search methods requires process reward models (PRMs) that can evaluate intermediate reasoning steps. Existing reward-model designs expose a practical trade-off. Value-head models provide continuous scores but modify the generative model interface, while generative reward models preserve textual rationales but are poorly matched to continuous floating-point regression because numeric values are split across tokens. We introduce Expected Value Alignment (EVA), a reward-modeling procedure that keeps the surface output discrete while extracting continuous scores from the model's token distribution. The model emits integer scores in a structured JSON format, and EVA computes a continuous score as the expectation over the logits of the corresponding anchor tokens. Training combines the causal language modeling objective with an auxiliary mean squared error loss on these expected values. We instantiate EVA in \textit{Leibniz}, a reward model for Lean 4 formal verification, and evaluate it against zero-shot and reward-modeling baselines. The evaluation demonstrates that continuous logit-based scoring significantly reduces discretization artifacts while retaining the interpretability of generative critiques.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、Lean 4のような形式的な対話型定理プローバーでますます使われています。 これらのシステムを強化学習や探索手法でスケールするには、中間的推論ステップを評価するプロセス報酬モデル(PRM)が必要である。 既存の報酬モデルの設計は、実用的なトレードオフを露呈する。 バリューヘッドモデルは連続的なスコアを提供するが、生成的モデルインターフェースを変更する一方で、生成的報酬モデルはテキストの有理性を保持するが、数値値がトークン間で分割されるため、連続的な浮動小数点回帰にはあまりマッチしない。 本稿では,モデルのトークン分布から連続的なスコアを抽出しながら,表面出力を離散的に維持する報奨モデルである期待値アライメント(EVA)を紹介する。 モデルは構造化JSON形式で整数スコアを出力し、EVAは対応するアンカートークンのロケットに対する期待値として連続スコアを計算する。 訓練は、因果言語モデリングの目的と、これらの期待値に対する平均2乗誤差の補助的損失を組み合わせる。 EVAは、Lean 4の形式的検証のための報酬モデルであるtextit{Leibniz}でインスタンス化し、ゼロショットと報酬モデリングのベースラインに対して評価します。 この評価は,連続ロジットに基づくスコアリングが,生成的批評の解釈可能性を維持しつつ,識別的アーティファクトを著しく減少させることを示す。

関連論文リスト

• From Coarse to Fine: Benchmarking and Reward Modeling for Writing-Centric Generation Tasks [2.2483228605450956]
  大規模な言語モデルは、テキスト生成において顕著な進歩を遂げてきたが、それでも生成的な書き込みタスクに苦戦している。 報酬モデルを記述するための細粒度評価パイプラインWEvalと、微粒度強化学習学習フレームワークWRLを提案する。 WRLは命令要求を選択的にドロップすることで正と負のサンプルを構築し、より正確な報酬モデルトレーニングを可能にする。
  論文  参考訳（メタデータ） (2026-04-30T05:49:29Z)
• Generalization is not a universal guarantee: Estimating similarity to training data with an ensemble out-of-distribution metric [0.09363323206192666]
  機械学習モデルの新しいデータへの一般化の失敗は、AIシステムの信頼性を制限する中核的な問題である。 本稿では、一般化可能性推定(SAGE)のための教師付きオートエンコーダを構築することにより、データの類似性を評価するための標準化されたアプローチを提案する。 モデル自体のトレーニングやテストデータセットのデータに適用しても,SAGEスコアのフィルタリング後にアウト・オブ・ボックスモデルの性能が向上することを示す。
  論文  参考訳（メタデータ） (2025-02-22T19:21:50Z)
• Evaluating Generative Language Models in Information Extraction as Subjective Question Correction [49.729908337372436]
  本稿では,新しい評価手法SQC-Scoreを提案する。 主観的質問訂正の原則に着想を得て,新しい評価手法SQC-Scoreを提案する。 3つの情報抽出タスクの結果から,SQC-Scoreは基準値よりもアノテータの方が好ましいことが示された。
  論文  参考訳（メタデータ） (2024-04-04T15:36:53Z)
• RewardBench: Evaluating Reward Models for Language Modeling [100.28366840977966]
  本稿では,報酬モデル評価のためのベンチマークデータセットとコードベースであるRewardBenchを紹介する。 データセットは、チャット、推論、安全性にまたがる、プロンプト・チョーゼン・リジェクトされたトリオのコレクションである。 RewardBenchのリーダーボードでは、様々な方法で訓練された報酬モデルを評価する。
  論文  参考訳（メタデータ） (2024-03-20T17:49:54Z)
• Evaluating Representations with Readout Model Switching [19.907607374144167]
  本稿では,最小記述長(MDL)の原理を用いて評価指標を考案する。 我々は、読み出しモデルのためのハイブリッド離散および連続値モデル空間を設計し、それらの予測を組み合わせるために切替戦略を用いる。 提案手法はオンライン手法で効率的に計算でき,様々なアーキテクチャの事前学習された視覚エンコーダに対する結果を示す。
  論文  参考訳（メタデータ） (2023-02-19T14:08:01Z)
• Consistent Diffusion Models: Mitigating Sampling Drift by Learning to be Consistent [97.64313409741614]
  本稿では, モデルが生成したデータ上での予測が時間とともに一定であることを示す, 両立性特性を強制することを提案する。 CIFAR-10の条件および非条件生成とAFHQとFFHQのベースライン改良について,本研究の新たな訓練目標が得られた。
  論文  参考訳（メタデータ） (2023-02-17T18:45:04Z)
• Explaining and Improving Model Behavior with k Nearest Neighbor Representations [107.24850861390196]
  モデルの予測に責任のあるトレーニング例を特定するために, k 近傍表現を提案する。 我々は,kNN表現が学習した素因関係を明らかにするのに有効であることを示す。 以上の結果から,kNN手法により,直交モデルが逆入力に対してより堅牢であることが示唆された。
  論文  参考訳（メタデータ） (2020-10-18T16:55:25Z)
• Goal-directed Generation of Discrete Structures with Conditional Generative Models [85.51463588099556]
  本稿では,強化学習目標を直接最適化し,期待される報酬を最大化するための新しいアプローチを提案する。 提案手法は、ユーザ定義プロパティを持つ分子の生成と、所定の目標値を評価する短いピソン表現の同定という2つのタスクで検証する。
  論文  参考訳（メタデータ） (2020-10-05T20:03:13Z)

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

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