Погрешность до m/4 не ломает шаг в доказательстве OpenAI

Команда 8Braid, которая не связана с OpenAI, заново прогнала формальные проверки доказательства разрушения решений уравнений Навье-Стокса, выложенного OpenAI 8 сентября. Заодно она сделала явной одну константу, которую исходный аргумент оставлял абстрактной, и проверила, удержит ли её собственная база данных 8DB этот результат от молчаливого превращения в более сильное утверждение.

В разборе 8Braid, опубликованном 16 сентября, есть три слоя: воспроизведение чужих проверок, новая лемма для одного алгебраического шага и опыт с отзывом опоры, на которой эта лемма держится. Сама OpenAI выпустила 166-страничную статью с формализацией в Lean, а доказательство, по словам компании, собрали около 10 000 параллельно работавших агентов на невыпущенной внутренней модели. Речь об альтернативах C и D из постановки Clay Mathematics Institute: в них разрешена гладкая внешняя сила и нужно построить контрпример. Конструкция начинается с покоящейся жидкости, к которой прикладывают гладкую силу, а в репозитории OpenAI результаты сформулированы для всего пространства R^3 и для периодического тора.

Что подтвердила проверка

Comparator, рабочий процесс сверки, сопоставил присланные результаты по C и D с ожидаемыми формальными формулировками. Решение приняли два ядра: Nanoda и штатное ядро Lean. Ядро здесь означает небольшую доверенную программу, которая перепроверяет каждый шаг формального вывода. В отчётах об аксиомах значатся три стандартные аксиомы Lean: propext, Classical.choice и Quot.sound. Проверка шла на ревизии f9e8bc5b38b6, успешный прогон на Linux сохранил исходную конфигурацию челленджа и настоящую песочницу, а 8Braid записала зависимости, версии проверяющих программ, команды и фактические результаты.

Что из этого следует, 8Braid формулирует узко: формальные доказательства приняты относительно закодированных формулировок. Прочитать саму математику, сверить формулировку с физической задачей и применить результат в новой постановке - это, по словам команды, отдельные работы. Формальное воспроизведение не заменяет ни рецензию специалистов, ни решение Clay. Lean проверяет, что вывод следует из заданных определений и аксиом, но сам по себе не говорит, правильно ли закодирован исходный вопрос.

На 9 сентября Clay результат не принял и через положенную для премии процедуру он не прошёл; OpenAI сказала, что не собирается претендовать на миллион долларов. В тот же день математики Caltech в открытом письме назвали перепроверку громких ИИ-результатов трудом, который «не оплачивают, не указывают в авторстве и не признают».

Запас m/4

Дальше 8Braid разобрала предложение 7.5 (уравнения 7.24-7.28, страницы 82-83 рукописи). Там используется положительное ковариационное разложение: конструкция складывает два вклада с весами, которые обязаны оставаться положительными. Вопрос простой: насколько можно сдвинуть входные данные, прежде чем положительность пропадёт.

Ответ команда вывела в нормированных координатах этого шага. Матрица имеет вид [[1+a, 1+b], [-1+c, 1+d]], цель равна (1, s), и она лежит внутри допустимого конуса с запасом m: |s| ≤ 1-m, где 0 < m < 1. Если каждая из четырёх ошибок a, b, c, d по модулю не больше m/4, веса коррекции остаются положительными, а определитель не опускается ниже 7/8.

Дроби точные, и утверждение доказано для всей заявленной области вещественных параметров, без выборки отдельных точек. Отдельные скрипты на Python восстанавливают рациональную алгебру, а самостоятельное доказательство в Lean проверяет общую импликацию. К нему приложены исходник, версии тулчейна и Mathlib, вывод по аксиомам и манифест файлов.

Ограничения 8Braid перечисляет сама. Лемма не подставляет конкретные профили из исходной статьи, не доказывает их оценку ошибки и не решает вопрос гладкого продолжения при нулевой цели. Для физической интерпретации нужны ещё оговорённая система отсчёта и положительные масштабы. На оптимальность запаса команда не претендует. Чтобы применить его ко всей конструкции, нужны аналитическая оценка ошибки и границы профилей из исходника.

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

Если отозвать опору

Эту условную лемму 8Braid пропустила через отдельную исследовательскую нагрузку 8DB. В записи хранится доступность леммы вместе с обязательствами, которые нужно выполнить, чтобы её применить. Затем команда отзывает допущение, на котором лемма держится, и заново читает сохранённое состояние:

• сама ковариационная лемма до отзыва доступна в заявленных границах, после отзыва больше не числится подкреплённой;
• её применение к реальной конструкции OpenAI держится на отдельных обязательствах, которые не приняты ни до, ни после;
• не связанные с ней прежние результаты сохраняют свою опору.

Отзыв меняет запись о доступной опоре, а не истинность математической импликации. Тест прошёл через штатного потребителя данных и отдельного читателя, включая повторный прогон из чистой локальной директории. В фикстуре 88 фактов и 26 правил, прошли семь тестов адаптера и 24 контрольных отказа. Шесть обязательств, относящихся к исходнику и самому уравнению, остаются непринятыми, а ранее квалифицированный результат 1/73 сохранился.

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

Проверка внутри цикла агента

У OpenAI на Навье-Стокс ушло около 2,7 миллиона сообщений агентов и 130 миллиардов выходных токенов; агенты пришли к результату примерно за 88 часов, после чего GPT-6 Astra ещё около 17 часов формализовала и проверяла его в Lean.

8Braid предлагает ставить проверяющую программу между предложением агента и его принятием в исследовательскую запись. Изменённый коэффициент многочлена не пройдёт проверку точного тождества. Артефакт из чужого контекста не пройдёт проверку применимости. Вывод без опоры останется непринятым, и у агента появится конкретная причина пересмотреть следующий шаг. Команда называет это проверкой во время исполнения и разделяет ошибки, которые можно протестировать, и утверждения, для которых адекватного теста нет: там по-прежнему нужны суждение или новая математика.

Насколько такой фильтр снижает долю ошибок у агента от начала до конца, 8Braid не измеряла, гарантий задержки для продакшена тоже не даёт и называет и то и другое целями для будущей оценки. Связку с другими своими инструментами команда тоже описывает как непостроенную. Интервальные численные методы её движка VTTE могли бы подавать ограниченные входные данные в неравенство с m/4, а следующий эксперимент сформулирован так: заключить в интервалы один набор параметров исходника, проверить ковариационный запас и согласованность там, где две сертифицированные области перекрываются.

Идея в целом сводится к новой единице совместной работы: агент передаёт утверждение вместе с исполняемой проверкой, допущениями и открытыми вопросами, второй агент воспроизводит проверку, третий берётся за открытое условие. Совместимые форматы для такого обмена и успешное применение в других исследовательских программах 8Braid относит к работе, которую ещё предстоит сделать всему сообществу. В сноске команда отмечает, что исследование и текст писались с помощью ИИ, а математические проверки и проверки записей перечислены отдельно.

Следующие шаги названы конкретно: в математике - получить аналитические оценки, чтобы применить запас m/4 к выбранным столбцам исходной конструкции, в базе данных - перевести результат в процесс работы с теоремами и доказательной базой, не привязанный к контексту.