一个在"工程性价比"上登峰造极，一个在"科研创造性"上触及质变。把它们放在一起看，会发现它们共同指向同一个命题：AI 做科研的时代，可能真的来了。这篇杂谈不打算罗列技术细节，而是想从科研范式的角度，谈谈这件事意味着什么。
一、两个标志性事件，同一个方向
先简单复述这两件事的"反直觉"之处。
事件一：DeepSeek-V4-Flash 的"换脑不换身"。 基座架构一字未改，所有提升全靠后训练重调，结果 13B 激活参数的模型，在 Agent 基准上反超自家 49B 激活的旗舰预览版。它颠覆了"能力提升必须靠堆预训练算力"的叙事，证明在强基座之上，后训练的工程化精细化能以极低成本撬动巨大跃升。
事件二：Astra 攻克十年开放难题。 它解的不是已知答案的竞赛题，而是方向都尚未清晰的开放难题，并附上了机器可逐行验证的 Lean 4 证明。它把 AI 从"在已知解空间里检索组合"，推进到了"在未知领域里探索创造"。
二者一个偏"工程"，一个偏"科学"，但合在一起，恰好勾勒出 AI 走向科研的两条腿：一条是"用得更巧"（后训练驱动 Agent），一条是"想得更新"（探索式科研）。
二、从"答题"到"探索"：能力本质的跃迁
理解这件事的关键，是分清"答题"与"做研究"的区别。
过去十年，AI 在各种考试里不断刷新分数：从 ImageNet 到 MMLU，从 AIME 到 SWE-bench。但所有这些基准都有一个共同特征——答案已知。模型本质上是在一个已被前人探索过的解空间里，做检索与组合。它像极了一个记忆力超群、反应极快的考生。
而真正的科研，是在没有地图的领域里画地图。它要求：
Astra 这次的工作，第一次让模型在这条"无地图"的路上走出了实质性的一步。这是从"考生"到"研究者"的角色转变，而非又一次分数提升。
# 用三段伪代码刻画能力的演进
def era_exam(known_problems, knowledge):
# 考场时代：在已知解空间里检索组合
return retrieve_and_combine(known_problems, knowledge)
def era_reasoning(known_problems, knowledge):
# 推理时代：多步思考 + 自我纠错，但仍收敛到已知答案
return self_correct(build_chain(known_problems, knowledge))
def era_research(open_problems, tools, verifier):
# 科研时代：答案未知，需要探索 + 创造 + 外部验证
idea = propose(open_problems) # 人/机提出猜想
draft = explore_and_construct(idea, tools) # 探索并构造证明
return verifier(draft) # 形式化/实验做最终裁判三、科研范式的三重转变
如果"AI 做科研"真的成立，它会重塑科研的三个底层范式。
3.1 验证范式：从"权威背书"到"机器校验"
传统科研的"正确性"高度依赖同行评议——一群权威专家花几个月时间审稿，来判断一项工作是否成立。这种方式的代价是慢、贵、且无法完全排除主观性。
Astra 公开 Lean 4 形式化证明，预示着另一种可能：正确性可以被机器逐行校验。当证明的每一步都必须由更基础的公理推导而来，"权威"就让位于"逻辑"。这对数学、理论计算机科学等领域的影响是颠覆性的。
3.2 分工范式：从"孤胆天才"到"人机协作"
浪漫主义科学史喜欢歌颂"孤胆天才"——一个人在阁楼里想出改变世界的理论。但真实科研中，研究者大约把 80% 的时间花在繁琐的严格化、试错、验证上，只有 20% 用于真正有创造性的"提出问题"。
如果"科研型 AI + 形式化验证"链路成熟，这个比例会被翻转：人类专注提出好问题，AI 负责执行与验证。这不是"AI 取代研究者"，而是"研究者被解放到更有价值的位置上"。
3.3 成本范式：从"重算力"到"重后训练"
DeepSeek-V4-Flash 的成功说明，科研能力的提升不一定来自天文数字的预训练算力。后训练的工程化精细化，同样能带来数倍跃升，且成本低得多、可重复性高得多。
这对资源有限的中小科研机构意义重大：你不必追赶旗舰基座，而可以在开源强基座上，把后训练做到极致。这为"平民化科研 AI"打开了一扇窗。
四、挑战与边界：别让热情跑在现实前面
在为突破欢呼之余，必须清醒地看到边界，否则很容易陷入新一轮的"AI 神话"。
4.1 领域偏科
Astra 的成果集中在结构清晰、可形式化的数学领域。在需要大量经验直觉的生物、化学实验科学，以及需要复杂社会语境的社科领域，AI 的科研能力仍有巨大差距。"能在数学上做研究"不等于"能在所有学科做研究"。
4.2 验证的成本与门槛
形式化证明本身有极高的学习与使用门槛。能把研究成果"翻译"成 Lean 4 的人才，全球都稀缺。这构成了一条现实的鸿沟：AI 能产出证明，但能"形式化翻译"的人很少。
4.3 伪证明的风险
当 AI 能产出"看起来正确"的证明时，未经形式化的伪证明可能大量涌现，混淆视听。社区必须建立"未形式化即不轻信"的把关机制，否则科学传播会被噪音淹没。
4.4 算力与开放的不对称
能做出此类突破的模型，训练与推理成本极高；而 OpenAI 此次只公开成果、未开放模型。这意味着短期内，普通研究者无法直接调用 Astra 的科研能力。"AI 科研民主化"还远未到来。
4.5 科研伦理的新课题
当 AI 成为论文的"协作者"甚至"贡献者"，署名、贡献界定、责任归属都需要新的规范。这不是细枝末节，而是关乎科学诚信根基的大问题。
五、给研究者的几条建议
面对这股浪潮，研究者既不必恐慌，也不宜观望。几条务实的建议：
5.1 学一门交互式定理证明器
无论是 Lean 4、Coq 还是 Isabelle，掌握至少一门 ITP，将和今天掌握 Python 一样基础。它是你与"科研型 AI"的共同语言。
5.2 把"提出好问题"作为核心能力来训练
当执行与验证可以被 AI 接管，人类最不可替代的价值，就是提出有洞察力的好问题。这恰恰是当前教育体系最不擅长培养的能力，值得刻意练习。
5.3 主动拥抱"人机协作流水线"
尝试建立"人提猜想 → AI 草拟证明/实验 → 机器/同行验证"的协作流程。先在小问题上跑通，再逐步扩展到核心课题。
5.4 警惕"AI 万能论"与"AI 无用论"两个极端
既不要神话 AI 的科研能力，也不要因为它的边界而全盘否定。把它当成一个"能力强但有盲区"的协作者，是最健康的心态。
# 一个朴素的人机协作科研流水线骨架
def collaborative_research_loop(human, ai, verifier, max_iter=10):
for _ in range(max_iter):
conjecture = human.propose() # 人：提出猜想
draft = ai.construct(conjecture) # AI：草拟证明/方案
result = verifier.check(draft) # 机器：形式化/实验验证
if result.ok:
return result.proof
human.feedback(result.counterexample) # 人：根据反例修正方向
return None # 超过迭代上限，交回人类深度思考六、冷思考：我们正在见证什么
把视角拉远一点，2026 年 8 月的这两件事，或许会被后来的科学史这样记录：
在那个夏天，AI 第一次同时证明了它"能更便宜地变强"（DeepSeek）和"能探索未知"（Astra）。前者让强大的能力变得人人可及，后者让"研究"这件事本身被重新定义。
但历史也常常提醒我们：技术突破与它真正改变科研日常之间，往往隔着十年以上的"工程化鸿沟"。深度学习 2012 年就在 ImageNet 上震惊世界，但真正渗透进每个学科，是很多年后的事。
所以，与其说"AI 做科研的时代已经到来"，不如说"AI 做科研的时代已经露出曙光"。对身处其中的我们，最理性的态度或许是：认真对待这束光，但不被它晃花了眼。
七、尾声
DeepSeek 的工程师们用后训练证明，"用得巧"能撬动"跑得快"；Astra 的研究者们用形式化证明，"想得新"能触及"做得深"。它们一个代表工程的极致，一个代表科学的远方。
而真正让人兴奋的，不是它们各自有多强，而是当"更便宜地变强"与"探索未知"结合在一起时，会发生什么。也许在不久的将来，一个偏远地区的研究者，能用开源模型提出一个改变学科的好问题，并由 AI 给出可被机器验证的证明。
那一刻，科研才真正属于每一个人。
科学史上有过几次"范式转移"——从经验到理论，从理论到计算，从计算到数据驱动。下一次，会不会是"从人类独占到人机共创"？答案，或许就藏在这个夏天。
💬 评论区 (0)
暂无评论，快来抢沙发吧！