OpenAI数学解题尚未达到业界标准

OpenAI本周发布了数百个号称能解答全球最难数学题的证明方案，但这场发布很快遭到数学界的质疑。这家前沿实验室此前表示，为了避免重蹈上次模型解题引发争议的覆辙，已咨询了一个由顶尖数学家组成的顾问小组。然而从实际发布的内容看，OpenAI并未达到顾问小组提出的标准，尤其是在数学家们反复强调的一点上——人类必须能够理解数学结果。这一缺失在另一篇新论文的映衬下显得格外刺眼：该论文指出，OpenAI模型号称解决的一个百万美元级数学难题，其自然语言证明与形式化代码之间存在明显出入。 这个名为AGMAI（数学与人工智能顾问小组）的机构由普林斯顿大学高等研究院主办，成员包括全球九位知名研究者，今年九月底发布了针对前沿实验室解题的指导原则。AGMAI在关于OpenAI最新证明集的声明中表示，最终要由数学界来评估其建议被落实的程度。但该组织的首要要求是停止在专有模型上测试高等数学问题，而OpenAI的发布明确表示正在用开放研究问题评估其专有模型。TechCrunch就OpenAI此次发布向AGMAI寻求更详细评估，对方未予回应。 OpenAI确实遵循了部分原则，比如尽快公开结果、披露模型得出答案的过程。但并非全部：719份证明稿中只有10份附带了模型的思维链。对于人类难以理解的论文，数学家们建议将证明形式化，而OpenAI发布的证明中有42%未经过这一流程。更根本的问题在于，OpenAI是否按照AGMAI的原则，承担起了确保人类能够理解这些证明的责任，目前仍不明朗。AGMAI建议OpenAI出资支持人类数学家的工作，因为只有他们才能让这些解答真正产生意义。 知名数学家陶哲轩在发布后于社交媒体上写道，问题正被AI提示者自动解决，而这些人一旦初始目标达成便对更广泛的领域失去兴趣，对AI输出的理解也不足以回答问题、做报告或与学界其他成员互动。剑桥大学和伦敦国王学院数学家本周发表的论文恰好印证了这一担忧。AI模型解数学题时，先产生自然语言解释，再尝试用Lean编程语言表达，理论上通过编译成代码来验证证明的正确性。但模型在将自然语言证明翻译成代码时可能出错。该论文记录了OpenAI针对纳维-斯托克斯方程（描述流体复杂行为）衍生问题所给解答中，自然语言证明与Lean代码之间至少存在两处不一致。这些出入未必推翻任一解答，但确实让人质疑：我们能否在没有人参与的情况下，单纯依赖模型将自己的解答形式化。这也是AGMAI要求OpenAI加入可读元数据、将自然语言与形式化产物关联起来的原因之一，而OpenAI此次发布并未做到这一点。