Resumen Técnico: Aprendizaje por Refuerzo Verificado por Procesos para la Demostración de Teoremas mediante Lean

Planteamiento del Problema

La Demostración Automática de Teoremas (ATP, por sus siglas en inglés) tiene como objetivo generar demostraciones formales para teoremas matemáticos. Si bien los Modelos de Lenguaje de Gran Escala (LLM) han avanzado en tareas de razonamiento, normalmente dependen del lenguaje natural (NL) o de recompensas binarias (correcto/incorrecto) durante el Aprendizaje por Refuerzo (RL). Esto crea una brecha:

1. Retroalimentación Dispersa: Los enfoques de RL estándar suelen utilizar únicamente una señal binaria final (la demostración pasa o falla), lo que proporciona una asignación de crédito dispersa y tiene dificultades para guiar al modelo a través de largas cadenas de razonamiento.
2. Estructurado vs. No Estructurado: A diferencia de los asistentes de demostración simbólica (p. ej., Lean, Coq, Isabelle), que ofrecen una verificación de tipo teórico fina de cada paso del razonamiento, los LLM se entrenan en secuencias de tokens con recompensas escalares.
3. Modelos de Recompensa de Proceso (PRM): Aunque trabajos recientes utilizan PRM para proporcionar recompensas a nivel de paso, estos suelen requerir grandes conjuntos de datos anotados o dependen de la supervisión de CoT basada en lenguaje natural, careciendo de la rigurosidad de la verificación simbólica.

El desafío central abordado es cómo aprovechar la retroalimentación rica y estructurada de un asistente de demostración simbólica (Lean) para entrenar LLM sin depender de PRM externos que puedan ser ruidosos o de anotaciones humanas.

Metodología

El artículo propone el Aprendizaje por Refuerzo Verificado por Procesos, un marco que integra la retroalimentación simbólica de Lean directamente en un objetivo de Optimización de Política Relativa de Grupo (GRPO). El método consta de tres componentes principales:

1. Oráculo de Proceso Simbólico

En lugar de tratar a Lean meramente como un verificador final, los autores lo utilizan como un oráculo de proceso durante el entrenamiento.

• Análisis (Parsing): Las demostraciones generadas se analizan en secuencias de tácticas ($T_1, \dots, T_N$) basadas en el Árbol de Sintaxis Abstracta (AST).
• Verificación: El proceso de elaboración de Lean proporciona dos tipos de señales:
  • Señal de Resultado: Una puntuación binaria global $g(Y) \in \{0, 1\}$ que indica si toda la demostración es válida.
  • Señal de Proceso: Retroalimentación detallada para cada táctica, identificando pasos localmente válidos y la ubicación específica del primer error.

2. Estrategia de Asignación de Crédito

Para cerrar la brecha entre la retroalimentación simbólica y el RL a nivel de token, los autores introducen reglas de asignación específicas:

• Propagación del Primer Error: Si una táctica $T_j$ falla, todas las tácticas subsiguientes ($T_k$ donde $k \ge j$) se consideran erróneas. Esto refleja la naturaleza causal de las demostraciones: un prefijo inválido invalida toda la cadena de razonamiento posterior.
• Puntuación a Nivel de Táctica ($\phi$):
  • Si la demostración pasa ($g(Y)=1$), todas las tácticas reciben una puntuación positiva (1).
  • Si la demostración falla ($g(Y)=0$):
    • Las tácticas antes del primer error reciben una puntuación parcial ($d_1$).
    • La primera táctica errónea y todas las subsiguientes reciben una puntuación de penalización ($d_2$).
• Mapeo a Nivel de Token: La ventaja a nivel de táctica se asigna únicamente al primer token de cada táctica (la palabra clave, p. ej., intro, apply). Esto se alinea con el punto de decisión semántica donde se determina la estrategia de la demostración.

3. Objetivo de RL (Integración con GRPO)

El marco combina ventajas de resultado y de proceso en un único objetivo GRPO:

• Ventaja de Resultado ($A_{outcome}$): Calculada basada en el estado global de paso/fallo relativo a la media del grupo.
• Ventaja de Proceso ($A_{process}$): Calculada basada en las puntuaciones de las tácticas, normalizadas por la media del grupo para tener en cuenta la dificultad del problema.
• Ventaja Combinada: Para un token $t$ que pertenece al primer token de la táctica $j$ en la respuesta $i$:
  $$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$$
  Para los tokens que no son los primeros, solo se aplica la ventaja de resultado. Esta formulación evita la necesidad de un modelo de valor o un PRM auxiliar, basándose únicamente en la verdad fundamental del verificador.

Contribuciones Clave

1. Formalización de la Retroalimentación Simbólica: Los autores formalizan la retroalimentación de nivel de táctica de Lean en señales de entrenamiento escalares, permitiendo una asignación de crédito fina a nivel de token sin guía de lenguaje natural.
2. RL Guiado por Verificador Simbólico: Integran recompensas de resultado y de táctica derivadas directamente de Lean en un marco de RL, proporcionando una asignación de crédito densa y verificable.
3. Mejoras de Benchmarks Estables: El enfoque demuestra mejoras consistentes en los benchmarks MiniF2F y ProofNet, superando el RL de solo resultado y los baselines vanilla sin requerir PRM externos o notación de lenguaje natural.

Resultados Experimentales

Los experimentos se realizaron utilizando STP-Lean y DeepSeek-Prover-V1.5 (modelos de 7B) en los benchmarks MiniF2F-Test y ProofNet-Test.

• Ganancias de Rendimiento:
  • STP-Lean: El método propuesto mejoró el pass@64 de MiniF2F en un +2.5% (de 56.7% a 59.2%) y el pass@32 de ProofNet en un +1.4%.
  • DeepSeek-Prover-V1.5: Se observaron mejoras consistentes, aunque marginales, en todos los entornos.
• Comparación con Baselines:
  • El método superó al GRPO de "Solo Resultado", que mostró inestabilidad y no logró mejorar en ProofNet en algunas configuraciones.
  • Logró resultados competitivos frente a fuertes baselines de búsqueda en árbol (p. ej., InternLM2.5-StepProver, DeepSeek-Prover-RL+RMaxTS) utilizando un enfoque de generación de un solo paso sin presupuestos masivos de búsqueda en tiempo de inferencia.
• Estudios de Ablación:
  • Asignación de Tokens: Asignar el crédito al primer token de una táctica produjo los resultados más estables en comparación con distribuir el crédito entre todos los tokens o al último token.
  • Propagación del Primer Error: Eliminar esta regla degradó significativamente el rendimiento, confirmando la necesidad de tratar los pasos subsiguientes como inválidos tras un error.
  • Timeouts: Un tiempo de espera de verificación de 15 segundos proporcionó el mejor equilibrio, fomentando demostraciones concisas sin descartar las complejas que son válidas.

Significado y Reivindicaciones

El artículo sostiene que los asistentes de demostración simbólica no deben verse únicamente como herramientas de evaluación, sino como oráculos activos de proceso de recompensa durante el entrenamiento. Al aprovechar la "retroalimentación estructurada rica y detallada" inherente a los sistemas de razonamiento formal, los autores demuestran un camino hacia marcos de RL que combinan la escalabilidad de los LLM con la fiabilidad de la verificación simbólica.

El estudio destaca que:

• Señales Densas y Verificables: El uso de los registros de error y los árboles de elaboración del propio demostrador proporciona una señal de recompensa densa y sólida que es superior a los resultados binarios dispersos o a los PRM aprendidos.
• Estabilidad: La combinación de recompensas de resultado globales y recompensas de táctica locales estabiliza el entrenamiento, evitando la convergencia prematura vista en el entrenamiento de solo tácticas y los problemas de dispersión del entrenamiento de solo resultado.
• Eficiencia: Este enfoque logra un rendimiento de vanguardia o competitivo sin la sobrecarga computacional de la búsqueda en árbol o los requisitos de datos para entrenar PRM separados.

Los autores mantienen la modestia respecto a las limitaciones, señalando que su método depende de puntuaciones de recompensa fijas ($d_1, d_2$) en lugar de estimadores de ventaja aprendidos y que actualmente se centra en demostraciones puras de Lean sin CoT, dejando abierto el diseño de recompensas para el razonamiento de lenguaje natural de larga extensión.