💻 computer science

Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study

Este estudio revela que los demostradores de teoremas Lean entrenados con RL sufren de colapso de modo en tiempo de inferencia, lo cual puede mitigarse eficazmente aplicando un calendario fijo de esqueletos de tácticas diversos para recuperar ganancias significativas de rendimiento, mientras que el parafraseo de prompts y los comentarios irrelevantes resultan ineficaces o perjudiciales.

Autores originales: Zachary Burton

Publicado 2026-05-19

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Zachary Burton

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina a un estudiante brillante que ha sido entrenado para resolver acertijos matemáticos muy difíciles usando un lenguaje informático especial llamado Lean. Este estudiante, llamémoslo "DeepSeek", es increíblemente inteligente pero tiene un hábito extraño: cuando se le pide resolver un acertijo, se queda atrapado en un carril mental.

Este artículo es un informe de diagnóstico sobre por qué ocurre esto y cómo solucionarlo. Aquí está la historia de lo que descubrieron los investigadores, contada en términos cotidianos.

1. El Problema: El Efecto del "Disco Rayado"

Los investigadores notaron que cuando pedían a DeepSeek resolver el mismo acertijo matemático una y otra vez (solo con semillas aleatorias ligeramente diferentes, como lanzar dados), el estudiante seguía intentando exactamente el mismo primer paso.

La Analogía: Imagina que estás intentando abrir una puerta cerrada con llave. Pruebas la llave en la cerradura. No funciona. Lo intentas de nuevo. Aún no funciona. Lo intentas por tercera vez, y por centésima vez. Incluso si lo intentas 64 veces, solo estás introduciendo la misma llave en la misma cerradura de la misma manera. No estás explorando otras llaves ni otras formas de abrir la puerta.
El Resultado: En el estudio, duplicar el número de intentos de 32 a 64 no resolvió un solo acertijo nuevo. El estudiante había sufrido un "colapso de modo": estaba atrapado en un camino estrecho y no podía pensar en nada más.

2. La Solución: Dar una Pista de "Primer Paso"

Los investigadores se dieron cuenta de que el estudiante no era perezoso; simplemente estaba demasiado atrapado en su rutina. Así que probaron un nuevo truco: antes de pedirle al estudiante que resolviera el acertijo, le dieron una instrucción específica sobre cómo empezar.

La Analogía: En lugar de decir simplemente "Resuelve este acertijo", los investigadores dijeron "Empieza simplificando los números" o "Empieza introduciendo una nueva variable". Es como darle al estudiante una llave específica para probar primero, en lugar de dejar que adivine.
El Resultado: Este simple empujón rompió el carril. De repente, el estudiante comenzó a resolver muchos más acertijos. El "carril" no se debía a que el estudiante fuera malo en matemáticas; se debía a que era demasiado rígido en cómo comenzaba.

3. El "Por Qué": Es un Problema de Entrenamiento, No de Cerebro

Los investigadores querían saber: ¿Es el estudiante naturalmente malo en matemáticas, o fue el entrenamiento el que lo volvió rígido?

El Experimento: Probaron al estudiante antes de recibir el entrenamiento matemático especial (el modelo "Base").
El Hallazgo: El estudiante no entrenado no podía resolver ningún acertijo en absoluto. Simplemente se rendía o repetía la pregunta.
La Conclusión: El entrenamiento especial (Aprendizaje por Refuerzo) fue lo que enseñó al estudiante a resolver acertijos en primer lugar. Pero, ese mismo entrenamiento es también lo que lo volvió rígido y lo atrapó en un carril. El entrenamiento creó la habilidad, pero también creó el problema del "disco rayado".

4. ¿Quién Más Tiene Este Problema?

Los investigadores probaron a otros "estudiantes" (diferentes modelos de IA) para ver si este era un problema universal.

El Estudiante "SFT": Un estudiante fue entrenado de manera diferente (Ajuste Fino Supervisado). Este estudiante era en realidad mejor resolviendo acertijos en general, pero no tenía el problema del "carril". Cuando los investigadores le dieron pistas, en realidad lo hizo ligeramente peor. Ya era lo suficientemente flexible como para encontrar su propio camino.
Los Estudiantes "RL": Los estudiantes entrenados con el método especial de "Aprendizaje por Refuerzo" (como DeepSeek) fueron los que se quedaron atrapados. Necesitaban las pistas de "primer paso" para salir de su pensamiento estrecho.

5. La Evidencia del "Primer Movimiento"

Para demostrar que esto no era solo una casualidad, los investigadores examinaron los "primeros movimientos" reales que hacían los estudiantes.

El Hallazgo: De 64 intentos en un solo acertijo, el estudiante "atrapado en un carril" usó exactamente el mismo primer movimiento en casi la mitad de los casos. Era increíblemente predecible.
La Metáfora: Si le pidieras a un humano que escribiera una historia 64 veces, podría empezar con "Érase una vez", "El sol brillaba" o "Era una noche oscura". Pero este estudiante de IA empezaría con "Érase una vez" 32 veces, y "El sol brillaba" 30 veces. Tenía casi ninguna variedad en su apertura.

Resumen

El artículo concluye que el Aprendizaje por Refuerzo (una forma específica de entrenar IA) crea un arma de doble filo:

Enseña a la IA a resolver pruebas matemáticas formales (algo que no podía hacer antes).
Pero también hace que la IA se enfoque tanto en unas pocas estrategias "ganadoras" que deja de explorar nuevas.

La solución no es darle a la IA más potencia de cálculo ni más tiempo para pensar; es darle guía estructural: un simple empujón sobre cómo comenzar la prueba. Esto obliga a la IA a romper su rutina y explorar nuevos caminos, desbloqueando soluciones que anteriormente era demasiado terca para encontrar.

Resumen Técnico: Diversidad en el Momento de Inferencia en Provers de Teoremas Lean Entrenados con RL

Declaración del Problema

Los recientes provers de teoremas neuronales, particularmente aquellos entrenados con Aprendizaje por Refuerzo (RL) y recompensas verificables (RLVR), han logrado un rendimiento sólido en benchmarks de pruebas formales como miniF2F. La hipótesis predominante es que un entrenamiento suficiente con RL y un aumento en el cómputo en el momento de la inferencia (mediante muestreo i.i.d.) permiten a los modelos internalizar los priores estructurales necesarios para las pruebas formales.

Este trabajo desafía esa hipótesis, diagnosticando un fenómeno de colapso de modos en el momento de la inferencia en provers Lean entrenados con RL. Específicamente, los autores observan que aumentar el presupuesto de muestreo ( $k$ ) produce rendimientos decrecientes mucho antes de lo esperado. En el benchmark miniF2F-test con DeepSeek-Prover-V1.5-RL, duplicar el presupuesto de muestreo de $k=32$ a $k=64$ produce cero teoremas resueltos adicionales (estancado en 42/244). El modelo converge en un conjunto estrecho de estrategias de prueba y falla al explorar alternativas, incluso cuando se le proporcionan muestras estocásticas adicionales.

Metodología

El estudio emplea un marco de diagnóstico controlado utilizando DeepSeek-Prover-V1.5-RL y su variante base sin RL, junto con comparaciones entre modelos con DeepSeek-Prover-V2-7B (RL) y Goedel-Prover (solo SFT).

1. La Intervención del Calendario de Esqueletos

Para probar si la meseta se debe a una falta de diversidad estructural en lugar de una falta de cómputo, los autores introducen un calendario fijo y determinista de 15 esqueletos de tácticas.

Estructura: Una cuadrícula de $15 \times 8 = 120$ que combina 15 esqueletos de tácticas Lean seleccionados a mano (por ejemplo, simp, intro, constructor, aesop) con 8 comentarios de pista de objetivo (sugerencias en lenguaje natural).
Ejecución: Para un presupuesto $k$ , el modelo intenta las primeras $k$ entradas de esta cuadrícula. Esto obliga al modelo a comenzar las pruebas con aperturas estratégicas específicas en lugar de depender del muestreo aleatorio.
Ablaciones: Para aislar la fuente de mejora, los autores comparan:
- B-RL (Esqueleto): El calendario estructurado de 15 esqueletos.
- C1 (Parafraseo): 16 parafraseos semánticamente equivalentes de las instrucciones (sin estructura de táctica).
- C2 (Comentarios Irrelevantes): 16 comentarios en Lean sin contenido.
- C3 (Solo NL): Una condición dedicada que utiliza solo pistas en lenguaje natural sin prefijos de táctica.

2. Estratificación de la Dificultad

Los autores definen una puntuación empírica de dificultad de formalización ( $\sigma$ ) utilizando una construcción de leave-one-out. Para un teorema objetivo, $\sigma$ cuenta cuántos otros modelos base (Goedel-Prover, V2-7B) lo resuelven sin intervención. Esto estratifica los teoremas en grupos: Frontera (no resueltos por otros), Difícil, Medio, Fácil y Trivial.

3. Medición Directa de la Distribución

Para ir más allá de las mesetas conductuales, los autores analizan la diversidad de la cabeza de la primera táctica a través de 13,159 muestras estocásticas. Cuentan el número de identificadores de tácticas principales distintos (por ejemplo, have, rw, norm_num) generados por teorema.

Resultados Clave

1. Rompiendo la Meseta mediante Guía Estructural

Colapso de la Línea Base: DeepSeek-Prover-V1.5-RL con muestreo i.i.d. resuelve 38 teoremas en $k=16$ , 42 en $k=32$ , y se mantiene en 42 en $k=64$ .
Eficacia del Esqueleto: El calendario fijo de esqueletos rompe esta meseta, resolviendo 55 teoremas en $k=16$ (+45% de mejora relativa) y continuando encontrando nuevas pruebas hasta $k=64$ (60 en total).
Hallazgos de Ablación:
- Estructura vs. Diversidad: Los parafraseos de instrucciones (C1) producen el mismo pass@16 que la línea base (38/244), mientras que los comentarios irrelevantes (C2) degradan el rendimiento a 25/244. Esto confirma que las ganancias son impulsadas por la guía estructural, no por la mera diversidad de prompts.
- NL vs. Tácticas: La condición solo NL (C3) resuelve 48/244, intermedia entre la línea base y los esqueletos completos. Esto indica que las pistas en lenguaje natural recuperan aproximadamente el 58% de la brecha, mientras que los prefijos literales de táctica contribuyen con el resto.

2. Localización de la Ganancia

La ganancia estructural se concentra en los grupos Fácil y Trivial (teoremas resolubles por otros provers de código abierto pero perdidos por el muestreo i.i.d. de V1.5-RL).

En la columna combinada Fácil+Trivial, la intervención de esqueleto produce una ganancia neta de +15, mientras que los parafraseos producen 0 y los comentarios irrelevantes producen -14.
Ninguna perturbación desbloquea el grupo "Frontera" (teoremas no resueltos por ninguna línea base), lo que sugiere que la intervención remedia la subexploración de problemas conocidos resolubles en lugar de expandir la frontera de capacidad.

3. Especificidad del RL del Colapso de Modos

Contraste con el Modelo Base: DeepSeek-Prover-V1.5-Base (sin RL) prueba cero teoremas bajo cualquier condición (i.i.d. o esqueletos). Esto establece que el RL es el locus tanto de la capacidad de prueba como del posterior colapso de modos. El modelo base carece de la capacidad para generar pruebas válidas; la etapa de RL crea la capacidad pero la colapsa en una política estrecha.
Contraste entre Modelos:
- V2-7B (RL): Muestra una ganancia agregada plana (+1) pero desbloquea +3 teoremas de frontera inalcanzables por cualquier línea base i.i.d.
- Goedel-Prover (SFT): Muestra una ganancia negativa (-10.0 $\pm$ 4.4) con esqueletos. Los modelos entrenados con SFT parecen ya explorar un conjunto amplio de tallos de tácticas, lo que hace que el calendario fijo de esqueletos sea redundante o restrictivo.

4. Evidencia Directa del Colapso

El análisis distribucional revela que el teorema mediano recibe solo 2 cabezas de primera táctica distintas a través de 64 muestras, con el 49% del benchmark recibiendo una apertura estratégica única determinista. La entropía de Shannon observada es $\le 8\%$ de la capacidad teórica, confirmando un severo colapso de modos.

Significado y Afirmaciones

El trabajo reencuadra la narrativa de "los esqueletos de tácticas mejoran el rendimiento" a "los provers entrenados con RL subexploran severamente el espacio de tácticas en el momento de la inferencia".

RL como Agente Dual: Los autores afirman que el RL juega un doble papel: es la etapa que crea la capacidad de prueba (ya que el modelo base no tiene ninguna) y simultáneamente la etapa que colapsa esa capacidad sobre una política estrecha.
Escalado en el Momento de la Inferencia: Los resultados sugieren que simplemente escalar el cómputo de inferencia mediante muestreo i.i.d. tiene rendimientos decrecientes mucho antes de lo asumido. La diversidad estructural (variando estrategias de prueba mediante prompts) es un eje más eficiente para el escalado.
Remediabilidad: El colapso de modos es específico de los modelos entrenados con RL. Los modelos entrenados con SFT no exhiben el mismo colapso recuperable mediante pistas estructurales; de hecho, sufren por ello. Esto implica que las futuras intervenciones (regularización de entropía en el momento del entrenamiento o recuperación de esqueletos en el momento de la inferencia) deben navegar la compensación entre crear capacidad y mantener la diversidad.

El estudio concluye que el "colapso de modos" es un fenómeno real, contingente al pipeline e inherente al proceso de ajuste fino con RL en dominios de verificación formal, y que las intervenciones estructurales fijas pueden recuperar efectivamente la exploración perdida sin requerir entrenamiento adicional.