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