論文の概要: 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を表現している。

関連論文リスト

• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
  本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。 IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。 シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
  論文  参考訳（メタデータ） (2025-07-31T17:00:30Z)
• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
  本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。 訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。 トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
  論文  参考訳（メタデータ） (2025-04-28T19:25:29Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。 目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
  論文  参考訳（メタデータ） (2024-09-09T18:21:28Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。 コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。 新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
  論文  参考訳（メタデータ） (2022-11-14T16:52:32Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)

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

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