Програмні алгоритми вже довели, що вони краще за людину як в настільних та комп’ютерних іграх, юриспруденції, так і в повітряному бою винищувачів. На черзі – золота медаль в математиці, яку штучний інтелект хоче завоювати на 61-й Міжнародній математичній олімпіаді. Розробники штучного інтелекту вважають, якщо алгоритм переможе – це означатиме, що він вже близько до людського сприйняття.
«Математична олімпіада, для мене, представляє найскладніший клас проблем, який розумна людина може навчитися вирішувати відносно надійно», – каже представник Microsoft Research Деніел Селсам. Він займається розробкою математичного штучного інтелекту.
Міжнародна математична олімпіада проводиться з 1959 року і в ній беруть участь найкращі представники молоді до університетського віку. Змагання проводиться два дні, учасники мають 4,5 години для вирішення трьох проблем, складність яких збільшується. За кожну проблему вони можуть отримати до семи балів. Переможці везуть додому медалі, а також стають визнаними фахівцями в математичній спільноті і в деяких випадках – видатними математиками.
Задачі на математичній олімпіаді відносно прості і не потребують якоїсь складної математики, навіть алгебра вважається поза межами змагання. Однак при цьому такі проблеми є дуже складними.
Ось, наприклад, п’ята задача з олімпіади 1987 року: «нехай n є цілим числом більшим або рівним 3. Доведіть, що є набір з n точок на площині, щоб відстань між будь-якими двома точками була ірраціональною і кожен набір трьох точок визначав недегеративний трикутник з раціональною площею».
«Ти читаєш питання і думаєш «я не можу це вирішити», – каже золотий медаліст олімпіади 1987 року Кевін Баззард. – Це надзвичайно складні питання, які доступні школярам, якщо вони складуть всі знайомі їм ідеї в геніальне рішення».
Вирішення проблем Міжнародної математичної олімпіади, як вважається, часто потребує прозріння та інтуїції, що неможливо для сучасного штучного інтелекту.
Розробники математичного штучного інтелекту взяли за основу програму Lean, яку Microsoft вперше запустила в 2013 році і автором якої є Леонардо де Мура. Це асистент доказів, який перевіряє математичну роботу і виконує нудні задачі по доказу її вірності.
Для перемоги в математичній олімпіаді Lean потрібно вивчити багато математичних концепцій, а також навчитися поєднувати ці знання у незвичний спосіб. Вирішити ці проблеми планується за допомогою успішного підходу – побудові дерева рішень і слідування по ньому поки не знайдеться вірне рішення.
«Ключовий крок в багатьох проблемах на олімпіаді – «погратися» з ними, шукаючи шаблони, – каже Селмас. – Звісно, це не очевидно як сказати комп’ютеру, щоб він «погрався».
