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

Гипотеза экспоненциального времени, или ETH, утверждает, что для задачи 3-SAT не существует алгоритма с субэкспоненциальным временем работы. В 3-SAT нужно определить, можно ли подобрать значения переменных так, чтобы выполнялись все условия формулы. Поэтому предложить более быстрый алгоритм и доказать его корректность достаточно, чтобы опровергнуть ETH. Из этого, однако, не следует решение вопроса P против NP: субэкспоненциальный алгоритм всё ещё может быть слишком медленным по сравнению с полиномиальным.

Anthropic представила работу «A 2^o(n) Time Algorithm for 3-SAT» с указанием «Claude, Anthropic» в качестве автора. В ней описан детерминированный алгоритм, время работы которого растёт медленнее любой экспоненты вида 2^cn при фиксированном положительном c. Компания также сообщает, что алгоритм подсчитывает число подходящих наборов значений для #3-SAT. По заявлению Anthropic, ядро решения внутренняя исследовательская модель Claude нашла 16 октября без подсказок человека; при работе она сгенерировала 14 млн выходных токенов.

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

В работе Anthropic доказательство оформлено в Lean 4 – системе, которая проверяет формальные шаги рассуждения. Указаны 1050 модулей поверх библиотеки Mathlib; проверку проводили ядро Lean и отдельный чекер nanoda. При этом авторы работы оговаривают, что ни один человек пока не известен как проверивший всю формализацию целиком: её создавали AI-модели, а проверяли другие экземпляры моделей. Для практического решения 3-SAT результат тоже пока не подходит: согласно приведённой оценке, выигрыш для типичной формулы появляется лишь при числе переменных порядка 10^10000.