Source-linked AI summary
ProofJudge: Tool-Grounded LLM Evaluation of Formal Proof Quality in Mathlib
Shane Caldwell
TL;DR
Formal proofs that pass Lean’s kernel can still differ in quality for human mathematicians and Mathlib library development. ProofJudge uses a tool-grounded LLM judge with a five-dimension rubric to compare revised and pre-revision proofs, and all six evaluated judges align with reviewers above chance, though repeated judgments are noisy.
Problem
Kernel correctness does not capture whether formal proofs are understandable, reusable, and consistent with Mathlib’s quality standards.
Method
ProofJudge scores five proof-quality dimensions using a Mathlib-informed rubric and tool access to the relevant library state, evaluated on 218 declaration pairs.
Results
All six judges align with reviewers above the 50% chance baseline, ranging from 80.8% to 63.5%, while two open-weight judges reach 70.2% and 69.3%.
Takeaways & Limitations
ProofJudge suggests that Mathlib’s qualitative proof-review preferences are legible to language-model agents and could help reduce maintainer burden.
Takeaways & Limitations
Repeated runs can flip between one-fifth and nearly half of verdicts, so single-run benchmark differences may not be supported by replication.
Abstract
from arXiv · showhide
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.
1 Motivation and Background
Lean proofs can be kernel-correct yet vary in usefulness to mathematicians. Mathlib review therefore evaluates structural and stylistic qualities beyond correctness, especially reusable library contributions.
- Kernel-checked proofs are correct, but current LLM-generated proofs often violate Mathlib’s deeper structural and stylistic standards.Reviewers assess tactic hygiene, lemma generality, proof structure, naming, and independently reusable components.
- Mathlib reviewers value proofs that improve understanding and extend the library’s reusable API.The paper frames library-building and infrastructure for future work as central benefits of formalization.
2 Method
ProofJudge evaluates formal proof quality beyond compilation using a Mathlib-informed rubric and access to the relevant library state. Its evaluation dataset consists of declaration pairs from Mathlib pull requests.
- ProofJudge evaluates formal proof quality beyond compilation using an Agentic Judge system grounded by Lean’s correctness anchor.The system assesses softer qualities that kernel checking does not capture.
- Tool access lets the judge query Mathlib through bash and ground assessments in the actual library state.This mirrors a human reviewer’s ability to inspect existing declarations and library context.
- ProofJudge targets qualitative standards for library inclusion rather than the semantic correctness of pull requests.This distinguishes its evaluation goal from recent LLM judging work focused on PR correctness.
- The rubric independently scores library leverage, automation fit, structural clarity, statement quality, and Mathlib conventions on 1–10 scales.The harness weights the five dimension scores into a final score.
- Dataset Construction: The test split contains 218 declaration pairs from Mathlib pull requests, alongside a 123-pair development split used to tune the rubric.The dataset excludes cases whose revision differences were only linting or involved a new declaration.
3 Results
ProofJudge’s preference judgments align with Mathlib reviewers well above a 50% chance baseline across six judges. Open-weight models also achieve substantial alignment, while repeated runs reveal important noise.
- Each proof pair was scored independently, and alignment meant the accepted post-revision proof received a higher score than the rejected pre-revision proof.Judges could use up to twenty tool calls before determining a verdict.
- 80.8% to 63.5% of declarations were aligned with reviewers’ preferences across all six judges, versus a 50% random-chance baseline.Each judge achieved p < 10^-5 by sign test on the 218-pair test split.
- Repeated runs flipped between one-fifth and nearly half of verdicts, making single-run benchmark differences unreliable.The same ablation produced p = 0.34 in one replicate and p = 0.006 in another.
- PR 11640 illustrates tool-grounded library-leverage judging: the agent found an existing declaration and penalized a redundant initial proof.The merged revision replaced the reconstruction with one line, H. restrictPreimage s.
4 Conclusion
Formal proof quality includes understandability and contribution to future library work, not only kernel correctness. ProofJudge’s alignment results support exploring model-based signals to reduce maintainer burden, while cheaper and less noisy judges remain future goals.
- Proof quality matters to mathematicians because proofs should be understandable and contributions should enable future work.The conclusion distinguishes these properties from correctness alone.
- ProofJudge’s alignment scores suggest that these qualities are legible to modern language-model agents.The paper proposes using this signal where possible to relieve maintainer burden.
- Future Work: Future work seeks judges matching claude-sonnet-5 while being cheaper and open-source.The stated goal is to help reduce undue burden on Mathlib maintainers.
- Future Work: Reducing judge noise may provide a better signal for iterating pull requests before human review.Proposed directions include single-dimension judges and tuning the tool-call budget.