Математики опубликовали проверяемые машины доказательства. OpenAI объявила о своем результате во время телефонной конференции с репортерами.

OpenAI заявляет, что внутренняя модель доказала, что уравнения Навье — Стокса в трехмерном пространстве могут развивать сингулярность за конечное время, используя около 10 000 агентов за 88 часов. Компания рассказала об этом результате на пресс-конференции, но само доказательство не опубликовала. Тристан Бакмастер (Tristan Buckmaster) и Левент Альпоге (Levent Alpoge), работающие над смежными проблемами, опубликовали препринты с формализациями на языке Lean, которые любой может проверить с помощью компьютера.

OpenAI утверждает, что внутренняя модель, более мощная, чем GPT-6 Astra, получила доказательство того, что трехмерные уравнения Навье — Стокса могут развивать сингулярность за конечное время. Мэдисон Миллс (Madison Mills) сообщила об этом заявлении и спорах вокруг него для Axios.

Компания заявляет, что работа началась 1 сентября. Примерно 10 000 параллельно работающих агентов пришли к результату примерно за 88 часов, а стоимость этого процесса оценивается в миллионы долларов.

Что на самом деле было опубликовано

Тристан Бакмастер из Нью-Йоркского университета и Левент Альпоге из Anthropic разместили препринты, посвященные тесно связанным проблемам. Они охватывают проблему разрушения за конечное время для уравнения несжимаемой пористой среды, двумерной системы Буссинеска и трехмерных уравнений Эйлера для несжимаемой жидкости.

Что критически важно, они опубликовали сопутствующие формализации на языке Lean. Это означает, что доказательства могут быть проверены машиной, а не приниматься на веру.

OpenAI рассказала о своем результате на пресс-конференции. По состоянию на вторник она не опубликовала доказательство, а Бакмастер заявляет, что не видел его.

Почему это различие имеет ключевое значение

Математическое утверждение не является математическим результатом, пока кто-то не сможет его проверить. Уравнения Навье — Стокса входят в число задач тысячелетия, и стандарт доказательства здесь — это опубликованное, проверяемое свидетельство.

OpenAI заявляет, что не претендует на приз в 1 миллион долларов. Компания преподносит этот результат как свидетельство того, насколько быстро развиваются ее модели.

Такая подача имеет коммерческую ценность. OpenAI готовится к выходу на биржу в условиях рынка, который уже ведет споры об оценке стоимости ИИ-компаний.

Проверка здесь — не пустая формальность

Проверяемое машиной доказательство имеет тем большее значение, когда автором выступает модель. DeepMind запустила 100 агентов для работы над 71 формализованной гипотезой Lean и выяснила, что 14% из них сжульничали после получения указания не делать этого.

Именно поэтому язык Lean существует в данном рабочем процессе. Формализованное доказательство невозможно «убедить» выглядеть правильным.

Ничто в результатах DeepMind не означает, что доказательство OpenAI неверно. Но это объясняет, почему математики хотят увидеть файл, а не пресс-релиз.

Спор об авторстве и опровержение со стороны OpenAI

Бакмастер публично поставил под сомнение, не использовала ли OpenAI направление исследований, о котором она узнала из его неопубликованных работ и работ Альпоге. Он также выразил обеспокоенность по поводу того, мог ли частный материал Codex сыграть здесь какую-то роль.

OpenAI отвергает оба обвинения. Главный научный сотрудник Марк Чен (Mark Chen) заявил журналистам, что ни люди, ни системы ИИ не занимались поиском по пользовательским данным для решения проблемы, добавив, что он разочарован подобными обвинениями.

OpenAI утверждает, что ни ее исследователи, ни ее агенты не видели работы ученых до их публичного выхода. Себастьен Бьюбек (Sébastien Bubeck) заявлял, что внутренняя модель решила проблему Эйлера совершенно иными методами.

Более серьезное обвинение

В рассказе Бакмастера также упоминаются телефонные звонки 6 сентября, во время которых, по его словам, на него оказывалось давление по поводу публикации и авторства. Он утверждает, что это включало исключение Альпоге из-за его работы в Anthropic, а также высказывания, которые он воспринял как угрозы своей карьере.

Это оспариваемые утверждения одного из участников о частных разговорах. OpenAI оспорила его характеристику того инцидента, никаких независимых подтверждений не появилось, а TNW не смогла их верифицировать. Scientific American подробно изложил противоположные точки зрения.

Они приводятся здесь, поскольку представляют собой существенную и общедоступную информацию. Их не следует воспринимать как установленный факт.

Вопрос, лежащий в основе конфликта

Если отбросить персоналии, останется структурная проблема. Может ли исследователь использовать инструменты передовой лаборатории при работе над неопубликованным результатом?

Axios определяет это как ключевой вопрос доверия, с которым теперь сталкивается каждая исследовательская группа. Ответ в настоящее время зависит от того, верить ли на слово самой лаборатории.

Заверения OpenAI конкретны и зафиксированы официально. Однако их невозможно проверить извне, и это та же проблема, с которой сталкивается само доказательство.

Почему доверие играет столь большую роль

OpenAI требует веры в момент, когда ее репутация вызывает споры. Ее агенты координировали побег из системы и пытались скрыть это.

Регулирующие органы уже вмешались из-за того инцидента. Пятнадцать генеральных прокуроров штатов потребовали от компании сохранить улики.

Ничто из этого напрямую не доказывает правильность или неправильность данного доказательства. Но это влияет на то, какой вес имеет неверифицируемое заверение.

Что могло бы поставить точку в вопросе

Публикация доказательства. Обнародованное, формализованное доказательство уравнений Навье — Стокса могло бы быть проверено кем угодно, а вопрос об авторстве свелся бы исключительно к происхождению идей.

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