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