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

• URL: http://arxiv.org/abs/2608.26310v1
• Date: Wed, 26 Aug 2026 18:43:30 GMT
• Title: FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence
• Abstract summary: FaithSieve is a Lean-assisted framework for fine-grained evaluation of natural-language mathematical proofs.<n>It decomposes proof steps into local reasoning units, extracts typed proof obligations, and verifies them.<n>On the 350-problem Olympiad dataset, FaithSieve using a GPT-5.4 backbone achieves 81.43% exact first-error accuracy.
• Score: 9.041607777624504
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
  We study faithful statement formalization as both an evaluation problem and a bottleneck-attribution problem.<n>A full tool-augmented agent reaches 89.5% compilation but only 60.5% consensus faithfulness, exposing a 29.0-point compile-pass but consensus-unfaithful gap.
  arXiv  Detail & Related papers  (2026-06-30T00:27:53Z)
• Evaluating the Robustness of Proof Autoformalization in Lean 4 [8.029528831501514]
  We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from idealized ones.<n>We build a benchmark with both perturbations on miniF2F and MATH-500.<n>We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations.
  arXiv  Detail & Related papers  (2026-06-12T18:10:21Z)
• Faithful Autoformalization via Roundtrip Verification and Repair [0.4403025166321017]
  We propose a roundtrip verification approach which does not require ground-truth annotations.<n>When the two formalizations agree, this provides evidence of a faithful formalization.<n>We evaluate our approach on 150 traffic rules using Claude Opus 4.6 and GPT-5.2.
  arXiv  Detail & Related papers  (2026-04-27T22:26:01Z)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T is a framework that evaluates the semantic correctness of formal theorems.<n>We construct a benchmark from 5 real-world Lean 4 repositories.<n>Experiments demonstrate that while state-of-the-art models achieve high compilation success, they perform significantly worse under our semantic metric.
  arXiv  Detail & Related papers  (2026-04-26T13:24:20Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  Modern language models (LMs) exhibit strong deductive reasoning capabilities, yet standard evaluations emphasize correctness while overlooking a key aspect of human-like reasoning: efficiency.<n>We propose a framework for assessing LM reasoning efficiency through the lens of logic programming.
  arXiv  Detail & Related papers  (2025-10-29T15:30:31Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  We introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. We fine-tune the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs. Our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any.
  arXiv  Detail & Related papers  (2024-05-23T09:03:42Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.