如何评估定理证明模型的性能？

评估定理证明模型的性能是个很有意思的话题，说实话，光看准确率可能远远不够。就像最近DeepSeek开源的Prover-V2模型在MiniF2F测试集上达到88.9%通过率这么惊人的数字，但如果我们仔细拆解这个结果，会发现背后还有更多值得思考的问题。比如，模型是真正掌握了数学证明的逻辑，还是只是记住了某些特定的解题模式？这个问题困扰着很多研究者。

基准测试集的局限性

当前主流的评估方法依赖于标准化的数学测试集，比如MiniF2F、PutnamBench等。但这就像用期末考试分数来评判一个学生——它能反映部分能力，却无法衡量真正的数学素养。有趣的是，DeepSeek-Prover-V2-7B在PutnamBench上反而解决了一些671B模型搞不定的题目，这说明参数量大并不总是万能的。

我注意到一个细节：测试集中题目分布的偏颇会导致评估结果的偏差。比如有些数据集过于侧重数论题，这会让擅长该领域的模型看起来性能特别好。DeepSeek发布的ProverBench包含了325道题目，覆盖竞赛和本科数学两个层面，这种多元化设计值得借鉴。

证明质量的深层评估

仅仅统计”通过/不通过”有点太简单了，不是吗？一个好的证明模型生成的形式化证明还应该具备可读性、创新性和可泛化性。看DeepSeek的技术报告很有意思，他们区分了CoT和non-CoT两种模式——前者产生具有完整思维链条的证明，后者直接生成精简代码。实验表明CoT模式效果更好，这提示我们评估时应该关注模型的推理过程。

我特别赞同DeepSeek团队的做法——他们不仅评估最终结果，还会检查证明的结构是否合理，子目标分解是否清晰。这就像老师批改数学题时不光看答案对错，还会看解题步骤是否合理。据说他们的7B模型意外发展出处理有限基数问题的特殊技巧，这种”进化”出来的能力在传统评估中很容易被忽视。

更全面的评价体系

要全面评估定理证明模型，可能需要考虑几个关键维度：首先是泛化能力，能否处理未见过的题型；其次是创新性，能否提供人类专家都没想到的新颖证明方法；还有鲁棒性，对数学表达的稍许变化是否依然能给出正确证明。DeepSeek报告提到他们收集了几百条高质量训练数据，这种数据多样性对确保评估可靠性至关重要。

说到底，评估定理证明模型就像评价一个数学家——简单看发了多少篇论文远远不够。我们需要更立体、更动态的评价方式，既要看它能不能解决问题，也要看它怎么解决的，以及在多大程度上能举一反三。或许，这正是DeepSeek等团队正在探索的方向。