（来源：科技行者）

作者 | 高飞

【编者按】8月21日，2026科学智能大会在北京中关村国际创新中心举办，由中国科协科学智能专家委员会提供学术指导。50余位院士、80余位青年学者及4000余名产学研各界代表参会，议题覆盖科学智能基础理论、科学基础大模型、行业智能体、数据集建设、产业落地应用、开源生态与国际合作等方向。本系列文章基于大会期间的报告与采访，记录各方在AI for Science领域的判断与实践。本文是对九章云极的采访。

九章云极做的是AI基础设施，为客户提供训练集群和Token推理服务。我们在2026科学智能大会的AI for Science基础理论平行会议期间，采访了九章云极AI首席科学家缪旭，他目前手头的一个重要工作正是与此有关。

缪旭认为，今年AI for Science出现了一个转折点。2026年5月，OpenAI宣布其内部推理模型证伪了数学家Paul Erdos在1946年提出的单位距离猜想，一个80年没有人解决的开放问题。在此之前，AI在数学领域的表现还停留在竞赛层面，2024年拿奥赛银牌，2025年拿金牌。Erdos猜想的证伪意味着跨了一步。“不光仅仅是像以前打金牌、打奥数的比赛做题这种类型的，它是可以做研究的。”

AI能做研究了，但离做科学发现还有距离。缪旭在采访中用了一个说法：整个AI for Science链条很长，从文献阅读到想法生成，到理论验证，到实验验证，到World Lab，“我们可能不能够做到底”。

他沿着这条链，谈了数据、模型能力、验证、基础设施和人才，每一环都有具体的判断。

数据：第100次实验

Andrew Ng团队做的AutoResearch、AI Scientist等概念正在产生示范效应，recursive self improvement（递归自我改进）的想法也在学术圈和产业界同时冒头。这些工作需要资本和组织支撑。

Jeff Dean离开Google创办了Discovery Loop，做AI驱动的自动化实验循环；图灵奖得主Richard Sutton成立了Oak Lab；盛大集团创始人陈天桥也在这个方向投入了大量资金。缪旭觉得，国内也需要类似的东西，“还没有很多新的实验室建设起来做这个事情”，目前主要还是高校在驱动。他估计后面可能会有一些新的startup出来。没有资本进来就没有办法做scaling law，而科学领域自动化实验所需的数据体量，“很可能超过互联网数据构成大模型的生态”。

但数据缺口不只是投入不足。科学界长期存在的发表偏差意味着，只有阳性结果才会被写成论文，阴性结果被系统性地过滤掉了。有研究显示，报告了阳性结果的论文被发表的概率，大约是阴性结果论文的三倍。

缪旭在大会上引用了王坚院士的一个说法：人积累知识的时候是偏科的。他把这句话落到了具体的数据问题上：“人类积累的可以用自然语言描述的数据对整个科学是冰山一角，大量的数据都埋藏在水面之下，我们都不知道。”每一个成功实验背后大概有99个100个没有成功的实验，“那些数据从来没有发表过，但是是非常有用处的一些数据，这个数据很可能你都没有了，你都找不到了，还得从头再来一遍”。

模型：归纳加演绎

当然，即使数据问题解决了，大模型本身的能力也有明确的边界。

缪旭的理由从数学出发。大模型本质上是一个回归性的算法，它的工作方式更接近统计归纳（induction），“更多是内插，不能够做很好的外推”。在已有数据点之间推算出合理的中间值，这件事大模型做得很好。但科学发现需要的往往是外推，从已知推向未知，从有限推向无限。

缪旭用数学归纳法举了个例子：如果你知道某个命题在N=0时成立，又知道从N推到N+1的规则，你可以一路推到无穷大。这是演绎（deduction）的力量，从有限步骤抵达无限结论。“但这点通过统计学是做不到的，一定有一定数学逻辑推理在里头，才能够合起来成为比较好的系统。”

“我相信，神经系统加符号系统合在一起是一个组合拳，才能最终达到哈萨比斯说的（科学发现）涌现。”采访中我们提到了DeepMind CEO Demis Hassabis的一个思想实验：如果把训练数据截止到爱因斯坦出生之前，大模型是否能涌现出相对论？缪旭对此的回答是“坦率说我持怀疑态度”，因为涌现“大家都觉得是一个观察到的现象，但没有一个理论证明存在涌现这样一件事”。因此，他给出的方向是组合：归纳加上演绎，神经网络加上符号推理。

这种组合的思路，也体现在他对科学家工作方式的观察上。“做实验的科学家很可能不这么关心理论，理论科学家可能不关心实验，有点割裂的。”他认为AI可以帮双方补上对方那块：“我是理论学家，我可以补足你做实验；我是实验学家，我可以帮你补足理论部分。”

验证：先证明，再流片

缪旭自己在九章云极内部带的研究实验室，做的就是链条上“理论验证”这一环。

整个AI for Science链条很长，不可能每一段都做。缪旭的实验室聚焦在形式化验证。他构建的系统是一个循环：一手是大模型，一手是Lean引擎。Lean是一种交互式定理证明器，用它写出的证明如果能编译通过，就意味着在数学上被机器确认是正确的，不依赖人的判断。大模型负责生成理论证明或者想法，Lean负责验证。通过了往下游传递，没通过就回到大模型重新生成。

芯片设计是目前一个具体的应用场景。“流片发现设计做错了就晚了，所以前面需要很好的验证。”缪旭的团队和复旦、北大在合作，基于一个开源的Lean库，通过大模型生成形式化表达，然后在Lean中检验。“一旦检验正确了，这表示我的设计是合理的，符合它的需求，再去生成你硬件的描述。”

这个验证前置的做法，类似于建筑师画完图纸后，结构工程师用力学公式验证承重能否达标，通过了才开工浇筑。区别在于，建筑行业这一步靠人工计算和软件模拟做了上百年，芯片设计中大模型和Lean的结合才刚刚开始。

基础设施：不动模型，动Token

验证系统要运转，底层需要Token。我们也在访谈中谈到了模型本身的演进。

九章云极的主营业务就是为客户提供算力服务，缪旭说九章是“双工厂”，一边做训练集群，一边做Token推理。

他认为Token生产的关键瓶颈在于内存带宽传输。“KV Cache你做得好与不好直接影响到输入Token质量和成本，所以为什么现在存储一飞冲天核心的原因。”九章在硬件侧围绕这些技术细节持续推进。

Token生产出来之后怎么用，也有大量可以优化的空间。缪旭观察到当前智能体的架构还比较粗暴：一个主智能体带很多子智能体做不同的事情，但所有智能体用同一个大模型。子智能体做的事情往往非常专业，不需要那么强大的模型，Token在这里被浪费了。

围绕智能体如何高效使用Token，行业经历了几轮工程迭代：从Prompt Engineering到Context Engineering，再到现在的Harness Engineering（harness指智能体的编排控制层），本质上都在解决对上下文的管理问题。

缪旭认为这些工程手段都是过渡性的。“等到自进化这件事情完成了，很可能这些都不需要了，harness会被融入背景里去，不是那么重要了。”他所说的自进化，第一步是让AI自己管理自己的上下文：知道什么时候该记忆，什么时候该修改Prompt，什么时候流程要变，目标要变。这件事“不动模型，动Token”，不需要重新训练模型，只需要模型已经具备足够的能力来做自我管理。

他给出了一个时间判断：明年初差不多能实现。被问到为什么这么乐观时，他说自己在学术论文里已经看到了很多成功的案例，前沿的新实验室也都在做这件事。“而且这个不难，他不是说动模型需要大量算力，动harness就是动Token，没有动到模型侧。”

这跟那些需要星际之门级别算力投入的叙事很不一样。缪旭认为存在两条路：如果你要进化模型本身，确实需要大厂的资源；但如果你做的是模型上面的添加层，“很可能是一个小的成本开始慢慢试错，你从小的开始试错，如果发现这里头需要scaling我再找资本”。小团队有可能完成这件事。

人才：值得投入的问题

康德说：人是目的。在AI4S的链条上最后一个环节是人自身。缪旭关注的是做AI工作所需要的能力结构正在改变。

“以前去做AI可能需要写代码那些人，但是现在AI不要写代码，而是懂得如何把一个问题能翻译成AI能听懂的格式的一个人。”行业里开始用FDE（Forward Deployed Engineer）和FDR（Forward Deployed Researcher）来描述这种角色，核心不再是对底层技术的理解深度，而是认知能力、学习速度和使用工具的能力，“强到快过于大模型”。

前一段时间，AI编程工具特别火的时候，很多企业裁掉了工程师，用AI替代。但最近又开始把人雇回去了，“当然不是所有人雇回去，雇了一些非常有经验的老师傅”。老师傅干的事情就是FDE干的事情：教AI怎么干这些活。“AI要想完整把它做下来不太可能，人跟机器之间关系发生很大变化。”

人跟机器之间的关系变了，教育也得跟着变。缪旭认为，应试教育训练出来的能力和AI时代需要的能力存在错位，“应试教育时代过去了，必须培养下一代小朋友们应该如何去面对创新这件事情”。

他自己就碰到过这种情况：给一些年轻人出了问题，自己都不知道怎么回答，结果他们拿着AI把问题解决了。

采访快结束时，记者把缪旭说的事情做了一个概括：从做题到解决问题，跳过中间模拟知识的部分，直接进入知识本身。缪旭的回应是：“应该找到值得投入的问题给下一代，这样的话给他们创造一个更好的空间，而不是让他们卷那些没有什么价值的题目。”