问题在于问题：迈向可扩展的数学发现

TL;DR FAR 将人机数学发现从“预先选单个问题”改为“给定方向后自动挖掘文献猜想”，通过级联过滤与推理聚焦专家评审到 77 项高潜候选，产出多个新结果。

问题

问题背景

AI 辅助数学研究已从解决竞赛题走向参与研究级猜想，但当前流程中 “选题” 和 “专家审稿” 两个环节高度依赖人工，成为规模化瓶颈。

现有方法局限

• 主流工作流是 人类预先选定一个具体问题，再由 AI 求解，最后人工审查。专家时间被大量消耗在从海量文献中筛选合适问题、核对猜想是否仍开放、评估 AI 解的正确性。
• 缺乏候选问题的 自动生成与过滤机制：选题环节未自动化，无法从大规模论文库中系统挖掘可攻击的开放问题。
• 前沿模型推理和专家审查均为稀缺资源，但现有方法没有 系统化的资源分配策略，导致计算浪费在已解决或低价值猜想上。

为什么这个问题难 / 重要

• 自动判断一个猜想的 良定义性、开放状态、研究价值 与 可攻击性，需要结合文献语义理解、形式化验证和启发式推理，技术挑战远超单一数学题求解。
• 该问题直接决定 AI-for-math 的 投入产出比：若能将专家注意力聚焦于经多级过滤后的高潜力候选，可显著提升发现效率，因此业界关注度持续上升。

行业类比

类似 推荐系统 的“召回 → 粗排 → 精排 → 人工审核”级联架构，将稀缺的人工审核资源精准分配给最可能转化的候选对象。

核心洞察

• 将数学发现的主要瓶颈从证明搜索转移到问题发现与专家评审分配。FAR 让人类仅提供研究方向，系统从文献中自动挖掘候选猜想并分层过滤，改变了以往人类需预先选定具体问题的模式。相比直接使用大模型做定理证明或反例搜索，该工作把“找什么题”本身建模为可扩展的信息检索与推荐流程。
• 把专家评审视为稀缺资源，用多阶段级联（提取、验证、尝试、评分、推荐）模仿搜索/推荐系统，实现对注意力的最优分配。这种设计直面研究实践中“推理算力有限、专家时间更稀缺”的约束，与仅优化证明成功率的系统形成差异；其有效性由组合学试点中 5245 篇论文筛至 77 项且产出多项有意义结果的产出率佐证。

方法

输入与总体流程

FAR 的输入是研究方向而非单一问题，人类专家仅标定感兴趣的领域，系统在大规模文献库中自动搜索与提取候选开放问题。

关键模块

1. Find：从指定语料（如 5,245 篇组合数学论文）中检索相关论文，通过标注模型识别包含猜想或开放问题的段落，抽取并恢复具体陈述，同时检查其有效性与解决状态（是否仍开放、是否良定义）。
2. Attempt：对筛选后的问题池调用推理模型尝试解决，生成候选证明或反例，并记录中间结果。
3. Recommend：基于自动打分（难度、重要性等）对候选解答进行分诊排序，筛选出值得人工审查的条目，推荐给专家。

输出与工程视角

最终输出是经过多级过滤的候选发现，示例中从 6,453 个猜想筛选到 77 个送审。该框架将稀缺的专家评审资源集中在高价值产物上，通过自动化扩展了问题发现与初步尝试的规模。

差异点: 与传统“人选题、人审查”的流程不同，FAR 将问题发现和初步求解前移为自动化流水线，人类专家从操作者变为方向指导者与终审者。

实验

实验设计

FAR 在组合数学领域开展 pilot run，从 5,245 篇组合数学论文出发，通过文献检索与标注、猜想提取与状态校验，构建候选开放问题池。随后经过推理尝试与自动分诊，逐步缩小范围，最终筛选出 77 项交由作者团队专家评审。整个流程是 literature-to-review cascade，将稀缺的专家注意力集中在多级过滤后的高潜结果上。

关键发现

• 从 5,245 篇论文中提取 6,453 条候选猜想，校验后保留 4,717 条仍开放且良定义的猜想。
• 自动推理与分诊阶段产出 598 个潜在解决结果，最终 77 个进入人工评审。
• 专家评审确认多项有趣发现，涉及 Davies--Jenssen--Perkins--Roberts、Erdős--Straus、Ikenmeyer--Pak--Panova、Lund--Saraf--Wolf 等著名猜想/问题。

对比解读

与常见 AI-for-math 工作流（人工选问题 + 事后评审）相比，FAR 将人类输入从单个问题改为研究方向，把问题发现与筛选自动化，使专家评审阶段更聚焦。这种级联筛选显著降低了人工在前期选题与后期评审中的瓶颈压力，体现了搜索/推荐系统思想在数学发现中的迁移价值。但由于缺乏与 baseline 的量化对比，后续需在多个数学方向验证泛化性。

行业影响

落地场景

FAR 流水线可嵌入 AI 辅助研究平台、企业内部知识发现系统 或 学术出版分析工具。例如，生物医药企业可利用它扫描海量论文，提取尚未解决的机制猜想，转化为可验证的研发假设；大型科技公司的研究院可自动挖掘理论计算机或运筹学文献中的开放问题，并初步尝试求解，筛选出对产品优化有潜在价值的数学结构。

商业价值

• 降本：将专家从繁重的文献筛选和问题识别中解放，减少每个候选问题的人工评审时间。
• 增收：加速从基础研究到技术转化的周期，提高专利/技术秘密产出率，尤其适合需要长期数学积累的行业（密码学、通信、材料计算）。
• 体验提升：研究人员获得经过多级过滤的高质量开放问题列表，避免无效探索，提升工作满意度与产出。

与现有产品/工作流的接口

FAR 可作为 微服务 或 插件 接入现有科研工作栈：

1. 对接文献数据库（arXiv、PubMed、Semantic Scholar）自动拉取论文元数据；
2. 调用 LLM 推理 API 完成猜想提取与初步求解；
3. 输出候选列表到任务管理工具（Jira、Notion）或实验平台，触发专家评审流程。

具体 use case：

• 某 药物研发 SaaS 将 FAR 集成到靶点发现模块，扫描生物通路文献中的未验证关系，生成候选靶点供计算化学团队复核。
• 某 自动驾驶公司 的研究部门用 FAR 挖掘控制理论/优化文献中的开放猜想，自动尝试构造反例或弱证明，辅助判断新算法可行性。

局限

• **试点范围单一且依赖文献陈述**：本研究仅在组合数学领域完成试点，从 arXiv 等开放语料中提取候选猜想，这天然受限于文献中明确写出的开放问题或猜想。许多前沿数学问题可能尚未被显式表述，或分散在非英语、非开放获取的出版物中。此外，自动提取与状态判定依赖 LLM 对论文上下文的理解，存在漏检或误判已解决/未解决状态的风险，而作者未对提取覆盖率与精确率进行系统评估。
• **多阶段错误累积与评审瓶颈未完全消除**：FAR 流水线包含查找、尝试、推荐等多个环节，任一阶段的错误（如命题形式化错误、验证不充分）都会向下游传播并放大。尽管最终仅推荐 77 项给专家评审，但专家仍须逐一验证这些候选解决方案，人力成本依然显著。作者承认自动检查无法完全替代人工证明验证，尤其对于深度组合数学结果，LLM 生成的证明草图可能存在隐藏漏洞。
• **评分模型泛化性存疑**：系统用内部评分（难度、重要性）来筛选推荐项，但该评分模型基于有限的人工标注数据训练或校准，其有效性仅在本次组合数学试点中通过少量结果验证。对于其他数学分支（如代数几何、数论、分析），问题的难度与重要性分布差异极大，现有评分是否可迁移尚不清楚。此外，该框架假设研究方向上存在足够多的可提取候选问题，对于新兴或小众领域，文献池过小可能导致流水线失效。