ИИ-система доказала гипотезу Ааронсона — Амбайниса в Lean
Исследовательская система стартапа Physical Superintelligence построила доказательство гипотезы Ааронсона — Амбайниса, которая оставалась без решения около 18 лет. О результате PSI сообщил 6 ноября. По данным компании, системе понадобилось три дня работы на невыпущенной модели Anthropic.
Полученный результат был не только сформулирован в естественном виде, но и формализован в Lean — системе автоматизированной проверки математических доказательств. Корректность доказательства подтвердило ядро пруф-ассистента, что позволяет проверить каждый формальный шаг независимо от самой ИИ-системы.
О чём гипотеза
Гипотеза связана с вопросом о том, насколько квантовые компьютеры могут превосходить классические при работе со случайными и неструктурированными данными. Скотт Ааронсон сформулировал её в лекции 2008 года, а позднее оформил математическую постановку совместно с Андрисом Амбайнисом.
Известные примеры квантового ускорения, включая алгоритм Шора для факторизации, используют определённую скрытую структуру входных данных. Гипотеза Ааронсона — Амбайниса рассматривает другой класс задач — вопросы формата «да или нет», в которых входы случайны и лишены такой структуры.
Согласно доказанному утверждению, для подобных задач квантовые алгоритмы не могут получить экспоненциальное преимущество над классическими только за счёт числа обращений к данным. Их выигрыш ограничен полиномиальным ускорением по этому параметру. Иными словами, случайный неструктурированный вход сам по себе не позволяет квантовым вычислениям превратить доступное классическим алгоритмам решение в экспоненциально более эффективное.
Почему важна формализация
Значимость результата связана не только с самим доказательством, но и с его проверяемой формой. Перенос математического рассуждения в Lean исключает необходимость доверять отдельным этапам, сгенерированным моделью: итог проверяет формальное ядро системы.
Этот случай показывает, как языковые модели могут использоваться не только для поиска идей, но и для подготовки строгих математических доказательств. При этом окончательную гарантию корректности здесь даёт не утверждение разработчиков ИИ, а независимая машинная проверка формализованного результата.
