論文の概要: Translating Informal Proofs into Formal Proofs Using a Chain of States

• arxiv url: http://arxiv.org/abs/2512.10317v2
• Date: Fri, 12 Dec 2025 08:11:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-15 13:50:29.186602
• Title: Translating Informal Proofs into Formal Proofs Using a Chain of States
• Title（参考訳）: 状態連鎖を用いた不定形証明の形式的証明への変換
• Authors: Ziyu Wang, Bowen Yang, Chenyi Li, Yuan Zhang, Shihao Zhou, Bin Dong, Zaiwen Wen,
• Abstract要約: 本稿では,自然言語で表現された非公式な数学的証明を,制約付き計算予算の下でLean4の形式的証明に変換する問題に対処する。 まず、中間形式的証明状態の列である状態の連鎖(CoS)を、非公式引数の論理構造に沿って抽出する。 次に、CoS内の隣接状態間の遷移戦略を生成し、完全な形式的証明を構築する。
• 参考スコア（独自算出の注目度）: 20.0011959667642
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We address the problem of translating informal mathematical proofs expressed in natural language into formal proofs in Lean4 under a constrained computational budget. Our approach is grounded in two key insights. First, informal proofs tend to proceed via a sequence of logical transitions - often implications or equivalences - without explicitly specifying intermediate results or auxiliary lemmas. In contrast, formal systems like Lean require an explicit representation of each proof state and the tactics that connect them. Second, each informal reasoning step can be viewed as an abstract transformation between proof states, but identifying the corresponding formal tactics often requires nontrivial domain knowledge and precise control over proof context. To bridge this gap, we propose a two stage framework. Rather than generating formal tactics directly, we first extract a Chain of States (CoS), a sequence of intermediate formal proof states aligned with the logical structure of the informal argument. We then generate tactics to transition between adjacent states in the CoS, thereby constructing the full formal proof. This intermediate representation significantly reduces the complexity of tactic generation and improves alignment with informal reasoning patterns. We build dedicated datasets and benchmarks for training and evaluation, and introduce an interactive framework to support tactic generation from formal states. Empirical results show that our method substantially outperforms existing baselines, achieving higher proof success rates.
• Abstract（参考訳）: 本稿では,自然言語で表現された非公式な数学的証明を,制約付き計算予算の下でLean4の形式的証明に変換する問題に対処する。 私たちのアプローチには2つの重要な洞察があります。 第一に、非公式な証明は、中間結果や補助補題を明示的に指定することなく、論理遷移(しばしば含意や等価性)を通じて進行する傾向がある。 対照的に、リーンのような形式的なシステムは、それぞれの証明状態とそれらを結び付ける戦術を明確に表現する必要があります。 第二に、各非公式な推論ステップは証明状態間の抽象的な変換と見なすことができるが、対応する形式的戦術を特定するには、しばしば非自明なドメイン知識と証明コンテキストの正確な制御が必要である。 このギャップを埋めるために、我々は2段階のフレームワークを提案する。 形式的戦術を直接生成するのではなく、まず、形式的議論の論理的構造に沿った中間的な形式的証明状態の列である状態の連鎖(CoS)を抽出する。 次に、CoS内の隣接状態間の遷移戦略を生成し、完全な形式的証明を構築する。 この中間表現は戦術生成の複雑さを著しく低減し、非公式な推論パターンとの整合性を改善する。 トレーニングと評価のための専用のデータセットとベンチマークを構築し、正式な状態から戦術生成をサポートするインタラクティブなフレームワークを導入します。 実験結果から,本手法は既存のベースラインを著しく上回り,高い証明成功率が得られることが示された。

関連論文リスト

• Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning [0.0]
  CoT(Chain-of-Thought)は、大規模言語モデルの推論能力を高める。 本稿では、カリー・ホワード対応に基づく新しい理論レンズを提案する。 我々はこの類似を運用し、CoTの非公式な自然言語ステップを形式化された型付き証明構造に抽出し、マッピングする方法を提供する。
  論文  参考訳（メタデータ） (2025-10-01T16:06:40Z)
• StepProof: Step-by-step verification of natural language mathematical proofs [16.150265021594088]
  本稿では,ステップ・バイ・ステップ検証のための新しい自動形式化手法であるStepProofを提案する。 StepProofは、完全な証明を複数の検証可能なサブプロテクションに分解し、文レベルの検証を可能にする。 StepProofは従来の手法に比べて証明成功率と効率を著しく改善することを示す。
  論文  参考訳（メタデータ） (2025-06-12T10:31:23Z)
• 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)
• Steering LLMs for Formal Theorem Proving [1.083373217040891]
  我々は,非公式な推論トレースに関連する残効活性化における線形方向を同定する推論時間介入を開発する。 このメカニズムはまた、大規模言語モデルのアクティベーション空間において、推論がどのように内部的にエンコードされているかについての解釈可能な情報を与える。 1) LLM の証明合成を導くための新しいアクティベーションベースの介入,(2) この介入が2つの復号化戦略の下で性能を向上させることの実証である。
  論文  参考訳（メタデータ） (2025-02-21T15:04:48Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference [0.16317061277457]
  自然言語推論の基礎となる推論過程をモデル化できる推論フレームワークを提案する。 このフレームワークは、形式論理におけるよく研究された証明システムであるセマンティック・テーブルー法に基づいている。 本稿では、自然言語推論タスクを構造化された説明で定義する方法について述べる。
  論文  参考訳（メタデータ） (2023-11-15T01:24:09Z)

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

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