OpenAI 发布内部前沿模型产出的数学研究成果
Sharing AI progress in mathematics
OpenAI 发布一批由内部前沿模型产出的新数学成果,成果以 GitHub 仓库形式公开,并附论文修订与引用协议,其中许多证明已用 Lean 形式化以便计算机验证。
原文说明了成果发布方式、Lean 形式化和计算开销等细节,读者可以了解 AI 数学成果如何面向数学社区开放。
分享数学领域的 AI 进展
分享
我们正在发布由内部前沿模型产出的一系列广泛的数学新成果。
为了改进我们与数学界分享成果的方式,我们一直在与独立的高等研究院数学与人工智能咨询小组(在新窗口中打开)磋商以制定最佳实践,并借鉴了他们的建议和公开建议(在新窗口中打开)来指导我们发布这些成果的方式。
对于本次发布,我们将成果发布在一个 GitHub 仓库中,并附有论文修订和引用的规范。我们也在继续探索其他符合委员会指南、由社区托管的替代方案用于本次发布。对于未来的发布,我们致力于通过引用、数学阐述和成果呈现方式进一步提升论文质量,以便更好地理解。
作为我们 GitHub 仓库的一部分,我们分享了其中许多证明在 Lean 中的形式化,Lean 是一种允许计算机检查数学证明的编程语言。随着我们获得更多形式化,我们将更新该仓库。
为了促进科学透明度和开放性,我们还在仓库中发布了关于我们如何获得这些成果的更多细节。其中包括 10 份模型推理摘要、以 ChatGPT 上 Pro 使用量估算的算力消耗,以及关于尝试问题数量的统计数据。平均每项成果使用的算力约相当于 ChatGPT Pro 思考三个小时。
我们希望这一进展能够推动人类知识的前沿,并促进数学的进一步发展。我们将资助一系列围绕理解 AI 产出的重大成果的研讨会、会议和特别项目——我们将在不久的将来分享更多相关信息。
我们希望直接以最先进的能力赋能科学家,并正在努力以负责任的方式发布产出这些成果的模型。这就是为什么继续在数学和其他科学领域评估我们的内部前沿模型很重要,这样我们才能加速开发推动这些领域进步的工具。我们将继续根据社区的反馈采取行动,并更新我们对未来重大科学进展披露的标准。
作者
OpenAI
来源:OpenAI:官网动态 · openai.com