“深度思维”AI系统探索科研级数学问题

人工智能（AI）正从解决数学竞赛题迈向探索科研级数学问题。谷歌旗下“深度思维”公司团队开发并测试了一种名为AlphaProof Nexus的AI框架，其能自主搜索数学证明，并利用计算机程序验证推理过程。在测试中，该系统解决了9个此前未解决的厄多斯问题，其中两个已悬而未决超过50年。此外，该系统还解决了44个开放数学猜想。相关成果发表于最新一期《科学》杂志。同期评论文章指出，AI用于科研级数学的时代已经到来。 近年来，AI解决数学问题的能力不断提升。然而，竞赛数学主要考查已有方法的灵活运用，大型语言模型还容易产生逻辑错误，难以直接用于严谨的数学研究。 为解决这一问题，团队让AI使用Lean等形式化证明工具。所谓“形式化”，就是用足够精确的语言完整写出数学证明，让计算机能够逐步检查每一步推理是否符合数学公理和规则。团队在这里使用的Lean证明助手，能够自动验证证明的逻辑正确性，帮助发现推理中的错误。 此次开发的AlphaProof Nexus能够根据Lean编译器的反馈不断调整证明。其功能更完善的版本还可利用进化算法协调多个子智能体，并调用“深度思维”的AlphaProof作为专门的证明工具。 团队用该系统挑战了以数学家保罗·厄多斯命名的一系列开放问题。在353个尝试解决的问题中，系统攻克了9个，其中两个此前已超过50年没有得到解决。 此外，该系统解决了《整数数列在线百科全书》492个开放猜想中的44个，同时处理了代数几何、优化、量子光学和图论等领域的多个科研级问题。 团队还发现，最基础版本的智能体同样解决了上述9个厄多斯问题，只是在处理较难问题时需要更多计算资源。该版本主要依靠商业化大型语言模型和Lean证明助手。这一结果表明，随着通用大模型能力提升，通用AI智能体也有望参与科研级数学探索。 不过，部分数学家担心，大规模使用AI可能削弱人们探索数学问题和理解证明过程的动力。团队认为，即使AI未能完成证明，其尝试也可能帮助数学家更好地理解问题、发现新思路。