研究人员开发了ProofJudge，一个基于LLM的系统，用于评估在Mathlib库中用Lean 4编程语言编写的形式化证明的质量。该代理系统在五个标准上评估证明，这些标准超出了单纯的正确性，包括库利用、自动化匹配、结构清晰度、陈述质量和对Mathlib约定的遵守程度。ProofJudge在218个Mathlib pull request的数据集上进行了评估，证明其与人类审阅者偏好的匹配程度显著高于随机水平，其中一些开源模型以较低的成本实现了高准确率。该项目旨在通过发布judge harness、评估数据集和traces作为开源产物，来促进进一步的研究。 AI
影响 该工具可以提高形式化数学证明代码审查的效率和一致性，有可能加速定理证明社区的发展。
排序理由 该集群描述了一篇详细介绍基于LLM的形式化证明评估系统的新研究论文。
在 Hugging Face Daily Papers 阅读 →
AI 生成摘要 · Google Gemini · 来自 2 个来源。 我们如何撰写摘要 →
arXiv:2608.20432v1 Announce Type: cross Abstract: 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:…
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 clar…