PSI повідомляє про перевірений машиною доказ гіпотези Ааронсона—Амбаініса

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. Саме цей поділ визначає, що підтверджують машинні перевірки, а що й далі потребує людської математичної експертизи.