arXiv cs.AI· Azim Ospanov, Zijin Feng, Ding Ding, Chengwu Liu, Haoli Bai, Jiacheng Sun, Lifeng Shang, Farzan Farnia·· 12 小时前AI 评分35
LLM 能否可靠批改奥赛证明?一项基于 LLM 的数学验证研究
Can LLMs Reliably Grade Olympiad Proofs? A Study of Mathematical Verification with LLMs
AI 导读
研究构建了含专家评分的 USAMO 2025 候选解答数据集,系统评估 LLM 对奥赛级自然语言证明的验证能力,覆盖 20 个模型、7 项指标、2 种提示风格、3 种推理方法和 3 种提示模板,结果显示 SOTA 模型仍有明显提升空间。
正文 · AI 翻译
摘要:大型语言模型(LLM)在解决竞赛级数学问题方面取得了显著进展,但其验证自然语言数学证明的能力仍相对缺乏探索。这一差距在奥赛级证明中尤为明显,因为这类证明需要对长推理链中的每一项论断进行细致评估。因此,当前的证明验证主要依赖专家人工检查,而这种方式难以低成本地规模化。本文对这一场景下基于 LLM 的验证进行了系统研究。具体而言,我们引入了一个由人工整理、经专家评分的 USAMO 2025 候选解答数据集,并对前沿模型中的现有 LLM 验证器进行了广泛评估。我们还提出了 TROJAN,一种迭代式自我批判流水线,用于大规模生成高保真对抗性证明。我们的综合评估覆盖 20 个模型,横跨七项指标、两种提示风格、三种推理方法和三种提示模板,结果表明最先进的模型仍有相当大的改进空间。为缩小这一差距,我们提出了 MABGrader,一个多臂老虎机框架,将评分重新表述为在离散分数空间上的臂选择问题。MABGrader 在二次加权 Kappa 上比 SOTA 的 ProofGrader 高出 26.4%,并将评分误差降低了 14%。代码和数据集可在 此 https URL 获取。
| 学科: | 人工智能(cs.AI) |
| 引用为: | arXiv:2610.36767 [cs.AI] |
| (或 arXiv:2610.36767v1 [cs.AI] 用于此版本) | |
| https://doi.org/10.48550/arXiv.2610.36767 由 DataCite 颁发的 arXiv DOI(待注册) |
提交历史
来自:Azim Ospanov [查看邮箱]
[v1]
2026年10月27日星期二 07:28:08 UTC(20,980 KB)
来源:arXiv cs.AI · arxiv.org