参考消息网6月17日报道 据英国《自然》杂志网站5月19日报道,利亚姆·普赖斯没有接受过正式的数学训练,也没有上过大学,但上个月,在ChatGPT的帮助下,他在数学研究领域取得了新突破。
普赖斯居住在英格兰西南部,他使用这种流行的人工智能工具,成功解答了埃尔德什第1196号问题,这也是匈牙利数学家保罗·埃尔德什(1913—1996年)终其一生搜罗的1000多道数学难题中的一道。
与人工智能生成的其他数学问题的解决方法不同,这次的方法让专家为之震惊。
美国斯坦福大学的数学家贾里德·迪克尔·利奇特曼在社交平台X上发帖,用国际象棋做了类比。他写道,就好像人工智能发现了一个以前受限于人类的审美惯性与固有思维而没人想到的突破口。
接连取得突破
这是人工智能在数学领域屡获佳绩的典型案例。学术界和人工智能公司的研究人员正全力探索这类系统的能力边界。如今计算机不再只承担机械的海量运算,还能完成严谨的逻辑推理。而这种能力,自2300多年前欧几里德时代起,就一直是数学家的核心专长。
诸多技术突破都依托GPT、Gemini、Claude等通用大语言模型实现,基于这类模型搭建的各类应用无需接受专门的数学定向训练。且与人工智能许多领域一样,其在数学方向的发展速度快得惊人。
现阶段,这类模型仍以借鉴现有文献中的研究方法为主。普赖斯之前与英国剑桥大学数学系本科生凯文·巴雷托合作解决其他埃尔德什难题时,便是如此。
但在破解埃尔德什第1196号问题时,数学家从模型的输出结果里,看到了具备原创性的“思考”痕迹,它还在不同数学分支间建立起意想不到的关联。
美国开放人工智能研究中心(OpenAI)的数学家圣塞巴斯蒂安·布贝克说:“这简直不可思议。一年前,学界还认为存在难以逾越的壁垒,判定大语言模型永远无法突破训练数据的局限。”
布贝克等人现在认为,人工智能迟早能达到顶尖数学家的水准,甚至实现超越。
谷歌深层思维公司超人推理团队的负责人东良(音)说:“我希望,也许到2030年,人工智能和数学家可以携手斩获菲尔兹奖(以加拿大数学家约翰·查尔斯·菲尔兹的名字命名,是数学领域的国际最高奖项之一)。”
开辟解题新路
埃尔德什于1966年提出第1196号问题,它涉及整数“原始集”,集合内任意一个整数,都无法整除集合内其他数字,素数是原始集的典型例子。
根据不同平台上的一些评论,那些尝试解决1196号问题的人使用了概率论的语言,重新拆解问题。美国加利福尼亚大学洛杉矶分校的数学家陶哲轩说,GPT直接沿用原题表述完成解答,其解法还在数论与概率论之间搭建起隐性联系。
加拿大多伦多大学数学家丹尼尔·利特表示,这一结果颇具价值,不像近段时间人工智能解决的埃尔德什问题。对人工智能迄今为止取得的成果,他态度审慎,并对围绕这些成果的炒作持批评态度。
不过利特说,看长远发展,质疑人工智能潜力的观点并不成立。
事实上,在他看来,如今人工智能拥有超越人类的数学知识储备,推理能力突出,且不知疲倦、不会懈怠,它至今未能取得颠覆性发现,反倒让人费解。
利特补充说:“谜团的一部分是,我们不知道人类数学家为何擅长数学。”人类是否拥有独有的、难以复制的创造力,目前依旧没有答案。
应用喜忧参半
与人工智能的许多领域一样,不断扩充算力、优化算法效率,会持续提升模型性能。
人工智能在数学领域的一大短板是,目前的模型最多只能产生三到四页篇幅的证明过程。东良说,谷歌内部测试的模型性能已经得到提高,或许短期内有望产出十页篇幅的证明。
他说:“现阶段模型还无法完成百页级别的证明,但我们正在朝着这个方向努力,也看到了进步。”
不过他也说,这将喜忧参半。人工审核数学论文本就压力巨大,大量人工智能生成的证明文稿,更是加剧了审稿负担。
哈佛大学数学家劳伦·威廉姆斯说:“人工智能生成的内容往往看似逻辑严密、说服力十足,审核人员需要耗费大量时间甄别其中的漏洞。”
和其他领域许多研究员一样,威廉姆斯担心劣质人工智能内容泛滥:“数学期刊上的不少编辑都可以给你讲述这类棘手问题。”
许多研究人员针对这一问题提出了应对方案。一种常见的策略是将文本输入大型语言模型(可能是生成文本的大型语言模型,也可能是其他模型),由人工智能自检正误。
例如,普赖斯和巴雷托经常将ChatGPT给出的解决方案重新导入模型,让它自己纠错,让其自查、修正错误,直至证明内容无误。如今许多数学家也会用这种方式自查论文。
谷歌团队专门开发了一款名为Aletheia的多智能体系统,其中包含针对数学文本的核验模块。不过,大语言模型的核验能力仍有缺陷,既会漏掉真实错误,也会误判出不存在的问题。
研究人员表示,更安全的策略是借助Lean(一种开源的正式编程语言,旨在为数学陈述和证明提供形式化语言并进行自动验证)。
北京大学的计算数学家董彬及其团队,就利用这一工具完成了一道代数题的核验工作。
与此同时,加州一家初创公司也借助这一翻译工具,将菲尔兹奖得主玛丽娜·维亚佐夫斯卡的研究成果转化为Lean格式,这也是首个被转化为Lean的重磅数学成果。
另一种方法是使用谷歌深层思维公司开发的人工智能数学证明系统AlphaProof,可直接基于Lean或类似的语言进行数学证明。
目前最大的局限在于,能够适配Lean编译的数学问题十分有限。扩展Lean的应用范围是一个艰难的过程。志愿者团队一直在研究这个问题。东良说:“目前只有少量数学问题可以完成形式化编译,其余内容仍需依托自然语言呈现。”
未来充满变数
2月初,当研究人员对数学领域人工智能评测基准“第一证明”开展测试时,上述短板也随之暴露。
研究人员邀请各细分领域专家出题,题目答案均未公开发表,仅出题人知晓真伪,各界均可提交人工智能生成的解答。
几乎所有的答案都是用自然语言生成的,只有一份通过Lean完成核验。部分解答经过人工校验,其他答案的对错至今仍然无从知晓。
今年6月,“第一证明”的组织者将向各种人工智能系统提出一批新的问题,并完成人工核验。研究人员表示,他们正热切期盼这项测试。
作为该项目组织者之一的威廉姆斯说,评测将聚焦面向公众开放的模型,因为大多数学家都可以使用这些模型。“希望我们所做的能够为数学界提供帮助。”
研究人员一致认为,至少在一段时间内,人类数学家仍将占据主导地位。OpenAI的数学家马克·塞尔克说:“选择研究方向更多依靠主观判断。这项工作在未来一段时间内,仍将由人类来完成。”
布朗大学数学家哈维尔·戈麦斯-塞拉诺说:“我现在甚至不敢想象五年后的行业模样。事情发展得如此之快,任何事情都有可能发生。”
不少研究人员强调,面对这场行业变革,数学界必须坚守以人为本的原则。他们说,如果机器推演的理论,连顶尖人类学者都无法理解,这样的成果便毫无意义,甚至潜藏风险。美国宾夕法尼亚州匹兹堡卡内基-梅隆大学数学家杰里米·阿维格德说:“数学的终极目标是理解数学现象,因而人类需要参与其中。我们不希望靠人工智能一味输出结论,然后去应和‘对,这个定理是正确的’。”(编译/文怡)




