Модели OpenAI и Anthropic опровергли гипотезу экспоненциального времени по задаче 3-SAT, результаты требуют независимой проверки

Внутренняя модель OpenAI достигла доказательства, которое опровергает гипотезу экспоненциального времени — важный ориентир в теории вычислительной сложности. По аналогичной траектории пришла к выводу и модель Anthropic. Гипотеза экспоненциального времени предполагает, что для ряда задач с ростом входных данных время решения в худшем случае растет экспоненциально. В частности речь идёт о классе задач, где рост сложности связывается с числом переменных.

Обсуждаемая задача 3-SAT описывает поиск присвоения значений истинности логическим переменным в булевой формуле, чтобы формула стала истинной. Формула состоит из ограничений, каждое из которых оперирует тремя переменными или их отрицаниями. По гипотезе экспоненциальности таких задач не решить быстрее экспоненциального времени в зависимости от числа переменных.

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

Гипотеза экспоненциального времени служит опорой для оценки вычислительной сложности задач во множества областей, в том числе графов, вычислительной биологии и геометрии. Если опровержение подтвердится, это вынудит исследователей пересмотреть работы, построенные на этой гипотезе, хотя практические последствия пока неочевидны: существование более быстрого алгоритма в теории не гарантирует его реальной эффективности на задачах реального мира.

Отдельно отмечается, что ранее внутренняя модель OpenAI решила 372 задачи по разным направлениям математики, но данная внутренняя разработка пока не стала доступной публике. Насчитывая, что независимая проверка будет необходима, по итогам кампании надлежащую верификацию получит ли открытая наглядность доказательства — станет ясно позже.