通过严格的步骤级验证评估研究型数学证明

大型语言模型在严格验证复杂数学证明方面表现不佳，全局评估易受“上下文污染”影响。本文提出从全局评估转向严格的步骤级验证框架，为每个推导步骤维护详细上下文并约束定理来源。在研究型证明对抗数据集上的评估表明，该演绎约束至关重要，能有效定位细微逻辑错误。该方法不仅优于全局评估，还改变了错误分类，将主要失败归因于对未陈述领域惯例的“过度严谨”，揭示了基准测试中的隐含歧义，为未来自动证明审查系统奠定理论基础。