PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Ziyu Wang, Qiming Dai, Yishan Wu, Zaiwen Wen

arXiv:2608.26310v1cs.AI

TL;DR

Evaluating natural-language mathematical proofs requires locating local reasoning errors, while Lean can be misleading when formal targets are nonlocal or semantically misaligned. FaithSieve decomposes proofs into local units, generates typed obligations, and gates Lean evidence with semantic alignment; it improves first-error localization across two expert-verified benchmarks.

  • Problem

    Natural-language judgments can overlook local reasoning gaps, while direct Lean validation may verify a nonlocal or semantically drifted statement instead of the original proof claim.

  • Method

    FaithSieve decomposes coarse proof steps into EdgeUnits, extracts typed obligations, validates selected obligations, and filters formal evidence through semantic alignment scoring.

  • Results

    FaithSieve improves exact first-error localization over direct judging on PROOFLOC-OLYMPIAD and PROOFLOC-UNIVERSITY, including 81.43% versus 72.29% with GPT-5.4 on Olympiad.

  • Takeaways & Limitations

    Local reasoning units and faithful formal evidence support more reliable evaluation of natural-language mathematical reasoning.

  • Takeaways & Limitations

    Formal validation is limited by its cost, coverage, possible timeouts, dependence on LLM autoformalization and proof repair, and incomplete domain coverage.

Abstract

from arXiv · show

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.

1 Introduction

FaithSieve addresses the difficulty of evaluating multi-step mathematical proofs by combining fine-grained local analysis with Lean evidence gated by semantic faithfulness. It introduces expert-verified benchmarks and improves first-error localization over direct judging.

  • Natural-language proof evaluation must inspect local reasoning because proofs can omit conditions, skip derivations, or continue from early mistakes.
  • Lean validation is used as structured evidence only when the formal target remains local and semantically faithful to the original claim.This prevents formalization drift from turning a different or weakened statement into evidence for the original proof step.
  • FaithSieve decomposes coarse proof steps into EdgeUnits, extracts typed obligations, and combines lightweight checks, Lean validation, and semantic alignment scoring.Its workflow localizes suspicious transitions, verifies selected obligations, and synthesizes evidence into a first-error prediction.
  • 350 problems form PROOFLOC-OLYMPIAD, while 200 advanced mathematics problems form PROOFLOC-UNIVERSITY.Both datasets are expert-verified benchmarks for first-error localization.
  • 81.43% exact first-error accuracy on PROOFLOC-OLYMPIAD exceeds the 72.29% GPT-5.4 direct-judging baseline.

2 Task Formulation and Challenges

The task is to identify whether a natural-language proof is valid or locate its earliest unreliable step, while Lean-based evidence must overcome locality and semantic mismatches. FaithSieve therefore validates localized, semantically aligned obligations rather than whole proofs.

  • 2.1 Problem Formulation: First-error localization predicts either that a proof is correct or the index of its earliest mathematically unreliable step.Later errors may exist, but they are not the target label.
  • 2.1 Problem Formulation: Binary accuracy distinguishes valid from invalid proofs, whereas exact accuracy also requires the correct first-error step for invalid proofs.
  • 2.2 Lean-Based Verification: Promise and Challenges: Lean can provide checkable artifacts for local claims such as algebraic rewriting, entailment, goal reduction, witness verification, and case coverage.
  • 2.2 Lean-Based Verification: Promise and Challenges: Validating a coarse target can bypass a local flaw, such as proving a → c without checking the intermediate transitions a → b and b → c.
  • 2.2 Lean-Based Verification: Promise and Challenges: Autoformalization can omit assumptions, alter quantifiers, reverse implications, or change conclusions while still producing a provable statement.
  • 2.2 Lean-Based Verification: Promise and Challenges: FaithSieve responds by operating on local reasoning units and requiring semantic alignment before treating Lean output as strong evidence.

3 Localizing Verifiable Reasoning Units

FaithSieve converts coarse proof steps into a proof-state tree whose typed local transitions can be prioritized and translated into explicit verification obligations. This makes formal checking more targeted and preserves the context needed to assess each reasoning move.

  • 3.1 Recursive Decomposition into a Tree of Proof States: A single chain-of-thought step may combine substitution, definition expansion, new facts, goal switching, or branch pruning, so it is not always a logical verification unit.
  • 3.1 Recursive Decomposition into a Tree of Proof States: The system constructs a tree T = (V, E) of natural-language proof states and state transitions modeled on Lean proof states.
  • 3.1 Recursive Decomposition into a Tree of Proof States: Each proof-state node stores accumulated assumptions and a current subgoal, while each edge represents a typed local transition.Examples include fact derivation, rewriting, goal reduction, case splitting, and lemma introduction.
  • 3.1 Recursive Decomposition into a Tree of Proof States: Each edge is recorded as an EdgeUnit, the basic object for subsequent review and formal validation.
  • 3.1 Recursive Decomposition into a Tree of Proof States: Recursive construction updates assumptions, goals, and branch-specific conditions according to the transition type, preserving local context.
  • 3.2 Suspicion Search: Suspicion Search scores EdgeUnits using their contexts, goals, branch scopes, transition types, and common failure modes.
  • 3.2 Suspicion Search: The audit window focuses on the earliest suspicious edge plus a short preceding prefix, controlling the cost of obligation discovery and validation.
  • 3.3 Obligation Statement Generation: Typed obligation generation maps each EdgeUnit’s state change to explicit local verification targets, including separate checks for newly introduced facts and goal reductions.

4 Faithfulness-Aware Verification and Evidence Fusion

FaithSieve validates local proof obligations through formal checks only after confirming that generated statements remain semantically faithful to the original claims. It then fuses local checking outcomes, faithfulness reports, and diagnostics into step-level decisions.

  • 4.1 Statement Faithfulness Scoring: Statement faithfulness scoring checks whether the generated formal statement preserves the original local mathematical claim.The score combines premise fidelity, conclusion fidelity, and holistic semantic fidelity.
  • 4.1 Statement Faithfulness Scoring: The premise score evaluates retention of hypotheses, local context, branch assumptions, and fixed witnesses, while the conclusion score evaluates correspondence with the target claim.
  • 4.1 Statement Faithfulness Scoring: The holistic score checks step relation, objects and witnesses, directionality, role alignment, and syntax to detect broader semantic distortions.It covers patterns such as wrong direction, role reversal, meta-level wrappers, and vacuous formalizations.
  • 4.2 Formal Evaluation Agent: Generated statements are compiled, semantically scored against the original obligation, and revised when language-meaning or critical component scores fall below threshold.Lean MCP tools repair syntax, type, or dependency errors before semantic checking.
  • 4.2 Formal Evaluation Agent: Pure numeric obligations use a SymPy checker, while other obligations passing the faithfulness gate enter Lean validation.The SymPy branch returns passed, refuted, or inconclusive for supported numeric forms; the Lean branch verifies propositions or counterexamples according to suspicion.
  • 4.3 Evidence Fusion and Final Decision: Local checking results are fused with typed obligations, faithfulness reports, and diagnostics before mapping evidence back to the original proof steps.A step is marked incorrect when it has faithful and reliable negative evidence, such as a refuted obligation or verified counterexample.

5 Empirical Evaluation

The evaluation benchmarks FaithSieve on expert-verified olympiad and university datasets, comparing structured local evidence against direct judging and component ablations. Results show consistent gains from the full pipeline, while removing locality or semantic filtering reduces performance.

  • Datasets: 350 olympiad problems and 200 university problems form the expert-verified evaluation benchmarks.The university benchmark spans topology, linear algebra, abstract algebra, real analysis, convex analysis, and convex optimization.
  • Main results: 81.43% exact accuracy on PROOFLOC-OLYMPIAD and 84.50% on PROOFLOC-UNIVERSITY exceed GPT-5.4 direct judging at 72.29% and 75.00%, respectively.With GPT-5.4, binary accuracy is 93.71% versus 88.29% on Olympiad and 92.50% versus 87.00% on University.
  • Main results: Across both datasets and tested backbones, FAITHSIEVE consistently improves first-error localization over direct judging.The evaluation uses GPT-5.4 and Qwen3.5-9B to test the pipeline effect.
  • Ablations: The Step3 graph judge reaches 75.71% exact accuracy, while EdgeUnit + NL reaches 73.43% with GPT-5.4 and 71.14% with Qwen3.5-9B.These variants remove formal validation and evidence fusion, or retain local review while removing the Evaluation Agent.
  • Ablations: Removing local EdgeUnits reduces GPT-5.4 exact accuracy to 60.86% and Qwen3.5-9B exact accuracy to 62.29%.The ablation falls back from fine-grained local transitions to coarse-step-level judging.
  • Ablations: Relaxing the semantic gate reduces exact accuracy to 70.86% for both GPT-5.4 and Qwen3.5-9B.The semantic gate controls whether hybrid-validation results enter the final evidence set, limiting contamination from semantically drifted statements.

6 Conclusion

The paper concludes that formal validation is most useful for natural-language proof evaluation when applied to local reasoning transitions and filtered for semantic faithfulness. FaithSieve uses this evidence to improve first-error localization while producing traceable signals for auditing generated proofs.

  • 6 Conclusion: FaithSieve decomposes coarse proof steps into EdgeUnits, extracts typed obligations, and fuses checker and Lean evidence into first-error predictions.The workflow builds a proof-state tree, scans suspicious units, performs local review, and validates selected obligations.
  • 6 Conclusion: Local reasoning units, faithful statement checking, formal or arithmetic evidence, and evidence fusion all contribute to the reported improvements.The conclusion frames these components as contributors across the PROOFLOC-OLYMPIAD and PROOFLOC-UNIVERSITY evaluations.
  • 6 Conclusion: The framework provides traceable local evidence for auditing generated proofs, supporting step-level feedback, and exposing where a proof first becomes unreliable.Future work targets geometry, combinatorics, definition-heavy university mathematics, and more efficient autoformalization and validation.
  • 6 Conclusion: Lean proof success is useful only when the generated statement faithfully represents the intended proof-state change.Proof failure or timeout is treated as inconclusive rather than as definitive evidence.

B.2 Tree of Proof State

The method represents informal proofs as trees of accumulated proof states connected by fine-grained EdgeUnits. It then ranks suspicious transitions, derives typed local obligations, and evaluates them as local evidence rather than as a global proof verdict.

  • Tree representation: Each proof-state node records accumulated conditions and a current local goal, while each edge represents a reasoning transition.A state describes the context after a step, not the step itself.
  • State updates: Child states inherit parent conditions and add, transform, or consume conditions according to the proof pattern.Supported patterns include case splits, lemma introduction, induction, witness instantiation, quantifier elimination, and iff splitting.
  • EdgeUnits: Every coarse proof step maps to exactly one normalized EdgeUnit carrying provenance, transition metadata, state changes, and scheduling cues.EdgeUnits record fields such as unit identity, source-step provenance, goals, conditions, and structural transformations.
  • Suspicion-guided review: Suspicion Search ranks units for local review and formalization, using a prefix window of the suspicious unit plus up to six preceding fine-grained steps.The search prioritizes the earliest plausible error and is a scheduling mechanism, not a final proof verdict.
  • Typed obligations: Typed obligation discovery converts selected transitions into explicit verification targets, checking newly introduced facts before allowing them to serve as premises.Obligation types include derived facts, rewrites, goal reductions, witnesses, case splits, entailments, and contested claims.
  • Local evaluation: The Formal Evaluation Agent returns passed, refuted, or inconclusive local evidence, while the cheap arithmetic checker handles only variable-free numerical claims.The arithmetic front end is deliberately conservative and does not decide symbolic or context-dependent claims.

C.3 Statement / Proof Generation and Compile Repair

FaithSieve separates Lean statement generation from proof generation and repairs each stage using compiler or proof diagnostics. Only statements that compile and pass semantic faithfulness checks proceed to proof or refutation search, while failures remain conservative local evidence.

  • Statement generation: The agent first generates and compiles a Lean statement, then checks whether it faithfully represents the natural-language obligation and local context.Compilation alone is insufficient because a formal statement can drift semantically.
  • Compile repair: Syntax, type, import, namespace, dependency, and elaboration errors trigger statement-only repair using returned Lean diagnostics.The repair loop revises the formal artifact before proof generation begins.
  • Proof generation: After the faithfulness gate passes, the proof agent repeatedly proposes Lean proof scripts and repairs them from diagnostics and current goal states.The statement is held fixed during proof repair unless the system explicitly returns to statement generation.
  • Conservative outcomes: Successful proofs or refutations become passed or refuted local evidence, whereas proof failure, timeout, and unproved statements remain inconclusive.This separation prevents engineering failures from being treated as evidence that the natural-language obligation is false.

D.1 Dataset Summary and Source Provenance

The evaluation uses two expert-verified benchmarks covering olympiad and university-level mathematical proofs. Candidate proofs are generated as ordinary numbered solutions and annotated for correctness and the earliest material proof break.

  • Benchmark composition: PROOFLOC-OLYMPIAD contains 350 olympiad-style algebra and number-theory problems.It is one of the two expert-verified benchmarks used for evaluation.
  • Benchmark composition: PROOFLOC-UNIVERSITY contains 200 problems spanning topology, metric spaces, linear algebra, abstract algebra, real analysis, convex analysis, and convex optimization.Its textbook provenance is reported to make the six-domain coverage auditable.
  • Data generation: GPT-4o generates complete numbered step-by-step candidate proofs without being asked to introduce errors.The benchmark therefore targets naturally occurring model reasoning failures rather than adversarial perturbations.
  • Expert annotation: Expert annotators label correctness and identify the earliest step that introduces a material proof break.Disagreements or ambiguities are jointly reviewed rather than resolved by a unilateral label.

E.1 Human Audits of Local Reasoning Construction

Human audits examine whether decomposition preserves first errors, whether suspicion search covers them, and whether the semantic gate agrees with expert faithfulness judgments. Main results then compare complete FaithSieve runs with direct judging under exact and binary accuracy.

  • Decomposition preservation: 84% and 86% of audited decompositions preserved the source proof’s first error according to two independent experts.The audit covered 50 original proof-decomposition logs.
  • Suspicion Search: Search covered the earliest error in 23 of 25 known-wrong proofs, despite moderate unit-level recall.The calibration used 50 Olympiad proofs and 752 EdgeUnits.
  • Semantic gate: 88.98% precision and 91.30% recall were achieved by the semantic gate on 135 theorem and lemma statements.Accepted drift included added or strengthened assumptions, vacuous propositions, and weakened targets, so gate acceptance is not a fidelity guarantee.
  • Candidate reduction: 31.51% of 5,458 Olympiad EdgeUnits were selected as candidates for expensive downstream checks.The fixed prefix lookback was six units, giving each audit a maximum contiguous context of seven units.
  • Main results: 81.43 exact accuracy was achieved by FAITHSIEVE with GPT-5.4 versus 72.29 for direct GPT-5.4 judging.The complete pipeline includes decomposition, proof-state graphs, EdgeUnits, suspicion scheduling, typed obligations, validation, and evidence fusion.
  • Main results: 74.00 exact accuracy was achieved by FAITHSIEVE with Qwen3.5-9B versus 53.71 for direct Qwen3.5-9B judging.The direct judge receives only the problem statement and original numbered proof steps.

F.5 Ablation Study and Analysis

Ablations show that FaithSieve’s gains depend on fine-grained local decomposition, semantic gating, and locally checkable evidence, while remaining costly and domain-sensitive. The full system improves first-error localization over direct judging and simpler structured variants.

  • Local evidence: The EdgeUnit + NL-only variant reaches 73.43% exact and 88.00% binary accuracy with GPT-5.4, showing local representations help even without formal validation.Its performance remains below the full replay result.
  • Locality: Removing local EdgeUnits causes the largest degradation, reducing GPT-5.4 to 60.86% exact and 72.29% binary accuracy.The result supports using local transitions rather than coarse annotation steps as reasoning units.
  • Semantic alignment: Disabling the semantic gate lowers GPT-5.4 performance to 70.86% exact and 86.29% binary accuracy.Formal evidence is useful only when the generated statement remains aligned with the original obligation.
  • Error analysis: FaithSieve reduces false-positive rates from 21.57% to 9.15% on Olympiad and from 16.92% to 6.92% on University.On University-200, localization remains the largest residual error category.
  • Cost controls: Comparable token budgets allocated to repeated natural-language judgments or structured NL-only agents do not reproduce the gain from locally checkable Lean evidence.The controls show FaithSieve is not inexpensive, despite its performance advantage.
  • Domain analysis: Performance is relatively high in Linear Algebra and Abstract Algebra, where algebraic objects and theorem dependencies align with fine-grained formalization.The authors caution that domain intervals remain important because some domains contain only 20–40 examples.

G.1 Limitations

FaithSieve’s limitations concern the cost and coverage of formal validation, dependence on current autoformalization agents, and restricted domain coverage. The system is intended as an auditing aid rather than a replacement for human mathematical judgment.

  • Formal validation is costly and incomplete because statement generation, proof repair, proof search, artifact checking, and normalization may fail or time out.
  • The method depends on current LLM agents, and unfamiliar Lean representations or mathlib conventions can produce inconclusive evidence for otherwise checkable claims.
  • Domain coverage is limited: Olympiad evaluation focuses on algebra and number theory, while geometry and combinatorics require additional encodings and library coverage.The University benchmark broadens coverage to six domains but still requires further annotation and verification.
  • FaithSieve should be used as an auditing aid that organizes local evidence, not as an automatic replacement for human mathematical judgment.In education, local feedback should support inspecting and repairing reasoning rather than assigning authoritative labels.
  • A successful Lean proof is informative only when its generated statement faithfully represents the original obligation, while inconclusive evidence does not imply an incorrect proof step.The system therefore separates semantic faithfulness, validation status, and benchmark prediction.

H Case Studies: Natural-Language Context for Representative Lean Statements

The case studies show how FaithSieve preserves local proof context when extracting Lean obligations, validating both correct steps and explicit negations of erroneous claims. These examples connect natural-language reasoning to concrete formal targets and counterevidence.

  • FaithSieve’s examples retain the source claim, extracted local obligation, and Lean target, with all six proof scripts rechecked successfully.The first two targets negate incorrect source claims; the remaining four prove correct local obligations.
  • Caught errors: For the polynomial-witness error, Lean proves that the four concrete witnesses cannot satisfy the asserted identity.At X = 1, the claimed identity yields 8 on the left and 12 on the right; coefficient comparison also fails because a fourth-degree term appears.
  • Caught errors: For the quadratic-coefficient error, the inherited equations are retained while the validation branch proves that a = 4/3 does not follow.
  • Caught errors: A corrected arithmetic step derives a = 4/5 by adding twice the second simplified equation to the first, rather than using the erroneous value 4/3.
  • Proved local steps: The functional-equation target preserves the recurrence, initial value, and derived fact f(3) = 15 before proving f(9) = 33.
  • Proved local steps: The logarithm example retains positivity assumptions and the original three-equation system while checking the change-of-base rewrite.
  • Proved local steps: The real-exponentiation example checks a right-hand-side rewrite while retaining the original equation as an assumption.
  • Proved local steps: The integer-arithmetic example preserves the concrete computation B = 0 · 5 −(−1) −(−5) = 6 and discharges it by normalization.
Loading 2608.26310v1…