自然语言数学证明的高性价比自动评判
Cost-Effective Automated Judging of Natural-Language Mathematical Proofs
浏览论文内容
中文总结 AI 辅助
该研究以 IMO-GradingBench 为基准，验证 GPT-OSS 120B 等三个低成本模型作为数学证明评判器的效果，发现全票通过规则的低成本方案与前沿模型效果相当，成本低达 100 倍。
中文摘要 AI 辅助
对自然语言数学证明进行评分是评估数学推理系统的一项持续成本，而前沿大型语言模型（LLM）评判器的成本很高。我们提出，在给定候选证明、真实证明和人工评分规则的情况下，低成本的开源权重模型能否成为可靠的评判器。在 IMO-GradingBench 的 200 个实例验证样本上，三个低成本评判器（GPT-OSS 120B、DeepSeek-V4 Flash、Gemma-4 31B）与人工通过/不通过决策的一致率在统计上与 Claude Opus 4.7 和 Gemini 3.1 Pro 无差异，成本却低达 100 倍。我们原本预计这三个模型的多数投票会是最佳预算选项，其表现与前沿模型相当，但并未优于其中最强的单个模型。扩展到完整的 1000 个实例基准并探索共识规则后，我们发现要求全票通过（三个模型均通过）可达到最高的通过一致率和精度，且在四次重复运行中，运行间差异最小。核心发现是低成本评判器与前沿模型具有竞争力，成本却低一到两个数量级；作为可部署的默认方案，我们推荐全票通过规则，但需注意该规则是事后确定的，需要独立重复验证。
英文摘要
Grading natural-language mathematical proofs is a recurring cost in evaluating math-reasoning systems, and frontier LLM judges are expensive. We ask whether cheap open-weight models can serve as reliable judges given a candidate proof, a ground-truth proof, and a human-grading rubric. On a 200-instance validation sample of IMO-GradingBench, two of three cheap judges (GPT-OSS-120B, DeepSeek-V4-Flash) and their three-model consensus are statistically no worse than the frontier (Claude Opus 4.7, Gemini 3.1 Pro) on agreement with human pass/fail decisions, at 4-100$\times$ lower cost. On the full 1000-instance benchmark, the choice of consensus rule over the three judges is a precision/recall dial: unanimous (all-three-pass) rules reach the highest precision (0.855), majority vote the highest recall (0.912); across four replicate runs the unanimous rule is also the steadiest. No rule won outright; the dial replicated on a held-out 600-instance split and on the independent ProofBench. In this domain, cheap judges are competitive with the frontier at one to two orders of magnitude lower cost, and unanimity is the right setting when false positives are costly.
