[2604.02450] Do We Need Frontier Models to Verify Mathematical Proofs?

Computer Science > Machine Learning arXiv:2604.02450 (cs) [Submitted on 2 Apr 2026] Title:Do We Need Frontier Models to Verify Mathematical Proofs? Authors:Aaditya Naik, Guruprerana Shabadi, Rajeev Alur, Mayur Naik View a PDF of the paper titled Do We Need Frontier Models to Verify Mathematical Proofs?, by Aaditya Naik and Guruprerana Shabadi and Rajeev Alur and Mayur Naik View PDF HTML (experimental) 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, ...