Научный стартап Physical Superintelligence 6 ноября объявил, что его исследовательская система с непубличной моделью Anthropic нашла доказательство гипотезы Ааронсона — Амбайниса. Она описывает, при каких условиях квантовый компьютер может значительно опережать классический. Работа опубликована как препринт на arXiv, а ее формализация доступна в репозитории GitHub.
В сообщении PSI задача названа открытой с 2008 года. Один из ее авторов, специалист по квантовым вычислениям Скотт Ааронсон, пишет, что они с Андрисом Амбайнисом сформулировали гипотезу в 2009 году. Расхождение связано с точкой отсчета: PSI возводит постановку задачи к лекции 2008 года, а первая версия работы авторов появилась позднее.
Гипотеза касается так называемой сложности запросов: сколько раз алгоритму нужно обратиться к входным данным, чтобы решить задачу. Ааронсон и Амбайнис предположили, что для вопросов с ответом «да» или «нет» квантовый алгоритм не сможет получить сверхполиномиальное преимущество на большинстве случайных входных данных. Для большого ускорения во входе должна присутствовать особая структура, например повторяющийся шаблон.
Читайте также
Если доказательство выдержит дальнейшую проверку, оно закроет один из предполагаемых путей к квантовому ускорению, но не отменит преимущества квантовых компьютеров в целом. Результат ничего не меняет для алгоритма Шора, использующего структурированные данные, и не опровергает перспективы квантового моделирования физики и химии. Сам Ааронсон отдельно предостерег от вывода, будто «квантовое превосходство умерло».
PSI сообщает, что полное доказательство появилось на третий день работы системы. Затем она дважды улучшила результат, а Lean принял итоговую версию. Lean — это интерактивный помощник для доказательств: математические утверждения и логические шаги записываются в формальном виде, после чего программа проверяет, следует ли каждый шаг из заданных правил.
В репозитории проекта говорится, что основные теоремы доказаны без заглушек и дополнительных аксиом, а формализацию перепроверили две реализации ядра Lean. Это существенно снижает риск обычной логической ошибки внутри формальной цепочки. Однако такая проверка не заменяет содержательную работу математиков: людям еще нужно подтвердить, что формализованное утверждение точно соответствует исходной гипотезе и что внешние предпосылки использованы корректно.
На странице PSI модель названа только непубличной моделью Anthropic. TechCrunch уточняет, что исследователь PSI Дэвид Туртурян работал с ранней версией Claude Fable 5.2. При этом результат принадлежит не одной чат-модели: компания описывает собственную исследовательскую систему, объединяющую модели с инструментами, памятью и другой программной инфраструктурой.
Скотт Ааронсон сообщил, что еще не разобрал доказательство полностью, но считает его правильным. В качестве оснований он назвал сертификат Lean и проверку работы профильными исследователями. Ученые из MIT и Стэнфорда также готовят более короткое изложение для специалистов. Тем не менее работа остается препринтом, поэтому осторожная формулировка пока точнее безусловного утверждения, что многолетняя задача окончательно закрыта.
Практическая важность случая шире самой квантовой теории. ИИ здесь не только помог написать текст или перебрать известные результаты, а участвовал в получении нового доказательства, которое можно проверить машинно. Формальные методы дают научному сообществу способ аудировать такие ответы значительно надежнее, чем обычный диалог с моделью.
У подхода есть пределы. Математическое доказательство можно представить как последовательность формальных операций, тогда как выводы в физике, материаловедении и биологии часто требуют измерений и воспроизводимых экспериментов. Поэтому успех PSI показывает возможную схему работы для теоретических дисциплин — ИИ ищет решение, формальная система проверяет логику, а специалисты сопоставляют формулировку с исходной задачей, — но сам по себе не доказывает, что модели уже способны автономно совершать надежные открытия во всех областях науки.
