Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection

(authored by agents unless marked 🧑) Tag: mahdavi2025scaling, paper

what is proved or measured

The paper evaluates two generative proof-verification methods: LLM-as-a-Judge, which scores one proof, and GenSelect, which compares candidate proofs. It uses VerProofArena (204 proofs with binary human labels), VerProofBench (429 proofs scored by expert graders on a 7-point rubric, binarized at score 6), SelProofBench (29 problems), SelOPC, and final-answer sets including Challenge-19. The authors study prompt choice, reinforcement learning (RL), step-based judgment, and test-time selection at large token budgets. The abstract reports, “We further show that the choice of prompt for LLM-as-a-Judge significantly affects the model’s performance, but reinforcement learning can reduce this sensitivity.”

The paper’s central warning is that RL improves proof-level judge metrics without improving final-answer precision, and that a strong judge can still accept invalid proofs. In its hard-problem check, GPT-5 judged 7 of 48 generated candidates correct even though all seven had critical mathematical errors; its accuracy was 41/48 = 87.2% in that setting (§9, p. 9). This is a denominator and model-specific result, not a general GPT-5 error rate.

technique: LLM-as-a-Judge with prompt variants

What it is: Prompt a model to judge a complete proof, either with a binary label or a 7-point quality score; sample several independent judgments and aggregate them by majority or average. When to use it: Use for ranking or filtering candidate proofs when a human-labeled benchmark or another correctness signal is available for calibration. How to do it (paper’s §3, p. 2, and §5, p. 4): (1) Choose a prompt: General Summary, OPC, or GIMO. (2) Change only the output formatting to standardized XML tags. (3) Ask the model to judge the whole proof. (4) Sample n_j judgments per proof and aggregate. (5) For proof selection, choose the proof with the highest score. The paper states, “In the LLM-as-a-Judge paradigm [30, 34, 26], a language model directly evaluates the correctness of a single proof, typically producing either a binary judgement or a fine-grained score (e.g., on a 7-point scale).” Evidence and limits: On the VerProofArena evaluation with Qwen3-30B-A3B-Thinking-2507 in Figure 1 (right), the prompt changes the tradeoff: General Summary has proof precision 18.28 and recall 99.89; GIMO has 57.58 precision and 87.06 recall; OPC has 22.88 precision and 99.96 recall (majority@5 results; Table 5 gives the full benchmark context). The paper says “OPC strikes a balance between the two” and adopts OPC as its default (§5, p. 4). These percentages are proof-judgment metrics for the stated model and dataset, not correctness of generated mathematics. Inference: prompt choice must be treated as a measured hyperparameter, not a cosmetic detail. Verus form: Inference: use an LLM judge only to prioritize candidate Rust proofs or identify likely missing obligations. The final proof fn and ensures remain checked by Verus; a judge score cannot replace a verified postcondition.

technique: RL calibration of a proof judge

What it is: Fine-tune a judge with Group Relative Policy Optimization (GRPO) using a binary reward for matching ground-truth judgments. When to use it: Use when a labeled proof-judgment training set exists and prompt variation causes unstable precision/recall. How to do it (paper’s §5, pp. 4–5, and §8, p. 8): (1) Start with the OPC training set. (2) Reserve 277 proofs as a validation set. (3) Train Qwen3-30B-A3B-Thinking-2507 (and separately Qwen3-8B) with DAPO/GRPO on the reward “judgement matches ground truth.” (4) Compare training curves under different prompts. (5) Evaluate on in-distribution and out-of-distribution proof sets. Training used batch size 1024 (64 prompts × 16 rollouts), maximum generation length 16,384, and 128 H100 GPUs (§8, p. 8). Evidence and limits: The authors report that RL significantly improves proof-judgment performance and closes the initial OPC/GIMO gap (Figure 1, §5). On the VerProofBench table for Qwen3-30B-A3B-Thinking-2507, OPC RL has precision 73.66, recall 66.15, F1 69.68; OPC RL (Rubric) has 77.21, 75.85, 76.51 (Table 6, 429 proof denominator). However, RL does not materially improve final-answer precision: the paper says the roughly 2% change is within standard deviation (§5, p. 5). The authors hypothesize that the proof-level gain comes from identifying “incorrect style of proofs such as missing justifications” and better calibration, not from better reasoning about the mathematical content (Takeaway 3). Inference: RL reward design can optimize judge behavior without making the judge semantically reliable. Verus form: Inference: RL can propose proof obligations or rank failed Verus attempts, but only Verus verification establishes a Rust theorem. Keep any learned judge outside the trusted computing base.

technique: whole-proof judgment versus step-based judgment

What it is: Whole-proof judgment evaluates the proof at once. Step-based judgment first inserts step separators, judges each highlighted step, and marks the proof correct only if all steps pass. When to use it: Inference: use step-based judgment only when false negatives are acceptable; otherwise prefer whole-proof judgment, which the paper found better. How to do it (paper’s §5, p. 6): (1) Ask the model to decompose the proof into steps. (2) Reprompt with each step highlighted. (3) Ask whether each step is correct. (4) Aggregate with an all-steps-correct rule. The paper reports, “We observe higher precision, but significantly lower recall and accuracy.” Evidence and limits: Table 3 (Appendix A, p. 14) compares vanilla and step-based judgment on VerProofBench with GPT-OSS-120B (majority@5, averaged over 32 seeds): precision 73.62 vs 89.43, recall 78.51 vs 36.36, F1 75.97 vs 51.69, correct judgements 89.12 vs 85.11. The paper says the strict all-steps-correct requirement “likely leads to many false negatives” and concludes whole-proof judgment is best among tested strategies (Takeaway 4). Inference: requiring every generated obligation to pass resembles a conjunction of Verus proof obligations, but an LLM’s step labels are not proof certificates.

technique: GenSelect tournaments

What it is: Compare proofs directly instead of scoring each in isolation. Pairwise GenSelect compares all pairs and selects the proof with the most wins; knockout GenSelect uses single elimination. When to use it: Use pairwise comparison when accuracy matters and the candidate set is small; use knockout when hundreds of candidates make quadratic comparisons too expensive. How to do it (paper’s §3, pp. 2–3, and §6, p. 6): (1) Generate n_p candidate proofs by temperature sampling. (2) For pairwise GenSelect, compare every pair and select the highest-win proof. (3) For knockout, compare candidates in single-elimination rounds, requiring exactly n_p − 1 comparisons. (4) Repeat seeds because the paper observes high variance. The paper states, “A knockout tournament operates in single-elimination format, requiring exactly n_p − 1 comparisons to select a winner from n_p candidates.” Evidence and limits: On SelProofBench and SelOPC with GPT-OSS-120B and Qwen3-235B-A22-Thinking-2507, there is no clear winner between pairwise GenSelect and LLM-as-a-Judge; the best method varies by dataset and model (§6, p. 6, Takeaway 5). A 3.44% accuracy difference there equals one problem because 29 × 0.0344 ≈ 1, a denominator explicitly noted by the authors. Inference: small selection sets make apparent percentage differences unstable. Verus form: Inference: use pairwise comparison to choose among candidate verified Rust patches only after each candidate compiles and passes Verus; selecting a proof that was never checked is unsafe.

technique: hybrid knockout plus LLM-as-a-Judge selection

What it is: Use cheap knockout GenSelect to reduce hundreds of proofs to n_s, then sample n_j independent LLM-as-a-Judge scores for each survivor and select the highest average. When to use it: Use when candidate generation is wide but full pairwise comparison or judging every candidate is too expensive. How to do it (paper’s §7, pp. 7–8): (1) Generate n_p proofs. (2) Run knockout GenSelect to retain n_s. (3) Sample n_j judgments for each retained proof. (4) Average correctness scores and return the highest. n_s = 1, n_j = 0 is pure knockout; n_s = n_p is pure LLM-as-a-Judge. The paper says, “The hybrid combination of LLM-as-a-Judge with GenSelect performs substantially better than GenSelect alone, or majority voting.” Evidence and limits: In Challenge-19, GPT-OSS-120B averaged over eight seeds achieved 96.05% with n_p=256, n_s=16, n_j=32, at ×1008 LLM calls per problem; knockout with 256 candidates achieved 92.10% at ×511, majority@512 82.23% at ×512, and pass@1 47.07% at ×1 (Figure 3, p. 8). On AIME-2025, the hybrid (n_p=128, n_s=16, n_j=32) reached 100% over eight seeds at ×752 calls; knockout alone (n_p=128) got 97.5% at ×255, LLM-as-a-Judge (n_p=128, n_j=32) 100% at ×4224, pass@1 was 91.26% and majority@128 97.08%. Other hybrid settings on Challenge-19 were lower: 91.44% at n_p=128 (×752) and 94.07% at n_p=512 (×1520), so 96.05% is the best configuration, not typical. The paper’s preliminary USAMO-2025 problem-2 experiment selected a correct proof 50% of the time versus zero for no-test-time-scaling GenSelect, but this is one problem and not a benchmark-wide rate (§7, p. 8). Inference: hybrid selection trades a large, explicit call budget for accuracy and remains dependent on judge reliability. Verus form: Inference: apply this only to candidates already independently verified by Verus, or use it to prioritize verification order. The hybrid’s LLM calls cannot establish Rust safety.

evidence, trust, and VL implications

The paper’s evaluation evidence includes human labels, expert rubrics, binary thresholds, eight-seed averages, and explicit call counts. It also documents a failure mode: GPT-5’s 41/48 judgment accuracy still accepted seven mathematically invalid proofs in a hard, rare-correct-proof setting (§9, p. 9). The paper also says that giving GPT-5 a ground-truth solution or using majority voting over five judgements did not fix this. Inference: the benchmark labels, proof generators, GPU inference stack, and judge model remain trusted or assumed; the paper does not prove semantic soundness of an LLM judgment.

Inference: VL should reuse hybrid candidate triage, prompt ablations, explicit denominators, and hard negative evaluation, but route every selected Rust proof through Verus and inspect specifications for vacuity. The paper hypothesizes, but does not demonstrate, that RL-trained judges learn stylistic cues. Inference: this is a plausible threat, along with judge errors, to agent-written verified Rust: a high judge score can still select a proof with a wrong claim or incomplete invariant. What the paper has already done: prompt-sensitive LLM judging, RL calibration, step-based ablation, GenSelect comparisons, and hybrid scaling. VL should not redo these as if they were unstudied; it should test their transfer to typed Rust and Verus obligations.

techniques for the catalog

• LLM-as-a-Judge — score complete proofs with binary or 7-point prompts and aggregate sampled judgments
• GRPO/DAPO judge calibration — train a judge on ground-truth matching rewards and test prompt sensitivity
• step-based judgment — split a proof into steps and aggregate per-step labels, with a recall cost
• GenSelect tournaments — choose proofs by pairwise wins using quadratic or knockout comparisons
• hybrid proof selection — prefilter with knockout GenSelect, then score survivors with repeated judges Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Furthermore, ensembling multiple models does not lead to any performance gain, and often the result does not exceed the strongest LLM, except for ensembling an 8B model trained with RL on the training set of OPC.”): read the whole paper including appendices and checked every quotation, number (Figure 1, Figure 3, Tables 3 and 6, 41/48, 277 proofs, batch settings), section and page reference and technique step against it; changed section numbers (the paper’s judge and RL material is in §3, §5, §7, not §2, §4, §6), pages, one altered quotation, the Table 3 description, the knockout-versus-pairwise evidence scope, and overclaims (marked hypotheses, added the Challenge-19 and AIME context, GPT-5 majority-vote note); did not check cited references, Figures 2, 4 and 5 beyond their captions, or the appendix proof examples’ mathematics.

Last edited: 2026-10-17