OpenAI 8 сентября представила доказательство для одной из знаменитых Проблем тысячелетия — задачи существования и гладкости решений уравнений Навье-Стокса. Эти уравнения описывают движение жидкостей и газов, а математическая проблема остается открытой около 90 лет.
Окончательного признания результата пока нет: представленное доказательство предстоит оценить математическому сообществу. Однако необычен уже сам способ, которым OpenAI получила результат. Вместо одной модели, последовательно рассуждающей над задачей, компания запустила около 10 тысяч автономных ИИ-агентов.
Тысячи ИИ искали решение одновременно
По словам Максима Абрамова, агентов разделили на группы и поставили перед ними разные варианты одной математической проблемы. Одни группы пытались прийти к доказательству, другие двигались в направлении опровержения.
При этом агенты могли обмениваться идеями внутри групп, а отдельная модель периодически собирала наиболее полезные промежуточные результаты и возвращала их другим участникам системы в качестве новых подсказок.
По сути своей это похоже на научный семинар: внутри групп агенты обменивались друг с другом идеями, а отдельная модель собирала результаты всех групп, обобщала их и отправляла обратно в виде новых подсказок.
Такая архитектура была нужна не только для ускорения перебора вариантов. Она позволяла системе одновременно сохранять несколько конкурирующих направлений поиска.
Сначала ИИ дали задачу попроще
Использовался и принцип постепенного усложнения. Прежде чем переходить непосредственно к основной проблеме, систему проверили на более простой родственной задаче.
По словам Абрамова, около сотни агентов работали над ней примерно 50 часов. Полученный результат затем использовали при работе над основной проблемой.
Итоговый результат появился примерно через 88 часов. Но на этом работа не закончилась: еще около 17 часов потребовалось для формализации доказательства на языке Lean и автоматической проверки.
Зачем понадобился Lean
Формальная проверка особенно важна из-за масштаба работы агентной системы. За время поиска решения агенты обменялись примерно 2,7 млн сообщений.
Проследить вручную всю цепочку их рассуждений практически невозможно. Поэтому результат необходимо было привести к форме, которую можно проверять независимо от огромного массива промежуточных рассуждений.
Именно сочетание массового параллельного поиска и формальной проверки эксперт считает наиболее интересной особенностью эксперимента.
Ранее подобные многоагентные системы было проще применять в областях, где итог автоматически проверяется, например в программировании. В случае с фундаментальной математикой ситуация сложнее: система работала над проблемой, для которой почти столетие не существовало общепринятого решения.
Ранее мы рассказывали, что ученый предложил новую систему оценки знаний в из-за развития ИИ.