Resumen Técnico: FormalRewardBench

Enunciado del Problema

Los avances recientes en demostradores de teoremas neuronales dependen en gran medida del Aprendizaje por Refuerzo con Recompensas Verificables (RLVR). En este paradigma, los asistentes de demostración (como Lean 4) proporcionan señales binarias de corrección (aprobado/reprobado) basadas en la verificación de tipos. Aunque estas señales son escalables e inmunes a la manipulación de recompensas, sufren de asignación de crédito dispersa: los modelos no reciben ninguna señal de aprendizaje para el progreso parcial en problemas difíciles, ya que una demostración que falla en el paso final recibe la misma recompensa cero que un enfoque completamente incorrecto.

Para mitigar esto, los investigadores han propuesto modelos de recompensa aprendidos capaces de evaluar la calidad de las demostraciones más allá de la verificación binaria. Sin embargo, comparar estos modelos de recompensa es actualmente un desafío porque típicamente requiere costosas ablaciones de entrenamiento por Aprendizaje por Refuerzo (RL). Además, las evaluaciones existentes para modelos de recompensa (por ejemplo, RewardBench, ProcessBench) se centran en el razonamiento en lenguaje natural informal y no abordan la precisión sintáctica, la corrección de tipos y la validez lógica requeridas para la demostración formal de teoremas. Actualmente no existe ninguna evaluación para evaluar directamente los modelos de recompensa en demostraciones formales sin ejecuciones de entrenamiento.

Metodología

Los autores presentan FormalRewardBench, la primera evaluación diseñada para evaluar modelos de recompensa para la demostración formal de teoremas en Lean 4. La evaluación consta de 250 pares de preferencia, donde cada par contiene una demostración correcta verificada formalmente y una variante incorrecta.

Construcción del Conjunto de Datos

El conjunto de datos se deriva de MiniF2F, una colección de 488 problemas matemáticos de nivel olímpico formalizados en Lean 4. Los autores emplean una canalización controlada de inyección de errores para generar demostraciones incorrectas que satisfacen tres criterios:

1. Validez Sintáctica: La demostración incorrecta debe analizarse como código Lean válido.
2. Plausibilidad Semántica: Los errores no deben ser triviales (por ejemplo, variables no definidas), sino que deben reflejar modos de fallo realistas.
3. Patrones de Error Realistas: Los errores deben imitar fallos reales de Modelos de Lenguaje Grandes (LLM).

Estrategias de Inyección de Errores

Se utilizan cinco estrategias curadas por expertos para generar variantes incorrectas, implementadas mediante prompts a un LLM de vanguardia (Claude Opus 4.5):

1. Variaciones Mínimas de Punto Único: Modificaciones quirúrgicas a demostraciones correctas (por ejemplo, intercambiar hipótesis, cambiar un solo nombre de variable o lema) que causan un fallo semántico mientras mantienen la validez sintáctica.
2. Justificación en Lenguaje Natural: Aumentar las demostraciones incorrectas con comentarios en lenguaje natural engañosos que justifican el razonamiento defectuoso, probando el "sesgo de verbosidad".
3. Inyección de Código Python: Reemplazar pasos de demostración formal Lean con código Python ejecutable que pueda resolver el problema computacionalmente pero que falla en el requisito de una demostración formal (probando la adherencia a la tarea).
4. Errores Forzados del LLM: Generar demostraciones que contengan errores formales comunes identificados en salidas anteriores de modelos, como la aplicación incorrecta de tácticas, la selección incorrecta de hipótesis o la instanciación incorrecta de lemas.
5. Demostraciones Incorrectas Verbosas: Generar demostraciones innecesariamente largas con estructuras sofisticadas y lemas intermedios que camuflan fallos lógicos fundamentales.

Protocolo de Evaluación

La evaluación evalúa los modelos en dos configuraciones:

• Puntual: El modelo puntúa cada demostración independientemente; la precisión se mide si la puntuación de la demostración correcta supera a la incorrecta.
• Por Pares: El modelo compara dos demostraciones y genera una preferencia. Para mitigar el sesgo de posición, la precisión solo se cuenta si el modelo identifica consistentemente la demostración correcta en ambos ordenamientos (correcto-primero y correcto-segundo).

Resultados Clave

Los autores evaluaron cuatro categorías de modelos: LLMs de vanguardia, LLMs Jueces, LLMs de Propósito General y Modelos Especializados en Demostración de Teoremas.

1. Jerarquía de Rendimiento: Los LLMs de vanguardia (por ejemplo, Claude Opus 4.5) lograron el rendimiento más alto (59.8% de precisión por pares). Los LLMs Jueces (entrenados en datos de preferencia) superaron sustancialmente a los demostradores de teoremas especializados entre modelos de pesos abiertos (52.8% frente a 12.8% para algunos modelos especializados).
2. La Brecha Generación-Evaluación: Los modelos especializados en demostración de teoremas (por ejemplo, DeepSeek-Prover-V2-7B, Gödel-Prover-V2-8B) obtuvieron el peor rendimiento (oscilando entre 0.0% y 24.4%). A pesar de lograr métricas state-of-the-art de pass@k en MiniF2F, estos modelos luchan para evaluar demostraciones. Los autores atribuyen esto a una falta de entrenamiento en detección de errores; estos modelos están optimizados para generar demostraciones correctas mediante SFT y RLVR, pero no han aprendido a identificar ni criticar errores.
3. Gradiente de Dificultad de Errores:
   • Más Fácil: Inyección de Código Python (S3), donde la detección depende de la identificación del idioma en lugar de la comprensión de la demostración.
   • Más Difícil: Demostraciones Incorrectas Verbosas (S5) y Errores Forzados (S4). Incluso los mejores modelos lograron solo ~60% en S5 y ~50% en S4.
   • Limitaciones del Modelo Juez: Los modelos jueces mostraron un patrón bimodal: rendimiento casi perfecto en la inyección de Python pero colapsando a casi cero en demostraciones verbosas, lo que sugiere que su entrenamiento en preferencias desarrolla una discriminación superficial en lugar de un razonamiento formal profundo.
4. Sesgo de Posición: Se observó un sesgo de posición significativo en todas las categorías, particularmente en los demostradores especializados (por ejemplo, DeepSeek-Prover-V2-7B prefirió la primera demostración el 94.9% de las veces independientemente de la corrección).

Significado y Afirmaciones

El artículo afirma tres contribuciones principales:

1. FormalRewardBench: Una evaluación novedosa que permite la comparación directa de modelos de recompensa para la demostración formal de teoremas sin la necesidad de costosas ablaciones de entrenamiento por RL.
2. Metodología: Un conjunto reutilizable de cinco estrategias de inyección de errores para generar demostraciones formales incorrectas realistas, aplicable a otros asistentes de demostración, aumento de datos o diseño curricular.
3. Perspectiva Empírica: El hallazgo de que las capacidades generales de modelado de recompensas (encontradas en modelos de vanguardia y jueces) se transfieren más efectivamente a la evaluación de demostraciones que el entrenamiento específico del dominio en demostración de teoremas.

Los autores enfatizan que, aunque desarrollar modelos de recompensa efectivos podría acelerar el descubrimiento y la verificación matemáticos, los modelos actuales tienen limitaciones significativas. Destacan que la verificación formal sigue siendo el árbitro último de la corrección, ya que los modelos de recompensa imperfectos conllevan riesgos de sobreconfianza. La evaluación se publica públicamente para fomentar más investigación sobre modelos de recompensa para las matemáticas formales.

El artículo concluye señalando limitaciones, incluida la dependencia de la verificación automática para la mayoría de los ejemplos, el enfoque exclusivo en Lean 4 y la exclusión de la evaluación a nivel de proceso o paso a paso. Se sugiere que el trabajo futuro se centre en enfoques híbridos que combinen modelos de recompensa aprendidos con verificación formal y en extender la evaluación a otros asistentes de demostración como Coq e Isabelle.