问题即问题:迈向可扩展的数学发现 The Problem Is the Problem: Towards Scalable Mathematical Discovery
把人的输入从『选一个问题』升级为『定一个方向』:FAR级联自动挖猜想、批量求解并推荐评审
前置知识
多臂老虎机与UCB初始化
把每个候选猜想 $c$ 看作一只『臂』,花费一次模型推理去尝试它就是『拉臂』一次,收益是评估结果 $Y(c)$(无结果、已知解、或候选证明/反例)。UCB类算法的第一步是对每只臂各拉一次以获得初始估计。本文流水线对池中每个猜想恰好尝试一次,正对应UCB的初始化阶段;如何在后续轮次用真正的bandit策略做自适应分配,作者明确留给未来工作。
论文第2.3节与第4.3节全部建立在『尝试=拉臂』这一形式化之上,理解它才能看懂努力分配的优化问题 $\max_{S\subseteq P}\ \mathbb{E}[f(A\cap S)]$ 及其各种求解策略。
搜索与推荐系统的级联架构
工业级搜索/推荐系统用多级漏斗处理海量候选:召回($10^6$量级)→粗排→精排→重排→过滤→最终Top-K($10^0$到$10^1$量级),越靠后的阶段单条候选分到的算力越多。级联的关键权衡是:早期阶段必须便宜且高召回,允许误报,因为后面有更贵的精确阶段兜底。
FAR的五个阶段(Label/Extract/Check/Solve/Judge)就是把这套级联搬到数学文献上:论文语料对应物品库,数学家对应被服务的用户,Figure 3明确画出了这种一一对应。
单调次模函数最大化
集合函数 $F$ 次模指边际递减:$F(S\cup T)+F(S\cap T)\le F(S)+F(T)$;单调指超集取值不减。基数约束下最大化单调次模函数是NP难的(包含最大覆盖特例),但简单贪心可保证达到最优值的 $(1-1/e)\approx 63\%$,且这是多项式算法的最优近似比(Feige, 1998)。
本文第三个目标 $f_3=\max_{c\in A\cap S} i(c)$(最优先工件的重要性)被证明是单调次模的,作者据此引入贪心思路,并在实践中提出『先按重要性截断、再按 $\hat p$ 排序』的替代算法。
AUC与Mann–Whitney检验
AUC(ROC曲线下面积)等于『随机抽一个正样本和一个负样本,分数把正样本排在前面』的概率:0.5等价于随机排序,1.0是完美排序。Mann–Whitney U检验正是检验这一概率是否偏离0.5的非参数方法,两者在数学上等价。
第4.3.1节用它验证模型自评分数是否真有预测力:难度分AUC=0.69($p<10^{-40}$)、重要性分AUC=0.60($p=0.008$),这是后续一切分配策略合法性的实证基础。
GapP完全性与归约
GapP函数是两个#P计数函数之差(可正可负的『间隙』计数)。说问题X是GapP完全的,指所有GapP函数都能归约到X:Turing归约允许多次自适应询问,many-one归约只允许一次映射,后者更强、更难证明。对称群不可约特征值 $\chi_\lambda(\mu)$ 的计算复杂度正是本文所证猜想的主题。
论文代表性新成果之一证明了Ikenmeyer–Pak–Panova猜想:二进制输入的特征计算COMPUTECHARBINARY在many-one归约下是GapP完全的,不懂这个概念就无法评估这条成果的分量。
研究动机
当前主流AI-for-math系统——从FunSearch、AlphaEvolve到AlphaProof Nexus、Aletheia——都建立在『问题级接口』上:数学家预先选好一个定理或猜想,交给系统尝试,输出再被检查。这意味着人类精力集中在流水线两端:开头选题、结尾审稿,而恰恰这两段正成为研究级数学的瓶颈。前沿模型推理是稀缺资源,专家评审更稀缺,把宝贵注意力浪费在已被解决、表述有缺陷或无关紧要的问题上代价高昂。更麻烦的是,数学文献中并不存在结构化的『可尝试问题池』:开放问题可能以编号猜想、问句、备注甚至正文一句话的形式散落在论文里,记号是局部的,状态还会随时间变化;现有专门集合如Open Problem Garden、AIM问题清单、Formal Conjectures覆盖面都很有限。本文的组合数学试跑清楚地量化了这一点:从51,110篇数学论文出发,只有5,245篇属于组合方向,从中抽出6,453条候选陈述,核查后仅剩4,717条『表述良定且仍开放』的猜想——超过四分之一的候选已被解决或本身就是病态表述。
本文的目标是本文的目标是把人类输入的粒度从『单个问题』上移到『研究方向』,让AI系统自动完成中间的选题劳动:给定一个数学家感兴趣且有能力评审的方向(如组合数学),系统应在大规模文献语料中检索相关论文、抽取其中仍未解决的猜想与开放问题、核实它们确实良定且未被解决,形成可尝试池 $P$;然后对池中每个问题投入推理算力尝试证明或反驳;最后只把少数通过多级筛选的『猜想-解答对』推荐给专家评审。同时,作者想把『有限算力花在哪些问题上』本身形式化为约束优化:给定预算 $B$ 次尝试,选集合 $S\subseteq P$ 以最大化产出工件的价值 $f$,并推导出可落地的分配策略。终极检验标准是实际产出数学:证明、反例、对开放问题的回答,且经专家核验无误。
与已有工作不同的是,本文的独特之处在于视角转换:它研究的不是『如何解好一个问题』而是『该解哪些问题』,把选题这个此前处于AI-for-math视野之外的环节变成研究对象。方法论上,作者从搜索与推荐系统借来级联漏斗思想:用越来越贵、越来越准的阶段把海量候选逐级收窄到专家可审的规模。与自动猜想生成这条互补路线(Ramanujan Machine、TxGraffiti、LeanConjecturer、Moonshine)本质不同:那些工作『发明』新猜想,而FAR『挖掘』文献中已存在的、原作者已认真陈述过的开放问题——每条候选都保留源论文、原文陈述、局部上下文和状态证据,后续尝试与评审都能回溯到源文本,这提供了天然的真实性与重要性先验。此外,作者把每次尝试视为对不确定性下决策的一次『拉臂』(bandit初始化),使分数采集、预算分配、策略评估都进入统一的优化框架。
核心方法
FAR(Find, Attempt, Recommend)是一个『文献到评审』的五阶段级联,直觉上就是把推荐系统的漏斗搬到数学发现上:物品库换成论文库,用户换成数学家。Find阶段把文献语料变成可尝试池 $P$:先用最便宜的模型给每篇论文打方向标签(对应召回),再抽取未解决陈述(对应粗排,宁滥勿缺),然后逐条检索后续文献核实其『良定且仍开放』(对应资格过滤)。Attempt阶段对 $P$ 中每个猜想恰好投入一次尝试,用流水线中最强的模型,先搜索文献再动手,输出KNOWN/NEW/FIX/NONE四种结局之一。Recommend阶段扮演审稿人:多个独立评审agent逐条检查NEW结局的正确性(全过才算PASS),再由另一agent做新颖性分级,只留『足以独立发表』的条目构成工件集 $A$。整条流水线在组合数学试跑中从51,110篇论文收窄到77个可发表工件,每一级单条算力递增、模型能力递增,与推荐系统级联的『每层更贵更准』原则完全同构。
核心创新有三层。第一是接口层面:把人机接口从『一个问题』改为『一个方向』,人的作用被重新定位为框定系统主动性的边界(兴趣与专长所在),并保留最终验证与署名责任(呼应Leiden Declaration),选题劳动交给系统。第二是数据层面:『可尝试池』的构建本身被当作一等公民问题,用『不完美信号的宽松抽取+严格状态核查』的组合,把散落在文献中的开放问题恢复成带完整出处元数据的结构化候选,这与依赖人工策展的benchmark和『凭空生成』的自动猜想系统都不同。第三是决策层面:把尝试预算分配形式化为约束优化 $\max_{S\subseteq P}\mathbb{E}[f(A\cap S)]$($|S|=B$),并证明:若能从便宜的前置分数估计每条猜想进入 $A$ 的概率 $p(c)=(1-\mathbb{E}\delta(c))\cdot\mathbb{E}\iota(c)$,则对总产出目标 $f_1$ 和总重要性目标 $f_2$ 按期望排序取前 $B$ 即近优;对最大重要性目标 $f_3$(单调次模)贪心有 $(1-1/e)$ 保证。关键洞察是这些分数在任何推理预算花费之前就已采集,是真正的先验信号。
方法步骤详情
五步流水线,输入输出明确。(1) Label:输入51,110篇论文(OpenAlex元数据),agent逐篇判断是否属于指定方向,输出5,245篇组合论文;用gpt-oss-120b,最便宜的模型。(2) Extract:抽取存活论文中的未解决陈述(编号猜想、问句、散文皆可),排除同文已解决和无具体数学内容者,其余刻意宽松——漏抽不可恢复而误抽会被下阶段过滤;输出6,453条候选(2,742篇);用gemini-3.5-flash。(3) Check:逐条检索后续文献,标注open/solved/invalid并记录状态证据,同时给出难度分 $d$(0=练习题,1=顶刊级)与重要性分 $i$(0=无实质,1=Fields奖级),近正态、中心0.5;输出4,717条开放猜想(2,206篇)构成 $P$;用gemini-3.1-pro带搜索。(4) Solve:每条猜想连同源论文交给opencode agent(gpt-5.5,xhigh档),先搜后解,输出KNOWN(443)、NEW(1,050)、FIX(319)、NONE(2,905)。(5) Judge+Grade:三个独立gpt-5.5评审查证NEW,全票PASS者598条;再分级为已解决(75)、过小(446)、可发表(77),构成 $A$;作者人工评审15条,全部正确。
技术新颖性
技术新颖性体现在四方面。其一,『方向级接口』与文献级问题池是新的基础设施性贡献:此前没有系统从数万篇论文中自动恢复开放猜想并保留状态证据,本文的漏斗(51,110→5,245→6,453→4,717→1,050→598→77)本身就是可复用的方法论模板。其二,把『选题』形式化为不确定性下的约束优化,并给出从便宜先验出发的近优策略:$f_1$、$f_2$ 用线性期望直接排序求解;$f_3$ 通过证明 $S\mapsto\mathbb{E}[f_3(A\cap S)]$ 单调次模而接入贪心近似理论(Nemhauser的 $(1-1/e)$ 保证与Feige的不可超越性)。其三,实证方法论严谨:分数在任何尝试发生前采集;评估采用5折交叉验证(1000次随机划分,被排序的猜想绝不参与拟合自身结局);分层AUC(0.56,$p<10^{-5}$)专门验证了难度与重要性携带不同信息,而非同一信号的重复。其四,诚实的失败分析:文中明确报告了把已解决问题误判为新的案例(Erdős除子差问题),并区分『已知』『新联系』『无先例』三档新颖性,这种自我审计在同类工作中少见。
实验结果
组合数学试跑主漏斗:51,110篇论文→5,245篇方向内→6,453条候选→4,717条开放猜想;全池单次尝试后NONE 2,905、KNOWN 443、FIX 319、NEW 1,050(约22.3%);三评审全票通过598条(56.9%),最终77条可发表(全池1.6%);作者人工评审15条全部正确。代表性成果:(a) 反例推翻Davies–Jenssen–Perkins–Roberts关于三角无关图 $\alpha(G)/\bar\alpha(G)\ge 2^{-o(1)}$ 的猜想——构造 $C_5\square K_{m,m}$ 使比值趋于 $24/13$,换 $C_{13}(1,5)$ 可降至 $32/19$;(b) 对所有奇素数幂 $q$ 反驳Lund–Saraf–Wolf的线并集猜想(三维Nikodym界关键),用抛物面 $z=x^2-\nu y^2$ 的半切线族达到密度 $1/2+o(1)$,$q\le 13$ 穷举验证;(c) 证明Ikenmeyer–Pak–Panova猜想:二进制对称群特征计算在many-one归约下GapP完全;(d) 回答Erdős–Straus问题:对每个固定 $n\ge 2$,密度 $d^*(n)=1$。评分有效性:难度分AUC 0.69($p<10^{-40}$)、重要性分AUC 0.60($p=0.008$),二者Spearman相关0.83但分层AUC 0.56证明信息不同。预算分配:$B=300$ 时按 $\hat p$ 排序期望产出7.92 vs 均匀随机5.17(+53%);$f_3$ 目标下重要性top-1/10截断+排序达0.850 vs 0.629(+35%)。教训:一条『新证明』(Erdős除子差问题)4个月前已被Price用ChatGPT-5.2解出并记录在erdosproblems.com,级联所有检索均漏检。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 文献级开放猜想池构建(组合数学) | 候选→仍开放且良定的猜想 | 6,453条候选保留4,717条(来自2,206篇论文),每条带源论文与状态证据 | 无文献级先例;人工策展库(Open Problem Garden、AIM清单、Formal Conjectures)覆盖选择性高 | 首次从5.1万篇论文自动构建带状态证据的可尝试池 |
| 开放猜想自动尝试(全池单次尝试) | 声称解决率(NEW/池)与最终可发表率 | NEW 1,050/4,717≈22.3%;评审通过598(12.7%);可发表77(1.6%) | 同类系统(Aletheia、QED等)仅在人工挑选的少数问题上运行,无可比全池数据 | 首次给出研究级开放猜想的全池尝试漏斗统计 |
| 难度分数校准(尝试前采集) | AUC(对『无接受解决』),Mann–Whitney检验 | 0.69($p<10^{-40}$);分最高桶(0.8–1.0)无果率96.0% vs 最低桶52.4%;分层AUC 0.56($p<10^{-5}$) | 0.5(随机排序) | +0.19,且控制重要性后仍显著,证明难度分携带独立信息 |
| 重要性分数校准(尝试前采集) | AUC(对『被评可发表』) | 0.60($p=0.008$);最高桶可发表率22.6% vs 最低桶1.0% | 0.5(随机排序) | +0.10,弱于难度分但统计显著 |
| 预算分配(目标 $f_1$:最大化工件总数,$B=300$) | 期望工件数(5折交叉验证×1000次划分) | 7.92(按 $\hat p=(1-\hat\delta)\hat\iota$ 排序) | 5.17(均匀随机) | +53%;$B=10$ 时为0.40 vs 0.17 |
| 预算分配(目标 $f_3$:最大化最优先工件,$B=300$) | 期望最大重要性 | 0.850(重要性top-1/10内按 $\hat p$ 排序) | 0.629(均匀随机) | +35%;注意全池 $\hat p$ 排序仅0.500,在大预算下反而劣于基线 |
局限与改进
作者承认的局限:77个可发表工件中只人工评审了15个(约19%),其余成果正确性未经验证;难度与重要性分数由检查阶段的agent主观给出且二者高度相关(Spearman 0.83);状态核查不完美——一条成果实际已被解决而各级检索全部漏检;分配策略的结论依赖本次运行的评分模型、语料来源与级联模型,外推需谨慎。我自己的观察:第一,全程无形式化验证,正确性最终靠LLM评审加专家抽查,对推理链更长的代数/几何结果风险更大;第二,『可发表/过小/已知』的分级本身也是模型判断,446条『过小』中可能埋没真金;第三,语料来自OpenAlex元数据,对arXiv最新论文的覆盖与时延不确定,那条漏检的Erdős问题解法正是记录在专门问答站而非arXiv上;第四,算力成本未披露,4,717次gpt-5.5 xhigh尝试加三轮独立评审的开销不小;第五,级联后半段依赖闭源前沿模型,版本更替会改变整条漏斗的数字;第六,试点仅在组合数学且方向由作者本人专长框定,换到需要大规模计算验证或形式化的领域是否成立未知。
独立分析的弱点
独立分析的弱点与改进方向:(1) 状态核查的盲区——Erdős除子差问题的解被漏掉,因为其记录在erdosproblems.com而非arXiv;改进方向是把Erdős问题站、MathOverflow、Formal Conjectures等垂直知识库纳入核查检索源,并做多源交叉投票。(2) 无形式验证墙——1,050条NEW全部只有自然语言评审;改进方向是与Lean及Formal Conjectures对齐,至少对可形式化的条目自动形式化,把443条KNOWN的反查也纳入形式核对,把『评审通过』升级为『机器可证』。(3) 分数太粗——单个标量 $d$ 和 $i$、正态锚定,与结局仅中度相关(AUC 0.69/0.60);改进方向是用本次运行4,717条带结局的数据训练专门的难度/重要性/可解性预测器,并引入子领域、问题长度、证明技术标签等特征。(4) 单次尝试浪费bandit结构——每臂只拉一次等于均匀分配;改进方向是两轮分配:先小预算探测子池,拟合 $\hat\delta,\hat\iota$ 后把剩余预算集中到高 $\hat p$ 区域,论文给出了理论框架但只做了回溯性评估。(5) 评审瓶颈依旧——77条只消化15条,流水线末端会重新堵塞;改进方向是建立领域专家评审网络或分级评审(先轻量核查再深审),并把人工确认的工件回灌为评审器的校准数据。
未来方向
作者明确提出的方向:把第2.3节的bandit解释做实——研究多轮自适应分配下的UCB/Thompson采样策略,而非只做UCB初始化式的一次拉臂;将FAR推广到组合以外的数学领域;随着模型能力提升,『可达区域』(Figure 2)会扩张,今天无果的猜想值得周期性重试,最优分配策略随之动态改变。基于其成果可延伸的方向:其一,形式化闭环——把77条工件中可形式化的条目转成Lean证明,形成『自然语言发现→机器验证』管道,同时反哺定理证明训练数据;其二,公开数据集——本次运行的4,717条(猜想、先验分数、尝试结局)是训练猜想难度/重要性预测器的稀缺监督数据;其三,主动学习式批量分配——每轮试探子池→拟合 $\hat p$→按策略分配剩余预算,把回溯性分析变成在线策略;其四,把带状态证据的开放猜想池做成社区基础设施,类似SWE-bench之于软件工程,让后续系统可在同一池上公平比较;其五,AI发现的学术责任机制——77条工件如何进入学术记录、如何署名与验证(Leiden Declaration框架下),这本身就是亟待研究的新问题。
复现评估
复现评估:代码开源于GitHub(zeyu-zheng/FAR),77个工件的完整数学写作收录于论文附录C并在probxiv.com提供;语料51,110篇来自开放的OpenAlex元数据,可重建;五个阶段的提示词全部在附录A给出。主要障碍在模型侧:级联后半段依赖闭源前沿模型——尝试/评审/分级用gpt-5.5(xhigh推理档),抽取用gemini-3.5-flash,核查用gemini-3.1-pro带网络搜索,只有标注阶段的gpt-oss-120b开源;作者未披露成本,但估算4,717次高强度推理尝试加3×1,050次独立评审再加全程搜索调用,花费应在数千至数万美元量级(Anysphere为合作者提供了算力)。复现难度评为中等偏高:流水线逻辑清晰、提示齐备,但三大不确定性会改变结果——模型版本更替、网络搜索返回内容的时效性、agent运行的随机性;漏斗各阶段数字应视为一次随机实现的样本而非确定值。数学层面的最终验证绕不开专家:不熟悉组合数学的团队即使完整复现流水线,也难以判断77条工件的真伪——这恰是论文自身论点的最好注脚:专家评审是整条链路中最难扩展的资源。
论文图表
上半部分是传统范式:数学家预先选定一个猜想→AI尝试→得到解决。下半部分是本文范式:数学家只选定一个研究方向→FAR从文献中抽取猜想池→大规模尝试→评判分级→推荐→专家评审,人从『出题人』变为『定方向者+终审者』。
一张图看懂论文的核心范式转变:人的输入从『问题』变为『方向』,选题劳动被移交给系统,这是全文所有设计的出发点。
示意图:横轴为数学重要性,纵轴定性地画出开放猜想、人工已解决猜想与『AI能力阈值』曲线所界定的当前可达区域;随着模型能力提升,更多猜想进入可达区。作者强调两轴只能定性解读。
解释了为什么努力分配是动态问题:今天尝试无果的猜想明天可能可解,这为『模型迭代后重试池中问题』和bandit式多轮分配埋下伏笔。