用形式化证明精准检测数学证明中的早期逻辑错误。
FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence
- 将复杂证明拆解为细粒度推理单元，结合语义匹配验证。
- 在奥数数据集上首错定位准确率达81.43%，优于直接判断基线。
- 适合需要高精度评估数学推理能力的研究者和教育工具开发者。
大型语言模型可生成复杂的多步数学证明，但可靠判断其正确性并定位早期逻辑错误仍是关键挑战。现有评估方法多依赖模型生成的自然语言判断，常忽略局部推理漏洞。尽管形式化定理证明器（如 Lean）能提供严格验证，但用于评估非正式文本时面临局部性与语义不匹配问题：证明器可能绕过局部缺陷通过证明更广泛目标，或认可与原意偏离的自动形式化陈述。为此，我们提出 FaithSieve——一种基于 Lean 的细粒度数学证明评估框架。该框架将粗粒度证明步骤分解为局部推理单元，提取带类型的证明目标，并通过形式化评估代理验证。形式化验证仅在语义对齐得分达标时启用，确保形式化陈述忠实保留原始命题的上下文、对象与逻辑结构。我们构建了两个专家验证的数据集：ProofLoc-Olympiad 和 ProofLoc-University，用于基准测试首错定位。在包含350个问题的奥数数据集上，使用 GPT-5.4 骨干的 FaithSieve 达到81.43%的首错精确率，优于直接判断基线的72.29%。在涵盖六个高级领域的200个问题的 ProofLoc-University 基准上，准确率达84.5%，高于直接判断的75.0%。结果表明，将证明细粒度分解并以忠实形式证据为根基，显著提升了自然语言推理评估的可靠性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。