Системы искусственного интеллекта AlphaProof и AlphaGeometry 2 достигли уровня серебряной медали на Международной математической олимпиаде (IMO), решив четыре из шести задач.
IMO — самое престижное соревнование для молодых математиков, которое проводится ежегодно с 1959 года. Участники тратят тысячи часов на подготовку к решению сложных задач по алгебре, комбинаторике, геометрии и теории чисел. Многие победители Филдсовской премии, одной из самых высоких наград в математике, участвовали в этой олимпиаде.
Результаты ИИ оценивали ведущие математики: профессор сэр Тимоти Гауэрс (Timothy Gowers), золотой медалист IMO и лауреат Филдсовской премии, и доктор Джозеф Майерс (Joseph Myers), двукратный золотой медалист IMO и председатель Комитета по отбору задач ИМО 2024.
Гауэрс отметил: «Способность приложения создавать неочевидные конструкции поражает и значительно превосходит то, что я считал современным уровнем развития».
AlphaProof решила две алгебраические задачи и одну из теории чисел, определив ответ и доказав его правильность. Система справилась с самой сложной задачей олимпиады, которую решили только пять участников нынешней IMO. AlphaGeometry 2 доказала геометрическую задачу, тогда как две комбинаторные задачи остались нерешенными.
AlphaProof — это система, которая самостоятельно учится доказывать математические утверждения на формальном языке Lean. Она сочетает предварительно обученную языковую модель с алгоритмом обучения с подкреплением AlphaZero, который ранее освоил шахматы, сёги и го.
AlphaGeometry 2 является улучшенной версией предыдущей системы. Ее языковая модель основана на Gemini и училась на значительно большем количестве синтетических данных. Это позволило системе решать более сложные геометрические задачи, в частности о движении объектов и уравнениях углов, соотношений или расстояний.
Разработчики продолжают исследовать различные подходы к совершенствованию математического мышления ИИ. Они стремятся создать будущее, где математики будут сотрудничать с инструментами ИИ для исследования гипотез, поиска новых подходов к решению давних проблем и быстрого выполнения трудоемких элементов доказательств.
Источник: Deepmind.google