Новинка DeepMind: ИИ для обработки математических доказательств

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

Но теперь команда Google DeepMind создала AlphaProof, систему искусственного интеллекта, которая сравнялась с результатами серебряных медалистов на Международной математической олимпиаде 2024 года, набрав всего на одно очко меньше золота на самом престижном соревновании студентов по математике в мире. И это очень важно.

Истинное понимание

Причина, по которой компьютеры плохо выступили на математических соревнованиях, заключается в том, что, хотя они намного превосходят возможности человечества по выполнению вычислений, на самом деле они не так хороши в логике и рассуждениях, которые необходимы для продвинутой математики. Другими словами, они хорошо выполняют вычисления очень быстро, но обычно плохо понимают, зачем они это делают. Хотя такие вещи, как сложение, кажутся простыми, люди могут проводить полуформальные доказательства, основанные на определениях сложения, или использовать полностью формальные доказательства. Арифметика Пеано который определяет свойства натуральных чисел и операций, таких как сложение, посредством аксиом.

Чтобы провести доказательство, люди должны понимать саму структуру математики. То, как математики строят доказательства, сколько шагов им нужно, чтобы прийти к выводу, и насколько умно они это делают, является свидетельством их блеска, изобретательности и математической элегантности. «Знаете, Бертран Рассел опубликовал 500-страничную книгу. книга доказать, что один плюс один равно двум», — говорит Томас Хьюберт, исследователь DeepMind и ведущий автор исследования AlphaProof.

Команда DeepMind хотела разработать ИИ, который понимал бы математику на этом уровне. Работа началась с решения обычной проблемы ИИ: нехватки обучающих данных.

Переводчик математических задач

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