荷鲁斯快报 (DeepHorus) 是一个专注于人工智能、加密与区块链、科技创新及前沿交叉领域的科技资讯平台。
发布日期

719 篇 AI 数学证明,人类真的理解了吗?

作者
  • avatar
    姓名
    荷鲁斯快报
    社交账号

陶哲轩质疑 OpenAI:719 篇 AI 数学证明,人类真的理解了吗?

OpenAI 于 10 月公布 719 份 AI 数学解答,涵盖 372 个数学结果族,涉及数百项开放研究问题。该发布随后被指尚未完全达到“数学与人工智能顾问小组”(AGMAI)提出的标准。围绕透明度、形式化验证与人类可理解性,数学界再度展开争论。加州大学洛杉矶分校数学教授、2006 年菲尔兹奖得主陶哲轩也公开表达质疑。

OpenAI 于 10 月 6 日最初在 GitHub 发布 722 份 AI 生成数学手稿,涉及 372 个结果族及多项开放研究问题。10 月 7 日,因一处符号错误及其连锁影响,OpenAI 撤回 3 份,公开目录变为 719 份。OpenAI 称发布前曾咨询普林斯顿高等研究院主持的 AGMAI,并参考其公开建议。

但从公开信息看,此次发布尚未完全达到 AGMAI 标准。AGMAI 建议前沿 AI 实验室停止在专有、外界无法访问的模型上测试高难度数学问题,并要求披露模型名称、提示词、推理链、耗时及计算成本。OpenAI 仍使用专有模型,且仅 10 份手稿附有推理链。AGMAI 还强调 AI 生成证明应便于数学家审查和学习,但约 42% 的证明未经形式化处理,也未提供将自然语言证明与形式化产物关联的机器可读元数据。

AGMAI 同时声明,其咨询角色不构成对 OpenAI 获取或发布这些结果的认可,最终仍需由数学界评估相关建议是否得到充分执行。该事件再度引发关于 AI 生成数学成果的透明度、形式化验证、同行审查及学术研究自主性的争议。

陶哲轩于 10 月 7 日在 mathstodon 发帖。他表示并不反对 AI 做数学,甚至一直是 AI 辅助研究的积极使用者;但他强烈反对把“用 AI 快速攻克著名难题”当成主要目标或产品展示。他认为,这会破坏数学共同体赖以运转的理解、教学、合作与开放探索机制。

陶哲轩指出,传统数学中,长期猜想的突破并不只是“得到答案”。作者会做报告、参加研讨、与同行交流,证明随后会被简化、解释、纳入教材,并催生后续问题、合作者和新方向。而 OpenAI 等公司当前往往由提示者驱动 AI 自主解题;目标一旦“解决”,后续理解、报告、同行讨论和领域建设却很少发生。发布者甚至可能不足以解释 AI 输出、回答问题或与领域互动。

他把这种状况称为数学界的“证明消化不良”:AI 能高速生成命题、证明和反例,但人类来不及验证、理解、写作、教学和吸收,结果出现大量“无人能消化的证明”。他尤其担心 OpenAI 把纳维–斯托克斯方程等千禧年难题当作模型能力基准来攻克。在他看来,这把“解出多少题、多快解出”当成了衡量“理解与洞见”的指标,但速度和数量本身并不等于数学理解。

陶哲轩强调,问题一旦被公开“解决”,就几乎无法恢复为“未解决”状态。即使人们后来想寻找不同路径、从中提炼新方法,仅仅知道答案存在,也会“污染”探索过程。因此,他批评这是一种不可持续的大规模“收割”:把开放问题当作可批量消耗的资源,最终会让整个数学领域变得不如传统研究方式下那样肥沃。公开资料显示,陶哲轩是 UCLA 数学教授、2006 年菲尔兹奖得主,常被称为“数学界的莫扎特”。

阅读原文 →来源:ithome