← 返回 2026-08-19

问题即问题:迈向可扩展的数学发现 The Problem Is the Problem: Towards Scalable Mathematical Discovery

Zeyu Zheng, Shengtong Zhang, Jeremy Avigad, Prasad Tetali, Sean Welleck 📅 2026-08-17 👍 4 2026-08-24 18:30
AI for Math 人机协作 开放猜想挖掘 搜索与推荐系统 算力分配 组合数学

把人的输入从『选一个问题』升级为『定一个方向』: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除子差问题),并区分『已知』『新联系』『无先例』三档新颖性,这种自我审计在同类工作中少见。

From papers to recommendations for expert review. The upper row shows a search or recommender pipeline that recalls and filters candidates from a large corpus. Its numbers indicate typical orders of magnitude. The lower row shows the analogous FAR pipeline. Numbers in the lower row are counts from our pilot run detailed in Section 4.
Figure 3: From papers to recommendations for expert review. The upper row shows a search or recommender pipeline that recalls and filters candidates from a large corpus. Its numbers indicate typical orders of magnitude. The lower row shows the analogous FAR pipeline. Numbers in the lower row are counts from our pilot run detailed in Section 4.

实验结果

组合数学试跑主漏斗: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,级联所有检索均漏检。

A recovered candidate, from source text to the pool.
Table 1: A recovered candidate, from source text to the pool.
Expected number of artifacts, the objective f1.
Table 2: Expected number of artifacts, the objective f1.
Expected total importance of the artifacts returned, the objective f2.
Table 3: Expected total importance of the artifacts returned, the objective f2.
Expected maximum importance among the artifacts returned, the objective f3.
Table 4: Expected maximum importance among the artifacts returned, the objective f3.
Each score against the quantity it judges. Panel (a) plots δ(d^{-1}[a, b)) on an axis starting at 50%, panel (b) plots ι(i^{-1}[a, b)). n counts attempts in (a) and accepted resolutions in (b).
Figure 4: Each score against the quantity it judges. Panel (a) plots δ(d^{-1}[a, b)) on an axis starting at 50%, panel (b) plots ι(i^{-1}[a, b)). n counts attempts in (a) and accepted resolutions in (b).
Allocation strategies against the budget. Each fit is made on four fifths of P and applied to the remaining fifth, from which B/5 conjectures are drawn. The five selections together make one set of B conjectures, and each point averages what that set returns over 1000 random partitions. Ties are broken at random, and the uniform baseline is computed exactly from its closed form. Here, B only counts the allocated attempts.
Figure 5: Allocation strategies against the budget. Each fit is made on four fifths of P and applied to the remaining fifth, from which B/5 conjectures are drawn. The five selections together make one set of B conjectures, and each point averages what that set returns over 1000 random partitions. Ties are broken at random, and the uniform baseline is computed exactly from its closed form. Here, B only counts the allocated attempts.
Each score against the quantity it judges, with Wilson intervals. Panel (a) gives δ against the difficulty score, panel (b) gives ι against the importance score.
Figure 6: Each score against the quantity it judges, with Wilson intervals. Panel (a) gives δ against the difficulty score, panel (b) gives ι against the importance score.
查看结构化数据
任务指标本文基线提升
文献级开放猜想池构建(组合数学) 候选→仍开放且良定的猜想 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条工件的真伪——这恰是论文自身论点的最好注脚:专家评审是整条链路中最难扩展的资源。