26 октября OpenAI объявила, что её исследовательская модель нашла алгоритм, опровергающий гипотезу экспоненциального времени, или ETH. Компания выложила рукопись и формализацию доказательства в Lean — системе, которая проверяет логическую правильность формальных выводов. Вскоре собственную работу представила Anthropic: по её сообщению, основу алгоритма нашла внутренняя исследовательская модель Claude.
ETH используют, когда исследователи оценивают, насколько быстро в принципе можно решать сложные вычислительные задачи. Поэтому сообщения лабораторий привлекли внимание далеко за пределами исследований ИИ. Но последствия зависят от точного содержания доказательств и их независимой проверки.
Основной блок
Что именно предполагает ETH
Задача 3-SAT предлагает определить, можно ли расставить переменным значения «истина» и «ложь» так, чтобы выполнялась вся логическая формула. Если подходящий набор уже найден, проверить его сравнительно просто. Найти его для произвольной формулы сложнее. Для n переменных существует 2ⁿ вариантов значений. Полный перебор проверял бы их по одному. ETH утверждает, что для решения 3-SAT в худшем случае нельзя получить алгоритм со временем 2^(o(n)) — таким, где показатель степени растёт медленнее n. Это предположение сформулировано в работах Рассела Импальяццо и Рамамохана Патури. Разница между оценками существенна: Время работы Тип зависимости n³ Полиномиальная 2^(√n) Субэкспоненциальная, но быстрее любого фиксированного полинома по мере роста n 2^(0,01n) Экспоненциальная, несмотря на небольшой коэффициент Заявленный алгоритм должен работать для произвольных входных формул, включая худшие случаи. Быстрых ответов на отдельных примерах для опровержения ETH было бы недостаточно.
Что опубликовали OpenAI и Anthropic
Согласно описанию OpenAI, её модель предложила способ за субэкспоненциальное время подсчитывать число подходящих наборов значений для формул с фиксированным максимальным числом переменных в каждом условии. Если число решений равно нулю, формула невыполнима; если больше нуля, решение существует. Частный случай для 3-SAT противоречит ETH. Работа Anthropic также заявляет алгоритм для 3-SAT со временем 2^(o(n)). Авторы указывают, что он решает и задачу подсчёта всех подходящих наборов значений. Компания опубликовала рукопись и формализацию в Lean 4. Это отдельная работа со своим алгоритмом; совпадение общего вывода не заменяет проверки каждой из них.
Что проверил Lean — и что предстоит проверить людям
Формальное доказательство позволяет проверить, следует ли записанная теорема из определений и предыдущих шагов. При этом исследователям всё равно нужно прочитать определения и убедиться, что формальная теорема соответствует заявлению в рукописи. Anthropic прямо отмечает это ограничение в материалах своей публикации. У OpenAI есть и различие между двумя опубликованными оценками времени. Рукопись заявляет более сильную границу, содержащую множитель log log n в числителе показателя степени. В описании формализации Lean указан вариант с (log log n)². Вторая оценка слабее, но тоже остаётся субэкспоненциальной для фиксированной длины условия. Если формализация относится именно к заявленной задаче, этой оценки достаточно, чтобы опровергнуть ETH.Таким образом, вопрос для научного сообщества шире проверки того, компилируется ли код Lean. Нужно разобраться в алгоритмах, сопоставить формальные утверждения с рукописями, проверить предпосылки и сделать результат понятным другим исследователям.
Почему P против NP остаётся открытой проблемой
Проблема P против NP спрашивает: можно ли любую задачу, решение которой быстро проверяется, также быстро решить? В этом вопросе «быстро» означает полиномиальное времяАлгоритм со временем 2^(√n) быстрее экспоненциального перебора в асимптотическом смысле, но медленнее любого фиксированного полинома при достаточно больших n. Поэтому возможное опровержение ETH не доказывает равенство P = NP. Оно меняет представление о границе сложности 3-SAT, оставляя другой фундаментальный вопрос без ответа.
Что может измениться на практике
На ETH опираются многие условные оценки сложности: если гипотеза верна, определённую задачу нельзя решить быстрее указанной границы. При её опровержении такие выводы потребуется пересмотреть. Сами доказанные утверждения вида «если ETH, то…» от этого не становятся логически ошибочными — меняется возможность применять их как Это также не означает немедленного ускорения программ. Асимптотическая оценка не сообщает, насколько сложна реализация, велики ли скрытые постоянные множители и при каком размере входных данных алгоритм начинает выигрывать у существующих методов. Последствия для других задач нужно изучать отдельно: сведение одной задачи к другой может изменить размер входа и итоговую оценку времени.
Как будет проходить проверка
OpenAI согласилась открыть материалы и поддержать конференцию для обсуждения последствий результата. Внешняя группа Импальяццо, Патури и Уильямса приглашает исследователей проверять доказательство, публиковать замечания и готовить доступные объяснения. По условиям, описанным OpenAI, участники группы работают добровольно, без соглашений о неразглашении и могут свободно критиковать выводы компании.
«Наше участие не следует воспринимать как подтверждение заявленного результата».
Так предупредили Рассел Импальяццо, Рамамохан Патури и Райан Уильямс — исследователи, организующие открытое изучение работы OpenAI.
При появлении новых разборов стоит следить за четырьмя пунктами:
- Постановка задачи: алгоритм ищет решение, определяет его существование или считает число решений?
- Оценка времени: какие параметры входят в формулу и что считается фиксированным?
- Объём формализации: совпадает ли проверенная теорема с главным утверждением рукописи?
- Практическая проверка: появилась ли реализация и сравнение с существующими алгоритмами?
Частые вопросы
ETH уже официально опровергнута?
OpenAI и Anthropic опубликовали заявленные доказательства и формализации. Внешняя группа подчёркивает, что её участие пока не означает научного подтверждения результата.
ИИ решил P против NP?
Нет. Заявленное субэкспоненциальное время само по себе не является полиномиальным.
Можно ли уже использовать новый алгоритм в разработке?
Из опубликованной асимптотической оценки нельзя сделать вывод о выигрыше на практических размерах задач. Для этого нужны реализация и измерения.
Главный результат теперь должен стать понятным и проверяемым
Лаборатории опубликовали материалы, которые ставят под вопрос одну из привычных границ теории алгоритмов. Формальные доказательства дают исследователям возможность проверять точные утверждения, а открытое обсуждение должно показать, выдерживают ли эти утверждения независимое изучение. Если да, следующим этапом станет пересмотр выводов, основанных на ETH, и поиск задач, для которых новый подход действительно даёт ускорение. В блоге SpeShu.AI мы следим за такими исследованиями и объясняем, что стоит за громкими заявлениями об ИИ. Подписывайтесь, чтобы читать новые разборы.
