加州大学洛杉矶分校 (UCLA) 团队获得 DARPA 价值 500 万美元的合同,开发人工智能以促进数学进步

ALPHA 团队包括菲尔兹奖得主陶哲轩 (Terence Tao),其目标是改变数学发现的形成、形式化和验证方式。

来源:UCLA

加州大学洛杉矶分校计算机科学家和数学家团队获得了国防高级研究计划局为期三年、价值 500 万美元的拨款,用于开发人工智能工具,旨在改变数学发现的制定、形式化和验证方式。

该项目名为“ALPHA”——利用神经符号自动化加速形式证明综合——由加州大学洛杉矶分校 Samueli 工程学院计算机科学系教授兼系主任 Wei Wang 领导。

其他 ALPHA 团队成员包括:

  • Andrea Bertozzi,数学、机械和航空航天工程杰出教授,加州大学洛杉矶分校 Betsy Wood Knapp 创新与创造力主席持有者
  • 张凯伟,计算机科学副教授
  • 彭南云,计算机科学副教授
  • Amit Sahai,计算机科学和数学教授,赛门铁克计算机科学学期主席
  • 陶哲轩,数学教授,詹姆斯和卡罗尔·柯林斯主席,纯粹与应用数学研究所特别项目主任
  • 与其他领域相比,数学的进展仍然相对缓慢,主要原因有两个。首先,将复杂的问题分解为更小的部分(称为引理)是一个耗时的手动过程。其次,证明这些引理需要大量的努力和专业知识。

    为了应对这些挑战,ALPHA 将自动化数学推理的关键方面,包括定理分解、引理识别和新颖证明策略的生成。开源人工智能平台还将在自然语言和形式证明系统之间无缝翻译,同时保持精度。

    该项目将重点关注数学的三个主要领域——偏微分方程、数论和复杂性理论——目标是解决高级数学问题并将其影响扩展到这些核心领域之外。