論文の概要: 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でさらなる進歩を促すためにオープンソース化されています。
関連論文リスト
- Multi-Agent Procedural Graph Extraction with Structural and Logical Refinement [66.51979814832332]
モデル式は、専用の構造的および論理的洗練を伴う多ラウンド推論プロセスとして手続きグラフ抽出を定式化する。
実験により、モデルが強いベースラインに対して構造的正当性と論理的整合性の両方において大幅に改善されることが示されている。
論文 参考訳（メタデータ） (2026-01-27T04:00:48Z) - Training LLMs with LogicReward for Faithful and Rigorous Reasoning [75.30425553246177]
定理証明器を用いてステップレベルの論理的正しさを強制することでモデルトレーニングを指導する報酬システムであるLogicRewardを提案する。
LogicRewardで構築されたデータに基づいてトレーニングされた8Bモデルは、GPT-4oとo4-miniを11.6%、自然言語推論と論理的推論タスクで2%超えた。
論文 参考訳（メタデータ） (2025-12-20T03:43:02Z) - Translating Informal Proofs into Formal Proofs Using a Chain of States [20.0011959667642]
本稿では,自然言語で表現された非公式な数学的証明を,制約付き計算予算の下でLean4の形式的証明に変換する問題に対処する。
まず、中間形式的証明状態の列である状態の連鎖(CoS)を、非公式引数の論理構造に沿って抽出する。
次に、CoS内の隣接状態間の遷移戦略を生成し、完全な形式的証明を構築する。
論文 参考訳（メタデータ） (2025-12-11T06:08:34Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。
本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2025-10-29T15:30:31Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。