Компания DeepMind, специализирующаяся на машинном обучении и являющаяся частью Google, объявила 25 июля о значительном прорыве в области искусственного интеллекта (ИИ) для решения математических задач. Их система ИИ успешно решила четыре из шести задач, предложенных школьникам на Международной математической олимпиаде (IMO) 2024 года в Бате, Великобритания. Система предоставила строгие, пошаговые доказательства, которые были оценены двумя ведущими математиками и получили 28 баллов из 42 возможных — всего на один балл меньше диапазона золотой медали.
Джозеф Майерс, математик из Кембриджа, который вместе с обладателем Филдсовской медали Тимом Гауэрсом проверял решения и участвовал в отборе задач для IMO этого года, назвал это достижение «очевидно очень существенным прогрессом».
Системы ИИ и их достижения:
- AlphaGeometry2: Усовершенствованная версия предыдущей системы, которая решила геометрическую задачу менее чем за 20 секунд.
- AlphaProof: Новая система, разработанная для решения задач по алгебре, комбинаторике и теории чисел. AlphaProof успешно решила две задачи по алгебре и одну по теории чисел за три дня. Однако она не смогла решить две задачи по комбинаторике.
Технология и подход
AlphaProof сочетает в себе языковую модель с методом обучения с подкреплением, используя движок ‘AlphaZero’, который ранее успешно применялся для игр, таких как Go. Система была обучена читать и писать доказательства на формальном языке Lean, который используется в популярном среди математиков программном пакете «помощника по доказательствам».
Для обучения языковой модели команда разработала дополнительную сеть, которая пыталась перевести существующий архив из миллиона задач, написанных на естественном языке, в Lean, но без включения решений, написанных человеком. Этот подход позволил AlphaProof научиться доказывать теоремы, не опираясь на готовые человеческие доказательства.
Значение достижения
Пушмит Кохли, вице-президент DeepMind по ИИ для науки, назвал это «ключевой вехой на пути создания продвинутых систем доказательства теорем». Задачи IMO стали своеобразным эталоном прогресса на пути к созданию машин, способных давать доказательства, которые решали бы существенные исследовательские вопросы в математике.
Перспективы и вызовы
Хотя это достижение впечатляет, остается вопрос, смогут ли эти методы быть усовершенствованы до уровня, позволяющего решать исследовательские задачи в математике. Джозеф Майерс отметил, что ключевым вопросом является возможность расширения этого подхода на другие области математики, где может не быть миллиона задач для обучения.
Тим Гауэрс добавил, что во многих случаях AlphaProof, казалось, смогла обеспечить тот творческий скачок, который необходим для решения сложных задач, предоставляя правильный шаг из бесконечно большого диапазона возможностей.
Будущие цели
Следующей значительной целью в этой области является создание ИИ, способного достичь уровня золотой медали на общем тесте IMO, включая вопросы по алгебре, комбинаторике и теории чисел. За достижение этой цели учрежден приз в 5 миллионов долларов, называемый AI Mathematical Olympiad (AIMO) Prize.
Дэвид Сильвер, специалист по компьютерным наукам из DeepMind, подытожил: «Мы достигли того момента, когда ИИ может доказывать не открытые исследовательские проблемы, но по крайней мере задачи, которые очень сложны для лучших молодых математиков в мире».
Это достижение знаменует собой важный шаг в развитии ИИ для математики и открывает новые перспективы для будущих исследований в этой области.
