重塑数学验证的“裁判”：ProofJudge对LLM评估维度的深度解析
形式化证明中的隐形质量陷阱
在当前的数学自动化浪潮中，Lean 4 等形式化验证系统已成为学术前沿的标配。开发者利用这些系统编写严谨的证明，确保每一步推导都经得起类型检查的严格审查。然而，鲜为人知的是，通过了 kernel 的型检并不等同于证明的质量上乘。形式化证明的质量呈现出显著的多样性，这在很大程度上取决于开发者对库的使用习惯、自动化工具的适配程度以及定理陈述的清晰度等非正式因素。
这种质量的差异性在开源数学库 Mathlib 的日常贡献中尤为明显。每天都有大量的 Pull Request（PR）被提交，其中包含了各种各样的定理和证明。传统的审查流程依赖于人工的专业判断，这既耗时又受限于审查者的专业深度和精力。如何在海量的贡献中快速、客观地评估证明的质量，成为了推动形式化数学发展的瓶颈。如果说形式化验证是“筑路”，那么评估证明质量就是“检路”，而这条路目前仍然充满了未知和变数。
ProofJudge：超越正确性的多维评估体系
针对上述痛点，研究团队推出了 ProofJudge，一个被设计为“LLM-as-judge”（LLM作为裁判）的智能体系统。它的核心创新不再局限于简单的正确性判断，而是将评估维度扩展到了五个关键维度：库利用度、自动化契合度、结构清晰度、陈述质量以及 Mathlib 约定。这五个维度共同构成了一个立体的质量画像，旨在捕捉人类审稿员潜意识里的评估标准。
ProofJudge 之所以能够实现这一跨越，关键在于其“工具 grounded”（工具 grounded）的特性。与传统的黑盒评估模型不同，ProofJudge 拥有对提交的 PR 所对应的提交记录的直接访问权。这种设计使得评审代理在打分时，能够实时查询当前的库状态，理解上下文变迁，从而做出更具针对性的评价。这种机制打破了评估过程的信息孤岛，让 LLM 能够“看见”它评估对象的完整历史脉络。
在实际应用中，研究者构建了一个由 218 个不同 Mathlib PR 声明组成的新型数据集。这些声明涵盖了从基础算法到高级数学理论的各个层面。评估过程揭示了一个有趣的现象：所有六个被测评的 judge 模型都在很大程度上恢复了审稿人的偏好，准确率高于随机猜测，范围从 80.8% 降至 63.5%。这一结果表明，即使是最基础的 LLM 判断，也具备一定的参考价值，但要达到高精度的审查水平，仍需依赖更强大的模型支撑。
成本与性能的博弈：开源模型的崛起
在讨论评估效果的同时，成本因素始终是产业界关注的焦点。文章数据显示，两个开源体重量级选手在大约十分之一的成本下，达到了接近最佳闭源 judge 的评估效果。这一发现具有里程碑式的意义。它意味着，高质量的形式化证明评估不再是少数顶级实验室的专属特权，而是可以通过相对有限的计算资源实现的大众化服务。
这种成本结构的反转，实际上是在重塑 AI 评估市场的格局。过去，闭源的大模型因其强大的推理能力和广泛的训练数据而被视为唯一的选择；而现在，开源模型凭借其透明的架构和可控的成本，正在逐步填补这一空白。对于 Mathlib 这样的开源项目而言，这意味着可以以极低的预算引入先进的自动化审查机制，大幅提升贡献者的体验和项目的整体健康度。
对齐人类偏好的艺术与科学
文章特别强调了“与人类偏好对齐”的概念。一个 judge 被视为与人类偏好对齐，是指它倾向于接受 Mathlib 社区最终采纳的 PR 版本，而非最初被退回进行修订的初版。这一标准将评估从抽象的数学正确性，拉回到了社区实践的具体语境中。这揭示了一个核心真理：形式化数学的质量，本质上是一个社区共识的问题。
ProofJudge 的设计理念正是基于这一洞察。它试图模拟并量化社区审稿员的行为模式。通过大量的样本对比，研究者验证了该系统能够捕捉到人类审稿员在处理复杂证明时的细微偏好，比如对代码复用的偏好、对阅读流畅性的要求以及对库规范的遵守情况。这种对人类偏好的精准对齐，使得 ProofJudge 成为了连接机器效率与人类审美之间的桥梁。
前瞻展望：从评估到生成的跃升
展望未来，ProofJudge 的出现不仅是一个评估工具的诞生，更是形式化数学自动化流程优化的重要一步。随着系统的开源和迭代，我们有理由期待，未来的 Lean 4 开发者将能够在编写证明的即时获得高质量的、多维度的反馈。这种实时的质量诊断能力，将极大降低形式化验证的学习门槛，鼓励更多数学家尝试使用正式方法。
此外，这种工具 grounded 的评估范式，也有望延伸到其他 AI 创作领域。无论是代码生成的质量把控，还是复杂文档的结构优化，都可以借鉴这种将 LLM 与具体工具环境绑定的方式。可以预见，在未来的很长一段时间里，ProofJudge 及其后续的演变版本，将成为连接人类数学直觉与机器精确计算的关键基础设施，推动整个数学生态向着更加规范、高效的方向迈进。