算力「芯」动向 | Astra:十项数学进展背后,OpenAI把模型竞争带进验证时代

🐆:OpenAI内部版Astra以十项数学与理论计算机科学成果亮相,核心价值不在低成本解题,而在打通论证生成、论文整理与Lean形式化验证链路,推动大模型竞争从输出答案转向提交可复核的科研证据。


OpenAI这次没有沿用榜单分数和对话演示的常见造势方式,而是直接公开了一份249页研究论文、模型解题思路说明,以及对应的Lean形式化证明。成果来自下一代重要模型Astra的内部版本,覆盖高维几何、编码理论、群论、算子代数、计算复杂性、量子复杂性、格密码学和极值组合学等方向。
图片

严格来说,这不是十道未解难题全部被攻克。OpenAI的官方口径是,十项成果分别解决或实质推进了各自领域的长期开放问题。

这一定义差异很重要。攻克意味着给出最终答案,实质推进则可能是改进上界、构造反例、证明新的困难性,或者推翻一项长期猜想。把不同性质的成果笼统包装成破解十道世纪难题,容易放大事实,也会掩盖这次成果真正值得关注的部分。

这些进展本身并不轻。Astra构造出非sofic群,推翻Connes刚性猜想,并将高维球体堆积密度上界推进至Cohn–Elkies阈值。论文称,这是1978年以来一般球体堆积指数的首次改进。与此同时,成果还涉及永久积和式的算术电路下界、一般双人量子博弈的指数级并行重复定理、最近向量问题的近似困难性、Ehrhart体积猜想、多色Ramsey数以及极值图论中的多个厄尔多什问题。


比十项结果更值得关注的,是它们背后的科研链路。

Astra负责生成数学论证,人类研究员借助同一模型整理论文,随后模型再将每项论证形式化为Lean证明。OpenAI还公开了十份Lean 4 formalizations,并提供构建与独立检查说明。

这意味着前沿模型的能力展示方式正在变化。过去,大模型证明自己擅长科研,往往依赖基准测试、解题演示或者专家评价。现在,OpenAI选择把论证过程、论文文本和机器可检查的证明文件一并交出。能力不再只停留在回答像不像专家,而是开始接受外部工具和研究者的复核。

图片

成本口径同样需要冷静看待。OpenAI披露,按Sol API费率估算,找到十项解法所需的token总成本约为2000美元。这个数字不是每道题2000美元,也不能外推为模型训练、科研人力、论文整理、Lean形式化或全部算力投入,更不能据此计算完整科研ROI。

这个数字真正说明的不是数学研究从此只要2000美元,而是高难度理论探索正在部分转化为可追加、可复用的推理计算。过去,模型能力主要通过一次回答体现。现在,价值开始向持续搜索、反复试错和最终形成可验证成果转移。


当然,Lean证明也不等于同行评审。Lean可以核查形式化命题在给定定义、公理和类型规则下的推导是否成立,却不能自动判断自然语言问题是否被准确翻译,也不能替代学界对成果新颖性、重要性和历史定位的评价。

OpenAI自己也强调了这层边界。公司参与整理论文和Lean形式化,并对结果正确性承担责任,但数学论证由模型生成。与此同时,OpenAI明确表示,如果把完全由AI生成的证明署名为人类成果,会同时模糊系统贡献和人类原创工作的性质。

这句话指向的是科研范式的深层变化。AI可以承担大规模搜索、推导和形式化,人类仍然需要负责提出问题、确认定义、判断价值、审查边界,并把新结果放回学术脉络中。数学家的角色不是被直接替代,而是从大量机械推导转向更高层级的判断与创造。


放在大模型产业里,Astra的差异化也不是首次使用Lean。谷歌DeepSeek此前都已围绕形式化定理证明布局。OpenAI这次更突出的地方,是把多个长期开放问题的论证生成、论文整理、形式化证明和公开复现材料集中在同一次成果发布中,形成一套更完整的科研交付形态。

未来前沿模型的竞争,可能不再只看谁给出的答案更流畅,而是看谁能在长周期任务中持续推理,并把最终结果交给外部工具检验。

这十项成果并不能证明AI已经无所不能,也不能宣告数学研究进入自动化时代。它们真正释放的信号是,前沿模型正在从输出可信内容,走向提交可验证成果。榜单热度只能制造短期声量,可验证、可复核、可复现的科研产出,正在成为下一代模型更重要的能力凭证。



算力“芯”动向 · 专注AI与算力产业观察

今日阅读文章分享:

(1)Ten advances in mathematics and theoretical computer science

(链接:https://openai.com/index/ten-advances-in-mathematics/)

(2)OpenAI发布报告:Astra模型攻克十项数学难题

(链接:https://www.pingwest.com/w/316119)

(3)OpenAI官宣下一代模型Astra,取得10大未解难题突破,附249页论文(链接:https://www.toutiao.com/article/7669584795349582342/?f_link_type=f_linkinlinenote&flow_extra=eyJpbmxpbmVfZGlzcGxheV9wb3NpdGlvbiI6MCwiZG9jX3Bvc2l0aW9uIjowLCJkb2NfaWQiOiI1ZWVmYmY0Nzc5YmIyMTVhLTJkNDAxMDQ2NWI2NTYwNWMifQ%3D%3D&source=m_redirect)

(4)OpenAI确认下一代模型Astra存在,以2000美元算力成本破解十项数学未解难题,正向监管层展示

(链接:https://xueqiu.com/1107854878/403250915)

本文若有歧义欢迎读者分享指正。




2026全球闪存峰会


随着生成式AI进入规模化落地阶段,大模型训练与推理对存储性能、容量、架构的需求持续攀升,存储正从被动的数据容器,升级为驱动AI产业发展的核心底座。


在此背景下,以“存力跃迁,AI破局”为核心主题的2026全球闪存峰会(Flash Memory World 2026),将于2026年8月26日在中国武汉正式举办。本届峰会由 DOIT 传媒、华中科技大学计算机科学与技术学院、华中科技大学集成电路学院联合主办,汇聚全球存储产业链力量,全面呈现闪存技术前沿突破与 AI 时代的产业新图景。



报名通道:https://app.ehub.net/register/nga5ph







扫描下方二维码 关注我们

我们以算力为线,持续跟进算力基础设施的报道,输出洞察,伴随算力行业实现算力自由。敬请关注!


本文来源于DOIT传媒,文章内容仅供参考,不构成投资建议。

赞 ()

相关推荐

发表回复

评论列表

点击查看更多

    联系我们

    微信:百易小助手

    邮件:contact@doit.com.cn

    工作时间:周一至周五,9:30-18:30,节假日休息

    微信