Модели искусственного интеллекта могут легко создавать эссе и другие типы текстов. Однако они далеко не так хороши в решении математических задач, которые, как правило, требуют логического рассуждения — то, что выходит за рамки возможностей большинства современных систем искусственного интеллекта.
Но это, наконец, может измениться. Google DeepMind заявляет, что обучила две специализированные системы искусственного интеллекта решать сложные математические задачи, требующие продвинутого мышления. Системы под названием AlphaProof и AlphaGeometry 2 работали вместе, чтобы успешно решить четыре из шести задач Международной математической олимпиады (IMO) этого года, престижного соревнования для старшеклассников. Они выиграли эквивалент серебряной медали.
Это первый случай, когда какая-либо система искусственного интеллекта достигла такого высокого уровня успеха в решении подобных задач. “Это большой прогресс в области машинного обучения и искусственного интеллекта”, - говорит Пушмит Кохли, вице-президент по исследованиям Google DeepMind, который работал над проектом. “До сих пор не было разработано такой системы, которая могла бы решать проблемы с таким успехом и с таким уровнем универсальности”.
Есть несколько причин, по которым системам искусственного интеллекта трудно решать математические задачи, требующие углубленного рассуждения. Эти типы задач часто требуют формирования абстракций и их использования. Они также включают в себя сложное иерархическое планирование, а также постановку подцелей, отслеживание изменений и поиск новых путей. Все это является сложной задачей для ИИ.
“Часто бывает проще обучить модель математике, если у вас есть способ проверить ее ответы (например, на формальном языке), но в Интернете сравнительно меньше формальных математических данных по сравнению с естественным языком в свободной форме (неформальный язык)”, - говорит Кэти Коллинз, исследователь из Кембриджского университета, которая специализируется на математике и искусственном интеллекте, но не участвовала в проекте.
Целью Google DeepMind было устранить этот пробел при создании AlphaProof - системы, основанной на обучении с подкреплением, которая обучается доказывать математические утверждения на формальном языке программирования Lean. The key - это версия искусственного интеллекта Gemini от DeepMind, которая точно настроена для автоматического перевода математических задач, сформулированных на естественном неформальном языке, в формальные утверждения, которые ИИ легче обрабатывать. Таким образом была создана большая библиотека формальных математических задач различной степени сложности.
Автоматизация процесса перевода данных на формальный язык - большой шаг вперед для математического сообщества, говорит Венда Ли, преподаватель гибридного искусственного интеллекта в Эдинбургском университете, которая выступила рецензентом исследования, но не участвовала в проекте.
“Мы можем быть гораздо более уверены в правильности опубликованных результатов, если они смогут сформулировать эту систему доказательств, и она также может стать более совместной”, - добавляет он.
Модель Gemini работает вместе с AlphaZero - моделью обучения с подкреплением, которую Google DeepMind разработала для освоения таких игр, как го и шахматы, — чтобы доказать или опровергнуть миллионы математических задач. Чем больше проблем было успешно решено, тем лучше AlphaProof справлялся с задачами возрастающей сложности.
Несмотря на то, что AlphaProof был обучен решать задачи по широкому кругу математических тем, AlphaGeometry 2 — улучшенная версия системы, анонсированная Google DeepMind в январе, — была оптимизирована для решения задач, связанных с перемещениями объектов и уравнениями, включающими углы, соотношения и расстояния. Поскольку он был обучен работе со значительно большим количеством синтетических данных, чем его предшественник, он смог справиться с гораздо более сложными геометрическими вопросами.
Чтобы проверить возможности систем, исследователи Google DeepMind поручили им решить шесть задач, поставленных перед людьми, участвующими в IMO в этом году, и доказать, что ответы были правильными. AlphaProof решил две задачи по алгебре и одну задачу по теории чисел, одна из которых была самой сложной на конкурсе. AlphaGeometry 2 успешно решила геометрический вопрос, но два вопроса по комбинаторике (области математики, ориентированной на подсчет и упорядочивание объектов) остались нерешенными.
“Как правило, AlphaProof намного лучше справляется с алгеброй и теорией чисел, чем комбинаторика”, - говорит Алекс Дэвис, инженер-исследователь из команды AlphaProof. “Мы все еще работаем над тем, чтобы понять, почему это так, и надеемся, что это приведет нас к улучшению системы”.
Два известных математика, Тим Гауэрс и Джозеф Майерс, проверили представленные системы. Они присудили каждому из четырех правильных ответов полные оценки (семь из семи), что дало системам в общей сложности 28 баллов из максимальных 42. Участник-человек, набравший этот балл, будет награжден серебряной медалью и просто не получит золото, пороговый уровень для которого начинается с 29 баллов.
Это первый случай, когда какая-либо система искусственного интеллекта смогла достичь показателей медального уровня по вопросам IMO. “Как математик, я нахожу это очень впечатляющим и значительным скачком по сравнению с тем, что было возможно ранее”, - сказал Гауэрс во время пресс-конференции.
Майерс согласился с тем, что математические ответы систем представляют собой существенный прогресс по сравнению с тем, чего мог достичь искусственный интеллект ранее. “Будет интересно посмотреть, как все масштабируется и можно ли это сделать быстрее, и может ли это распространиться на другие виды математики”, - сказал он.
Создание систем искусственного интеллекта, способных решать более сложные математические задачи, может проложить путь к захватывающему сотрудничеству человека и искусственного интеллекта, помогая математикам как решать, так и изобретать новые виды задач, говорит Коллинз. Это, в свою очередь, могло бы помочь нам узнать больше о том, как мы, люди, справляемся с математикой.
“Мы все еще многого не знаем о том, как люди решают сложные математические задачи”, - говорит она.
автор Рианнон Уильямс
