自然语言数学证明的高性价比自动评判

# 具有成本效益的自然语言数学证明自动评判

来源：https://arxiv.org/html/2608.00004

###### 摘要

对自然语言数学证明进行评分是评估数学推理系统时反复出现的成本，而前沿 LLM 评判模型价格昂贵。我们探究的问题是：在给定候选证明、ground-truth 证明和人工评分 rubric 的情况下，廉价的开源权重模型能否作为可靠评判者？在 IMO-GradingBench 的 200 个实例验证样本上，三个廉价评判模型（GPT-OSS-120B、DeepSeek-V4-Flash、Gemma-4-31B）与人工 pass/fail 判定的一致率在统计上与 Claude Opus 4.7 和 Gemini 3.1 Pro 无法区分，而成本低至 100 倍。我们原本预期三者的多数投票是最佳预算选项；它确实与前沿模型持平，但并未超过其中最强的成员。将实验扩展到完整 1000 实例基准并探索共识规则后，我们发现要求一致同意（all-three-pass）能够达到最高的 pass 一致率和精确率，并且在四次重复运行中，运行间波动最小。核心发现是：廉价评判模型能以低一到两个数量级的成本与前沿模型竞争；作为可部署的默认配置，我们推荐 all-three-pass，但需注意该规则是事后确定的，有待独立重复验证。

LLM-as-a-judge、数学推理、自然语言证明评分、成本效率、开源权重模型

## 1 引言

AI 数学推理的基准测试越来越多地包含这样的问题：其解决方案是完整的自然语言证明，而不是简短的最终答案，而对这些证明进行评分是一个瓶颈。使用证明助手（如 Lean（de Moura and Ullrich, 2021 (https://arxiv.org/html/2608.00004#bib.bib1)））进行形式化验证能提供可信的保证，并已通过 AlphaProof 达到 IMO 金牌水平（Hubert 等，2025 (https://arxiv.org/html/2608.00004#bib.bib2)）。通过自动形式化和自进化证明器将其扩展到广泛的研究数学领域，是一个活跃的前沿方向；在该覆盖范围实现之前，大多数证明仍以自然语言评分，正如 2025 年前沿模型在 IMO 中获得金牌的结果所展示的那样。

虽然被研究的模型可以在不同实验之间变化，但评判模型必须可靠，并且在整个研究中保持固定，因此其成本是对整个研究工作的税收，而前沿评判模型价格昂贵。同样的成本会出现在自我改进系统中：一个生成、批判和修订证明的循环每一步都需要评判，因此昂贵的评判模型会限制此类系统的迭代次数。这引出了一个具体问题：*对于一个预算受限的研究者来说，是否存在可以信赖的廉价评判模型用于证明评分？*

我们在 IMO-GradingBench（Luong 等，2025 (https://arxiv.org/html/2608.00004#bib.bib3)）上研究这一评判任务，即 IMO-Bench 的评分拆分：1000 个实例，每个实例将一个奥林匹克竞赛问题与一个参考解答配对，同时给出候选证明和专家人工评分（采用标准的 0–7 IMO 量表）。评判模型阅读问题、参考解答和候选证明，并预测分数。我们有意将范围收窄；这是一项关于*评判*而非*解题*的研究，针对的是自带参考证明和人工评分的问题（而非无参考验证）。

我们先前预期，遵循 Panel-of-LLM-evaluators 的结果（Verga 等，2024 (https://arxiv.org/html/2608.00004#bib.bib4)），多个廉价模型的（多数投票）共识将是最安全的选择，因为偏移偏差应该会相互抵消。我们对此进行了测试：共识表现良好，但并未超过其中最强的单个模型。更有用且更普遍的发现是，廉价层整体具有竞争力：廉价开源权重评判模型在 pass/fail 与人工评分的一致性上能匹配前沿基线（Claude Opus 4.7、Gemini 3.1 Pro），而在我们的设置中成本低 1–2 个数量级。在完整基准上的一次事后规则搜索中，我们发现同一三人组的全体一致变体（all-three-pass）在 pass 一致率、精确率和稳定性方面均优于廉价和前沿评判模型，这也是我们在有待独立复现的前提下推荐的配置。

## 2 相关工作

LLM-as-a-judge（Zheng 等，2023 (https://arxiv.org/html/2608.00004#bib.bib5)）现已成为标准工具，但已知存在位置、冗长度和自我偏好偏差，并且对提示设计敏感（Gu 等，2024 (https://arxiv.org/html/2608.00004#bib.bib6)）。具体到证明而言，前沿模型即使最终答案正确，也常常无法生成有效论证（Petrov 等，2025 (https://arxiv.org/html/2608.00004#bib.bib7)），这促使了专门评分基准的出现，如 Open Proof Corpus（Dekoninck 等，2025 (https://arxiv.org/html/2608.00004#bib.bib8)）和 IMO-GradingBench（Luong 等，2025 (https://arxiv.org/html/2608.00004#bib.bib3)）。成本受到的关注较少：Verga 等 (2024 (https://arxiv.org/html/2608.00004#bib.bib4)) 表明，在 QA 和聊天机器人任务上，小模型小组能以约 7 倍更低的成本优于单个大评判模型。

两项同期工作为我们的贡献提供了背景。Ma 等 (2026 (https://arxiv.org/html/2608.00004#bib.bib9)) 搜索了评估器设计空间，并结合强推理主干、参考解答、评分方案和集成方法，达到了专家级一致率；我们研究的问题是，主干本身是否必须强大，并发现对于基于参考的 pass/fail 评分而言，它并不需要。Naik 等 (2026 (https://arxiv.org/html/2608.00004#bib.bib10)) 研究了与我们问题最接近的参考*无关*版本，并报告廉价评判模型在准确率上落后前沿模型约 10%，在自一致性上落后约 25%，而提示集成可以缩小这一差距。在我们的*基于参考*设置中（对照 ground-truth 解答进行评判），准确率差距完全消失。这与以下观点一致：参考解答承担了本应由评判模型完成的部分工作。我们没有测量自一致性，这仍是一个开放问题。

## 3 问题设定

我们考虑如下形式的评分实例：*(问题、ground-truth 解答、候选解答、人工评分)*。评判模型阅读前三项并输出一个分数；我们将它的分数与人工分数进行比较。对下游使用最重要的决策是 pass/fail 边界：候选证明是否达到标准（在 0–7 IMO 量表上得分 ≥ 6）？我们的主要指标是 pass 一致率：评判模型的 pass/fail 判定与人工判定一致的实例比例。我们报告该边界上的精确率、召回率和 F1，以及 Spearman 秩相关作为次要的序数度量（适用于粗粒度的 {0,1,6,7} 输出）。我们还报告单次评分的成本。

## 4 方法

#### 数据与采样。

从 IMO-GradingBench 的 1000 个实例（涵盖 30 个 IMO 风格问题）中，我们采用无放回均匀抽样，抽取两个不相交的 200 实例随机样本：一个*先验*（探索性）样本，种子为 42，用于探索和选择共识三人组；一个*验证*样本，种子为 7，从其余 800 个实例中抽取，用作干净的留出测试集。第 6.1 节 (https://arxiv.org/html/2608.00004#S6.SS1) 还报告了完整 1000 实例基准上的结果。除非另有说明，所有主要结果均基于验证样本。

#### 评判提示与评分桶。

每个评判模型使用相同的提示，并被要求输出 {0,1,6,7}（不正确 / 部分正确 / 基本正确 / 正确）中的分数；我们的解析器接受 0–7 之间的任何整数，少数非桶内分数（所有运行共 4 个，低于 0.1%）按解析结果计分。这种四桶方案遵循 IMO-GradingBench（Luong 等，2025 (https://arxiv.org/html/2608.00004#bib.bib3)）随附发布的公开评分提示，我们对其做了少量调整，以便我们的评判模型在既定的、外部定义的 rubric 下评分，而不是使用我们自己设计的 rubric。Pass/fail 和所有混淆矩阵指标均使用原始人工评分，因此一个人工评分为 4、而评判模型评分为 6 的实例会被正确计为假阳性。该基准还附带了每个问题的评分方案；我们不会将其提供给评判模型。

#### 评判模型与推理设置。

我们评估三个廉价开源权重模型（GPT-OSS-120B、DeepSeek-V4-Flash 和 Gemma-4-31B）以及两个前沿基线：Claude Opus 4.7 和 Gemini 3.1 Pro。选择这三个廉价模型是出于其成本-准确率权衡以及相互抵消的校准偏差（Gemma 倾向于多给分，DeepSeek-V4-Flash 倾向于少给分），这正是多数投票所需的组成要素。这些偏差方向在我们的重复运行中保持一致（第 6.2 节 (https://arxiv.org/html/2608.00004#S6.SS2)），因此三人组的多样性是模型本身的属性，而非某次运行的结果。*对于每个模型，我们使用其暴露出的最强推理配置。*这些设置并未归一化，也不能跨提供商直接比较：GPT-OSS-120B 以 effort=xhigh 运行，Gemma-4-31B 和 Gemini-3.1-Pro 开启推理（列为 effort=high），而 Claude Opus 4.7（自适应思考）和 DeepSeek-V4-Flash（默认）自行调节推理，因此我们报告其默认设置。每个表格中的 “Reasoning” 列标明了各模型的具体设置。

#### 共识规则。

廉价共识是三个廉价模型 pass/fail 判定的多数投票。我们还报告一个*连续*共识分数（成员分数的平均值），但这仅为完整性而设：由于对 {0,1,6,7} 桶输出取平均会产生任何单个评判模型都无法输出的中间值，共识 Spearman ρ 与单个评判模型的相关性不可比，因此我们自始至终将其省略（显示为 “—”）。多数投票是预先指定的共识规则；其他变体（两两组合、all-three-pass）是在第 6.1 节 (https://arxiv.org/html/2608.00004#S6.SS1) 的完整基准分析中，观察到多数投票在验证集上并未优于其最强成员之后才加入的。

#### 提供商、覆盖范围与重跑。

廉价开源权重评判模型通过 OpenRouter 由不断变化的第三方提供商池提供服务，量化级别各不相同；我们没有固定提供商，因此单个评判模型的 pass 一致率在不同运行之间可能会有几个百分点的波动（在第 6.2 节 (https://arxiv.org/html/2608.00004#S6.SS2) 中量化）。如需可复现的数字，请固定提供商并记录 served-provider 字段；前沿基线是第一方、单一提供商且稳定的。不到 2% 的评判调用在第一次尝试时未能返回可解析分数（瞬时限流，或推理超出 32k token 输出上限而未得出结论）；我们重新运行了这些调用（失控的调用通常在重试时收敛），并且从未替换为伪造分数。最终覆盖率：每个廉价评判模型为 1000/1000，每个前沿基线为 200/200。所有逐实例分数以及能够重新生成每个表格和图表的独立代码（仅使用标准库）均包含在补充材料中。

## 5 结果

表 1 (https://arxiv.org/html/2608.00004#S5.T1) 报告了按 pass 一致率排序的验证结果，并附 95% 自助法置信区间（1000 次重采样）。这是我们的主要比较：这是五种评判模型（前沿和廉价）进行正面交锋的唯一设置。图 1 (https://arxiv.org/html/2608.00004#S5.F1) 以森林图形式展示相同比较。

表 1：验证结果（n=200；指标基于有效回答）。Reasoning 列标明各模型的最大/自然设置（见第 4 节 (https://arxiv.org/html/2608.00004#S4)）；共识 Spearman ρ 省略（“—”），因为它与单个评判模型的相关性不可比。

图 1：验证样本（n=200）上六种系统（五种评判模型和廉价共识）与人工的 pass/fail 一致率（95% CI），按点估计排序，右侧为每 200 次调用的成本（前沿成本加框）。每个廉价评判模型的区间都与领先者的估计值（虚线）重叠，而成本比前沿基线低一到两个数量级。

#### 廉价层与前沿模型具有竞争力。

前五种系统（除 Gemma 外）的置信区间有大幅重叠。GPT-OSS-120B 的点估计最高，但最合理的解读是它是一个聚类中的领跑者，而非明确的胜者：在成对比较中，它与 Claude Opus 4.7 在统计上无法区分（重采样中更高的概率约为 P≈0.76），与 Gemma 也只有弱分离。我们的样本不足以支持任何单一模型最优的主张。但它确实支持这样的主张：廉价聚类位于前沿模型区间之内：三个开源权重评判模型，每个模型每 200 次评分成本不到 1 美元，却能匹配两个做同样工作需要花费 28–32 美元的模型。

#### 共识并未超过其最佳成员。

多数投票在 pass 一致率上追平了 Opus，但其一致率（0.855）和 F1（0.779）低于其最强的单个成员 GPT-OSS-120B（0.875、0.806），而成本约为后者的五倍（1.73 美元对 0.32 美元）。将强模型与两个较弱模型组合，结果是稀释而非改进。我们将在第 6.1 节 (https://arxiv.org/html/2608.00004#S6.SS1) 回到同一三人组采用不同共识规则是否效果更好的问题。

#### 价格差距非常显著。

GPT-OSS-120B 的评分为每实例 0.0016 美元，比 Claude Opus 4.7（0.162 美元）便宜约 100 倍，比 high reasoning 下的 Gemini 3.1 Pro（0.143 美元）便宜约 90 倍。表 1 (https://arxiv.org/html/2608.00004#S5.T1) 中的每个廉价评判模型都比任一前沿基线便宜一到两个数量级，而在 pass/fail 决策上没有一致的准确率损失。这是实践层面的核心结论。

#### 前沿模型仍然领先之处。

前沿模型在与人评分的秩相关方面保持优势：Opus（0.715）和 Gemini（0.704）高于廉价评判模型（0.62–0.68）。差距不大（Gemma 达到 0.676），但对于需要分级质量信号而非 pass/fail 门槛的应用而言，前沿评判模型仍然是更安全的选择。附录 B (https://arxiv.org/html/2608.00004#A2) 可视化了这种差异。

#### 所有结论都是相对的。

在绝对意义上，这里的任何评判模型都不是高度可靠的：单评判模型的精确率和 F1 位于 0.6–0.8 区间，而且由于只有约 30% 的实例是 pass，高 pass 一致率看起来并没有那么亮眼（一个全判失败的基线已经能得 0.715）。要将精确率推到 0.80 中段，需要第 6.1 节 (https://arxiv.org/html/2608.00004#S6.SS1) 的全体一致共识规则。

推理投入被证明是一个模型特定的杠杆：将 Gemini 提升到 high reasoning 不会改变其一致率，而对 GPT-OSS-120B 则影响很大；我们在附录 A (https://arxiv.org/html/2608.00004#A1) 中报告了这一比较。

## 6 附加结果

以下两项研究扩展了主要比较。两者都不改变核心结论，并且都只在廉价层上运行（前沿基线仅用于验证集，以控制预算）；我们将其作为支持性证据呈现。

### 6.1 完整基准（n=1000）

我们对三个廉价评判模型在*完整 1000 实例基准*（先验 + 验证 + 其余 600 个）上进行了评分，以获得更稳定的估计，并探索预先指定的多数投票之外的共识配置。

表 2：完整基准（n=1000），95% 自助法置信区间（2000 次重采样）。“两两组合”和 “all-three” 使用全体一致通过规则（候选证明只有在所有成员都判为 pass 时才通过）：