自然推論の限界を押し広げる：形式論理検証によるインターリーブ報酬

要旨

大規模言語モデル（LLM）は顕著な能力を示す一方で、その確率的な次トークン予測は、形式的記号システムが回避する論理的不整合や報酬ハッキングを生み出す。この隔たりを埋めるため、我々は形式的論理検証誘導型フレームワークを提案する。これは自然言語生成プロセスと形式的記号検証を動的に交互に行い、エラー発生時の検出と修正を可能とするリアルタイムフィードバックを提供する。受動的な事後検証に限定された従来の神経記号手法と異なり、本手法は推論連鎖内で生じる中間段階の誤りを能動的に抑制する。我々はこのフレームワークを、形式的論理検証誘導型教師ありファインチューニングと方策最適化を統合した新しい2段階訓練パイプラインにより実現した。数学的推論、論理的推論、一般推論にわたる6種のベンチマークによる広範な評価において、当該7Bモデルと14Bモデルは既存の最高性能ベースラインを平均でそれぞれ10.4%、14.2%上回った。これらの結果は、形式的検証が先進的LLM推論の性能限界を大幅に拡大するスケーラブルなメカニズムとなり得ることを実証する。

English

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.

自然推論の限界を押し広げる：形式論理検証によるインターリーブ報酬

Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification

要旨

Support