FaithSieve：基于忠实形式证据的数学证明细粒度评估
FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence
- Peking University（北京大学）
- School of Mathematical Sciences（数学科学学院）
- Huawei Technologies Co., Ltd.（华为技术有限公司）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本研究提出Lean辅助框架FaithSieve，通过分解数学证明为细粒度单元并结合忠实形式证据，在两个专家验证数据集上提升了首个错误定位的精确评估准确率。
AI中文摘要：
大型语言模型如今能够生成复杂的多步骤数学证明，但可靠判定其正确性并定位早期逻辑错误仍是关键挑战。现有评估方法大多依赖基于模型的自然语言判断，常忽略局部推理缺口。尽管Lean等形式化定理证明器提供了严格验证的途径，但用其评估非形式化文本需解决局部性和语义不匹配问题：证明器可能通过证明过宽的目标绕过局部缺陷，或验证与原始数学意图偏离的自动形式化陈述。为解决此问题，我们提出FaithSieve，一种Lean辅助的自然语言数学证明细粒度评估框架。FaithSieve将粗粒度证明步骤分解为局部推理单元，提取带类型的证明义务，并通过形式化评估智能体验证。形式化验证由语义对齐评分控制，仅当形式化陈述忠实保留原始主张的上下文、对象和逻辑形式时，才纳入Lean证据。我们构建了两个经专家验证的数据集ProofLoc-Olympiad和ProofLoc-University，用于基准测试首个错误定位能力。在含350个问题的奥林匹克数据集上，采用GPT-5.4主干的FaithSieve达到81.43%的首个错误精确准确率，优于72.29%的直接判断基线。此外，在涵盖六个高级领域、含200个问题的ProofLoc-University基准上，FaithSieve达到84.5%的精确准确率，而直接判断为75.0%。本研究表明，将证明分解为细粒度单元并以忠实形式证据为基础，可显著提升自然语言推理的可靠评估效果。
英文摘要：
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.
