Решение задач Международной математической олимпиады доверят ИИ

Оргкомитет Международной математической олимпиады предложил создать конкурс IMO Grand Challenge, посвященный созданию алгоритма, который автоматически решает классические олимпиадные математические задачи. Алгоритм необходимо будет разработать с помощью языка программирования Lean. Пока что правила конкурса уточняются, сообщается на странице IMO Grand Challenge на github.

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

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

Участникам такого конкурса предложат к решению классические олимпиадные задачи (в формальном виде), которые разработанный ими алгоритм будет решать с помощью языка Lean. Алгоритму дается столько же времени, сколько и участникам самой олимпиады (по 4,5 часа на каждый набор из трех задач), при этом в конкурсе не ограничены используемые вычислительные средства. 

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

Пока что неясно, будет ли конкурс отдельным мероприятием или же станет частью самой Международной математической олимпиады. Среди участников оргкомитета, который будет заниматься созданием конкурса, — исследователи из Microsoft Research, Питтсбургского и Стэнфордского университетов и Лондонского имперского колледжа. Они уточнили, что предложенные правила пока что предварительные и пригласили всех желающих принять участие в их обсуждении. 

В этом году на Международной математической олимпиаде первое место с 226 баллами (из 252 возможных) разделили команды из США и Китая. Российская команда набрала 179 баллов.

Елизавета Ивтушок