评判我们无法解决的问题:基于后果的无预言机研究级数学评估方法 Judging What We Cannot Solve: A Consequence-Based Approach for Oracle-Free Evaluation of Research-Level Math
通过测量候选解在邻域问题上的转移能力来评估其正确性,无需真实答案
前置知识
Oracle-Free Validation(无预言机验证)
在数学和科学发现中,验证一个假设通常需要一个「预言机」(oracle),即可以判定真假的权威标准——比如参考答案或人类专家。无预言机验证是指在没有这类权威标准可用的情况下,通过间接手段判断候选解质量的方法。常见策略包括多数投票(majority voting)、奖励模型(reward model)和 LLM 裁判(LLM-as-a-judge)。这些方法的核心困难在于:对于研究级问题,正确性往往不能简化为离散标签(如数值答案),而是取决于整个推导过程的逻辑有效性,这对自动化验证提出了极高的要求。
本文的核心贡献就是提出了一种新的无预言机验证方法。理解现有方法的局限性(依赖人类专家成本高、LLM裁判不可靠且有偏见)是理解本文研究动机的前提。
In-Context Learning(上下文学习)
上下文学习是指大语言模型通过在提示中提供少量示例(即 few-shot examples),无需额外训练即可适应新任务的能力。例如,给定一个问题和一个候选解作为上下文,LLM 能够利用该解中的方法论信息来解决相关问题。这一能力是本文方法的理论基础:如果一个候选解是正确的,那么它包含的方法级信息应该能够「转移」到相关的邻域问题上,帮助模型更好地解决这些可验证的问题。
Consequence-Based Utility 的核心假设正是:正确的候选解可以作为高质量的上下文示例,提升模型在邻域问题上的表现。理解上下文学习的工作机制是理解本文方法「为什么有效」的关键。
Reward Model 与 Generative Reward Model(奖励模型与生成式奖励模型)
奖励模型(RM)是一个标量评分函数,用于近似评估解的「质量」。常见的训练方式是通过 Bradley-Terry 偏好模型,使用成对比较数据进行最大似然训练。生成式奖励模型(GenRM)则更进一步,不直接输出标量分数,而是生成一段评估文本,再通过解析器提取分数。这种「生成式评估」方式利用了 LLM 的推理能力,是当前奖励模型领域的重要趋势。
本文将 CBU 与传统 RM 和 GenRM 进行了系统对比。理解这些基线方法的工作原理和局限性(如泛化RM在研究级问题上表现不佳),有助于理解 CBU 的优势所在。
Solve-to-Judge Gap(求解-评判能力差距)
Solve-to-Judge Gap 是指一个模型「评判解的质量」的能力和「自己解决问题」的能力之间的差距。在研究级数学问题上,即使模型无法自己求解(例如 GPT-5 在 EXPERTMATH 上仅达到 35.71% 的平均准确率),它可能仍然能够区分正确和错误的解。然而,随着问题难度增加,LLM 裁判的区分能力会急剧下降,而本文提出的 CBU 方法能够保持更强的鲁棒性。这一现象说明,对于真正困难的问题,直接检查推理过程(LLM-Judge 的做法)变得不可靠,而通过「后果」来间接评估(CBU 的做法)更加稳健。
Figure 3 的核心发现就是:在高难度区间,CBU 的正确-错误分离度远高于 LLM-Judge。理解 Solve-to-Judge Gap 概念是理解这一发现的理论基础。
Neighborhood Questions(邻域问题)
邻域问题是指围绕原始研究级问题构造的一组相关但可验证的问题变体。这些变体保留原始问题的核心数学思想,但通过修改参数或条件使得答案可以通过标准方法获得。例如,对于一个关于 D8 型 Coxeter 群渐近 Hecke 代数的问题,邻域问题可能是将类型修改为 D6 或 D7 的变体。邻域问题的构造原则是:一旦理解了原始问题的解法,这些变体应该变得「直接可行」,且难度略低于原始问题。每个原始问题通常配对 2 个邻域变体。
邻域问题是 CBU 方法的核心组件。CBU 通过测量候选解在邻域问题上的转移性能来估计其正确性。邻域问题的质量和难度直接影响 CBU 的有效性——太简单会导致所有候选解都成功、无法区分;太难则所有解都失败。
研究动机
在研究级数学领域,LLM 已经展现出有意义的问题解决能力——例如帮助证明 Nesterov 加速梯度方法的点收敛性、构造非交互式相关蒸馏中「多数最优性」猜想的有限反例、以及确定 Wasserstein 界定污染下鲁棒密度估计的精确极小极大最优误差率。然而,这些进展也暴露了一个关键瓶颈:验证环节严重依赖人类专家。论文引用了三个具体案例:Jang & Ryu (2025) 报告 ChatGPT 生成的论证中「大约 80% 是错误的」;Dobriban (2025) 指出 GPT-5「有时跳过需要数天工作才能填补的细节」;Schmitt (2025) 观察到「一些模型声称存在虚假反例」。因此,进展仍然依赖于教授级别的甄别——专家必须拒绝幻觉证明尝试、修复缺失步骤、将想法转化为可检查的论证。现有的自动化验证方法面临两个根本问题:人类专家成本高昂且无法规模化;LLM 裁判虽然成本较低但往往不可靠且存在系统性偏见,如对冗长、格式规范的文本给予过高评价(verbosity bias),以及被权威性表述(如引用知名定理)所误导。在 EXPERTMATH 数据集上,LLM 裁判(如 GPT-OSS-120B)对错误解给出高于平均分的概率高达 53%(Qwen3-235B-A22B),严重降低了验证的可靠性。
本文的目标是本文的具体目标是提出一种无需真实答案即可评估研究级数学候选解正确性的方法。该方法需要满足以下要求:(1)不依赖人类专家标注,实现自动化评估;(2)在 LLM 自身无法解决的问题上仍能有效区分正确和错误的解;(3)对表面特征(如文本长度、格式、权威性表述)不敏感,专注于方法级信息的有效性;(4)在标准评估指标上超越现有的所有无预言机基线方法,包括奖励模型、生成式奖励模型和 LLM 裁判。论文希望该方法能够在「高风险设置」中发挥作用,即需要对固定、困难问题进行高置信度验证的场景。此外,论文还发布了 EXPERTMATH 基准数据集,包含 192 个专家撰写的数学问题(其中一半仍未被前沿模型解决)和 425 个 LLM 生成的问题。
与已有工作不同的是,本文的独特切入角度在于借鉴了数学研究中「后果支持」(support by consequences)的经典验证思想。在数学中,当一个假设难以直接验证时,数学家会评估它所蕴含的结果的广度和一致性。最经典的例子是黎曼假设:尽管至今未被证明,但它在解析数论和算法数论中支撑了大量精确的条件结果(如 Von Koch 1901 年的素数分布结果、Miller 1975 年的素性测试)。类比地,本文将每个候选解视为关于目标问题的一个「临时假设」,通过评估它在邻域问题上的转移效果来判断其质量。这一视角的独特之处在于:与 LLM 裁判直接检查单一推理轨迹的做法不同,CBU 通过测量候选解的「下游后果」来评估其正确性——就像软件工程中的单元测试,不看代码本身是否好看,而是看它的输出是否正确。这种评估模式在问题变得越难时越有价值,因为直接检查推理过程变得越不可靠,而通过后果验证的信号依然稳健。
核心方法
Consequence-Based Utility(CBU)的核心直觉可以用一个日常类比来理解:假设你拿到了一份可能是正确答案的数学作业,但没有参考答案来核对。一个巧妙的办法是:把这份作业当作「解题模板」,让同一个学生去解几道类似但更简单的题目——如果学生用这份作业中的方法能解对这些题目,那原作业大概率是正确的;如果解不对,那原作业大概率有问题。技术上,给定一个研究级问题 Q 和 N 个候选解,CBU 首先为每个候选解构造一组邻域问题。然后,对于每个候选解,将原始问题和候选解作为上下文提供给求解器模型,要求它解决每个邻域问题。最后,通过验证器检查求解器是否正确解决了邻域问题,并计算平均准确率作为该候选解的效用分数。直觉上,如果候选解在邻域问题上诱导了更高的准确率,说明它提供了更有帮助的信息,因此更可能是正确的。
CBU 与已有方法的最本质区别在于评估的「模式」不同。LLM 裁判类似于代码审查(code review):它检查单一推理轨迹的合理性和一致性,这在错误解看起来表面连贯、错误微妙时变得不可靠。CBU 则类似于单元测试(unit test):它通过候选解的下游后果来打分——不管解本身是否看起来漂亮,只看它是否能帮助解决相关问题。这一区别的关键在于:当直接检查推理过程变得越困难(问题越难),通过后果验证的信号依然保持稳健。论文通过 Figure 3 的实验数据有力地证明了这一点:在最难的问题区间,LLM 裁判的正确-错误分离度急剧下降,而 CBU 保持强劲。另一个关键区别是对「人类风格」解的识别能力。人类专家撰写的解通常简洁、直觉驱动,而 LLM 裁判倾向于过度重视表面特征(如冗长度、规范格式),CBU 对这些呈现特征不那么敏感,因此能更好地识别人类撰写的正确解。在 GPT-OSS-120B 上,CBU 将 HumanWin(人类解评分高于平均错误解的概率)从 48.57 提升到 82.86,提升幅度达 +34.29 个百分点。
方法步骤详情
CBU 方法的完整流程包括五个步骤。第一步是候选解生成:给定研究级问题,使用生成器 LLM 采样 N 个候选解,在本文实验中每个问题有 1 个专家撰写的正确解和 9 个 LLM 生成的解(其中 4 个正确、5 个错误)。第二步是邻域问题构造:为每个原始问题构造一组邻域问题,这些变体保留核心数学思想但修改参数或条件,使得一旦理解原始解法就变得可解,且难度略低于原始问题,本文中每个问题配对 2 个邻域变体。第三步是上下文条件求解:对于每个候选解和每个邻域问题,将原始问题和候选解作为上下文提供给求解器,采样 T 个独立的求解尝试,模型最多推理 16k 个 token。第四步是验证:使用验证器检查每个求解尝试是否正确解决了邻域问题。第五步是效用计算:对每个候选解,计算其在所有邻域问题上的平均准确率作为效用分数。
技术新颖性
CBU 的技术新颖性体现在三个方面。首先,它是首个将上下文学习能力(in-context learnability)作为无预言机验证信号的方法。尽管此前有工作利用上下文表现来评估示例价值(如 Chang & Jia 2023 的数据整理工作),但主要用于数据策展、检索和训练,而非作为候选解的验证机制。CBU 创造性地将「一个解能否帮助模型解决相关问题」转化为正确性的代理信号。其次,CBU 与数学中「后果支持」的传统验证思想建立了直接联系——黎曼假设虽未被证明但支撑大量精确条件结果——但将这一思想从人工验证转化为自动化评估流程。第三,CBU 在方法论上实现了从「检查过程」到「检查后果」的范式转变。传统 LLM 裁判类似于「代码审查」,检查单一推理轨迹;CBU 类似于「单元测试」,通过下游表现打分。这种范式转变使得 CBU 在高难度区间保持稳健性,而直接检查方法随着错误变得微妙而失效。论文的错误分析进一步揭示了 CBU 优势的来源:在 112 个 LLM 裁判高估但 CBU 正确降序的错误解中,71.4% 存在「不正当压缩」(跳过关键中间步骤),68.8% 存在「错误推理」,31.3% 存在「外部引用」(仅引用定理名而不推导),这些都缺乏可转移的方法级信息。
实验结果
论文在 EXPERTMATH 数据集上进行了系统性实验,核心发现可以从五个维度来分析。第一,CBU 在所有评估指标上一致超越所有基线方法。以 GPT-OSS-120B 为例,CBU 将 Acc@1(排名第一的解是否正确)从 LLM 裁判的 67.21 提升到 76.27,提升 +9.06 个百分点;AUC(正确与错误解的配对可分离度)从 71.42 提升到 79.63,提升 +8.21 个百分点;HumanWin(人类解评分高于平均错误解的概率)从 48.57 提升到 82.86,提升 +34.29 个百分点。第二,在不同模型骨干上,CBU 均展现出一致的改进。GPT-OSS-20B 的 AUC 从 69.03 提升到 79.18(+10.15),Qwen3-30B-A3B 从 65.81 提升到 76.24(+10.43),Qwen3-235B-A22B 从 69.48 提升到 71.38(+1.90)。第三,CBU 在「求解-评判能力差距」上表现更优。Figure 3 显示,随着问题难度增加,LLM 裁判的正确-错误分离度急剧下降,而 CBU 保持稳健,使其特别适合研究级问题的高难度尾部。第四,CBU 与 LLM 裁判捕获互补信息。Table 3 显示,训练在 CBU 分数上的逻辑回归分类器准确率为 73.09-76.31,高于训练在 LLM 裁判分数上的 58.06-66.67;将两者结合后准确率进一步提升至 73.90-79.65。第五,CBU 对 LLM 裁判的典型失败模式具有鲁棒性。Figure 5 显示,LLM 裁判对错误解给出高于平均分的概率为 0.51-0.53(Qwen3 模型),而 CBU 仅为 0.08-0.14,表明 CBU 能更可靠地惩罚错误解。奖励模型基线表现最差(如 AceMath-72B-RM 的 AUC 仅 20.75),但考虑到其计算预算仅为其他方法的 1/64,这一结果符合预期。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 研究级数学解排名(GPT-OSS-120B) | Acc@1 | 76.27 | 67.21(LLM-Judge) | +9.06 pp |
| 研究级数学解排名(GPT-OSS-120B) | AUC | 79.63 | 71.42(LLM-Judge) | +8.21 pp |
| 研究级数学解排名(GPT-OSS-120B) | HumanWin | 82.86 | 48.57(LLM-Judge) | +34.29 pp |
| 研究级数学解排名(GPT-OSS-20B) | AUC | 79.18 | 69.03(LLM-Judge) | +10.15 pp |
| 研究级数学解排名(Qwen3-30B-A3B) | AUC | 76.24 | 65.81(LLM-Judge) | +10.43 pp |
| 研究级数学解排名(Qwen3-235B-A22B) | AUC | 71.38 | 67.85(GenRM) | +3.53 pp |
| 正确性预测(GPT-OSS-120B 特征) | 逻辑回归准确率 | 73.49 | 64.66(LLM-Judge 特征) | +8.83 pp |
| 竞赛级数学解排名(Daft-Math) | Acc@1 | 85.58 | 93.51(LLM-Judge) | -7.93 pp(CBU 较弱) |
局限与改进
论文和实验揭示了几个值得注意的局限性。首先是适用范围的限制:CBU 最适合高风险、需要高置信度验证的固定困难问题场景。对于竞赛级简单问题(如 Daft-Math),CBU 的表现反而不如 LLM 裁判(Acc@1 85.58 vs 93.51),因为求解器无论提供什么上下文示例都能成功,导致效用信号失去区分度。其次,CBU 的有效性依赖于邻域问题难度的「甜蜜点」——如果邻域问题太简单,求解器不需要帮助就能成功;如果太难,求解器无论如何都会失败。这使得邻域问题的构造部分依赖于求解器模型的能力,增加了工程复杂性。第三,邻域问题的构造成本:虽然论文展示了 LLM 自动生成的邻域问题在挑战性问题上可以替代专家撰写的邻域问题(Section 7.2),但可靠性取决于生成器产生合理变体的能力,缺乏人类监督时可能出现质量不稳定。第四,论文承认 CBU 的推理成本与 LLM 裁判相当(Table 5 显示 token 使用量在 ±15% 以内),但需要多次采样(论文使用 64 次 rollout),单次评估虽然更快但收敛需要至少 8 次 rollout(Figure 6 显示 n ≥ 8 将归一化误差控制在 0.05 以下)。
独立分析的弱点
从独立分析的角度看,CBU 存在几个值得关注的弱点。第一个弱点是邻域问题构造的「鸡生蛋」问题:要评估候选解的质量,需要构造邻域问题;但邻域问题的质量本身需要专家验证。论文虽然展示了 LLM 自动生成邻域的可行性(通过 RealMath 数据集),但依赖三个模型(Gemini-3-Pro、GPT-5-Pro、Grok-4)达成一致来获得「临时答案」,这种方式在真正未解决的问题上可能不可靠。改进方向:可以探索基于「共识投票」的自动邻域质量评估,或者开发专门的邻域难度校准方法。第二个弱点是对求解器能力的强依赖:如果求解器太强(不需要帮助就能解决所有邻域问题),或者太弱(即使有正确帮助也无法解决),CBU 的区分度都会下降。论文发现 Daft-Math 上 CBU 不如 LLM 裁判,正是因为竞赛级问题对求解器太简单。改进方向:可以根据求解器的能力动态调整邻域问题的难度,或者引入多个不同能力的求解器进行交叉验证。第三个弱点是缺乏对「部分正确」解的处理:CBU 将所有解二分为正确/错误,但研究级数学中许多解可能部分正确(如正确的方法但遗漏了关键步骤)。改进方向:可以将效用函数从二值验证扩展为连续评分,或引入渐进式验证策略。
未来方向
论文提出了三个主要的未来研究方向。第一,改进全自动邻域问题生成的可靠性。当前的方法依赖 LLM 生成变体并通过多模型一致获取临时答案,但缺乏人类监督的质量保证。未来可以探索基于形式化数学系统(如 Lean 4)的邻域问题生成和验证,或者开发专门的邻域难度预测模型。第二,将 CBU 扩展到数学以外的其他 STEM 领域。CBU 的核心思想——通过候选解在相关问题上的转移效果来评估其质量——理论上可以应用于任何具有可验证邻域问题的推理任务,如物理、化学、计算机科学中的开放问题。关键挑战是如何为这些领域构造高质量的邻域问题。第三,在真正未解决的问题上评估 CBU 的有效性。当前的评估基于已知正确答案的问题,但 CBU 的最终目标是验证 LLM 在真正开放问题上的生成质量。这需要开发新的评估协议,如将 CBU 与其他验证方法(如形式化验证)结合,或者在人类-LLM 协作的真实场景中进行纵向评估。
复现评估
从复现性评估的角度看,论文提供了相对充分的支持。代码方面:论文声称「所有代码和解析的生成结果都包含在补充材料中」(Section C),但具体仓库地址未在论文中给出。数据方面:EXPERTMATH 数据集包含两部分——425 个 LLM 生成的问题计划在 Hugging Face 上发布,但 192 个专家撰写的数学问题因资助方要求在 2026 年 7 月前保持限制。论文承诺在限制期间「应要求对提交的模型提供评估」。算力方面:CBU 需要 64 次 rollout 来获得稳定的效用估计,但论文表明 n ≥ 8 即可将归一化误差控制在 0.05 以下(Figure 6),这为资源受限的复现提供了参考。论文使用的四个模型(GPT-OSS-20B/120B、Qwen3-30B-A3B/235B-A22B)均为公开可用的模型。总体而言,复现的主要障碍是专家撰写的数学问题数据集的访问限制,以及对特定模型 API 的依赖。建议复现者首先从 RealMath 或 Daft-Math 数据集开始验证 CBU 的基本流程。
论文图表
该图展示了四个 LLM 裁判骨干模型在 1-10 分制上的评分分布直方图。GPT-OSS 模型分布较均匀,而 Qwen 模型评分高度集中在 10 分附近,表明存在天花板效应。
这张图解释了为什么 Qwen 模型作为 LLM 裁判时表现相对不佳——评分过度自信导致区分度下降。它也为 Table 2 中 Qwen3-235B-A22B 在 Recall@5 上 LLM 裁判优于 CBU 的例外情况提供了解释。