論文の概要: ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization

• arxiv url: http://arxiv.org/abs/2510.15981v1
• Date: Mon, 13 Oct 2025 10:20:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-25 00:56:38.744231
• Title: ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
• Title（参考訳）: ProofFlow: Fithful Proof Autoformalizationに対する依存性グラフアプローチ
• Authors: Rafael Cabral, Tuan Manh Do, Xuejun Yu, Wai Ming Tai, Zijin Feng, Xin Shen,
• Abstract要約: 現在のアプローチでは、オリジナルの人間による議論の意味的意味と論理的構造を保存できない。 本稿では,構造的忠実度を主目的とする新しいパイプラインであるProofFlowを紹介する。 我々は184人の学部レベルの問題に対して,ステップバイステップのソリューションを手動でアノテートした新しいベンチマークを提示する。 また,構文的正しさ,意味的忠実度,構造的忠実度を評価するための新しい合成指標ProofScoreを導入する。
• 参考スコア（独自算出の注目度）: 10.021930888250546
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Proof autoformalization, the task of translating natural language theorems and proofs into machine-verifiable code, is a critical step for integrating large language models into rigorous mathematical workflows. Current approaches focus on producing executable code, but they frequently fail to preserve the semantic meaning and logical structure of the original human-written argument. To address this, we introduce ProofFlow, a novel pipeline that treats structural fidelity as a primary objective. ProofFlow first constructs a directed acyclic graph (DAG) to map the logical dependencies between proof steps. Then, it employs a novel lemma-based approach to systematically formalize each step as an intermediate lemma, preserving the logical structure of the original argument. To facilitate evaluation, we present a new benchmark of 184 undergraduate-level problems, manually annotated with step-by-step solutions and logical dependency graphs, and introduce ProofScore, a new composite metric to evaluate syntactic correctness, semantic faithfulness, and structural fidelity. Experimental results show our pipeline sets a new state-of-the-art for autoformalization, achieving a ProofScore of 0.545, substantially exceeding baselines like full-proof formalization (0.123), which processes the entire proof at once, and step-proof formalization (0.072), which handles each step independently. Our pipeline, benchmark, and score metric are open-sourced to encourage further progress at https://github.com/Huawei-AI4Math/ProofFlow.
• Abstract（参考訳）: 証明の自己形式化(Proof autoformalization)は、自然言語の定理と証明を機械で検証可能なコードに変換するタスクであり、大きな言語モデルを厳密な数学的ワークフローに統合するための重要なステップである。 現在のアプローチでは実行可能コードの生成に重点を置いているが、本来の人間の記述した引数の意味的意味と論理的構造を保存できないことが多い。 これを解決するために,構造的忠実度を主目的とする新しいパイプラインであるProofFlowを紹介した。 ProofFlowはまず、証明ステップ間の論理的依存関係をマッピングするために、有向非巡回グラフ(DAG)を構築する。 次に、各ステップを中間補題として体系的に形式化し、元の引数の論理構造を保存するために、新しい補題に基づくアプローチを採用する。 評価を容易にするために,ステップバイステップのソリューションと論理依存グラフを手動でアノテートした184人の学部レベルの新しいベンチマークと,構文的正当性,意味的忠実性,構造的忠実性を評価するための新しい合成指標ProofScoreを紹介する。 実験結果から, 完全完全形式化 (0.123) や, ステップごとに独立に処理するステップ完全形式化 (0.072) などのベースラインをほぼ超え, 0.545のProofScoreを実現した。 私たちのパイプライン、ベンチマーク、スコアは、https://github.com/Huawei-AI4Math/ProofFlow.comでさらなる進歩を促すためにオープンソース化されています。

関連論文リスト

• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
  ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。 中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。 我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
  論文  参考訳（メタデータ） (2025-10-17T14:20:50Z)
• 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)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Improving Autoformalization using Type Checking [15.58948808529849]
  我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)

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

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