FaithSieve：基于忠实形式化证据的数学证明细粒度评估

大语言模型如今能生成复杂的多步数学证明，但可靠地判定其正确性并定位早期逻辑错误仍是关键挑战。现有评估方法大多依赖基于模型的自然语言判断，往往忽略局部推理缺口。虽然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%。我们的工作表明，将证明分解为细粒度单元并以忠实的形式化证据加以锚定，显著提升了自然语言推理的可靠评估。