論文の概要: Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries

• arxiv url: http://arxiv.org/abs/2603.29500v1
• Date: Tue, 31 Mar 2026 09:42:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-01 15:25:03.466422
• Title: Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries
• Title（参考訳）: 形式的に検証可能なステップ・バイ・ステップ論理推論を構造化形式媒介を介して生成する学習
• Authors: Luoxin Chen, Yichi Zhou, Huishuai Zhang,
• Abstract要約: PRoSFI(Process Reward over Structured Formal Intermediates)は、精度を損なうことなく推論信頼性を高める新しい報奨法である。 完全に検証された推論チェーンのみが高い報酬を受け取る。 形式的検証の統合は、ステップバイステップのマシンチェック可能な証明を生成するためのモデルを導く。
• 参考スコア（独自算出の注目度）: 18.744562922743405
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) have recently demonstrated impressive performance on complex, multi-step reasoning tasks, especially when post-trained with outcome-rewarded reinforcement learning Guo et al. 2025. However, it has been observed that outcome rewards often overlook flawed intermediate steps, leading to unreliable reasoning steps even when final answers are correct. To address this unreliable reasoning, we propose PRoSFI (Process Reward over Structured Formal Intermediates), a novel reward method that enhances reasoning reliability without compromising accuracy. Instead of generating formal proofs directly, which is rarely accomplishable for a modest-sized (7B) model, the model outputs structured intermediate steps aligned with its natural language reasoning. Each step is then verified by a formal prover. Only fully validated reasoning chains receive high rewards. The integration of formal verification guides the model towards generating step-by-step machine-checkable proofs, thereby yielding more credible final answers. PRoSFI offers a simple and effective approach to training trustworthy reasoning models.
• Abstract（参考訳）: 大規模言語モデル(LLM)は最近、複雑な多段階推論タスクにおいて印象的なパフォーマンスを実証している。 しかし、結果の報奨は、しばしば欠陥のある中間ステップを見落とし、最終回答が正しければ、信頼できない推論ステップにつながることが観察されている。 この不確実な推論に対処するため,我々はPRoSFI(Process Reward over Structured Formal Intermediates)を提案する。 形式的証明を直接生成するのではなく、モデストサイズの (7B) モデルでは達成できないが、モデルは自然言語の推論と整合した構造化中間ステップを出力する。 それぞれのステップは、正式な証明者によって検証される。 完全に検証された推論チェーンのみが高い報酬を受け取る。 形式的検証の統合は、モデルをステップバイステップのマシンチェック可能な証明を生成するためのガイドとなり、それによってより信頼性の高い最終回答が得られる。 PRoSFIは、信頼できる推論モデルをトレーニングするためのシンプルで効果的なアプローチを提供する。

関連論文リスト

• Training LLMs with LogicReward for Faithful and Rigorous Reasoning [75.30425553246177]
  定理証明器を用いてステップレベルの論理的正しさを強制することでモデルトレーニングを指導する報酬システムであるLogicRewardを提案する。 LogicRewardで構築されたデータに基づいてトレーニングされた8Bモデルは、GPT-4oとo4-miniを11.6%、自然言語推論と論理的推論タスクで2%超えた。
  論文  参考訳（メタデータ） (2025-12-20T03:43:02Z)
• StepProof: Step-by-step verification of natural language mathematical proofs [16.150265021594088]
  本稿では,ステップ・バイ・ステップ検証のための新しい自動形式化手法であるStepProofを提案する。 StepProofは、完全な証明を複数の検証可能なサブプロテクションに分解し、文レベルの検証を可能にする。 StepProofは従来の手法に比べて証明成功率と効率を著しく改善することを示す。
  論文  参考訳（メタデータ） (2025-06-12T10:31:23Z)
• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
  本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。 訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。 トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
  論文  参考訳（メタデータ） (2025-04-28T19:25:29Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Deductive Verification of Chain-of-Thought Reasoning [22.79166959432764]
  大型言語モデル(LLM)は、様々な推論タスクを実行する上で、Chain-of-Thoughtの恩恵を受ける。 CoTはモデルがより包括的な推論プロセスを生成することを可能にするが、中間的推論ステップに重点を置くことは、必然的に幻覚や累積エラーをもたらす可能性がある。 本研究では,自然言語に基づく帰納的推論形式であるNatural Programを提案する。
  論文  参考訳（メタデータ） (2023-06-06T17:18:56Z)

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

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