Вперше в історії штучний інтелект досяг рівня виконання завдань, достатнього для отримання медалі на Міжнародній математичній олімпіаді (IMO). Хоча нагорода не була офіційно присуджена через правила змагань, система AI під назвою AlphaProof продемонструвала рівень, який дозволив би отримати срібну медаль на MMO 2024. Це знакове досягнення, описане в статті, опублікованій в журналі Nature, демонструє швидкий прогрес ШІ у вирішенні складних математичних задач.
Розроблений Google DeepMind, AlphaProof відрізняється від інших великих мовних моделей (LLM), які, хоча й здатні розв’язувати математичні проблеми, часто ставляться під сумнів через потенційні приховані помилки в їхніх міркуваннях. AlphaProof виділяється тим, що гарантує 100% точність. Цього видатного результату можна досягти завдяки унікальному навчальному середовищу: програмному забезпеченню Lean для перевірки теорем. Lean діє як суворий вчитель, ретельно перевіряючи кожен логічний крок процесу вирішення проблем AlphaProof, щоб забезпечити незаперечні результати.
Навчання генія математики
Створення такого математично обдарованого штучного інтелекту вимагало триетапного процесу навчання:
-
Почати основи: AlphaProof вперше занурився у масивний набір даних із приблизно 300 мільярдів токенів, включаючи загальний код і математичний текст. Це відкриття дало йому широке розуміння математичної мови, логіки та структур програмування.
-
Навчання від експертів: Штучний інтелект був представлений з 300 000 ретельно розроблених математичних доказів, написаних експертами, і все в середовищі Lean. Цей етап прищепив AlphaProof глибоке розуміння того, як математики будують суворі аргументи.
-
Масштабне навчання: Останнім і вирішальним кроком було дати AlphaProof величезну кількість домашніх завдань: розв’язати 80 мільйонів формальних математичних завдань. Використовуючи Reinforcement Reinforcement (RL), система отримувала винагороду за кожне успішне підтвердження, заохочуючи її вдосконалювати свої стратегії вирішення проблем шляхом проб і помилок у колосальному масштабі.
Для особливо складних проблем AlphaProof використовував метод під назвою Test-Time RL (TTRL). Цей інноваційний метод передбачає створення та розв’язання мільйонів спрощених версій цільової проблеми, доки не буде знайдено рішення, схоже на розбивання складної головоломки на керовані частини.
«Наша робота демонструє, що масштабне навчання на основі досвіду реального світу призводить до створення агентів зі складними математичними стратегіями міркування, прокладаючи шлях до надійних інструментів штучного інтелекту для вирішення складних математичних проблем», — пишуть дослідники.
Поза змаганнями: потужний інструмент для математиків
Можливості AlphaProof виходять далеко за межі простого вирішення проблем; він має величезний потенціал, щоб допомогти людям-математикам. Ретельно перевіряючи докази та виявляючи незначні помилки, AlphaProof може служити незамінним інструментом для забезпечення точності та прискорення математичних відкриттів. Уявіть собі, як він допомагає математикам формулювати нові теорії, пропонувати альтернативні підходи або розкривати приховані зв’язки в складних математичних структурах.
Це проривне досягнення є значним прогресом у здатності штучного інтелекту вирішувати проблеми абстрактного мислення, які раніше вважалися сферою діяльності людей. У міру розвитку таких систем штучного інтелекту, як AlphaProof, ми можемо очікувати дедалі складніших застосувань у математиці та інших галузях, розсуваючи межі можливого в обох сферах.
