Компания OpenAI опубликовала отчет, в котором утверждает, что невыпущенная модель искусственного интеллекта справилась с одной из «задач тысячелетия» — проблемой существования и гладкости решений уравнений Навье-Стокса. Этот математический вопрос входит в список семи премий Clay Mathematics Institute, установленных в 2000 году, где за каждое решение предусмотрено вознаграждение в 1 миллион долларов. На данный момент из семи задач решена только гипотеза Пуанкаре.
Масштабный вычислительный эксперимент и методология
По данным OpenAI, для достижения результата система задействовала до 10 000 ИИ-агентов, координирующих свои действия. Весь процесс занял 88 часов. В результате была создана формальная математическая проверка на языке Lean, который позволяет подтвердить логическую корректность каждого этапа доказательства. Использование этого языка помогает избежать проблемы «убедительных, но ошибочных» рассуждений, характерных для обычных текстовых генеративных моделей.
Исследователь OpenAI Дэн Робертс сравнил процесс координации агентов с работой шмеля-опылителя, который переносит полезные идеи между разными группами, ищущими решения по разным направлениям. Научный сотрудник компании Ноам Браун признал, что проект потребовал значительных вычислительных мощностей, стоимость которых исчисляется миллионами долларов, однако выразил уверенность в снижении затрат по мере совершенствования инфраструктуры.
Суть уравнений Навье-Стокса и проверка доказательства
Уравнения Навье-Стокса описывают поведение жидкостей и газов и широко применяются в аэродинамике и метеорологии. Математическая проблема заключается в вопросе: всегда ли уравнения дают плавные решения в трехмерном пространстве или при определенных условиях в модели возникает «сингулярность» — точка, где расчеты перестают работать. В OpenAI заявляют, что их доказательство подтверждает наличие такого разрушения модели. При этом компания подчеркивает, что это касается лишь теоретических пределов уравнений как системы, а не предсказания того, что жидкости начнут нарушать законы физики в реальности.
Теперь представленный отчет направлен на рецензирование внешним математикам. Если экспертное сообщество подтвердит корректность доказательства, это станет важным аргументом в пользу того, что ИИ способен решать сложнейшие открытые математические задачи, а не просто имитировать человеческие рассуждения.
Развитие ИИ в математике и экспертное мнение
Данный проект отражает тенденцию обучения нейросетей на задачах с четкими критериями «пройдено-провалено», где результат поддается объективной проверке, как в коде или математическом доказательстве. Это позволяет системам обучения с подкреплением прогрессировать через серию ошибок и исправлений. Ранее, в январе, OpenAI и компания Harmonic уже заявляли о решении одной из проблем Эрдёша, хотя тогда некоторые математики сомневались, является ли предложенный ИИ подход принципиально новым.
Научное сообщество с осторожностью относится к подобным достижениям. Профессор Калифорнийского университета в Лос-Анджелесе Теренс Тао ранее выражал опасения, что передача решения крупных математических задач машинам может ослабить саму дисциплину. По его словам, процесс самостоятельного поиска решения человеком несет высокую образовательную ценность, которой можно лишиться при полной автоматизации процесса.
Контекст и независимость исследования
Важно отметить, что OpenAI обратилась к решению этой сложной задачи после того, как узнала о похожих исследованиях, проводимых сторонними группами. Компания подчеркивает, что не знакомилась с их наработками ни по каким каналам. Это заявление прозвучало на фоне того, что Тристан Бакмастер, профессор математики из Нью-Йоркского университета, незадолго до анонса сообщил, что сам занимается изучением схожих вопросов совместно с математиком, работающим в Anthropic — прямом конкуренте OpenAI.
Особенности методологии Lean
Язык Lean играет критическую роль в данном проекте. В отличие от стандартных методов генерации текста, где модель может выдать внешне правдоподобное, но логически несостоятельное решение, Lean служит инструментом формальной верификации. Он не оценивает научную значимость или новизну результата, однако гарантирует, что каждый логический шаг строго соответствует установленным правилам системы. Именно такой подход к обучению на задачах с жесткими критериями «пройдено-провалено» становится новым стандартом для систем с обучением с подкреплением, позволяя им эффективно развиваться через итеративный процесс выявления ошибок и внесения корректив.
