Autoformalization with Large Language Models [2022] - собираем чемпиона по математике среди алгоритмов.

Продолжаем серию постов про док-ва теорем: раз, два, три.

В данной работе в качестве базовой модели используется Thor. Дополнительно применяется схема из статьи GPT-f - после начального претрейна и файнтюна модели мы запускаем процесс под названием Expert Iteration:
1) Применяем нашу модель на тренировочном датасете задач и пытаемся доказать каждую из них.
2) Собираем датасет из успешных доказательств, на котором мы дообучаем нашу языковую модель.
3) Повторяем процедуру, пока не надоест

В чём ключевая новизна статьи - авторы пытаются расширить тренировочный датасет: берут другой датасет задач по математике, написанных на естественном языке, и просят Codex перевести эти задачи на "формальный язык", с которым мы работаем. По словам авторов, они проверили качество перевода на случайных 150 задачках и получили 38 корректных переводов.

В остальном ничего сильно нового в статье нет, после 2-х итераций Expert Iteration с использованием "автоформализованных" задач получается 29.9% на miniF2F-test превратить в 35.2%!
К сожалению, я не нашёл ablation по поводу того, помогает ли тут именно добавление автоформализованных задач, а не только Expert Iteration.

В пятницу подведём итоги.

@knowledge_accumulator