Leanabell-Prover: Posttraining Schaalvergroting in Formeel Redeneren

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

Samenvatting

Recente vooruitgang in automatisch theorema bewijzen (ATP) door middel van LLM's heeft het potentieel van formeel redeneren met Lean 4-codes benadrukt. Echter, ATP is nog niet gerevolutioneerd door de recente posttraining-schaalvergroting zoals gedemonstreerd door OpenAI O1/O3 en Deepseek R1. In dit werk onderzoeken we de volledige posttraining van ATP, met als doel deze af te stemmen op doorbraken in redeneermodellen in natuurlijke talen. Om te beginnen trainen we huidige ATP-modellen voortdurend met een hybride dataset, die bestaat uit talrijke statement-bewijsparen en aanvullende data gericht op het integreren van cognitief gedrag dat menselijk redeneren en hypothesenverfijning nabootst. Vervolgens verkennen we reinforcement learning met behulp van uitkomstbeloningen die worden geretourneerd door de Lean 4-compiler. Door onze ontworpen voortdurende training en reinforcement learning-processen hebben we bestaande formele bewijzers, waaronder zowel DeepSeek-Prover-v1.5 als Goedel-Prover, succesvol verbeterd, wat resulteert in state-of-the-art prestaties op het gebied van volledig bewijsgeneratie. We behalen bijvoorbeeld een slagingspercentage van 59,8% (pass@32) op MiniF2F. Dit is een doorlopend project en we zullen onze bevindingen geleidelijk bijwerken, evenals onze data en trainingsdetails vrijgeven.

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.