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