Математики не подтвердили, что OpenAI украла подход к уравнениям Навье–Стокса

Доказательство для уравнений Навье–Стокса, представленное OpenAI в сентябре, по мнению нескольких групп математиков, не повторяет метод исследователей, обвинивших компанию в использовании их идей. Эксперты около месяца изучали 166-страничный текст и пришли к выводу, что при детальном рассмотрении подходы различаются.

‹›

«Когда доходишь до деталей, это другой подход», — сказал математик Гонсало Као-Лабора из Лозанны. Речь идет об одной из семи «проблем тысячелетия», сформулированных Институтом Клэя. OpenAI заявила о доказательстве вариантов C и D: в построенном примере гладкая жидкость, находящаяся в покое, под воздействием гладкой внешней силы за конечное время достигает бесконечной скорости, при этом ее энергия остается конечной.

8 сентября OpenAI сообщила, что задачу решила внутренняя система из 10 000 агентов. За 88 часов они построили пример, в котором скорость жидкости стремится к бесконечности, а еще 17 часов заняла формальная проверка в системе Lean. Текст доказательства и код проверки позже открыли для изучения.

Расхождения между текстом и формальной проверкой

Почти одновременно с анонсом профессор Нью-Йоркского университета Тристан Бакмастер, специалист по уравнениям жидкости, обвинил OpenAI в том, что компания использовала маршрут из его совместной работы с Левентом Альпеге, штатным математиком Anthropic. Институт Клэя заявил, что проблема, по-видимому, решена, но отказался от поспешной окончательной оценки.

В октябре Александр Бастунис, Фабиан Чирчелли и Андерс Хансен сравнили текст OpenAI с его версией в Lean. Они обнаружили расхождения между формулировками и тем, что действительно проверяет код. Например, в одном месте статья обещает оценку с четырьмя дополнительными производными, тогда как Lean требует пяти. В результате формально подтвержденное утверждение оказывается слабее написанного в тексте. В другом фрагменте меняются условия и структура оценки.

Исследователи отдельно подчеркнули, что не утверждают ошибочность словесного доказательства. Их вывод касается пределов формальной проверки: Lean-код подтверждает не все утверждения, содержащиеся в статье. Подобные трудности уже возникали в математике. Доказательство теоремы о четырех красках, опубликованное в 1976 году, опиралось на масштабный компьютерный перебор случаев. Из-за сложности независимой проверки вокруг него возникли споры, а в 1997 году появилось более простое компьютерное доказательство.

Испанская программа и новый маршрут

Оставался и более общий вопрос: действительно ли OpenAI использовала тот же путь, что Бакмастер и Альпеге. Изначально многие предполагали, что модель довела до конца так называемую «испанскую программу» — подход, предложенный Диего Кордобой и Луисом Мартинесом-Сороа. Бакмастер и Альпеге почти год работали в этом направлении с помощью Codex от OpenAI.

Именно это стало основанием для обвинений. Бакмастер предположил, что OpenAI могла получить доступ к их диалогам с моделью, использовать найденное решение и завершить работу быстрее благодаря 10 000 параллельно действовавшим агентам. Однако математики, опрошенные Scientific American, считают, что испанская программа была скорее отправной точкой. С ее помощью удалось решить задачу для уравнений Эйлера, которую рассматривали как промежуточный шаг к уравнениям Навье–Стокса.

Дальше, по мнению экспертов, OpenAI пошла другим путем. Общее между подходами сводится главным образом к особенности формулировки задачи Клэя: в рассматриваемую систему разрешено добавить внешнюю силу, и ключевой вопрос заключается в ее построении. Испанская программа создает силу последовательными слоями, переходя от одного масштаба к другому.

В решении OpenAI центральную роль играет вихрь, который закручивается внутрь и вытягивается вдоль оси, напоминая «спагетти». Недостающую энергию, согласно описанию компании, дают короткие импульсы. Они раскручиваются, забирают энергию у окружающего потока и исчезают, когда их поглощает вязкость.

За два дня до объявления OpenAI Бакмастер по переданным ему деталям решил, что компания использовала именно его маршрут. На тот момент OpenAI уже проверила текст в Lean, но, как утверждается, люди не успели изучить само доказательство: его написала модель, а на анализ оставалось около трех дней. Позднее различия между двумя подходами ослабили аргумент о прямом совпадении, но не сняли вопрос о происхождении идеи.

Что остается нерешенным

Бакмастер и сейчас настаивает, что модель следовала его методу. OpenAI заявляет, что работа Бакмастера и Альпеге не была доступна ее исследователям и агентам до публикации, а запросы Бакмастера к Codex за предыдущие два месяца не могли повлиять на систему, в том числе через обучение.

Камилло Де Леллис из Института перспективных исследований в Принстоне считает, что окончательно разрешить спор может быть невозможно: он касается не только проверяемых математических фактов, но и происхождения исследовательского маршрута.

Кроме того, результат OpenAI не дает автоматического перехода к варианту A задачи Клэя — формулировке без внешней силы. В сентябре Питер Константин, Михаэла Игнатова и Влад Виколь показали, что из конструкции OpenAI нельзя просто удалить внешнее воздействие, сохранив основные свойства решения. Для рассматриваемого устройства они доказали, что сила не может тождественно исчезать вблизи предполагаемой сингулярности.

Таким образом, Институт Клэя еще должен завершить оценку результата, а вопрос о возникновении сингулярности в жидкости без внешнего воздействия остается открытым. Главная проблема, по мнению экспертов, связана не только с корректностью отдельных формул. Модель смогла построить сложную конструкцию и формально проверить ее часть, но не объяснила метод так, чтобы его быстро и уверенно поняли независимые специалисты. Пока математики восстанавливают понятное изложение доказательства, спор о приоритете продолжается.