AI на Міжнародній математичній олімпіаді: як AlphaProof і AlphaGeometry 2 досягли рівня срібної медалі

Математичне мислення є важливим аспектом людських когнітивних можливостей, що сприяє прогресу в наукових відкриттях і технологічних розробках. При розробці штучного інтелекту, який дорівнює людському мисленню, наділення штучного інтелекту можливостями математичного мислення є важливим. Хоча сучасні системи штучного інтелекту можуть вирішувати базові математичні задачі, вони мають труднощі з комплексним мисленням, необхідним для вищої математики, наприклад, алгебри та геометрії. Однак ця ситуація може змінитися, оскільки Google DeepMind зробив значний крок у розвитку математичного мислення штучного інтелекту. Цей прорив стався на Міжнародній математичній олімпіаді (IMO) 2024. Заснована у 1959 році, IMO є найстарішою та найпрестижнішою математичною олімпіадою, яка пропонує завдання з алгебри, комбінаторики, геометрії та теорії чисел для школярів усього світу. Кожного року команди молодих математиків змагаються у вирішенні шести дуже складних завдань. Цього року Google DeepMind представив дві системи штучного інтелекту: AlphaProof, який спеціалізується на формальному математичному мисленні, та AlphaGeometry 2, який спеціалізується на вирішенні геометричних завдань. Ці системи штучного інтелекту вирішили чотири з шести завдань, показавши результат на рівні срібної медалі. У цій статті ми розглянемо, як ці системи працюють для вирішення математичних завдань.

AlphaProof: Об’єднання штучного інтелекту та формальної мови для математичного доведення

AlphaProof є системою штучного інтелекту, розробленою для доведення математичних тверджень за допомогою формальної мови Lean. Він поєднує Gemini, попередньо навчену мовну модель, з AlphaZero, алгоритмом навчання з підкріпленням, відомим своєю здатністю освоювати шахи, шогі та ґо.

Gemini перекладає природні мовні завдання в формальні, створюючи бібліотеку завдань з різним рівнем складності. Це служить двом цілям: переклад природної мови в формальну для верифікації математичних доведень та використання передбачувальних можливостей Gemini для генерації списку можливих рішень з точністю формальної мови.

Коли AlphaProof зустрічає завдання, він генерує потенційні рішення та шукає кроки доведення в Lean для верифікації або спростування цих рішень. Це по суті нейро-символічний підхід, де нейронна мережа, Gemini, перекладає природні мовні інструкції в символічну формальну мову Lean для доведення або спростування твердження. Аналогічно до механізму самозігрівання AlphaZero, де система вчиться, граючи в ігри проти себе, AlphaProof тренується, намагаючись довести математичні твердження. Кожна спроба доведення уточнює мовну модель AlphaProof, з успішними доведеннями, що посилюють здатність системи вирішувати складніші завдання.

Для Міжнародної математичної олімпіади (IMO) AlphaProof був тренований на доведенні або спростуванні мільйонів завдань різних рівнів складності та математичних тем. Ця підготовка тривала під час змагання, де AlphaProof уточнював свої рішення до тих пір, поки не знайшов повні відповіді на завдання.

AlphaGeometry 2: Інтеграція великих мовних моделей та символічного штучного інтелекту для вирішення геометричних завдань

AlphaGeometry 2 є останньою ітерацією серії AlphaGeometry, розробленої для вирішення геометричних завдань з підвищеною точністю та ефективністю. Будуючи на основі свого попередника, AlphaGeometry 2 використовує нейро-символічний підхід, який поєднує великі мовні моделі з символічним штучним інтелектом. Ця інтеграція поєднує логіку, засновану на правилах, з передбачувальною здатністю нейронних мереж для ідентифікації допоміжних точок, необхідних для вирішення геометричних завдань. Велика мовна модель AlphaGeometry передбачає нові геометричні конструкції, тоді як символічний штучний інтелект застосовує формальну логіку для генерації доведень.

Коли AlphaGeometry зустрічає геометричне завдання, його велика мовна модель оцінює численні можливості, передбачаючи конструкції, необхідні для вирішення завдання. Ці передбачення служать цінними підказками, спрямовуючи символічний двигун до точних висновків та наближення до рішення. Цей інноваційний підхід дозволяє AlphaGeometry вирішувати складні геометричні завдання, які виходять за рамки традиційних сценаріїв.

Одним із ключових покращень у AlphaGeometry 2 є інтеграція великої мовної моделі Gemini. Ця модель тренується з нуля на значно більшій синтетичній даних, ніж її попередник. Це інтенсивне тренування дозволяє їй вирішувати складніші геометричні завдання, включаючи завдання, пов’язані з рухом об’єктів та рівняннями кутів, відношень або відстаней. Крім того, AlphaGeometry 2 має символічний двигун, який працює в два порядки швидше, дозволяючи йому досліджувати альтернативні рішення з безпрецедентною швидкістю. Ці вдосконалення роблять AlphaGeometry 2 потужним інструментом для вирішення складних геометричних завдань, встановлюючи новий стандарт у галузі.

AlphaProof і AlphaGeometry 2 на IMO

Цього року на Міжнародній математичній олімпіаді учасникам були запропоновані шість різноманітних завдань: два з алгебри, одне з теорії чисел, одне з геометрії та два з комбінаторики. Дослідники Google переклали ці завдання на формальну математичну мову для AlphaProof і AlphaGeometry 2. AlphaProof вирішив два алгебраїчні завдання та одне завдання з теорії чисел, включаючи найскладніше завдання змагання, яке вирішили лише п’ять учасників цього року. Тим часом AlphaGeometry 2 успішно вирішив геометричне завдання, хоча не зміг вирішити два завдання з комбінаторики.

Кожне завдання на IMO оцінюється в 7 балів, що складає максимум 42 бали. AlphaProof і AlphaGeometry 2 набрали 28 балів, досягнувши ідеальних результатів на завданнях, які вони вирішили. Це поставило їх на високому рівні категорії срібної медалі. Поріг золотої медалі цього року становив 29 балів, який досягли 58 учасників з 609 учасників.

Наступний крок: Природна мова для математичних завдань

AlphaProof і AlphaGeometry 2 продемонстрували вражаючі досягнення у вирішенні математичних завдань. Однак ці системи все ще залежать від експертів, які перекладають математичні завдання на формальну мову для обробки. Крім того, залишається невідомим, як ці спеціалізовані математичні навички можуть бути інтегровані в інші системи штучного інтелекту, наприклад, для дослідження гіпотез, тестування інноваційних рішень давніх проблем та ефективного управління часоємкими аспектами доведень.

Для подолання цих обмежень дослідники Google розробляють систему природної мови, засновану на Gemini та їхніх останніх дослідженнях. Ця нова система спрямована на розвиток можливостей вирішення завдань без потреби перекладу на формальну мову та призначена для безшовної інтеграції з іншими системами штучного інтелекту.

Висновок

Виступ AlphaProof і AlphaGeometry 2 на Міжнародній математичній олімпіаді є помітним кроком вперед у розвитку можливостей штучного інтелекту вирішувати складні математичні завдання. Обидві системи продемонстрували результат на рівні срібної медалі, вирішивши чотири з шести складних завдань, продемонструвавши значні досягнення у формальному доведенні та вирішенні геометричних завдань. Незважаючи на свої досягнення, ці системи штучного інтелекту все ще залежать від людського входу для перекладу завдань на формальну мову та стикаються з труднощами інтеграції з іншими системами штучного інтелекту. Майбутні дослідження спрямовані на подальше вдосконалення цих систем, потенційно інтегруючи природну мову для розширення їхніх можливостей у вирішенні математичних завдань.