用廉价模型自动判数学证明，成本降百倍仍准确。
Cost-Effective Automated Judging of Natural-Language Mathematical Proofs
- 三款低成本模型结合人类评分标准判断证明对错
- 在200个样本上与顶级模型一致率达统计无差异
- 推荐全票通过规则，适合大规模自动化评测
评估自然语言数学证明的代价高昂，前沿大模型评判成本过高。我们探究在给定候选证明、标准答案和人工评分标准的前提下，廉价开源模型是否可作为可靠评判者。在包含200个实例的IMO-GradingBench验证集上，三款低成本模型（GPT-OSS 120B、DeepSeek-V4 Flash、Gemma-4 31B）与人类通过/失败判定的一致率在统计上与Claude Opus 4.7和Gemini 3.1 Pro无显著差异，成本低至其1/100。尽管预期多数投票最优，但实际表现仅匹配最强个体，未进一步提升。扩展至1000实例并测试共识规则，发现要求全票通过（all-three-pass）时，通过率一致性和精确度最高，且在四次重复实验中波动最小。核心结论：廉价模型在成本低一到两个数量级的情况下，表现可比肩前沿模型；建议默认采用all-three-pass，但该规则为事后发现，需独立验证。
原文摘要 · Abstract (English)
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, three cheap judges (GPT-OSS 120B, DeepSeek-V4 Flash, Gemma-4 31B) agree with human pass/fail decisions at rates statistically indistinguishable from Claude Opus 4.7 and Gemini 3.1 Pro, at up to $100\times$ lower cost. We had expected a majority vote of the three to be the best budget option; it matched the frontier but did not improve on its strongest member. Extending to the full 1000-instance benchmark and exploring consensus rules, we found that requiring unanimous agreement (all-three-pass) reaches the highest pass-agreement and precision and, on four replicate runs, the smallest run-to-run spread. The headline finding is that cheap judges are competitive with the frontier at one to two orders of magnitude lower cost; as a deployable default we recommend all-three-pass, with the caveat that this rule was identified post-hoc and warrants independent replication.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。