Google DeepMind на шаг ближе к решению сложнейших математических задач 🧠➗

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

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

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

Особенности работы систем:

• AlphaProof сочетает большой языковой ИИ с подходом усиленного обучения, применяемым DeepMind для игры в Go. Система учится формальной математике — методике, где доказательство можно записать как программу, которая выполняется только при правильности. AlphaProof решала три задачи, но на сложнейшую потратила три дня непрерывной работы, тогда как некоторые задачи решались за секунды.
• AlphaGeometry 2 специализируется на геометрии и показала удивительные результаты: задачу она решила всего за 16 секунд, предложив необычный, но элегантный путь решения, напоминающий «ход 37» в исторической победе DeepMind в Go. Система использовала построение окружностей для соединения треугольников и доказательства решения.

Примеры:

• Лёгкая задача AlphaGeometry 2: доказать, что сумма углов, связанных с окружностями и точками в треугольнике, равна 180°. Решение заняло 19 секунд.
• Сложнейшая задача AlphaProof: «Turbo улитка» перемещается по доске с тысячами клеток и скрытыми монстрами, цель — достичь последнего ряда. Задача остаётся нерешённой.

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

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