Do We Need Frontier Models to Verify Mathematical Proofs?

• URL: http://arxiv.org/abs/2604.02450v1
• Date: Thu, 02 Apr 2026 18:31:44 GMT
• Title: Do We Need Frontier Models to Verify Mathematical Proofs?
• Abstract summary: We show that smaller open-source models are only up to 10% behind frontier models in accuracy.<n>We then demonstrate that the smaller models, in fact, do possess the mathematical capabilities to verify proofs at the level of frontier models.<n>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.
• Score: 14.254472131009654
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• LLMs as a Jury: Cross-Model Consensus Can Outperform Process Reward Models for LLM Reasoning [6.241883798820154]
  We study cross-model consensus, the degree to which independently trained models, each solving the problem once, agree on a final answer.<n>We treat the panel as an LLM-jury, in which the structure of agreement, not any model's score of another, is the verification signal.<n>We make this precise with a parameter-free law, derived in closed form, that predicts consensus accuracy from three measured panel statistics to a mean absolute error of $0.03$.
  arXiv  Detail & Related papers  (2026-07-11T05:57:54Z)
• How reliable are LLMs when it comes to playing dice? [0.0]
  We investigate the reasoning capabilities of large language models through a controlled benchmarking study on discrete probability problems.<n>Models achieve an average accuracy of 0.96 on standard problems but only 0.59 on counterintuitive ones.<n> Embedding misleading suggestions in the prompt reduces performance by up to 34%, with no model proving immune.
  arXiv  Detail & Related papers  (2026-06-05T17:59:42Z)
• Learning to Reason Efficiently with A* Post-Training [119.18396754931602]
  We investigate whether large language models can learn to generate correct and efficient proofs with guidance from A* search.<n> Empirically, we find that Llama-3.2 models in the 1B--3B range benefit substantially from A* post training.<n>On larger search spaces, models trained with imperfects exhibit superior accuracy.
  arXiv  Detail & Related papers  (2026-05-23T14:28:57Z)
• FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models [0.0]
  We introduce textbfFormalRewardBench, the first benchmark for evaluating reward models in formal theorem proving with Lean 4.<n>Our results reveal that frontier LLMs achieve the highest performance (59.8%%) while specialized theorem provers perform the worst (24.4%)<n>We release textbfFormalRewardBench publicly to encourage more research on developing reward models in formal mathematics.
  arXiv  Detail & Related papers  (2026-05-11T07:51:15Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  Large Language Models (LLMs) have demonstrated strong math reasoning abilities through Reinforcement Learning with *Verifiable Rewards* (RLVR)<n>Many advanced mathematical problems are proof-based, with no guaranteed way to determine the authenticity of a proof by simple answer matching.<n>To enable automatic verification, a Reward Model (RM) capable of reliably evaluating full proof processes is required.
  arXiv  Detail & Related papers  (2026-02-02T17:42:53Z)
• Mitigating LLM Hallucination via Behaviorally Calibrated Reinforcement Learning [32.32593439144886]
  Behavior-calibrated reinforcement learning allows smaller models to surpass frontier models in uncertainty quantification.<n>Our model's log-scale Accuracy-to-Hallucination Ratio gain (0.806) exceeds GPT-5's (0.207) in a challenging in-domain evaluation.
  arXiv  Detail & Related papers  (2025-12-22T22:51:48Z)
• Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models [11.250861762443801]
  We introduce the RFMDataset (Reveal Failure Modes), a collection of 200 diverse mathematical proof problems.<n>We thoroughly evaluate advanced models' performance on it.<n>Our analysis uncovers 10 fine-grained error types, which shows fundamental limitations in current large reasoning models.
  arXiv  Detail & Related papers  (2025-06-20T16:14:18Z)
• ProcessBench: Identifying Process Errors in Mathematical Reasoning [62.80402845414901]
  We introduce ProcessBench for measuring the ability to identify erroneous steps in mathematical reasoning.<n>ProcessBench consists of 3,400 test cases, primarily focused on competition- and Olympiad-level math problems.<n>We conduct extensive evaluation on ProcessBench, involving two types of models: process reward models (PRMs) and critic models.
  arXiv  Detail & Related papers  (2024-12-09T15:11:40Z)
• An Assessment of Model-On-Model Deception [0.0]
  We create a dataset of over 10,000 misleading explanations by asking Llama-2 7B, 13B, 70B, and GPT-3.5 to justify the wrong answer for questions in the MMLU. We find that, when models read these explanations, they are all significantly deceived. Worryingly, models of all capabilities are successful at misleading others, while more capable models are only slightly better at resisting deception.
  arXiv  Detail & Related papers  (2024-05-10T23:24:18Z)
• The False Promise of Imitating Proprietary LLMs [158.65692029352584]
  An emerging method to cheaply improve a weaker language model is to finetune it on outputs from a stronger model. This approach looks to cheaply imitate the proprietary model's capabilities using a weaker open-source model. We first finetune a series of LMs that imitate ChatGPT using varying base model sizes. We then evaluate the models using crowd raters and canonical NLP benchmarks.
  arXiv  Detail & Related papers  (2023-05-25T05:00:12Z)
• How Can We Know When Language Models Know? On the Calibration of Language Models for Question Answering [80.82194311274694]
  We examine the question "how can we know when language models know, with confidence, the answer to a particular query?" We examine three strong generative models -- T5, BART, and GPT-2 -- and study whether their probabilities on QA tasks are well calibrated. We then examine methods to calibrate such models to make their confidence scores correlate better with the likelihood of correctness.
  arXiv  Detail & Related papers  (2020-12-02T03:53:13Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  We propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs. Our model learns to predict nodes and edges corresponding to proof graphs in an efficient constrained training paradigm. We conduct experiments on synthetic, hand-authored, and human-paraphrased rule-bases to show promising results for QA and proof generation.
  arXiv  Detail & Related papers  (2020-10-06T15:47:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.