Hugging Face libera el método que usó para entrenar modelos de IA capaces de demostrar teoremas matemáticos
La plataforma publica kimina-prover-rl, un sistema de entrenamiento que enseña a modelos pequeños de lenguaje a resolver pruebas formales en Lean 4 mediante razonamiento estructurado y aprendizaje por refuerzo
Hugging Face publicó kimina-prover-rl, un sistema de entrenamiento de código abierto que enseña a modelos de lenguaje a resolver demostraciones matemáticas en Lean 4 (un lenguaje para verificar pruebas formales). El método usa aprendizaje por refuerzo y divide las respuestas en razonamiento natural seguido de código verificable. Con él entrenaron dos modelos pequeños que establecen récords de rendimiento en su categoría.
Hugging Face (una plataforma donde desarrolladores comparten y descargan modelos de IA ya entrenados) ha publicado kimina-prover-rl, un sistema de entrenamiento de código abierto que enseña a modelos de lenguaje a resolver demostraciones matemáticas formales en Lean 4 (un lenguaje de programación especializado en verificar pruebas matemáticas con rigor absoluto). El método, inspirado en DeepSeek-R1, divide la generación del modelo en dos etapas: primero produce un razonamiento en lenguaje natural y después el código verificable, lo que según sus creadores mejora la capacidad de corrección de errores y hace más transparente el proceso.
El sistema se entrena mediante GRPO (un algoritmo de aprendizaje por refuerzo diseñado específicamente para modelos de lenguaje grandes), implementado sobre Verl (una biblioteca de código abierto para entrenar modelos con refuerzo). Durante el entrenamiento, el modelo genera múltiples soluciones para cada problema y recibe una recompensa de 1 solo si el código Lean resultante es verificado correctamente por un servidor especializado llamado kimina-lean-server. Para garantizar que las respuestas sigan el formato correcto, el sistema penaliza salidas mal estructuradas con recompensa cero, independientemente de si la demostración matemática es válida.
Una característica destacada es el mecanismo de corrección de errores: cuando una demostración falla, el sistema crea automáticamente un nuevo ejemplo de entrenamiento donde el modelo recibe el mensaje de error de Lean y tiene la oportunidad de revisar su razonamiento y código. Esto permite que el modelo aprenda de sus propios fallos durante el entrenamiento, una capacidad que los desarrolladores consideran fundamental para mejorar el rendimiento en problemas complejos. El método también incluye filtros para rechazar respuestas excesivamente verbosas o con razonamiento repetitivo.
Hugging Face ha liberado dos modelos entrenados con este sistema: uno de 1.700 millones de parámetros que alcanza un 76,63% de éxito en el benchmark MiniF2F (un conjunto de prueba estándar para medir capacidad de demostración formal), y otro de 600 millones de parámetros con 71,30% de éxito. Según la compañía, ambos establecen nuevos récords de rendimiento entre modelos de código abierto en sus respectivas categorías de tamaño. El entrenamiento del modelo más grande tomó 48 horas en 8 GPUs H100 (procesadores gráficos especializados en entrenar modelos de IA de última generación), y el código completo está disponible en un fork de Verl.
