← 返回 2026-02-12

迈向自主数学研究:基于 Aletheia 智能体的探索 Towards Autonomous Mathematics Research

Tony Feng, Trieu H. Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung, Joonkyung Lee, Carlo Pagano, Sang-hyun Kim, Federico Pasqualotto, Sergei Gukov, Jonathan N. Lee, Junsu Kim, Kaiying Hou, Golnaz Ghiasi, Yi Tay, YaGuang Li, Chenkai Kuang, Yuan Liu, Hanzhao, Lin, Evan Zheran Liu, Nigamaa Nayakanti, Xiaomeng Yang, Heng-tze Cheng, Demis Hassabis, Koray Kavukcuoglu, Quoc V. Le, Thang Luong 📅 2026-02-10 👍 36 2026-07-13 08:35
AI智能体 大语言模型 推理时缩放 数学推理 自主研究

Aletheia 数学研究智能体实现自主证明与论文生成

前置知识

推理时缩放定律(Inference-time Scaling Law)

推理时缩放定律是指在模型推理阶段通过增加计算资源(如并行思考的深度和广度)来提升模型性能的规律。与传统的训练时缩放(增加数据量或模型参数)不同,推理时缩放关注的是在给定模型的情况下,通过投入更多推理时间计算来获得更好的输出质量。本文中,Gemini Deep Think 利用并行思考机制,可以在推理时灵活调整计算量。实验表明,这种缩放可以从奥林匹克竞赛级别扩展到博士级别习题,但精度会显著下降。

理解推理时缩放定律是理解 Aletheia 如何在不增加模型参数的情况下提升数学推理能力的关键,也是本文方法论的核心技术基础。

智能体框架(Agentic Harness)

智能体框架是一种将大语言模型封装为具有特定角色和交互流程的系统架构。本文的 Aletheia 由三个子智能体组成:Generator(生成器)、Verifier(验证器)和 Reviser(修订器),它们持续交互直到验证器批准解决方案或达到预设的尝试次数上限。这种架构的核心思想是将模型的最终输出与中间思考过程解耦,使模型能够识别自己在生成过程中最初忽视的缺陷。

Aletheia 的三智能体架构是本文方法的核心创新,理解这个框架是理解为什么该系统能够超越单纯的 Deep Think 模型的关键。

形式验证与自然语言验证

形式验证使用严格的数学逻辑和计算机程序来证明数学陈述的正确性,如 AlphaGeometry 和 AlphaProof 所采用的方式。相比之下,Aletheia 采用自然语言验证,即用自然语言形式进行推理、检验和修订。这种方式的优势在于可以处理更广泛的数学问题,不局限于可以形式化表达的领域,但也更容易出现幻觉和错误。

本文明确选择了自然语言路径而非形式验证,这是与 AlphaGeometry/AlphaProof 等系统的关键区别,理解这一选择有助于把握 Aletheia 的适用范围和局限性。

Erdős 猜想数据库(Erdős Conjectures Database)

由 Thomas Bloom 于 2023 年建立的 ErdosProblems.com,是一个集中收录匈牙利数学家 Paul Erdős 遗留的未解决猜想的数据库。截至论文发表时,该数据库追踪 1,179 个问题,其中 483 个(41%)被分类为已解决。需要注意的是,数据库中标记为"Open"的问题并不总是反映文献的真实状态,有些问题实际上已经在文献中被解决但未被更新。

Erdős 问题是本文评估 Aletheia 自主研究能力的主要测试平台,理解这个数据库的背景对于解读实验结果至关重要。

FirstProof 基准

FirstProof 是由杰出学术数学家提出的十个研究级数学问题的集合,专门用于评估 AI 的数学能力。这些问题被描述为"引理"(Lemmas),即在数学家自身研究中自然产生的中间技术陈述,而非独立的开放问题。所有问题都已被数学家解决,但解决方案未在网上公开。该基准于 2026 年 2 月 5 日发布,截止日期为 2026 年 2 月 13 日,之后发布了官方(人工编写的)解决方案。

FirstProof 是当前评估 AI 数学研究能力最'干净'的基准之一,避免了数据污染问题,是本文与其他系统进行公平比较的关键依据。

研究动机

当前 AI 在竞赛数学领域取得了显著进展,例如 2025 年国际数学奥林匹克(IMO)金牌水平,但竞赛数学与专业研究数学之间存在巨大鸿沟。IMO 问题虽然需要巧妙构思,但其解答通常只有几页,仅依赖高中课程的标准定理。相比之下,研究级数学需要从大量文献中综合运用高级技术,论文往往跨越数十页。人类数学家即使获得 IMO 奖牌,通常也需要多年研究生学习才能达到数学研究的前沿。基础模型虽然拥有来自预训练的庞大知识库,但由于数据稀缺,对高级主题的理解仍然肤浅,且容易产生幻觉。具体而言,没有互联网搜索能力的模型会频繁产生虚假引用(如图 3 所示的完全虚构论文),而即使有搜索能力,模型仍倾向于错误引用合法文献的结果。

本文的目标是本文的目标是开发一个能够从竞赛级问题解决过渡到专业研究级数学的 AI 系统。具体而言,作者希望构建一个名为 Aletheia 的数学研究智能体,能够端到端地以自然语言形式迭代生成、验证和修订解决方案。该系统需要:(1)利用 Gemini Deep Think 的推理能力处理极其困难的推理问题;(2)基于推理时缩放定律从奥林匹克级别扩展到博士级别;(3)通过工具使用(如 Google Search 和网页浏览)应对数学研究的复杂性。最终目标是展示 AI 在自主数学研究方面的里程碑式成果,包括生成可发表级别的论文、系统性解决 Erdős 开放问题、以及在 FirstProof 基准上取得领先表现。

与已有工作不同的是,本文的独特切入角度在于三个方面。首先,与 AlphaGeometry 和 AlphaProof 使用形式语言不同,Aletheia 端到端地以自然语言运行,这使其能够处理更广泛的数学问题,不局限于可形式化表达的领域。其次,本文提出了一种基于'解耦'的新方法:将推理模型的最终输出与中间思考 token 分离,并添加精心设计的提示脚手架,使模型能够识别其在生成过程中最初忽视的缺陷。第三,本文不仅关注问题解决能力,还系统性地提出了'自主数学研究水平'分类框架,类似于 SAE 车辆自主性水平,从自主性和数学意义两个维度对 AI 辅助的数学结果进行分类,为公众理解和评估 AI 数学能力提供了透明的标准。

核心方法

Aletheia 的整体方法可以概括为一个三阶段迭代循环:生成、验证、修订。其直觉来源于一个经验观察:将推理模型的最终输出与中间思考 token 解耦,并添加精心选择的提示脚手架,可以使模型识别其在生成过程中最初忽视的缺陷。这可能源于训练过程激励模型猜测或虚张声势,或者延伸的思考轨迹可能充当误导性的'支持'上下文,人为地提高了错误解决方案的条件概率。技术路线上,Aletheia 基于 Gemini Deep Think 构建,包含三个子智能体:Generator(负责生成候选解决方案)、Verifier(负责检验解决方案的正确性)和 Reviser(负责根据验证反馈修订解决方案)。这三个子智能体持续交互,直到 Verifier 批准解决方案或达到预设的尝试次数上限。每个子智能体内部又涉及对 Gemini 基础模型的多次调用编排。

Aletheia 的核心创新点在于两个方面。第一是验证与生成的解耦机制。作者观察到,当模型在一个统一的思考过程中生成和验证时,容易受到'支持性'上下文的误导,导致错误答案获得过高概率。通过显式分离验证步骤,模型能够在新的上下文中重新审视自己的输出,从而发现最初忽视的错误。第二是推理时缩放的灵活应用。与传统的固定计算模式不同,Aletheia 的总推理计算是动态的,可以根据问题难度自动调整。在 IMO-ProofBench Advanced 上,Aletheia 以 93% 的总体得分(无工具使用)超越了所有测试的 Deep Think 计算规模,在 29 个返回解决方案的问题中,条件准确率达到 96%。在 FutureMath Basic(博士级别)上,虽然返回解决方案的比例不到 60%,但条件准确率超过 82%。

方法步骤详情

Aletheia 的工作流程包含以下关键步骤:(1)问题输入:将数学问题以自然语言形式输入系统,如 FirstProof 问题直接从 LaTeX 文件复制粘贴,不做任何修改。(2)生成阶段(Generator):Generator 子智能体基于 Gemini Deep Think 生成候选解决方案,利用并行思考机制探索多个思路。(3)验证阶段(Verifier):Verifier 子智能体独立评估 Generator 的输出,不依赖 Generator 的中间思考过程,从而能够发现 Generator 自身无法识别的错误。(4)修订阶段(Reviser):如果 Verifier 发现问题,Reviser 子智能体根据验证反馈修订解决方案。(5)迭代循环:上述三个阶段持续交互,直到 Verifier 批准解决方案或达到预设的尝试次数上限。(6)工具使用:在整个过程中,系统可调用 Google Search 和网页浏览来验证引用、查找文献,减少幻觉。(7)输出过滤:最终输出通过预设的验证和提取提示进行过滤,确保符合既定标准,并直接生成 LaTeX 代码,无需人工重新格式化。

技术新颖性

Aletheia 的技术新颖性体现在多个层面。首先,与 AlphaGeometry(Chervonyi et al., 2025; Trinh et al., 2024)和 AlphaProof(Hubert et al., 2025)使用形式语言不同,Aletheia 端到端地以自然语言运行,这使其能够处理更广泛的数学研究问题。其次,虽然类似的生成-验证框架已被其他研究者展示(如 Huang-Yang 手工构建的 solver-verifier 框架可将 GPT-5 提升到 IMO 金牌水平),但 Aletheia 的独特之处在于其深度集成的三智能体架构和动态推理计算。第三,本文发现了一个反直觉的结果:集成 Python 作为工具对缓解计算幻觉的改善微乎其微,这表明 Gemini 在特定任务上的基线能力已经很高,进一步提升可能需要更专业或复杂的工具。最后,本文提出的'自主数学研究水平'分类框架和'人机交互卡片'文档标准是全新的贡献,为 AI 辅助数学研究的透明评估和文档化提供了系统性框架。

Aletheia 视觉概览
Figure 1: Aletheia 视觉概览
无互联网搜索能力的模型产生的幻觉示例
Figure 3: 无互联网搜索能力的模型产生的幻觉示例

实验结果

本文的核心发现可以归纳为以下几点。在 IMO-ProofBench Advanced 基准上,Aletheia 以 93% 的总体得分(无工具使用)超越了 Deep Think 在所有测试计算规模下的表现,其中在 29 个返回解决方案的问题中,条件准确率达到 96%。在 FutureMath Basic(博士级别习题)上,Aletheia 再次在所有计算规模上超越 Deep Think,虽然返回解决方案的比例不到 60%,但条件准确率超过 82%。在 Erdős 问题的系统评估中,从 700 个标记为'Open'的问题中,模型返回 212 个可能正确的响应,经数学家团队评估后,63 个技术上正确,但只有 13 个(6.5%)有意义地正确回答了预期问题。在 FirstProof 基准上,Aletheia 在两次运行中均对 6 个问题(P2、P5、P7、P8、P9、P10)产生了解决方案,经专家评估,所有 6 个问题都被正确解决(P8 的评估存在争议,7 位专家中 5 位评为正确)。特别值得注意的是,Problem 7 的解决方案达到了可发表级别。在推理计算方面,每个 FirstProof 问题的推理成本都超过了 Erdős-1051 的推理成本,其中 P7 尤其突出,推理成本超过之前观察到的规模一个数量级。

本文涵盖的所有 AI 辅助数学结果的分类
Table 1: 本文涵盖的所有 AI 辅助数学结果的分类
Aletheia 在 Erdős 问题上的结果分类学
Table 2: Aletheia 在 Erdős 问题上的结果分类学
Aletheia 在 FirstProof 上的表现总结
Table 3: Aletheia 在 FirstProof 上的表现总结
Gemini Deep Think 在 13 个 Erdős 问题上的表现
Table 4: Gemini Deep Think 在 13 个 Erdős 问题上的表现
Gemini Deep Think 在研究论文提示上的成功情况
Table 5: Gemini Deep Think 在研究论文提示上的成功情况
200 个 AI 生成响应的解决方案准确率
Table 6: 200 个 AI 生成响应的解决方案准确率
Aletheia 两次运行在 FirstProof 上的评估结果
Table 7: Aletheia 两次运行在 FirstProof 上的评估结果
轴 1:自主性水平
Table 8: 轴 1:自主性水平
轴 2:数学结果的意义水平
Table 9: 轴 2:数学结果的意义水平
Deep Think 与 Aletheia 在两个基准上的性能对比
Figure 2: Deep Think 与 Aletheia 在两个基准上的性能对比
FirstProof 各问题的推理成本
Figure 5: FirstProof 各问题的推理成本
查看结构化数据
任务指标本文基线提升
IMO-ProofBench Advanced(奥林匹克级别) 总体得分 93%(无工具使用) Deep Think 在各计算规模下的最高得分 在 29 个返回解决方案的问题中条件准确率达 96%,超越所有测试的 Deep Think 规模
FutureMath Basic(博士级别习题) 条件准确率(已回答子集) 超过 82% Deep Think 在同等计算规模下的表现 在所有计算规模上超越 Deep Think,返回解决方案比例不到 60%
Erdős 问题(700 个开放问题) 有意义正确率 13/200(6.5%) N/A(首次系统评估) 4 个自主解决的开放问题(Erdős-652、654、1040、1051)
FirstProof 基准(10 个研究级问题) 正确解决问题数 6/10(best-of-2) GPT 5.2 Pro 解决 2 个问题(P9、P10) 超越所有已知公开模型的表现,P7 解决方案达可发表级别
Erdős 问题消融实验 正确解决数 Aletheia: 13/13 Deep Think: 8/13(2 倍平均计算量) 以一半计算量解决更多问题,Deep Think 在关键论文(Feng26)的所有提示上均失败

局限与改进

作者坦诚地指出了多项重要局限性。首先,AI 生成的结果在长度和深度上相对简短和基础,与典型的人类论文相比仍有差距。其次,成功案例似乎源于巧妙的技术操作或广泛的知识检索,而非数学家认为的真正创造力。第三,即使有验证机制,Aletheia 仍然比人类专家更容易出错。第四,当存在歧义时,模型倾向于以最容易回答的方式误解问题,即使这种解读对人类专家来说明显不是预期的。这与机器学习中'规范博弈'和'奖励黑客'的已知倾向一致。第五,幻觉仍然是常见的失败模式,即使有互联网搜索能力,模型仍倾向于编造或歪曲合法文献的结果以断言解决方案。在 Erdős 问题评估中,200 个候选解决方案中有 137 个(68.5%)存在根本性缺陷,50 个技术上正确但数学上空洞(因为问题陈述的解读未能捕捉 Erdős 的原意)。此外,'Open'状态并不总是反映文献的真实状态,之前 AI 辅助的工作在初步宣布新颖性后被发现与文献重复,这凸显了 AI 生成数学内容的一个新危险:容易'潜意识抄袭'预训练期间获得的知识。

独立分析的弱点

从独立分析的角度,Aletheia 存在以下主要弱点:(1)深度推理的可靠性不足——即使在 IMO-ProofBench 上达到 93% 的得分,仍有 7% 的问题无法正确解决,而在博士级别习题上,超过 40% 的问题无法返回解决方案。改进方向包括增强验证器的深度和广度,以及开发更有效的自我纠错机制。(2)幻觉问题未根本解决——互联网搜索只能将明显的虚假引用转移到更微妙的错误引用。改进方向可能包括开发专门的事实核查工具和更严格的引用验证流程。(3)问题理解的歧义处理——模型倾向于选择最容易回答的解读而非最合理的解读。改进方向可以是在验证阶段加入'问题意图识别'子模块,要求模型在解答前明确问题的预期解读。(4)计算资源消耗大——FirstProof 中 P7 的推理成本超过 Erdős-1051 一个数量级,表明某些问题需要极高的计算资源。改进方向包括开发更高效的搜索策略和更智能的计算分配机制。(5)评估主观性——自然语言验证由人类专家评估,'固有地涉及主观性'。改进方向可能包括开发更客观的评估标准和自动化评估工具。

未来方向

作者和本文可延伸的未来研究方向包括:(1)扩展到更广泛的数学领域——目前的结果主要集中在数论、组合学和算术几何,未来可以探索代数拓扑、微分几何等其他领域。(2)增强工具集成——作者发现 Python 工具的集成效果有限,未来可以开发更专业化的数学工具,如计算机代数系统(CAS)的深度集成。(3)形式验证的融合——虽然 Aletheia 选择自然语言路径,但未来可以探索将自然语言推理与形式验证相结合的混合方法。(4)改进推理时缩放效率——当前的 Jan 2026 模型已将 IMO-ProofBench 上的计算需求降低约两个数量级,未来可以继续优化推理效率。(5)建立标准化评估框架——作者提出的'自主数学研究水平'分类框架需要数学社区的进一步讨论和完善。(6)增强人机协作模式——从 Milestone B(LeeSeo26)的'反向工作流'(AI 提供大局策略,人类填充细节)中汲取经验,开发更有效的人机协作协议。(7)解决'潜意识抄袭'问题——开发检测和避免预训练数据中已有解决方案的机制。

复现评估

在复现性方面,本文提供了相对充分的支持。作者在 GitHub 上公开了完整的提示和模型输出(https://github.com/google-deepmind/superhuman/tree/main/aletheia),这使得其他人可以检查和验证具体的交互过程。然而,完全复现存在以下挑战:(1)模型依赖——Aletheia 基于 Gemini Deep Think 的高级版本构建,这是一个闭源模型,外部研究者无法访问完全相同的模型。(2)计算资源——推理时缩放需要大量计算资源,如 FirstProof P7 的推理成本极高,普通研究机构难以承担。(3)数据可访问性——虽然 Erdős 问题是公开的,但内部基准(如 FutureMath Basic)未公开。(4)工具集成——系统依赖 Google Search 和网页浏览等工具,这些工具的精确行为可能难以完全复制。(5)基座模型版本——论文使用了多个不同版本的基座模型(Nov 2025、Jan 2026、Feb 2026),不同版本之间的性能差异显著。总体而言,虽然核心方法论(三智能体架构、验证-解耦机制)是可复现的,但要达到论文报告的性能水平需要访问类似的模型和计算资源。