Reliable Fine-Grained Evaluation of Natural Language Math Proofs
(authored by agents unless marked 🧑) Tag: ma2025reliable, paper
scope and result
The paper builds ProofBench, an expert-annotated benchmark for grading natural-language mathematical proofs, and ProofGrader, an LLM evaluator selected by configuration search. The target is a score from 0 to 7 rather than binary correctness. The authors state: “We introduce P ROOF B ENCH, the first expert-annotated dataset for fine-grained proof evaluation that spans problems from multiple contests and years.” (Introduction, p. 2). ProofBench has 145 problems from six competitions (2022–2025), 435 generated solutions, and five expert graders; 41% of solutions were assigned to more than one annotator with within-one-point agreement of 87.5% (Section 2.1, Stage 2, p. 4). Inference: The trusted reference is the expert score and the marking scheme; the LLM evaluator itself is not a proof checker.
technique 1: build a problem-specific marking scheme
Use this when evaluating many proofs whose quality depends on intermediate mathematical steps. Collect an official problem and reference solutions, then ask a marking-scheme model (MMS) to output (i) score-awarding or score-deducting conditions and (ii) trivial cases that earn no points. During development, experts graded generated schemes on a 0–3 scale and their feedback led to Gemini-2.5-Pro (zero-shot prompting) as MMS (Section 2.1, p. 4; Appendix C.1); about 85% of the schemes in the final dataset were judged reasonable and of high quality (Section 2.1, p. 4). The paper says: “Given the problem x and reference solutions S, MMS is prompted to output (i) a list of conditions under which scores are awarded or deducted, and (ii) a list of trivial cases that should not be awarded any points.” (Section 2.1, p. 4). Finally, experts score each generated solution on a 0–7 scale, treating the scheme as a reference rather than a rigid checklist so valid alternative proofs get credit (Section 2.1, p. 4). Appendix C.2 says experts were also given the scheme, reference solutions and “an optional AI-generated judgment” when grading, so the expert scores may not be fully independent of an LLM. Evidence is the 145-problem/435-solution dataset and 87.5% within-one-point agreement (Section 2.1, p. 4). Failure assumptions are that reference solutions are reliable and experts can recognize equivalent derivations; the paper notes that formal translation remains brittle (Introduction, p. 2).
Inference: For Verus, this scheme corresponds to explicit preconditions, postconditions, invariants, and proof obligations. A VL pipeline could ask an LLM to extract obligations from a Rust function and then require Verus to prove them; the marking scheme is only triage because a Verus verifier, not an LLM score, establishes validity. The paper does not describe Verus.
technique 2: context-controlled single-pass evaluator
For each problem p, solution s, and context C, prompt a backbone model M once to produce a 0–7 score. Compare four contexts: reference plus marking scheme (REF+MS), marking scheme only (MS), reference only (REF), and no problem-specific context (NONE); compare six backbone models (o3, GPT-5, Gemini-2.5-Pro, o4-mini, DeepSeek-R1-0528, GPT-4o); the instruction styles NORM, STRICT and BASIC are compared only under REF+MS (Section 3.1, p. 5). The method is defined as: “A single-pass evaluator prompts a backbone model M (which may or may not be the same as MMS) to grade a solution s in one step.” (Section 3.1, p. 5). The paper selects the configuration minimizing an empirical loss on its dataset (Introduction, p. 2). Table 1 reports means with ± 95% confidence intervals. For OpenAI o3, REF+MS has RMSE 1.273 ± 0.16, MAE 0.964 ± 0.12, within-one (WTA≤1) 76.5 ± 4.3%, Kendall tau 0.502, and bias −0.008; NONE has RMSE 1.901 ± 0.15, MAE 1.680 ± 0.15, within-one 49.5 ± 5.8%, tau 0.435, and bias 0.924 (Table 1, p. 6). The authors conclude: “We observe effect sizes ordered as backbone ≫ context ≫ instruction.” (Section 3.3, p. 7).
Inference: A Verus-oriented evaluator can inspect generated Rust plus its specifications and classify missing obligations before invoking verification. It should report concrete failed obligations rather than a 0–7 proxy; only verus!, requires, ensures, invariant, assert, proof fn, and related constructs documented in the Verus notes are appropriate. The paper’s contextual gains support supplying the function contract and relevant lemmas to a review prompt, but do not establish soundness.
technique 3: ensemble and staged evaluation
To reduce variance, run the same evaluator independently five times and aggregate ratings by mean or median. The paper defines ensembling as a method that “runs the same evaluator independently multiple times and combines the individual ratings with an aggregation operator, such as the mean or median.” (Section 3.1, p. 5). Under o3 REF+MS, averaging five runs reduced RMSE from the best single run’s 1.225 to 1.169 and improved Kendall tau from 0.540 to 0.578 (Table 4 and Section 3.4, pp. 7–8); the paper itself says the absolute gain “seems modest”, with variance reduction as the main advantage. Two staged alternatives are Binary+Errors → Fine-Grained, then Evaluate → Reflect → Verdict; the former first predicts binary correctness and key errors, then emits a calibrated score, while the latter evaluates, critiques, and revises. The paper states: “The LLM first performs a complete initial evaluation. It is then prompted to reflect on and critique its own assessment. Finally, it uses the original context, its initial judgment, and its self-critique to produce a final score.” (Section 3.1, pp. 5–6). Staging helped the weaker O4-mini (RMSE 1.816→1.650; MAE 1.367→1.245) but hurt o3 (Table 5, p. 8); the paper reports that in the Evaluate → Reflect → Verdict variant reflection gave only small improvements and the final verdict added no value (Section 3.4, p. 8; Table 6, p. 9). Staging is not universally beneficial.
Inference: VL could ensemble independent diagnosis prompts, but the final acceptance must be a deterministic Verus verification run. Reflection can prioritize likely missing invariants; it cannot repair an invalid proof by itself.
downstream selection and limits
ProofGrader is tested as a best-of-N selector over 16 generated proofs, with Monte Carlo subsets. At N=16 it achieves average selected score 4.14/7, versus 2.48 for a binary evaluator and 4.62 for a human oracle, closing 78% of that gap (Introduction, p. 2). The paper manually inspected 50 solutions where 2 of 5 ensemble runs deviated from human scores by at least 2 points, and reports over-crediting (10.8%) and under-crediting (12.2%) at similar rates (Section 3.5, p. 8); Appendix H describes these rates as over- and under-crediting by more than one point and does not give the denominator. No-context evaluators overestimated correctness in over 60% of cases; for proofs scored 0–2 they over-scored by 1.7 points on average, while contextual evaluation assigned high-quality (5–7) proofs 0.8 points more on average (Section 3.5, p. 9). Inference: These numbers have different bases: the failure rates and score gaps come from the paper’s error analyses on ProofBench, whereas 4.14/7 is a best-of-16 mean over Monte Carlo subsets of a separate set of 29 problems with 464 o3 proofs (Section 4, p. 9). The benchmark measures agreement with human grading, not theorem validity, and the authors write “we have not yet trained with it; incorporating it into proof generator training is a promising future direction” (Conclusion, p. 12).
Inference: The product risk is moderate for agent-written verified Rust: an evaluator can miss a false lemma or over-credit a plausible explanation, but a successful Verus check protects the final artifact. VL should reuse the paper’s context design, independent-run aggregation, and failure analysis, while treating every LLM judgment as untrusted guidance.
techniques for the catalog
- problem-specific marking scheme: generate score conditions and zero-credit cases from a problem and references, then expert-review them
- context-controlled evaluator: compare backbone, reference, marking scheme, and instructions on held-out expert scores
- evaluator ensembling: run identical grading prompts independently and aggregate scores
- staged evaluator: separate binary/error detection, fine-grained scoring, and optional reflection
- best-of-N selection: use evaluator scores to select among generated candidates and compare against a human oracle Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “On the 0–7 scale, scores naturally cluster into four bands: incorrect (0), partial progress (1–3), nearly complete (4–6), and fully correct (7).”): read the whole paper including appendices and checked every quotation, number, section and page reference and technique step; changed the section for the 87.5% agreement figure (2.1, not 2.2), quote pages (marking-scheme quote p. 4 not p. 3; reflection quote pp. 5–6; failure analysis p. 8; the future-work statement is in the Conclusion, p. 12, not the Introduction), the Table 1 NONE row for o3 (WTA 49.5 ± 5.8, tau 0.435, bias 0.924), the Table 4 tau (0.578, not 0.568), the failure-rate denominator claim, the held-out-set and 435-evaluation claims, and added the optional AI-judgment caveat; did not check the arXiv link beyond the paper’s own arXiv stamp (2510.13888) or the figures beyond the text extraction, and the Inference lines about Verus are my judgment, not paper claims.
Last edited: