LLM 能可靠地评判奥林匹克竞赛证明吗？基于 LLM 的数学验证研究

大型语言模型（LLM）在解决竞赛级数学问题方面取得了显著进展，但其验证自然语言数学证明的能力仍未得到充分研究。对于奥林匹克竞赛级别的证明而言，这一空白尤为明显，因为此类证明需要对冗长推理链中的每个论断进行细致评估。目前，证明验证主要依赖专家审查，而这种方式难以大规模推广且成本高昂。在本文中，我们针对这一场景对基于 LLM 的验证进行了系统研究。具体而言，我们引入了一个由人工整理、包含 USAMO 2025 候选解答及专家评分的数据集，并对现有的 LLM 验证器在各类前沿模型上的表现进行了广泛评估。我们还提出了 TROJAN，这是一种迭代式自我批评流程，用于大规模生成高保真对抗性证明。我们的综合评估涵盖 20 个模型、七项指标、两种提示风格、三种推理方法和三种提示模板，结果表明，当前最先进的模型仍有相当大的改进空间。为缩小这一差距，我们提出了 MABGrader，这是一种多臂老虎机框架，将评分重新定义为在离散分数空间上的臂选择问题。MABGrader 在二次加权 Kappa 指标上比 SOTA ProofGrader 高出 26.4%，并将评分误差降低了 14%。代码和数据集见 https://github.com/aziksh-ospanov/TROJAN。