Для обучения компьютерной математике исследователи объединяют подходы искусственного интеллекта

«Они будут говорить о единорогах, но забудут, что у них один рог, или расскажут вам историю, а после изменят детали», — рассказывает о больших языковых моделях (LLM — Large Language Model) Джейсон Рут из IBM Research.

Это больше, чем просто ошибки — LLM изо всех сил пытаются распознать свои ошибки, что ограничивает их производительность. Эта проблема не присуща системам искусственного интеллекта. Модели машинного обучения, основанные на методе обучения с подкреплением, позволяют компьютерам учиться на своих ошибках и становиться вундеркиндами в таких играх, как шахматы и го. Хотя эти модели, как правило, более ограничены в своих возможностях, они представляют собой обучение такого рода, которого LLM еще не освоили.

«Не хочется создавать языковую модель, которая просто говорит как человек», — сказал Юхуай (Тони) Ву из Google AI. «Мы хотим, чтобы она понимала, о чем говорит».

Ву — соавтор двух недавних статей, где предлагается способ достижения этой цели. На первый взгляд, речь идет об очень конкретном приложении: обучении систем ИИ выполнять математические операции. В первой статье описывается обучение LLM переводу обычных математических выражений в формальный код, который компьютер может запускать и проверять. Во второй LLM обучили не только понимать математические задачи на естественном языке, но и решать их с помощью системы под названием Minerva.

В совокупности статьи предлагают форму будущей архитектуры ИИ, где LLM могут учиться рассуждать с помощью математического мышления.

«Есть глубокое обучение, обучение с подкреплением, AlphaGo, а теперь и языковые модели, — говорит об этом Сиддхартха Гэдгил, математик из Индийского института науки в Бангалоре, работающий с математическими системами ИИ. — Технология развивается во многих разных направлениях, и все они могут работать вместе».

Не очень простые переводы

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

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

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

Вот почему авторы первой статьи, представляющие как академические, так и отраслевые организации, предпочли автоматическую формализацию коротких математических утверждений, а не полных доказательств. Исследователи работали в основном с LLM Codex, который основан на GPT-3, но имеет подготовку по техническим материалам из таких источников, как GitHub. Чтобы Codex понимал математику достаточно хорошо для автоматической формализации, ученые предоставили ему всего два примера математических задач на естественном языке и их формальные переводы в код.

После этого краткого урока ученые передали Codex формулировки на естественном языке почти 4000 математических задач со школьных соревнований. Поначалу его производительность может показаться неутешительной: Codex перевел их на язык математической программы Isabelle/HOL с точностью чуть менее 30%. А когда Codex терпел неудачу, чтобы заполнить пробелы в переводческом лексиконе, он придумывал новые термины.

«Иногда он просто не знает слова, которое ему нужно знать (какое название в Isabelle/HOL у «простого числа» или «факториала») и просто выдумывает, а это самая большая проблема с такими моделями, — сказал Рут. — Они много гадают».

Но для исследователей важным было не то, что Кодекс терпел неудачу в 70% случаев; дело в том, что после просмотра такого небольшого количества примеров ему удавалось добиться успеха в 30% случаев.

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

Ли и его соавторы рассматривают результат как образец скрытых способностей, которые LLM могут приобрести при наличии достаточного количества общих обучающих данных. До этого исследования Codex никогда не переводил с естественного языка на формальный математический код. Но этот ИИ был знаком с кодом после изучения GitHub, а с математикой на естественном языке — из Интернета. Чтобы опираться на эту базу, исследователям нужно было только показать несколько примеров того, что они хотели, и Codex мог начать собирать все воедино, чтобы понять больше.

«Во многих отношениях в этой статье удивительно то, что [авторы] мало что сделали, — считает Рут. — У этих моделей была естественная способность к выполнению задачи».

То же самое исследователи наблюдали, когда пытались LLM не только тому, как переводить математические задачи, но и тому, как их решать.

Математика Minerva

Вторая статья, хотя и независимая от более ранней работы по автоформализации, обладает схожими чертами. Группа исследователей из Google обучила LLM подробно отвечать на вопросы школьного уровня математики, например «Прямая, параллельная y = 4x + 6, проходит через (5, 10 ). Какова y-координата точки пересечения с осью y?»

Авторы начали с LLM под названием PaLM, обученного на общих текстах на естественном языке, подобно GPT-3. Исследователи обучили PaLM на материалах о математике, таким как страницы arxiv.org, и другим техническим материалам, имитируя источники Codex. Эту дополненную модель исследователи назвали Minerva.

Исследователи показали Minerva четыре примера того, что они хотели: пошаговые решения математических задач на естественном языке.

Затем они проверили модель на ряде вопросов по количественному мышлению. Показатели варьировались в зависимости от предмета: модель отвечала на вопросы правильно чуть лучше, чем в половине случаев по некоторым темам (например, по алгебре), и чуть меньше, чем в половине случаев — по другим (например, по геометрии).

У авторов была одна проблема, распространенная во многих областях исследований ИИ: Minerva правильно отвечала на вопросы только потому, что уже видела их или подобные вопросы в обучающих данных. Эта проблема называется «загрязнением», и из-за нее трудно понять, действительно ли модель решает задачи или просто копирует чужую работу.

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

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

Чтобы предотвратить угадывание, исследователи заставили сеть сдать национальный экзамен по математике 2022 года в Польше, который вышел после того, как были установлены данные обучения. По словам Рута, система ответила правильно на 65% вопросов, а это достойный результат для студента и особенно хороший — для LLM. Опять же положительные результаты после такого небольшого количества примеров свидетельствуют о присущей хорошо обученным моделям способности выполнять такие задачи.

«Это урок, который мы продолжаем усваивать в глубоком обучении, этот масштаб на удивление хорошо помогает во многих задачах», — сказал об этом Гай Гур-Ари, бывший исследователь Google и соавтор статьи.

Исследователи также узнали, как повысить производительность Minerva. Например, в методе, который называется «голосование большинством», Minerva решала одну и ту же задачу несколько раз, подсчитывала различные результаты и определяла окончательный ответ как наиболее часто встречающийся (правильный ответ только один, а возможных неправильных очень много). Это увеличило оценку по определенным задачам с 33 до 50%.

Также важно было научить Minerva разбивать решение на ряд шагов — это метод, называемый подсказкой по цепочке мыслей. Это дало модели преимущества студентов: перед ответом модель замедлялась и уделяла больше вычислительного времени каждой части задачи.

«Если вы попросите языковую модель объяснить шаг за шагом, точность резко повысится», — рассказывает Гэдгил.

Наведение мостов

Впечатляющая работа Minerva содержала отмеченную авторами существенную оговорку: Minerva не может автоматически проверить правильность своего ответа. Даже если она ответила на вопрос правильно, она не может проверить правильность шагов к ответу.

«Иногда он дает ложные срабатывания, что дает благовидные причины для правильных ответов», — сказал Гэдгил.

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

«Я правда сомневаюсь, что этот подход можно масштабировать для решения сложных задач», — сказал Кристиан Сегеди, исследователь ИИ в Google и соавтор предыдущей статьи.

Вместо этого исследователи обеих статей надеются начать обучать машины математике теми же методами, которые позволили машинам добиться хороших результатов в играх. В мире множество математических задач, которые могли бы послужить обучающими данными для таких систем, как Minerva, но система не может распознать «хороший» ход в математике, как AlphaGo знает, когда он хорошо сыграл в го.

«С одной стороны, если вы работаете над естественным языком или рассуждениями типа рассуждений Minerva, там есть много данных, весь интернет математики, но, по сути, вы не можете использовать их для обучения с подкреплением», — рассказывает Ву. С другой стороны, «ассистенты по доказательствам дают среду, но у них мало данных для обучения. Нам нужен какой-то мост, чтобы перейти с одной стороны на другую».

Автоформализация и есть этот мост. Ее улучшения могут помочь математикам автоматизировать разные стороны процесса написания доказательств и проверять правильность своей работы.

Объединив достижения двух статей, такие системы, как Minerva, могут сначала формализовать математические задачи, а затем решать их и проверять их работу с помощью ассистента по проверке доказательств, такого как Isabelle/HOL. Эта мгновенная проверка даст обратную связь, необходимую для обучения с подкреплением, позволяя этим программам учиться на своих ошибках. Наконец, программы приходили к доказуемо правильному ответу со списком логических шагов, эффективно сочетая мощь LLM и обучения с подкреплением.

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

• Профессия Data Scientist (24 месяца)
• Профессия Fullstack-разработчик на Python (16 месяцев)