Leanabell-Prover : Mise à l'échelle post-entraînement en raisonnement formel

Leanabell-Prover: Posttraining Scaling in Formal Reasoning

April 8, 2025

Auteurs: Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, Kun Gai

cs.AI

Résumé

Les récents progrès dans la démonstration automatique de théorèmes (ATP) grâce aux LLM ont mis en lumière le potentiel du raisonnement formel avec les codes Lean 4. Cependant, l'ATP n'a pas encore été révolutionnée par le récent passage à l'échelle post-entraînement, comme l'ont démontré Open AI O1/O3 et Deepseek R1. Dans ce travail, nous étudions l'ensemble du post-entraînement de l'ATP, dans le but de l'aligner sur les avancées des modèles de raisonnement en langage naturel. Pour commencer, nous entraînons continuellement les modèles actuels d'ATP avec un ensemble de données hybride, composé de nombreuses paires énoncé-preuve, ainsi que de données supplémentaires visant à intégrer des comportements cognitifs imitant le raisonnement humain et l'affinement d'hypothèses. Ensuite, nous explorons l'apprentissage par renforcement en utilisant les récompenses de résultat retournées par le compilateur Lean 4. Grâce à nos processus d'entraînement continu et d'apprentissage par renforcement, nous avons réussi à améliorer les démonstrateurs formels existants, notamment DeepSeek-Prover-v1.5 et Goedel-Prover, atteignant des performances de pointe dans le domaine de la génération de preuves complètes. Par exemple, nous obtenons un taux de réussite de 59,8 % (pass@32) sur MiniF2F. Il s'agit d'un projet en cours, et nous mettrons progressivement à jour nos découvertes, ainsi que nos données et détails d'entraînement.

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.