OpenAI и Anthropic почти одновременно заявили об опровержении одной из главных гипотез информатики

OpenAI и Anthropic представили два алгоритма, которые опровергают гипотезу экспоненциального времени (ETH). Это одно из фундаментальных предположений теории вычислительной сложности, на которое исследователи опирались больше 25 лет.
Обе компании получили результаты 16 октября. OpenAI опубликовала своё доказательство 26 октября, а следом появились материалы Anthropic. Разбираемся, что нашли модели и при чём тут IPO.
Что вообще за ETH?
Гипотезу сформулировали в 1999 году. Она утверждает, что задачу 3-SAT нельзя решить за субэкспоненциальное время по числу переменных.
Если совсем просто, 3-SAT — это задача, в которой нужно подобрать значения логических переменных так, чтобы формула стала истинной. Сложность в том, что с ростом числа переменных количество возможных комбинаций увеличивается экспоненциально.
ETH предполагает, что принципиально обойти такой характер роста вычислительных затрат не получится. На этой гипотезе основаны сотни работ по теории алгоритмов, графам, базам данных и другим направлениям.
Что нашли модели?
OpenAI сообщила, что её внутренняя модель разработала детерминированный алгоритм, который решает 3-SAT за субэкспоненциальное время. Более того, он умеет подсчитывать количество комбинаций, удовлетворяющих формуле, — это более сложная задача #3-SAT.
Доказательство модель получила 16 октября, а 17 октября его формализовали в Lean. OpenAI уже привлекла к независимой проверке Рассела Импальяццо и Рамамохана Патури — исследователей, участвовавших в формулировке ETH, — а также Райана Уильямса из MIT.
Anthropic опубликовала работу A 2^o(n) Time Algorithm for 3-SAT, автором которой указан Claude. Компания утверждает, что её внутренняя исследовательская модель независимо получила другой алгоритм с аналогичным результатом.
Для него тоже подготовили формальное доказательство на Lean 4 с использованием Mathlib. Дополнительно предусмотрена проверка независимым ядром nanoda.
В репозитории Anthropic, например, есть два sorry — специальных маркера незаполненных доказательств. Однако они находятся в файле Challenge.lean, который задаёт формулировки проверяемых теорем. Сами доказательства проверяются отдельно, поэтому считать наличие этих маркеров свидетельством ошибки было бы неправильно.
Что это значит?
Предложенные алгоритмы дают асимптотическое улучшение, то есть преимущество проявляется при чрезвычайно больших размерах задачи. Для практических вычислений они пока мало что меняют.
Опровержение ETH также не решает проблему P против NP. Алгоритм с субэкспоненциальным временем работы всё ещё может быть намного медленнее полиномиального.
При этом последствия для теоретической информатики могут оказаться серьёзными. Если результаты подтвердятся, придётся пересмотреть представления о сложности целого ряда задач, нижние оценки для которых выводились из ETH.
Что ещё нашли модели OpenAI?
Помимо опровержения ETH, OpenAI сообщила ещё о двух крупных результатах — в математике и теоретической физике.
Гипотеза Какэя и локальное сглаживание
Модель предложила доказательство гипотезы Согге 1991 года, которая описывает поведение волн при фокусировке. Если проще, очень сильная концентрация волны не может сохраняться долго. Ранее исследователям удавалось доказать связанные результаты лишь для отдельных размерностей, а модель OpenAI, по заявлению компании, справилась со всеми размерностями от двух и выше.
Из этого доказательства также следуют результаты по гипотезам Какэя и Штейна — двум известным открытым задачам математического анализа. Работу получили 18 октября, а на следующий день формализовали в Lean. Материалы уже опубликованы.
Квантовая хромодинамика и теория Янга — Миллса
Здесь задача ещё масштабнее: строго математически доказать существование квантовых теорий поля, описывающих взаимодействия элементарных частиц. OpenAI утверждает, что её модели получили такие доказательства для четырёхмерной квантовой хромодинамики (КХД), чистой теории Янга — Миллса и одной из моделей объединения взаимодействий Стандартной модели.
Это связано с одной из семи задач тысячелетия, но пока не означает её полного решения: отдельно требуется доказать существование массового зазора.
Работы по физике пока не опубликованы. Их изучением займётся группа исследователей во главе с нобелевским лауреатом Дэвидом Гроссом.
Научный прорыв или маркетинг?
Есть у этой истории и любопытный финансовый контекст. 26 октября, в день публикации OpenAI, Anthropic официально подала заявку на IPO — компания планирует выйти на Nasdaq под тикером ANT. А вскоре после анонса конкурента опубликовала собственное опровержение ETH.
По данным Reuters, OpenAI тоже готовится к выходу на биржу в 2027 году и ускоряет привлечение финансирования, чтобы опередить Anthropic. Обеим компаниям важно убедить инвесторов, что их модели способны не только писать код и генерировать тексты, но и совершать настоящие научные открытия.
Поэтому к громким заявлениям стоит относиться с осторожностью. Независимая проверка ещё не завершена, зато публикации уже работают на репутацию разработчиков. Впрочем, само совпадение дат ничего не доказывает: свидетельств того, что компании специально приурочили исследования к IPO или подстроили публикации друг под друга, нет. И если доказательства подтвердятся, их научная ценность от этого не уменьшится.
KioskNews shows a cleaned-up reading view extracted from the publisher’s page — the original always lives on their site, not ours.