Исследователи протестировали AlphaGeometry на 30 геометрических задачах Международной математической олимпиады (IMO), которые считаются сложными даже для опытных математиков. Система решила 25 задач за стандартное время в 4,5 часа, что соответствует среднему баллу золотых медалистов, решивших аналогичные задачи. Языковая модель опирается на ту же технологию, что лежит в основе поисковой системы Google и систем распознавания естественного языка. Механизм дедукции основан на методе, разработанном китайским математиком Вэнь-Цюн Ву в 1978 году. Предыдущая система, основанная на методе Ву, решила только 10 задач.
Математика и, в частности, геометрия, вызывают трудности у исследователей ИИ, поскольку требуют как творческого подхода, так и строгости. В отличие от текстовых моделей ИИ, которые можно обучать на огромных объемах данных из интернета, для математики доступно относительно мало данных, которые являются более символическими и предметно-ориентированными. Кроме того, решение математических задач требует логических рассуждений, с которыми большинство современных моделей ИИ справляется не очень хорошо.
Чтобы преодолеть эти проблемы, исследователи разработали новый нейросимволический подход, который использует сильные стороны как нейронных сетей, так и символических систем. Нейронные сети хорошо распознают закономерности и прогнозируют следующие шаги, но они часто допускают ошибки или не дают объяснений. Символические системы, напротив, основаны на формальной логике и строгих правилах, которые позволяют им корректировать и обосновывать решения нейронной сети.
Команда сосредоточилась на задачах евклидовой геометрии, цель которых — написать математическое доказательство заданного утверждения. Они встроили в свой собственный язык десятки основных правил геометрии, например, «если одна прямая пересекает вторую прямую, она также пересечет линию, параллельную второй прямой». Затем они написали программу, которая автоматически генерирует 100 млн «доказательств». Эти доказательства состояли из случайных последовательностей простых, но логически неопровержимых шагов, например, «по двум точкам A и B построить квадрат ABCD». AlphaGeometry прошла обучение на этих машинных доказательствах. Это позволило искусственному интеллекту решать задачи шаг за шагом, аналогично тому, как чат-боты генерируют текст. Благодаря возможности отсеивать неверные варианты, ИИ мог надежно предоставлять правильные результаты, а их точность было легко проверить.
AlphaGeometry может обобщать невидимые проблемы и открывать новые теоремы, которые явно не указаны в постановке задачи. Например, система смогла доказать теорему о биссектрисе треугольника, которая не была задана как предпосылка или цель задачи.
Исследователи надеются, что их система с открытым исходным кодом вдохновит на дальнейшие исследования. Они считают, что их подход с использованием синтетических данных поможет ИИ преуспевать в математике и естественных науках, где данных для обучения, созданных человеком, недостаточно. Но ученые признают и ограничения модели — необходимость более понятных доказательств, масштабирования для решения сложных задач, а также этические вопросы, связанные с использованием систем искусственного интеллекта в математике.
