🤖 AI 资讯早报 · 10-12

🔥 必读

1. 陶哲轩最新演讲《数学 2.0》：数学正从「证明稀缺」走进「证明富足」，盲目刷题已在损害数学长期健康

陶哲轩公开了在加州理工学院的最新演讲《Math 2.0》。他透露这场演讲筹划一年多，最初叫《机器辅助证明》、原定今年 5 月，因近期一系列事件推迟到 10 月且内容大改。他先回顾「Math 1.0」的核心前提——证明稀缺：找到开放问题的答案并严格证明极为困难，数学界整套制度、激励与目标都建立在这个假设上。AI 正在动摇它，因为数学有三个特别适合现代 AI 的条件：客观可验证（正确性有共识，写成 Lean 后计算机可机械检查）、高度数字化（不需物理载体或现实数据）、拥有大量高质量数据。推论是数学进入证明富足时代——有足够算力的前提下，许多过去几十年难解的开放问题可能在很短时间内被给出答案，提问者甚至不需具备相应专业知识。但他强调三点限定：① AI 能力呈明显「锯齿状」分布，前沿大多数问题仍未解决；② 解题只是更深层目标（理解数学结构、推动知识发展）的代理指标——证明富足后这一代理关系正在脱钩，「AI 给出答案 ≠ 人类获得理解」；他给出强烈判断：继续盲目只优化解题，如今已在积极损害数学的长期健康；③ 社交媒体存在幸存者偏差（他只用了「满身弹孔的飞机」示意图），公众看到的都是成功案例，失败的尝试没有曝光，因此迫切需要更透明、更科学的能力评估——须完整报告算力消耗、失败与负面结果，而非只挑成功案例，并点名 First Proof 项目是一次尝试。Math 2.0 的愿景是：AI 用于支持数学研究共同体、维护并强化「人类理解」，靠人机协作共同扩展数学边界，同时降低传统「解题」在数学研究中的中心地位。演讲幻灯片在 teorth.github.io。 原文：机器之心 · 陶哲轩最新演讲：数学2.0来了，证明稀缺时代正在终结

2. 机器人伸手时杯子被挪走：LIBERO-MAX 用 22.4 万次仿真量化「执行中途世界变了」的代价

斯坦福、CMU、MIT、UIUC、UT Austin 等机构提出 LIBERO-MAX（论文 arXiv 2609.36518，已入选 NeurIPS’26 Robotics World Modeling Workshop 口头报告）。它针对的是机器人进入真实生活的关键盲区：环境会在动作执行过程中变化（手伸到一半杯子被挪走），而机器人已依据旧画面生成了尚未执行完的动作串。现有鲁棒性评测多在任务开始前改条件；LIBERO-MAX 把变化搬到执行中途并做成可重复、可比较的考试。方法核心是配对评测：同一任务跑两次，共享初始状态、指令、模型随机种子与「变化前的全部动作」，到同一关键时刻再分叉——Base（不加入中途变化）与 Dynamic（加入一次变化）；若 Base 成功、Dynamic 失败，就识别出「原本能完成却被变化打断」的任务。它基于 LIBERO-Plus / LIBERO-PRO 构建 8,000 组配对案例、8 类中途变化（目标移动、容器移动、相机视角、传感器噪声、光照切换、视觉主题、干扰物增加、障碍物插入）。对 14 种当前机器人策略（VLA、混合架构、世界动作模型 WAM）各跑 16,000 次执行、累计 22.4 万次仿真，结论：所有受测策略成功率都下降 11.0–25.7 个百分点，动态条件下最好的 MolmoAct2 / π₀.₅ 也只有 66.9% / 65.7%，其中一个策略超过一半原有成功案例在变化后转为失败。分解看，目标/容器移动、相机与传感器变化造成损失最大，光照与视觉主题影响较小。两个反直觉发现：① 把观测频率调密（测 4 个策略、18 种执行间隔）并不能自动消除差距；② 同样的视角变化，执行到一半才出现反而比「从一开始就用改变后的视角」更容易成功——说明执行历史本身会影响结果。改进示范：在 X-VLA 前加一个图像质量检测模块（按质量触发修复、不重训），变化后成功率 40.7% → 47.7%。 原文：机器之心 · 机器人伸手时，杯子被挪走了：LIBERO-MAX用22.4万次仿真检验动态可靠性

📌 值得看

3. OpenRSI Index：用「独立验收 + 真实训练实验」考科研 Agent，能不能改进人类设计的训练方案

OpenRSI Index 在 X 上引发关注，发布帖浏览量超 13.3 万、上了 X 的 Today’s News。它直指一个瓶颈：当模型试图改进另一个模型、甚至改进自身（RSI）时，谁来定义「真实有效」的环境反馈？它的做法是从真实世界有影响力的开源研究项目出题，把已有的模型、代码、数据和训练方案交给智能体去继续改进，覆盖预训练、后训练与图像生成，算力进入数千至上万 H100·小时量级。官网三个代表任务：预训练——改进 Marin 的优化器，要求同一套规则跨 6 档模型（5.5 亿–25.45 亿参数）成立（单次 18,432 H100·小时）；后训练——为 Qwen-122B 设计更好的 RL 任务（约 20,864 H100·小时）；视觉生成——从 GPIC 学更好的生成方法（5,815 H100·小时）；另有 Open-Jev/Kev 决策架构、机器人、检索等任务。它最想改变的不是算力规模，而是评测中保留的现实复杂度（试错、尺度变化、有限预算、失败实验）。关键机制是工作区与验收环境隔离：提交时系统暂停工作区、保存快照，交给新启动的干净评测环境打分；私有测试不交给执行研究的 AI；篡改奖励路径、泄露评测信息、超预算等硬性违规计零分。架构上是两个循环——内循环（研究：Agent 在持续存在的 workspace 改代码、跑实验、按反馈继续）与外循环（验证：每次正式提交冻结为 snapshot，交独立 Judge 重新验收）。导师阵容包括 Luke Zettlemoyer（RoBERTa/BART/Toolformer 共同作者）等。⚠️ 这是一个新发布的评测项目与组织，代表任务与机制已公开，但尚无独立第三方验证的领先结果，暂按其自述口径理解。 原文：机器之心 · 从「刷榜」到「做科研」：研究员还有多久被 AI超越？

4. ChatGPT 共同创造者 Liam Fedus：数学之后，AI 该去实验室了

ChatGPT 共同创造者、OpenAI 前副总裁与后训练负责人 Liam Fedus 在播客 The Frontier（Mercor 创始人 Brendan Foody 主持、约 50 分钟）谈他为何离开大厂去门洛帕克搭实体实验室。他的核心判断是：数学之所以是 AI 攻城略地最快的科学领域，很大程度上因为它自带裁判（Lean 证明对不对编译器说了算）；但一旦问题从纸面转向物质世界——某种材料能否在液氮温区超导、某种合金高温会不会开裂——没有任何形式化系统能替代一次真实实验，这正是他创办 Periodic Labs 的动因：为 AI 科学家补上互联网给不了的那块数据。公司另一位联合创始人是 Ekin Dogus Cubuk（前 DeepMind 化学与材料团队、GNoME 论文作者之一），2025 年以 3 亿美元种子轮走出隐身状态（a16z、DST、英伟达 NVentures、Accel，以及贝索斯、施密特、Jeff Dean 等个人投资者）；9 月发布首个模型 Periodic Neon（约 1 万亿参数、在自家实验室数据上后训练，用于解读 X 射线衍射图谱），公司称在自建基准上超过 GPT-6 Astra（⚠️ 仅为公司自报）。他回顾：MIT 物理出身 → Google Brain（与 Barret Zoph、Noam Shazeer 合作提出 Switch Transformer，把 MoE 推到万亿参数）→ 2022 年加入 OpenAI 参与创造 ChatGPT → 2024-10 接掌后训练 → 2025-03 离职创业。访谈还披露 ChatGPT 诞生内幕：GPT-4 领先约一年半但仍会幻觉、不会做数学；团队曾考虑写作机器人、编程机器人乃至「会议机器人」，最终由 John Schulman 拍板做通用聊天机器人；真正引爆全球的甚至不是 GPT-4 而是早已开 API 的 GPT-3.5，关键变量是产品形态从「补全」变成「对话」；内部预测用户数时最大胆的猜测只有 100 万，「我们原本只想做一个低调的研究预览」。背景：OpenAI 前几天一次性放出 722 篇数学手稿（17 个领域、部分附 Lean 形式化证明、出自未发布内部模型，平均每个结果算力约合 ChatGPT Pro 思考模式 3 小时），随后陷入署名、优先权与是否「刷 benchmark」的争论。 原文：机器之心 · ChatGPT共同创造者Liam Fedus：数学之后，AI该去实验室了