ProofJudge：基于工具的形式化证明质量 LLM 评估方法

ProofJudge 是一个基于 LLM 的智能体裁判系统，用于评估 Lean 4 形式化证明的质量，从库利用、自动化适配、结构清晰度、陈述质量和 Mathlib 约定五个维度打分。在包含 218 个声明的数据集上，六种裁判模型均高于随机水平地复现人类评审偏好（准确率 63.5%–80.8%），两个开放权重模型在约十分之一成本下达到约 70% 的准确率。系统通过工具访问提交对应的库状态进行评分。

此前形式化证明的质量评估主要依赖人工审查或二元正确性判断，缺乏自动化、细粒度的质量度量。ProofJudge 首次将 LLM 作为裁判，结合工具访问库状态，在多维度上量化证明质量，并证明其与人类偏好高度一致，为形式化数学的项目维护和代码审查提供了可扩展的自动化方案。

ProofJudge 采用智能体式 LLM 裁判，通过工具访问证明所处提交的具体库版本，从而在评分时检索相关定义和定理。评分依据五个质量维度，并通过对比被接受版本和退回修订版本的评分来校准裁判与人类偏好的对齐程度。低成本开源模型仍能有效评分，表明质量评估能力可能具有规模效率。

对形式化数学项目（如 Mathlib）的维护，可大幅降低人工审查成本，加速 PR 合并流程。对依赖 Lean 4 的工具链，可集成 ProofJudge 作为自动质量门禁。对 LLM 应用，开源评估工具和数据集可复用于训练或微调模型，以生成更符合社区标准的证明。

• 将 ProofJudge 集成到 Mathlib 的 CI 流程，自动给 PR 质量打分并给出修改建议，减少维护者负担。
• 基于其评估数据集微调代码生成模型，优化生成证明的结构与库使用习惯。
• 开发面向 Lean 4 用户的 IDE 插件，实时反馈证明质量评分与改进提示。
• 将 ProofJudge 方法推广至其他形式化证明库（如 Coq 或 Isabelle），输出跨平台质量评估工具。

• ProofJudge 在非 Mathlib 库或不同 Lean 版本上的泛化性能尚未验证。
• 五维评分的权重和具体标准公开程度不明。
• 开放权重模型达到约 70% 准确率的具体条件（如模型大小）未说明。
• LLM 裁判在未见过的复杂证明上的稳定性未提及。