Can LLMs Reliably Grade Olympiad Proofs? A Controlled Study of Mathematical Verification with LLMs
Abstract
Large Language Models (LLMs) have made remarkable progress on solving competition-level mathematics, yet their ability to verifying natural-language mathematical proofs remains relatively underexplored. Current proof verification primarily relies on expert inspection that is costly to scale and Olympiad-level problems represent a significant challenge in this area, as they require the meticulous evaluation of every claim in the reasoning chain. In this paper, we present a systematic study of LLM-based verification in this setting. Specifically, we introduce a human-curated dataset of 48 USAMO 2025 candidate solutions with expert grading, conduct a broad study of existing LLM verifiers in Olympiad mathematics across frontier models. We also propose an iterative self-critique pipeline TROJAN to generates high-fidelity adversarial proofs at scale. Our evaluation spans 20 models on 7 metrics across two prompt styles with three inference methods and three prompt templates, illustrating that the state-of-the-art models still have more room for improvement. To address this gap, we propose MABGrader, a Multi-Armed Bandit framework that reframes grading as arm selection over the discrete score space. MABGrader outperforms the SOTA ProofGrader by 26.4% in Quadratic Weighted Kappa and reduces grading error by 14%.