OpenAI и Anthropic заявили об опровержении гипотезы экспоненциального времени

Компании опубликовали созданные ИИ алгоритмы и формализации в Lean, которые дают субэкспоненциальное решение задачи 3-SAT и тем самым противоречат гипотезе экспоненциального времени. Если доказательства выдержат проверку, потребуется пересмотреть множество условных оценок сложности, однако результат не решает задачу P vs NP и не означает появления практичного SAT-решателя.

OpenAI сообщила, что ее внутренняя ИИ-система нашла алгоритм, опровергающий гипотезу экспоненциального времени (Exponential Time Hypothesis, ETH). Компания опубликовала препринт и формализацию в системе доказательств Lean.

ETH предполагает, что задача выполнимости булевых формул 3-SAT в худшем случае не может быть решена за время 2^o(n), где n — число переменных. Предложенный алгоритм подсчитывает решения формул k-CNF за субэкспоненциальное время и с полиномиальным объемом памяти. Если результат подтвердится, гипотеза окажется ложной, а сотни основанных на ней условных нижних оценок сложности придется интерпретировать заново.

Anthropic вскоре опубликовала собственную работу с алгоритмом для 3-SAT и формальным доказательством в Lean, указав автором внутреннюю исследовательскую модель Claude. Компания подчеркивает, что результат носит исключительно асимптотический характер и ничего не говорит о практической скорости решения формул.

Заявленные результаты пока проходят проверку научным сообществом. Изучением работы OpenAI займется группа под руководством Рассела Импальяццо и Рамамохана Патури из Калифорнийского университета в Сан-Диего, участвовавших в формулировке ETH, и специалиста по теории сложности Райана Уильямса из MIT. Проверка в Lean снижает риск ошибок внутри формального доказательства, но не заменяет экспертную оценку постановки задачи и соответствия формализации заявленным выводам.

Опровержение ETH само по себе не доказывает равенство P и NP: новый алгоритм остается суперполиномиальным. Непосредственных практических последствий для криптографии или существующих SAT-решателей пока не показано.