# Do We Need Frontier Models to Verify Mathematical Proofs?

arXiv: https://arxiv.org/abs/2604.02450 · HTML: https://mlsanity.com/paper/2604.02450/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 23 of its 24 references that are in the map.
- First posted on arXiv 2 Apr 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 23 of 23)

- [A Survey on LLM-as-a-Judge](https://mlsanity.com/paper/2411.15594/) (2024)
- [Understanding the Effects of RLHF on LLM Generalisation and Diversity](https://mlsanity.com/paper/2310.06452/) (2023)
- [Cognitive Behaviors that Enable Self-Improving Reasoners, or, Four Habits of Highly Effective STaRs](https://mlsanity.com/paper/2503.01307/) (2025)
- [MathArena: Evaluating LLMs on Uncontaminated Math Competitions](https://mlsanity.com/paper/2505.23281/) (2025)
- [ProcessBench: Identifying Process Errors in Mathematical Reasoning](https://mlsanity.com/paper/2412.06559/) (2024)
- [Inference-Time Scaling for Generalist Reward Modeling](https://mlsanity.com/paper/2504.02495/) (2025)
- [PRMBench: A Fine-grained and Challenging Benchmark for Process-Level Reward Models](https://mlsanity.com/paper/2501.03124/) (2025)
- [Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad](https://mlsanity.com/paper/2503.21934/) (2025)
- [Towards Robust Mathematical Reasoning](https://mlsanity.com/paper/2511.01846/) (2025)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [A Survey of Process Reward Models: From Outcome Signals to Process Supervisions for Large Language Models](https://mlsanity.com/paper/2510.08049/) (2025)
- [Shrinking the Generation-Verification Gap with Weak Verifiers](https://mlsanity.com/paper/2506.18203/) (2025)
- [Premise-Augmented Reasoning Chains Improve Error Identification in Math reasoning with LLMs](https://mlsanity.com/paper/2502.02362/) (2025)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Variation in Verification: Understanding Verification Dynamics in Large Language Models](https://mlsanity.com/paper/2509.17995/) (2025)
- [Reliable Fine-Grained Evaluation of Natural Language Math Proofs](https://mlsanity.com/paper/2510.13888/) (2025)
- [VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks](https://mlsanity.com/paper/2511.04662/) (2025)
- [Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection](https://mlsanity.com/paper/2511.13027/) (2025)
- [Graph of Verification: Structured Verification of LLM Reasoning with Directed Acyclic Graphs](https://mlsanity.com/paper/2506.12509/) (2025)
- [Verdict: A Library for Scaling Judge-Time Compute](https://mlsanity.com/paper/2502.18018/) (2025)
- [StepProof: Step-by-step verification of natural language mathematical proofs](https://mlsanity.com/paper/2506.10558/) (2025)
- [Auto-Prompt Ensemble for LLM Judge](https://mlsanity.com/paper/2510.06538/) (2025)
- [Explicit Reasoning Makes Better Judges: A Systematic Study on Accuracy, Efficiency, and Robustness](https://mlsanity.com/paper/2509.13332/) (2025)

## Built on by (most cited first, 3 of 3)

- [Cost-Effective Automated Judging of Natural-Language Mathematical Proofs](https://mlsanity.com/paper/2608.00004/) (2026)
- [Learning Strategies to Break Judges](https://mlsanity.com/paper/2609.33773/) (2026)
- [One-Sided Verification Under Limited Expert Review](https://mlsanity.com/paper/2610.18089/) (2026)

## Abstract (arXiv)

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.