10 ноября 2026 г.
Модели PSI доказали гипотезу о квантовых вычислениях: результат проверил Lean
PSI получила доказательство давней гипотезы с помощью непубличной модели Anthropic и опубликовала материалы для проверки.
По данным PSI от 6 ноября, её исследовательская система получила полное доказательство гипотезы Ааронсона — Амбайниса на третий день работы.
Гипотеза касается пределов ускорения квантовых вычислений. Полученный результат исключает сверхполиномиальное преимущество по числу запросов для задач с ответом «да» или «нет» на большинстве случайных входов. Алгоритм Шора и квантовое моделирование физики и химии этот вывод не затрагивает.
Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.
От поиска к проверке. Прежние общие оценки влияния переменной ухудшались экспоненциально со степенью полинома. PSI получила полиномиальную оценку, а затем система дважды улучшила результат. Финальную версию принял Lean, инструмент для формальной проверки математических доказательств.
Математические утверждения, первый черновик статьи и формализацию в Lean создали ИИ-модели. Разработчик Дэвид Туртурян подготовил исследовательскую обвязку PSI и проверил статью. 8 ноября Скотт Ааронсон признал доказательство корректным на основании проверки Lean и экспертов, хотя сам ещё не разобрал его.
Локальная проверка. В репозитории PSI опубликованы команды для воспроизведения: после установки elan, make и python3 нужно скачать репозиторий и выполнить `lake exe cache get`, `make check`, `make replay`. По замеру PSI от 6 ноября, параллельный запуск использовал 173 ГБ оперативной памяти на восьми ядрах. Однопоточный `LEAN_NUM_THREADS=1 make replay` потребовал 7,4 ГБ и занял 11 минут.
Для воспроизведения PSI закрепила версии Lean и математической библиотеки Mathlib в опубликованном репозитории.
Первоисточник