Aletheia自主攻克FirstProof数学研究挑战 Aletheia tackles FirstProof autonomously
Gemini 3数学Agent在FirstProof中自主解决6/10道研究级难题
前置知识
自主数学研究Agent
指能够在无人类数学内容干预的情况下，独立完成数学问题求解全流程的AI系统。与传统的交互式定理证明助手不同，自主Agent从问题陈述出发，自行生成证明候选方案，并通过内部验证机制筛选输出。Aletheia的设计理念是：对于研究级数学问题，可靠性比求解能力更重要，因此宁可拒绝回答也不给出错误证明。
本文的核心就是评估Aletheia作为自主数学Agent在真实研究级问题上的表现，理解这一概念是理解整个实验设计和结果解读的基础。
FirstProof挑战
由Abouzaid等人于2026年发起的数学AI能力评估，包含10个研究级数学问题，这些问题均来自专业数学家的实际研究工作。问题被描述为'引理'（Lemma），即研究过程中的中间技术陈述，而非独立的开放性问题。挑战于2026年2月5日发布，截止日期为2月13日晚11:59（太平洋标准时间），之后官方人工解答被公布。
这是本文评估的基准平台，理解其问题性质、难度水平和评估标准对于解读实验结果至关重要。
Best-of-2选择策略
对每个问题运行Agent两次，产生两个候选解决方案，然后由人类专家审查并选择最佳方案。这种策略的核心假设是：多次独立运行可以产生不同质量的输出，通过后验选择可以提高最终结果的正确率。本文中每个问题都运行了Aletheia A和Aletheia B两个不同基础模型的Agent各一次。
这一策略是本文方法论的关键组成部分，直接影响了6/10的求解率，但也引入了对人类专家选择能力的依赖。
自过滤（Self-filtering）机制
Aletheia的一个核心设计特性：当Agent对问题无法产生有信心的解决方案时，会主动输出'未找到解答'或在时间限制内不返回任何输出，而非强行给出可能错误的证明。这一机制在本文中表现为：对于P1、P3、P4、P6四个问题，两个Agent均返回无解。
自过滤直接决定了本文的一个核心发现——零误报率（false positive），即Agent从不输出错误的解决方案（在已输出的问题上），这被视为比求解率更重要的可靠性指标。
辛几何（Symplectic Geometry）
数学的一个分支，研究辛流形（symplectic manifold）及其上的几何结构。辛流形是配备了一个闭非退化2-形式的光滑流形，该2-形式称为辛形式。辛几何在经典力学（相空间）、弦理论和拓扑学中都有核心应用。本文中P8涉及多面体拉格朗日子流形（polyhedral Lagrangian submanifold）的局部光滑化问题。
P8是本文中最具争议的问题，其评估需要辛几何专业知识，5/7的专家同意率反映了该领域对证明充分性的不同标准。
Euler特征数的可乘性
对于紧流形M和N，其紧支撑有理Euler特征数满足乘积可乘性。然而，这一性质需要适当的有限性假设（如紧致性或有限型条件）才能成立。本文中Aletheia A在P7上的关键错误正是在于忽略了这些假设，错误地将可乘性应用于一般情形。
这是Aletheia A在P7上犯的关键数学错误的具体机制，理解这一概念有助于理解为什么该解被判定为'严重缺陷'。
手术理论（Surgery Theory）与切片过滤
手术理论是拓扑学中研究流形分类的核心工具，通过系统地修改流形的局部结构来构造新的流形。切片过滤（slice filtration）是该理论中的一个技术概念，其含义在历史发展中有所演变。本文中P5的问题表述存在歧义，导致Aletheia B使用了'古义'（archaic usage）解读切片过滤，与现代用法不同，从而被判定为对问题的误解。
P5的案例展示了数学问题表述的精确性对AI求解的重要影响，以及领域知识在评估中的关键作用。
研究动机
尽管大型语言模型在数学竞赛题（如MATH、GSM8K）上的表现持续提升，但AI系统在研究级数学问题上的自主求解能力仍是一个开放问题。现有评估大多依赖于标准化的竞赛题目或交互式定理证明基准，这些题目虽然困难但与实际数学研究中的问题存在本质差异——研究级问题通常缺乏明确的解题路径，需要跨领域的知识整合，且对证明的严谨性要求极高。FirstProof挑战的提出正是为了填补这一空白：它包含10个来自活跃数学家实际研究工作的问题，涵盖代数拓扑、辛几何、组合数学等多个领域，且问题本身被描述为研究过程中的中间引理而非独立的开放问题。然而，在此之前，尚无AI系统在严格的自主性约束下（即完全无人类数学内容干预）对此类问题进行系统评估。
本文的目标是本文的具体目标是评估Aletheia——一个由Gemini 3 Deep Think驱动的数学研究Agent——在FirstProof挑战的全部10个问题上的自主求解能力。更精确地说，作者希望回答三个核心问题：第一，当前最先进的AI数学Agent能否在无人类干预的情况下解决研究级数学问题？第二，Agent能否可靠地识别自己无法解决的问题（自过滤能力）？第三，通过多次运行和专家选择（best-of-2策略），能否在保持零误报率的同时最大化求解率？作者明确指出，这不是Google的集体努力，而是Aletheia团队对其系统能力的一次有限但严格的评估。
与已有工作不同的是，本文的独特切入角度体现在三个层面。首先是自主性的严格保证：与之前需要人类采样、拼接最佳输出的评估不同，Aletheia的求解过程完全自主，人类专家仅在最终输出阶段进行评估性检查，不修改任何内容。其次是可靠性优先的设计哲学：Aletheia被设计为宁可不回答也不给出错误答案，这与追求最大化问题覆盖率的传统评估思路形成鲜明对比。第三是透明度的极致追求：作者公开了完整的提示词和输出（通过GitHub），提供了Human-AI Interaction Card来记录人机交互流程，并在官方解答公布前11小时（11:07pm PST）通过邮件将解答发送给FirstProof作者以证明无数据污染。这种程度的透明度在AI数学能力评估中是前所未有的。
核心方法
Aletheia的整体方法论可以概括为'自主生成+自动验证+专家评估'的三阶段流水线。直觉上，这类似于一个数学研究小组的工作流程：研究者独立完成证明草稿，然后由同行进行审稿，最后由编辑决定是否接受。技术路线上，首先将FirstProof的10个问题的LaTeX原文直接复制粘贴作为输入（不做任何修改或简化），然后由Aletheia Agent进行自主求解。Agent的输出经过一个预先确定的验证和提取提示（verification and extraction prompt）进行过滤，该提示被设计为符合FirstProof作者提出的'符合数学文献中普遍的严谨性和学术性水平'的标准。最后，由学术数学家对输出进行独立评估。关键在于，整个求解过程中没有任何人类干预——人类专家仅在评估阶段介入，检查最终输出但不修改任何内容。
本文的核心创新在于将'可靠性'而非'求解率'作为自主数学Agent的首要设计目标。与现有方法的本质区别体现在：第一，严格的自主性约束——Aletheia的求解过程保证在最严格意义上完全自主，没有任何人类对数学内容的干预，这与需要人类专家采样和拼接最佳输出的方法形成根本区别；第二，自过滤机制——当Agent无法产生有信心的解决方案时，会主动拒绝回答而非强行输出可能错误的证明，这在10个问题中表现为4个问题（P1、P3、P4、P6）均返回无解；第三，双模型集成——使用两个不同的基础模型（Aletheia A基于Gemini 3 Deep Think，Aletheia B基于2026年1月的Gemini模型）独立求解，通过best-of-2策略选择最佳方案，这使得单个模型的错误可以被另一个模型纠正（如P7中Aletheia A失败但Aletheia B成功）。
方法步骤详情
方法的具体步骤如下：第一步，问题输入——将FirstProof的10个问题从LaTeX源文件中直接复制粘贴，不做任何修改或预处理，确保输入的原真性。第二步，自主求解——分别使用Aletheia A（基于Gemini 3 Deep Think基础模型）和Aletheia B（基于2026年1月的Gemini基础模型）对每个问题进行独立求解，每个问题运行两次（每个模型各一次）。Agent内部包含Generator子Agent和Verifier子Agent的交互循环：Generator生成候选解，Verifier进行验证和反馈，两者之间进行多轮交互直至通过验证或达到计算预算上限。第三步，自动验证和提取——将Agent的原始输出通过一个预先确定的验证和提取提示进行过滤，该提示设计为确保输出符合数学文献中普遍的严谨性和学术性水平，同时直接输出LaTeX代码以避免人工格式化。第四步，专家评估——对每个问题的候选解，由至少2名学术数学家（部分与Google有附属关系）进行独立评估。当专家信心不足时，邀请更多专家参与（如P8最终有7名专家评估）。评估标准是'经过小幅修订后可发表'（publishable after minor revisions）。第五步，最佳方案选择——根据专家评估结果，从Aletheia A和Aletheia B的输出中为每个问题选择一个首选解决方案，其评级显示在Table 1中。
技术新颖性
本文的技术新颖性主要体现在以下几个方面：第一，自主性认证机制——作者通过Human-AI Interaction Card和提前邮件认证（在官方解答公布前11小时发送给FirstProof作者）建立了严格的自主性证明，这在AI数学评估中是首创；第二，可靠性导向的评估框架——不同于传统的'能解决多少问题'的评估思路，本文将'是否输出了错误答案'（false positive率）作为核心指标，自过滤机制确保了在已输出问题上的零误报率；第三，双模型集成的互补性分析——通过对比Aletheia A和B在不同问题上的表现（如P7中A失败B成功，P5中A正确B误解），揭示了不同基础模型在数学推理上的互补性，这为未来的模型集成策略提供了实证依据；第四，推理成本作为问题难度的代理指标——创新性地将推理计算量与之前的基准（Erdos-1051）进行对比，为衡量数学问题的AI难度提供了新的量化视角。
实验结果
本文的核心发现可以从三个维度进行分析。首先，在求解能力方面，Aletheia在best-of-2评估下自主解决了10个FirstProof问题中的6个（P2、P5、P7、P8、P9、P10），求解率达到60%。具体而言，P2、P9、P10两个模型均正确求解（分别获得4/4、4/4+2/2、2/2的专家同意率）；P5中Aletheia A正确（4/4）但Aletheia B误解了问题（对'切片过滤'使用了古义解读）；P7中Aletheia B正确（3/3）但Aletheia A存在严重缺陷（错误应用Euler特征数的可乘性）；P8最具争议，Aletheia B的解获得5/7专家同意（3名辛几何专家+2名相邻领域数学家认为正确，1名辛几何专家+1名相邻数学家认为细节不足）。其次，在可靠性方面，对于P1、P3、P4、P6四个问题，两个Agent均返回无解，实现了零误报率。这意味着当Aletheia输出一个解决方案时，该方案在专家评估中被判定为正确的概率极高。第三，在推理成本方面，所有问题的推理计算量均超过Erdos-1051基准，其中P7的推理成本超过该基准一个数量级——这是因为Generator子Agent需要更多计算来生成候选解，且需要更多轮次才能通过Verifier子Agent的验证。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| FirstProof整体求解率（best-of-2） | 正确求解问题数/总问题数 | 6/10（60%） | 无先前基线（首次评估） | 首个在严格自主性约束下对此类研究级问题进行系统评估的AI系统 |
| 单模型求解率（Aletheia A） | 正确求解问题数/总问题数 | 4/10（P2、P5、P9、P10正确，P8不充分，P7严重缺陷） | Aletheia B: 4/10（P2、P7、P9、P10正确，P5误解，P8有争议） | 两个模型的错误模式互补，best-of-2策略将求解率提升至6/10 |
| 误报率（False Positive Rate） | 错误输出数/总输出数 | 0%（自过滤机制确保不输出无信心的解答） | 无先前基线 | 首次在AI数学Agent中实现零误报率 |
| 推理成本（相对Erdos-1051） | 推理计算量倍数 | 所有问题均超过1倍，P7超过10倍 | Erdos-1051（1倍） | 首次量化研究级数学问题的AI推理成本分布 |
局限与改进
本文的局限性需要从作者承认的和独立观察的两个层面来分析。作者明确承认的局限性包括：第一，这是一个有限的研究，由Aletheia团队自行进行，不代表Google的集体努力；第二，FirstProof本身不是正式基准，而是'实验性试验'，其问题选择和评估标准都存在主观性；第三，'正确'的定义（'经过小幅修订后可发表'）具有主观性，特别是在P8的案例中，5/7的专家同意率反映了对'细节充分性'的不同标准——所有专家都同意证明的数学内容没有错误，但部分专家认为某些步骤（如多面体拉格朗日子流形的局部光滑化在顶点和边之间的插值步骤）缺乏足够细节。作者独立观察到的局限性包括：第一，best-of-2策略虽然提升了求解率，但需要人类专家审查两个候选解并选择最佳方案，这在实际应用中可能难以规模化；第二，自过滤机制虽然保证了零误报率，但也意味着Agent无法回答40%的问题，对于需要探索性尝试的研究场景，这种保守策略可能不适用；第三，专家评估的样本量较小（每题2-7人），且缺乏评估者间一致性的量化指标；第四，论文未提供推理成本的绝对数值（仅给出相对倍数），使得独立复现和成本评估变得困难；第五，评估仅涵盖拓扑学和几何学领域的问题（P5、P7、P8），缺乏代数、数论、组合数学等领域的覆盖，限制了结论的普适性。
独立分析的弱点
本文存在几个值得深入分析的弱点。首先，best-of-2选择策略的人类依赖问题：虽然作者声称求解过程完全自主，但'为每个问题选择首选解决方案'这一关键步骤仍然需要人类专家的领域知识。在实际应用中，如果数学家不具备足够的专业知识来判断哪个候选解更好，这一策略的有效性将大打折扣。改进方向可以是开发自动化的解质量评估模型，或使用更多次运行（如best-of-N）来减少对单次人类判断的依赖。其次，P5案例暴露的问题表述敏感性：Aletheia B对'切片过滤'使用了古义解读，这说明Agent对数学术语的历史演变和上下文依赖性处理不足。改进方向可以是在Agent的知识库中整合术语的多义性信息，或在问题输入阶段增加术语消歧的预处理步骤。第三，P7中Aletheia A的Euler特征数错误揭示了Agent在应用数学定理时对前提条件的忽视——可乘性需要有限性假设，但Agent未检查这些假设是否满足。改进方向可以是强化Verifier子Agent对定理适用条件的检查能力。第四，推理成本的不透明性：论文仅提供相对倍数而未给出绝对数值，且承认两个基础模型与Erdos-1051中使用的模型不同，使得成本对比的有效性受到质疑。改进方向可以是标准化推理成本的度量方式，并在相同硬件配置下进行公平对比。
未来方向
基于本文的成果，未来研究方向可以从以下几个维度展开。第一，扩展问题覆盖范围：当前评估仅涵盖拓扑学和几何学领域的问题，未来可以将评估扩展到代数、数论、组合数学、分析等更多数学分支，以检验Aletheia的通用性。第二，改进自过滤机制的灵敏度：当前机制过于保守（40%的问题被过滤），未来可以研究如何在保持低误报率的同时提高问题覆盖率，例如通过渐进式信心评估或多阶段过滤策略。第三，开发自动化的解质量评估：减少对人类专家的依赖，可能的方法包括使用多个AI模型的共识、形式化验证工具的集成、或基于证明结构的自动分析。第四，研究推理成本与问题特征的关系：本文发现P7的推理成本远高于其他问题（超过Erdos-1051一个数量级），未来可以系统研究哪些数学问题特征（如涉及的数学领域、证明长度、所需的创造性跳跃）与推理成本相关。第五，探索Aletheia与其他AI数学系统的集成：如与Lean、Coq等形式化证明助手的结合，以实现从非形式化证明到形式化验证的自动化流水线。第六，研究多Agent协作求解：当前的best-of-2策略是后验选择，未来可以探索让多个Agent在求解过程中实时协作，共享中间结果和策略。
复现评估
本文在可复现性方面提供了较高程度的透明度，但仍存在一些挑战。开源方面，作者公开了完整的原始提示词和输出，托管在GitHub仓库（https://github.com/google-deepmind/superhuman/tree/main/aletheia），这使得研究者可以审查Agent的完整推理过程。然而，Aletheia Agent本身及其基础模型（Gemini 3 Deep Think）并非开源，这意味着其他研究者无法直接复现求解过程，只能分析已有的输入输出。数据方面，FirstProof的10个问题是公开的（来自1stproof.org），官方解答也在截止日期后公布，这为结果验证提供了基础。算力方面，论文未提供推理成本的绝对数值（如GPU小时数或token消耗量），仅给出相对于Erdos-1051的倍数，且承认使用的模型与Erdos-1051中的模型不同，这使得独立的成本评估和资源配置变得困难。复现难度方面，即使拥有相同的模型和算力，best-of-2策略中的'选择最佳方案'步骤仍需要领域专家的参与，这增加了复现的人力成本。此外，P8案例的专家评估不一致性（5/7）表明，即使是相同的输出，不同的评估者也可能得出不同结论，这进一步增加了结果复现的不确定性。总体而言，本文的可复现性处于中等水平：输入输出和评估标准是透明的，但核心Agent和模型的不可获取性限制了完全独立的复现。
论文图表
