Can LLMs Reliably Grade Olympiad Proofs? A Study of Mathematical Verification with LLMs

📄 arXiv: 2610.36767v1 📥 PDF

作者: Azim Ospanov, Zijin Feng, Ding Ding, Chengwu Liu, Haoli Bai, Jiacheng Sun, Lifeng Shang, Farzan Farnia

分类: cs.AI

发布日期: 2026-10-27

🔗 代码/项目: GITHUB

💡 一句话要点

提出MABGrader以提升奥林匹克数学证明的验证准确性

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 数学证明 自动化评分 多臂老虎机 教育技术 验证系统

📋 核心要点

  1. 现有的数学证明验证方法主要依赖专家评审，难以满足大规模需求，且效率低下。
  2. 本文提出MABGrader框架，将评分问题重新定义为在离散评分空间中的臂选择，提升了验证的准确性。
  3. 实验结果表明，MABGrader在Quadratic Weighted Kappa指标上比现有的ProofGrader提高了26.4%，显著降低了评分错误。

📝 摘要（中文）

大型语言模型（LLMs）在解决竞赛级数学问题上取得了显著进展，但其在验证自然语言数学证明方面的能力仍然相对欠缺。尤其是奥林匹克级证明，需要对长推理链中的每个主张进行细致评估。当前的验证主要依赖专家检查，难以规模化。本文系统研究了LLM在此场景下的验证能力，提出了一个人类策划的数据集，并评估了多种LLM验证器。我们还提出了TROJAN，一个迭代自我批评的流程，用于大规模生成高保真对抗性证明。实验结果显示，现有模型仍有显著提升空间，MABGrader框架在评分上表现优于现有方法，减少了14%的评分错误。

🔬 方法详解

问题定义：本文旨在解决大型语言模型在验证奥林匹克数学证明时的准确性不足问题。现有方法依赖人工专家评审，难以扩展且成本高昂。

核心思路：论文提出MABGrader框架，通过将评分视为在离散评分空间中的臂选择，优化了评分过程。该方法利用多臂老虎机算法提高了评分的准确性和效率。

技术框架：整体架构包括数据集构建、模型评估和MABGrader框架的实现。数据集由人类专家评分的USAMO 2025候选解组成，评估涵盖20种模型和多种评估指标。

关键创新：MABGrader是本研究的核心创新点，通过引入多臂老虎机算法，显著提升了评分的准确性，与传统方法相比具有本质区别。

关键设计：在MABGrader中，设计了特定的参数设置和损失函数，以优化模型在评分过程中的表现。通过多种推理方法和模板，确保了模型的灵活性和适应性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果显示，MABGrader在Quadratic Weighted Kappa指标上比现有的ProofGrader提高了26.4%，并且成功减少了14%的评分错误。这表明MABGrader在数学证明验证任务中具有显著的性能优势。

🎯 应用场景

该研究的潜在应用领域包括教育评估、自动化评分系统和数学竞赛的辅助工具。通过提高数学证明的验证效率，能够减轻专家的工作负担，并为大规模教育场景提供支持，未来可能对教育技术领域产生深远影响。

📄 摘要（原文）

Large Language Models (LLMs) have made remarkable progress on solving competition-level mathematics, yet their ability to verify natural-language mathematical proofs remains relatively underexplored. This gap is especially pronounced for Olympiad-level proofs, which require meticulous assessment of each claim in a long reasoning chain. Current proof verification thus primarily relies on expert inspection, which is costly to scale. In this paper, we present a systematic study of LLM-based verification in this setting. Specifically, we introduce a human-curated dataset of USAMO 2025 candidate solutions with expert grading, and conduct a broad evaluation of existing LLM verifiers across frontier models. We also propose TROJAN, an iterative self-critique pipeline for generating high-fidelity adversarial proofs at scale. Our comprehensive evaluation covers 20 models spanning seven metrics, two prompt styles, three inference methods, and three prompt templates, showing that state-of-the-art models still leave considerable room for improvement. To narrow 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%. Code and dataset are available at https://github.com/aziksh-ospanov/TROJAN.