Leanabell-Prover: Escalado Postentrenamiento en Razonamiento Formal

Leanabell-Prover: Posttraining Scaling in Formal Reasoning

April 8, 2025

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

cs.AI

Resumen

Los recientes avances en la demostración automática de teoremas (ATP, por sus siglas en inglés) a través de modelos de lenguaje de gran escala (LLMs) han destacado el potencial del razonamiento formal con códigos de Lean 4. Sin embargo, el ATP aún no ha sido revolucionado por el escalamiento posentrenamiento reciente, como lo han demostrado Open AI O1/O3 y Deepseek R1. En este trabajo, investigamos todo el proceso de posentrenamiento del ATP, con el objetivo de alinearlo con los avances en los modelos de razonamiento en lenguajes naturales. Para comenzar, entrenamos continuamente los modelos actuales de ATP con un conjunto de datos híbrido, que incluye numerosos pares de enunciado-prueba, además de datos adicionales destinados a incorporar comportamientos cognitivos que emulan el razonamiento humano y el refinamiento de hipótesis. A continuación, exploramos el aprendizaje por refuerzo utilizando las recompensas de resultados devueltas por el compilador de Lean 4. A través de nuestros procesos diseñados de entrenamiento continuo y aprendizaje por refuerzo, hemos mejorado con éxito los demostradores formales existentes, incluyendo tanto DeepSeek-Prover-v1.5 como Goedel-Prover, logrando un rendimiento de vanguardia en el campo de la generación de pruebas completas. Por ejemplo, alcanzamos una tasa de aprobación del 59.8% (pass@32) en MiniF2F. Este es un proyecto en curso y actualizaremos progresivamente nuestros hallazgos, liberando nuestros datos y detalles de entrenamiento.

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.