Команда из двух новых систем ИИ набрала на один балл меньше золота на глобальном математическом конкурсе для одаренных студентов
Хотя компьютеры были созданы для выполнения математических вычислений быстрее, чем человек, высший уровень формальной математики остается исключительно человеческой сферой. Однако прорыв исследователей из Google DeepMind приблизил системы ИИ к тому, чтобы превзойти лучших человеческих математиков в их собственной игре.
Две новые системы — AlphaProof и AlphaGeometry 2, работали вместе, чтобы решать задачи Международной математической олимпиады (IMO), глобального математического конкурса для школьников, который проводится с 1959 года.
Олимпиада состоит из шести крайне сложных задач, охватывающих области алгебры, геометрии и теории чисел. Золотая медаль дает победителю статус одного из лучших молодых математиков в мире.
Совместные усилия двух систем DeepMind не совсем соответствовали этому уровню. Их ответы оценивал профессор Тимоти Гауэрс — лауреат «медали Филдса» (математического эквивалента «Нобелевской премии») и обладатель золотой медали на олимпиаде, команда DeepMind набрала 28 из 42 баллов — достаточно для серебряной медали, но на один балл меньше золота.
В отличие от человеческого математика, системы либо были безупречны, либо абсолютно беспомощны. В каждой из решенных задач они набрали максимальные баллы, но по двум из шести задач не смогли даже начать работу. Более того, у DeepMind, в отличие от человеческих конкурентов, не было ограничения по времени. В то время как студенты получают девять часов на решение задач, системы DeepMind работали над одной задачей три дня без перерыва, хотя с другой справились за считанные секунды.
Системы сильно различались. AlphaProof, которая решила три задачи, использует крупную языковую модель — такую же, как в чат-ботах, — и специальный подход «обучения с подкреплением», аналогичный тому, который DeepMind использовал для игры в Го. Секрет заключается в использовании существующего подхода под названием «формальная математика», набора правил, позволяющих записать математическое доказательство как программу, которая работает только в том случае, если она верна.
«Мы пытаемся построить мост между этими двумя сферами, чтобы мы могли воспользоваться преимуществами формальной математики и данными, доступными в неформальной математике», — сказал Томас Хьюберт, руководитель проекта AlphaProof.
После обучения на большом количестве задач, записанных на английском языке, AlphaProof использовала свои знания для создания конкретных доказательств на формальном языке. Поскольку эти доказательства могут быть либо истинными, либо ложными, можно обучить систему самоулучшению. Этот подход может решать сложные задачи, но не всегда быстро: хотя он намного лучше простого метода проб и ошибок, на одну из самых сложных задач ушло три дня.
Другая система, AlphaGeometry 2, аналогично сочетает языковую модель с более математически ориентированным подходом. Но ее успех в узкой области геометрических задач был поразителен: задача была решена всего за 16 секунд. И, как отметил Гауэрс, система выбрала неожиданный путь для этого. «Существуют легендарные примеры компьютерных доказательств, которые длиннее, чем Википедия. Это не тот случай: речь идет о очень кратком, человекоподобном решении.»
Руководитель проекта AlphaGeometry 2, Тханг Луонг, описал результат как аналог знаменитого «хода 37» в исторической победе DeepMind в Го, когда ИИ сделал ход, о котором ни один человек бы не подумал, и выиграл.
Доказательство AlphaGeometry 2 включало построение окружности вокруг другой точки и использование этой окружности для доказательства общего ответа. «Сначала наш эксперт не совсем понял, зачем вообще была построена эта точка, но после изучения решения стало ясно, что оно действительно объединяет множество треугольников, и решение оказалось весьма элегантным», — сказал Луонг.
Пример одной из задач AlphaGeometry 2:
Пусть ABC — треугольник с AB < AC < BC. Пусть I — центр вписанной окружности треугольника ABC, а ω — вписанная окружность. Пусть X — точка на прямой BC, отличная от C, такая что прямая, проходящая через X параллельно AC, касается ω. Аналогично, пусть Y — точка на прямой BC, отличная от B, такая что прямая, проходящая через Y параллельно AB, касается ω. Пусть AI пересекает описанную окружность треугольника ABC снова в точке P ≠ A. Пусть K и L — середины AC и AB соответственно.
Докажите, что ∠KIL + ∠YPX = 180°.
Задача была решена за 19 секунд.
Самая сложная задача AlphaProof
Улитка по имени Турбо играет в игру на доске с 2024 рядами и 2023 столбцами. В 2022 клетках спрятаны монстры. Изначально Турбо не знает, где находятся монстры, но знает, что в каждом ряду, кроме первого и последнего, точно по одному монстру, и что в каждом столбце не больше одного монстра.
Турбо делает серию попыток пройти с первого ряда до последнего. В каждой попытке он выбирает любую клетку в первом ряду, а затем неоднократно переходит в соседнюю клетку, имеющую общую сторону. (Он может вернуться в ранее посещенную клетку.) Если он достигает клетки с монстром, его попытка заканчивается, и он возвращается в первый ряд, чтобы начать новую попытку. Монстры не двигаются, и Турбо запоминает, содержит ли каждая посещенная им клетка монстра. Если он достигает любой клетки в последнем ряду, его попытка заканчивается, и игра заканчивается.
Определите минимальное значение n, для которого у Турбо есть стратегия, гарантирующая достижение последнего ряда на n-й попытке или раньше, независимо от расположения монстров.
Эта задача осталась нерешенной.
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Автор: andrey_belkin
