ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
Authors: Rafael Medeiros Cabral
Tuan Manh Do
Yu Xuejun
Wai Ming Tai
Zijin Feng
SHEN XIN
Venue: ICLR 2026 Poster (2026)
Keywords: Autoformalization
Large Language Models
Dependency Graph
Lean (Formal Language)
Structural Fidelity
Semantic Faithfulness
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

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.279), which processes the entire proof at once, and step-proof formalization (0.046), 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.

Published as a conference paper at ICLR 2026
PROOFFLOW: A DEPENDENCY GRAPH APPROACH TO FAITHFUL PROOF AUTOFORMALIZATION
Rafael Cabral', Tuan Manh Do', Xuejun Yu', Wai Ming Tai', Zijin Feng", Xin Shen
"Huawei Celia Team
Huuwei Foundation Model Department shenxin 90huawei......................m. com
ABSTRACT
Proof autoformalization, the task of translating natural language theorems and proofs into machine-verifiabl code, is critical step for integrating large lan- guage models into rigorous mathematical workflows. Current approaches focus on producing executable code, but they frequently fail to preserve the seman- tic 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 directed acyclic graph (DAG) to map the logical dependencies between proof steps. Then, it employs 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- problems, manually annotated with step-by-step solutions and logical dependency graphs, and introduce PROOFSCORE, a new composite metric to evaluate syntac- tic correctness, semantic faithfulness, and structural fidelity. Experimental re- sults show our pipeline sets a new state-of-the-ar for autoformalization, achiev- ing a PROOFSCORE of 0.545, substantially exceeding baselines like full-proof formalization (0.279), which processes the entire proof at once, and step-proof formalization (0.046), which handles each step independently. Our pipeline. benchmark, and score metric are open-sourced to encourage further progress at attps://githus. com Huwewii http://hwww....oooooooaaaaaatttt
INTRODUCTION
The effort to automate mathematical reasoning is advancing on two key fronts. Recent advances in large language models (LLMs) have greatly enhanced their ability to solve mathematical prob- lems (Liang et al., (025). Meanwhile, symbolic engines such as Lean (Moura & Ullrich| 2021) and Isabelle (Hales et al. 2017) provide machine-verifiable frameworks that enforce strict logical cor- rectness. LLLMd automated theorem provers (ATPs), such as Goedel-Prover (Lin et al. 2025) and Kimina- Prover (Wang et al. 2025). generate formal proofs for problems that are written in symbolic language, which are then checked by the symbolic engine ensure logical correctness.
This paper studies automated proof formalization: the task of faithfully translating the natural lan- guage theorem and proof into machine-verifiable the aforementioned ATPs, where the goal is to discover a proof from an already formalized problem. Here, the goal is to translate existing proof, crucial step for verification in real-world mathe- matical workflows. After composing a proof, a mathematician may wish to formalize it to verify its correctness, uncover missing assumptions, of formal languages like Lean, a system that can automate this translation is highly desirable. The manual effort these automated proof formalizers seek to automate is immense, demonstrated by landmark efforts such as the Flyspeck project, which took over 20 years to formalize the Kepler conjecture (Hales et al., (017);: the Blue-Diamond project for the Polynomial Freiman-Ree -uzssa con- jecture (Tao) 2023); and the ongoing formalization of Fermat's Last Theorem (Buzzard & Taylor 2025), among other projects (Math Inc. 2025 Scholze. 2021
verifiable formal representation. This task is distinct from
fill logical gaps. Given the steep learning curve
Gonthier et al. 2013).
Corresponding author.

---

Published as a conference paper at ICLR 2026
NL theorem and Proof
Lean4: Tactic Approach
Lean4: Lemma Approach
Theorem: aorasi -xcxx"="""""""++ then X20.
(hecrem polenomia Jrequality (oiid ieatd ars 2.1%
Lo
Proof: (Coneagasttive) Suppose is not true that xed.
Then xxll, that i, x is negative. Cansequertly the
Presf contrspoative contrapooe
by
K.00
Jenls
sony
excressions xf, 72.. powers), 50 Sxcc.
all
(note
-n_negix
Ierma
Simblrly, the temms x1, st, and 6 are al postive (nore
int6h_ P_Peg
(es)
< 75r8 5
powers), 0ixe 6
Inanth
x<0 2n5 -h romy
from this we get =exex" +4x+00, so it not true
x >xx-8
pow, .ig. cl. Leg it neg
mut mog. ple of nng lshow [ij from by
mumm (pno) meg (shoe
-55 c
from
[tS]
norii, (umi Iu jnog.
60
x=0 1874 0 00 bymy
pos, prom jieg pou mpr tu megi 6, nugge 2
pow, joom O from
Dependency Graph
(eal)
[LB (1 www.00000000...0000
x
sony.
Theorem concition
TC
TS
L1: Lemma
12: Lemma
Inma T5
(eal
L3 Lemma
cee0 (eMt 00
14: Lemma
Xg Par5 9w2.44 222+ 2-22---x000 By 2017
1S: Theorem Solution
Comparison of our PROOFFLOW "Lemma Approach" and the common "Tactic Ap- proach" in formalizing a natural language (NL) theorem and its proof into Lean code. The Lemma Approach directly mirrors the sequence of steps and their dependencies in the NL proof. By con- trast, the Tactic Approach produces tacties that fail to adhere to the structure of the initial NL proof.
Figure 1:
A key challenge in autoformalization is the fundamental mismatch between the flexible and high- level nature of human language and the rigid, low-level syntax of formal systems. To bridge this gap, ATPs typically generate "tactics" for formal proof assistants like Lean 4. However, this tactic- based approach often fails to preserve the logical structure of the original human argument. For instance, as shown in Figure [I] under "Lean 4: Tactic Approach", the generated tactics do not follow the sequence of steps in the natural language proof. Furthermore, single tactic, linarith, consolidates three distinct steps from the original proof (TS, 1.2, and I.4). This disparity creates two major issues. First, not all natural language mathematical expressions can be directly translated into low-level tactics, which can cause the formalization process to fail. Second, even if an automated system generates a verifiable proof, it may take shortcuts or skip intermediate steps, arriving at the correct conclusion without mirroring the explicit, step-by-step reasoning of the original proof. This makes it difficult to verify that the formal proof truly captures the human's intended logic.
To address these issues and ensure faithful autoformalization, we propose a novel approach that avoids direct translation into limited, low-level formal tactics. Instead, we deconstruct the natural language proof into a sequence of structured, high-level lemmas, as illustrated by the "Lemma Ap- proach" in Fig. [ The key advantage of this method is that it enables us explicitly follow the sequence of steps in the original proof with low friction" This stands in sharp contrast to the con- ventional tactic-based approach, which is often convoluted and hinders mirroring the human proof structure. Second, our lemma- based approach preserves the logical structure of the natural language proof by explicitly defining dependencies. As shown in Figure I the final step. lemma TS (the theo- rem's 's solution), depends only on lemma I.2 and lemma L4. This explicit dependency management crucial in enforcing structurally faithful formalization, which is often not achieved in a standard mucicc-bsee workflow. For instance, common tactic like "have" in Lean 4 feeds the entire preced- ing context to each new step, not just the specific premises required by the original proof logic. In contrast, our approach of explicitly defining how lemmas depend one another prevents the system from incorrectly using unintended dependencies, a common failure in tactic-based proving. These two innovations, high-level lemma generation and explicit dependency tracking, form the core of our new autoformalization pipeline, PROOFFLOW.
Another primary challenge is defining what constitutes "faithful" formalization. In existing work, researchers either focus on syntactic correctness (Hu et al. 2025), i.e., no compilation errors, or
While we currently use the placeholder "by sorry" for unproven parts, our ultimate goal is generate Leann tactics prove each lemma and the final solution.
2

---

Published as a conference paper at ICLR 2026
simple BLEU score for semantic measurement (Poiroux et al. 2024 Wu et al. 2022) while ignoring the structural fidelity of the proof. To properly evaluate proof formalizations, we propose viewing proof not monolithic block of text, but structured sequence of theorem condi- tions, definitions, and lemmas that form a logical progression toward the final theorem solution or solutions (see Figure T). Based on this, introduce new and more comprehensive proof autofor- malization scoring metric (PRoOFSCORE) and we also address the lack of an advanced benchmark by providing new university-leve dataset tailored for this task (PROOFFLOW BENCH).
Drawing on our new framework, we make the following key contributions:
PROOFFLOW: In Section 3 we propose a novel pipeline for translating natural language theo- rems and proofs into structured and formal Lean code, ensuring the preservation of the proof's logical structure. When formalization step fails, the pipeline identifies the error source, be it in the formalization, the tactic completion process, or the initial NL statement, thereby alerting mathematicians of potential flaws in their original proof.
PRoorSCORE: Section 4 introduces new and comprehensive scoring method evaluate the quality of autoformalized proofs. This metric is the first to explicitly measure syntactic correct- ness, semantic faithfulness, and structural fidelity, providing a more complete assessment than existing methods.
PROOFFi.ow BENCH: In Section 5
we present a new, manually curated benchmark dataset for proof autoformalization, containing a collection of 184 undergraduate level problems.
Comparative Study: 6 empirical study using state-of-the-an models to evaluate our structure-aware pipeline, PROOFFLow, against alternative strategies. The results show that PROOFFLOw has significantly higher proof autoformalization quality.
2 BACKGROUND AND RELATED WORK
Proof assistants and automatic theorem proving: Proof assistants like Isabelle (Paulson 1994), Lean 4 (Moura & Ullrich 2021), and Coq (Barras et al. 1997) are software environments for devel- oping and verifying mathematical proofs. Proofs constructed within these systems are what we call "formal" proofs, distinguishing them from informal or natural language proofs written in standard mathematics (e.g., in LITBX). The user's workflow involves interactively applying tactics, which are small programs that perform logical inferences, to solve the theorem's 's goals (Jiang et al., 2024). Despite their power, a steep learning curve and the significant manual effort required by their rigid syntaxes have hindered widespread adoption (Zhou et al.) 2024). Recently, Large I Language Models (LLMs) have emerged as powerful automated theorem provers (ATPs) capable of generating com- plete formal proof' from already formalized theorem statements (Shang et al. 2025 Lin et al. 2025 Ren et al. 2025). Proof Agents have further advanced this ability (Chen et al,, Zhou et al. 2025 Baba al.. 2025). In the context of Figure [ the task of an ATP is to
Wang et al.
2025
2025
automatically replace the placeholder command "sorry" with formal tactics to complete the proof.
Autoformalization with LLMs: For fully automatic theorem-proving system, mathematical prob- lems originating in natural language must first be translated into a formal language, a process known as autoformalization. Historically, autoformalizatio efforts have primarily focused on translating theorem statements, and not the natural language proof (Huang et al.] 20255] Wu et al. 2025 Liu
al. 2025 Yu et al., 20255 Poiroux al. 2024 Pathak 2024 Patel al.] 2023), often support the training of automated provers (Lin et al.) 2025 Wang et al.) 2025). A different approach uses informal proof sketches to guide an LLM's search for formal proof (Cao al. 2025 Zhou al.,
2024 Jiang et al., 2023). In these methods, the natural language proof sketch is not the target of formalization itselt. Rather, it serves as high-level guide, often interleaved as comments within the formal code to steer the generation process. This guidance technique is also employed by recent ATPs like DeepseekProver-VV V2 (Ren et al. 2025) and Goedel Prover V2 (Lin et al. (025).
Proof Autoformalization: In the literature of proof autoformalization. most existing attempts di- rectly translate entire proofs using LLMs (Gao et al. 2024 Lu et al. 2024 Cunningham et al. 2023). This approach, however, remains highly challenging due frequent syntactic errors and it often pro- duces outputs that are not semantically trustworthy. Step-level formalization, which involves solving the autoformalizatio step-by-step based on the proof's logical steps, has been explored by Hu al.
3

---

Published as a conference paper at ICLR 2026
StepProof formalization
Theorem
TC1
is odd
Suppose n is an odd integer. Show that (mod 8)
TC
L1
L2
L1
n = 2k+1
k integer
Prover allowed
any subgraph
n²2 4k*2 4k+1
k(k+1) 1) even
L4
k(k+1) 2m
L5
n 4k(k+1) +1
integer
L1
L3
L2
L4
L2
L4
L4
L6
n^2 8m+1
TS
(mod 8)
(a)
(b)
Figure 2: Comparing structural fidelity in automated proof generation. (a) A scenario for the prob- lem in Figure [1] where the dependency graph fails to adhere to the structure of the original proof. (b) This problem was intentionally formalized without enforcing DAG. This approach sacrificed structural fidelity, by reusing lemma L1 to prove L3, thereby rendering L2 redundant.
2025) in Isabelle. However, this approach suffers from two limitations. First, they treated all pre- Vious proof steps valid premises for the current step, significant simplification that overlooks the proper logical structure. Second, their evaluations focused solely on syntactic correctness while overlooking semantic consistency.
PROOF AUTOFORMALIIATTIO
Although most prior work formalizes entire proofs once, notable exception is the "STEP PROOF" method (Hu et al. 2025). This approach assumee each proof step depends on all preceding steps, simplification that creates unfaithful dependency structure and can lead to ATP taking "shortcut." This shortcut may involve using only the initial theorem conditions or an incorrect subset of lemmas to construct a valid proof that does follow the logic of the original NL proof, as depicted in Figure 2a A clear example found in PROOFFLOW BENCH is illustrated in Figure 2b In the natural language proof, step L3 directly uses the outcome of L2, which is faithfully followed by our DAG-enforcing pipeline. By contrast, an ablated version of our pipeline which lacks the mechanism enforce the correct dependencies (noDAG) reuses the outcome of LI prove L3, despite having proven 1.2. Thus, it not only dissipates step L. but also disregards the structure of the original proof. More details and examples are found in Appendix A.5 If the sole objective is to find any correct formal proof for theorem, which is often the sole goal of ATPs, these behaviors are not problematic. However, for proof autoformalization, they represent critical failure of faithfulness. Our goal is to ensure that each step is proven only taking into account the correct set previous lemmas and theorem conditions specified by the original proof's logic. Enforeing this correct dependency structure offers significant practical advantages well. improves efficiency by constraining the autoformalizer's search space, which can lead to fewer spent tokens and faster verification.
4

---

Published as a conference paper at ICLR 2026
Graph Builder
Tactic Completer
NL Proof
Yes (relty proving)
Theorem: Suppose A and
TC1
L1
tactics
LLM
TS
Jemma L2
Since AB=l and dat[]]=1 know
Proof:
TC2
Lean errors?
(TC2:A 1)
dat A del =
LLM
no [-ddel mut TC2.
Node dictionary
Original statement: |A|B|-11
Formalizer
No
L2
Depandancies: (TC1. TC2]
Formal lamma
Self-contained statement:
LLM
Lean errors?
We assume:
(AB: Marrik n ITC2:A 8 1): der dat B by sorry
-A. B are n square matricos (TC1)
AB [TC?]
Therefore we condlate:
Yes (retry formalization)
Figure 3: Our proof autoformalization pipeline with three parts: (1) Graph builder; (2) Lemma Formalizer, and (3) Tactic Completer. Lean errors verified by the Lean 4 compiler.
3.1 NEW WORKFLOW FOR PROOF AUTOFORMALIZATION
As shown in Figure our method enforces correct dependency graph through a three-stage pipeline, leveraging LLMs at each step to bridge the gap between natural language (NL) and formal proof code. The first stage, Graph Builder, constructs a dependency directed acyclic graph (DAG) from the original proof. Next, the Formalizer uses an LLM to translate each proof step into formal Lean code. Finally, the Tactic Completer fills in the necessary tactics to complete the Lean proof. The specific LLM models used at each stage are detailed in Section 6
This step parses the natural language (NL) theorem and its proof to construct dependency graph with LLM. Formally, this graph is DAG, G (V, E). where V is the set of all nodes and E' S V x V is the set directed edges. The nodes are partitioned into disjoint sets: V = Vrc UVD UVZ UVs, representing Theorem Conditions, Definitions, Lemmas, and Theorem Solutions, respectively. Each edge uu E E signifies that node u prerequisite for proving the statement of node From the theorem statement, we extract nodes for theorem conditions and theorem solutions. From the proof statement, we extract nodes for lemmas and extra definitions. Each node assigned its original NL statement, its dependencies, and self-contained NL statement that provides a complete description of the current proof step (see Figure 3). To ensure the graph's ' validity, the system checks for forward references and cycles and verifies that every node, except the theorem solutions, has an outgoing edge. If the check fails, we task the LIM to improve the graph.
Graph Builder:
Formalizer: For each node in the graph, the LLM formalizes its self-contained NL statement into Lean 4 code. This process is iterative: generated errors are fed back to the LLM for correction. At this stage, each lemma finalized with the "by sorry" placeholder, as tacties are not yet applied.
3. Tactic Completer: The final step completes the proofs for the lemmas by replacing the "by sorry" placeholders the formalized lean code with the appropriate Lean tactics.
To streamline the entire workflow illustrated in Figure we developed user-friendly Python pack- age for PROOFFLOW. This package automates the complete process, allowing users to provide an informal theorem and proof with just few lines of code. The package then autonomously exe- cutes the full workflow. It also integrates PROOFSCORE evaluation and our PROOFFLOWBENT benchmark for comprehensive assessment. The package is available at ht / trittuu thub. com/ [Huawei-a MateweeiAA4Math.. Pto.o/oooofooooooo with all the LLM prompts used this project included in the repository.
5

---

Published as a conference paper at ICLR 2026
ts_1
Type Solation
Toogl Info Panel
NATURAL LANGUWGE
Conditions
Definttoon
STATEMENT
Theorem Solutions
Uneow wassto a.
Formulization falled
noch than the all C.S.
Formalization passed
HCT
with XL01 ii
hover (PTH) You 1.1
Fully venfeed
[Lens Lbs cantinalito dat and 201
Staostoce, cssciades
Figure 4: An example of interactive visualization generated by PROOFFLOW. Node contours signify the outcome of each step: Red for formalization error, orange for formalized statement without Lean 4 tactics, and green for formalized statement with Lean 4 tactics.
The final output of our package is interactive diagram that visualizes the proof graph, seen in Figure 4 Users can click on each node to get detailed information about its results. The contours of each node provide an at-a-glance summary the outcomes, indicating whether its formalization and solving steps were successful. This allows users to immediately assess the progress of the autoformalization and pinpoint the locations the proof graph where manual effort is needed.
SCORING PROOF AUTOFORMALIZATION AND ERROR DETECTION
As discussed Section D a faithful autoformalization must satisfy three key properties: (1) Struc- tural Fidelity, which ensures the proof'ss dependency graph is preserved; (2) Syntactic Correctness, which ensures the output is verifiable code without compilation errors; and (3) Semantic Faith- fulness, which ensures each formalized statement accurately preserves the precise mathematical meaning of its original natural language statement.
4.1 PROOFSCORE
To evaluate the effectiveness of our PROOFFLOW pipeline, we introduce PROOFSCORE, a single unified score that synthesizes these three criteria.
Structural Fidelity is evaluated by checking whether the dependencies for given node are valid. For node 0ú we check if its estimated dependencies. (v;) = {u E Ves (u, v;) Eest match dependencies a ground truth graph. We permit several valid graphs (Gmm)) because the level of granularity can vary. For example, the calculation 1 + 13 = 14 + 5 19 could be broken down into either one or two steps, depending on the user's granularity preference.
Syntactic Correctness is denoted by c; E {0, 1]. where free of Lean 4 compilation errors at the end the Tactic Completer step and c; otherwise.
if the formalization of node it is
Semantic Faithfulness is assessed by adapting the "LeanScore" metric from Yu et al. (2025a) which was originally designed to evaluate the semantic faithfulness of theorem statement formal- ization. A detailed deseription is given in Appendix A.2 This metric provides faithfulness score, fi E [0, 1), for each node v, of the dependency graph, and this score measures the semantic equiva- lence between the input NI statement and its corresponding formalized Lean 4 lemma. The higher the score, the more faithful the Lean 4 lemma is to the input NI. statement.
The final unified PROOFSCORE, for proof with steps is computed as:
PROOFSCORE = Σ fs c (D)) E Dane (u:))

---

Published as a conference paper at ICLR 2026
Node is TS
Lean factics
Prove negation
NL statement error
cifi 0.6
Yes-
sucess
fallure V Tacific completer error
Formalizer error
No error
No error
Figure 5: Flowchart illustrating the error detection mechanism. This is applied lemma by lemma and fi is the semantic faithfulness of node oú and G; 0 if there syntactic errors.
where ProofScore E [0, 1]. and Pime is the set of valid dependencies for node step u, When the GraphBuilder is configured enforce the DAG structure, structural fidelity is guaranteed for all nodes. Otherwise, we use the Claude-Sonnet Sonnet-4 LLM with specialized prompt verify structural fidelity. This same LLM model also used to check for semantic faithfulness, utilizing prompts available within the PROOFFLOW package. Additional details about PROOFSCORE, including ex- amples of natural language proofs paired with their Lean code and respective scores, are provided in Appendix A.2
4.2 ERROR ANALYSIS
PROOFFLOW also has an error detection system operating at each proof step. This process (Figure 5) determines the error source, which can be the formalizer, tactic completer, or original natural language proof. First, proof node's semantic faithfulness score is compared against a 0.6 threshold, following Yu al. (2025a).
passes, the system checks if it's provable statement (lemma or theorem solution). Otherwise, the process for that node ends. For provable statements, the tactic completer attempts to apply Lean tactics. Success means the proof step complete with no errors. If the tactics fail, the LLM tries to prove the negation of the statement. If the negation can be proven, then the original natural language statement deemed imprecise. Otherwise, the error considered to be with the tactic completer LLM, which is incapable of either proving or disproving the step.
5 PROOFFLOOBENNCE
Existing mathematical benchmarks are often limited to pure calculation and are designed to test problem solving accuracy. Previous natural language proof datasets are also not self-contained, often referencing external sources for non-standard theorems (Welleck et al.) (021). Furthermore, they focus on specific topics and sometimes also including calculation problems instead of proofs (Sheng et al. 2025). To address these limitations, we introduce new benchmark, PROOFFI.OW BOOOFFFO.OBBEC,,H,... to specifically evaluate automated proof formalization pipelines. The benchmark, provided as part of the PROOFFLOw package, consists of 184 undergraduate--ever mathematics theorems and proofs in natural language from six key areas: number theory and algebra (27), real analysis (42), inequality (36), probability and set theory (31), complex analysis (25), and sequences and series (23). To construct this dataset, we adapted 63 problems from the NaturalProofs benchmark (Welleck et al. 2021 and 36 problems from the Ineq benchmark (Sheng al. 2025
The benchmark also contains the natural language proofs divided into proof steps, and the respective dependency graphs (DAGs), which can be used to evaluate structural fidelity. On average, each problem's graph consists of 8.4 total nodes (more statistics provided in Appendix A.3). The proof graphs have been manually validated. However, we emphasize that for the same proof different proof graphs are possible depending on the desired level of detail of each proof node.
6 COMPARISON STUDY
To evaluate our PROOFFLOW pipeline, we conduct a comparison study with three main objectives. First, assess the effectiveness of formalizing proofs using our high-level, lemma-based approach (PROOFFLOW) versus low-level tactics. This compares the "Lemma Formalization" (ours) with the "Tactic Formalization" (existing), as depicted in Figure Secondly, to examine the role of explicit
7

---

Published as a conference paper at ICLR 2026
dependency management in ensuring structural fidelity to the original proof, compare the DAG- enforcing version of PROOFFLOW with a variant where this is relaxed (noDAG). Finally, we conduct the error analysis of Section 4.2. to detect the source of errors in the PROOFFLOW pipeline variants.
6.1 EXPERIMENTAL SETTINGS
PROOFFL.OW: We consider the PROOFFI.OW variant that explicitly enforces the correct depen- dency graph as our main method, referred to as PROOFFL.OW DAG. To evaluate the role of this de- pendency enforcement, such mechanism relaxed. That is, in PROOFFLOW noDAG, all previous lemmas and premises are provided when formalizing each step, similarly to how dependency is handled by most prior work.
ablation study, we also consider PROOFFLOw noDAG version, where
Existing methods: We compare our pipeline against existing tactic- formalization methods: (1) "FULL PROOF" autoformalizationn (Lu et al., (024), which calls the LLM once to formalize the entire theorem and proof using Lean 4 tactics, and (2) "STEP PROOF" autoformalization (Hu et al,) 2025), which formalizes one proof step time into Lean 4 tacties. We note that STEP PROOF utilizes the same Graph Builder LLM and prompt as PROOFFLOW to decompose the initial NL proof into steps.
Thinking modes: All methods were evaluated in both thinking and non-thinking modes to pro- vide more comprehensive assessment. For existing methods, Koedel-Prover-V2-332 and Gemini- Flash-2.5 (Gemini Team 2025) are used for the thinking and non- non-thinking modes. For our PROOF- FLOW pipeline, the Graph Builder always uses Gemini-2.5-PP P.5-Proo the thinking mode utilizes Goedel- Formalizen-2-52B and froedel-Prover. Prover-V2-32B (L.in et al., 2025) as the Formalizer and the Tactic Completer, while non-thinking mode utilizes Gemini-2.5-Flass and DeepSeekProver V2 671B (Ren) for the two components. All LLM models were given appropriate system prompts.
al. 2025
Evaluation metrics: Our main evaluation metric in PROOFSCORE, supplemented by measures of syntactic correctness, both at step-level and proof-level. Step-level syntactic correctness of the gen- erated Lean 4 code is measured at two key stages: after the Formalizer step (Formalizer accuracy) and after the Tactic Completer step (Tactic accuracy). We also report proof-level "correct syn- tax", whether all of the formalizer and solver steps are syntactically valid. All syntactic correctness checks are verified by LeanServer (Santos et al. 2025) with Lean version v4. 15.0. We also adapted PRoOFScORE (Sect.Pe 4). so it could evaluate the FULL PROOF and STEP PROOF pipelines (see Ap- pendix A.2.2 for details). Finally, we report the elapsed time and the number of generated tokens. Since our experiments use both local and API-based model deployments, inference speeds vary. Therefore, the number of generated tokens is a more meaningful indicator of the effort required.
Data and reproducibility: We utilized the problems in the CROOFFLOWBENCE benchmark for this comparison study. Reproducible code is provided as part of the PROOFFLOW package.
6.2 EMPIRICAL RESULTS
The results evaluated at @ rate are presented in Table 1 This Pass@5 setting allows for up to five self-correction retries for each stage in the pipelines. If generated step produces syntacti- cally incorrect code, the model is re-prompted with the error and its previous output, giving an opportunity to fix the mistake. The results for Pass@1 and 3 are show in Appendix A.4
Existing Methods Comparison: The results clearly demonstrate that our pipeline outperforms ex- isting methods (FULL PROOF and STEP PROOF), achieving the highest PROOFSCORE (0.545). The FULL PROOF method calls the LLM once for the entire proof formalization and therefore we only report proof-level results. This approach achieves a comparatively high syntax passing rates (0.571 for the thinking mode), however, the PROOFSCORE was comparatively low, indicating that the gen- erated formal proofs, while syntactically correct, often fail to faithfully capture the structure and in- tent of the original natural language proof. The STEP PROOF method exhibits the lowest proof-level syntax passing rates (0.005 for the non-thinking mode and 0.119 for the thinking mode) because the LLM struggles to maintain correct and consistent indentation in Lean 4 across steps. Also, once an error appears in step, subsequent steps cannot achieve syntactic correctness. The poor syntax passing rates of the STEP PROOF approach results in correspondingly low PROOFSCORE values, given that this metric incorporates syntactic correctness as component.
8

---

Published as a conference paper at ICLR 2026
Table 1: Performance metrics under the Pass@5 setting on our 184-problem benchmark. Step-level averages are computed over all individual steps, while proof-level averages are computed per proof. Entries marked with "/" indicate not applicable.
Step-Level
Proof-Level
Think mode
Form. accuracy
Tactic accuracy
Proof Score
Correct syntax
Time (mins)
Output tokens (k)
Pipeline
PROOFFLOw
No
0.751
0.358
0.355
0.027
8.8
22.4
DAG
Yes
0.939
0.742
0.545
0.375
31.8
94.2
PROOFFLOw
No
0.807
0.391
0.347
0.049
12.3
25.8
noDAG
Yes
0,936
0.681
0.417
0.353
32.0
98.5
No
/
/
0.021
0.027
0.8
10.5
FULL PROOF
Yes
/
0.279
0.571
3.8
15.1
No
/
0.068
0.046
0.005
0.2
1.2
STEP PROOF
Yes
0.129
0.029
0.119
10.6
32.9
Ablation Study: The PROOFSCORE evaluation metric establishes the DAG version of PROOFFLOW the nop-performing method for proof autoformalization. This is most evident in the "thinking" mode, where the DAG variant achieves a PROOFSCORE of 0.545, compared to the noDAG's 0.417, due improved structural fidelity and syntactic correctness. While the DAG also outperforms the noDAG variant for all syntax metrics the thinking mode, we observed a higher syntax passing rate for the noDAG in the non thinking setting. This because the noDAG variant provides all previ- ous steps as known conditions to the LLM, and this extra information can lead to higher syntactic passing rates for weaker models, but often results a logically inconsistent formal proof structure, as shown by the lower PROOFSCORE averages. This finding underscores the critical importance of maintaining structural fidelity.
Alternative benchmark: We additionally validated our findings on the established miniF2F bench- mark (Zheng et al. (02T) by evaluating 50 randomly selected test problems. The results (Ap- pendix A.7) confirm that the relative performance ordering across all pipeline configurations is pre- served, with all accuracy indicators universally higher on miniF2F, indicating represents an easier evaluation setting.
Computational efficiency: Appendix A.8 provides a detailed breakdown of computational costs across pipeline components. Our analysis reveals that the Tactic Completer stage is the primary computational bottleneck, consuming 81-89% of total execution time across all configurations. A straightforward solution to address this bottleneck, enabled by DAG-based pipeline design, is parallelization. Our architecture naturally supports parallel execution at multiple levels: proof nodes in different branches can be formalized concurrently, and once formalized, tactic completion can proceed independently across nodes, In principle, our DAG design enables extensive parallelization that could substantially reduce wall-clock time. However, we did not implement parallelization in our experiments due to limited GPU resources, which restricted us to sequential processing.
6.3 ERROR ANALYSIS
The error analysis, shown in Table 2 identifies the Formalizer as the primary source of failure, accounting for 32% to 47% of all autoformalization outcomes, depending on the pipeline configura- tion. These failures are predominantly semantic, stemming from discrepancies between the natural language and the formalized Lean code, despite the high syntactic correctness (Table Our most robust configuration, which uses the PROOFFLOW DAG architecture in thinking mode, has 53.3% error-free free proof steps and clearly outperforms the 42.8% rate of the baseline (noDAG) version. This confirms that while the DAG architecture improves performance, improving semantic preservation during the formalization stage remains challenge for future work.

---

Published as a conference paper at ICLR 2026
Table 2: Breakdown of step-level outcomes for different pipeline configurations. "None" indicates the percentage of total steps completed successfully, while other columns show the percentage of steps that failed due to a specific error source.
Pipeline
Think
Total Steps
Error Source %
None
Formalizer
Tactic
NL Statement
PROOFFLOW DAG
No
1735
33.7
46.5
19.6
0.2
PROOFFLOW DAG
Yes
1737
53.3
38.9
5.6
2.2
PROOFFLOW noDAG
No
1751
32.8
45.6
21.4
0.2
PROOFFLOW noDAG
Yes
1755
42.8
47.0
7.6
2.6
The PROOFFLOW's error detection process goes beyond simple checks, being able, in some in- stances, identify spectrum of flaws the initial natural language proof. Examples are provided in Appendix[A.d These detected issues range from blatant algebraic errors to subtle ambiguities and unstated assumptions. By flagging these mistakes, pipelines like PROOFFLOW can provide feedback that not only helps correct errors but also strengthens the overall rigor and clarity of the proof.
DISCUSSION
Our results demonstrate the importance of preserving a proof"s structural fidelity. The PROOFFI.Ov lemma-based approach significantly outperforms both monolithic ("FulL PROOF") and sequential ("STEP PROOF") methods, which falter by tackling excessive complexity once by imposing linear structure unfaithful to the proof logic. Our method succeeds by using a lemma-based struc- ture that explicitly models the proof's dependency graph. This approach deconstructs the problem into manageable, logically-constrained steps. It guides the LLM along the author's intended path, preventing logical "shortcuts" that undermine other approaches. However, performance hinges on the Formalizer step, where poor semantic preservation remains the primary bottleneck.
limitation of our work was the exclusive focus on undergraduate-Ievel proofs, omitting research- level problems. However, this scope reflects the current capabilities of the field rather than intrin- sic limitations of the pipeline architecture we propose. Testing our system on more challenging research-lever problems did reveal the expected performance drop, consistent with observations across the literature (e.g.. (Jiang et al.] 20255). Critically, our pipeline's core contributions, the DAG-based lemma decomposition and structural preservation, are not the primary limiting factors. The main bottlenecks lie the underlying formalizer and tactic-completer LLMs, which currently struggle with research-leve concepts, and in MathLib's incomplete coverage of specialized mathe- matical domains. As these foundational components mature and the formal mathematics ecosystem grows, anticipate that pipeline's performance will naturally improve, providing scalable framework that is designed to grow more capable alongside these broader advances.
Our modular three-stage pipeline also enables the curation of high-qualing training data for both end- to-end proof autoformalization models and individual Formalizer and Tactic Completer LLMs, key direction for future work. Our error detection mechanisms can filter low-quality autoformalizations at different pipeline stages, creating curated datasets that support multiple training paradigms: su- pervised fine-tuning on the complete thain-of-thhuse reasoning process and reinforcement learning using detected errors as negative examples.
Ultimately, our work demonstrates that proof autoformalization an achievable goal: achieved 37.5% proof-level syntactic accuracy undergraduate problems, significant leap from existing approaches that only achieved 6.10% accuracy on simpler middle-schoo school mathematics (Hu et al., 2025). More importantly, we establish that for these tools to be truly useful to mathematicians, they must faithfully represent the structure and logic of human-created arguments they seek to formalize. Addressing the current bottlenecks could lead to practical tools that function as proof "auto-correct" for mathematicians, pinpointing errors and ambiguitics directly natural language and in real time.
10

---

Published as a conference paper at ICLR 2026
ETHICS STATEMENT
This research adheres to the ICLR Code Ethics and does not involve human subjects, privacy con- cerns, or ethical issues. The study uses only publicly available mathematical data, with no personal or sensitive data involved.
The proposed PROOFFLOW pipeline, PROOFSCORE metric, code, and datasets are designed sist mathematicians in theorem formalization, aiming to advance mathematical research and Al for mathematics. This work poses no foresecable harmful applications and contributes positively the scientific community by enhancing automated theorem proving capabilities.
REPRODUCIBILITY STATEMENT
To ensure the reproducibility of this work, we have made all necessary materials openly available. The complete implementation of the methodology (PROOFFLOw pipeline, PROOFSCORE metric), all experimental data, LLM prompts and comparison study code are publicly accessible through our package repository: https: /tt::/gitttts com/ Huawei AI 4M44tth/Proofff vided GitHub repository includes detailed instructions and documentation for replicating all experi- mental results presented this paper.
The pro-

---

Published as a conference paper at ICLR 2026
REFERENCES
Kaito Baba, Chaoran Liu, Shuhei Kurita, and Akiyoshi Sannai. Prover agent: An agent-based framework for formal mathematical proofs. arXiv preprint arXiv:2506. 19923, 2025.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Lean-Christophe Filliâtre, Eduardo Giménez, Héctor Herbelin, Gérard Mohring, Amokrane Saïbi, and Benjamin Werner The Cog Proof Assistant Reference Manual: Version 6.1. Technical Report RT-0203,, INRIA, 1997.
Kevin Buzzard and Richard Taylor. Towards Lean proof of Fermat's last theorem. Technical report, Imperial College London, 2025, Blueprint. Available at https:// github..hh....o 1o/.oIIII wttp:uu...o//////eeeeeeeeeee httpp//uppppp..............
Amperiaaccoleeeeeoeeoo
Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. Reviving dsp for advanced theorem proving in the era of reasoning models. arXiv preprint arXiv:2506. / 1487, 2025.
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23726 2025.
Garett Cunningham, Razvan C Bunesou, and David Juedes. Towards autoformalization of mathematics and code correctness: Experiments with clementary proofs. arXiv preprint
arXiv:2301.02//55 2023.
Guoxiong Gao, Yutong Wang. Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. arXiv preprint arXiv:2410. 10878, 2024.
Google Gemini Team. Gemini 2.5:
Pushing the frontier with advanced reasoning, multimodality. org/
long context, and next generation agentic capabilities, 2025. URL abs/2507.06255
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O' Connor, Sidi Ould Biha, at A machine-checked proof of the Odd Order Theorem. Lecture Notes in Computer Science, 8332:163-177 2013.
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaaghlin, Tat Thang Nguyen, et al. formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5, 2017.
Xiaolin Hu, Qinghua Zhou, Bogdan Grechuk, and Ivan Y. Tyukin. StepProof: Step-by-step veri- fication of natural language mathematical proofs, 2025. URL
org.abs/
2506. 10558
Yanxing Huang, Xinling Jin, Sijie Liang, Peng Li, and Yang Liu. Formarl: Enhancing autoformal- ization with labeled data. arXiv preprint arXiv:2508. 18914, 2025.
Albert Q. Jiang, Sean Welleck, Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs, 2023. URL http:/ttt////rtttt http://////aaa....o//////2220 12283
Albert Q. Jiang, Wenda Li, Mateja Jamnik, Sean B. Holden, and Lawrence C. Paulson. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. In The Twelfth International Conference on Learning Representations (ICLR), 2024. URL. httpt:ttt/:///t http::s////peereviieee net.
Forum??d=VV0Zzzome -
Jiedong Jiang, Wanyi He, Yuefeng Wang, Guoxiong Gao, Yongle Hu, Jingting Wang, Nailing Guan, Peihao Wu, Chunbo Dai, Liang Xiao, and Bin Dong. Fate: A formal benchmark series for frontier algebra of multiple difficulty levels, 2025. URL https: // arxiv. org/ abs 2511. 02872
Zhenwen Liang, Linfeng Song, Yang Li. Tao Yang. Feng Zhang, Haitao Mi, and Dong Yu. Towards solving more challenging imo problems via decoupled reasoning and proving. arXiv preprint (5t::2507.00804 2025.
12

---

Published as a conference paper at ICLR 2026
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge. Jingruo Sun, Jiayun Wu, Jini Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-Prover-V Scal- ing Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction, 2025. URL
https: Stttps://arxiie wwtparrwwwwww.aaaaaaaa/aooooaa//
org alss///s///at 2508 03613
Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data. arXiv preprint arXiv:2502.05567, 2025.
Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang. et al. Process-driven autoformalization in lean 4. arXiv preprint arXiv:2406. 01940, 2024.
Math Inc. The strong Prime Number Theorem. https://eeithb..ccommttttt
strongpnt] 2025. Accessed: 2025-09-11.
Leonardo de Moura and Sebastian Ulirich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pp. 625-635. Springer, 2021.
Nilay Patel, Rahul Saha, and Jeffrey Flanigan. A new approach towards autoformalization, arXiv preprint arX1v:2310.0795,, 2023.
Shashank Pathak. GFLean: An autoformalisation framework for lean via GF. arXiv preprint arXiv:2404.01234, 2024.
Lawrence Paulson. Isabelle: A Generie Theorem Prover. In Alan Bundy (ed.), Proceedings of the 12th International Conference on Automated Deduction (CADE-12), volume 814 of Lecture Notes in Computer Science, pp. 37 37-41. Springer, 1994.
Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bossclut. Improving autoformalization using type checking. arXiv preprint arXiv:2406.07222. 2024.
ZZ Ren. Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, al. prover---:: Advancing formal mathematical rea- soning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
Marco Dos Santos, Haiming Wang, Hugues de Saxcé, Ran Wang, Mantas Baksys, Mert Unsal, Jungi Liu, Zhengying Liu, and Jia Li. Kimina lean server: Technical report, 2025. httptt
//axiiv.org o225v...rg//b/2204..... 21230
Peter
Scholze. The Liquid Tensor Experiment at:
Xena Blog. 2021.
Avail-
able
http:///eenappjj.teoooooooe wot.rresssccoo.eeooooo com/ 2atnm/222105/111
the- hee_-uuuud--eess--ppeeeeeere
Shijie Shang, Ruosi Wan, Yue Peng, Yutong Wu, Xiong-hui Chen, Jie Yan, and Xiangyu Zhang. StepFun Prover Preview: Let's Think and Verify Step by Step. arXiv preprint arXiv:2507.20199 2025.
Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, and Pan Lu. Solving Inequality Proofs with Large Language Models. arXiv preprint arXiv:2506.07927 2025.
Michio Sugeno. Theory of fuzzy integrals and its applications. Doctoral Thesis, Tokyo Institute of Technology, 1974.
Terence Tao. Formalizing the proof of PFR in Lean4 using blueprint: a short tour. What's new Blog, 2023. Available at: http:///eeeryyttooooooeeeeee wttp:/ssscoomm///eeeee Formalizing the wwwttthheep-heeee ofte---oooooof----eee- -n--n-nd--eee------ a
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504 /1354 2025.
13

---

Published as a conference paper at ICLR 2026
Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. NaturalProofs: Mathematical Theorem Proving in Natural Language, 2021. URL https:
/aaxiv.org/abs////1.. 01112
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in neural informa- tion processing systems, 35:32353-32368 2022.
Yutong Wu, Di Huang, Ruosi Wan, Yue Peng. Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, et al. Stemfinn-ormalizer:: Unlocking the autoformalization potential of Ilms through knowledge-reasoningg fusion. arXiv preprint arXiv:2508. 04440, 2025.
Xuejun Yu, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haox- iong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, al. Mathesis: Towards Formal Theorem Proving from Natural Languages. arXiv preprint 2506::2500.00444 2025a.
Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al. Formalmath: Benchmarking formal mathemati- cal reasoning of large language models. arXiv preprint UrXiv:2505.02735, 2025b.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: cross-system benchmark for formal Olympiad mathematics, 2021.
Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, and Yuhuai Wu.
Don't Trust: Verify Grounding LLM Quantitative Reasoning with Autoformalization, 2024.
URL https::tt/axaiiii www.aaaxvvvv.....aaaaa...eaa org/ 22w0///////.......////// 18120
Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, et al. Solving formal math problems by decomposition and iterative reflection. arXiv preprint arXiv:2507. 15225, 2025.
14

---

Published as a conference paper at ICLR 2026
A APPENDIX
A.1 LLM USAGE STATEMENT
In this work, Large Language Models (LLMs) were employed in specific components of our research pipeline and experimental framework. The primary applications of LLMs include:
1. PROOFFLOW Pipeline Implementation: LLMs were utilized as core components within our proposed ProofFlow pipeline as Graph Builder, Formalizer and Tactic Completer.
Existing Methods Comparison: During the experimental evaluation, LLMs were employed to perform inference with existing methods for comparative analysis against our proposed approach.
PROOFSCORE Computation: LLMs were integrated into the calculation process of our pro- posed PROOFSCORE metric for quantitative assessment of formalization quality.
Benchmark Dataset Construction: The proof graphs included our benchmark dataset were initially generated by LLMs, followed by human verification.
LLMs served as computational tools in these specific applications and for grammatical correction of an early draft. All research idcation, methodological design, analysis, and interpretation of results were conducted exclusively by the human authors, who take full responsibility for the content of this paper, including any Mas--ssisteed components.
A.2 ADDITIONAL DETAILS ON PROOFSCORE
A.2.1 EVALUATION OF SEMANTIC EQUIVALENCE OF PROOFSCORE
In this section, we detail how obtain the semantic equivalence score Si of each node, proposed in Section 4 Note that by default, the score fi is O if the syntactic check at the formalizer step is not passed.
In particular, we assess the semantic equivalence between the self-contained natural language state- ment nls; and Lean code lc; of each node, which are the input and output of the Formalizer step of PROOFFLOW (Sect. 3.1). The process is as follows:
1. First, prompt LLM break down both nls; and le, into components.
We employ an jugeeee to evaluate the semantic equivalence between each formalized component, 1c, and its natural language counterpart, nls;, The LLM is provided with few-shot examples illustrating specific error types and assigns one of the following evaluations to each component:
Perfectly match: The component lc; fully captures the reasoning of nll;, It may include ad- ditional constraints or conditions that were implicit in the natural language but are necessary for formal rigor.
Minor inconsistency:
The component ic; correctly represents the core logic of nls; but may feature slight structural reordering or other small deviations.
Major inconsistency: The component lo; either omits key part of the logic from nils; or introduces entirely different reasoning.
3. A Fuzzy measurement score is then computed for each component based on these evaluations, following the method in Yu et al.) (2025a). This score is effectively a weighted average of the counts for "Perfectly match" and "Minor inconsistency." with zero tolerance for any component rated as a "Major inconsistency."
The final score, ft, calculated by aggregating the Fuzzy measurements using a Sugeno Inte- gral (Sugeno 1974).
In brief, the score fi of proof step is equal to 1 if the Lean code fully captures the self-contained natural language statement with all necessary conditions and f, is equal to if least one component of the Lean code contains major flaws.
15

---

Published as a conference paper at ICLR 2026
A.2.2 PROOFSCORE FOR FULL PROOF AND STEP PROOF
Our evaluation score, PROOFSCORE, is the average faithfulness evaluations of individual steps (nodes in the dependency graph) of our PROOFFLOw method. To create a fair comparison with FULL PROOF and STEP PROOF, we adapted this evaluation metric as follows. In all cases, any syntactically incorrect Lean code was automatically assigned score of 0.
Since this method generates single, complete proof for each problem, we applied the scoring process (detailed in Appendix [A.2.]] to the entire proof. The final score in Tables and the average score across all problems. Note that if the proof fails Lean syntactic check, the score is by default.
For FULL PROOF:
This method generates code for each individual step. Therefore, we applied the scoring process to each step independently. The final score in the tables the average across all individual steps from every problem in the benchmark. If any step fails Lean syntactic check, the score is by default.
For STEP PROOF:
The results of this comparative analysis are presented in Tables 1 and
A.2.3 RELIABILITY AND CONSISTENCY OF PROOFSCORE
As Claude is not involved in any module of the pipeline (Graph builder, Formalizer and Tactic Completer), employ Claude-Sonnet-4 evaluate the semantic faithfulness in PROOFSCORE.
To further validate the reliability PROOFSCORE, we compare it with variants (using Gemini- 2.5-Flash and DeepSeek-V3. in lieu of Claude) and merely Claude-as-a-ludge. While the variants of PROOFSCORE evaluate faithfulness on a component basis and aggregate using Sugeno Integral (see Sect. for Claude-as-a-Judge we prompt semantically equivalent to the natural language proof step.
evaluate directly whether the Lean code is
We employ these methods to evaluate sample of 200 natural language proof steps from our bench- mark and check their formalization faithfulness evaluations against the results obtained by a human expert. For human evaluations, the ground-truth label is "PASS" the Lean code is semantically equivalent to natural language and "FAIL" otherwise. Consistently with Section 0 for variants of PROOFSCORF, a proof score that larger or equal to 0.6 means the scorer method predicts "PASS", and the scorer predicts "FAIL." otherwise. On the other hand, Vlaude-as-a-Judge predicts "PASS"/FFAL" directly. We compute the Fl scores of these predictions versus the ground-truth labels.
The results are summarized in Table While the variants PROOFSCORE obtain close perfor- mances, they all achieve higher scores in judging semantic equivalence than Claude-as-a auddde These results suggest that PRoOFSCORE reliable in judging semantic faithfulness and this relia- bility is consistent across different Large Language Models.
Table 3: Comparison of Fl scores of variants PROOFSCORE by Claude, Gemini and DeepSeek and Claude-as-a-Iudge against human expert evaluations. All variants of PRoOFSCORE achieve higher level of correctness in judging semantic equivalence than Claude, demonstrating the reliability and consistency PROOFSCORE.
PROOFSCORE
PROOFSCORE
PROOFSCORE
Method
Claude-as-a-Judge
Claude (paper)
Gemini 0.88
DeepSeek
Fl -core
0.83
0.91
0.9
A.2.4 EXAMPLES OF PROOFSCORE RESULTS
To illustrate how PROOFSCORE behaves for each proof node, we provide several examples in Ta- bles Each example shows a natural language proof step paired with its formalized Lean code and the corresponding PRoOFSCORE. Note that display each proof step's 's individual contribu- tion to the overall PRoOFSCORE from Section that is, the product of terms within the summation (each term in the sum).
16

---

Published as a conference paper at ICLR 2026
In short, any Lean code is assigned score of 0 if either the code is syntactically incorrect or the tactics are structurally unfaithful to the proof step or there is at least one component that is significantly inconsistent with the natural language. By contrast, score means that all components of the Lean code match perfectly with their counterparts in the natural language proof step.
Natural Language
Lean code
Score and Explanation
From 2k + 1 [1I] and
Score O: structurally
n² = 4 + 4k + [12], we
lemma 13
unfaithful. The code to prove L3 only utilizes header by L1 while ig- noring L2, structurally unfaithful to the input NL proof.
conclude: n²² 4k(k (1]++)++1 [13].
(n : 2)
(tc_1
1)
(Example highlighted in Fig- ure 2(b)).
(11 $1exists$ k 2, 2+k + 1)
(12 : n 4 [Classical, choose 11) + *
Classical.chos 11) +
4 (Classical. 11
1 1* ([Classical. 11)
by have h = (Classical,
+ 1) +
choose 11) +1 by have h1 n. in= 2
Classical.cher choose 11) +
:= by exact classical choosee_pes 11 exact h1
have h:3 : n 2 = 4
Classical cetssical.ccccoe choose 11) 2 + 4 (Classical.che) choose 11)
:- by
have h4 : =
classical.choose choose 11) * ((
Classical.choose 11) + 1)
1 by
have h5 (Classical,
choose 11) 2
Elassical.cheoss 11) + 1
4 (Classical. choose 11)
[[Classical.chool 11)
1) + :- by ring_nf
linarith [h3, h5]
exact h4
We have: (c-2)2+10 (1) 1)2 5 and (x (x) + (iy-11= 1)2 5. So, 3.
theorem 13
Score wrong syn- tax. should be ": by sorry" but "= by sorry" was used. As the code fails Lean check (syn- tax error), the PROOF- SCORE
(x y R)
(11 : (x 22 + (y 1)
5)
(12
" ( 1)
5)
x 3 by sorry
Table 4: Examples of varying PROOFSCORE with natural language proof step and Lean code.
A.3 BENCHMARK DATASET STATISTICS
The distribution of the number of nodes per proof in the FROOFFLOWBENCH benchmark is shown in Figure 6 On average, the proofs have 2 theorem conditions, 0.6 definitions, 4.4 lemmas, and 1.2 theorem solutions.
17

---

by Published as a conference paper at ICLR 2026
Natural Language
Lean code
Explanation
Because (a - c), c
theorem 16
Score 0: major incon- sistency. The Lean code is syntactically correct but contains a major inconsistency the proposition. While NL has 2, the propo- sition in Lean has >. This results in Proof Score 0.
a). (c + a - b) > 0 and we
(a b c : R)
have: a² (a+c-b)(a+b-
(tc_1 a > 0 b
>
>
c), 02 2 (b+c-a](-aad)
a b
+
>
and c² 2 ac+t-aa(c+a-
b). Thus: d²b22² ca
(14
(b
+
(a + () + (b+
- a 0)
(c
a
b
cc b 6).
0))
(15 a >=
b) (a
b
+
a) (b
c"2 >= C)
(c + b a)
& (c b)
a-2
b-2
c02
(a
b)
(a + C)
(b 0
*
0) * (0
a) (c
b)
1 by
sorry
As the complex conjugate of 2 is & ig, we conclude:
theorem 13 (x y (z
Score 0.67: minor in- consistency. The Lean code is syntactically correct and equivalent the proof. The right- hand side of the propo- sition contains a slight variable ordering: (x+ 2y) vs. (2 * y + x) in Lean. However, this change is minor and still preserves the mantic meaning of the proof step.
h =
Comp Complex.c
(2-i)= = (2x 12x-y))i(x++))
:
(2 Complex.1) star 2 (2
y) Complex. (2
y x) = by sorry
Because (a c), c
Score 1: perfectly match. The Lean code is syntactically cor- rect and semantically equivalent to the proof step.
theorem 16 (a b
a), + a b) and we
B)
have: 2² (a+c-b)(atb-
(tc_1
> 0
b
>
c), b² (b+c-a)(--ac))
and c² 2 (c+b-a)(cta= a
c a b)
b). Thus: 2² 2 ta
(14 (a b
c
0)
(b
(a +b c)(b + -- d) () a) b).
0)
(c
0))
(15
a >=
(a
c
b) (a
b 6)
2
>=
(b +
a)
(b +
C)
c-2 >=
(c
a b c12
(a + 1 b)
* (a b
c)
(b +
a) (b
c) *
sorry
Table 5; Examples of varying ProofScores with natural language proof step and Lean code.
18

---

Published as a conference paper at ICLR 2026
Distribution of Total Nodes
Count of "Theorem Conditin" Nodos
Count "Dafiition' Nodes
35
Frequency
80
Frequency
100
30
40
20
25
Broquenyy
20
Count
Count
150
10
Fraquency
Frequenay
100
20
8 10 Total Nodes
12
13
15
17
6
10
Count
Gount
Figure 6: The distribution of the total number of nodes per problem (left) and the frequency of each node type (right).
A.4 COMPARISON RESULTS
This section contains extra comparison results. We show in Table extended version of Table which includes Pass @ and 5 rates.
A.5 COMPARISON EXAMPLES
In this section, present several examples of proof autoformalization illustrate how different pipelines perform when formalizing natural language proofs. The examples below, selected from comparative study in Section show how PROOFFLOW DAG maintains a high degree of fidelity to the input proof. In contrast, other approaches, such as PROOFFLOW noDAG, FULL PROOP, and STEP PROOF, often fail to either adhere the flow of the natural proof or even generate valid Lean 4 code.
To evaluate structural fidelity, we analyzed the dependencies for each syntactically correct proof step. By inspecting the Lean tactics, we identified exactly which previously proven steps and theo- rem conditions the solver utilized. A step was deemed structurally faithful this set of dependencies precisely matched the logic of the original natural language proof. If the dependencies differed in any way, the step was marked as unfaithful.
For the purposes of illustration, the figures presented in this section are based on the actual depen- dency graph of the input natural language proof, and annotations will be provided in the case the logical flow of the generated proof graph deviates from this input dependency graph.
A.5.1 EXAMPLE: PROOFFLOW DAG IS SUPERIOR IN STRUCTURE FIDELITY
This example corresponds to entry "dummy_6" -6" in the PROOFFLOWBENCH benchmark.
Theorem
n is odd integer, then n² (mod 8).
Proof
Since is odd, can write 2k + for some integer k. Then n² (2k + 1)2 4k2 + 4k + 1. We can factor this as n² = 4k(k + 1) + Now, either is even or à is odd.
If l is even, then &s 1 is odd, and if & is odd, then 1 is even. In either case, k(k 1) is even, so kck + 1) = 2m for some integer m. Therefore n? 4(2m) + = 8m + 1, which means n = 1 (mod 8).
19

---

Published as a conference paper at ICLR 2026
Table 6: Performance metries for all pipelines, evaluated @ass@1, 1, and rates on our 184-
problem benchmark. Entries marked with "/" indicate not applicable.
Step-Level
Proof-Level
Think mode
Form. accuracy
Tactic accuracy
Proof Score
Correct syntax
Time (mins)
Output tokens (k)
Pipeline
Pass
1
0.644
0.252
0.320
0.016
3.3
8.1
No
3
0.722
0.323
0.347
0.027
6.3
15.7
PROOFFLow
5
0.751
0.358
0.355
0.027
8.8
22.4
DAG
1
0.844
0.629
0.508
0.245
19.3
55.7
Yes
3
0.925
0.723
0.541
0.348
27.0
78.0
0.939 5
0.742
0.545
0.375
31.8
94.2
0.697
0.225
0.312
0.022
4.8
9.8
No
3
0.791
0.328
0.344
0.038
9.0
18.4
PROOFFLOW
5
0.807
0.391
0.347
0.049
12.3
25.8
noDAG
1
0.860
0.573
0.397
0.217
18.9
56.0
Yes
3
0.921
0.662
0,414
0.332
27.0
80.0
0.936 5
0.681
0.417
0.353
32.0
98.5
1
0.2
2.7
No
3
0.011
0.011
0.5
6.6
5
0.021
0.027
0.8
10.5
FULL PROOF
1
0.156
0.309
0.9
3.5
Yes
3
0.216
0.467
2.5
9.5
5
0.279
0.571
3.8
15.1
0.054
0.03
0.1
No
3
0.061
0.05
0.3
5
0.068
0.046
0.005
0.2
1.2
STEP PROOF
1
0.123
0.023
0.065
1.3
4.9
Yes
3
0.127
0.028
0.092
3.7
12.9
5
0.129
0.029
0.119
10.6
32.9
20

---

Published as a conference paper at ICLR 2026
Proof Graph (DAG)
k(k+1) even
k[k+ 2m integer
Theorem
n²2 8m+1
Suppose n is an odd integer. Show that n (mod 8)
TC
L6
TS
odd
n 2k+1 integer
n (mod 8)
n²2 4Kh1
n²2 = 4k(k+1)
Proof Graph (NoDAG)
k(k+1) 1)
k(K+1) in 2m integer
Theorem
m22 8m+1
L4
L5
Suppose add integer. Show that (mod
TC1
L1
L3
is odd
integer
(mod
n22 = 4kh1 4k+1
m^2
4k(k+1)
Figure 7: Comparison of proof structures generated by PROOFFLOW DAG (top) and PROOFFLOw noDAG (bottom) with respect the original natural language proof. The red arrow indicates dependency in PROOFFLOW noDAG not in the natural language proof. The blue dashed arrow indicates dependence in the natural language proof but not included in PROOFFLOW noDAG. The PROOFFLOW DAG formal proof faithfully follows the dependency of the original proof. However, the one by PROOFFLOW noDAG proves step L2 then reuses LI to prove L3, which is structurally unfaithful to the original proof.
The proof produced by PROOFFLOW DAG follows correctly the structure of the natural language proof and generates syntactically correct Lean code (see Figure 7
PROOFFLOW DAG:
PROOFFLOW noDAG: PROOFFLOW noDAG fails to adhere to the dependency structure of the
natural language proof. In particular, illustrated in Fig. 7 the transition from step L2 to L3 was inherent in the natural language proof but neglected in noDAG. The proof code for step L3 utilized step LI to reprove the result of step L.2. In other words, step L.2 made redundant.
FULL PROOF: FULL PROOF failed to generate syntactically correct Lean code (the first syntax error "unknown identifier").
STEP PROOF: STEP PROOF failed to generate syntactically correct Lean code for steps L4, LS, L6, and TS (the first syntax error "type mismatch").
A.5.2 EXAMPLE: PROOFFL.OWDAG IS SUPERIOR IN PROVER ACCURACY
This example corresponds entry "dummy 7" in the PROOFFL.OWBENCH benchmark.
21

---

Published as a conference paper at ICLR 2026
Theorem
If P(A) = 0.6 and P(B) 0.7, then P(An B) 2 0.3.
Proof
We know that P(AU B) P(B) P(An B). Since P(AU B) < 1, we have P(A) + P(B) P(An B) < Substituting the given values: 0.6 P.An-P(An B) - 1, which gives 1.3 P(An B) < 1. Therefore P(An B) 2 0.3.
Proof Graph (DAG)
PIA B) =PIAH P(B)
-PIAN B)
1.3-PrAn B)
Theorem
P(A) = 0.6, 0.7 So: ==
TS
L2
P(A) = 0.6. P
P(ANB) 0=
P(Au
PIA)P(()- P(AN8)<=
Figure 8: The structure of the proof produced by PROOFFLOW DAG faithfully follows the depen- dency graph the input natural language proof.
PROOFFLOW DAG: PROOFFLOW DAG generates step-by-step proof faithfully following the log- ical transition of the natural language proof (see Fig. (8)
PROOFFLOW noDAG: The Lean code proof achieves very low prover accuracy. This is likely
attributed to the fact that each step is given all previous steps, in contrast to only the necessary steps. As consequence, the prover fails to produce concise and correct Lean code.
FULL PROOF: FULL PROOF failed generate syntactically correct Lean code to prove this theo- rem (the first syntax error is "unknown identifier").
STEP PROOF: STEP PROOF failed generate syntactically correct Lean code prove this theorem (the first syntax error function type error).
A.5.3 EXAMPLE: PROOFFLow DAG IS SUPERIOR IN PROOF EFFICIENCY
This example corresponds to entry "dummy 9" in the PROOFFLOOWBENCH benchmark.
Theorem
(a,)) is an arithmetic sequence with a1 and 03 11, then as 17.
Proof
Since (a,,) is arithmetic, there exists a common difference such that a, aj + (n 1)d
for all n. From the given information, 0₁ + 2d. Substituting the values: 11 + 2d, which gives us 2d 6, so d Now we can find a5 a + 4d 5+3(3) 5 17.
PROOFFLOW LOW DAG: PROOFFLOW DAG generates step-by-step proof faithfully following the log- ical transition of the natural language proof (Fig. 9h.
22

---

Published as a conference paper at ICLR 2026
Proof Graph (DAG)
nnnea 14/n-1jd __3Fa_1+22 1+2d
a_ 1+4_
anthmetic
Theorem
L5
(a_n): arithmetic sequence, a_1 5, a_3 11, so a_5 17
L2
L3
L4
8 8_1=5 5, a_3=11 11
a_5
11 5+2d
2 6
d=3 3
Proof Graph (NoDAG)
a n 1+(n-1)d 3
(a n) is arithmetic
8 a_5-a_144d 1+4d
L1
Theorem
TC1
(a nj: arithmetic
sequence, a_1 = 5, a_3 a_55
TC2
TS
L3
a_15 5 a_3
a_5 = 17
11 5+2d
24
d
Figure 9: Comparison of proof structures generated by PROOFFLOW DAG (top) and PROOFFL.ow noDAG (bottom) with respect to the original natural language proof. The red arrow indicates dependency in PROOFFLOW noDAG not in the natural language proof. The blue dashed arrow indicates a dependence in the natural language proof but severed in PROOFFLOW noDAG. The one by PROOFFLOW DAG faithfully follows the dependency of the original proof. However, the one by PROOFFLOW noDAG proves the final step TS solely by the two given theorem conditions TC1 and TC2 and step L5. This is not only structurally unfaithful to the structure of the natural language proof but also inefficient the efforts to prove all intermediate steps L.,, L.2, L3, L.4 squandered.
PROOFFI.Ow noDAG: The Lean code proof by PROOFFI.OW noDAG is not only structurally un- faithful but also inefficient. As illustrated Fig. g the final step TS proven by the tactics stem- ming from theorem conditions TC1 and TC2 and intermediate step L5 (direct result of TC1) while neglecting all intermediate steps L1, L2, L3, L4. These steps are proven but not utilized for the final goal of the proof. As consequence, the logical flow of the proof by PROOFFLOw noDAG fails to adhere to the structure of the natural language proof and squanders the resources used to prove L1, L2, L3, L4.
FULL PROOF: FULL PROOF failed to generate syntactically correct Lean code to prove this theo- rem (the first syntax error is function type emror).
23

---

Published as a conference paper at ICLR 2026
STEP PROOF: STEP PROOF failed generate syntactically correct Lean code to prove this theorem (the first syntax error is function type error).
A.6 EXAMPLES OF ERRORS IN THE NATURAL LANGUAGE PROOF
The errors listed in Table 7 were identified using the thinking mode of our PROOFFLOW DAG pipeline at pass@5.. These examples detection pipeline (detailed in Section 4.2) flagged as an "NL statement error."
specifically extracted from proof steps that error
We have decided to keep these issues in the benchmark because they reflect the kinds of common and subtle ambiguities made by humans when writing proofs. For example, using ambiguous informal language like "we get [result x]" is frequent occurrence in practice. By including these ambiguities, we ensure the benchmark remains a realistic representation of human-written written proofs, rather than an overly artificial one.
Original Natural Language
Error Type
Comment
3a 3b b- 3ab² +3b (a² (a- b)
Incorrect Statement
An outright algebraic error. The left-hand side is exactly three times the right-hand side.
Let be a natural number. If is prime, we are done. If n is com- posite, then nt = ab ... By induction...
1,
Logical Flaw
The proof sketch is intuitively cor- rect but structurally flawed. It con- flates the base case and the in- ductive step of strong induction proof.
...we get + (r/2-1)2
Ambiguity
The phrase "we get" misleadingly suggests a general identity, when this actually conditional equa- tion that only holds for the specific value =
From the condition Arg(2) π T/6, we
Missing tion
Assump-
The statement is incomplete be- cause it relies on the unstated pre- condition that = + 0 for the Arg(z) function to be well-defined.
can write z r( /3 2) for some 0.
Hence, (X-Y)² < 11 because if not, then p would have two distinct real zeros...
Incomplete
Argu-
The reasoming, based on the dis- criminant quadratic, incom- plete it fails for the case where Y = O, where the polynomial de- generates.
ment
Integrating... yields v(x, v) = 2ay + 3y + g(x), where g(x) is function of ment
Incomplete
State-
The statement is true but insuffi- cient. In the context of solving a PDE, omits the crucial condi- tion that the function of integration g(x) must also be differentiable.
x.
Table 7: Analysis of Flaws Identified in Natural Language Proof Steps
A.7 EVALUATION ON THE MINIF2F BENCHMARK
To validate our findings on an established benchmark, we evaluated 50 randomly selected problems from the miniF2F test set (Zheng et al.) 2021). We focused on PROOFFLOw BBNCH pri- mary benchmark because it represents higher complexity for natural language proofs, where proofs average 637 characters, being 37% larger than miniF2F.
The results, presented in Table g confirm that the relative performance ordering of the different pipeline configurations preserved on this established benchmark. Crucially, all accuracy indicators were universally higher on miniF2F compared to PROOFFLOWBBNCCE indicating that miniF2F represents easier evaluation setting for proof autoformalization.
24

---

Published as a conference paper at ICLR 2026
Table @ performance of different pipelines on the miniF2F test set (sample of 50 problems).
Step-Level
Proof-Level
Pipeline
Think
Form. Acc.
Tactic Acc.
Proof Score
Correct Syntax
Time (min)
Output (k)
PROOFFLOW DAG
No
0.96
0.53
0.51
0.12
6.7
19.9
Yes
0.99
0.88
0.63
0.58
11.9
58.4
PROOFFLOw noDAG
No
0.94
0,46
0.46
0.08
9.7
23.6
Yes
0.98
0.83
0.53
0.50
11.8
57.9
STEPPROOF No
0.11
0.09
0.02
0.2
1.7
Yes
0,36
0.01
0.17
6.7
22.5
FULLPROOF No
0.12
0.14
0.8
10.7
Yes
0.38
0.86
2.0
7.2
A.8 COMPUTATIONAL EFFICIENCY
We provide comprehensive diagnostics of the pipeline by examining each subcomponent in detail. Table 2 presents key metrics across different pipeline configurations.
Our analysis reveals that the current pipeline bottleneck, in terms of both time and token efficiency, lies primarily in the Tactic Completer stage. The Graph Builder demonstrates high reliability, suc- ceeding on the first attempt most cases (1.01-1.08 tries per problem). contrast, the Formalizer typically requires 1-2 attempts depending on the thinking mode, while the Tactic Completer de- mands significantly more iterations, averaging 2-3 attempts thinking mode and 3-4 attempts in non-thinking mode per node to generate valid Lean code. The temporal distribution further empha- sizes this bottleneck: the Tactic Completer consumes 81-89% of the total execution time across all configurations, with the Graph Builder and Formalizer accounting for substantially smaller fractions.
Regarding token generation, we observe a difference between thinking and non-thinking modes. In thinking mode, the Tactic Completer dominates token usage (81-84%), primarily due to Goedel models generating substantial informal reasoning and extensive thinking before producing formal proofs. Conversely, in non-thinking mode, token distribution is more balanced, with both the Graph Builder and Tactic Completer each accounting for approximately 40% of tokens. This difference stems from the reasoning-heavy output of Gemini-2.55PPr in the Graph Builder stage, contrasting with DeepSeek-Provers which was instructed to minimize preliminary reasoning.
Table 9: Performance breakdown of ProofFlow pipeline components across different configurations. Metrics include average number attempts per component, time distribution percentages, and token usage distribution.
Metric Think Mode
ProofFlow DAG
ProofFlow noDAG
No
Yes
No
Yes
Average Attempts
Graph Builder (per problem)
1.08
1.08
1.01
1.01
Formalizer (per node)
2.20
1.39
1.94
1.37
Tactic Completer (per node)
4.04
2.39
3.69
2.67
Time Distribution (%)
Graph Builder
13.8
3.9
10.1
3.3
Formalizer
4.9
9.8
4.7
7.9
Tactic Completer
81.2
86.3
85.3
88.8
Total Time (mins)
8.8
31.8
12.3
32.0
Token Distribution (%)
Graph Builder
44.5
10.0
36.7
8.3
Formalizer
14.1
9.0
19.0
7.5
Tactic Completer
41.4
81.0
44.3
84.2
Total Tokens (k)
22.4
94.2
25.8
98.5
25


Reviews:
[{"review_id": "GfQcQqVaob", "reviewer": "Reviewer_2CoE", "summary": "The idea of this paper is to autoformalize proofs faithfully, meaning the semantic structure of the proof is maintained rather than just the correctness. The authors provide a new formalization pipeline called ProofFlow, in which they decompose the proof into a DAG where each node is a proof step, and edges indicate dependency. They also introduce scoring system to evaluate faithfulness (ProofScore), and a benchmark dataset of undergrad problems. They also conduct experiments to support their claims.", "questions": "L192: This approach assumes each proof step depends on all preceding steps, a simplification that can lead to unintended consequences.\n\nFigure 2: L3 typo, should be ^2 I think. Also, it seems to me that L3 is entirely redundant. Why not simply use L2 and L5 to get to L6? Is this a fault of the system(s) used? Possibly showing the full informal proof would be helpful.\n\nFigure 5: Could be the case that multiple errors occured, i.e. a NL statement error could be hidden behind a tactic completer error. Does this happen?\n\n* I'm confused on the ProofScore metric. When you say syntactic correctness, my understanding is that you are just concerned about whether a statement passes the Lean compiler, regardless of the \"fidelity\" to the original informal statement. For example, is \"theorem abc : True := by trivial\" considered syntactically correct?\n\n* I'm also not sure how to interpret the ProofScore metric. I think showing some examples of proofs with various proof scores would be useful to help readers understand how the numbers vary.", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 4, "strengths": "The paper introduces a novel approach to proof autoformalization which enforces structural fidelity. The authors make a good case for why this is an important problem, and why their proposed method would do so (if effective). Furthermore, the provided dataset and software seems like a useful contribution to the autoformalization/ATP community. Additionally, their pipeline and scoring metric both seem like reasonable and inuitive approaches to the problems.", "weaknesses": "I think while your method has merit, the comparisons to previous methods is not exactly fair. You are using a un-finetuned Gemini to formalize and prove proofs/steps for the previous methods, whereas ProofFlow uses much stronger, (nearly) state-of-the-art autoformalization/ATP models in the Goedel models. While this might be tricky for Full Proof (since Goedel models are not trained for proof-autoformalization), I think a more fair comparison for Step Proof would be \n\n1. Break down the proof into steps using the same model as you used for GraphBuilder\n2. Prove each step using Goedel Formalizer/Prover\n\nIn this way you're normalizing for the strength of the model to ensure you're comparing the method. Without this (or another way to ensure the model strength doesn't affect performance), the performance gain is difficult to believe. \n\nSecondly, ProofFlow requires significantly more computation than previous methods, which is a limitation of the work. I believe it would benefit from some analysis on computationally demanding elements of the pipeline (e.g., how many iterations is usually required to make a valid DAG in the GraphBuilder step?). This would offer some avenues for improvement to mitigate this limitation.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "gfA5kbjkls", "reviewer": "Reviewer_aiML", "summary": "This paper presents ProofFlow, a DAG-based framework for faithful proof autoformalization that decomposes natural language proofs into lemma nodes and translates them into Lean 4 via LLMs. It introduces ProofScore, a composite metric for syntactic, semantic, and structural quality, and a new dataset (184 undergraduate proofs). Experiments show its pipline outperforms Full-Proof and Step-Proof in accuracy and structural fidelity.", "questions": "Please refer to the Weakness section.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "1.\tThis paper introduces an appealing DAG-based, lemma-driven approach that preserves the logical structure of natural language proofs while improving interpretability and consistency.\n2.\tIt proposes ProofScore, a new metric capturing syntactic correctness, semantic faithfulness, and structural fidelity, providing a more rigorous evaluation.\n3.\tExperiments demonstrate improvements with ProofFlow, achieving a ProofScore of 0.545 compared to 0.123 (Full-Proof) and 0.072 (Step-Proof), validating its effectiveness and generalizability.", "weaknesses": "1. The Formalizer stage contributes to 32–47% of failures due to semantic mismatches between natural language and Lean 4 code, suggesting that its efficiency remains limited.\n2. Semantic faithfulness is evaluated through subjective LLM judgments without human verification or inter-rater reliability, which may introduce bias and reduce objectivity.\n3. Experiments are restricted to undergraduate-level proofs (average 8.4 nodes per proof, covering elementary topics), leaving the method’s generalizability to research-level or large-scale mathematical corpora untested.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "9KlE87WNQw", "reviewer": "Reviewer_VRSK", "summary": "This paper introduces PROOFFLOW, a three-stage pipeline for the proof autoformalization. The pipeline first constructs a directed acyclic graph (DAG) to represent the logical structure of the NL proof (Graph Builder), then translates each node into Lean 4 code (Formalizer), and finally generates tactics to complete the formal proof (Tactic Completer). To support this research, the authors also present two new contributions: PROOFFLOWBENCH, a benchmark of 184 undergraduate-level problems, and PROOFSCORE, a composite metric designed to evaluate the syntactic, semantic, and structural fidelity of the formalized output. The experimental results demonstrate that PROOFFLOW achieves a PROOFSCORE of 0.545, significantly outperforming the baseline methods considered.", "questions": "In the \"Structural Fidelity\" evaluation (line 297), the assessment appears to be based on a per-node check of dependencies. Have the authors considered a more holistic assessment of the entire proof structure, for instance, by employing graph structural similarity metrics?\n\nIn the experimental setup (lines 399-404), the paper defines \"thinking\" and \"non-thinking\" modes with different model configurations for the Formalizer and Tactic Completer stages. Could the authors elaborate on the rationale for selecting these specific model combinations? What hypotheses about model capabilities motivated these distinct configurations? From my understanding, I think it's just about using Gemini-2.5-Pro and Gemini-2.5-Flash in Graph Builder, while the model selection for Formalizer and Tactic Completer should be the same.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "- Systematic Pipeline Design: The paper presents a well-structured methodology. The PROOFFLOW pipeline thoughtfully deconstructs the complex task of autoformalization into manageable stages. The work is commendably thorough, extending beyond the pipeline itself to include the development of a new benchmark and a tailored evaluation metric.\n\n- Novel \"Lemma Approach\": A key contribution is the clear conceptual distinction between the conventional low-level \"Tactic Approach\" and the paper's high-level \"Lemma Approach.\" By demonstrating the superiority of preserving the proof's structure through intermediate lemmas, the paper offers valuable insights that could guide future research in faithful autoformalization.\n\n- Integrated Error Analysis: The inclusion of an error detection system is a significant strength. This mechanism goes beyond simple pass/fail metrics by attempting to diagnose the source of failure, attributing it to the formalizer, the tactic completer, or a potential flaw in the original NL proof. This diagnostic capability is a valuable feature for practical applications.", "weaknesses": "- Limited Evaluation Scope: The empirical validation is confined to the newly introduced PROOFFLOWBENCH. The omission of established benchmarks such as miniF2F and ProofNet, which also contain problems with NL proofs, makes it difficult to contextualize the performance of PROOFFLOW within the broader landscape of autoformalization research. A more robust evaluation would compare the proposed method against baselines on these widely recognized datasets.\n\n- Potential Metric Subjectivity and Lack of Validation: The proposed PROOFSCORE metric relies on an \"LLM-as-a-judge\" to assess semantic faithfulness, introducing a significant risk of subjectivity and unreliability. The evaluation is contingent on the specific LLM employed, and the paper provides no validation for this judge. The absence of an analysis measuring inter-rater reliability (i.e., consistency across different LLMs or against human experts) weakens confidence in the reported scores and the conclusions drawn from them.\n\n- Lack of Transparency and Potential for Data Contamination: The appendix notes that ground-truth dependency graphs for PROOFFLOWBENCH were generated by LLMs before human verification. The paper fails to specify whether the models and prompts used for this data generation are distinct from those used in the pipeline's Graph Builder stage. If they are not, this constitutes a form of data contamination, as the model would be evaluated on a task that closely mirrors its own data generation process. Furthermore, the complete omission of the prompts used for both the pipeline and the metric evaluation is a critical lapse in transparency that hinders the reproducibility of this work.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "F2OXbvb6H0", "reviewer": "Reviewer_hcof", "summary": "This paper focuses on the task of proof autoformalization, distinguishing it from automated theorem proving. The key difference is:\n\nAutomated Theorem Proving: A prover constructs a verifiable proof from a given formal statement.\n\nProof Autoformalization: The model is given both the natural language statement and its proof, and must translate this proof into a formal language while preserving its structure.\n\nThe paper introduces ProofFlow, a pipeline that utilizes a DAG (Directed Acyclic Graph) to ensure the final translated proof accurately preserves the logical dependencies between the original proof steps. This pipeline was evaluated on a new benchmark, where it demonstrated good performance.", "questions": "Do you think it is possible to train a model that can faithfully translate proofs into lean (not relying on your pipeline)? Is it possible to use your pipeline to curate training data for the training of proof formalizer?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "Regarding originality, this paper tackles the under-explored problem of proof autoformalization, specifically focusing on the requirement that the translated proof preserve its structure. This aspect is seldom noticed in previous ATP papers. Moreover, their proposal to use a DAG to address this task is of great novelty.\n\nThe paper also provides comprehensive explanations and evaluations of its idea and results. The overall quality and clarity are good, and the evaluations demonstrate that their pipeline achieves good performance.", "weaknesses": "No significant weaknesses.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)