Resumen: Presentamos nuestro Leanabell-Prover-V2, un modelos de lenguaje grande 7B (LLMS) que puede producir pruebas formales del teorema en Lean 4, con una larga cadena de pensamientos (COT) integrada por el verificador. Después de nuestro trabajo anterior Leanabell-Prover-V1, continuamos optando por postrar a los modelos de Prover fuertes existentes para una mayor mejora del rendimiento. En nuestra versión V2, actualizamos principalmente el aprendizaje de refuerzo (RL) con los comentarios proporcionados por el verificador Lean 4. De manera crucial, la retroalimentación del verificador, como indicar el éxito o detallando errores específicos, permite que la LLM se convierta en “ autónomo ” de la corrección de su propio proceso de razonamiento y aprenda a corregir los errores reflexivamente. Leanabell-Prover-V2 optimiza directamente las trayectorias de razonamiento de LLM con interacciones verificadoras múltiples, junto con el enmascaramiento de token de retroalimentación para capacitación RL estable y una estrategia de recompensa simple. Los experimentos muestran que Leanabell-Prover-V2 mejora el rendimiento en un 3,2% (pase@128) con Kimina-Pres-Preview-Distill-7B y 2.0% (pase@128) con Deepseek-Presprase-V2-7B en el conjunto de pruebas MINIF2F. Los códigos de origen, los datos curados y los modelos están disponibles en: esta URL HTTPS.
Publicado Originalme en export.arxiv.org El 13 de julio de 2025.
Ver Fuente Original
