OpenAI и Anthropic заявили о субэкспоненциальном алгоритме для 3-SAT

Если они выдержат проверку, учёным придётся пересмотреть исследования, опиравшиеся на ETH.

Гипотезу ETH сформулировали в 1999 году Рассел Импальяццо, Рамамохан Патури и Фрэнсис Зейн. Она касается класса логических задач, для которых исследователи не ожидали найти алгоритм, скорость которого достаточно быстро растёт с увеличением числа переменных. ETH широко использовали как основание для выводов о сложности задач в теории графов, вычислительной биологии и базах данных. Заявления двух компаний ставят под вопрос это основание, но не означают, что все такие задачи легко решать.

Алгоритмы OpenAI и Anthropic против гипотезы ETH

Модель OpenAI нашла предполагаемое опровержение 16 октября, сообщила компания. На следующий день результат проверили с помощью Lean, системы машинной проверки доказательств. OpenAI опубликовала описание алгоритма и формальное доказательство на GitHub. В тот же день компания представила ещё две работы — по математике и физике.

Anthropic утверждает, что её исследовательская версия ИИ-модели Claude тоже пришла к основному алгоритму 16 октября, независимо от OpenAI. По словам исследователя компании Левента Альпёге, на получение результата ушло 14 млн выходных токенов, а люди не участвовали в самом открытии. Затем сотрудники Anthropic вместе с Claude подготовили изложение для статьи.

В статье Anthropic представлен алгоритм для задачи 3-SAT, в которой нужно определить, существует ли набор значений, удовлетворяющий логической формуле. Авторы также рассматривают #3-SAT, где требуется подсчитать число подходящих наборов. Заявленное время работы алгоритма называют субэкспоненциальным: возможность решить 3-SAT с такой скоростью противоречит ETH. Anthropic сообщает, что формализовала доказательство в Lean 4 и дополнительно проверила его независимым инструментом nanoda.

Машинная проверка не заменяет открытого разбора исследователями. В статье Anthropic сказано, что доказательство для Lean написали ИИ-модели и проверяли другие экземпляры моделей; на момент подготовки работы авторам не было известно ни об одном человеке, полностью проверившем его. Группа, приглашённая разбирать результат OpenAI, тоже подчёркивает, что её участие не означает признания доказательства верным.

Почему выводы ещё предстоит проверить

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

Уильямс рассказал, что часть доказательства OpenAI выглядит привычно, но несколько фрагментов требуют совместной работы специалистов. Гипотеза ETH служила предпосылкой во многих научных статьях. Поиск, приведённый в работе Anthropic, выявил более 800 публикаций, которые опираются на ETH или связанную с ней усиленную гипотезу SETH. Если опровержение подтвердится, исследователям придётся выяснить, какие выводы сохранятся без прежней предпосылки.

ETH связана с вопросом P против NP: можно ли быстро находить решение любой задачи, для которой найденный ответ легко проверить. Судоку помогает уловить разницу: проверить заполненную сетку проще, чем найти её решение. Опровержение ETH само по себе не решает вопрос P против NP. Уильямс считает, что результат заставляет внимательнее отнестись к возможности равенства P и NP, тогда как авторы работы Anthropic прямо указывают: их алгоритм этого равенства не доказывает.

Работа Anthropic не обещает быстрого способа решать практические задачи. Согласно её оценке, преимущество представленного алгоритма перед простым перебором для типичной формулы 3-SAT проявилось бы лишь при числе переменных больше примерно 10 в степени 10 000. Уильямс отдельно спросил OpenAI, не угрожает ли её результат криптографическим системам. По его словам, компания проверила этот вопрос и достаточно уверена, что доказательство не указывает на их взлом.

OpenAI по-разному организовала обсуждение трёх объявленных работ. Математическое доказательство компания выложила на GitHub, результат по ETH передала на открытое рассмотрение компьютерным учёным, а порядок публикации физической работы определит отдельная группа исследователей. Компания также сообщила, что выделила $5 млн (около 403 млн ₽) фонду Simons Foundation на семинары и конференции, посвящённые результатам, полученным ИИ.