Российский ученый объяснил, как ИИ-агенты решили задачу Навье — Стокса

Для того, чтобы найти решить «задачу тысячелетия» — решение уравнений Навье — Стокса, потребовались усилия около 10 тыс. ИИ-агентов, которые в разных группах одновременно искали разные подходы к проблеме. Как именно была решена задача, рассказал руководитель лаборатории прикладного искусственного интеллекта СПб ФИЦ РАН Максим Абрамов в разговоре с Наука Mail.

Уравнения Навье — Стокса описывают движение жидкостей и газов. Уравнения были сформулированы французским физиком Анри Навье и британским математиком Джорджем Стоксом в 1822 и 1829 годах соответственно. С тех пор ученые пытались доказать или опровергнуть, что уравнения гидродинамики в трехмерном евклидовом пространстве всегда имеют единственное гладкое решение с конечной энергией при любых «быстро затухающих» начальных условиях.

Для того, чтобы решить задачу, одна группа ИИ-агентов пыталась прийти к доказательству верности уравнений, другие двигались в направлении их опровержения. «По сути своей это похоже на научный семинар: внутри групп агенты обменивались друг с другом идеями, а отдельная модель собирала результаты всех групп, обобщала их и отправляла обратно в виде новых подсказок», — объяснил Абрамов. Все это позволяло системе одновременно сохранять несколько конкурирующих направлений поиска решения. «Без такого механизма агенты быстро пришли бы к одному и тому же способу рассуждения и перестали бы находить новые пути», — объяснил эксперт.

Кроме тог, использовался метод постепенного усложнения. Сначала систему натренировали на более простой связанной задаче — около 100 агентов работали над ней примерно 50 часов, после чего накопленные результаты использовали для основной.

Основной поиск решения занял около 88 часов, а затем ещё примерно 17 часов ушло на перевод доказательства в формальный язык Lean. Это было необходимо, потому что агенты обменялись около 2,7 млн сообщений: вручную проверить такую цепочку рассуждений почти невозможно. Lean помог проверить каждый логический шаг и отделить собственно доказательство от огромного массива черновых гипотез и ошибок поиска.

«Задачи тысячелетия» (Millennium Prize Problems) — это семь ключевых нерешенных математических проблем, за доказательство или опровержение каждой из которых Математический институт Клэя (Clay Mathematics Institute, CMI) в Кембридже (США) назначил премию $1 млн. Список был представлен 24 мая 2000 года на заседании в Коллеж де Франс в Париже.

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