ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization

TL;DR

This work tackles faithful autoformalization of natural-language proofs by preserving their logical structure through a DAG-based, lemma-centered pipeline called ProofFlow. It introduces a three-stage architecture (Graph Builder, Formalizer, Tactic Completer), a composite ProofScore metric combining structural fidelity, syntactic correctness, and semantic faithfulness, and a publicly available ProofFlowBench benchmark of 184 undergraduate proofs. Empirical results show the DAG-enabled ProofFlow surpasses baselines, achieving a ProofScore of about 0.545 and demonstrating stronger structural fidelity and syntax correctness than monolithic or step-wise tactic approaches. The framework and benchmark enable reproducible evaluation and pave the way for more reliable, verifiable autoformalization workflows in formal mathematics.

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.

Figures (9)

• Figure 1: Comparison of our ProofFlow "Lemma Approach" and the common "Tactic Approach" in formalizing a natural language (NL) theorem and its proof into Lean 4 code. The Lemma Approach directly mirrors the sequence of steps and their dependencies in the NL proof. By contrast, the Tactic Approach produces tactics that fail to adhere to the structure of the initial NL proof.
• Figure 2: Comparing structural fidelity in automated proof generation. (a) A scenario for the problem in Figure \ref{['fig:autoformalization_task']}, where the dependency graph fails to adhere to the structure of the original proof. (b) This benchmark problem was intentionally formalized without enforcing a DAG. This approach sacrificed structural fidelity, by reusing lemma L1 to prove L3, thereby rendering L2 redundant.
• Figure 3: Our proof autoformalization pipeline with three parts: (1) Graph builder; (2) Lemma Formalizer; and (3) Tactic Completer. Lean errors are verified by the Lean 4 compiler.
• Figure 4: An example of the interactive visualization generated by ProofFlow. Node contours signify the outcome of each step: Red for a formalization error, orange for formalized statement without Lean 4 tactics, and green for formalized statement with Lean 4 tactics.
• Figure 5: Flowchart illustrating the error detection mechanism. This is applied lemma by lemma and $f_i$ is the semantic faithfulness of node $v_i$ (between 0 and 1).