用AI评估数学证明质量，比传统检查更懂代码规范和可读性。
ProofJudge: Tool-Grounded LLM Evaluation of Formal Proof Quality in Mathlib
- 让大模型通过工具访问代码库，从五个维度评分证明质量。
- 在218个真实提交中，评分准确率超随机水平63.5%~80.8%。
- 开源评估工具和数据集，适合形式化验证与AI辅助编程研究者。
Lean 4 中通过内核类型检查的形式化证明质量仍差异显著。我们提出 ProofJudge，一种基于工具的代理型大模型评审系统，从五个维度（库复用、自动化契合度、结构清晰性、命题质量、Mathlib 规范）评估证明质量，超越单纯正确性。我们在一个包含 218 个声明的新数据集上评估该系统，这些声明来自不同的 Mathlib PR。评审代理通过访问对应提交的库状态进行评分。当其对被接受版本的评分高于初始修订版本时，视为与人工偏好对齐。六种评审模型均显著优于随机水平，准确率在 63.5% 至 80.8% 之间；其中两个开源权重模型仅需最佳模型成本的十分之一，即达约 70% 准确率。我们已开源评审框架、评估数据集及评估轨迹，以支持后续研究。
原文摘要 · Abstract (English)
Formal proofs in Lean 4 that pass the kernel's type checker can nonetheless vary widely in quality. We introduce ProofJudge, an agentic LLM-as-judge system that scores formal proof quality along five dimensions beyond correctness: library leverage, automation fit, structural clarity, statement quality, and Mathlib conventions. We evaluate ProofJudge on a novel dataset of 218 declarations drawn from distinct Mathlib PRs. The judge agent is grounded by tool access to the commit the PR is applied to, enabling it to query the library state when scoring. A judge is considered aligned with human preferences when it rates the version of the PR Mathlib accepted above the initial version that was sent back for revision. All six judge models evaluated recover the reviewers' preference well above chance, from 80.8% to 63.5%, and two open-weight judges reach roughly 70% at a tenth of the best judge's cost. We release the judge harness, evaluation dataset, and evaluation traces as open-source artifacts to support further research.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。