Leanabell-Prover: Scalabilità Post-Addestramento nel Ragionamento Formale

Leanabell-Prover: Posttraining Scaling in Formal Reasoning

April 8, 2025

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

cs.AI

Abstract

I recenti progressi nel campo del teorema automatico (ATP) attraverso i modelli linguistici di grandi dimensioni (LLMs) hanno evidenziato il potenziale del ragionamento formale con codici Lean 4. Tuttavia, l'ATP non è stato ancora rivoluzionato dal recente scalamento post-addestramento, come dimostrato da Open AI O1/O3 e Deepseek R1. In questo lavoro, indaghiamo l'intero processo post-addestramento dell'ATP, con l'obiettivo di allinearlo alle innovazioni nei modelli di ragionamento per i linguaggi naturali. Per iniziare, addestriamo continuamente i modelli ATP attuali con un dataset ibrido, composto da numerose coppie di enunciato-dimostrazione, e dati aggiuntivi mirati a incorporare comportamenti cognitivi che emulano il ragionamento umano e il perfezionamento delle ipotesi. Successivamente, esploriamo l'apprendimento per rinforzo utilizzando la ricompensa basata sui risultati restituiti dal compilatore Lean 4. Attraverso i nostri processi di addestramento continuo e apprendimento per rinforzo, abbiamo migliorato con successo i dimostratori formali esistenti, inclusi sia DeepSeek-Prover-v1.5 che Goedel-Prover, raggiungendo prestazioni all'avanguardia nel campo della generazione di dimostrazioni complete. Ad esempio, otteniamo un tasso di successo del 59,8% (pass@32) su MiniF2F. Questo è un progetto in corso e aggiorneremo progressivamente i nostri risultati, rilasciando i nostri dati e i dettagli dell'addestramento.

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.