ИИ решает задачи по геометрии не хуже победителей международной математической олимпиады

При тестировании на наборе из 30 задач по геометрии, взятых из задач Международной математической олимпиады (ММО), AlphaGeometry смогла решить 25. Это приближается к показателям золотых медалистов соревнований — по крайней мере, по геометрии.

Кевин Баззард, математик из Имперского колледжа Лондона, отмечает, что геометрия — это лишь одна из дисциплин, в которых участники IMO должны преуспеть, и что компьютерам может быть намного сложнее добиться столь же хороших результатов в решении задач IMO в других областях, таких как, например, теория чисел. Тем не менее, говорит Баззард, «тот факт, что им удалось решить 25 проблем IMO, а также создать удобочитаемые доказательства, очень впечатляет».

Сравнение AlphaGeometry с результатами участников Международных олимпиад по математике

Исследователи экспериментировали с решением различных математических задач, используя большие языковые модели — программы искусственного интеллекта, которые обучаются на больших коллекциях текстов и которые используются в самых популярных чат-ботах, в том яисле ChatGPT. Результаты были интересными, но часто бессмысленными.

Например, ориентированный на математику чат-бот под названием Minerva, разработанный Google для исследовательских целей, обучался с использованием работ по углубленной математике и решений основных математических задач школьного уровня, написанных людьми. Хотя численные решения, к которым приходит Минерва, обычно верны, текст, который она создает для объяснения своих рассуждений, часто ошибочен — и его необходимо проверять. «Если система обучена на естественном языке, она будет строить вывод на естественном язык, которому мы не можем доверять», — говорит Триу Трин, из Google DeepMind, соавтор работы.

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

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

Затем они написали программу, которая автоматически генерирует 100 миллионов «доказательств». По сути, они состояли из случайных последовательностей простых, но логически неопровержимых шагов — например, «по двум точкам A и B построить квадрат ABCD».

AlphaGeometry прошла обучение на этих машинных доказательствах. Это означало, что ИИ мог решать проблемы, угадывая шаг за шагом, точно так же, как чат-боты создают текст. Но это также означало, что его выходные данные были машиночитаемыми и их точность можно было легко проверить. Для каждой проблемы AlphaGeometry генерировала множество попыток решения. Поскольку ИИ мог автоматически отсеивать неверные, он мог надежно выдавать правильные результаты, в том числе при решении задач по геометрии, предложенных на ММО.

AlphaGeometry сочетает в себе грубые статистические предположения о языковых моделях (своего рода переборный алгоритм) и символические рассуждения. Сочетание двух таких разных подходов может быть источником ее силы, говорит Стефан Шульц, университета Баден-Вюртемберга в Штутгарте, Германия.

Баззард говорит, что обучение AlphaGeometry на синтетических данных также устраняет одну из больших потенциальных ловушек при применении типичных больших языковых моделей к математике: мошенничество. По его словам, когда нейронная сеть обучается на миллиардах текстов, взятых из Интернета, «крайне сложно гарантировать, что модель не видела решение раньше». Но поскольку она предъявляет новое доказательство, можно быть уверенным, что она нашла его сама.

Обучение AlphaGeometry с помощью автоматически сгенерированных доказательств преследовало и другую цель, говорит соавтор исследования Хе Хе, из Нью-Йоркского университета. «Мы хотим построить такую систему без использования человеческих данных, чтобы однажды она могла превзойти человеческие возможности», — говорит она.

Но рабочим местам математиков пока ничего не угрожает. «Я могу представить, что через несколько лет те или иные методы машинного обучения смогут решать математические задачи на уровне самых умных студентов бакалавриата», — говорит Баззард. «Но я не вижу никаких свидетельств того, что машины способны автономно работать с современной математикой исследовательского уровня».