今天，谷歌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分。
今年5月，谷歌DeepMind又发布的AlphaEvolve，堪称最强通用AI智能体。
在数学分析、几何学、组合数学和数论领域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，也包括神经网络、可满足性求解器、证明助手以及任何其他复杂的工具。
1 AI使用声明
论文中，所有对AI实质性的使用，超出其基础功能，比如自动补全、拼写检查，或搜索引擎AI摘要，都必须明确声明。
2 AI风险讨论与缓解措施
论文中，应讨论所用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/#narrow/channel/539992-Web-public-channel---AI-Math/topic/Best.20practices.20for.20incorporating.20AI.20etc.2E.20in.20papers/near/546518354
文章来自于微信公众号 “新智元”，作者 “新智元”
