OpenAI 宣布以内部 AI 系统给出 Navier-Stokes 千禧年问题解答

OpenAI 自述用内部模型与上万智能体给出 Navier–Stokes 奇点证明和 Lean 形式化，还交代了欧拉方程副产物与协作细节。

OpenAI 宣布其内部 AI 系统给出 Navier–Stokes 存在与光滑性问题的解答，证明初始光滑的流体可在有限时间内形成奇点，并附证明文稿与 Lean 形式化验证。

我们正在分享一个关于纳维-斯托克斯存在性与光滑性问题的解决方案，这是千禧年大奖难题之一。这一证明由 OpenAI 内部系统生成，表明流体运动的纳维-斯托克斯方程动力学可以在有限时间内产生奇点。我们将同时分享证明的书面说明以及 Lean 中的形式化版本。

千禧年大奖难题⁠ 代表了数学前沿最深奥的问题之一。光滑三维流体运动是否会破裂这一问题，至今已悬而未决约 90 年。

我们工作的一个主要目标是赋能科学家，推动惠及全人类的研究与技术发展。为解决纳维-斯托克斯问题，我们使用了一个内部模型，其能力显著强于 GPT‑6 Astra。我们认为，让世界了解 AI 进步的节奏以及即将推出的模型值得期待之处，这一点非常重要。

纳维-斯托克斯方程运用牛顿第二运动定律（“F=ma”）来描述流体如何运动。重要的是，它们将流体视为连续介质，而非追踪单个分子。这些方程被用于飞行器设计、天气预报以及血流研究。

这些动力学方程的一个基本开放问题是，流体的连续介质近似是否可能失效。具体而言，对于密度恒定的三维不可压缩流体，纳维-斯托克斯方程是否会在运动初始光滑的情况下发展出“奇点”？这里的奇点意味着，动力学导致流体中的速度在有限时间内无界增长。奇点的发展必须在存在黏性的情况下发生，而黏性本身倾向于使运动趋于平滑。由于真实流体不可能以无限速度运动，这将标志着方程对流体的建模出现失效。为了继续对该系统进行建模，人们就需要逐一追踪每个粒子的行为。

这些方程源自十九世纪克劳德-路易·纳维和乔治·加布里埃尔·斯托克斯的研究。1934年，让·勒雷证明了方程在广义意义下存在解，但这些解是否始终保持光滑，成为悬而未决的核心问题。2000年，克莱数学研究所将纳维-斯托克斯方程的存在性与光滑性问题列为七大千禧年大奖难题之一。

我们的系统产出了一份分析性证明和一份 Lean 形式化验证，证明一个初始光滑的静止流体可以在有限时间内形成奇点。该流体受到一个光滑的外力作用，其能量在整个动力学过程中始终保持有限，从静止状态一直到奇点形成。这通过确立 官方千禧年大奖问题表述⁠ 中的陈述“C”（以及“D”），解决了纳维-斯托克斯千禧年大奖问题。

解决方案是一个涡旋——一种旋转的流体涡流，它向内盘旋并不断被拉长，形似意大利面。这个中心区域在收缩的同时加速旋转，其能量仍然保持有限，符合物理定律的要求。技术难点在于，要让方程组通过流体自身的运动发展出这种破裂，而不是例如我们人为地施加一个无限大的力。从数学角度更准确地说，描述运动的纳维-斯托克斯方程各项——加速度、压力梯度、动量传递、黏性——必须同时变得巨大又以精确的方式相互抵消。这种精细的平衡使得即使流体速度无界增长，外部力仍然保持平滑。

局部不可压缩运动的快照。橙色表示更快的角旋转；青色表示较慢的旋转。环流速度还取决于半径。轨迹显示了向内螺旋和轴向拉伸。

自 8 月 28 日以来，我们一直在训练一个新的内部模型，该模型在我们的基准测试中展现出前所未有的表现，包括数学领域。该模型的训练仍在进行中，其性能持续提升。

在 9 月 1 日（星期二），我们听到传言称有两个千禧年大奖难题已被解决。受这些传言以及我们内部模型性能的阶跃式提升所启发，我们启动了一项工作，在所有未解决的千禧年大奖难题以及其他几个高影响力问题上对该模型进行评估。

我们使用了一套由内部模型驱动的协调智能体系统。这些智能体能够访问多种工具，例如读取互联网缓存版本以及运行代码。智能体被划分为多个小组，小组内部可以进行通信。各组规模不一，其中解决纳维-斯托克斯问题的小组涉及约 10,000 个并发智能体。在整个过程中，我们始终维持与所有前沿模型评估相同的严格安全措施，包括监控和隔离。

针对每个问题，我们向不同的智能体小组提示了问题陈述的不同变体，覆盖了该问题的所有变体形式。对于纳维-斯托克斯问题，我们向不同的小组分别提示了版本“A”和“B”（纳维-斯托克斯问题的特定形式，可导向证明）以及版本“C”和“D”（可导向反证）。

除了完整的千禧年大奖难题之外，我们还要求我们的多智能体系统尝试一组“较简单”的问题。其中一个问题是关于去除粘性项后纳维-斯托克斯问题极限的类似爆破问题。这被称为欧拉方程的正则性问题，而我们的智能体解决了这个问题，令我们感到惊讶。它们所解决的具体问题变体是无外力版本，即流体不受任何外力作用。近 100 个智能体协同工作约 50 小时，得出了我们的欧拉正则性反证。1

当我们看到欧拉方程的解之后，我们认为纳维–斯托克斯方程是最值得攻克的问题。因此，我们决定将资源投入到纳维–斯托克斯方程上。为此，我们将智能体从其他千禧年难题上转移过来，并用欧拉方程的解法对这些智能体进行提示。在攻关过程中，当我们内部模型的进一步训练版本可用时，我们便将智能体更新到该模型上。

我们鼓励不同的智能体小组探索多样化的方法。一段时间后，我们通过使用 Codex 整合各智能体小组最有价值的见解，对它们进行了交叉融合。这些后续提示词利用了智能体自身的中间结果。找到纳维–斯托克斯方程解法的那个小组正是以这种方式得到引导的。

智能体于 9 月 5 日（星期六）得出了解法，距首批智能体启动约 88 小时。Lean 形式化与验证又花费了 17 小时，由 GPT‑6 Astra 完成。

在所有尝试过的问题中，智能体共发送了 490 万条消息，使用了约 3000 亿个输出 token。在解决纳维–斯托克斯问题的过程中，智能体发送了 270 万条消息，使用了约 1300 亿个输出 token。

我们的工作始于 9 月 1 日，当时我们听到一则传闻，后来意识到它与 Anthropic 员工 Levent Alpöge 以及纽约大学数学教授 Tristan Buckmaster 有关。在我们完成整个项目并通过 Lean 验证（9 月 6 日）之后，由于我们根据传闻相信他们也得到了 Navier–Stokes 方程的一个解，于是我们联系了他们，提议同时发布我们的结果，并在联合公告中承认他们的优先权。那时我们才发现，他们解决的是受迫 Euler 问题。在这些讨论中，我们让他们查看了我们使用的所有提示词，后来又让他们查看了证明。我们承认他们在受迫 Euler 问题上的优先权，并祝贺他们取得了卓越的数学成就。

我们（研究人员和智能体）在他们公开发布之前，没有通过任何途径看到他们的任何工作——特别是，我们没有访问任何特定用户数据来解决这个问题。虽然可能性不大，但我们无法排除从他们使用我们产品所产生的去标识化数据帮助改进了我们的模型⁠。不过，我们的证明存在显著差异，而且在 Euler 情形下，所证明的精确结果甚至也是不同的（受迫与不受迫）。

我们发布这一结果的目标是报告我们 AI 模型取得的实质性进展。我们不打算就此结果申领千禧年大奖。

这一里程碑凝聚了数学家与 AI 研究者的大量工作。然而，这并非终点，而只是 AI 发展进程中的一个阶段性快照。

我们相信，如今正处于 AI 进步的下一阶段⁠，今天的结果为此提供了进一步佐证。我们正专注于理解这一模型，并利用所学来引导和把握我们追求能力进一步突破的节奏。我们的关键目标之一⁠是构建可控、可问责且与人紧密相连的 AI 系统，这或许要求我们在推进速度上做出更审慎的选择，同时继续践行确保 AGI 惠及全人类的使命。

We’re sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We’re sharing both a writeup of the proof and a formalization in Lean.

The Millennium Prize Problems⁠ represent some of the deepest questions at the frontier of mathematics. The question of whether smooth three-dimensional fluid motion can break down has remained unresolved for roughly 90 years.

A major goal of our work is to empower scientists to advance research and technology that benefits all of humanity. To solve the Navier–Stokes problem, we used an internal model that is significantly more capable than GPT‑6 Astra. We believe it is important to inform the world about the pace of AI progress and what to expect from upcoming models.

The Navier–Stokes equations use Newton’s second law of motion (“F=ma”) to describe how fluids move. Importantly, they treat a fluid as a continuous medium rather than tracking individual molecules. These equations are used for aircraft design, weather forecasting, and the study of blood flow.

A fundamental open question for these dynamical equations has been whether the continuum approximation of the fluid can break down. Specifically, can the Navier–Stokes equations for a three-dimensional incompressible fluid with constant density develop a “singularity,” even when the motion starts smoothly? Here, a singularity means the dynamics lead to speeds in the fluid growing without bound within a finite amount of time. The development of a singularity would have to happen despite the presence of viscosity, which tends to smooth out motion. Because a real fluid cannot move infinitely fast, this would mark a breakdown in how the equations model the fluid. To continue modeling the system, one would then need to track the behaviour of each particle individually.

The equations date to the nineteenth-century work of Claude-Louis Navier and George Gabriel Stokes. In 1934, Jean Leray proved that solutions exist in a generalized sense, but whether they always remain smooth became a central unanswered question. In 2000, the Clay Mathematics Institute named the Navier–Stokes existence and smoothness problem one of seven Millennium Prize Problems.

Our system produced an analytical proof and a Lean formalization that an initially smooth fluid at rest can develop a singularity in a finite time. The fluid has a smooth force applied to it, and its energy remains finite through the entire dynamics, from rest to the formation of the singularity. This resolves the Navier–Stokes Millennium Prize problem by establishing statement “C” (and also “D”) in the official Millennium Prize formulation⁠ .

The solution is a vortex, a spinning swirl of fluid, that spirals inward and gets increasingly elongated, like spaghetti. This central region shrinks while it speeds up in such a way that its energy still stays finite, as required by the laws of physics. The technical challenge is for the equations to develop the breakdown through the motion of the fluid itself, rather than, for example, us putting in an infinite force by hand. More mathematically, the terms in the Navier–Stokes equations that describe the motion—acceleration, pressure gradients, momentum transfer, viscosity—must both become big yet cancel in a precise way. This detailed balance leaves a smooth external force even as the velocity of the fluid grows without bound.

A snapshot of local incompressible motion. Orange marks faster angular rotation; teal marks slower rotation. Circulating speed also depends on radius. The trajectories show inward spiraling and axial stretching.

Since August 28 we have been training a new internal model that has exhibited unprecedented performance in our benchmarks, including mathematics. This model’s training is ongoing and its performance continues to improve.

On Tuesday, September 1, we heard rumors that two Millennium Prize problems had been resolved. Inspired by these rumors and by the step change in performance of our internal model, we launched an effort to evaluate it on all open Millennium Prize problems and a few other high-impact problems.

We used a system of coordinating agents powered by our internal model. The agents had access to tools such as the ability to read from a cached version of the internet and the ability to run code. Agents were subdivided into groups with the ability to communicate within the group. The groups varied in size, and the group that produced the Navier–Stokes resolution involved on the order of 10,000 concurrent agents. At all times we maintained the same strict safeguards that we apply to all our frontier model evaluations, including monitoring and isolation.

For each problem, we prompted different groups of agents with different variants of the problem statement, covering all variants of the problem. For the Navier–Stokes problem, we suggested versions “A” and “B” (particular forms of the Navier–Stokes problem which would result in a proof) and versions “C” and “D” (which would result in a disproof) to separate groups of agents.

In addition to the full Millennium Prize problems, we asked our multiagent system to try a set of “easier” problems. One of these problems was a similar blowup question for the limit of the Navier–Stokes problem with the viscosity term removed. This is known as the regularity problem for the Euler equations, and our agents surprised us by resolving this question. The specific variant of the question that they resolved was the unforced version, where no external force is applied to the fluid. Nearly 100 agents worked together for approximately 50 hours to produce our Euler regularity disproof.1

Once we saw the Euler solution, we thought that Navier–Stokes was the most promising problem to work on. Thus, we decided to devote our resources to Navier–Stokes. To do so, we shifted agents away from the other Millennium Problems and prompted these agents with the Euler resolution. When a further trained version of our internal model became available over the course of the effort, we updated our agents to that model.

We encouraged different groups of agents to explore a diversity of approaches. After some time, we cross-pollinated the agent groups by using Codex to consolidate the most useful insights from each agent group. These follow-up prompts drew on the agents’ own intermediate results. The group that found the solution to Navier–Stokes was guided in such a way.

The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.

Across all attempted problems, the agents sent 4.9 million messages and used about 300 billion output tokens. In the process of resolving the Navier–Stokes problem, the agents sent 2.7 million messages and used approximately 130 billion output tokens.

Our effort began on September 1st after hearing a rumor which we later realized was related to Levent Alpöge, an Anthropic employee, and Tristan Buckmaster, a math professor at NYU. After the completion of our full project and Lean verification (on September 6th), believing from the rumor they also had a solution of Navier–Stokes, we reached out to them to offer a concurrent release of our result and to recognize their priority in a joint announcement. At that point we found out that they had a resolution of the forced Euler problem. In these discussions we offered them visibility into all of the prompts we used and later to see the proof. We recognize the priority of their work on forced Euler and congratulate them on their remarkable mathematical achievement.

We (the researchers and the agents) did not see any of their work through any means until they released it publicly — in particular, no specific user data was accessed in order to solve this problem. While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models⁠. However, our proofs differ significantly and even the precise results proved are different in the Euler case (forced vs unforced).

Our goal in releasing this result is to report on the substantial progress of our AI models. We do not intend to claim the Millennium Prize for this result.

This milestone represents substantial work by mathematicians and AI researchers. However, this is not a culmination, but rather a snapshot in time, of progress on AI development.

We believe we are now in the next period of AI progress⁠, and today’s results provide further evidence of this. We are focusing on understanding this model, and using what we learn to help us guide and pace how we pursue further advances in capability. One of our key goals⁠ is to build AI systems which are steerable, accountable, and connected to people, which may require more deliberate choices about the pace of progress, as we continue our mission to ensure AGI benefits all of humanity.

来源：OpenAI：官网动态（RSS · 排除企业/客户案例）· openai.com