論文の概要: Training Step-Level Reasoning Verifiers with Formal Verification Tools

• arxiv url: http://arxiv.org/abs/2505.15960v1
• Date: Wed, 21 May 2025 19:23:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-23 17:12:47.881568
• Title: Training Step-Level Reasoning Verifiers with Formal Verification Tools
• Title（参考訳）: 形式的検証ツールを用いたステップレベル推論検証器の訓練
• Authors: Ryo Kamoi, Yusen Zhang, Nan Zhang, Sarkar Snigdha Sarathi Das, Rui Zhang,
• Abstract要約: 本稿では,形式的検証ツールによって自動的に注釈付けされたステップレベルのエラーラベルに対して,PRMをトレーニングするためのアプローチであるFoVerを提案する。 FoVerは形式的検証と互換性のあるタスクに対してのみ使用可能である。 LLMをベースとしたPRMは,多種多様な推論タスクの検証を改善し,クロスタスクの一般化を示す。
• 参考スコア（独自算出の注目度）: 10.625896243556578
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Process Reward Models (PRMs), which provide step-by-step feedback on the reasoning generated by Large Language Models (LLMs), are receiving increasing attention. However, two key research gaps remain: collecting accurate step-level error labels for training typically requires costly human annotation, and existing PRMs are limited to math reasoning problems. In response to these gaps, this paper aims to address the challenges of automatic dataset creation and the generalization of PRMs to diverse reasoning tasks. To achieve this goal, we propose FoVer, an approach for training PRMs on step-level error labels automatically annotated by formal verification tools, such as Z3 for formal logic and Isabelle for theorem proof, which provide automatic and accurate verification for symbolic tasks. Using this approach, we synthesize a training dataset with error labels on LLM responses for formal logic and theorem proof tasks without human annotation. Although this data synthesis is feasible only for tasks compatible with formal verification, we observe that LLM-based PRMs trained on our dataset exhibit cross-task generalization, improving verification across diverse reasoning tasks. Specifically, PRMs trained with FoVer significantly outperform baseline PRMs based on the original LLMs and achieve competitive or superior results compared to state-of-the-art PRMs trained on labels annotated by humans or stronger models, as measured by step-level verification on ProcessBench and Best-of-K performance across 12 reasoning benchmarks, including MATH, AIME, ANLI, MMLU, and BBH. The datasets, models, and code are provided at https://github.com/psunlpgroup/FoVer.
• Abstract（参考訳）: 大規模言語モデル(LLM)が生み出す推論を段階的にフィードバックするプロセス・リワード・モデル(PRM)が注目されている。 トレーニングのために正確なステップレベルのエラーラベルを収集するには、一般的に人為的なアノテーションが必要であり、既存のPRMは数学推論の問題に限られている。 これらのギャップに対応するために,本論文では,自動データセット作成の課題と多様な推論タスクへのPRMの一般化について論じる。 この目的を達成するために,形式論理用Z3や定理証明用Isabelleなどの形式検証ツールによって注釈付けされたステップレベルのエラーラベルに対して,PRMをトレーニングするためのアプローチであるFoVerを提案する。 この手法を用いて,人間のアノテーションを使わずに,形式論理および定理証明タスクに対するLLM応答の誤りラベル付きトレーニングデータセットを合成する。 このデータ合成は形式的検証と互換性のあるタスクに対してのみ実現可能であるが、我々のデータセットでトレーニングされたLCMベースのPRMは、クロスタスクの一般化を示し、多様な推論タスクの検証を改善している。 具体的には、FoVerでトレーニングされたPRMは、オリジナルのLLMに基づいてベースラインPRMを著しく上回り、MATH、AIME、ANLI、MMLU、BBHを含む12の推論ベンチマークでProcessBenchとBest-of-Kのパフォーマンスのステップレベル検証によって測定され、人間またはより強力なモデルでアノテートされたラベルに基づいてトレーニングされた最先端のPRMと比較して、競争力や優れた結果が得られる。 データセット、モデル、コードはhttps://github.com/psunlpgroup/FoVerで提供されている。

関連論文リスト

• Beyond the First Error: Process Reward Models for Reflective Mathematical Reasoning [49.21525229904197]
  本研究では,長いCoT推論プロセスのスコアリングに特化して設計されたPRMのための新しいデータアノテーション手法を提案する。 本稿では, 誤り伝播と誤認識の概念を導入し, PRMの効果的な自己訂正行動と誤ったステップに基づく推論の両方を識別する能力を高めた。 我々のPRMは,探索誘導,BoN,F1スコアなど,様々な指標で優れた性能を実現している。
  論文  参考訳（メタデータ） (2025-05-20T14:12:05Z)
• Accurate and Diverse LLM Mathematical Reasoning via Automated PRM-Guided GFlowNets [6.001837672951086]
  モンテカルロ木探索を用いたプロセス・リワード・モデル(PRM)を提案する。 次に、生成フローネットワーク(GFlowNets)を推論ステップレベルで運用するように適応します。 経験的評価は、挑戦的な数学的ベンチマークにおいて、精度と解の多様性の両方が強く改善されていることを示している。
  論文  参考訳（メタデータ） (2025-04-28T16:56:41Z)
• Process Reward Models That Think [86.88809596842428]
  ステップバイステップ検証 - プロセス報酬モデル(PRM)としても知られる - は、テスト時間スケーリングの鍵となる要素である。 この研究は、検証チェーン・オブ・シント(CoT)を生成することにより、ソリューションのすべてのステップを検証する言語化されたステップワイド報酬モデルとして、データ効率の高いPRMを構築することを目的としている。 我々は差別的PRMよりもプロセスラベルを桁違いに少なめに微調整した長いCoT検証器ThinkPRMを提案する。
  論文  参考訳（メタデータ） (2025-04-23T15:44:54Z)
• Free Process Rewards without Process Labels [55.14044050782222]
  より安価な応答レベルラベルでORMをトレーニングすることで,テキストシンプルなPRMを追加のコストで得ることができることを示す。 我々の暗黙のPRMは、クロスエントロピー(CE)損失でインスタンス化されると、よりデータ効率が良く、命令1回に1回しか応答しない訓練でも生成モデルを改善することができることを示す。
  論文  参考訳（メタデータ） (2024-12-02T21:20:02Z)
• InfiMM-Eval: Complex Open-Ended Reasoning Evaluation For Multi-Modal Large Language Models [50.03163753638256]
  MLLM(Multi-modal Large Language Models)は人工知能の分野で注目されている。 本ベンチマークは, 帰納的, 帰納的, 類推的推論の3つの主要な推論カテゴリから構成される。 我々は,この厳密に開発されたオープンエンド多段階精巧な推論ベンチマークを用いて,代表MLLMの選択を評価する。
  論文  参考訳（メタデータ） (2023-11-20T07:06:31Z)

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

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