Наверное, многие слышали новость о том, что "AI завоевал серебро на межнаре по математике (IMO)" Так вот, я прочитала блогпост DeepMind по этому поводу и собрала главные поинты про модельку в пост.

Для начала, вводная по олимпиаде. IMO — это международная математическая олимпиада, высшая ступень олимпиад по математике. От каждой страны туда едет команда из шести человек. Олимпиада проходит в два дня, в каждый из дней дается три задачи и 4.5 часа на их решение. Задачи бывают четырех видов по темам: алгебра, теория чисел (тч), комбинаторика и геометрия. Каждая задача оценивается из 7 баллов, где 7 баллов — это полностью правильное решение задачи без ошибок и пробелов в рассуждении. Промежуточные баллы от 0 до 7 за решение получить при этом тоже можно. Например, если в решении пропущены пара незначительных моментов, поставят 5-6 баллов, а если задача не решена, но написаны идеи, потенциально ведущие к правильному решению, то можно получить до трех баллов.

Теперь, как устроена система для решения IMO от DeepMind и что там интересного:
Задачи по алгебре, тч и комбе решала модель AlphaProof, а по геометрии – другая, AlphaGeometry2. Всего модель решила 4 из 6 задач, все полностью правильно. Получается, набрала 7*4=28 баллов из возможных 36. Это — серебро на IMO 2024. Золото выдавалось от 29🤣

Теперь про модельки. Начнем с AlphaProof.
AlphaProof принимает на вход условие задачи и генерируют решение на формальном языке Lean. Получается, нужно как-то уметь переводить условие задачи, записанное на английском языке, на язык Lean. Для этого DeepMind взяли свою LLM Gemini и дообучили ее на эту задачу. Теперь условие задачи сначала попадает в Gemini, который переводит ее на Lean, и затем подает на вход AlphaProof.

AlphaProof — это RL-модель, практически идентичная AlphaZero, которая играла в Go. Работает AlphaProof так: сначала генерирует возможный ответ на задачу, а затем пытается доказать или опровергнуть правильность этого ответа, блуждая по пространству возможных утверждений-шагов доказательства (proof steps). Если удалось собрать верное доказательство, то этот пример используется для дообучения AlphaProof. Пишут, что до IMO модельку обучали на огромном пуле разных задач, а на самой олимпиаде делали вот что: генерировали разые вариации задач олимпиады, просили AlphaProof их решить, а верно найденные решения тоже использовали для дообучения AlphaProof на ходу. И так, пока не будет найдено решение основной задачи. Чем-то напоминает то, как люди тоже сначала стараются решить relaxed версии задач, прежде чем додуматься до решения основной.

Из интересного:
— на IMO были две задачи на алгебру, одна на тч, две на комбу и одна на геометрию. AlphaProof решила обе алгебры и тч, но не смогла решить ни одну комбинаторику 😂 В принципе, у человеков тоже обычно проблемы с комбой, судя по моему школьному опыту...
— время, потраченное AlphaProof на решение разных задач, очень разное. Одни задачи она решила за минуты, а на другую потратила три дня. Учитывая, что у людей на решение трех задач дается 4.5 часа, то сравнение модели с человеками-участниками олимпиады не очень честное;
— решения модель выдавала только на те задачи, которые точно полностью смогла решить. Частичные решения модели не оценивались. Вот тут нечестно в другую сторону: возможно, с частичными решениями задач на комбу модель могла бы получить и больше 28 баллов, претендуя и на золото;
— утверждается, что решения модели полностью в соответствии с правилами олимпиады проверяли два уважаемых математика: Prof Sir Timothy Gowers (золотой медалист IMO и филдсовский лауреат) и Dr Joseph Myers (дважды золотой медалист IMO и член комитета IMO). Так что свои 28 баллов моделька, кажется, получила честно.

Продолжение ⬇️