Решение (некоторых) задач официальных математических олимпиад02.02.2022 08:00

Мы создали нейросетевой инструмент для автоматического доказательства теорем в системе Lean⁠, который научился решать различные сложные задачи школьных олимпиад, в том числе задачи с соревнований AMC12⁠ и AIME⁠, а также две задачи, адаптированные с IMO⁠.

Мы создали нейросетевой инструмент для автоматического доказательства теорем в системе Lean⁠, который научился решать различные сложные задачи школьных олимпиад, в том числе задачи с соревнований AMC12⁠ и AIME⁠, а также две задачи, адаптированные с IMO⁠.A Программа использует языковую модель для поиска доказательств формальных утверждений. Каждый раз, когда мы находим новое доказательство, мы используем его в качестве новых обучающих данных, что улучшает нейросеть и позволяет ей итеративно находить решения для все более и более сложных утверждений.

Мы установили новый рекорд (41.2% против 29.3%) на бенчмарке miniF2F⁠, представляющем собой сложную подборку задач школьных олимпиад. Наш подход, который мы называем обучением на основе учебной программы формулировок (statement curriculum learning), заключается в ручном сборе набора утверждений разного уровня сложности (без доказательств), где самые сложные утверждения близки к целевому бенчмарку. Сначала наша нейросетевая программа слаба и способна доказать лишь немногие из них. Мы итеративно ищем новые доказательства и дообучаем нашу нейросеть на вновь обнаруженных доказательствах, и после 8 итераций наш доказыватель оказывается значительно превосходящим аналоги при тестировании на miniF2F.

Формальная математика — это увлекательная область для исследования, поскольку (i) она обладает исключительным богатством, позволяя доказывать произвольные теоремы, требующие рассуждений, творчества и озарения, и (ii) она похожа на игры (в которых искусственный интеллект добился потрясающих успехов) тем, что в ней есть автоматизированный способ определения того, успешно ли доказательство (т.е. верифицировано ли оно формальной системой). Как показано на тривиальном примере ниже, доказательство формального утверждения требует генерации последовательности шагов доказательства, каждый из которых представляет собой вызов тактики.B

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

Мы замечаем, что способность генерировать оригинальные математические термы, необходимые в качестве аргументов тактик (что невозможно сделать без нейросетевой языковой модели), возникает в ходе нашей процедуры обучения. Приведенное ниже доказательство является тому примером: шаг доказательства use n + 1 (полностью сгенерированный нашими моделями) предлагает использовать n + 1 в качестве решения, а оставшаяся часть формального доказательства полагается на тактику [ring_exp](https://leanprover-community.github.io/mathlib_docs/tactic/ring_exp.html), чтобы проверить его правильность.

Мы также отмечаем, что наши модели и процедура поиска способны создавать доказательства, объединяющие в цепочку несколько нетривиальных шагов рассуждения. В приведенном ниже доказательстве модель начинает с применения контрапозиции, приводящей к экзистенциальному утверждению (∃ (x : ℝ), f x ≠ a * x + b). Затем она генерирует для него свидетель с помощью use (0 : ℝ) и завершает доказательство, задействуя тактику [norm_num](https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num).

Наши модели, обученные с помощью обучения на основе учебной программы формулировок, смогли справиться с различными задачами из учебников по курсу обучения, а также с соревнований AMC12⁠ и AIME⁠, а также с двумя задачами, адаптированными с IMO⁠. Ниже мы представляем три примера таких сгенерированных доказательств.

Формальная математика сопряжена с двумя основными трудностями, из-за которых наивное применение обучения с подкреплением вряд ли будет успешным.

• (i) Бесконечное пространство действий: формальная математика имеет не только чрезвычайно большое пространство поиска (как, например, Го), но и бесконечное пространство действий. На каждом шаге поиска доказательства модель должна выбирать действие не из хорошо устроенного конечного набора, а из сложного и бесконечного набора тактик, включающих экзогенные математические термы, которые необходимо генерировать (например, генерация математического утверждения для использования в качестве свидетеля — объекта, используемого на таких шагах, как «существует такое x, что…», или разреза, то есть введения и объединения леммы в середине доказательства).
• (ii) Отсутствие самообучения (self-play): в отличие от игр для двух игроков, доказыватель играет не против противника, а против набора утверждений, которые нужно доказать. При столкновении с утверждением, которое оказывается слишком сложным, не существует очевидного способа переформулировки, который позволил бы доказывателю сначала сгенерировать промежуточные более простые утверждения для решения. Эта асимметрия препятствует наивному применению алгоритмов самообучения, которые оказались успешными в играх для двух игроков.

В нашей работе мы решаем проблему бесконечного пространства действий путем выборки действий из языковой модели в процессе поиска доказательства. Языковые модели способны генерировать вызовы тактик, а также оригинальные математические термы, часто требуемые в качестве аргументов. Основой для преодоления проблемы отсутствия самообучения послужило наблюдение, что ключевая роль самообучения в играх для двух игроков заключается в предоставлении неконтролируемой учебной программы (unsupervised curriculum). Наша методология предлагает заменить эту неконтролируемую учебную программу вспомогательным набором формулировок задач (без требования доказательств) разной степени сложности. Мы эмпирически показываем, что при достаточной вариативности сложности этих вспомогательных задач наша процедура обучения способна справляться с программой обучения возрастающей сложности, в конечном счете обобщаясь на тот набор задач, который нас интересует.

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