- 10月6日，OpenAI将719篇来自未发布内部模型的数学手稿上传至GitHub。
- 其咨询小组曾于9月29日要求各实验室停止在专有模型上测试高级数学问题。
- 一篇论文指出，OpenAI 用于纳维-斯托克斯方程证明的 Lean 代码所证明的命题弱于其书面版本。
10 月 6 日，OpenAI 将来自一个未发布内部模型的 719 篇数学论文推送至 GitHub。
一周前，其自身的顾问小组曾要求各实验室停止在专有模型上测试高级数学问题。
超过 600 份调查回复塑造了 IAS 小组 9 月 29 日的指导方针
数学与人工智能咨询小组位于新泽西州普林斯顿高等研究院。9月29日，该小组发布了建议，这些建议基于超过600份调查回复。
“我们想从一开始就明确声明：我们不认可这种做法，并要求他们停止在专有模型上测试高级数学问题，”该小组写道。
同一份文件警告称，私有内部模型可能导致一种两级体系，使某些实验室跑在领域其他参与者前面。
OpenAI 在其存储库中表示，作为模型开发的一部分，该公司会在开放研究问题上测试其模型。在其现有数学基准饱和后，它扩展了这些测试。
OpenAI 表示其与小组进行了协商，并借鉴了其关于发布的建议。该小组在 10 月 6 日发布的声明中表示，其顾问角色并非“对 OpenAI 获取这些论文的过程的认可”。
该小组将合规性的裁决权委托给更广泛的数学界。
Navier-Stokes Lean 代码所证明的结论弱于论文中的表述
OpenAI 将 719 篇论文归类为 372 个数学家族，每个家族围绕一个主要结果及其相关证明构建。该公司向专有模型提供了约 4,000 个问题，平均每个结果需要 ChatGPT Pro 约三小时的推理计算时间。
该团队要求 AI 实验室公布每个结果所使用的模型名称、提示词、简化的思维链、耗时以及计算成本。
OpenAI 发布了 10 份推理摘要，其中约 42% 的主要结果附带了 Lean 形式化验证。
Lean 是一种可用于由计算机检查证明过程的编程语言。如果代码编译成功，并不意味着代码与书面论证完全一致；它仅表明形式化陈述是正确的。
亚历山大·巴斯图尼斯、法比安·奇尔切利和安德斯·C·汉森在10月6日发布的一篇论文中考察了这一差距。他们发现，OpenAI的书面纳维-斯托克斯论文所做出的主张，比其Lean代码所证明的要强，且其中一个估计改变了输入导数的阶数。
作者们在 OpenAI 的欧拉（Euler）证明中也发现了类似的误译现象。他们在文中写道：“OpenAI 的书面证明及其他自动形式化的 Lean 证明，不应像其他证明那样，在未经同等同行评审和严格审查的情况下被轻易信任。”
纳维-斯托克斯结果由OpenAI于9月8日宣布。据Cryptopolitan报道，纽约大学数学家特里斯坦·巴克马斯特随后质疑了该工作所涉及的最小人类投入的描述。
该公司承诺为重大 AI 成果相关的研讨会、会议和特别项目提供资金支持。
10月6日，陶哲轩写道，AI提示词工程师往往在解决问题后就对该领域失去兴趣。他写道，许多人无法回答关于该成果的问题或就此发表演讲。他的帖子并未点名OpenAI。
该公司表示，其顾问对其研究进度没有发言权，Cryptopolitan于9月对此进行了报道。
最聪明的加密领域人士已经在阅读我们的通讯。想加入吗？加入他们。
常见问题
OpenAI在6年2026月发布了什么？
来自一个未发布内部模型的719篇数学手稿，其中约42%的主要结果附有Lean形式化验证。
咨询小组要求OpenAI做什么？
停止在专有模型上测试高级数学问题，并公布每项结果的提示词和简化的思维链。
数学家为何对纳维-斯托克斯方程的证明感到担忧？
一篇论文发现，OpenAI的Lean代码所证明的命题弱于其书面证明，并且在某项估计中改变了导数的阶数。
免责声明。 所提供的信息不构成交易建议。Cryptopolitan.com 对基于本页信息进行的任何投资不承担任何责任。我们强烈建议在做出任何投资决策之前进行独立研究或咨询合格的专业人士。
Randa Moses
Randa Moses 是 Cryptopolitan 的编辑兼记者，专注于科技、人工智能、机器人技术、加密货币、诈骗及黑客攻击等领域的报道。自 2017 年以来，她一直活跃于加密货币领域，曾担任 Forward Protocol、AmaZix 和 Cryptosomniac 等公司的职务。Randa 拥有布拉德福德大学电气工程与电子工程学位。
