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

25 июля компания официально объявила об этом достижении. Два ведущих математика, включая лауреата Филдсовской премии, проверили решения и признали их корректными. Факт налицо: алгоритм показал результат, сопоставимый с лучшими молодыми умами планеты.

ИИ выходит на уровень олимпийских чемпионов по математике

«Это, несомненно, очень существенный прогресс», — заявил Джозеф Майерс, математик из Кембриджа, участвовавший в проверке. Задачи IMO давно стали для разработчиков своеобразным Священным Граалем — «грандиозным вызовом», который проверяет, может ли машина не только вычислять, но и логически рассуждать на высочайшем уровне.

«Это первый раз, когда система смогла достичь результатов на уровне медали», — подчеркнул вице-президент DeepMind Пушмит Кохли. Фраза звучит весомо, не правда ли?

Скорость прогресса поражает

Еще в январе система AlphaGeometry от той же DeepMind блеснула в задачах по евклидовой геометрии. Но сейчас речь идет о качественном скачке: новый дуэт моделей атаковал алгебру, теорию чисел и комбинаторику — области, которые математики часто считают более сложными, чем геометрия.

Интересно, что за создание ИИ, способного выиграть золотую медаль IMO по всем направлениям, даже назначена премия в $5 млн (AIMO Prize). Хотя результат DeepMind ее не получает из-за технических условий конкурса, сам факт такого приближения говорит о многом.

Как же они это сделали? Для геометрии использовали улучшенную версию AlphaGeometry2, которая щелкает задачи за 20 секунд. А для остального создали принципиально новую систему — AlphaProof. Она потратила три дня на решение двух алгебраических задач и одной по теории чисел. Напомню, у живых участников на все про все — два тура по 4,5 часа. Правда, две комбинаторные задачи остались неподвластны машине. Выходит, ее гениальность пока имеет свои границы.

Как работает AlphaProof? Без учителя, но с упрямством

В основе AlphaProof — гибрид языковой модели и обучения с подкреплением (знаменитый движок AlphaZero, покоривший го). Система училась методом проб и ошибок, проверяя свои ходы на формальном языке программирования Lean, который популярен среди математиков для верификации доказательств.

Самое интересное: команда сознательно не кормила модель готовыми человеческими решениями. Вместо этого они попытались перевести миллион задач с естественного языка на Lean, оставив решения «за кадром». «Мы хотели понять, можем ли мы научиться доказывать, даже если мы не обучались на доказательствах, написанных людьми?» — говорит один из руководителей разработки. По сути, они заставили ИИ изобретать математику самостоятельно, играя самому с собой, как в той же го. И это сработало.

Волшебный ключ и темная комната

Многие олимпиадные задачи обладают свойством «волшебного ключа»: задача кажется неприступной, пока не найдешь одну изящную идею, которая открывает ее мгновенно. По словам Тима Гауэрса, проверявшего решения, иногда AlphaProof, кажется, находил такой ключ, делая правильный шаг из бесконечного множества возможных.

Но как именно он к нему приходил? Этот процесс остается внутри «черного ящика». И главный вопрос теперь: поможет ли этот метод в реальной, не олимпиадной, исследовательской математике? «Можно ли распространить эти методы на другие виды математики, где может и не быть миллиона задач для обучения?» — задается вопросом Джозеф Майерс. Пока ответа нет. Машина нашла ключи к известным дверям. Но сможет ли она построить новые? Вот в чем загадка.