AlphaProof: нейросеть-математик или модель от Google, решающая олимпиадные задачи

Пресс-служба DeepMind (подразделения AI в Google) опубликовала статью, посвященную новому прорыву в области искусственного интеллекта: созданию модели, способной решать сложнейшие математические задачи на уровне серебряного призера Международной Математической Олимпиады (ММО, англ. «IMO»).

Публикация вызвала широкий резонанс в научном сообществе и за его пределами. Давайте разберемся, действительно ли AlphaProof — это прорыв к «мыслящему» ИИ, или за громкими заявлениями скрывается нечто иное?

Цитаты сообщений DeepMind в Твиттере:

Представляем первый ИИ, способный решать задачи ММО на уровне серебряного медалиста. Он сочетает в себе AlphaProof — новую модель для формальных доказательств, и AlphaGeometry 2 — улучшенную версию нашей предыдущей системы

Наша система решила 4 из 6 задач ММО этого года, охватывающих алгебру, комбинаторику, геометрию и теорию чисел, набрав 28 баллов — что эквивалентно серебряной медали

AlphaProof использует язык Lean для создания доказательств. Модель сочетает в себе языковую модель и алгоритм обучения с подкреплением AlphaZero

AlphaGeometry 2 — нейро-символическая система. Ее языковая модель, основанная на Gemini, обучена на большем объеме синтетических данных, что позволяет ей решать более сложные задачи

AlphaProof и AlphaGeometry 2: тандем, покоривший олимпиаду

DeepMind представила две модели: AlphaProof, специализирующуюся на формальном математическом доказательстве, и AlphaGeometry 2, усовершенствованную версию предыдущей системы решения геометрических задач. Совместно эти модели решили 4 из 6 задач ММО 2024 года, что сопоставимо с результатами лучших участников-людей.

Как работает AlphaProof?

AlphaProof использует язык формальной логики Lean для записи и проверки математических доказательств. Модель обучается на огромном наборе задач, переведенных с естественного языка на Lean. В процессе обучения AlphaProof использует алгоритм AlphaZero, тот самый, что ранее научился играть в шахматы, го и сёги на уровне, превосходящем человеческий.

AlphaGeometry 2:

AlphaGeometry 2 — это нейро-символическая система, обученная на значительно большем наборе данных, чем ее предшественник. Модель способна решать задачи, связанные с движением объектов, углами, соотношениями и расстояниями, демонстрируя впечатляющую скорость и точность.

Что это значит для будущего?

Успех AlphaProof и AlphaGeometry 2 — несомненно, важная веха в развитии ИИ. Ведь речь идет не просто о решении абстрактных задач, а о покорении вершины, ранее доступной лишь человеческому интеллекту — Международной Математической Олимпиады.

Важно понимать, что эти модели не «мыслят» как математики-люди, а скорее действуют как невероятно талантливые и быстро обучаемые ученики. Они анализируют огромные объемы данных, выявляют закономерности и учатся применять правила и алгоритмы для решения сложнейших задач.

Тем не менее, подобные системы обладают колоссальным потенциалом. Представьте себе мир, где рутинная работа математиков автоматизирована, где доказательства проверяются за считанные секунды, а новые гипотезы рождаются при активном участии ИИ.

Возможно, в будущем мы увидим, как AlphaProof и его последователи не просто помогают решать задачи, но и самостоятельно выдвигают новые математические теории, открывая перед человечеством неизведанные горизонты науки.