Штучний інтелект за три дні довів математичну гіпотезу, яку не могли розв’язати 18 років

Математична задача, яка не давалася вченим 18 років, впала перед штучним інтелектом за три дні. Американська дослідницька компанія Phys­i­cal Super­in­tel­li­gence (PSI) оголосила, що її ШІ-система довела гіпотезу Аронсона — Амбайніса, пов’язану з можливостями квантових комп’ютерів. Доказ перевірила математична система Lean, хоча незалежна наукова експертиза ще триває.

Гіпотезу сформулювали у 2008 році американський вчений Скотт Аронсон та латвійський математик Андріс Амбайніс. Вона стосується одного з фундаментальних питань квантових обчислень: за яких умов квантовий комп’ютер здатен вирішувати задачі експоненційно швидше за звичайний. За 18 років математикам вдавалося довести лише окремі часткові випадки — загальне рішення залишалося недосяжним.

Для пошуку доказу PSI задіяла власну дослідницьку систему під керівництвом Девіда Туртуряна. У її роботі використовувалися екземпляри ще не випущеної публічно моделі Anthrop­ic. ШІ аналізував наявні математичні результати, пропонував нові підходи та перевіряв проміжні міркування. Вже на третій день система отримала повний доказ.

Ключову роль у перевірці відіграла система Lean, призначена для формальної верифікації математичних доказів. На відміну від звичайної мовної моделі, яка може сформулювати переконливе, але хибне міркування, Lean перевіряє логічну послідовність математичних тверджень за чіткими правилами. Після першого результату дослідницька система двічі вдосконалила доказ — усі версії пройшли формальну перевірку.

Згідно з отриманим результатом, для широкого класу задач із випадковими вхідними даними класичний комп’ютер може приблизно оцінити ймовірність відповіді квантового алгоритму без експоненційного збільшення обчислень. Утім доказ не виключає суттєвих переваг квантових комп’ютерів при вирішенні спеціально структурованих задач — зокрема, розкладання великих чисел на множники.

Роботу ще не опубліковано в рецензованому науковому журналі. Математик Джим Халверсон провів додаткову перевірку доказу, а фізик Фіала Шанахан вивчила його формальне представлення в Lean. Дослідники Гай Блан, Джордан Доктер, Кармен Страссле та Лі-Ян Тан, які раніше довели частковий випадок гіпотези, нині вивчають нову роботу і готують скорочений виклад доказу для математичної спільноти.