論文の概要: Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification

• arxiv url: http://arxiv.org/abs/2601.22642v1
• Date: Fri, 30 Jan 2026 07:01:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-02 18:28:15.285781
• Title: Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification
• Title（参考訳）: 自然推論の境界を押し上げる:形式論理的検証からのインターリーブボーナス
• Authors: Chuxue Cao, Jinluan Yang, Haoran Li, Kunhao Pan, Zijian Zhao, Zhengyu Chen, Yuchen Tian, Lijun Wu, Conghui He, Sirui Han, Yike Guo,
• Abstract要約: 大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。 本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。 我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
• 参考スコア（独自算出の注目度）: 49.506412445511934
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large Language Models (LLMs) show remarkable capabilities, yet their stochastic next-token prediction creates logical inconsistencies and reward hacking that formal symbolic systems avoid. To bridge this gap, we introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process, providing real-time feedback to detect and rectify errors as they occur. Distinguished from previous neuro-symbolic methods limited by passive post-hoc validation, our approach actively penalizes intermediate fallacies during the reasoning chain. We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization. Extensive evaluation on six benchmarks spanning mathematical, logical, and general reasoning demonstrates that our 7B and 14B models outperform state-of-the-art baselines by average margins of 10.4% and 14.2%, respectively. These results validate that formal verification can serve as a scalable mechanism to significantly push the performance boundaries of advanced LLM reasoning.
• Abstract（参考訳）: 大きな言語モデル(LLM)は目覚ましい能力を示すが、その確率的な次世代の予測は、形式的な象徴的なシステムが避ける論理的不整合と報酬的ハッキングを生み出している。 このギャップを埋めるために、我々は自然言語生成プロセスと形式的記号検証を動的にインターリーブする形式論理検証誘導フレームワークを導入し、エラーを検知し修正するためのリアルタイムフィードバックを提供する。 受動的ポストホックバリデーションによって制限された従来のニューロシンボリック法とは違い,本手法は推論チェーン中に中間的誤認を積極的に罰する。 我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。 数学、論理学、一般の推論にまたがる6つのベンチマークの広範囲な評価は、我々の7Bと14Bモデルは、それぞれ平均マージン10.4%と14.2%で最先端のベースラインを上回っていることを示している。 これらの結果は、形式的検証が高度なLCM推論の性能境界を大幅に推し進めるためのスケーラブルなメカニズムであることを示す。

関連論文リスト

• VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning [4.3414302048068745]
  本稿では,大規模言語モデルとSMTソルバを組み合わせたニューロシンボリック・フレームワークを提案する。 本稿では,(1)形式的意味的等価性チェックによるマルチモデルコンセンサス,(2)適切な検証戦略に異なるクレーム型を指示するセマンティックルーティング,(3)最小補正サブセットによる正確な論理的エラーローカライゼーション,の3点を紹介する。 GPT-OSS-120Bモデルでは、VERGEはシングルパスアプローチと比較して、一連の推論ベンチマークにおいて平均18.7%の性能向上を示す。
  論文  参考訳（メタデータ） (2026-01-27T20:59:11Z)
• VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
  Referring Expression (REC) は、自然言語クエリに対応する画像領域をローカライズすることを目的としている。 最近のニューロシンボリックRECアプローチは、大規模言語モデル(LLM)と視覚言語モデル(VLM)を利用して構成推論を行う。 推論ステップ内に軽量な演算子レベルの検証器を組み込む,ニューロシンボリックなフレームワークであるVIROを紹介する。
  論文  参考訳（メタデータ） (2026-01-19T07:21:19Z)
• 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)
• Efficient Thought Space Exploration through Strategic Intervention [54.35208611253168]
  本稿では,この知見を2つの相乗的コンポーネントを通して操作するHint-Practice Reasoning(HPR)フレームワークを提案する。 フレームワークの中核となる革新は、動的に介入点を識別する分散不整合低減(DIR)である。 算術的および常識的推論ベンチマークによる実験は、HPRの最先端の効率-精度トレードオフを実証している。
  論文  参考訳（メタデータ） (2025-11-13T07:26:01Z)
• A Neurosymbolic Approach to Natural Language Formalization and Verification [4.697939947463767]
  大規模言語モデルは、自然言語の解釈や推論においてよく機能するが、その固有性は金融や医療といった規制された産業における採用を制限する。 本稿では,LLMを用いた2段階のニューロシンボリック・フレームワークを提案する。 提案手法は, 論理的妥当性の同定において, ほぼゼロの偽陽性率を示すため, 99%以上の音響性を示した。
  論文  参考訳（メタデータ） (2025-11-12T06:00:37Z)
• Foundation Models for Logistics: Toward Certifiable, Conversational Planning Interfaces [59.80143393787701]
  大規模言語モデル(LLM)は不確実性に対処し、導入障壁を低くしながら再計画の加速を約束する。 本稿では,自然言語対話のアクセシビリティと目標解釈の検証可能な保証とを組み合わせたニューロシンボリック・フレームワークを提案する。 わずか100個の不確実性フィルタで微調整された軽量モデルは、GPT-4.1のゼロショット性能を上回り、推論遅延を50%近く削減する。
  論文  参考訳（メタデータ） (2025-07-15T14:24:01Z)
• CTRLS: Chain-of-Thought Reasoning via Latent State-Transition [57.51370433303236]
  チェーン・オブ・シント(CoT)推論は、大規模な言語モデルで複雑な問題を解釈可能な中間ステップに分解することを可能にする。 我々は,遅延状態遷移を伴うマルコフ決定プロセス(MDP)としてCoT推論を定式化するフレームワークであるgroundingSを紹介する。 我々は、ベンチマーク推論タスクにおける推論精度、多様性、探索効率の改善を示す。
  論文  参考訳（メタデータ） (2025-07-10T21:32:18Z)
• Enhancing Logical Reasoning in Language Models via Symbolically-Guided Monte Carlo Process Supervision [43.05159920832912]
  大規模言語モデル(LLM)は多くの推論ベンチマークで高いパフォーマンスを示している。 LLMはコンテンツのバリエーションに影響を受けやすく、堅牢な計画や象徴的な抽象化の欠如を示している。 そこで我々は,段階的に擬似ラベルで高品質な記号推論軌道を合成することで,そのような制限を克服することを提案する。
  論文  参考訳（メタデータ） (2025-05-26T18:06:39Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。 提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
  論文  参考訳（メタデータ） (2020-12-21T10:03:44Z)

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

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