Несколько математиков из DeepMind представили статью в Nature, описывающую гибридный математический решатель AlphaGeometry (AG). Исследователи ввели 30 геометрических задач международной математической олимпиады, составленных с 2000 по 2022 год. Система решила 25; исторически за тот же период обычный золотой медалист решил 25,9. Предыдущий самый сильный геометрический решатель, разработанной в 1970-х годах, сумел решить лишь 10 задач.
За последние несколько лет Google DeepMind инициировали ряд проектов, исследующих применение ИИ в математике. AG - гибридная, нейро-символьная система, сочетающая в себе языковую модель и символьный движок для рассуждения.
В отличие от всех предыдущих геометрических решателей, AG имеет две особенности. Во-первых, AG обучена только на синтетических данных - 100 миллионов геометрических доказательств - без использования человеческих примеров. Это позволило преодолеть нехватку данных обучения, решений геометрических задач, доказанных человеком и переведенных на машиночитаемый язык.
Во-вторых, вначале работает символьный решатель. Если он стопорится, то нейронная сеть ищет способы дополнения доказательства. Цикл продолжался до тех пор, пока не найдено решение или не закончилось время (четыре с половиной часа).
Комментарии математиков прямо скажем, смешанные. Конечно, это большое достижение в целом для науки. Но вот переносимость предложенного подхода на другие области вызывает вопросы. Кроме того, геометрия - это пространственное воображение. AG вообще ничего не воображает, она просто пересчитывает картинки в набор цифр (именно поэтому использованы синтетические данные). Ну и последнее. Учитель одного из авторов статьи, так и сказал - доказательство некрасивое, не изящное. Все-таки математики знают толк в красоте.
#от_редактора #AlphaGeometry
За последние несколько лет Google DeepMind инициировали ряд проектов, исследующих применение ИИ в математике. AG - гибридная, нейро-символьная система, сочетающая в себе языковую модель и символьный движок для рассуждения.
В отличие от всех предыдущих геометрических решателей, AG имеет две особенности. Во-первых, AG обучена только на синтетических данных - 100 миллионов геометрических доказательств - без использования человеческих примеров. Это позволило преодолеть нехватку данных обучения, решений геометрических задач, доказанных человеком и переведенных на машиночитаемый язык.
Во-вторых, вначале работает символьный решатель. Если он стопорится, то нейронная сеть ищет способы дополнения доказательства. Цикл продолжался до тех пор, пока не найдено решение или не закончилось время (четыре с половиной часа).
Комментарии математиков прямо скажем, смешанные. Конечно, это большое достижение в целом для науки. Но вот переносимость предложенного подхода на другие области вызывает вопросы. Кроме того, геометрия - это пространственное воображение. AG вообще ничего не воображает, она просто пересчитывает картинки в набор цифр (именно поэтому использованы синтетические данные). Ну и последнее. Учитель одного из авторов статьи, так и сказал - доказательство некрасивое, не изящное. Все-таки математики знают толк в красоте.
#от_редактора #AlphaGeometry