OpenAI宣称解决多项重大数学难题,但其1147页证明尚未公开,另一项成果的论文与计算机验证代码又出现不一致。数学家担忧,缺乏透明度可能让AI制造出难以核实的数学突破。
10月29日,世界各地的顶尖数学家齐聚伦敦皇家学会,讨论数学研究的未来。人工智能取得的惊人进展令与会者兴奋不已,也让一些人怀念2026年初那个数学研究仍主要由人类主导的时代。
然而,许多数学家对AI实验室处理研究成果的方式提出批评。最近几个月,AI实验室不断发表人类几乎难以理解的数学论文,却对关键研究细节秘而不宣。数学家担忧,这种不透明不仅增加了出现不必要错误的风险,还可能制造出科学正在迅速突破的假象。
10月26日,OpenAI宣布解决了另外3个长期悬而未决的数学难题。
第一个是挂谷猜想(Kakeya conjecture),涉及如何让一根无限细的针完成旋转,同时使其扫过的面积尽可能小。此前,相关猜想已在不超过三维的空间中得到证明,而OpenAI声称将证明推广到了任意维度。
第二个是推翻指数时间假设(ETH)。这一长期被认为成立的计算复杂性假设,对计算生物学、数据库管理等领域具有重要意义。OpenAI表示,其结果将促使研究人员重新思考某些计算问题究竟能以多快的速度求解。对于这两项成果,OpenAI已经公开AI生成的证明,供专家研究。
但第三项成果却被笼罩在神秘之中。它涉及杨-米尔斯存在性与质量间隙问题,这是著名的七大千禧年数学难题之一。该问题试图从严格的数学意义上,证明现代粒子物理学的重要理论基础确实成立。尽管杨-米尔斯理论早已成功解释大量实验现象,数学家仍希望为其建立无懈可击的理论基础。
OpenAI声称,其AI模型已经证明杨-米尔斯理论的存在性,却拒绝公开长达1147页的证明。该公司将其交给一个由5名物理学家组成的审查委员会。委员会表示,在公开之前,他们首先希望确信证明是正确的。在独立专家能够审查之前,这项成果的可信度仍然存疑。
这种担忧并非没有根据。
9月8日,OpenAI曾公布另一项千禧年难题,即纳维-斯托克斯方程问题的解答,并附上使用Lean证明助手编写的形式化验证代码。Lean能够通过计算机检查证明过程中的逻辑推导是否符合规则,因此这项成果引起数学界高度关注。
然而,10月6日,剑桥大学Anders Hansen领导的团队发表研究指出,OpenAI提供的Lean验证代码与论文中的数学证明实际上并不对应。
这一问题未必意味着成果错误。Hansen认为,Lean代码可能确实包含纳维-斯托克斯问题的有效证明,但它所证明的内容与论文描述存在差异。OpenAI则回应称,其模型可能独立找到了两种不同的证明方法。
问题在于,计算机验证只能确认代码中形式化表达的命题及推导成立,并不能自动保证代码准确反映论文想要证明的内容。如果AI实验室不仔细核对两者的一致性,就可能制造出本可避免的混乱。
伦敦帝国理工学院的Lean专家Kevin Buzzard在皇家学会的报告中指出,AI实验室目前只完成了数学证明工作的一部分。真正可靠的数学突破,不仅需要机器能够验证的逻辑推导,还需要确保这些推导与人类理解和讨论的数学命题一致。
AI正在展现前所未有的数学研究能力,但能否让人类独立理解、检查并确认这些成果,仍是决定其科学价值的关键。
原文:https://www.hindustantimes.com/science/openais-approach-to-mathematics-does-not-add-up-101793846637750.html