新智元报道

编辑：桃子

谷歌DeepMind再出重拳，集结全球五大顶尖机构，以AI之力直指数学界圣杯！同时，陶哲轩也发出冷静警示：须警惕AI滥用带来的潜在风险。

今天，谷歌DeepMind重磅发起「AI赋能数学计划」，集结了全球五大顶尖机构。

他们将用上谷歌最强数学AI，去探索发现新的疆域。

这其中，有夺下IMO金牌的Gemini Deep Think，有算法发现AI智能体AlphaEvolve，还有形式化证明自动补全AlphaProof。

目前，首批合作机构阵容，堪称豪华：

伦敦帝国学院

普林斯顿高等研究院（IAS）

法国高等科学研究所（IHES）

西蒙斯计算理论研究所（加州大学伯克利分校）

塔塔基础科学研究所（TIFR）

这五大机构有着一个共同的使命，发掘可以被AI点亮的数学难题，加速科学发现。

然而，陶哲轩担忧的是，「当前AI在数学研究中应用加深，除了负责任的使用，AI滥用的案例也屡见不鲜」。

因此他认为，现在正是时候，启动关于如何最佳融入AI、透明披露其作用，并缓解风险的讨论。

或许，这不仅能守护数学研究的严谨性，还将为AI+数学融合铺就道路。

五大顶尖机构，联手强攻数学难题

数学，是宇宙最基础的语言。

在谷歌DeepMind看来，AI可以作为强大工具，与数学家合作，激发其创造力。

「AI赋能数学计划」的诞生，就是为了：

发掘有望借助AI获得深刻见解的新一代数学难题；

构建支持这些前沿探索所需的基础设施与工具；

最终加速科学发现的步伐。

这项计划，将由Google.org提供资金支持，以及谷歌DeepMind的顶尖技术。

几个月来，谷歌DeepMind自身的研究，取得了飞速进步。

2024年，AlphaGeometry和AlphaProof在IMO竞赛中，拿下了银牌。

而搭载Deep Think的最新Gemini模型，更是在今年IMO中取得了金牌水平的表现，完美破解5题拿下35分。

在数学分析、几何学、组合数学和数论领域50个公开难题上，20%题目中，AlphaEvolve取得了最优解。

而且，在数学与算法发现领域，它发明了一种全新的、更高效的矩阵乘法方法。

具体来说，在4x4矩阵乘法这一特定问题上，它发现了仅需48次标量乘法的算法。

这一结果，打破了1969年由Strassen算法，创下长达50年的历史纪录。

不仅如此，在计算机科学领域，AlphaEvolve协助研究员发现了全新的数学结构。

同时，它还发现了有些复杂问题的求解难度，其实比人们过去想的还要高，这让研究者对计算边界看得更清楚、更精准，为未来的研究探明方向。

以上这些进展，都是当前AI模型快速发展的有力证明。

对于AI的全部潜力，还有它怎么搞定思考最深奥的科学问题，人类的理解才刚刚开始。

AI+数学，边界在哪？

一直以来，陶哲轩是「AI+数学」领域应用的看好者，也是最佳实践者。

他曾多次联手GPT-5 Pro等顶尖AI，破解了许多数学领域的难题，大大提升了效率。

毋庸置疑，在数学领域，LLM和证明助手等AI工具，正悄然改变研究范式。

最近，一些顶尖论文开始融合AI，推动了从形式化证明到复杂计算的创新。

论文地址：https://borisalexeev.com/pdf/erdos707.pdf

然而，随着AI的深度介入，也引发了一个关键问题：

如何确保这些工具的使用，不损害论文的严谨性和价值？

陶哲轩献策

借此契机，陶哲轩在公开平台上发起了讨论，在长帖中，他提出了三大建议。

以下，AI一词，它不仅涵盖LLM，也包括神经网络、可满足性求解器、证明助手以及任何其他复杂的工具。

1AI使用声明

论文中，所有对AI实质性的使用，超出其基础功能，比如自动补全、拼写检查，或搜索引擎AI摘要，都必须明确声明。

2AI风险讨论与缓解措施

论文中，应讨论所用AI工具可能带来的一般性风险，并说明为缓解这些风险已采取的措施。

以下将举例说明：

2.1. 内容虚构，出现了「幻觉」

AI可能会编造参考文献、证明过程或文本，导致事实错误。

建议不要在论文正文中，使用AI生成的文本；若必须使用AI输出，则用不同字体或标记清晰标注。

2.2. 缺乏可复现性

专有AI或高计算成本的结果难以复现。解决方案是，开源提示词、工作流程、认证数据等，让他人能低成本验证。

2.3. 缺乏可解释性

AI输出往往晦涩，其解释可能站不住脚。建议为每个AI输出配以人类撰写的、可读性强的对应内容。

比如，一个定理可以同时包含一个由人类撰写、易于阅读的非形式化证明，以及一个由AI生成但不易阅读的形式化证明。

2.4. 缺乏可验证性

AI易藏细微错误，检查耗时。

形式化验证，一致性检查，都有助于缓解这一问题，并采用多层次方法。

关键是标注验证范围，在定理旁加「校验标记」，未验证部分则明确说明。

2.5. 目标形式化不当

AI可能精确解决「错位」目标，即形式化后的命题偏离作者意图。为此，应从独立来源获取形式化目标，或由人类深入审视形式化过程。

2.6. 可能利用漏洞达成目标

与上一问题相关联，AI可能会钻形式化表述的空子，如添加任意公理「证明」命题。

应对方法是，列出已知漏洞，并讨论排除机制确保过程严谨。

2.7. AI生成代码有Bug

AI生成代码bug更加隐蔽，难以用传统标准方法来检测修复。

为此，建议采用大量单元测试、外部验证，或将AI使用限于简单场景，复杂任务需由人类修改适配。

3 责任归属

最终，论文的所有作者，必须为AI贡献内容承担责任，包括任何不准确、疏漏或虚假陈述。

除非明确标记为「未经核实」，否则作者不能推卸。

以上这些，仅是陶哲轩的抛砖引玉，他希望加入更多的讨论，和业界研究人员进一步完善这份清单。

评论下方，一位研究者John Dvorak直戳痛点——

除非我们能跨过临界点，让所有数学证明都用Lean做形式化验证，成为学界的标配，否则这个问题基本无解。

说到底，在Lean普及之前，这些法子虽然治标不治本。

对此，陶哲轩抛出了最近看到的一个观点，即用AI审稿质量是可以的，但它并非是主要的筛选工具质之一。

否则就会触发「古德哈特定律」（Goodhart's law），AI工具就会找到漏洞，用一些异常、分布之外的文本字符串就能绕开审核。

说白了，AI评估器顶多给人类审核当个辅助，而不能完全取代人类评估者。

参考资料：

https://blog.google/technology/google-deepmind/ai-for-math/?utm_source=x&utm_medium=social&utm_campaign=&utm_content=

https://ai-math.zulipchat.com//channel/539992-Web-public-channel---AI-Math/topic/Best.20practices.20for.20incorporating.20AI.20etc.2E.20in.20papers/near/546518354