Янник Кильчер беседует со Стэном Полу (Stan Polu), исследователем из OpenAI и первым автором работы «Formal Mathematics Statement Curriculum Learning». В центре обсуждения — создание системы ИИ, способной решать задачи Международной математической олимпиады (IMO) через объединение языковых моделей и формальных методов верификации.
🧠 Математика как фронтир искусственного интеллекта 1:22
Математика долгое время оставалась одной из сложнейших областей для нейросетевых моделей. По словам Стэна Полу, прогресс в этом направлении вызывает ажиотаж в сообществе, так как математика воспринимается как «последний рубеж» на пути к созданию систем с полноценным логическим мышлением . Исследователь отмечает, что работа является прямым продолжением предыдущих изысканий OpenAI в области GPT-f (использование языковых моделей для поиска доказательств).
Стэн Полу поделился личной историей: он не имеет степени PhD в области машинного обучения и до прихода в OpenAI работал программным инженером в компании Stripe . Однако его глубокий интерес к формальной математике и ИИ совпал с миссией лаборатории. По его мнению, текущая система уже способна доказывать утверждения, которые были бы не под силу многим выпускникам инженерных вузов, хотя ИИ всё ещё пасует перед задачами, кажущимися людям элементарными .
💻 Что такое формальная математика и зачем она нужна 6:54
Формальная математика возникла как ответ на проблему человеческих ошибок в сложных доказательствах. Полу объясняет суть дисциплины:
- В современной науке существуют доказательства настолько сложные, что лишь считанные единицы специалистов в мире способны их проверить.
- Всегда остается риск, что в фундаментальном труде закралась ошибка, которую никто не заметил .
- Цель формализации — перевести математический язык в код, который компьютер может проверить шаг за шагом на предмет логической непротиворечивости.
Основная трудность здесь заключается в трудоемкости процесса. Полу приводит в пример работу математика Питера Шольце (Peter Scholze), чье доказательство объемом в десятки страниц заняло у группы экспертов шесть месяцев интенсивной работы по формализации в системе Lean . На сегодняшний день ИИ фокусируется не на создании новых теорий, а на решении упражнений в рамках уже существующих формальных библиотек, таких как mathlib .
🪜 Проблема самообучения и концепция «учебного плана» 13:13
В обучении ИИ для игр (как в AlphaZero) используется механизм self-play (самоигра), где агент соревнуется сам с собой, постоянно повышая сложность. В математике этот подход не работает напрямую, так как здесь нет очевидного противника.
Стэн Полу выдвигает гипотезу: ключевая роль self-play в играх заключается в создании неявного «неконтролируемого учебного плана» (unsupervised curriculum) . В математике же, если дать модели слишком сложную задачу, она просто не найдет решения, и вы не получите никаких данных для дальнейшего обучения.
Для решения этой проблемы команда OpenAI использовала следующие подходы:
- Ручное кураторство: Исследователи взяли учебники, по которым люди готовятся к олимпиадам, и формализовали задачи из них .
- Постепенное усложнение: Модель начинает с легких примеров, и по мере их решения база данных успешных доказательств пополняется, что позволяет модели обучаться на собственных результатах и переходить к более сложным задачам.
- Перенос распределения: Обучение на таком учебном плане смещает распределение модели от общих теорем библиотеки
mathlibв сторону специфических олимпиадных задач (бенчмарк miniF2F) .
⚙️ Механика системы: тактики и бесконечное пространство действий 21:07
Процесс доказательства в системе Lean выглядит как взаимодействие человека (или ИИ) с машиной. Цель разбивается на подцели, к которым применяются «тактики» — метапрограммы, преобразующие текущее состояние доказательства .
Стэн Полу выделяет две основные технические сложности:
- Бесконечное пространство действий: В отличие от шахмат, ИИ в математике должен не просто выбирать из списка ходов, но и генерировать математические термины «из головы» (например, предложить конкретное число или вспомогательную переменную) . Языковые модели идеально подходят для этой роли, так как могут генерировать произвольный текст.
- Две цели обучения: Модель обучается одновременно предсказывать следующий шаг (proof step objective) и оценивать оставшуюся длину доказательства (proof size objective), что служит своего рода «функцией ценности» для поиска в дереве доказательств .
Интересной деталью является то, что при каждой итерации (Expert Iteration) модель обучается «с нуля», а не дообучается . По словам Полу, это делается для научного контроля над переобучением и для агрессивной дедупликации данных .
📈 Результаты и удивительные открытия масштабирования 46:58
Системе удалось успешно решить две задачи Международной математической олимпиады (IMO). Однако в ходе экспериментов авторы столкнулись с неожиданным эффектом масштабирования:
- Модели малого размера против гигантов: Исследователи обнаружили, что для доказательства теорем не обязательно использовать огромные модели уровня GPT-3 .
- Эффективность вычислений: Оказалось выгоднее направить вычислительные ресурсы на то, чтобы сделать больше попыток (сэмплов) из маленькой модели, чем один раз запустить очень большую модель .
- Роль верификатора: Маленькая модель может выдавать «шумные» результаты, но наличие жесткого формального верификатора позволяет отсеять ошибки и найти верное решение среди тысяч попыток.
🚀 Будущее: симбиоз человека и машины 54:47
Стэн Полу считает, что формальная математика — это идеальная «лаборатория» для изучения рассуждений (reasoning). В отличие от обычных чат-ботов, здесь у ИИ нет возможности «галлюцинировать» или обманывать — любая ошибка будет мгновенно отвергнута верификатором .
Перспективы технологии по мнению гостя:
- Ускорение работы математиков: Инструменты вроде GPTF (плагин для Lean) могут в разы ускорить процесс формализации теорем, выполняя рутинные шаги за человека .
- Автоформализация: Полу видит большой потенциал в переводе обычных математических текстов на формальный язык с помощью ИИ .
- Развитие общего интеллекта: Успехи в математике станут «чертежом» для внедрения глубоких логических рассуждений в обычные языковые модели, которые сейчас часто ошибаются в многошаговых логических цепочках .
Стэн Полу заключает, что работа над формальной математикой позволяет объединить мощь языковых моделей (интуиция, генерация идей) с надежностью формальных систем (логическая строгость), создавая систему, обладающую подобием «внутреннего монолога» при решении задач .
