論文の概要: StepProof: Step-by-step verification of natural language mathematical proofs

• arxiv url: http://arxiv.org/abs/2506.10558v1
• Date: Thu, 12 Jun 2025 10:31:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-13 15:37:22.684196
• Title: StepProof: Step-by-step verification of natural language mathematical proofs
• Title（参考訳）: StepProof: 自然言語の数学的証明のステップバイステップ検証
• Authors: Xiaolin Hu, Qinghua Zhou, Bogdan Grechuk, Ivan Y. Tyukin,
• Abstract要約: 本稿では,ステップ・バイ・ステップ検証のための新しい自動形式化手法であるStepProofを提案する。 StepProofは、完全な証明を複数の検証可能なサブプロテクションに分解し、文レベルの検証を可能にする。 StepProofは従来の手法に比べて証明成功率と効率を著しく改善することを示す。
• 参考スコア（独自算出の注目度）: 16.150265021594088
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Interactive theorem provers (ITPs) are powerful tools for the formal verification of mathematical proofs down to the axiom level. However, their lack of a natural language interface remains a significant limitation. Recent advancements in large language models (LLMs) have enhanced the understanding of natural language inputs, paving the way for autoformalization - the process of translating natural language proofs into formal proofs that can be verified. Despite these advancements, existing autoformalization approaches are limited to verifying complete proofs and lack the capability for finer, sentence-level verification. To address this gap, we propose StepProof, a novel autoformalization method designed for granular, step-by-step verification. StepProof breaks down complete proofs into multiple verifiable subproofs, enabling sentence-level verification. Experimental results demonstrate that StepProof significantly improves proof success rates and efficiency compared to traditional methods. Additionally, we found that minor manual adjustments to the natural language proofs, tailoring them for step-level verification, further enhanced StepProof's performance in autoformalization.
• Abstract（参考訳）: インタラクティブ定理プロバー(英: Interactive theorem provers、ITP)は、数学的証明を公理レベルまで形式的に検証するための強力なツールである。 しかし、自然言語インタフェースの欠如は依然として大きな限界である。 大規模言語モデル(LLM)の最近の進歩は、自然言語入力の理解を強化し、自然言語証明を検証可能な形式証明に変換するプロセスである自己形式化の道を開いた。 これらの進歩にもかかわらず、既存の自己形式化アプローチは完全な証明の検証に限られており、より微細で文レベルの検証能力が欠如している。 このギャップに対処するために,ステップ・バイ・ステップ検証のための新しい自動形式化手法であるStepProofを提案する。 StepProofは、完全な証明を複数の検証可能なサブプロテクションに分解し、文レベルの検証を可能にする。 実験結果から、StepProofは従来の手法に比べて証明成功率と効率を著しく改善することが示された。 さらに、ステップレベルの検証のために、自然言語証明を手作業で微調整することで、オートフォーマル化におけるStepProofのパフォーマンスをさらに向上することを発見した。

関連論文リスト

• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
  論文  参考訳（メタデータ） (2025-06-05T03:16:08Z)
• 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)
• Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation [27.60611509339328]
  1つのトレーニングデータサンプルの最適順序は、特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに発生すると論じる。 証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。
  論文  参考訳（メタデータ） (2024-10-30T18:00:04Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Improving Autoformalization using Type Checking [15.58948808529849]
  我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• Verifying Quantum Phase Estimation (QPE) using Prove-It [0.0]
  Prove-Itと呼ばれる汎用的な対話型定理証明アシスタントは、量子位相推定(QPE)アルゴリズムを検証するために使用された。 Prove-Itは、量子回路に関するステートメントを含む洗練された数学的ステートメントを表現する能力に特有である。
  論文  参考訳（メタデータ） (2023-04-05T01:21:00Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)

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

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