DARPA 借助人工智能加速数学创新

美国国防高级研究计划局（ DARPA ）认为数学进展的速度不够快。

为了加速——或者说“指数性提升”——数学研究的进程，DARPA 本周举办了一场提案人日活动，旨在与技术界进行交流，以期望与会者在实际发布“广泛机构公告（ BAA ）”征集通知后提交提案。等等，慢点，山姆大叔。

DARPA 的项目命名为 expMath，目标是借助人工智能（或者更愿意说机器学习）来启动数学创新。

DARPA 在其网站上解释道：“指数性数学（ expMath ）的目标是通过开发一种能够提出和证明有用抽象概念的 AI 合著者，从根本上加速纯数学的进展速度。”

在弗吉尼亚州阿灵顿的 DARPA 会议中心举行的活动上，DARPA 项目经理 Patrick Shafto （ 需在左括号前加空格 Patrick Shafto ）通过展示 1878 年至 2018 年间数学进展缓慢的事实，论证了加快数学研究的重要性。

在此期间，数学进展——通过每年科学出版物数量的对数来衡量——增长率不足 1 ％。

这是基于 Lutz Bornmann 、 Robin Haunschild 和 Rüdiger Mutz 在 2021 年进行的一项研究，他们计算出，不同学科整体的科学增速约为 4.10 ％。

科学研究也会带来创新浪潮。例如，在生命科学领域，以让-巴蒂斯特·拉马克（ 1744-1829 ）和查尔斯·达尔文（ 1809-1882 ）为代表的时代中，1806 年至 1848 年间的出版物增长率达到了 8.18 ％；而在物理和技术科学领域，1793 年至 1810 年间录得 25.41 ％ 的增长，这一时期正值约瑟夫-路易·拉格朗日（ 1736–1813 ）的重要工作阶段。

“所以这些领域都经历了变化，可数学却没有，我们希望将这种变化带到数学中来。”Shafto 在他的演讲中如是说道。

DARPA 提议的创新加速器正是人工智能。但问题是，现有的 AI 智商不够高。它可以做高中水平的数学，但无法应对高水平的数学。

正如 Shafto 的一张幻灯片上所指出的，“OpenAI o1（ Strawberry ）尽管宣称具备推理能力，但在基础数学方面仍然惨遭失败。”

尽管如此，expMath 的目标是令 AI 模型具备以下能力：

auto decomposition —— 自动将自然语言叙述分解为可复用的自然语言引理（一个已被证明可用于证明其他命题的陈述）；以及

auto(in)formalization —— 将自然语言引理转换为形式化证明，再将证明转换回自然语言。

AI 研究机构 Fountain Abode 的创始人兼首席执行官 Robin Rowe 也出席了此次活动。他向 The Register 解释道，自己大学主修数学，但觉得数学枯燥，于是转向计算机科学。

尽管如此，他表示，看到目标似乎是创造一种能够作为合作者的 AI 数学家——相当于一名能够协助证明的研究生——这一点让他觉得很有趣。

也就是说，他承认这将是超越当前 AI 模型所表现出的能力水平。

Rowe 说道：“我们现在已经有了 chain-of-thought（链式思考），所以这就好比是链式思考注射了类固醇。”

对于 Rowe 来说，关键在于如何让 AI 在高级数学方面表现得更好。

他提到：“负责该项目的 Patrick Shafto 撰写了一篇关于贝叶斯归纳的论文（ PDF ），该观点认为可以使用大语言模型来解决这个问题。”

Rowe 补充说：“这并不是我倾向的方式，但房间里很多人就是这么想的，因为如果要使用现有技术，这似乎是显而易见的下一步。

我认为我们需要的是数学推理能力。

‘在场的人则觉得：‘哦，你知道，大语言模型在过去一年里有了很大进步，我们就这么不断推进下去。’ DARPA 之所以设定为三年项目，正是表明他们对这一挑战之艰巨感到担忧，这在 DARPA 中并不常见。

但就我个人而言，我认为我们需要的是数学推理能力。提案还未提交，但这就是我们计划采取的方向。不过在场还有其他人提出了不同的看法，例如采用几何数学推理等等，这样大概会有十几种不同的方式。”

换句话说，Rowe 并不确定是否应当把焦点放在自然语言上。他建议，基于视觉或音频输入的模型可能在处理高级数学时会更加得心应手。

Rowe 问道：“我们是选择基于 大语言模型 的贝叶斯归纳，这似乎是如果你来自这个领域首先会想到的方式，还是选择更激进的，例如几何建模和视觉化处理，而完全不使用文字。

“而且在现场并没有讨论，但确实有数学家在头脑中进行音频运算——他们会将数字视作音乐音调。因此，如果我们按照数学家在实际证明中所使用的多种方法来建模，可能会有很多狂野而新奇的提案出现，因为大多数人只了解常规方法，而其他方法则需要非凡的天赋，这是常人难以企及的。”

话虽如此，Rowe 依然持乐观态度，他说：“我想我们会大获成功，老实说。我认为这可能不会花费整整三年，但如果使用大语言模型的话，可能确实需要三年。那么问题就变成了，每个人愿意接受多激进的方法？”