Quanta magazine: компьютеры готовятся побеждать на мировой олимпиаде по математике

Ученые-информатики пытаются создать систему искусственного интеллекта, которая может выиграть золотую медаль на главном в мире математическом соревновании.

Автор: Кевин Хартнетт

61-я Международная математическая олимпиада, или IMO, вот-вот начнётся. И она может войти в историю как минимум по двум причинам: из-за пандемии COVID-19 это первый раз, когда мероприятие проводится удаленно, и, возможно, это последний раз, когда искусственный интеллект не участвует в соревнованиях.

Действительно, исследователи рассматривают IMO как идеальный полигон для испытаний машин, способных мыслить как люди. Если система искусственного интеллекта может преуспеть здесь, она будет соответствовать важному аспекту человеческого познания.

«Для меня IMO представляет собой сложнейший класс проблем, которые умные люди могут научить решать достаточно надежно» — говорит Дэниел Сельсам из Microsoft Research. Сельсам — основатель IMO Grand Challenge, цель которого — обучить систему искусственного интеллекта, чтобы выиграть золотую медаль на главном в мире математическом соревновании.

С 1959 года IMO собирает лучших студентов-математиков в мире. В каждый из двух дней соревнований участникам дается четыре с половиной часа, чтобы решить три задачи возрастающей сложности. Можно заработать до семи очков за задачу, а лучшие забирают домой медали, как на Олимпийских играх. Самые титулованные участники IMO становятся легендами математического сообщества. Некоторые из них стали выдающимися математиками-исследователями.

Задачи IMO просты, но только в том смысле, что они не требуют каких-либо сложных расчётов. В остальном же они чертовски трудны. Например, вот пятая задача соревнований 1987 года на Кубе:

Пусть n будет целым числом, большим или равным 3. Докажите, что существует набор из n точек на плоскости, такой, что расстояние между любыми двумя точками иррационально, и каждый набор из трех точек определяет правильный треугольник с рациональной площадью.

Как и многие другие задачи IMO, эта может сначала показаться невозможной для решения.

«Вы читаете вопросы и думаете: «я не могу этого сделать» — говорит Кевин Баззард из Имперского колледжа Лондона, член команды IMO Grand Challenge и золотой медалист IMO 1987 года. «Это чрезвычайно сложные вопросы, которые доступны для решения школьникам, если они блестяще соединят воедино все свои идеи».

Для меня IMO представляет собой сложнейший класс задач, которые умных людей можно научить решать надежно.

Решение задач IMO часто требует озарения — первоклассного первого шага, который сегодня весьма сложен для ИИ – быть может и невозможен.

Например, одним из старейших результатов по математике является доказательство Евклида 300 г. до н.э. о том, что существует бесконечное множество простых чисел. Оно начинается с признания того факта, что вы всегда можете найти новое простое число, умножив все известные простые числа и прибавив 1. Доказательство, которое следует ниже, простое, но придумать начальную идею было искусством.

«Вы не можете заставить компьютеры понять эту идею» — сказал Баззард. По крайней мере, пока.

Команда IMO Grand Challenge использует программу под названием Lean, впервые запущенную в 2013 году исследователем Microsoft по имени Леонардо де Моура. Lean — это «помощник по доказательству», который проверяет работу математиков и автоматизирует некоторые утомительные части написания доказательства.

Де Моура и его коллеги хотят использовать Lean в качестве «решателя», способного разработать собственные доказательства задач IMO. Но на данный момент он даже не может понять концепции, связанные с некоторыми из этих задач. Чтобы добиться большего, нужно изменить две вещи.

Во-первых, Lean нужно лучше выучить математику. Программа использует математическую библиотеку mathlib, которая постоянно растет. Сегодня она содержит почти все, что может знать математик к концу второго года обучения в колледже, но с некоторыми элементарными пробелами, которые имеют значение для IMO.

Вторая, более серьезная проблема — научить Lean управлять своими знаниями. Команда IMO Grand Challenge хочет научить Lean подходить к математическому доказательству так, как другие системы ИИ уже успешно подходят к сложным играм, таким как шахматы и го, — следуя древу решений в поисках лучшего хода.

«Если мы сможем заставить компьютер реализовать эту блестящую идею, просто изучая тысячи и тысячи идей и отвергая их все, пока он не наткнется на правильную, возможно, мы сможем ответить на Большой вызов IMO» — говорит Баззард.

Но что такое математические идеи? На удивление сложно дать определение. На высоком уровне многое из того, что делают математики, когда они подходят к новой задаче, невыразимо.

«Ключевым шагом во многих задачах IMO является игра с этим и поиск закономерностей» — говорит Сельсам. Конечно, не очевидно, как дать указание компьютеру «поиграться» с проблемой.

На низком уровне математические доказательства — это просто серия очень конкретных логических шагов. Исследователи IMO могли бы попытаться обучить Lean, показав ему все детали предыдущих доказательств IMO. Но на детальном уровне отдельные доказательства становятся слишком специализированными для конкретной задачи.

«Нет ничего, что помогло бы решить следующую задачу» — отмечают Сельсам.

Это чрезвычайно сложные вопросы, которые доступны школьникам, если они блестяще соединят воедино все известные им идеи.

Чтобы помочь с этим, команде IMO Grand Challenge нужны математики, которые должны написать подробные формальные доказательства предыдущих задач IMO. Затем команда возьмет эти доказательства и попытается выделить методы или стратегии, которые приводят к решениям. Далее они должны обучить систему искусственного интеллекта поиску среди этих стратегий «выигрышной» комбинации, которая позволит решать задачи IMO, с которыми она никогда раньше не сталкивалась. Уловка, замечает Сельсам, заключается в том, что выигрывать по математике намного сложнее, чем выигрывать даже в самых сложных настольных играх. В этих играх, по крайней мере, вы знаете правила.

«Например, в го цель состоит в том, чтобы найти лучший ход, тогда как в математике цель — найти лучшую игру, а затем найти лучший ход в этой игре» — говорит специалист.

В настоящее время грандиозный вызов IMO — это шедевр. Если бы Lean участвовал в конкурсе в этом году, «мы, вероятно, получили бы ноль баллов» — признаёт де Моура.

Но у исследователей есть несколько критериев, которые они пытаются выполнить до мероприятия следующего года. Они планируют заполнить пробелы в mathlib, чтобы Lean мог понимать все вопросы. Они также надеются получить подробные формальные доказательства десятков предыдущих задач IMO, которые положат начало процессу предоставления Lean базового сценария, из которого можно будет извлечь пользу.

Пока золотая медаль для машины все еще недосягаема, но, по крайней мере, Lean готов вступить в гонку.

«Прямо сейчас происходит много всего, но нет ничего особенно конкретного» — подчёркивает Сельсам. «[В следующем] году нас ждёт настоящий старт».

Оригинал: Quanta Magazine

Похожие Записи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Последние <span>истории</span>

Поиск описаний функциональности, введя ключевое слово и нажмите enter, чтобы начать поиск.