OpenAI 发布 719 份数学难题解答，未达数学家咨询组设定的标准
来源TechCrunch AI查看原文
速览
- OpenAI 发布 719 份数学难题解答，仅 10 份公开思维链。
- AGMAI 首要建议是停止在专有模型上测试高等数学问题，OpenAI 未遵守。
- 42% 的证明未做形式化，与 AGMAI 建议不符。
- 新论文发现 OpenAI 某解答的自然语言证明与 Lean 代码存在至少两处不一致。
- AGMAI 要求提供自然语言与形式化产物的关联元数据，OpenAI 未提供。
- 数学家 Terence Tao 批评 AI 解题者缺乏对领域的持续参与和理解。
- Melanie Wood 指出 AI 解答发布时无人类理解，后续工作才刚开始。
- AGMAI 称最终评估权在数学界，未对 OpenAI 此次发布做完整评价。
OpenAI 本周发布了数百份针对世界级数学难题的解答，并称已咨询由普林斯顿高等研究院主办的「数学与人工智能咨询组」（AGMAI）以避免重蹈此前争议。但 TechCrunch 的核查显示，OpenAI 的做法与 AGMAI 在 9 月底发布的指导原则存在明显落差：AGMAI 的第一条要求是「停止在专有模型上测试高等数学问题」，而 OpenAI 明确表示其正是用开放研究问题评估专有模型；719 份手稿中只有 10 份公开了模型的思维链；AGMAI 建议对难以理解的证明进行形式化，而 OpenAI 发布的证明中有 42% 未经过这一流程。与此同时，剑桥大学与伦敦国王学院数学家本周发表的论文记录了 OpenAI 就一个源自 Navier-Stokes 方程的问题所给解答中，自然语言证明与 Lean 代码之间至少存在两处不一致，说明模型在「自然语言→形式化代码」的转换环节可能出错。数学家 Terence Tao、Melanie Wood 等人指出，AI 产出的解答在发布时并不伴随人类理解，后续的验证与消化工作才刚刚开始。
关键事实
- OpenAI 本周发布了 719 份针对高难度数学问题的解答手稿，其中仅 10 份公开了模型的思维链。
- AGMAI 由普林斯顿大学高等研究院主办，由全球九位知名研究者组成，于 9 月底发布针对前沿实验室的数学解题指导原则。
- AGMAI 的第一条要求是「停止在专有模型上测试高等数学问题」，而 OpenAI 的发布说明中明确表示正在用开放研究问题评估其专有模型。
- OpenAI 发布的证明中有 42% 未经过形式化流程，而 AGMAI 建议对人们难以理解的证明进行形式化。
- 剑桥大学与伦敦国王学院的数学家本周发表论文，记录了 OpenAI 就一个源自 Navier-Stokes 方程的问题所给解答中，自然语言证明与 Lean 代码之间至少两处不一致。
- AGMAI 要求 OpenAI「包含将自然语言与形式化产物关联起来的机器可读元数据」，OpenAI 此次发布未做到。
本站视角
这件事的关键不在于 OpenAI 又解出了多少难题，而在于它暴露了前沿实验室与数学共同体之间正在形成的规则冲突。对做形式化验证和 Lean 工具链的中文团队来说，剑桥与国王学院那篇论文指出的「自然语言到 Lean 的误译」是一个可直接落地的技术信号：自动形式化不能默认可信，需要引入交叉校验或人工复核环节，否则下游任何基于这些证明的工作都可能建立在错误之上。对使用 API 做数学或科研辅助的中小团队，这意味着不能把模型输出的证明直接当作结论使用，尤其在涉及 Navier-Stokes 这类复杂问题时，验证成本可能高于自己重做。对关注 AI for Science 的国内研究者，AGMAI 提出的「机器可读元数据关联自然语言与形式化产物」是一个值得跟进的具体标准，未来可能成为论文与成果发布的合规要求。我们的判断是：OpenAI 此次发布在流程上部分回应了 AGMAI，但在最核心的两点——不在专有模型上测试高等数学问题、确保人类理解跟进——上并未达标，719 份中仅 10 份公开思维链、42% 未形式化，这些数字本身就说明「可核查性」被放在了次要位置。需要观察的是，AGMAI 明确把评估权交给数学界，而数学界目前缺乏强制手段，若前沿实验室继续以发布速度优先，这类指导原则很可能停留在倡议层面。另一个可疑之处是，AGMAI 未回应 TechCrunch 的置评请求，也未对 OpenAI 此次发布给出完整评估，因此「OpenAI 是否遵守了标准」目前只有 TechCrunch 的单方面核查，读者应保留这一信息来源的局限。
背景与影响
这并非 OpenAI 第一次因数学成果引发争议。此前其模型解决了一个长期悬而未决的数学问题，随之而来的争议促使 OpenAI 在本次发布前咨询了 AGMAI。AGMAI 由普林斯顿大学高等研究院主办，成员为全球九位知名研究者，9 月底发布的指导原则核心是：前沿实验室在发布数学成果时应确保人类能够理解，并承担相应责任。数学界的惯例是，人类发现新结果后要对其负责，通过论文、演讲和研讨会与更广泛的共同体互动，这一过程既加深理解，也提炼出可迁移的解题策略，并让新知识进入实际应用。AI 模型解题的流程通常是先生成自然语言解释，再尝试用 Lean 语言表达，理论上 Lean 编译通过即可确认证明正确。但剑桥大学与伦敦国王学院的论文指出，模型在自然语言到代码的转换中可能出现「误译」，这直接动摇了「模型可自行形式化其解答而无需人类介入」的假设。这意味着，如果前沿实验室继续以专有模型产出数学成果、又不提供足够的可核查信息，数学界将难以像对待人类成果那样对其进行同行评审，成果的实际价值与可信度都会打折扣。
本文由 AI 辅助整理自公开信源，事实部分以原文为准；「本站视角」一节为编辑部判断，欢迎指正。版权归原作者所有，如有异议请联系我们。