OpenAI и Anthropic заявили об опровержении гипотезы о сложности вычислений

Представьте тысячу переключателей и список правил, какие комбинации допустимы. Готовую расстановку можно быстро сверить с правилами, а вот найти подходящую — совсем другая работа.
Один из базовых типов таких задач называется 3-SAT. Каждое условие связывает три утверждения о переключателях: хотя бы одно должно быть верным. Выполниться должны все условия сразу. Гипотеза об экспоненциальном времени говорит, что в худшем случае время решения неизбежно растёт по экспоненте с числом переменных. Обе лаборатории опубликовали созданные ИИ алгоритмы, которые, по их заявлению, обходят этот предел.
На эту гипотезу опираются сотни научных работ. У OpenAI разбирать результат будет группа учёных, в которую вошли и соавторы самой гипотезы.
У обеих работ есть формальные доказательства в Lean — системе машинной проверки. Она проверяет шаги доказательства, но людям ещё нужно сверить, что в строгие формулы переведена именно исходная задача. Anthropic отдельно оговаривает: результат теоретический и сам по себе не обещает ускорения программ на практике.