OpenAI 26 октября опубликовала алгоритм, который, по утверждению компании, опровергает экспоненциальную временную гипотезу, или ETH. На следующий день аналогичную работу представила Anthropic. Пока это две заявки на научное открытие, требующие независимой проверки.
ETH относится к задачам, где нужно подобрать значения переменных так, чтобы логическая формула оказалась истинной. В базовом варианте 3-SAT каждое условие содержит до трёх переменных. Гипотеза утверждает, что время решения таких задач в общем случае должно расти экспоненциально вместе с числом переменных.
OpenAI описывает алгоритм, который точно подсчитывает подходящие наборы значений для формул фиксированной ширины за субэкспоненциальное время и с полиномиальным объёмом памяти. Частный случай для 3-SAT противоречит ETH. Доказательство формализовано в Lean, системе машинной проверки математических рассуждений.
Читайте также
Anthropic сообщает, что её внутренняя модель Claude получила основной алгоритм 16 октября, использовав 14 млн выходных токенов без участия человека. Исследователи компании затем помогли оформить работу. Алгоритм решает более трудную задачу #3-SAT и подсчитывает все подходящие наборы значений. Его доказательство также формализовано в Lean 4.
Материалы OpenAI изучит независимая группа под руководством Рассела Импальяццо и Рамамохана Патури из Калифорнийского университета в Сан-Диего и профессора MIT Райана Уильямса. Импальяццо и Патури участвовали в формулировке ETH. Учёные подчеркнули, что их участие не означает подтверждения результата.
Если алгоритмы окажутся корректными, исследователям придётся пересмотреть сотни работ по теории алгоритмов, графам, вычислительной биологии и базам данных, которые опираются на ETH. При этом результат не доказывает равенство P и NP: предложенные алгоритмы остаются субэкспоненциальными, а не полиномиальными. По словам Уильямса, OpenAI проверила возможные последствия для криптографии и не обнаружила признаков взлома используемых систем.