На протяжении почти двух веков математическое сообщество пытается разгадать уравнения Навье — Стокса, описывающие механику движения газов и жидкостей. С момента их появления в работах Анри Навье (1822 год) и Джорджа Стокса (1829 год) ученые ищут ответ на фундаментальный вопрос: всегда ли в трехмерном евклидовом пространстве эти уравнения при определенных начальных условиях дают единственное гладкое решение с конечной энергией. Сегодня на передовой этой интеллектуальной битвы встали не только люди, но и колоссальные вычислительные мощности.
Как удалось организовать этот процесс, пояснил Максим Абрамов, возглавляющий лабораторию приключеского искусственного интеллекта в СПб ФИЦ РАН, в беседе с изданием «Наука Mail». Для преодоления сложнейшего барьера была задействована целая экосистема, состоящая примерно из 10 тысяч ИИ-агентов. Процесс был организован не как монолитное вычисление, а как масштабная научная дискуссия.
Структура работы напоминала работу исследовательского семинара. Агенты были разделены на несколько групп, каждая из которых преследовала противоположные цели: одни пытались найти подтверждение корректности уравнений, другие — опровергнуть их. Внутри этих подгрупп происходил непрерывный обмен идеями, а специальная управляющая модель выступала в роли модератора: она анализировала наработки всех участников, синтезировала общие выводы и возвращала их в систему в виде уточняющих инструкций. По словам Абрамова, такой подход был критически важен — без постоянного стимулирования разнообразия мнений агенты рисковали закостенеть в единой логической колее и перестали бы генерировать нестандартные пути решения.
Подготовка к основному этапу также требовала поэтапного подхода. Сначала разработчики использовали метод прогрессивного усложнения: небольшая группа из 100 агентов в течение 50 часов решала более простую, но связанную с основной проблемой задачу. Накопленный опыт стал фундаментом для финального рывка.
Сам процесс поиска ответа в основной фазе длился около 88 часов. Однако последующая работа оказалась не менее трудоемкой: еще 17 часов потребовалось для того, чтобы перевести полученные результаты на строгий формальный язык Lean. Необходимость в этом была продиентирована колоссальным объемом данных — за время работы агенты обменялись примерно 2,7 миллионами сообщений. Проверить такую гигантскую цепочку рассуждений человеческими силами практически невозможно, поэтому именно Lean позволил верифицировать каждый логический переход, эффективно отсеяв массив ошибок и промежуточных гипотез от чистого доказательства.
Напомним, что уравнения Навье — Стокса входят в список так называемых «задач тысячелетия» (Millennium Prize Problems). Этот перечень из семи сложнейших проблем был официально обнародован Математическим институтом Клэя (CMI) в Кембридже, США, 24 мая 2000 года на заседании в Коллеж де Франс в Париже. За успешное решение каждой из этих задач институт обещает награду в размере 1 миллиона долларов.
На сегодняшний день в этом списке удалось закрыть лишь одну позицию. Речь идет о гипотезе Пуанкаре, касающейся топологических свойств трехмерных многообразий. Ее доказательство представил российский математик Григорий Перельман. В 2010 году институт официально признал его работу, хотя сам ученый от положенной премии отказался.
