Способен ли искусственный интеллект решать задачи из области чистой математики, требующие глубокого абстрактного мышления и стратегического планирования? Популярный исследователь ИИ Янник Килчер представил подробный разбор научной работы от OpenAI, Федеральной политехнической школы Лозанны (EPFL) и Кембриджа, посвященной автоматическому доказательству теорем. Разработанная учеными система продемонстрировала революционные результаты, сумев самостоятельно решить две задачи из Международной математической олимпиады (IMO).
🚀 Новая веха в символьном мышлении ИИ 0:01
Вопрос о том, может ли ИИ заниматься чистой математикой, выходит далеко за рамки простых арифметических вычислений вроде «два плюс два». Рассматриваемая научная работа под названием «Formal Mathematics Statement Curriculum Learning» предлагает автоматизированную систему для доказательства математических теорем в символьном виде.
Самым удивительным фактом, по мнению Янника Килчера, является то, что эта система смогла решить две сложнейшие задачи с Международной математической олимпиады, в которой участвуют самые одаренные старшеклассники мира.
Предыдущие алгоритмы автоматизации значительно отставали от неформальной человеческой математики. Прошлые подходы во многом полагались на простой перебор вариантов доказательства (brute force), направляемый лишь базовыми эвристиками.
Новая технология кардинально улучшает этот процесс. Она использует большие языковые модели для управления поиском доказательств, а метод «экспертной итерации» (expert iteration) позволяет системе автоматически выстраивать для себя учебную программу из все более сложных утверждений.
Как отмечает ведущий, последствия этого открытия важны не только для математики, так как речь идет о символьном мышлении и способности модели самостоятельно обучаться, что критически важно для многих областей искусственного интеллекта.
Сам Янник Килчер скромно называет себя новичком в формальной математике и признается, что при чтении текста у него возникло множество вопросов и критических замечаний. Ответы на них он получил во время интервью с первым автором статьи, которое пообещал выпустить на следующий день.
🧩 Бесконечное пространство и вызовы формальной математики 4:26
Авторами исследования выступили специалисты из OpenAI, EPFL и Кембриджа. В своей работе они применили технику экспертной итерации к процессу доказательства формальных математических утверждений.
Глубокое обучение уже достигло огромных успехов в таких задачах, как языковое моделирование, компьютерное зрение и генерация изображений. Тем не менее, исследователи констатируют, что ИИ до сих пор не демонстрировал сопоставимых успехов в задачах, требующих долгосрочного планирования и логического вывода.
Математика, по мнению авторов, является идеальной средой для таких экспертных систем: она бросает вызов возможностям планирования, но при этом ИИ не зависит от внешних данных и может проверять корректность доказательств самостоятельно в любое время.
Главными вызовами в этой сфере остаются экстремально огромное пространство поиска и бесконечное пространство действий. Когда человек или машина доказывает теорему, существует бесконечное множество потенциальных шагов.
Проблема заключается не только в манипулировании уже существующими символами, но и в необходимости вводить новые сущности. Например, в доказательстве может потребоваться заявить: «существует переменная $x$, которая удовлетворяет определенным условиям», хотя до этого момента символ $x$ вообще не упоминался в задаче.
🌲 Анатомия доказательства: деревья решений и «тактики» 6:00
Для понимания работы системы важно разобраться, как устроено формальное доказательство на компьютере. В таких системах существует исходное формальное утверждение, которое необходимо доказать. Оно записывается не обычными словами, а с использованием строго определенного синтаксиса предопределенной логической системы.
Чтобы доказать это утверждение, система строит дерево решений, декомпозируя главную задачу на несколько более простых подутверждений. Этот процесс аналогичен человеческому мышлению, когда математик разбивает сложную теорему на несколько промежуточных шагов, каждый из которых должен быть истинным.
Переход от верхнего утверждения к нижним называется применением «тактики» (tactic). Подутверждения строятся на основе контекстно-свободной грамматики, то есть каждое из них должно быть доказуемо независимо от соседних веток. Дерево разрастается вниз до тех пор, пока на его концах (листьях) не останутся элементы, истинность которых уже известна.
Листьями дерева доказательства могут быть:
- Предусловия самой теоремы (например, допущение, что переменные являются рациональными числами).
- Ранее доказанные и известные системе вспомогательные леммы.
- Фундаментальные математические аксиомы, принимаемые без доказательств.
Когда все листья дерева сведены к этим трем категориям, теорема считается официально доказанной. Поиск правильных ветвей, которые в итоге приведут к успеху, Янник Килчер называет истинной «магией математики», составляющей суть работы ученых.
Данный процесс отдаленно напоминает игровые алгоритмы вроде AlphaGo или AlphaZero, однако между ними есть принципиальная разница. Если в игре Го у ИИ всегда есть строго фиксированный набор возможных ходов на доске, то в математических доказательствах пространство действий бесконечно и требует генерации внешних терминов.
🔄 Экспертная итерация: как заменить отсутствие соперника 9:43
Помимо бесконечного пространства действий, перед учеными встала еще одна проблема — отсутствие режима прямой игры с самим собой (self-play). В отличие от шахмат или Го, где нейросеть может играть против собственных копий и бесконечно повышать уровень мастерства, в математике нет явного противника. Математическое утверждение либо доказуемо, либо нет, у него нет градации сложности в зависимости от оппонента.
Это делает невозможным наивное применение алгоритмов симметричного самообучения. Однако авторы статьи выдвинули гипотезу, что ключевая роль игры с самим собой в ИИ заключается в неявном формировании «обучающей программы» (curriculum) без надзора. В играх оба соперника начинают очень слабыми, а затем синхронно и постепенно развивают свои навыки шаг за шагом.
Янник Килчер соглашается с тем, что этот эволюционный процесс по сути является идеальной автоматической учебной программой. Чтобы решить проблему в математике, OpenAI предложила использовать сторонний набор вспомогательных задач различной сложности без заранее известных решений.
Если этот набор имеет плавный градиент сложности, то простая процедура экспертной итерации способна последовательно щелкать задачи как орехи. Процесс выглядит следующим образом:
- Базовая модель пробует доказать широкий пул задач и успешно справляется только с самыми простыми из них.
- Найденные ею успешные доказательства собираются и используются для повторного обучения этой же модели.
- Обновленная, более сильная модель получает способность решать чуть более сложные задачи из предложенного пула.
- Новые доказательства снова отправляются в обучающую выборку, и цикл запускается заново.
Янник Килчер подчеркивает, что этот метод базируется на синергии глубокого обучения и поисковых алгоритмов. Если просто скармливать выходы нейросети ей же на вход без этапа поиска решений, модель быстро застрянет на одном уровне сложности. Поисковый блок выступает надстройкой, которая генерирует качественные данные, вытягивая возможности языковой модели на новый уровень.
📝 Языковая модель в роли математика: архитектура и цели обучения 15:35
В качестве цифровой среды для проведения экспериментов исследователи выбрали интерактивную среду Lean. Это специализированная программная платформа для верификации формальных математических доказательств. Существуют и другие аналоги, например Metamath, однако Lean обладает важным преимуществом — поддержкой высокоуровневых тактик. Благодаря этому доказательства в Lean получаются в среднем в 10 раз короче, чем в других аналогичных системах.
Для управления поиском ученые применили языковые модели типа Transformer (архитектура decoder-only). Самая крупная конфигурация сети состояла из 36 слоев и насчитывала 700 миллионов обучаемых параметров. Модель была предварительно обучена на комбинации специализированных математических датасетов и огромного текстового массива Common Crawl, полученного из интернета.
Янник Килчер находит удивительным тот факт, что нейросеть для точной математики обучали на текстах на естественном языке, учитывая, насколько специфичен и скрытен синтаксис Lean. Внутренний след среды Lean заполнен сложными конструкциями вроде nat.prime.dvd_mul и техническими состояниями тактик, не имеющими ничего общего с человеческой речью. Тем не менее, предобучение на обычных текстах, по-видимому, обеспечивает важный трансфер знаний.
Модель обучали решать две ключевые задачи. Первая — цель шага доказательства (proof step objective). Нейросеть должна сгенерировать правильную тактику (команду), основываясь на текущем состоянии дерева доказательства. На вход подается имя теоремы (declaration) и текущая цель (goal), а модель предсказывает следующий логический шаг. Структура обучающего промпта выглядит так:
decal [Имя_теоремы] goal [Состояние_цели] proof step [Шаг_доказательства]
Во время работы ключевое слово proof step и последующий текст скрываются, и модель генерирует их самостоятельно. Имя теоремы служит подсказкой, указывающей, в каком месте математической библиотеки mathlib находится ИИ. Это позволяет модели понять, какие функции и переменные ей сейчас доступны.
Янник Килчер проводит аналогию с программированием: имя теоремы — это путь к файлу проекта и его импорты, цель — сигнатура функции и ее документация, а шаг доказательства — сам код реализации.
Вторая цель обучения — предсказание размера доказательства (proof size objective). Модели подают те же данные, но вместо шага просят указать токен размера доказательства. Всего используется 11 буквенных бакетов (корзин) от A до K. Бакет 0 зарезервирован для бесконечных или еще не доказанных путей, бакет 1 — для самых длинных доказательств, а бакет 10 — для самых коротких.
На этапе инференса логиты этих бакетов переводятся по специальной формуле в оценку от 0 до 1. Если модель уверена, что путь бесконечен, ценность ветки равна 0. Если она видит кратчайший путь, ценность равна 1. Это позволяет ИИ при поиске приоритизировать те цели, которые ведут к наиболее коротким доказательствам.
⚙️ Алгоритм бутстрапинга и круговорот данных 29:08
Процесс экспертной итерации требует наличия стартовой точки для запуска цикла обучения, то есть бутстрапинга. Сначала исследователи обучили исходную модель $\theta_0$ только на базовой задаче предсказания шагов доказательства, используя существующие в библиотеках готовые человеческие доказательства. Затем эту базовую модель запустили генерировать доказательства для утверждений из библиотеки mathlib. Все успешные результаты сформировали массив $s_0$.
На основе $s_0$ были созданы дедуплицированные наборы предсказаний шагов и размеров доказательств, которые объединили с исходным датасетом. На этой объединенной выборке заново обучили модель $\theta_0$, получив полноценную модель первой итерации — $\theta_1$, которая уже знала обе целевые функции.
Каждая последующая итерация $k$ строилась по строгому правилу: модель генерирует новые траектории поиска, успешные варианты фильтруются, добавляются в общий котел знаний, а затем исследователи снова берут «чистую» базовую модель $\theta_0$ и дообучают ее с нуля на всем накопленном объеме данных, получая модель $\theta_{k+1}$.
Янник Килчер обращает внимание на важную деталь: fine-tuning всегда идет от исходной точки $\theta_0$, а не последовательно от $\theta_1$ к $\theta_2$. По его мнению, последовательное обучение могло бы намертво запереть модель в локальных тупиках.
Объединенный датасет постоянно дедуплицируется, и если система находит более короткое доказательство для старой теоремы, длинный вариант выбрасывается. Проще обучить модель заново на чистых и коротких примерах, чем заставлять ее «забывать» старые плохие привычки. Побочным продуктом поиска становятся и негативные примеры (ошибочные пути), которые также помогают в обучении.
📊 Результаты тестов: от синтетических неравенств до Олимпиады IMO 34:13
Исследователи провели в общей сложности 9 полных экспертных итераций. На графиках эффективности вырисовывается стабильный восходящий тренд: с каждой итерацией система доказывала все больше и больше уникальных утверждений.
В обучающем наборе mathlib train число успешно доказанных теорем выросло с 17 390 на первой итерации до 19 476 к девятой итерации. При этом средняя длина шагов доказательства сократилась с 4,8 до 4,0.
Ученые связывают этот успех с двумя факторами: открытием новых оригинальных (более коротких) путей и постепенным взятием «маргинально более сложных» задач, что расширяло учебную базу для следующего шага. К девятой итерации модель более чем на 90% обучалась на данных, которые сгенерировала сама.
Ведущий подчеркивает уникальность математической среды: в отличие от других сфер, здесь дообучение на собственных данных безопасно, так как компьютерный верификатор Lean мгновенно и со стопроцентной точностью подтверждает правильность любого шага.
Сравнение с базовым методом (sample-only), где поиск идет без переобучения модели, показало безоговорочное преимущество экспертной итерации. На первых порах обычный сэмплинг кажется эффективнее, так как не тратит время на фазу долгого обучения. Однако при масштабировании вычислительных мощностей метод сэмплирования упирается в плато, тогда как экспертная итерация демонстрирует взрывной рост эффективности.
Чтобы проверить концепцию обучения на учебных программах, авторы создали синтетический генератор неравенств (таких как неравенство Гёльдера или Коши-Буняковского). Сложность контролировалась числом вложенных композиций теорем. Было создано 100 стартовых простых задач с доказательствами и пул более сложных утверждений без решений со сложнейшими уровнями от 0 до 6.
Тесты показали, что метод простого сэмплирования вообще не смог решить ни одной задачи наивысшего 6-го уровня сложности. В то же время система с экспертной итерацией успешно взломала этот уровень.
Главной же целью проекта был датасет miniF2F, содержащий задачи олимпиадного уровня. Ученые вручную формализовали 300 задач из школьных сборников для подготовки к экзаменам, создав целевой curriculum. Объединив эти задачи с синтетическими неравенствами и базой mathlib, ИИ смог сместить свое распределение данных ближе к олимпиадному уровню и в итоге успешно решить две реальные задачи Международной математической олимпиады.
⚡ Цена прогресса: вычислительные мощности и будущее технологии 47:17
Исследование OpenAI также пролило свет на особенности масштабирования моделей в точных науках. Авторы обнаружили, что масштабирование размера нейросетей в символьных вычислениях работает не так линейно, как в обычном обучении без учителя (unsupervised learning). Крупные модели действительно показывают более высокий процент успеха при единичном запуске доказательства.
Однако в условиях фиксированного бюджета вычислительной мощности зачастую выгоднее запустить множество параллельных попыток сэмплирования из более мелкой и быстрой модели, нежели тратить ресурсы на один тяжелый запуск крупной сети.
Сами требования к железу для проведения этого эксперимента оказались колоссальными. Как отмечает Янник Килчер, для проведения одного полного цикла из 9 экспертных итераций на большой модели потребовалось около 2000 дней работы графических процессоров NVIDIA A100. При этом одиночный поиск доказательства для одного утверждения при правильном распараллеливании занимает в среднем 0,1 часа работы одной карты A100.
Несмотря на колоссальные затраты, система решила всего две олимпиадные задачи, что, по мнению Килчера, доказывает: эта область ИИ все еще находится в зачаточном состоянии. Тем не менее, ведущий выражает огромный оптимизм по поводу интеграции нейросетей с жесткими логическими поисковыми процедурами, ведь этот подход может научить машины генерировать безупречные обучающие данные самостоятельно.
