Summary (Overview)

• FaithSieve is a Lean-assisted framework for fine-grained evaluation and first-error localization in natural-language mathematical proofs, addressing the critical challenge of reliably determining correctness of LLM-generated multi-step proofs.
• The framework decomposes coarse proof steps into local reasoning units (EdgeUnits), extracts typed proof obligations, and validates them through a formal evaluation agent gated by semantic alignment scoring—ensuring Lean evidence is incorporated only when the formal statement faithfully preserves the context, objects, and logical form of the original claim.
• Two expert-verified datasets are constructed: ProofLoc-Olympiad (350 algebra/number theory problems) and ProofLoc-University (200 problems across six advanced domains).
• FaithSieve achieves 81.43% exact first-error accuracy on the Olympiad dataset (vs. 72.29% for direct-judging baseline) and 84.5% exact accuracy on the University dataset (vs. 75.0% for direct judge) using a GPT-5.4 backbone.
• Ablation studies demonstrate that local reasoning units, faithful statement checking, formal evidence, and evidence fusion all contribute to the performance gains.

Introduction and Theoretical Foundation

Background and Motivation

Large language models can now generate complex, multi-step mathematical proofs, but evaluating them and locating the first logical error remains difficult. Such proofs may:

• Omit conditions
• Skip derivations
• Use implicit assumptions
• Continue from early mistakes to plausible-looking conclusions

Reliable evaluation must check not only final answers but also local reasoning steps.

Two Central Challenges for Lean-Based Verification

The paper identifies two critical mismatches when using formal theorem provers like Lean to evaluate informal text:

1. Locality mismatch: A proof consists of local reasoning transitions rather than a single theorem. If a proof claims to derive $b$ from $a$, and then $c$ from $b$, proving only $a \Rightarrow c$ does not establish that the two local steps $a \to b$ and $b \to c$ are correct. A strong prover may directly prove a stronger or coarser target and ignore a local error.

2. Semantic mismatch: Even after localization, the system must translate the informal claim into a formal proposition. Autoformalization may omit assumptions, add conditions, reverse implications, alter quantifiers, weaken or strengthen the conclusion, or replace the claim with a different but provable statement.

These two mismatches lead to two requirements:

• Formal validation should operate on local reasoning units
• The Lean statement being validated must be semantically aligned with the original natural-language obligation

The paper's central thesis: Lean evidence is most useful when it is local and faithful.

Methodology

1. Proof-State-Tree Decomposition

FaithSieve treats COT steps as annotation units but not directly as logical verification units. The framework:

1. Pre-decomposes original COT steps into finer-grained substeps, removing redundant statements while preserving proof logic faithfully
2. Constructs a tree of proof states $\hat{T} = (\hat{V}, \hat{E})$ where each node $v \in V$ represents a natural-language proof state $S_v = (\Gamma_v, G_v)$:
   • $\Gamma_v$: currently available accumulated assumptions
   • $G_v$: current subgoal to be proved
3. Each edge $e = (v \to v') \in E$ represents a local reasoning transition of type $\tau_e$, recorded as an EdgeUnit $u_e$

2. Suspicion Tree Search

Since Lean validation is expensive, FaithSieve runs Suspicion Search over all edges to estimate which local transitions are more likely to contain the first material error. The model produces:

• Whether the transition is suspicious
• How suspicious it is
• An overall suspicion risk score in [0, 1]

Edges with suspicion risk above 0.6 are treated as relatively suspicious candidates. An audit window is built by selecting the earliest suspicious edge plus a short prefix of preceding edges.

3. Typed Obligation Generation

Each EdgeUnit's mathematical responsibility is summarized as an explicit obligation statement using conversion templates matched to edge types:

4. Statement Faithfulness Scoring

The statement faithfulness score measures semantic alignment between the formal statement $\hat{m}$ and the natural-language obligation $m$ under local context $C$:

$$S_{\mathrm{faith}}(m, \hat{m}; C) = \sqrt{S_{\mathrm{prem}}(m, \hat{m}; C) \cdot S_{\mathrm{conc}}(m, \hat{m}; C)} \cdot S_{\mathrm{hol}}(m, \hat{m}; C) \tag{1}$$

where:

• $S_{\mathrm{prem}}$: premise fidelity (whether hypotheses of $\hat{m}$ faithfully retain local context, branch assumptions, fixed witnesses)
• $S_{\mathrm{conc}}$: conclusion fidelity (whether conclusion of $\hat{m}$ matches the target claim)
• $S_{\mathrm{hol}}$: holistic score capturing step-relation fidelity, object/witness fidelity, directionality fidelity, role-alignment fidelity, and syntax fidelity

The component scores are computed as:

$$S_{\text{prem}} = \frac{\sum_{t \in T_{\text{prem}}} \operatorname{match}(t, \hat{m})}{|T_{\text{prem}}|} \quad S_{\text{conc}} = \frac{\sum_{t \in T_{\text{conc}}} \operatorname{match}(t, \hat{m})}{|T_{\text{conc}}|} \tag{2}$$

5. Formal Evaluation Agent

The agent runs on each obligation and returns:

• Local checking status: passed, refuted, or inconclusive
• Evidence strength adjusted by faithfulness and checker confidence
• A checkable artifact or diagnostic message

Three validation paths:

1. Equation SymPy Checker: For pure numeric claims with no variables or natural-language explanation
2. Lean Prover Checker: For obligations passing the faithfulness gate—verifies the original proposition (for likely-correct obligations) or a negated proposition/counterexample (for likely-wrong obligations)
3. Inconclusive: For timeouts or failures to pass the faithfulness gate

6. Evidence Fusion and Final Decision

Local results are aggregated back to original COT steps. A step is marked:

• Incorrect: when it has faithful and reliable negative evidence (refuted obligation, verified counterexample, or agreement between formal diagnostics and local review)
• Uncertain: when evidence mainly reflects semantic drift, formalization failure, timeout, or conflicting diagnostics

The system returns the earliest step with reliable negative evidence as the first error.

Empirical Validation / Results

Datasets

• ProofLoc-Olympiad: 350 algebra and number theory problems
• ProofLoc-University: 200 problems across topology, linear algebra, abstract algebra, real analysis, convex analysis, and convex optimization

Candidate proofs generated by GPT-4o, annotated by experts for correctness and first-error step.

Direct-Judge Baseline Results (Table 4)

FaithSieve Main Results

• ProofLoc-Olympiad (GPT-5.4): 81.43% exact / 93.71% binary accuracy (vs. 72.29% / 88.29% direct judging)
• ProofLoc-University (GPT-5.4): 84.50% exact / 92.50% binary accuracy (vs. 75.00% / 87.00% direct judging)

Domain-Level Results on ProofLoc-University (Table 3)

Ablation Results on ProofLoc-Olympiad (Table 5)

Key Ablation Findings

• w/o local EdgeUnits (falling back to coarse-step-level judging) drops GPT-5.4 to 60.86% exact—directly supporting the locality hypothesis: a benchmark step is an annotation unit, but not necessarily the actual reasoning unit
• w/o semantic gate (relaxing faithfulness thresholds) drops GPT-5.4 to 70.86% exact—showing that Lean success signals are reliable only when the statement remains semantically aligned with the original obligation

Theoretical and Practical Implications

Theoretical Contributions

1. Identification of locality and semantic faithfulness as the central challenges in applying formal validation to natural-language proof evaluation—a conceptual framework that clarifies why naive "Lean-as-judge" approaches fail
2. Proof-state-tree representation that bridges the gap between coarse annotation units and fine-grained logical verification units
3. Typed obligation system providing a structured way to specify what each local transition must establish
4. Statement faithfulness scoring offering a formalized approach to measuring semantic alignment between natural-language claims and their formal counterparts

Practical Implications

• Traceable local evidence: FaithSieve provides checkable artifacts for auditing generated proofs, supporting step-level feedback rather than just final-answer correctness
• Error localization: The framework pinpoints where a proof first becomes unreliable, enabling targeted correction rather than wholesale rewriting
• Smaller model improvement: The EdgeUnit + NL-only variant shows particular benefit for smaller backbones (Qwen3.5-9B: 71.14% exact vs. 53.71% direct), suggesting decomposition helps compensate for weaker reasoning
• Domain applicability: Strong gains in linear algebra (100% exact), abstract algebra (97.5%), and real analysis (80% vs. 68%) suggest the approach transfers well to structured mathematical domains

Conclusion

FaithSieve demonstrates that formal validation can serve as structured evidence for evaluating natural-language mathematical proofs when properly conditioned on two requirements: locality (decomposing proofs into fine-grained reasoning units) and faithfulness (ensuring formal statements preserve the original mathematical intent).

The framework operationalizes this view through:

1. Decomposition of coarse steps into EdgeUnits via proof-state trees
2. Extraction of typed obligations specifying local reasoning responsibilities
3. Validation through cheap checking (SymPy) and Lean-assisted agents
4. Filtering of formal evidence through semantic alignment scoring
5. Fusion of local results into benchmark-aligned first-error predictions

Across both datasets and multiple backbones, this local-evidence design consistently improves both correctness judgment and first-error localization over direct judging. Future work should extend the approach to geometry, combinatorics, and definition-heavy university mathematics while improving autoformalization and validation efficiency.