Do We Need Frontier Models to Verify Mathematical Proofs?

Aaditya Naik; Guruprerana Shabadi; Rajeev Alur; Mayur Naik

cs.LGApr 2, 2026

Do We Need Frontier Models to Verify Mathematical Proofs?

Authors: Aaditya Naik, Guruprerana Shabadi, Rajeev Alur, Mayur Naik

Organizations: University of Pennsylvania, U.S.A.

Abstract

Advances in training, post-training, and inference-time methods have enabled frontier reasoning models to win gold medals in math competitions and settle challenging open problems. Gaining trust in the responses of these models requires that natural language proofs be checked for errors. LLM judges are increasingly being adopted to meet the growing demand for evaluating such proofs. While verification is considered easier than generation, what model capability does reliable verification actually require? We systematically evaluate four open-source and two frontier LLMs on datasets of human-graded natural language proofs of competition-level problems. We consider two key metrics: verifier accuracy and self-consistency (the rate of agreement across repeated judgments on the same proof). We observe that smaller open-source models are only up to ~10% behind frontier models in accuracy but they are up to ~25% more inconsistent. Furthermore, we see that verifier accuracy is sensitive to prompt choice across all models. We then demonstrate that the smaller models, in fact, do possess the mathematical capabilities to verify proofs at the level of frontier models, but they struggle to reliably elicit these capabilities with general judging prompts. Through an LLM-guided prompt search, we synthesize an ensemble of specialized prompts that overcome the specific failure modes of smaller models, boosting their performance by up to 9.1% in accuracy and 15.9% in self-consistency. These gains are realized across models and datasets, allowing models like Qwen3.5-35B to perform on par with frontier models such as Gemini 3.1 Pro for proof verification.

Figures & tables

Panel of Figure 1 — Figure 1: (Left) Mean balanced accuracy and self-consistency rates of frontier and open-source LLM judges across all datasets and prompts. Low and high-reasoning settings are denoted with ‘ $\bullet$ ’ and ‘ $\blacklozenge$ ’, respectively, while ‘ $\star$ ’ denotes performance after prompt ensembling. Smaller open-source models are only ${\sim}10\%$ behind frontier models in balanced accuracy, but are substantially less self-consistent. Prompt ensembling closes much of this gap, allowing models such as Qwen3.5-35B to approach frontier-level verifier performance. (Right) Overview of our prompt-ensemble method. A proof is evaluated under a collection of prompts with complementary roles, including general grading prompts and prompts specialized to different aspects of proof correctness. Their judgments are aggregated by threshold voting to produce a final verdict.

Figure 2: Comparing mean balanced accuracy of all the models on the combined dataset using the three prompts: IMOBench , GIMO , ProofBench7pt . The mean is computed over three independent runs and the error bars indicate the maximum and minimum balanced accuracies amongst the runs.

Panel of Figure 3 — Figure 3: False positive rates (left) and false negative rates (right) of few models on the combined dataset, compared across the three prompts.

Panel of Figure 4 — Figure 4: Two failure modes of GPT-OSS-120B with IMOBench prompt on IMO-GradingBench and how targeted prompts address them. Each column shows the proof excerpt (top), the IMOBench prompt’s reasoning (middle), and a targeted prompt’s response (bottom). Excerpts are marked by a thick left bar; red highlights mark errors. Yellow highlights mark fixed judgements. Case 1: the IMOBench prompt accepts the proof’s invalid inequality combination without investigating deeper, while Logic Chain Verifier catches the error. Case 2: the IMOBench prompt invents a core missing justification rather than flagging the reasoning gap as an error, while Proof Repair identifies the incomplete case analysis.

Panel of Figure 5 — Figure 5: Performance of the prompt ensemble on the three datasets.

Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 6: Self-consistency rate as a function of the number of independent samples for Qwen3.5-35B and GPT-OSS-120B on IMO-GradingBench. Consistency decreases monotonically as unanimous agreement is required across more samples.

Figure 7: Balanced accuracy vs self-consistency on IMO-GradingBench under two grading thresholds: only 7-point proofs treated as correct (left) vs both 6-point and 7-point proofs treated as correct (right).

Panel of Figure 8 — Figure 8: Mean balanced accuracy vs self-consistency across all datasets, including high reasoning effort variants (diamonds) for open-source models. Prompt ensemble results are shown as stars.

Figure 9: Comparison of ensemble strategies averaged across all datasets: the full diverse prompt ensemble, a single merged prompt (single-query ens.), and the best single prompt repeated 12 times with threshold voting (12 $\times$ same prompt). Base prompt performance shown as circles.

Figure 10: False positive rate (FPR) and false negative rate (FNR) of GPT-OSS 120B for each of the 12 error detection prompts and the IMOBench baseline on the full IMO-GradingBench dataset.

Figure 11: FPR and FNR comparison of open-source models (with and without the prompt ensemble) and frontier models on IMO-GradingBench.

Explore similar work

Jul 13, 2026

AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification

Large language models (LLMs) have achieved remarkable performance on high-school and competition-level mathematics, yet their capabilities on advanced mathematics remain poorly understood. Existing benchmarks, however, fall short in both scope and evaluation granularity: they provide limited disciplinary coverage and often rely on final-answer correctness or coarse judgments, leaving the validity of the reasoning process inadequately assessed. To bridge this gap, we introduce AdvancedMathBench, a benchmark suite designed to evaluate the reasoning capabilities of LLMs on advanced mathematical proofs. Its core generation benchmark, ProverBench, contains 245 problems spanning undergraduate (UG) and doctoral qualifying-exam (QE) levels. To reliably evaluate these proofs, we develop a dedicated automatic verification pipeline that is trained on large-scale expert annotations, produces both correctness verdicts and fine-grained analyses, and exhibits strong agreement with human experts on held-out proof trajectories. We further introduce VerifierBench, consisting of 888 model-generated proof trajectories paired with expert ground truth, to evaluate whether models can correctly judge proof validity and provide sound verification rationales. Experiments show that AdvancedMathBench remains challenging for frontier models. On proof generation, the best-performing model, GPT-5.5-xhigh, achieves only 64.5 and 48.9 on the UG and QE splits, respectively. On proof verification, the best model only attains a Balanced F1 of 65.1. Further analysis reveals a notable mismatch between proof generation and verification capabilities across models.

Lingkai Kong, Zijian Wu, Yuzhe Gu +11

Shanghai AI Laboratory · Shanghai Jiao Tong University · MMLab, The Chinese University of Hong Kong +1

Mathematical Reasoning Benchmarks Automated Theorem Proving Benchmark Design LLM Mathematical Reasoning

Ask PDF

Jun 9, 2026

Evaluating Research-Level Math Proofs via Strict Step-Level Verification

Large Language Models (LLMs) struggle to rigorously verify complex mathematical proofs. Standard global evaluation approaches suffer from "context poisoning," in which superficially plausible statements mask subtle logical flaws, leading to hallucination or over-skepticism. To address this, we shift from global evaluation to strict step-level verification: our framework maintains detailed context for each deduction step and strictly constrains the sources of applied theorems. We evaluate on a carefully curated adversarial diagnostic suite of research-level proofs drawn from the FirstProof challenge. A systematic ablation study demonstrates that these deductive constraints are indispensable, as unconstrained global prompting consistently fails to localize subtle logical errors. Beyond outperforming global evaluation, our approach fundamentally alters the failure taxonomy. Error analysis reveals that, rather than exhibiting severe logical hallucinations, remaining rejections are primarily instances of "pedantic hyper-rigor" stemming from unstated domain conventions, effectively exposing implicit ambiguities within the expert benchmark itself. Our findings suggest that prompting agents to organize their verification notes in a cautious, human-mathematician-like manner can substantially improve their ability to distinguish rigorous proofs from flawed ones, with the potential to strengthen agentic reasoning on frontier mathematical concepts that the base model does not already know well, and to lay a theoretical foundation for future automated proof-review systems. Code and prompts are available at GitHub.

Yifeng Sun

Independent Researcher

LLM Answer Verification Automated Theorem Proving LLM Mathematical Reasoning Reasoning Verification

Ask PDF

Oct 11, 2026

Review Rarely Beats the Stronger Model: Separating Verification from Capability Transfer in LLM Pipelines

Qwen3-8B reviewing Llama-3.1-8B in math adds 33.2 points, yet Qwen3-8B alone is 6.4 points more accurate than the result. Reviewing another model's answer is usually judged by its gain over the generator. We show that this confuses verification, which adds accuracy beyond either model alone, with capability transfer, where a stronger reviewer supplies answers it could have given on its own. Measured against the stronger model alone, across 48 pairs of 12 open-weight models (3B to 72B) in math, knowledge, code and reasoning, review beats it in only 9 of 96 review directions, and does worse the larger the capability gap. The reason is anchoring: the reviewer mostly follows the generator, discarding its own correct answers. Review costs 2.6 to 2.8 times as much as the stronger model alone, while a selector using the same two calls is 2.7 to 4.2 points more accurate than review and cheaper. Studies of verification should report the stronger model alone, not only the gain over the generator.

Yirui Zhang, Yash Raj Shrestha

University of Lausanne

LLM Answer Verification LLM Evaluation LLM-as-a-Judge

Ask PDF