详细内容或原文请订阅后点击阅览
数学家的最新助手是人工智能
人工智能与人类的合作可能在数学上取得超人的成就
来源:科学美国人数学家通过提出猜想并用定理证明它们来探索思想。几个世纪以来，他们一行一行地建立这些证明，大多数数学研究人员今天仍然以这种方式工作。但人工智能有望从根本上改变这一过程。绰号为“副驾驶”的人工智能助手开始帮助数学家开发证明——这很有可能有一天让人类解答一些目前超出我们思维范围的问题。
加州理工学院正在开发一种有前途的人工智能副驾驶。它可以自动提出证明中的下一步并帮助完成中间数学目标，帮助建立更大步骤之间的逻辑连接。“如果我正在开发一个证明，这个新的副驾驶会给我提供多个前进的建议，”加州理工学院计算和数学科学教授 Animashree Anandkumar 说。Anandkumar 和她的团队在最近的一篇预印本论文中介绍了人工智能副驾驶，该论文尚未经过同行评审。她说，至关重要的是，这些建议“都将是正确的”。
最近的预印本论文副驾驶是一个大型语言模型 (LLM)，与 OpenAI 的 ChatGPT 和谷歌的 Gemini 背后的机器学习系统相同。虽然它的训练方式不同，但也类似于谷歌的 AlphaProof 和 AlphaGeometry 2 所采用的技术——这两项技术都在今年的国际数学奥林匹克 (IMO) 中为世界最优秀的高中生生成了银牌标准的复杂数学证明。虽然 LLM 可以生成从技术意义上讲是“胡说八道”的东西，但副驾驶的错误建议会被检查和拒绝。在加州理工学院副驾驶的案例中，这要归功于人工智能运行的软件 Lean，它使用严格的数学逻辑来筛选有效的陈述。
银牌 产生技术意义上的“废话”