摘要：上下文窗口只说明可接收的序列长度，有效检索、状态管理、搜索预算和验证器共同决定数学智能体能否完成长程推导。本文结合长上下文评测与形式化证明系统拆解这些能力。
David Piffer 在《AI Isn’t Outthinking Mathematicians. It’s Out-Remembering Them》中提出一个很有解释力的视角：大模型在数学上的优势，部分来自巨大的外部符号工作区。题目、约束、中间式、旧结论和尝试过的路线都能留在上下文里，像一张容量惊人的草稿纸。人类工作记忆容量有限；Cowan 对相关实验的综述给出的典型估计约为四个“组块”。多项儿童研究和元分析也显示，工作记忆与数学成绩稳定相关，并能在控制 IQ、年龄等变量后解释一部分差异。
这个视角抓住了数学智能的一块关键拼图，但容易把几种能力折叠成“记得更多”。上下文窗口、可用记忆、信息检索、局部推导、路线搜索和经验复用，分别受不同机制约束。把它们拆开，才能看清数学智能体究竟从哪里获得进步。
容量写在规格表上，使用能力藏在任务里
模型支持 128K 或 1M token，只说明接口能够接收这么长的序列。它没有承诺任意位置的信息都能被稳定调用，更没有承诺模型能在全长文本上完成多步推导。
“Lost in the Middle”发现，相关材料放在长文本开头或末尾时，模型往往表现较好；放到中部，成绩会明显下降。RULER 将简单的“大海捞针”扩展为多目标检索、变量追踪和聚合任务。受测模型在单针检索上接近满分，任务稍复杂、序列变长后，几乎都出现明显退化；17 个宣称至少支持 32K 的模型中，只有约一半在 32K 仍超过论文设定的合格线。
NoLiMa 又拿掉了问题与答案片段之间的字面重合。模型需要先知道“森帕歌剧院位于德累斯顿”，再据此从长文中找到相关人物。12 个宣称至少支持 128K 的模型里，有 10 个在 32K 时降到短上下文基线的一半以下；GPT-4o 也从 99.3% 降至 69.7%。词面线索消失后，长上下文中的关联检索迅速变难。于是可以定义一个更实用的量：有效上下文，即模型在指定任务和精度阈值下仍能可靠使用的最长输入。它会随任务、噪声、相关片段位置和推理跳数变化，无法由产品标称值直接推出。
上下文像档案柜，工作记忆还要负责调度
人类工作记忆包含保持、更新、抑制干扰和操作表征。模型上下文更接近可回看的只读记录：旧 token 留在那里，模型逐步追加新 token。若要修改先前结论，通常只能写一份新结论，再让后续生成选择采用哪一份。旧错误仍在场，甚至会持续吸引注意。
因此，“保存了”与“当前会用”应分开测量。长文本里可能同时存在定义、引理、失败分支和工具日志；检索器要定位相关项，控制器要决定何时重读，状态管理器要维护当前目标，推理模型才有机会完成下一步。把所有材料原样塞入提示词，经常扩大干扰面。对科研智能体来说，结构化状态、索引、摘要和按需展开常比单纯加长窗口更有效。
LongBench v2 展示了容量与深度的交互。它收录 503 道现实长文本题，材料从 8K 到 200 万词，涵盖论文、代码仓库、多文档和结构化数据。直接作答的最佳模型为 50.1%，带较长推理过程的 o1-preview 达到 57.7%。后者说明额外推理预算有帮助；它仍不能证明窗口长度自动转化为推理深度，因为输入材料、搜索时间和解题策略同时发生了变化。
“想得更久”常常包含更广的搜索
一条更长的思维链可能完成了更多局部推导，也可能只是在同一路线上绕行。数学题的测试时计算至少有三种花法：生成更多独立解法，沿候选解继续修订，或在部分解之间做树搜索。Snell 等人的实验显示，最优分配取决于题目难度：已有雏形的题更适合修订；需要换思路的题更受益于并行采样或由过程验证器引导的搜索。固定预算下，自适应策略可比朴素 best-of-N 高效四倍以上。
这里应把推理深度与搜索预算分开。前者关心单条路线内部是否形成长依赖、抽象中间命题和有效的信用分配；后者关心尝试了多少路线、每条走多远、何时回溯。上下文容量只是容纳搜索记录的上限之一。若没有分支管理和可靠评价函数，更多 token 也可能堆积成冗长而相互矛盾的轨迹。
数学突破依赖“可验证环境＋搜索”
AlphaProof 的成果很适合校准 Piffer 的判断。系统以 Lean 的证明状态为环境，用神经网络提出 tactic、估计状态价值，再通过专门的树搜索探索证明路径。2024 年 IMO 的五道非几何题由专家手工形式化；P1、P2、P6 各经过两到三天的测试时强化学习，系统围绕目标生成大量变体并反复证明或证伪。AlphaProof 加 AlphaGeometry 2 最终达到银牌分数。
这项成绩远超“把整份草稿放进长窗口”。Lean 内核提供逐步、确定的反馈；证明状态压缩了当前假设与待证目标；树搜索保存分支并回到旧状态；强化学习把大量成功和失败经验写回策略与价值网络。Nature 论文报告，主强化学习阶段约消耗 8 万 TPU 日，自动形式化约消耗 10 万 TPU 日。系统的搜索耐力、验证密度和训练规模共同支撑了结果。
LeanDojo 的经验也指向同一方向：定理证明的瓶颈包含前提检索、搜索与规划。模型即使会生成看似合理的 tactic，仍需在形式环境中接收错误反馈、恢复证明状态、选择新分支。数学领域对 AI 友好，很大一部分原因来自反馈清晰、状态可保存、尝试可复现，而非符号文本天然让推导变得轻松。
失败轨迹只有经过压缩才会成为资产
保留失败记录还不够。LATS 在树搜索中保存失败轨迹，并生成文字反思供后续尝试使用；论文同时观察到，反思有时过于泛化，会让智能体困在局部区域。Reflexion 也把反馈转成情景记忆，作为下一轮的“语义梯度”。两者都依赖反馈质量和记忆筛选。
科研智能体需要把失败加工成可检索的对象：失败发生在哪个前提、哪一步被验证器拒绝、适用范围是什么、换用了哪条替代路线。原始长轨迹适合审计，不适合每轮全量注入。较好的做法是保留可重放日志，同时抽取“禁用动作—触发条件—证据”和尚未解决的子目标；遇到相似证明状态时再召回。这样才能减少重复犯错，也避免旧失败污染无关任务。
给数学与科研智能体的工程启示
设计重点应从“最大窗口”转向一组可测的资源：在不同噪声和推理跳数下测有效上下文；分别报告检索召回率、局部步骤正确率、整条证明通过率与单位算力成功率；为简单题、可修订题和需换表征的难题分配不同搜索策略。
系统层面可采用分层工作区：顶层保存目标、约束和已验证结论；中层维护候选引理、依赖图和分支价值；底层存放完整日志、论文片段与工具输出。每一步优先读取当前证明状态和少量相关证据，必要时再展开历史。验证器应尽量靠近生成环路，代码交给解释器，代数交给 CAS，形式证明交给 Lean。缺少强验证器的科研任务，则应记录来源、置信度和反例搜索结果，防止流畅文本冒充证据。
评测也要从单一通过率升级为压力矩阵。固定同一道题，分别改变材料长度、证据位置、无关段落比例、所需前提数量和推导跳数；再控制模型调用次数、并行分支数和验证器权限。这样可以定位失败来自“没找到”“找到后没连起来”“路线选错”还是“预算耗尽”。对于可交互系统，还应报告随预算增长的成功曲线，以及首次找到正确路线之前扩展了多少无效节点。只有把长度与计算量同时固定，模型间的比较才有解释力。基准还应保留每次工具调用、状态回滚和证据引用，便于复盘同一成功率背后的路径差异；否则高分可能来自偶然采样，低分也可能只是预算提前截断。
最后还要单独测“发现”：系统能否提出有信息增益的新定义、新表征或中间猜想，并在后续实验中得到支持。长上下文提高了保管材料的能力，搜索预算延长了试错寿命，验证器让经验可积累。数学发现还需要选题、重构问题和判断何种方向值得继续。把这些环节分别建模，AI 的数学进展才不会被一个窗口数字遮住。
来源
- David Piffer, AI Isn’t Outthinking Mathematicians. It’s Out-Remembering Them.
- Nelson Cowan, The magical number 4 in short-term memory, 2001.
- Friso-van den Bos et al., Working memory and mathematics in primary school children: A meta-analysis, 2013.
- Liu et al., Lost in the Middle, TACL 2024.
- Hsieh et al., RULER, COLM 2024.
- Modarressi et al., NoLiMa, ICML 2025.
- Tu et al., LongBench v2, 2024.
- Snell et al., Scaling LLM Test-Time Compute Optimally, 2024.
- Shinn et al., Reflexion, NeurIPS 2023.
- Zhou et al., Language Agent Tree Search, ICML 2024.
- Yang et al., LeanDojo, NeurIPS 2023.
- Hubert et al., Olympiad-level formal mathematical reasoning with reinforcement learning, Nature 2025.