論文の概要: Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning

• arxiv url: http://arxiv.org/abs/2609.37203v1
• Date: Tue, 29 Sep 2026 10:21:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-30 21:28:47.417424
• Title: Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning
• Title（参考訳）: 証明への学習 : 自然な言語論理的推論のための形式的検証からの強化学習
• Abstract要約: 自然言語の論理的推論では、中間的な結論はその前提から従うべきであり、結果の導出は最終的な答えを支持するべきである。 既存の方法には、中間的な結論と回答をサポートする証明依存関係のマシンチェック可能な検証が欠如している。 本稿では,LLMを学習し,自然言語論理的推論の検証可能な証明を構築するための形式検証からRLフレームワークProof-R1を提案する。
• 参考スコア（独自算出の注目度）: 21.780677296439958
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Large language models (LLMs) are increasingly deployed for natural-language logical reasoning, where the final answer is easy to check but the proof behind it is not. In natural-language logical reasoning, an intermediate conclusion should follow from its premises, and the resulting derivation should support the final answer. Existing methods lack machine-checkable verification of intermediate conclusions and answer-supporting proof dependencies, so they may assign credit to invalid or answer-irrelevant steps. We propose Proof-R1, an RL framework from formal verification that trains LLMs to construct verifiable proofs for natural-language logical reasoning. Proof-R1 admits a generated conclusion into the verified proof state only when the corresponding reasoning action satisfies the proof obligations through UNSAT-based machine-checkable formal verification. Proof-R1 also recovers the answer-supporting dependency closure to trace the proof structure of the final answer and align outcome credit with the proof dependencies. Experiments demonstrate that Proof-R1 improves answer accuracy across three logical reasoning benchmarks and four backbone models and outperforms training-free agents and training-based methods in terms of reasoning-process verifiability.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、最終的な答えは簡単にチェックできるが、その裏にある証明はそうではない、自然言語論理的推論のためにますます多くデプロイされている。 自然言語の論理的推論では、中間的な結論はその前提から従うべきであり、結果の導出は最終的な答えを支持するべきである。 既存の方法には中間的な結論のマシンチェック可能な検証や、解答支援の証明依存関係がないため、無効または解答関連ステップにクレジットを割り当てることができる。 本稿では,LLMを学習し,自然言語論理的推論の検証可能な証明を構築するための形式検証からRLフレームワークProof-R1を提案する。 Proof-R1は、UNSATベースのマシンチェック可能な形式検証によって、対応する推論動作が証明義務を満たす場合にのみ、証明状態に生成された結論を認める。 Proof-R1はまた、応答支持依存クロージャを回復し、最終回答の証明構造をトレースし、結果クレジットを証明依存と整合させる。 実験により、Proof-R1は3つの論理的推論ベンチマークと4つのバックボーンモデルで解答精度を向上し、推論プロセスの検証可能性の観点からトレーニングフリーエージェントとトレーニングベースメソッドより優れていることが示された。

関連論文リスト

• Autoformalizing Argumentative Material Inferences [26.35292656634472]
  我々は、ガード補完として議論材料推論のための自己形式化を開発する。 GUARDは、証明された信条を大幅に改善する。 シンボル的ソフトな批判と明示的な仮定層がこれらの利益の大部分を担っていることを示す。
  論文  参考訳（メタデータ） (2026-09-15T11:05:26Z)
• Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries [18.744562922743405]
  PRoSFI(Process Reward over Structured Formal Intermediates)は、精度を損なうことなく推論信頼性を高める新しい報奨法である。 完全に検証された推論チェーンのみが高い報酬を受け取る。 形式的検証の統合は、ステップバイステップのマシンチェック可能な証明を生成するためのモデルを導く。
  論文  参考訳（メタデータ） (2026-03-31T09:42:13Z)
• Translating Informal Proofs into Formal Proofs Using a Chain of States [20.0011959667642]
  本稿では,自然言語で表現された非公式な数学的証明を,制約付き計算予算の下でLean4の形式的証明に変換する問題に対処する。 まず、中間形式的証明状態の列である状態の連鎖(CoS)を、非公式引数の論理構造に沿って抽出する。 次に、CoS内の隣接状態間の遷移戦略を生成し、完全な形式的証明を構築する。
  論文  参考訳（メタデータ） (2025-12-11T06:08:34Z)
• 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)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• ProoFVer: Natural Logic Theorem Proving for Fact Verification [24.61301908217728]
  本稿では,自然論理を用いた事実検証システムProoFVerを提案する。 証明の生成により、ProoFVerは説明可能なシステムになる。 証明により,人間がProoFVerの判断を正しくシミュレートできることが判明した。
  論文  参考訳（メタデータ） (2021-08-25T17:23:04Z)

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

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