Research map / Large language models / Agents, code and math

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

NeurIPS 2026 · Large language models › Agents, code and math · approach: Inductive and abstract reasoning evaluation · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Proposes FaithSieve, a Lean-assisted first-error localization framework for natural-language math proofs that decomposes proofs into EdgeUnits, extracts typed obligations, and gates Lean evidence by a semantic faithfulness score, evaluated on two new expert-verified datasets.

Problem

Reliably judging natural-language math proofs and localizing the first erroneous step, where direct LLM judging misses local gaps and Lean validation suffers from locality and semantic (autoformalization drift) mismatches.

Approach

Decompose coarse proof steps into a tree of proof states with local EdgeUnits, convert transitions into typed proof obligations, and only accept Lean/SymPy evidence when a semantic alignment score shows the formal statement faithfully preserves the original local claim; fuse local evidence back to step-level first-error prediction.

Key results

• FaithSieve with GPT-5.4 reaches 81.43% exact first-error accuracy on ProofLoc-Olympiad vs 72.29% for direct judging.
• On ProofLoc-University (200 problems), FaithSieve reaches 84.50% exact accuracy vs 75.00% for GPT-5.4 direct judging.
• With Qwen3.5-9B, FaithSieve reaches 74.00% exact on ProofLoc-Olympiad vs 53.71% direct judging.

Surprising findings

• Removing local EdgeUnits drops GPT-5.4 exact accuracy to 60.86%, below direct judging, indicating benchmark steps are not the actual reasoning units.

Limitations

• Gains on Convex Optimization are essentially tied with direct judging.
• Relies on autoformalization quality; semantic gate can leave many steps uncertain.
• Evaluated on algebra, number theory and selected university domains only; geometry and combinatorics not covered.

Experimental setup

Datasets: ProofLoc-Olympiad ProofLoc-University

Benchmarks: ProofLoc-Olympiad ProofLoc-University

Metrics: exact first-error accuracy binary accuracy

Baselines: Direct judge Step3 graph judge EdgeUnit + NL only w/o local EdgeUnits w/o semantic gate

Builds on: Lean mathlib BIG-Bench Mistake ProcessBench Lean Tools MCP

Closest papers by meaning

• Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.92)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · similarity 0.90)
• ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.89)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.89)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.89)
• RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics (NeurIPS 2025 · similarity 0.89)