科技日报讯 (记者张佳欣)人工智能(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未能完成证明,其尝试也可能帮助数学家更好地理解问题、发现新思路。
关于启动2024年与莫斯科大学互换奖学金、与圣彼得堡大学互换奖学金遴选工作的通知 根据《中国国家留学基金管理委 2023年,对中国高等教育而言,是内外激荡的一年。 ChatGPT的横空出世让高等教育界猝不及防;疫情的结束使得公众对校园 想象一下,在野外调查时,从森林或公园沿着小径行走时,需要走多远才能遇到一个新物种?从生态采样的角度来看,新种就是同一 12月16日至17日,由中国科学院高能物理研究所主办的南方先进光源指导委员会新能源与器件工作组研讨会在位于广东东莞的中 12月18日23时59分,甘肃省临夏回族自治州积石山保安族东乡族撒拉族自治县发生6.2级地震,震源深度10公里。截至19日16时,此次 关于全国科普工作先进集体和先进工作者拟推荐名单的公示 根据《科技部 中央宣传部 中国科协关于评选表彰全国科普 。本文链接:“深度思维”AI系统探索科研级数学问题http://www.sushuapos.com/show-11-38130-0.html
声明:本网站为非营利性网站,本网页内容由互联网博主自发贡献,不代表本站观点,本站不承担任何法律责任。天上不会到馅饼,请大家谨防诈骗!若有侵权等问题请及时与本网联系,我们将在第一时间删除处理。
上一篇: 可用光控制显色的隐形墨水研制成功
下一篇: 一周热闻回顾(2026年10月11日)