Google DeepMind приблизился к решению задач высшей математики 🤖📐

Хотя компьютеры всегда были быстрее человека в арифметике, настоящая вершина формальной математики до сих пор оставалась прерогативой человека. Но исследователи Google DeepMind сделали шаг к тому, чтобы искусственный интеллект мог конкурировать с лучшими математиками мира.

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

После проверки ответов профессором Тимоти Гауэрсом, обладателем Медали Филдса и золотой медали олимпиады, системы DeepMind набрали 28 из 42 баллов, что соответствует серебряной медали — всего на один балл меньше золотой. Особенность ИИ заключалась в том, что там, где он решал задачи, решения были безупречны, а две из шести задач система не смогла даже начать решать.

Интересно, что DeepMind не ограничивался по времени: если студенты олимпиады имеют 9 часов на все задачи, системы работали круглосуточно и занимали три дня на одну из самых сложных задач, тогда как другую решили за секунды.

Как работают системы

AlphaProof сочетает большую языковую модель (как в чат-ботах) с подходом «обучения с подкреплением», похожим на тот, что DeepMind использовал в игре Go. Она опирается на формальную математику, позволяющую писать доказательства как программы, которые запускаются только если доказательство верно. Система учится, анализируя огромное количество задач на английском языке, генерируя формальные доказательства.

AlphaGeometry 2 ориентирована на геометрию. Она решала свои задачи невероятно быстро — например, одну задачу за 16 секунд, выбрав необычный, но эффективный путь решения. Как отмечает Гауэрс, её вывод был коротким и «человеческим», в отличие от громоздких доказательств некоторых компьютерных программ.

Примеры задач

AlphaGeometry 2: задача с треугольником ABC и различными точками, связанная с окружностями и углами — решена за 19 секунд.

AlphaProof: задача с улиткой Turbo на огромной доске с монстрами — пока не решена, так как требует стратегического планирования для гарантированного прохождения всех рядов.

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