LeanPRM: Lean etiquetó 152 000 pasos de demostraciones sin humanos y elevó la precisión hasta el 74,7%

Verificar las demostraciones matemáticas largas que escriben los modelos de lenguaje se está convirtiendo en un cuello de botella. Los autores de LeanPRM proponen obtener el etiquetado paso a paso del asistente de demostraciones Lean, sin anotadores. El resultado es un conjunto de datos con 10 634 demostraciones y 152 mil pasos etiquetados. Un verificador basado en Qwen3-4B y entrenado con él subió la coincidencia exacta con la etiqueta del paso del 48,2 al 74,7 en el conjunto reservado LeanPRM-Bench (200 demostraciones). El mismo modelo base entrenado con PRM800K obtuvo 60,3.

De dónde salen las etiquetas

Un verificador de proceso (PRM) solo se puede entrenar con datos en los que cada paso tiene una valoración de «correcto» o «incorrecto». Con demostraciones abiertas, esas etiquetas son difíciles de conseguir. Los anotadores humanos son caros. Las etiquetas derivadas de la respuesta final no sirven, porque una demostración no tiene un número con el que contrastar el resultado. Y formalizar cada demostración en Lean exige el trabajo de expertos.

LeanPRM sortea estas limitaciones de la siguiente manera. El modelo escribe la demostración en lenguaje natural y, en paralelo, una demostración formal, sin recibir retroalimentación de Lean. Después, Lean comprueba la versión formal y asigna una etiqueta a cada paso. Un segundo modelo descarta los casos en los que el fallo se debe únicamente a la sintaxis del texto formal. Así, las etiquetas negativas reflejan errores matemáticos y no defectos de transcripción.

Qué muestran los números

Principales resultados del artículo:

• conjunto de datos: 10 634 demostraciones, 152 mil pasos con etiquetas, sin etiquetado manual;
• LeanPRM-Bench (200 demostraciones reservadas): Qwen3-4B pasó de 48,2 a 74,7 de coincidencia exacta por pasos;
• línea base PRM800K con el mismo modelo: 60,3;
• en tres de cuatro benchmarks externos, el verificador entrenado con LeanPRM supera a la versión entrenada con PRM800K;
• en la selección best-of-N con problemas de nivel IMO, elige demostraciones de mayor calidad;
• la mejora se confirma en modelos de 0,6B a 8B parámetros en LeanPRM-Bench, Hard2Verify e IMO-GradingBench.

Que el efecto se mantenga en todos los tamaños importa tanto como la cifra récord. La mejora se ve tanto en un modelo muy pequeño como en el de 8B. Es decir, el mérito está en la calidad de la señal y no en haber acertado con una configuración concreta.

Dónde conviene mirar con más atención

La brecha principal, 48,2 frente a 74,7, se midió en un benchmark que construyeron los propios autores, con los mismos procedimientos de generación y etiquetado. Para una muestra así, el entrenamiento con LeanPRM tiene una ventaja natural. Por eso las pruebas externas valen más: ahí la mejora aparece en tres benchmarks de cuatro, es decir, no en todos. La descripción del artículo no aclara qué ocurre con el cuarto, y conviene comprobarlo en el texto completo.

Hay además una limitación estructural. Las etiquetas son tan fiables como la correspondencia entre la demostración formal y la natural. Si el modelo escribe una versión formal que se aparta del texto, Lean evaluará algo distinto de lo que lee una persona. El filtro del segundo modelo reduce el riesgo de ruido por sintaxis, pero no garantiza que las dos versiones coincidan por completo. El alcance también es limitado: solo se puede etiquetar lo que se logró formalizar.

El valor práctico está en la escalabilidad. El volumen de datos crece con el número de enunciados formales disponibles, no con el presupuesto para expertos. Para los equipos que entrenan modelos matemáticos con best-of-N o con RL sobre recompensas de proceso, es una vía para obtener una señal densa en los pasos de razonamiento sin comprar etiquetado. Para evaluar el enfoque, conviene pasar el propio verificador por Hard2Verify e IMO-GradingBench. También es útil comprobar hasta qué punto se mantiene la mejora en demostraciones de áreas alejadas de las formalizadas en Lean.