ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization

📄 arXiv: 2510.15981v1 📥 PDF

作者: Rafael Cabral, Tuan Manh Do, Xuejun Yu, Wai Ming Tai, Zijin Feng, Xin Shen

分类: cs.AI, cs.LO

发布日期: 2025-10-13

🔗 代码/项目: GITHUB

💡 一句话要点

提出ProofFlow，通过依赖图提升定理证明自动形式化的语义忠实度。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 自动形式化 定理证明 依赖图 语义忠实度 结构保真度

📋 核心要点

  1. 现有自动形式化方法难以保持自然语言证明的语义和逻辑结构，导致形式化结果与原始证明不一致。
  2. ProofFlow构建依赖图来表示证明步骤间的逻辑关系，并使用基于引理的方法逐步形式化，确保结构保真度。
  3. ProofFlow在新的基准测试中取得了显著提升，ProofScore达到0.545，超越了现有基线方法。

📝 摘要（中文）

本文提出ProofFlow，一种用于定理证明自动形式化的新颖流程，旨在将自然语言定理和证明翻译成机器可验证的代码。现有方法侧重于生成可执行代码，但常未能保持原始论证的语义意义和逻辑结构。ProofFlow将结构保真度作为主要目标，首先构建有向无环图（DAG）来映射证明步骤之间的逻辑依赖关系，然后采用基于引理的方法系统地将每个步骤形式化为中间引理，从而保留原始论证的逻辑结构。为了便于评估，本文提出了一个包含184个本科水平问题的新基准，并手动标注了逐步解决方案和逻辑依赖图，同时引入了ProofScore，一种用于评估语法正确性、语义忠实性和结构保真度的综合指标。实验结果表明，ProofFlow在自动形式化方面达到了新的SOTA，ProofScore为0.545，显著超过了全证明形式化（0.123）和逐步证明形式化（0.072）等基线。

🔬 方法详解

问题定义：定理证明自动形式化旨在将自然语言描述的定理和证明转化为机器可验证的代码。现有方法主要关注生成可执行的代码，但忽略了对原始证明语义和逻辑结构的保持，导致形式化后的证明与原始证明在意义上存在偏差。这种偏差使得自动形式化结果难以被人类理解和信任，限制了其在数学研究和教育中的应用。

核心思路：ProofFlow的核心思路是将自动形式化过程分解为两个主要步骤：首先，构建一个有向无环图（DAG）来精确地表示证明步骤之间的逻辑依赖关系；其次，利用这些依赖关系，采用一种基于引理的方法，将每个步骤形式化为一个中间引理。通过这种方式，ProofFlow能够系统地保留原始证明的逻辑结构，从而提高形式化结果的语义忠实度。

技术框架：ProofFlow 包含以下主要模块： 1. 依赖图构建模块：该模块负责分析自然语言证明，识别证明步骤，并确定它们之间的逻辑依赖关系，最终构建一个有向无环图（DAG）。 2. 引理形式化模块：该模块根据依赖图的结构，将每个证明步骤形式化为一个中间引理。该模块利用大型语言模型生成候选引理，并使用形式化验证工具验证其正确性。 3. 证明组合模块：该模块将形式化后的引理按照依赖图的结构组合起来，形成完整的形式化证明。

关键创新：ProofFlow 最重要的技术创新点在于其对结构保真度的强调和依赖图的使用。与现有方法不同，ProofFlow 将保持原始证明的逻辑结构作为首要目标，并通过构建依赖图来显式地表示这种结构。这种方法使得 ProofFlow 能够更好地理解原始证明的语义，并生成更忠实于原始证明的形式化结果。此外，基于引理的逐步形式化方法也降低了单个步骤形式化的难度，提高了整体的成功率。

关键设计：ProofFlow 的关键设计包括： 1. 依赖图的表示方式：依赖图使用有向无环图（DAG）来表示，节点代表证明步骤，边代表逻辑依赖关系。 2. 引理形式化的策略：采用基于大型语言模型和形式化验证工具的混合方法，提高引理形式化的准确性和效率。 3. ProofScore 评估指标：ProofScore 是一种综合评估指标，用于评估自动形式化结果的语法正确性、语义忠实性和结构保真度。它综合考虑了形式化结果的多个方面，能够更全面地反映自动形式化方法的性能。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，ProofFlow 在自动形式化任务中取得了显著的性能提升。在新的基准测试中，ProofFlow 的 ProofScore 达到了 0.545，显著超过了全证明形式化（0.123）和逐步证明形式化（0.072）等基线方法。这表明 ProofFlow 在保持语义忠实度和结构保真度方面具有显著优势。

🎯 应用场景

ProofFlow 的潜在应用领域包括：数学教育、形式化验证、软件工程等。它可以帮助学生更好地理解数学证明，提高形式化验证的效率，并促进软件的可靠性。未来，ProofFlow 可以与自动化定理证明器结合，实现更强大的自动化数学推理能力。

📄 摘要（原文）

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.