Leanabell-Prover: Skalierung nach dem Training im Bereich des formalen Denkens

Leanabell-Prover: Posttraining Scaling in Formal Reasoning

April 8, 2025

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

cs.AI

Zusammenfassung

Jüngste Fortschritte im Bereich des automatisierten Theorembeweises (ATP) durch LLMs haben das Potenzial des formalen Schließens mit Lean 4-Codes aufgezeigt. Allerdings wurde ATP noch nicht durch das kürzlich demonstrierte Posttraining-Scaling, wie es von Open AI O1/O3 und Deepseek R1 gezeigt wurde, revolutioniert. In dieser Arbeit untersuchen wir das gesamte Posttraining von ATP, mit dem Ziel, es mit den Durchbrüchen in den Schließmodellen für natürliche Sprachen in Einklang zu bringen. Zunächst trainieren wir aktuelle ATP-Modelle kontinuierlich mit einem hybriden Datensatz, der aus zahlreichen Aussage-Beweis-Paaren sowie zusätzlichen Daten besteht, die darauf abzielen, kognitive Verhaltensweisen zu integrieren, die menschliches Schließen und Hypothesenverfeinerung nachahmen. Anschließend untersuchen wir Verstärkungslernen unter Verwendung der Ergebnisbelohnung, die vom Lean 4-Compiler zurückgegeben wird. Durch unsere entwickelten kontinuierlichen Trainings- und Verstärkungslernprozesse haben wir bestehende formale Beweiser, einschließlich DeepSeek-Prover-v1.5 und Goedel-Prover, erfolgreich verbessert und Spitzenleistungen im Bereich der gesamten Beweisgenerierung erzielt. Beispielsweise erreichen wir eine Erfolgsquote von 59,8 % (pass@32) bei MiniF2F. Dies ist ein laufendes Projekt, und wir werden unsere Erkenntnisse kontinuierlich aktualisieren sowie unsere Daten und Trainingsdetails veröffentlichen.

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.