Модели OpenAI и Anthropic независимо сформулировали доказательства, опровергающие гипотезу экспоненциального времени. Она предполагает, что для некоторых классов задач время решения в худшем случае растет экспоненциально с увеличением объема входных данных.
В качестве примера в исходной статье приводится задача 3-SAT: согласно гипотезе, ее нельзя решить быстрее экспоненциального времени относительно числа переменных. Обе компании представили результаты, формализованные на языке Lean. Доказательство OpenAI также позволяет предсказывать число решений булевых формул за субэкспоненциальное время.
Выводы пока не прошли независимую проверку. OpenAI передала свой результат группе специалистов по теории вычислительной сложности, в которую входят авторы исходной формулировки гипотезы. Если доказательства подтвердятся, они могут повлиять на фундаментальные представления о сложности вычислительных задач.