陶哲轩与邓煜对谈AI数学成果:证明量产背后存在理解缺口与溯源断裂

真正值得关注的问题不是AI解决了多少新问题,而是这些证明能否被理解、能否验证、能否在此基础上继续探索。

在OpenAI于10月6日一次性发布722篇AI生成的数学预印本、随后因符号错误撤回三篇之后,围绕AI与数学关系的讨论从“是否取代数学家”转向了更基础的层面。近日,在陶哲轩发起的非营利机构SAIR Foundation播客节目中,菲尔兹奖得主、SAIR主席陶哲轩与今年新晋菲尔兹奖得主、芝加哥大学教授邓煜展开对谈,讨论AI产出数学成果的理解责任与学术传承问题。

事件的时间线显示,今年9月OpenAI宣称其模型攻克纳维-斯托克斯方程,25位菲尔兹奖得主随后联名发出公开信;10月6日的722篇预印本发布后,次日因符号错误撤回三篇;10月8日的成果更新日志显示,另有14篇被修订、13篇更新引用,手稿总数从722降至719。两位对谈者均位列联名公开信的签署者之中。

邓煜在对话中提出,数学存在两条边界:一条是已有证明的问题的边界,另一条是人类能够理解证明的边界。过去几个世纪里两者基本重合,解出一道难题通常意味着真正弄懂了它。陶哲轩进一步指出,数学界奖励“解题”,实际奖励的是包括讲解证明、提出新问题、培养学生在内的整套活动,解题只是其中最易衡量的指标。AI在短时间内生成大量证明后,“得到解答”与“掌握背后逻辑”开始分离。

陶哲轩表示,OpenAI发布的成果中有十来个问题他都很关心,之后会去看,但按目前的解释方式还未能打动他。不过他同时认可其中与编号003的准黎曼猜想相关的结果,该结果将zeta函数零点的无零点区域推进到7/8,陶哲轩称之为“该问题五十年来最大进展”,并认为这个由三四个既有想法拼出的安排“恐怕没有一位在世数学家能独自组装出来”。问题不在成果本身,而在发布方式。

理解缺口已有量化证据。按发布初期对仓库形式化目录的统计,722篇预印本中经过Lean等形式化验证的比例仅约22%,10月3日至6日新增的143篇中无一经过Lean形式化验证。且Lean只验证形式化后的陈述,并不保证其与原问题一致。陶哲轩将这一现象称为“证明消化不良”,即产出速度远超消化能力。

对谈揭示的第二个问题是思想溯源链条的断裂。陶哲轩指出,科技公司利用AI研究数学,本质上是在提炼他人的研究成果,从论文和研究中获取数据。学术界遵循开放科学原则数百年,引用让思想可被追溯,而AI将积累的文献“不透明地转化为答案”,有时能指出参考文献,有时则无法追溯。邓煜举例称,已出现有人直接使用他人在ChatGPT中输入的想法来生成证明的情况,他主张AI至少应公开思维链,让人知道参考了什么材料。

这一问题与9月公开信的批评一脉相承。信中批评AI公司以越来越快的节奏大规模生产“真/假”陈述,绕开同行评议,而验证与消化的成本由数学共同体承担。10月7日,人类数学协会发表声明,称一次性发布700多份文件“展示的不是学术研究,而是权力展示”,并敦促数学家停止与OpenAI的合作,陶哲轩在个人博客转发了该声明。他在对谈中表示,批量解题产出的成果成了某种副产物,甚至可以说是“有毒废料”,后续需要想办法处理,或由数学家来处理。

国内学界也作出回应。10月11日,“丘成桐数学与人工智能实验室联盟”在清华大学成立,丘成桐在求真书院回应争议时称“就像海啸来了,我们该如何应对海啸”。何旭华则认为,这批内容“并非全部符合学术规范,但其中有很多值得吸收的想法和成果”。

两位数学家给出的方案核心是改变激励而非拒绝技术。陶哲轩主张,如果AI产出的成果只给出答案,而不附带理解、解释和可追溯的引用,就不应成为数学文献的一部分,这类产出需先经过形式化验证并留出人类消化期。他还认为,理想状态是AI公司在项目启动时就与数学家协作,帮助理解证明、标注来源,而非发布之后再请学界兜底。

从722篇预印本的批量发布到形式化验证率仅约22%的现实,AI在数学领域的产出能力与学术共同体的消化能力之间已出现明显落差。如何在保持开放科学传统的前提下,为AI生成的研究成果建立可追溯、可验证的准入标准,将成为AI公司与学术机构下一阶段需要共同面对的问题。

该文观点仅代表作者本人,企服科学平台仅提供信息存储空间服务。

赞 (0)
AI冲击白领岗位后,程序员转向PLC培训寻求再就业
上一篇 1小时前
商务部:前三季度重点平台具身智能机器人销售额增长22.6%
下一篇 1小时前

相关推荐

发表回复

登录后才能评论
分享本页
返回顶部