Command Palette
Search for a command to run...
迈向自主数学研究
迈向自主数学研究
摘要
近年来,基础模型的快速发展催生了具备国际数学奥林匹克竞赛金牌水平推理能力的系统。然而,从竞赛级问题求解迈向专业科研,仍需应对浩如烟海的文献资料,并构建长周期、多步骤的证明过程。在本研究中,我们提出 Aletheia——一个数学研究智能体,能够以自然语言实现从问题求解的迭代生成、验证到修正的端到端闭环流程。具体而言,Aletheia 依托三大核心能力:(i)基于 Gemini Deep Think 的增强版本,用于应对高难度推理任务;(ii)一种新颖的推理时扩展规律(inference-time scaling law),可将能力延伸至超越奥数水平的复杂问题;(iii)深度工具调用机制,以应对数学研究本身的复杂性。我们展示了 Aletheia 从奥数题到博士级别习题的广泛适用性,并在人工智能辅助数学研究领域实现了若干关键里程碑:(a)由 AI 完全自主生成的一篇研究论文(Feng26),无需人类参与即可计算算术几何中一类称为“特征权重”(eigenweights)的结构常数;(b)另一篇论文(LeeSeo26),展示了人类与 AI 在证明“独立集”(independent sets)这类相互作用粒子系统界值方面的协同合作;(c)对 Bloom 的 Erdős 猜想数据库中 700 个开放问题开展的大规模半自主评估(Feng 等,2026a),其中成功自主解决四个长期悬而未决的数学问题。为帮助公众更清晰地理解人工智能与数学发展的前沿动态,我们建议建立衡量人工智能辅助成果在自主性与新颖性方面的标准化评估体系,并提出一种新型“人机协作卡片”(human-AI interaction cards)概念,以提升研究过程的透明度。最后,本文对数学领域中人机协作的未来方向进行了反思与展望。
一句话总结
谷歌DeepMind研究团队推出了Aletheia,这是一个由先进Gemini Deep Think模型、新型推理时扩展定律以及结合网页搜索和Python的工具增强推理驱动的自主数学研究代理,在IMO-ProofBench(95.1%)和FutureMath Basic上达到最先进性能,并实现三项里程碑成果:一篇完全由AI生成的算术几何特征权重论文(Feng26)、人类与AI协作完成的独立集证明(LeeSeo26),以及自主解决四个长期未解的Erdős猜想——与形式化方法系统不同,Aletheia全程以自然语言进行端到端迭代生成、验证与修订。
核心贡献
- 该论文提出了一种专门的数学推理代理,通过整合非形式化的自然语言验证,弥合了LLM推理不可靠与数学研究中形式化系统不成熟之间的鸿沟。
- 它建立了一个用于数学领域人机协作的框架,展示了一种策略:在包含3000个陷阱的3002行×3001列对抗网格中,最多仅损失两个罚分即可确保成功。
- 研究证实AI可增强而非取代数学家——表明在当前系统中,人类监督对于纠正幻觉和引导问题构建仍不可或缺。
引言
作者利用先进的语言模型,弥合竞赛级数学推理与自主研究之间的差距:解决开放性问题需要综合大量专业文献,而非回答自包含的竞赛题。此前系统,即使在国际数学奥林匹克中获得金牌水平,也因接触的研究级数学内容有限,仍难以克服幻觉与浅层理解问题。为克服这些局限,作者推出Aletheia——一个结合增强推理模型、新型推理时扩展定律和高强度工具使用(包括网页浏览与搜索)的数学研究代理,能够迭代生成、验证和修订自然语言形式的证明。Aletheia取得里程碑成果:自主推导算术几何中的特征权重、实现人类与AI在独立集界界上的协作、解决四个长期未解的Erdős问题;同时,团队提出了一套自主性层级分类与人机交互卡片,以标准化AI辅助数学中的透明度与评估体系。
方法
由Gemini Deep Think驱动的Aletheia代理采用多智能体迭代框架,通过结构化的生成、验证与修订循环解决研究级数学问题。整体架构包含三个主要子代理:生成器、验证器和修订器,它们在闭环流程中运行,直至解决方案被验证或达到最大尝试次数。框架以问题输入开始,由生成器产生候选解;该解随后由验证器评估其正确性。若判定为正确,则作为最终输出;若仅需微调,则交由修订器修改后返回生成器重新评估。此迭代优化过程持续进行,直至验证器通过解或用尽尝试次数。

系统中每个子代理均通过调用Gemini基础模型实现内部协同,以利用其强大的语言理解与推理能力。生成器负责生成初始或修订后的候选解;验证器评估这些解的逻辑一致性和正确性;修订器根据验证器反馈对解进行优化,确保内容逐步改进。这种模块化设计使Aletheia能够应对研究级数学的挑战——其解决方案通常需要超越中学课程的深厚领域知识与复杂推理。系统全程以自然语言运行,区别于AlphaGeometry和AlphaProof等基于形式语言的方法。框架的迭代特性使Aletheia能持续生成、验证和修订解,最终产出符合数学研究严格标准的高质量成果。
实验
实验评估了推理算力在奥数与博士级数学问题上的扩展表现,发现虽然增加算力可提升竞赛题的准确率,但在研究级推理中,其效果趋于饱和,无法解决普遍存在的幻觉与误读问题。引入Aletheia这一具备显式验证与工具使用的智能体框架后,显著优于先前模型,有效减少错误输出并能在不确定时主动承认失败,但仍面临细微引用错误和开放性问题误读的挑战。Erdős猜想的案例研究表明,尽管AI可生成技术上正确的解,但多数在数学上 trivial 或偏离问题本意,凸显当前系统在检索与操作方面优于真正的创造性与深度理解。
作者进行了消融实验,比较Gemini Deep Think与Aletheia在研究问题上的表现。结果表明,Deep Think虽能复现部分解,但在更复杂的提示下失败,即使使用相近算力。该对比凸显Aletheia在解决研究级问题上的优越性。Gemini Deep Think虽能复现部分解,但在复杂提示下表现更差,尽管使用了相似算力,其在多数研究问题上的表现仍逊于Aletheia。Aletheia在解决研究级问题上表现优于Deep Think。

该表格总结了Aletheia在一组Erdős问题上的表现,标明哪些问题被正确求解,哪些未解决。结果显示成功与失败尝试并存,部分问题标记为正确,其余则为错误或模糊。Aletheia成功解决了若干Erdős问题,如表格中标记的勾号所示;部分问题标记为错误,红色叉号表示失败尝试。表格涵盖多种问题类型,结果各异,反映模型在不同挑战下的表现。

该表格总结了对200个AI生成的Erdős问题解的评估,将其分为根本性错误、技术上正确、语义上正确三类。结果显示多数解为根本性错误,仅有极少数同时具备技术与语义正确性。绝大多数AI生成解为根本性错误,构成评估样本的主体;少数解技术上正确,但仅极小部分准确回应了问题本意。评估凸显了在AI生成数学解中实现语义正确性的重大挑战。

消融实验比较了Gemini Deep Think与Aletheia在研究级问题上的表现,表明即使在相近计算资源下,Aletheia在复杂提示上持续优于Deep Think。对Erdős问题AI解的评估显示,多数解为根本性错误,仅极小部分同时实现技术与语义正确,凸显生成可靠数学推理的持续性挑战。