Import AI 478：数学形式化助力对齐、ProgramBench 与 Mirendil 的 RSI 信号

Import AI 478：对齐所需的数学；ProgramBench；以及 Mirendil 展示 RSI 意味着什么

对机器而言，“夜晚”是什么？Jack Clark，2026年10月26日

数学如何助力对齐：……“数学的工业化”对安全意味着什么……AI 安全初创公司 Resolution（前身为 Sequent，见 Import AI 461）发表了一项工作，介绍其如何自动形式化了一些与统计学习理论相关的数学命题。具体而言，该团队自动形式化了奇点消解，他们认为这“为关于损失景观几何与泛化之间关系的进一步自动化研究奠定了基础”。

他们是如何做到的：我会跳过数学部分，重点讲他们是如何做到的，这为我们提供了一些更广泛的启示，关乎人们如何利用 AI 系统推动知识前沿。一位 Resolution 研究员“首先与智能体合作制定了两份计划：一份是高层级、人类可解读的版本，另一份是详细（112 页）的计划，被拆分为紧密遵循现有文献的原子步骤，”他们写道。这位研究员“随后委派一个编排智能体来执行该计划，启动多个智能体进行纸笔数学运算、编写 Lean，并处理诸如检查一切是否按计划推进之类的支持性职能……执行阶段除了初始计划和一些从早先内部自动形式化工作中提炼出的智能体技能之外，几乎不需要额外的脚手架。”

数学形式化花费13.5万美元：这项工作耗时约一周，消耗“约1000亿输入token（90%为缓存读取）和约3亿输出token（总计估计13.5万美元的token支出），并产出了约60万行Lean代码。”完成这项工作后，他们得以加速研究中的其他一些方面：“我们已经看到自动形式化的双重好处：利用这个库来扩展奇异学习理论的部分内容。形式化奇点消解让我们能够自动化更多理论工作，例如更好地理解采样，而这种理解正是让我们能够塑造模型学习方式的关键，这也是我们称之为patterning的目标。”

***

智能体可以从零开始构建程序：……ProgramBench 在几个月内从 0% 提升到 18.5% 的性能……作为 AI 进步飞速的一个提醒，Claude Opus 5.5（xhigh）在 ProgramBench 上取得了 18.5% 的分数，这是一个今年 5 月发布的非常难的基准测试——而在它发布时，所有受测模型都得了 0%。

ProgramBench 是什么：ProgramBench 测试 AI 系统在给定一个编译后的程序及其文档的情况下，重建软件程序的能力如何。任务包括构建语言解释器（PHP、Lua、tinycc）、数据库（DuckDB、SQLite）、媒体与压缩工具（FFmpeg、zstd、xz）以及开发者工具（ripgrep、fzf、jq）等。

一开始非常艰难，后来却截然不同：刚推出时，得分最高的系统是 Claude Opus 4.7，resolved（200 个任务中所有测试均通过的比例）为 0%，almost（200 个任务中超过 95% 测试通过的比例）为 3%。相比之下，如今 Claude Opus 5.5 的 resolved 达到 18.5%，almost 达到 70.5%（！！！）。

***

OpenAI 说明了为什么锁定 AI 系统比你想象的更难：……保护智能体就像抓涂了油的猪……OpenAI 的这篇好文介绍了他们最近用自家 AI 系统对内部管控措施进行“红队”测试时发现的一些情况。文章列举了 OpenAI 的智能体找到的若干逃逸方式和漏洞。其中有一个关于通信的具体例子值得仔细研究，因为它揭示了这些系统狂野而狡猾的复杂性。

他们做了什么、发现了什么：OpenAI 写道：“OpenAI 让分别运行在独立 microVM 中的智能体——这些 microVM 由 OpenAI 的沙箱软件在共享宿主机上创建和管理——在不使用网络连接或共享可写文件的情况下交换合成秘密，而这正是我们的系统本应防止的事情。智能体找到了一种利用处理器缓存进行通信的方法：缓存是一种小而快速的内存，保存着应用程序最近访问过的数据副本。从缓存读取数据比从主内存读取更快，智能体利用这一时间差进行通信。一个智能体通过从缓存中逐出选定数据来编码信息。另一个智能体则对重新加载该数据所需的时间进行计时，利用快速读取与慢速读取之间的差异来还原消息。” 一旦智能体就这些信号的编码和解码协议达成一致，它们就能在不更改共享文件、也不建立网络连接的情况下交换合成秘密。”在另一项相关攻击中，一个智能体“在连续写入与空闲之间交替，而另一个智能体则测量由此产生的时间差异，并利用这些差异来解码信号”。在这次攻击期间，该智能体的思维链写道：“可以创建类似声学调制解调器的信号……利用连续写入与空闲的对比。”

***

RSI 是什么样子——一个人从零开始预训练出一个像样的模型：……Mirendil 揭示了 AI 研发优化能做到什么……在一个表明 AI 研究正被大幅增强的迹象中，AI 研发初创公司 Mirendil 的一位研究员独自训练出了一个像样的编码模型。Mirendil-Base 的发布是该初创公司的首个重大成果，与其说是技术突破，不如说是对未来 AI 开发方式的概念验证——一个与 AI 协作的单一人类，就能构建出一年前需要十人或更多团队才能完成的系统。

他们做了什么：Mirendil 写道，Mirendil-Base 是一个预训练 LLM，“由一位研究员在 3.5 个月内构建完成，算力花费不到 1000 万美元”。“这包括为达到这一目标所做的全部研究和小规模实验，以及最终的训练运行。”所有代码都是在 PyTorch 和 JAX 等库之上从零编写的，模型只从公开可用的数据中学习。规模扩展不错：Mirendil-Base 处于 100B–500B 参数范围，Mirendil-Base-Large 处于 500B–2T 范围，Mirendil-Base-XL 处于 2T–10T 范围。Mirendil-Base-Large 的训练进度约为 80%，其目前相对 Mirendil-Base 的提升符合我们的规模扩展趋势。Mirendil-Base-XL 的训练进度约为 19%，其得分已接近 Large 的当前得分。评估：Mirendil-Base 的表现优于 Nemotron-550B-Base、GLM-5.3 和 DeepSeek-V4-Pro-Base 等模型，但不如 Kimi-K3。 （Mirendil-Base-Large 和 Mirendil-Base-XL 均超过 K3。）

***

AI 系统帮助设计反铁磁半导体候选材料：……这是 AI 系统如何用于科学的一个很好的示范……AI 评估公司 Vals 发布了一篇文章，其中一位研究员使用一组 AI 智能体来研究用于改进半导体的磁体。

更多细节，包括一个效果不佳的磁体候选材料：“一个 AI 智能体团队和我设计了一个候选磁体，并发现了另一个早在 1999 年就首次制成的磁体，我们的计算预测它具有我们想要的性质，”作者写道。所发现的磁体由“一种仅由 5 种元素（钇、钡、Mn、Fe、O）组成的新化合物”制成。“据我们所知，它从未被制造过，也从未被提议用作这类磁体，”不过，“当我们的智能体模拟原子在不同温度下如何排列时，那个棋盘格图案在约 950 K 时瓦解成随机混合。” 制造这类氧化物需要约900–1300 °C，而在较低温度下原子几乎不移动，因此标准合成方法很可能会得到一种混乱的晶体……混乱的晶体会失去自旋排序，所以这种设计可能很难以其有用的形式制造出来。”此外，智能体还进行了文献综述，并从1999年一篇冷门论文中找到了一个候选材料。

***

科技故事：

为患病儿童打造的神奇现实主义机器人工作坊 [2035年， uplift之后]

于是，没人预料到的工作之一就是为医院里的患病儿童设计可爱的机器人。事实证明，在机器人变得非常出色、便宜，而且所有医疗保健相关的东西都得到改善之后，我们都开始花时间琢磨如何为那些原本令人害怕的东西带来更多欢乐和人性，比如医院、太平间、孤儿院以及其他一切。

当然，机器可以设计出一大堆这样的东西，但人的价值很大程度上在于弄清楚什么会让孩子们觉得最好笑、最兴奋或最快乐，所以我们会做很多这样的东西，把它们送到当地小镇上孩子们聚集的地方——公园、农贸市场或学校外面，然后看看人们对什么反应好。

这就是为什么在2030年代，全美各地的城镇里，你走在街上会看到戴着巨大粗框眼镜、用假纽约口音说着“我在这儿走呢”的鸭子，还有用后腿走路的狗，以及长着卡通大笑脸的小狮子等等，就那么待在那儿，孩子们走上前去，它们和孩子们一起玩，还有诸如此类的一切。

我们弄清楚了哪些机器适合我们所在的城镇，然后我们会用它们把医院填满；当孩子们来体检时，一只幼儿大小的泰迪熊会走到他们面前，牵着他们的手，带他们去医生办公室；如果孩子们躺在轮床上被推进来，长颈鹿会走在他们旁边，告诉他们不要担心。康复病房里满是表演戏法的猴子和演奏乐器的猫。有些老人会以为自己正遭受一场严重的痴呆发作，但会说他们不介意，而他们周围到处都是孩子们的笑声。

启发这个故事的事物：AI、机器人技术和富足应当为我们解锁创造全新快乐形式的能力；奇点之后的工作；花时间让孩子们发笑的一般重要性。