FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence

Ziyu Wang; Qiming Dai; Yishan Wu; Zaiwen Wen

cs.AIAug 26, 2026

FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence

Authors: Ziyu Wang, Qiming Dai, Yishan Wu, Zaiwen Wen

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

Abstract

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 .

		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.

GPT-5.4			Qwen3.5-9B
Variant	Exact (%)	Binary (%)	Variant	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

Appendix

Table 12: Ablation results on ProofLoc-Olympiad .

Dataset	Method	TP/TN/FP/FN	FPR	FNR
Olympiad-350	Direct@1	189/120/33/8	21.57%	4.06%
Olympiad-350	FaithSieve	189/139/14/8	9.15%	4.06%
University-200	Direct@1	66/108/22/4	16.92%	5.71%
University-200	FaithSieve	64/121/9/6	6.92%	8.57%

Appendix

Table 13: Complete GPT-5.4 correct/incorrect confusion matrices.

Dataset	Exact errors	FP	FN	Binary correct, location wrong
Olympiad-350	65	14 (21.5%)	8 (12.3%)	43 (66.2%)
University-200	31	9 (29.0%)	6 (19.4%)	16 (51.6%)

Appendix

Table 14: Composition of the remaining GPT-5.4 FaithSieve Exact errors.

Dataset / backbone	Method	$N$	Exact (%)	Binary (%)
University / GPT-5.4	FaithSieve	200	84.5	92.5
University / GPT-5.4	Direct@1	200	75.0	87.0
University / GPT-5.4	Direct@5	200	76.0	85.5
University / GPT-5.4	Two critics + adjudicator	200	76.0	86.5
BIG-Bench / Qwen3.5-9B	FaithSieve	200	61.0	74.5
BIG-Bench / Qwen3.5-9B	Direct@1	200	51.0	56.5

Appendix

Table 15: Additional natural-language baselines. The BIG-Bench Mistake result uses the tested 200-example subset.

Method	Model size	University Exact	University Binary	BIG-Bench Exact	BIG-Bench Binary
FaithSieve / Qwen3.5-9B	9B	69.5	78.5	61.0	74.5
Qwen3.5-9B Direct	9B	61.0	76.5	51.0	56.5
Qwen2.5-Math-PRM-7B	7B	47.5	64.0	56.5	74.0
Skywork-o1-Open-PRM	7B	47.5	64.5	14.0	61.0
EurusPRM-Stage2	7B policy + 7B reference	12.0	37.0	9.5	51.5

Appendix

Table 16: Off-the-shelf PRM transfer under the same first-error interface.

Model	Direct@1 tokens/problem	FaithSieve tokens/problem	Ratio
GPT-5.4	910.74	124,970.56	137.22 $\times$
Qwen3.5-9B	1,078.34	164,025.20	152.11 $\times$

Appendix

Table 17: Average recorded token consumption in the fixed 50-problem cost evaluation.

Method	Exact (%)	Binary (%)	FaithSieve token share
FaithSieve / Qwen3.5-9B	61.0	74.5	100.00%
Direct Majority@1 (pool mean)	51.6	55.7	0.42%
Direct Majority@3	52.2	55.5	1.25%
Direct Majority@5	52.0	55.1	2.08%
Direct Majority@9	52.0	54.6	3.75%
Direct Majority@17	51.8	54.1	7.08%

Appendix

Table 18: Same-data, same-backbone token-budget controls on BIG-Bench-200.

Domain	$n$	FaithSieve	Direct@5	Two critics + adjudicator
Topology	20	80.0 [58.4, 91.9]	65.0 [43.3, 81.9]	65.0 [43.3, 81.9]
Linear Algebra	40	100.0 [91.2, 100.0]	92.5 [80.1, 97.4]	95.0 [83.5, 98.6]
Abstract Algebra	40	97.5 [87.1, 99.6]	90.0 [76.9, 96.0]	87.5 [73.9, 94.5]
Convex Analysis	30	60.0 [42.3, 75.4]	50.0 [33.2, 66.8]	56.7 [39.2, 72.6]
Convex Optimization	20	80.0 [58.4, 91.9]	70.0 [48.1, 85.5]	55.0 [34.2, 74.2]
Real Analysis	50	80.0 [67.0, 88.8]	74.0 [60.4, 84.1]	76.0 [62.6, 85.7]

Appendix

Table 19: University-200 Exact accuracy with two-sided Wilson 95% confidence intervals.

Method / stage	Temperature	Max output tokens
Direct@1	0	64
Decomposition generation	0.3	default
Decomposition verification / deduplication	0.2	default
Informal-tree generation	0.7	default
Informal-tree verification	0.2	default
Suspicion Search	0.1	1600

Appendix

Table 20: Decoding configuration of the original University-200 experiment.

LLM Evaluation

Large language model evaluation measures what models can do, how reliably they do it, and whether benchmark scores predict real-world performance.

See all 2,408 papers

Pseudo-Formalization for Automatic Proof Verification
May 19, 2026Slim Barkallah, Luke Bailey, Kaiyue Wen +2Mathematical Reasoning Benchmarks LLM-as-a-Judge
Stanford University
Evaluating Research-Level Math Proofs via Strict Step-Level Verification
Jun 9, 2026Yifeng SunLLM Answer Verification Automated Theorem Proving
Independent Researcher
Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs
Jun 13, 2026Jierui Zhang, Siyuan Tan, Xinhang Li +8Mathematical Reasoning Benchmarks LLM Evaluation
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

May 19, 2026J/K move · Enter open · S save

Pseudo-Formalization for Automatic Proof Verification

Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid+1

Stanford University

Mathematical Reasoning Benchmarks LLM-as-a-Judge Autoformalization

Open paper AskPDF arXiv

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.

Abstract

LLM Evaluation

Explore similar work

Pseudo-Formalization for Automatic Proof Verification

Evaluating Research-Level Math Proofs via Strict Step-Level Verification

Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs