Нав’є-Стокс, шпигунство та OpenAI

💡 Усі статті, обговорення, новини про AI — в одному місці. Приєднуйтесь до AI спільноти!

По-перше, розпочну з гарної новини. Виглядає так, що ще одна проблема тисячоліття закрита. Впав Нав’є-Стокс. Доказ формалізований на мові програмування Lean 4, ви його можете знайти за посиланням github.com/...​enai/NavierStokesAndEuler плюс короткий прес-реліз openai.com/...​x/navier-stokes-solution. Так, математична спільнота перевіряє, чи все точно у формулюваннях, це процес місяців, але виглядає досить переконливо.

Рис. 1 Знімок локального руху нестисливої рідини. Помаранчевий позначає швидше кутове обертання, бірюзовий показує повільніше. Швидкість обертання також залежить від радіуса. Траєкторії показують спіралеподібний рух до центру та розтягування вздовж осі.

Я не хочу писати, яка модель використовувалась, скільки агентів було в рої, ... Тут цікаво інше. Цей доказ з’явився напередодні публікації Бакмастера, Альпьоге, та інших, та дивним чином ми бачимо збіг у доказах. Так, Бакмастер та Альпьоге довели лише рівняння Ейлера з силовим членом (forced Euler equations). Це суміжна, формально інша задача. Але вочевидь кінцева ціль у них це Нав’є-Стокс. Це типова практика, коли команда, штурмуючи важку задачу, спочатку отримує проміжний результат на суміжній постановці, та і публікує саме його, поки повне рішення ще не готове або вилизане. Подивимося у repo, ми бачимо у корені дві директорії, NavierStokes та Euler.

Йдемо далі. За словами Бакмастера, з ним зв’язався Бубек, дослідник OpenAI, та запропонував йому вибір: або Бакмастер з Альпьоге публікують свою часткову роботу, а наступного дня OpenAI оголошує про повне рішення, визнаючи їх «найближчими до розв’язку людьми». Або Бакмастер публікує сам, забирає премію, але тільки вкаже, що модель OpenAI теж усе розв’язала. А... і ще... прибере Альпьоге зі списку співавторів, бо афіляція з Anthropic не дуже радує... Оскільки про це стало відомо, то Бакмастер відмовився.

OpenAI політкоректно зазначає, що «не може повністю виключити, що знеособлені дані з використання їхніх продуктів могли якось „покращити модель“». Виглядає як перестраховка та захист, якщо спільнота математиків визнає докази ідентичними. Для мене цей пасаж це визнання, що справа не зовсім чиста: якщо OpenAI дійсно мали незалежний інший доказ, то навіщо звертатися? Бери та публікуй!

А давайте подумаємо, що могло витекти. Ну... звісно що запити до ChatGPT. Але якщо припустити, що проєкт вели у git, використовували Codex хоча б для підготовки LaTeX файлів, то OpenAI могла просто мати доступ до всіх етапів дослідження, включаючи чернетки. А оськільки формальна верифікація це багато спейифічної рутини, то будувати доказ в IDE за допомогою асистента цілком логічно. А значить могло витекти абсолютно все. Додам, що технічно нескладно можливо мати бота, який буде слідкувати за успішністю роботи видатних вчених та не тільки. Також не проблема найняти спеціалістів, які б допомогли моделям на правах частинки рою у разі чого. Я не бачу, як це перевірити взагалі, лишається лише джентльменам вірити на слово. Що ми маємо? Сильний мотив, технічну можливість, і поведінку компанії до публікації, яка куди більше нагадує спробу контролювати наратив, ніж впевненість у власній незалежності.

Особисто мене в цій історії більше радує, що методи формальної верифікації все більше й більше використовуються у математиці, черга за програмуванням.