О проблеме тысячелетия Навье — Стокса

Читать научную работуСсылка на формализованное доказательство в Lean

Мы представляем решение проблемы существования и гладкости решений уравнений Навье — Стокса, которая является одной из Проблем тысячелетия. Данное доказательство, полученное внутренней системой OpenAI, показывает, что динамика уравнений Навье — Стокса для движения жидкости может приводить к образованию сингулярности за конечное время. Мы публикуем как текст самого доказательства, так и его формализацию на языке Lean.

Проблемы тысячелетия представляют собой одни из самых глубоких вопросов на переднем крае математики. Вопрос о том, может ли плавное трехмерное движение жидкости разрушаться, оставался нерешенным на протяжении примерно 90 лет.

Главная цель нашей работы — дать ученым возможность развивать исследования и технологии на благо всего человечества. Для решения проблемы Навье — Стокса мы использовали внутреннюю модель, которая значительно превосходит по своим возможностям GPT-6 Astra. Мы считаем важным информировать общественность о темпах прогресса в области искусственного интеллекта и о том, чего ожидать от будущих моделей.

Проблема

В уравнениях Навье — Стокса используется второй закон движения Ньютона («F=ma») для описания того, как движутся жидкости. Важно отметить, что они рассматривают жидкость как сплошную среду, а не отслеживают отдельные молекулы. Эти уравнения применяются при проектировании самолетов, прогнозировании погоды и изучении кровотока.

Фундаментальным нерешенным вопросом для этих динамических уравнений оставалось то, может ли континуальное приближение жидкости нарушаться. В частности, могут ли уравнения Навье — Стокса для трехмерной несжимаемой жидкости постоянной плотности развивать «сингулярность», даже если движение начинается плавно? Под сингулярностью здесь понимается ситуация, когда динамика приводит к тому, что скорость жидкости возрастает до бесконечности за конечный промежуток времени. Появление сингулярности должно было бы происходить вопреки наличию вязкости, которая обычно сглаживает движение. Поскольку реальная жидкость не может двигаться с бесконечной скоростью, это означало бы крах применимости уравнений в качестве модели жидкости. Чтобы продолжать моделирование системы, в таком случае потребовалось бы отслеживать поведение каждой отдельной частицы.

Эти уравнения восходят к работам Клода-Луи Навье и Джорджа Габриэля Стокса девятнадцатого века. В 1934 году Жан Лере доказал существование решений в обобщенном смысле, однако вопрос о том, всегда ли они остаются гладкими, оставался центральной нерешенной задачей. В 2000 году Математический институт Клэя назвал проблему существования и гладкости решений уравнений Навье — Стокса одной из семи Проблем тысячелетия.

Результат

Наша система создала аналитическое доказательство и его формализацию в Lean того, что изначально гладкая неподвижная жидкость может за конечное время развить сингулярность. К жидкости приложена плавная сила, а ее энергия остается конечной на протяжении всей динамики — от состояния покоя до формирования сингулярности. Это разрешает проблему тысячелетия Навье — Стокса, устанавливая утверждение «C» (а также «D») в официальной формулировке Проблемы тысячелетия.

Решение представляет собой вихрь — вращающийся поток жидкости, который закручивается по спирали внутрь и все сильнее вытягивается, напоминая спагетти. Эта центральная область сжимается, одновременно ускоряясь таким образом, что ее энергия все же остается конечной, как того требуют законы физики. Техническая сложность заключается в том, чтобы разрыв в уравнениях развился за счет движения самой жидкости, а не, например, в результате того, что мы вручную приложим бесконечную силу. Говоря более математически, члены в уравнениях Навье — Стокса, описывающие движение (ускорение, градиенты давления, перенос импульса, вязкость), должны стать большими, но при этом компенсировать друг друга определенным образом. Этот тонкий баланс сохраняет внешнюю силу гладкой даже тогда, когда скорость жидкости растет до бесконечности.

Diagram of a swirling vortex illustrating inward spiral and axial stretching.

Срез локального несжимаемого движения. Оранжевым цветом отмечено более быстрое угловое вращение, бирюзовым — более медленное. Скорость циркуляции также зависит от радиуса. Траектории показывают спиралевидное движение внутрь и аксиальное растяжение.

Как мы нашли доказательство

С 28 августа мы обучаем новую внутреннюю модель, которая продемонстрировала беспрецедентную производительность в наших бенчмарках, в том числе в области математики. Обучение этой модели продолжается, и ее показатели продолжают улучшаться.

Во вторник, 1 сентября, до нас дошли слухи о том, что две Проблемы тысячелетия были решены. Вдохновленные этими слухами и качественным скачком в производительности нашей внутренней модели, мы предприняли попытку оценить ее возможности на всех нерешенных Проблемах тысячелетия и нескольких других задачах высокой важности.

Мы использовали систему координируемых агентов, работающих на базе нашей внутренней модели. У агентов был доступ к таким инструментам, как чтение кэшированной версии интернета и выполнение кода. Агенты были разделены на группы с возможностью общения внутри группы. Группы варьировались по размеру, а в группе, получившей решение уравнения Навье — Стокса, участвовало порядка 10 000 одновременно работающих агентов. Мы неизменно соблюдали те же строгие меры безопасности, которые применяются при оценке всех наших передовых моделей, включая мониторинг и изоляцию.

Для каждой задачи мы давали разным группам агентов различные формулировки условия, охватывающие все возможные варианты постановки проблемы. Для задачи Навье — Стокса мы предложили версиям «A» и «B» (частные формы проблемы Навье — Стокса, которые привели бы к доказательству) и версиям «C» и «D» (которые привели бы к опровержению) разным группам агентов.

Помимо полных Проблем тысячелетия, мы попробовали задействовать нашу многоагентную систему для решения набора «более простых» задач. Одной из них стал аналогичный вопрос об образовании каспа (взрыве) для предельного случая уравнений Навье — Стокса с удаленным членом вязкости. Эта задача известна как проблема регулярности уравнений Эйлера, и наши агенты удивили нас, разрешив ее. Конкретным вариантом вопроса, который они разрешили, стала несиловая версия (unforced), в которой к жидкости не прикладывается внешняя сила. Около 100 агентов работали совместно в течение примерно 50 часов, чтобы получить наше опровержение регулярности Эйлера.1

Увидев решение для уравнений Эйлера, мы решили, что задача Навье — Стокса является наиболее перспективным направлением для работы. Таким образом, мы решили направить все наши ресурсы на Навье — Стокса. Для этого мы перевели агентов с других Проблем тысячелетия и передали им решение для Эйлера в качестве отправной точки. Когда в ходе работы стала доступна дообученная версия нашей внутренней модели, мы перевели наших агентов на нее.

Мы поощряли разные группы агентов исследовать самые разнообразные подходы. Спустя некоторое время мы провели перекрестное опыление групп агентов, используя Codex для консолидации наиболее полезных идей из каждой группы. Эти последующие запросы опирались на промежуточные результаты самих агентов. Именно так была направлена группа, нашедшая решение задачи Навье — Стокса.

Агенты пришли к своему решению в субботу, 5 сентября, примерно через 88 часов после запуска первых агентов. Формализация и верификация в Lean заняли дополнительные 17 часов с использованием GPT-6 Astra.

В общей сложности по всем испытанным задачам агенты отправили 4,9 миллиона сообщений и израсходовали около 300 миллиардов токенов вывода. В процессе решения проблемы Навье — Стокса агенты отправили 2,7 миллиона сообщений и использовали примерно 130 миллиардов токенов вывода.

Параллельные исследования

Наша работа началась 1 сентября после того, как мы услышали слух, который, как мы позже поняли, был связан с Левентом Алпёдже (сотрудником Anthropic) и Тристаном Бакмастером (профессором математики в Нью-Йоркском университете). После завершения нашего полного проекта и верификации в Lean (6 сентября), полагая на основании слухов, что у них также есть решение задачи Навье — Стокса, мы связались с ними, чтобы предложить одновременный выпуск нашего результата и выразить признание их приоритета в совместном анонсе. В тот момент мы выяснили, что у них было решение силовой задачи Эйлера (forced Euler). В ходе этих обсуждений мы предоставили им доступ ко всем промптам, которые мы использовали, а позже показали и само доказательство. Мы признаем приоритет их работы по силовой задаче Эйлера и поздравляем их с этим выдающимся математическим достижением.

Мы (исследователи и агенты) никоим образом не видели их работу до тех пор, пока они не опубликовали ее официально; в частности, для решения этой проблемы не использовались никакие конфиденциальные пользовательские данные. Хотя это маловероятно, мы не можем полностью исключить, что деанонимизированные данные, полученные в результате использования ими наших продуктов, помогли улучшить наши модели. Тем не менее, наши доказательства существенно различаются, и даже точные доказанные результаты в случае Эйлера отличаются (силовой и несиловой варианты).

Прогресс и ответственность

Наша цель при публикации этого результата — рассказать о существенном прогрессе наших ИИ-моделей. Мы не претендуем на получение Премии тысячелетия за этот результат.

Этот рубеж представляет собой результат масштабной работы математиков и исследователей в области искусственного интеллекта. Тем не менее, это не кульминация, а лишь срез прогресса в разработке ИИ на определенный момент времени.

Мы считаем, что сейчас мы вступили в новый период прогресса ИИ, и сегодняшние результаты служат тому дополнительным подтверждением. Мы сосредоточены на понимании этой модели и использовании полученных знаний для того, чтобы направлять и регулировать темпы дальнейшего наращивания ее возможностей. Одна из наших ключевых целей — создание систем искусственного интеллекта, которыми можно управлять, которые подотчетны и связаны с людьми. Это может потребовать более взвешенных решений в отношении темпов прогресса по мере продолжения нашей миссии по обеспечению того, чтобы общий искусственный интеллект (AGI) приносил пользу всему человечеству.

Автор

OpenAI

Сноски

  1. 1

    Читать документ с доказательством для уравнений Эйлера · Ссылка на формализованное доказательство в Lean

Полный текст статьи читайте на OpenAI