Resolution 发布 AI 自动形式化数学研究进展

欢迎来到 Import AI，这是一份关于 AI 研究的通讯。Import AI 的动力源自 arXiv、卡布奇诺咖啡以及读者的反馈。如果您希望支持我们，请订阅。

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

他们是如何做到的： 我将略过具体的数学细节，重点介绍他们的实现方式，这为我们提供了关于人们如何利用 AI 系统推动知识前沿的更广泛启示。一位 Resolution 的研究人员写道：“首先，我们与智能体（agents）合作制定了两套方案：一套是高层级、人类可理解的版本，另一套是分为原子步骤的详细计划（共 112 页），紧密遵循现有文献。”随后，该研究人员“授权一个编排智能体（orchestrator agent）执行计划，启动其他智能体进行纸笔推导、编写 Lean 代码，并处理诸如确保任务不偏离轨道等支持性功能……执行阶段除了初始计划和从早期内部自动形式化工作中提炼出的一些智能体技能外，几乎不需要额外的脚手架（scaffolding）。”

13.5 万美元用于数学形式化： 这项工作耗时约一周，“消耗了大约 1000 亿个输入 token（其中 90% 为缓存读取）和约 3 亿个输出 token（总 token 费用估计为 135,000 美元），并生成了约 60 万行 Lean 代码。” 既然完成了这一工作，他们已经能够加速研究的其他方面：“我们已经看到了自动形式化的好处，即利用这个库来扩展奇异学习理论的某些部分。形式化奇点消解让我们能够自动化更多理论内容，例如更好地理解采样过程，而这种理解正是我们塑造模型学习方式的基础，这也是我们所谓的‘模式构建’（patterning）的目标。”

为何这很重要——也许数学热潮将助我们打造安全的 AI： 尽管前沿数学往往看似与其他领域的即时进展脱节，但此类文章凸显了二者可能融合的趋势。这里的关键点在于，AI 使得那些过去成本极其高昂、耗费大量人力时间以至于极少有人从事、且难以融入初创公司研发路线图的事情成为可能——而现在情况已发生变化。“我们预期，数学的工业化进程将催生一门全新的、严谨的研究自动化科学，”Resolution 写道。