論文の概要: Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification

• arxiv url: http://arxiv.org/abs/2506.04592v1
• Date: Thu, 05 Jun 2025 03:16:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-06 21:53:49.508309
• Title: Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification
• Title（参考訳）: 安全: ふりかえりのステップ認識形式検証による大規模言語モデルにおける数学的推論の強化
• Authors: Chengwu Liu, Ye Yuan, Yichun Yin, Yan Xu, Xin Xu, Zaoyu Chen, Yasheng Wang, Lifeng Shang, Qun Liu, Ming Zhang,
• Abstract要約: Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
• 参考スコア（独自算出の注目度）: 56.218970738892764
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Chain-of-Thought (CoT) prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs). However, to mitigate hallucinations in CoT that are notoriously difficult to detect, current methods such as process reward models (PRMs) or self-consistency operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness. To address this issue, we draw inspiration from the idea that "the gold standard for supporting a mathematical claim is to provide a proof". We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations. We evaluate our framework $Safe$ across multiple language models and various mathematical datasets, demonstrating a significant performance improvement while offering interpretable and verifiable evidence. We also propose $FormalStep$ as a benchmark for step correctness theorem proving with $30,809$ formal statements. To the best of our knowledge, our work represents the first endeavor to utilize formal mathematical language Lean 4 for verifying natural language content generated by LLMs, aligning with the reason why formal mathematical languages were created in the first place: to provide a robust foundation for hallucination-prone human-written proofs.
• Abstract（参考訳）: CoT(Chain-of-Thought)プロンプトは,大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 しかし、検出するのが非常に難しいCoTの幻覚を緩和するために、プロセス報酬モデル(PRM)や自己整合性といった現在の手法は不透明なボックスとして機能し、彼らの判断に対する検証可能な証拠を提供しておらず、おそらくその効果を制限している。 この問題に対処するため、我々は「数学的主張を支持するための金の標準は証明を提供することである」という考えから着想を得た。 我々は,段階対応の形式検証フレームワークである$Safe$を提案する。 任意のスコアを割り当てるのではなく、各推論ステップで形式的な数学的言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。 我々は、複数の言語モデルと様々な数学的データセットにまたがるフレームワーク$Safe$を評価し、解釈可能かつ検証可能なエビデンスを提供しながら、大幅なパフォーマンス向上を実証した。 また、30,809ドルの形式文で証明されたステップ正当性定理のベンチマークとして$FormalStep$を提案する。 我々の知識を最大限に活用するために、我々の研究は、LLMが生成した自然言語の内容を検証するために、フォーマルな数学的言語を利用するための最初の取り組みであるLean 4を表現している。

関連論文リスト

• 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)

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

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