Organizations: Academy for Advanced Interdisciplinary Studies Peking University · School of Mathematical Sciences Peking University · Theory Lab, 2012 Labs Huawei Technologies Co., Ltd. · Beijing International Center for Mathematical Research Peking University
Large language models can now generate complex, multi-step mathematical proofs, but reliably determining their correctness and localizing early logical errors remains a critical challenge. Existing evaluation approaches largely depend on model-based natural-language judgments, which often overlook local reasoning gaps. While formal theorem provers like Lean offer a path to rigorous verification, using them to evaluate informal text requires solving locality and semantic mismatches: a prover might bypass a local flaw by proving an overly broad target, or validate an auto-formalized statement that drifts from the original mathematical intent. To address this, we introduce FaithSieve, a Lean-assisted framework for fine-grained evaluation of natural-language mathematical proofs. FaithSieve decomposes coarse proof steps into local reasoning units, extracts typed proof obligations, and verifies them through a formal evaluation agent. Formal validation is gated by semantic alignment scoring, so Lean evidence is incorporated only when the formal statement faithfully preserves the context, objects, and logical form of the original claim. We construct two expert-verified datasets, ProofLoc-Olympiad and ProofLoc-University, to benchmark first-error localization. On the 350-problem Olympiad dataset, FaithSieve using a GPT-5.4 backbone achieves 81.43% exact first-error accuracy, outperforming the direct-judging baseline of 72.29%. Furthermore, on the 200-problem ProofLoc-University benchmark spanning six advanced domains, FaithSieve reaches 84.5% exact accuracy, compared to 75.0% for the direct judge. Our work demonstrates that decomposing proofs into fine-grained units and grounding them with faithful formal evidence significantly improves reliable evaluation of natural-language reasoning.
Figures & tables
Figure 1: Overview of the FaithSieve workflow for Lean-assisted first-error localization.
Figure 2: From Proof Steps to a Tree of Proof States
Type
Local check
Trigger
Derived fact
New fact follows from context
Implication to new claim
Rewrite
Rewrite or calculation is valid
Equivalent rewrite or simplification
Goal reduction
After-goal implies before-goal
Sufficient condition for goal
Fact plus reduction
New fact and reduction are valid
Claim + goal change
Case split
Cases are valid and covering
Case analysis
Branch elimination
Discarded branch is impossible
Infeasible branch
Table 1: Typed obligation kinds for selected EdgeUnits .
Table 4
ProofLoc-University
ProofLoc-Olympiad
Base model
Params.
Exact (%)
Binary (%)
Exact (%)
Binary (%)
GPT-5.4
undisclosed
75.00
87.00
72.29
88.29
Gemini-3.1-Pro
undisclosed
70.00
77.50
70.86
82.86
Opus-4.6
undisclosed
64.50
77.00
71.71
89.14
DeepSeek-v4-Pro
undisclosed
72.00
82.00
48.00
71.14
GLM-5.1
undisclosed
66.00
75.50
57.71
78.57
Table 4: Direct-judge base-model results on both datasets.
GPT-5.4
Qwen3.5-9B
Experiment
Exact (%)
Binary (%)
Experiment
Exact (%)
Binary (%)
Full FaithSieve
81.43
93.71
Full FaithSieve
74.00
89.14
Direct judge
72.29
88.29
Direct judge
53.71
76.00
Step3 graph judge
75.71
88.57
Step3 graph judge
65.71
77.71
EdgeUnit + NL only
73.43
88.00
EdgeUnit + NL only
71.14
86.00
w/o local EdgeUnits
60.86
72.29
w/o local EdgeUnits
62.29
77.71
Table 5: Ablation results on ProofLoc-Olympiad .
Appendix figures & tables15 assets
Supplementary material from the paper’s appendix.
Appendix
Domain
N
Source book
Author(s)
Topology / metric spaces
20
Topology [ Munkres, 2000 ]
James R. Munkres
Linear algebra
40
Linear Algebra Done Right [ Axler, 2015 ]
Sheldon Axler
Abstract algebra
40
Abstract Algebra [ Dummit and Foote, 2004 ]
David S. Dummit; Richard M. Foote
Real analysis
50
Analysis II [ Tao, 2016 ]
Terence Tao
Convex analysis
30
Convex Analysis [ Rockafellar, 1970 ]
R. Tyrrell Rockafellar
Convex optimization
20
Convex Optimization [ Boyd and Vandenberghe, 2004 ]
Stephen Boyd; Lieven Vandenberghe
Appendix
Table 6: Textbook provenance of ProofLoc-University .
Audit measure
Count
Result
EdgeUnit precision
174/(174+57)
75.32%
EdgeUnit recall
174/(174+93)
65.17%
Known-wrong first-error coverage
23/25
92.00%
Conditional first-error recall
23/24
95.83%
Appendix
Table 7: Human calibration of Suspicion Search.
Human judgment
Gate accept
Gate reject
Faithful
105
10
Unfaithful
13
7
Appendix
Table 8: Human calibration of the statement semantic gate on 135 statements.
Structure
Mean
Median
90th percentile
Raw proof-state nodes
16.81
15
28
Normalized non-placeholder EdgeUnits
15.59
14
27
Search-selected candidates
4.91
5
7
Appendix
Table 9: Tree and candidate sizes on the complete Olympiad-350 artifacts.
ProofLoc-Olympiad
ProofLoc-University
Setting
Exact (%)
Binary (%)
Setting
Exact (%)
Binary (%)
Direct (GPT-5.4)
72.29
88.29
Direct (GPT-5.4)
75.00
87.00
FaithSieve (GPT-5.4)
81.43
93.71
FaithSieve (GPT-5.4)
84.50
92.50
Direct (Qwen3.5-9B)
53.71
76.00
Direct (Qwen3.5-9B)
61.00
76.50
FaithSieve (Qwen3.5-9B)
74.00
89.14
FaithSieve (Qwen3.5-9B)
69.50
78.50
Appendix
Table 10: Main FaithSieve results.
Variant
Decomp./graph
EdgeUnits
Local NL review
Cheap/Lean evidence
Semantic gate
Evidence fusion
Direct judge
No
No
No
No
No
No
Step3 graph judge
Yes
Graph-level only
No
No
No
No
EdgeUnit + NL only
Yes
Yes
Yes
No
No formal gate
Yes
w/o local EdgeUnits
Yes
No / coarse-step
Partial
Yes
Yes
Yes
w/o semantic gate
Yes
Yes
Yes
Yes
Disabled or loosened
Yes
Full FaithSieve
Yes
Yes
Yes
Yes
Yes
Yes
Appendix
Table 11: Component configuration of ablation variants.
Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most proofs, particularly those written by AI systems, have neither property, and translating them into formal languages remains challenging in many frontier math settings. We propose Pseudo-Formalization (PF), a proof format that captures the modularity and precision of formal proofs while retaining the flexibility of natural language. A Pseudo-Formal proof is decomposed into self-contained modules, each stating its premises, conclusion, and proof in natural language. To verify the correctness of a regular natural language proof, an LLM translates it to Pseudo-Formal and then verifies each module independently, an algorithm we call Block Verification (BV). We evaluate PF+BV on two benchmarks spanning olympiad and research-level mathematics, where it pareto-dominates LLM-as-judge baselines on error-finding precision and recall. To support future work, we release our research-level proof verification benchmark ArxivMathGradingBench.
Large Language Models (LLMs) struggle to rigorously verify complex mathematical proofs. Standard global evaluation approaches suffer from "context poisoning," in which superficially plausible statements mask subtle logical flaws, leading to hallucination or over-skepticism. To address this, we shift from global evaluation to strict step-level verification: our framework maintains detailed context for each deduction step and strictly constrains the sources of applied theorems. We evaluate on a carefully curated adversarial diagnostic suite of research-level proofs drawn from the FirstProof challenge. A systematic ablation study demonstrates that these deductive constraints are indispensable, as unconstrained global prompting consistently fails to localize subtle logical errors. Beyond outperforming global evaluation, our approach fundamentally alters the failure taxonomy. Error analysis reveals that, rather than exhibiting severe logical hallucinations, remaining rejections are primarily instances of "pedantic hyper-rigor" stemming from unstated domain conventions, effectively exposing implicit ambiguities within the expert benchmark itself. Our findings suggest that prompting agents to organize their verification notes in a cautious, human-mathematician-like manner can substantially improve their ability to distinguish rigorous proofs from flawed ones, with the potential to strengthen agentic reasoning on frontier mathematical concepts that the base model does not already know well, and to lay a theoretical foundation for future automated proof-review systems. Code and prompts are available at GitHub.
Large language models (LLMs) are increasingly capable of mathematical problem solving and can even assist with research-level proofs, yet we still lack a scalable and reproducible way to measure step-level reasoning in long proofs across diverse sources. This evaluation gap limits trustworthy AI assistance in proof-certified scientific progress. Existing evaluations often emphasize final answers or rely on costly expert grading, while end-to-end proof generation remains open-ended and hard to verify automatically. We introduce Mask-Proof, a pipeline that turns real proofs into automatically checkable masked-step tasks. It masks key formula steps, provides the necessary surrounding context, and evaluates model reconstructions with an LLM-based equivalence judge using repeated votes for stability. The resulting Mask-ProofBench contains 292 curated problems across diverse research areas. Experiments with 17 models show that reasoning-enhanced models outperform standard models by 12% to 27%. Our evaluator achieves 96.8% agreement with expert annotators, enabling faithful, reproducible, and comparable measurement of step-level mathematical reasoning. Benchmark, annotations, and code are available at https://github.com/weating/Mask-Proof.
Jierui Zhang, Siyuan Tan, Xinhang Li +8
School of Computer Science Beijing University of Posts and Telecommunications Beijing, China · Graduate College for Engineers Beijing University of Posts and Telecommunications Beijing, China · School of Mathematical Sciences Fudan University Shanghai, China +6