Thor [2022]: комбинируем языковую модель и молотки

Программы и инструменты для доказательства теорем это отдельная вселенная, которую я за короткое время не смог полностью осознать. Я мучил вопросами ChatGPT, перечитывал статью кругами, и в итоге вроде бы смог немного понять суть.

Есть тут такая вещь, как hammer-ы - это название для "традиционных" методов поиска доказательств утверждения. Они работают, получая на вход утверждение в формализованном виде, и какой-то эвристикой находя его доказательство. Конечно же, возможности молотков сильно ограничены, но простые леммы доказывать умеет.

В то же время, есть система типа GPT-f. В статье утверждается, что успех GPT-f и hammer-ов плохо скоррелирован, потому что GPT-f плохо умеет находить факт, который нужно использовать, а hammer-ы плохи в длинных док-вах. Поэтому их нужно использовать вместе!

Делают это так же, как языковые модели учат использовать API: в датасет для файнтюна GPT-f интегрируют токен вызова <hammer>, который будет просить молоток доказать данное утверждение. Такой гибрид и есть Thor. Генерируется датасет из тех утверждений, которые hammer успешно доказывает. Пример совместной работы человека и hammer-ов см. на картинке, нейросеть тут делает по сути кусок слева, строя своё дерево.

Результаты: в статьях после GPT-f используют уже не только Metamath. Все последние работы тестируют на miniF2F - интегрированном бенчмарке из разных сервисов / датасетов.

Молоток сам решает 10%, GPT-f без дообучения (в том посте описана эта процедура) 24%, объединение этих задач - это 27.5%. Thor решает 29.9% без дообучения. При этом GPT-f с дообучением решает 29.6%. Объединение Thor и дообучения на своих же доказательствах находится за рамками этой статьи.

В среду вас ждёт SOTA на miniF2F, пристегните ремни!

@knowledge_accumulator