Доказательство для уравнений Навье–Стокса, которое модель OpenAI представила в сентябре, не повторяет маршрут математиков, обвинивших компанию в краже идей. К такому выводу пришли несколько групп экспертов, месяц разбиравших 166-страничный текст, пишет Scientific American. “Когда доходишь до деталей, это другой подход”, – говорит математик Гонсало Као-Лабора из Лозанны. Речь об одной из семи математических “проблем тысячелетия”: формулировка задачи допускает четыре исхода, и OpenAI заявила доказательство вариантов C и D. В построенном примере гладкая жидкость из состояния покоя под действием гладкой внешней силы за конечное время разгоняется до бесконечной скорости, а энергия ее при этом остается конечной.
8 сентября OpenAI объявила, что ее внутренняя модель решила задачу: 10 000 агентов за 88 часов построили пример, в котором скорость жидкости уходит в бесконечность, а формальную проверку на Lean сделали еще за 17 часов. Текст доказательства и Lean-код с тех пор открыты. Анонс совпал с заявлением Тристана Бакмастера, профессора Нью-Йоркского университета и одного из ведущих специалистов по уравнениям жидкости: он обвинил компанию в том, что она взяла маршрут из его работы с Левентом Альпеге, штатным математиком Anthropic. Институт Клэя написал, что проблема “по-видимому, решена”, и пообещал не торопиться с оценкой.
В октябре Александр Бастунис, Фабиан Чирчелли и Андерс Хансен сравнили доказательство OpenAI с его Lean-версией и нашли расхождения в аргументах и промежуточных утверждениях. В одном месте текст обещает оценку с четырьмя дополнительными производными, а Lean требует пяти: формально доказанное утверждение слабее написанного. В другом меняются условия и структура оценки. Авторы прямо оговаривают, что не утверждают, будто словесное доказательство неверно. Их вывод касается границ проверки: Lean-код сам по себе не подтверждает все, что написано в статье.
Препринт Бастуниса, Чирчелли и Хансена: Lean-версия доказательства OpenAI не совпадает с его текстом
Математика уже сталкивалась с трудностями проверки компьютерных доказательств. Теорему о четырех красках в 1976 году доказали с помощью масштабного перебора случаев на компьютере. Это вызвало споры о проверяемости результата, а в 1997 году появилось более простое компьютерное доказательство. Независимую проверку затрудняли объем и сложность вычислений.
Собственно, проблема OpenAI куда шире расхождений между текстом и Lean-кодом. Журналист Scientific American связался с несколькими группами математиков, которые месяц читали текст OpenAI: никто из них до сих пор не смог до конца понять, как именно модель решила задачу.
Сначала считалось, что модель довела до конца так называемую “испанскую программу” – подход, предложенный испанскими математиками Диего Кордобой и Луисом Мартинесом-Сороа. Этим же маршрутом почти год шли Бакмастер с Альпеге – и тоже с помощью Codex от OpenAI. Отсюда и обвинение: Бакмастер решил, что OpenAI могла прочитать их диалоги с моделью, взять оттуда решение и добить его первой за счет ресурсов – тех самых 10 000 одновременно работавших агентов.
Но опрошенные SciAm математики считают, что “испанская программа” стала лишь катализатором. С ее помощью удалось решить задачу для уравнений Эйлера, считавшуюся промежуточным шагом к Навье–Стоксу: это сделали Бакмастер с Альпеге, а по мнению части экспертов – и первый, малый отряд агентов OpenAI.
Дальше модель пошла совершенно иным маршрутом. Общего у двух подходов осталось немного – только лазейка, разрешенная формулировкой Клэя: жидкость можно подталкивать внешней силой, и весь вопрос в том, как эту силу построить. Испанская программа складывает ее слоями, масштаб за масштабом, – так, судя по всему, шел и малый отряд на Эйлере. Рой из 10 000 агентов на Навье–Стоксе сделал иначе: в центре – вихрь, который закручивается внутрь и вытягивается вдоль оси, по описанию самой OpenAI, “как спагетти”, а недостающее усилие дают короткие импульсы: они раскручиваются, отбирая энергию у потока вокруг, и гаснут, когда их съедает вязкость.
Источник: habr.com