从选题目到选方向！CMU等提出FAR框架：77项数学新解直面专家评审

The Problem Is the Problem: Towards Scalable Mathematical Discovery

大模型解决一道给定的数学竞赛题或验证一个形式化命题，已经屡见不鲜。从 Putnam 竞赛基准到各类形式化证明系统，AI 的推理能力在快速逼近人类顶尖水平。然而，在真正的数学前沿研究中，这种“人出题、AI 做题、人复核”的单题交付模式正迅速遭遇天花板。

ArXiv URL：https://arxiv.org/abs/2608.16977v1

瓶颈不在于做题的速度，而在于题目从哪里来以及做完之后谁来读。数学家的精力极为有限，前沿模型的深度长思考推理（如 o1、gpt-5.5 类模型）同样算力昂贵。如果把大量昂贵算力倾注在极少数预先挑选的著名难题上，往往会碰得头破血流；而如果任由模型随机搜索，又会产生海量平庸甚至微不足道的琐碎结论，迅速压垮人类数学家的评审精力。

来自 Anysphere（Cursor 团队）与 Carnegie Mellon University（卡耐基梅隆大学，CMU）的研究者们指出：当前 AI 数学研究的瓶颈已不再是“证明”，而是“选题”与“资源分配”。

为了打破这一僵局，研究团队提出了名为 FAR（Find, Attempt, and Recommend）的文献端到评审端级联框架，并在组合数学领域展开了一场真实测试：系统自动扫描 5,245 篇组合数学论文，提取出 4,717 个货真价实且尚未解决的猜想，最终通过模型自主求解与层层过滤，为人类专家筛选出 77 项达到可发表潜力的全新数学成果。

数学研究的本质是资源分配

目前的 AI-for-Math 工作大多遵循“点对点”的单题求解逻辑：数学家输入一个特定的猜想，Agent 尝试寻找构造或证明，再由人工校验。但数学研究的真实发生过程并非如此。陶哲轩曾指出，我们正在经历从“证明匮乏”向“证明丰裕”的转变。当大模型的证明尝试变得相对廉价时，决定研究产出质量的关键，就变成了如何在浩瀚的问题空间中分配注意力。

如果将所有可以用自然语言表达的数学问题集合记为 $\mathcal{U}$，人类的数学研究活动本质上是在 $\mathcal{U}$ 上进行的有限资源分配。但对于 AI 辅助系统而言，在整个 $\mathcal{U}$ 空间漫无目的地自动提出新猜想（Automated Conjecturing）往往收效甚微，因为生成的猜想很可能是平凡的、缺乏学术脉络的伪问题。

与之相对，已经正式发表的数学文献库是一座巨大的金矿。数十年甚至上百年来，数学家们在论文的正文、讨论和展望中留下了大量明确表述过、但因篇幅或当时工具所限未予解决的开放猜想与设问。

这些问题天然具备学术价值与研究上下文。FAR 的核心洞察就在于：不再让数学家指定某一个孤立的题目，而是让数学家指定一个他们具备专业鉴赏力的“研究方向”。系统随之化身为主动的信息检索与推荐流水线，自动从海量文献中打捞出合适的问题池，统一调配推理算力进行攻克，最后仅将高置信度、有学术分量的解推荐给专家。

借鉴推荐系统：FAR 级联架构的设计逻辑

受到工业界搜索与推荐系统（从全量召回、粗排、精排到最终重排）的启发，FAR 构建了一条漏斗式的“文献到评审”级联流水线。随着候选对象逐层锐减，每一阶段分配给单项任务的模型能力与算力成本则呈指数级递增。

整个流程主要由三大核心环节构成：

1. 寻找与沉淀（Find）：构建可攻克问题池 $\mathcal{P}$

给定专家感兴趣的研究方向（在测试中为组合数学），系统首先需要在全量文献中捞出真正值得尝试的开放问题：

方向标注（Labeling）：充当大粗排角色。面对成千上万篇原始论文，调用极轻量且成本极低的模型（实验中采用 gpt-oss-120b）快速通读，判断论文是否属于该研究方向。
猜想提取（Extraction）：由轻量长上下文模型（实验中采用 gemini-3.5-flash）对留存论文进行精细抽取。不管是明确标为 Conjecture、Question 的段落，还是隐式散落在正文讨论中的开放问题，一律连同前后上下文、来源出处一同结构化抽离。
状态与合法性检验（Checking）：抽取出来的问题往往鱼龙混杂，有的可能早被后续论文解决，有的可能并非严格良构的数学命题。该阶段使用具备联网检索能力的中型模型（gemini-3.1-pro），主动检索该问题后续的学术进展。一旦发现已有公认证明，或者问题描述不完整，立即丢弃；仅保留被确证为未决且良构的命题，最终沉淀为可攻克问题池 $\mathcal{P}$。

2. 大规模求解（Attempt）：在不确定性中博弈

进入问题池 $\mathcal{P}$ 的所有猜想，将统一迎来计算资源的注入。在此阶段，系统调用顶尖前沿推理模型（实验中采用处于极高推理强度的 gpt-5.5），并以配备论文上下文与代码沙箱环境的 Agent（如 opencode）形式对猜想展开攻关。

这一阶段产生的结果集 $\mathcal{Y}$ 会明确给出四种状态之一：彻底失败未产出、检索到已知解、提出了反例构造，或给出了新的严格证明。

3. 筛选与推荐（Recommend）：守护专家的注意力

人类专家的评审是整个链条中最昂贵、弹性最小的资源。因此，模型给出的“潜在解”绝不能直接抛给人类，必须经历极其苛刻的自动化同行评审：

合规审判（Judging）：由 3 个独立的专家级判决 Agent 组成陪审团，同时对每一个声称产出新解的候选进行深度交叉核验，检查其是否完整回应了原猜想、步骤是否存在逻辑跳跃或计算漏洞。只有获得 3 位裁判一致 PASS 的结果才能进入下一轮。
价值分级（Grading）：通过正确性检验的解，并不一定都值得写成论文。另一个评审 Agent 会对其进行学术价值定级，区分为“其实已被巧妙文献覆盖”、“结果正确但过于细碎”，以及“具有独立发表价值的实质性进展（Publishable Artifacts）”。只有最后一组会被打上标记，构成最终呈递给人类数学家的成果集 $\mathcal{A}$。

组合数学实战：从 5,245 篇论文到 77 项待审成果

研究团队在组合数学这一极度依赖人类直觉与精巧构造的领域全面跑通了 FAR 流水线。

原始文献输入来自 OpenAlex 等公开学术库的 51,110 篇数学论文。经过初步过滤与方向打标，系统锚定了 5,245 篇组合数学核心论文；在随后的提取阶段，系统从 2,742 篇论文中抽取出 6,453 个候选开放问题。通过联网查重与合法性检验后，最终锁定了 4,717 个确证为目前依然悬而未决、表述清晰的猜想，构成了庞大的问题池 $\mathcal{P}$。

随后，系统为这 4,717 个猜想统一分配了一次高强度推理机会（每个问题尝试一次）。在这次全量冲击下：

自动化初筛捕捉到了 598 项潜在的问题解决线索（NEW resolutions）；
经过 3 位独立裁判 Agent 的严格交叉审查，以及进一步的学术重要性定级，最终压缩至 77 个达到可发表标准（Publishable）的成果集 $\mathcal{A}$。

从 5,000 余篇论文、数千个未决难题，最终收敛到几十个高价值候选，人类数学家的评审负担被缩减了两个数量级。

作者团队随机抽取并深入复核了成果集 $\mathcal{A}$ 中他们最感兴趣的 15 项成果，人工验证确认这 15 项成果全部在数学上完全正确。

在这 15 项经过确认的战果中，不乏该领域著名的难题或知名学者的公开设问：

构造反例：成功构造了反例，推翻了 Davies–Jenssen–Perkins–Roberts 提出的关于图独立集多项式的猜想；同时推翻了 Lund–Saraf–Wolf 的代数猜想。
完成正向证明：完成了 Ikenmeyer–Pak–Panova 关于对称群特征标（Characters of Symmetric Groups）渐近性质猜想的严格证明。
回答历史设问：正面解答了数学大师 Erdős（埃尔德什）与 Straus 几十年前提出的关于二项式系数整除性的数论与组合交叉问题。

唯一戏剧性的插曲是，在复核其中一个关于 Erdős 因子差值渐近界的问题时，作者查到该问题在他们实验运行前的几个月刚刚被一位数学家独立攻克——而这恰恰侧面印证了流水线筛选出的问题，无论在难度还是前沿关注度上，都精准咬合在当前数学界的最前沿脉搏上。

算力该花在谁身上？有限预算下的最优解题策略

在实际应用中，学术团队往往没有足够的预算将几千个问题全量跑一遍昂贵推理。那么，如果只给你 $B$ 次求解机会（Budget），你应该优先把算力分配给哪些猜想？

作者在论文中将这一问题形式化为一个受约束的最优化问题：在猜想集 $\mathcal{P}$ 中选择子集 $\mathcal{S}$（$

\mathcal{S}

= B$），以最大化某种成果效用函数 $f(\mathcal{A} \cap \mathcal{S})$ 的期望：

\[\max_{\mathcal{S} \subseteq \mathcal{P}} \mathbb{E}\big[ f(\mathcal{A} \cap \mathcal{S}) \big] \quad \text{subject to } |\mathcal{S}| = B\]

为了建立分配基准，系统在未消耗求解算力之前，让轻量评估模型为池子中的每个猜想预先打出两个分数（服从中心在 0.5 的正态分布）：

难度分 $d(c)$：预测该猜想有多难被解决；
重要性分 $i(c)$：预测该猜想一旦解决，在学术上的意义有多大。

统计验证显示，模型在做题前给出的预估评分高度有效。在控制重要性分层的条件下，难度打分对模型最终能否成功攻克该问题展现出了显著的区分能力（分层 $\mathrm{AUC}_{\mathrm{strat}} = 0.56$，$p < 10^{-5}$）。这证明了在零试错成本阶段先验预判问题可行性的可能性。

基于此，研究团队针对三类截然不同的科研目标，推导出了最佳算力分配策略：

目标一：最大化产出数量（Maximize Artifact Count, $f_1 = |\mathcal{A} \cap \mathcal{S}|$） 如果目标是获得尽可能多的突破性论文，理论最优解是根据猜想最终能被解决且被评为可发表的边际概率 $\hat{p}(c) = (1 - \hat{\delta}(c))\hat{\iota}(c)$ 从大到小贪心排序，取前 $B$ 个问题。实验表明，按 $\hat{p}$ 排序大幅超越了随机均匀分配的基线。
目标二：最大化加权影响力（Maximize Total Importance, $f_2 = \sum i(c)$）

理论上应按“预期价值” $i(c)\hat{p}(c)$ 排序。而在实际测试中，按纯概率 $\hat{p}$ 排序与按预期价值排序的表现咬得极紧，均明显压制随机分配。
目标三：冲刺最高单项大奖（Maximize the Single Best Artifact, $f_3 = \max i(c)$）

数学研究中，解决一个世纪悬赏难题的价值往往盖过一百篇灌水论文。针对这种“求单极值”的目标，目标函数 $\mathbb{E}[f_3]$ 在数学上被严格证明为单调次模函数（Monotone Submodular）。

令人意外的是，如果在全量问题池上简单按得分排序，效果在算力变大时甚至会劣于随机盲抽。因为池中存在大量虽然容易被模型攻克、但重要性极低的边缘问题，贪心算法会迅速被这些低垂果实占满配额。真正有效的实操策略是“激进截断”：直接丢弃池中 90% 重要性平庸的问题，仅在最顶尖的 10% 高价值猜想中，再依据可行性概率 $\hat{p}$ 分配算力。

从“单题做题家”到“自主策展人”

长久以来，AI 社区在衡量模型数学水平时习惯于依赖静态试卷（如 GSM8K、MATH 或各类奥数基准）。这种范式默认了“题目是先验给定的、良构的、且必然存在解的”。

然而，真实的科学探索并非开卷考试。从历史文献中嗅出哪些未决问题已经被时代的技术所包围、哪些长期悬空的假设可能隐藏着致命漏洞，本身就是数学家最宝贵的核心直觉。

这项工作展现了一种清晰的未来人机协作范式：人类学者不再需要事必躬亲地阅读每一篇相关文献并逐个提炼开放式猜想，而是向上跃迁为研究方向的掌舵人与终局把关者。中间关于文献检索、猜想提炼、开放性尝试以及初步同行评审的整个繁杂流水线，都可以交由层级分明的 Agent 网络协同完成。

当大模型的长程推理算力不再像无头苍蝇一样在单一极端难题上撞墙，而是以一种经过严密概率规划的方式浇灌到整座人类知识库的待解猜想网络中时，大规模自主数学发现的黄金时代，才算真正拉开了帷幕。