大型语言模型已经能够生成复杂的多步数学证明，但如何可靠地判断其正确性并定位早期的逻辑错误仍是关键难题。现有评估方法大多依赖模型的自然语言判断，容易忽视局部推理缺口。形式化定理证明器（如 Lean）提供了严格验证的途径，但直接用于非形式化文本时会遇到局部性和语义不匹配的问题：证明器可能通过证明一个过宽的目标绕过局部缺陷，或验证一个在自动形式化过程中偏离原始数学意图的陈述。
为了解决这些问题，本文提出了 FaithSieve——一个借助 Lean 的细粒度评估框架。FaithSieve 首先将粗粒度的证明步骤拆解为局部推理单元，随后提取带类型的证明义务，并交由形式化评估代理进行验证。验证过程受到语义对齐得分的门控，只有当形式化陈述在上下文、对象和逻辑形式上忠实于原始声明时，才会纳入 Lean 证据。
我们构建了两个经专家验证的数据集：ProofLoc-Olympiad（350 题）和 ProofLoc-University（200 题，覆盖六个高级领域），用于基准测试首错误定位。实验表明，在 Olympiad 数据集上，使用 GPT-5.4 作为骨干的 FaithSieve 达到 81.43% 的精确首错误定位准确率，显著高于直接判断基线的 72.29%。在 University 基准上，FaithSieve 的精确准确率为 84.5%，而直接判断仅为 75.0%。
这些结果表明，将证明拆解为细粒度单元并结合忠实的形式化证据，可显著提升对自然语言数学推理的可靠评估。
博主点评：FaithSieve 的思路新颖，通过语义对齐过滤形式化证据，有效弥补了纯语言评估的盲点，为 LLM 生成的数学证明提供了更可信的验证手段。