OpenAI заявила, что опровергла гипотезу ETH. Проверяющие просят не считать это подтверждением

26 октября OpenAI выложила на GitHub работу «The Exponential Time Hypothesis is False». Если она устоит, это громкая новость для теории алгоритмов.

Объясню на пальцах. Есть задача 3-SAT: много переключателей «да/нет» и условия, которые должны выполниться разом. Каждый новый переключатель удваивает число вариантов. При сотне переключателей это 2 в сотой степени.

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

Модель OpenAI предложила алгоритм чуть быстрее экспоненты. Выигрыш появляется только на гигантских размерах, практических применений в ближайшее время, по словам Райана Уильямса из MIT, нет.

Теперь главное. Проверять работу будут сами авторы гипотезы вместе с Уильямсом. И они сразу написали в открытом письме: «Наше участие не стоит считать подтверждением».

Доказательство прогнали через Lean, программу, которая механически сверяет каждый шаг. Только по документации самой OpenAI в Lean проверена оценка слабее, чем в рукописи. И Lean не скажет, совпадают ли определения с исходной гипотезой. Это решают люди.

Вскоре Anthropic выложила свой алгоритм с тем же выводом. Независимой проверки пока нет ни у той, ни у другой.

Плюс в том, что материалы открыты сразу, и проверка идёт публично.

Разработчики, вам хватает Lean-доказательства, чтобы поверить? Или ждёте вердикта людей?

#ии #алгоритмы #наука