Leanabell-Prover: Масштабирование после обучения в формальных рассуждениях

Leanabell-Prover: Posttraining Scaling in Formal Reasoning

April 8, 2025

Авторы: Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, Kun Gai

cs.AI

Аннотация

Недавние достижения в области автоматизированного доказательства теорем (ATP) с использованием языковых моделей (LLMs) подчеркнули потенциал формальных рассуждений с использованием кода Lean 4. Однако ATP еще не претерпела революционных изменений благодаря последним достижениям в масштабировании после обучения, как это продемонстрировали модели Open AI O1/O3 и Deepseek R1. В данной работе мы исследуем весь процесс постобучения ATP, стремясь согласовать его с прорывами в моделях рассуждений для естественных языков. Для начала мы продолжаем обучение текущих моделей ATP на гибридном наборе данных, который включает множество пар "утверждение-доказательство", а также дополнительные данные, направленные на включение когнитивных поведений, имитирующих человеческое рассуждение и уточнение гипотез. Далее мы исследуем обучение с подкреплением, используя награды, возвращаемые компилятором Lean 4. Благодаря разработанным нами процессам непрерывного обучения и обучения с подкреплением, мы успешно улучшили существующие формальные проверы, включая DeepSeek-Prover-v1.5 и Goedel-Prover, достигнув передовых результатов в области генерации полных доказательств. Например, мы достигли показателя успешности 59,8% (pass@32) на тестовом наборе MiniF2F. Это продолжающийся проект, и мы будем постепенно обновлять наши результаты, публиковать данные и детали обучения.

English

Recent advances in automated theorem proving (ATP) through LLMs have highlighted the potential of formal reasoning with Lean 4 codes. However, ATP has not yet be revolutionized by the recent posttraining scaling as demonstrated by Open AI O1/O3 and Deepseek R1. In this work, we investigate the entire posttraining of ATP, aiming to align it with breakthroughs in reasoning models in natural languages.To begin, we continual train current ATP models with a hybrid dataset, which consists of numerous statement-proof pairs, and additional data aimed at incorporating cognitive behaviors that emulate human reasoning and hypothesis refinement. Next, we explore reinforcement learning with the use of outcome reward returned by Lean 4 compiler. Through our designed continual training and reinforcement learning processes, we have successfully improved existing formal provers, including both DeepSeek-Prover-v1.5 and Goedel-Prover, achieving state-of-the-art performance in the field of whole-proof generation. For example, we achieve a 59.8% pass rate (pass@32) on MiniF2F. This is an on-going project and we will progressively update our findings, release our data and training details.