The Register 写道，DARPA 的一个名为 expMath 的新项目“旨在借助人工智能推动数学创新”。美国“国防高级研究计划局”认为，根据他们的文章，数学的发展速度还不够快……因此，为了加快——或“指数化”——数学研究的速度，DARPA 本周举办了一次提案者日活动，与技术界进行交流，希望与会者能够在实际的广泛机构公告征集结束后准备提交提案……问题是人工智能并不是很聪明。它可以做高中数学，但不能做高级数学。 [DARPA 项目经理帕特里克·沙夫托 (Patrick Shafto) 的一张幻灯片指出，OpenAI o1“尽管声称具有推理能力，但在基础数学方面仍然严重失败。”] 尽管如此，expMath 的目标是使 AI 模型能够： – 自动分解 – 自动将自然语言语句分解为可重用的自然语言引理（用于证明其他语句的经过验证的语句）；和自动（内）形式化——将自然语言引理翻译成形式证明，然后将证明翻译回自然语言。 “人工智能代理如何才能更快地推动技术进步，解决新的数学证明？”前 DARPA 研究科学家 Robin Rowe（也是 Slashdot 的长期读者 robinsrowe）问道：DARPA 表示，“指数数学的目标是通过开发一位能够提出和证明有用抽象的 AI 合著者，从根本上加快纯数学的进展速度。”文章中提到 Rowe 是一家名为“Fountain Adobe”的人工智能研究机构的创始人/首席执行官。 （他告诉 The Register 称，“这表明 DARPA 担心这个为期三年的计划可能会非常困难。这对 DARPA 来说并不正常。”）罗很乐观。 “老实说，我认为我们会扼杀它。我认为这不会花三年的时间。但我认为法学硕士可能需要三年的时间才能做到这一点。那么问题就变成了，每个人都愿意有多激进？”该项目的主页解释道：“我们将积极与数学和人工智能社区合作，从根本上重塑数学家的数学实践。”他们已经上传了一段长达一小时的提案者日活动视频。 “目前还不清楚当前的人工智能系统能否成功完成这项任务……”项目经理沙夫托在介绍该项目的简短视频中说道。但是……“数学界对改变数学实践方式的可能性充满了热情。它为数学家开辟了全新的事物。但当然，他们不是人工智能研究人员。这个项目的动机之一是将两个不同的社区聚集在一起——致力于数学人工智能的人和正在做数学的人——这样我们就解决了同样的问题。从本质上讲，这是一个非常困难且相当技术性的问题。这是DARPA 的主要任务是尝试改变世界，我认为它有潜力做到这一点。
在 Slashdot 上阅读这个故事的更多内容。