Модели и платформы ИИ
PSI сообщает о доказательстве гипотезы Ааронсона — Амбаиниса, проверенном компьютером
Добавьте Unite.AI в избранные источники в Google
Physical Superintelligence объявила 6 ноября 2026 года, что внутренняя исследовательская система, работавшая с экземплярами непубличной модели Anthropic, нашла доказательство гипотезы Ааронсона — Амбаиниса — задачи в области квантовых вычислений, остававшейся открытой с 2008 года.
Система выдала полное доказательство на третий день работы на собственной инфраструктуре PSI, и помощник по доказательствам Lean его принял. Затем PSI поручила системе связанные открытые задачи, и та дважды улучшила результат, прежде чем Lean принял окончательный вариант. Рукопись и формализация на Lean 4 находятся в открытом доступе.
Что гипотеза говорит об ускорении квантовых вычислений
Речь идёт о том, в каких случаях квантовые компьютеры могут работать экспоненциально быстрее классических. Алгоритм факторизации Шора 1994 года зависит от структуры: входные данные содержат повторяющийся шаблон, который алгоритм может использовать. Результат PSI относится к противоположному случаю — случайным или неструктурированным входным данным, для которых такой шаблон, как правило, отсутствует.
В модели запросов классический алгоритм считывает по одному биту за запрос, тогда как квантовый запрос может находиться в суперпозиции сразу по многим позициям входных данных. В объяснении PSI эта модель связана с многочленами: после T квантовых запросов вероятность того, что алгоритм ответит «да», представляет собой ограниченный многочлен от входных битов степени не выше 2T. Поэтому имитация квантового алгоритма сводится к оценке этого многочлена без считывания экспоненциально большого числа входных битов.
В своей первоначальной статье Скотт Ааронсон и Андрис Амбаинис выдвинули гипотезу, что у каждого ограниченного многочлена низкой степени есть переменная с большим влиянием. Они доказали, что при условии справедливости этой гипотезы любой квантовый алгоритм с T запросами можно имитировать на большинстве входных данных с помощью классического алгоритма, выполняющего полиномиальное по T число запросов. Следствие состоит в том, что при любой фиксированной погрешности аппроксимации и любой фиксированной доле исключаемых входных данных число классических запросов растёт полиномиально, а не экспоненциально; это не исключает экспоненциального преимущества квантовых вычислений для задач с подходящей структурой.
Формально в репозитории рассматривается вещественный многочлен p степени не выше d, значения которого на дискретном кубе находятся в диапазоне от 0 до 1. Если его дисперсия на равномерно выбранном случайном входе не меньше ε, то у некоторой координаты влияние составляет не менее (8√15 / (125π⁴)) · ε^(5/2) / d⁶ и, следовательно, не менее (ε/d)⁷. Влияние — это ожидаемое значение квадрата изменения p при инвертировании бита этой координаты.
Как было построено и проверено доказательство
Доказательство следует плану Шахара Ловетта и Цзяпэна Чжана, основанному на дробных сертификатах и множествах уровня, но вместо неравенства, которое в их плане оставалось гипотезой, использует новое неравенство для всех пар. Определитель задаёт взаимно однозначное сопоставление настроек входных данных. По словам PSI, это сопоставление превосходит более слабое сопоставление из леммы о бабочке Дэвида Раймера, поскольку также ограничивает частоту совпадения сопоставленных настроек по каждой координате; эта граница необходима для нового неравенства.
В репозитории элементарное доказательство разделено на четыре части: выведение неравенства для всех пар из определителя и биекции, интегрирование по множествам уровня, усреднение по координатам и установление границы для строки с помощью поточечной границы чувствительности. В совокупности эти шаги дают явную границу для влияния.
Согласно зафиксированному в репозитории аудиту, формальная разработка не содержит заглушек для доказательств или добавленных аксиом. Объявления были повторно проверены с помощью ядра Lean и lean4lean — независимой реализации системы проверки типов Lean. В изолированной среде программа сравнения, использующая ядра nanoda и Lean, приняла все четыре итоговые теоремы; на втором компьютере она приняла один корректный небольшой пример решения и отклонила четыре заведомо неверных.
У этих проверок есть чёткие ограничения. Читателю всё ещё необходимо убедиться, что формальная формулировка соответствует гипотезе в опубликованном виде. Статья, написанная для людей, сама по себе не проверена компьютером; кроме того, ядро и компилятор Lean, определения Mathlib и компьютеры, использовавшиеся для проверки, остаются частью доверенной базы.
Участие людей и экспертная проверка
Дэвид Туртурян, сотрудник технического отдела PSI, разработал и запустил исследовательскую систему, определил рамки задачи, предложил модели оформить первый вариант, проверил его и отвечает за корректность статьи. В репозитории указано, что математические утверждения, первый вариант и формализацию на Lean создали модели ИИ. Джим Халверсон провёл аудит доказательства, а Фиала Шанахан высказала замечания по формализации.
Объявление последовало за статьёй, поданной 19 августа 2026 года Гаем Бланком, Джорданом Доктером, Кармен Штрассл и Ли-Яном Таном. Эти авторы установили следствие для классической имитации параллельных квантовых алгоритмов, доказав, что алгоритм с t запросами и d раундами можно имитировать на большинстве входных данных, используя t^(O(d²)) классических запросов. По словам PSI, все четверо изучили полное доказательство и прислали замечания; сейчас они готовят более краткое изложение для специалистов.
В своей оценке, опубликованной PSI, исследователи написали: «Это грандиозный результат. Он разрешает гипотезу, которой уже несколько десятилетий и которая имеет важные последствия для понимания природы задач, допускающих квантовое ускорение. Доказательство опирается на несколько направлений исследований в области анализа булевых функций и вероятностной комбинаторики и развивает их. Всё это объединено воедино почти волшебным образом».
Непосредственная проверка здесь необычайно конкретна: независимые ядра могут повторно проверить закодированную аргументацию, однако экспертам ещё предстоит подтвердить, что закодированное утверждение соответствует гипотезе Ааронсона — Амбайниса, и оценить те части статьи, которые не проверены в Lean. Это разграничение определяет, что именно подтверждает машинная проверка, а что по-прежнему требует математической экспертизы человека.
