論文の概要: Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure
- arxiv url: http://arxiv.org/abs/2509.09726v1
- Date: Wed, 10 Sep 2025 09:22:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-15 16:03:07.857714
- Title: Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure
- Title（参考訳）: 証明ステップのインフォーマル化と帰納的要約による形式的証明の自然言語翻訳
- Authors: Seiji Hattori, Takuya Matsuzaki, Makoto Fujiwara,
- Abstract要約: 本手法は、学部レベルの教科書から得られた自然言語証明に従って作成された形式的証明データに適用される。
本手法は,リーン証明アシスタントの既存の形式証明ライブラリに適用することにより,極めて可読かつ正確な自然言語証明を出力できることを実証する。
- 参考スコア（独自算出の注目度）: 0.15293427903448023
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This paper proposes a natural language translation method for machine-verifiable formal proofs that leverages the informalization (verbalization of formal language proof steps) and summarization capabilities of LLMs. For evaluation, it was applied to formal proof data created in accordance with natural language proofs taken from an undergraduate-level textbook, and the quality of the generated natural language proofs was analyzed in comparison with the original natural language proofs. Furthermore, we will demonstrate that this method can output highly readable and accurate natural language proofs by applying it to existing formal proof library of the Lean proof assistant.
- Abstract（参考訳）: 本稿では,LLMの非公式化(形式言語証明ステップの言語化)と要約機能を活用した,機械検証可能な形式証明のための自然言語翻訳手法を提案する。
評価のために,学部レベルの教科書から抽出した自然言語証明に従って作成した形式的証明データに適用し,生成した自然言語証明の品質を原自然言語証明と比較した。
さらに,本手法は,リーン証明アシスタントの既存の形式証明ライブラリに適用することにより,極めて可読かつ正確な自然言語証明を出力できることを実証する。
関連論文リスト
- 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) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Trustworthy Formal Natural Language Specifications [3.8073142980733]
本稿では、自然言語の表現的サブセットで書かれた仕様を構築できることを示す。
モジュール的に形式化された英語のサブセットで仕様を提供する手段を実装し、それらを形式的なクレームに自動的に変換する。
我々は,各単語の解釈方法と文の構造を用いて意味を計算したことを示す証明証明書を作成した。
論文 参考訳（メタデータ） (2023-10-05T20:41:47Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳（メタデータ） (2023-01-05T17:56:00Z) - 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) - Natural Language Specifications in Proof Assistants [0.0]
既存の証明アシスタント内で自然言語仕様のサポートを構築することができる。
本稿では,既存の証明アシスタント内で自然言語仕様のサポートを構築することが可能であることを論じる。
論文 参考訳（メタデータ） (2022-05-16T17:05:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。