Resumen Técnico: OProver: Un Marco Unificado para la Prueba Formal de Teoremas Agéntica

Enunciado del Problema

Los avances recientes en la prueba formal de teoremas, particularmente dentro del ecosistema Lean 4, han aprovechado la generación de pruebas a gran escala y el entrenamiento consciente del verificador para mejorar el rendimiento en puntos de referencia como MiniF2F y PutnamBench. Sin embargo, persiste una limitación crítica: las capacidades de prueba agéntica (búsqueda, retroalimentación del compilador y reparación iterativa) suelen tratarse como heurísticas aplicadas en tiempo de inferencia a un probador fijo, en lugar de como políticas aprendidas integradas en el proceso de entrenamiento.

Esto crea una discrepancia entre entrenamiento e inferencia. Los modelos entrenados principalmente con pruebas finalizadas y exitosas encuentran la retroalimentación del compilador y el contexto recuperado solo durante la implementación, en distribuciones para las cuales nunca fueron optimizados. Además, los corpus formales existentes se centran en los productos finales (enunciados y pruebas verificadas), omitiendo los historiales de interacción de múltiples rondas: intentos fallidos, contexto recuperado y diagnósticos del compilador, esenciales para aprender a reparar pruebas. En consecuencia, la señal de supervisión que impulsa la reparación de pruebas en la práctica permanece en gran medida sin explotar en el entrenamiento del modelo.

Metodología

El artículo presenta OProver, un marco unificado que integra la búsqueda, la retroalimentación del compilador y la reparación iterativa directamente en la política del probador mediante una tubería de entrenamiento coevolutivo.

1. El Marco OProver

OProver trata la prueba de teoremas como un bucle de refinamiento acotado y de múltiples rondas. En cada ronda $t$, la política $\pi$ se condiciona sobre un estado compacto $X_t = (s, R_t, p_{t-1}, f_{t-1})$, donde:

• $s$: El enunciado del teorema objetivo.
• $R_t$: Las pruebas recuperadas y verificadas por el compilador de los $k$ mejores resultados desde una memoria $M$.
• $p_{t-1}$: El intento de prueba anterior.
• $f_{t-1}$: La retroalimentación textual cruda del compilador (diagnósticos) desde el verificador Lean 4.

La política genera un intento revisado $p_t$. Si la verificación falla, la retroalimentación cruda se devuelve a la política para la siguiente ronda. Crucialmente, la política se condiciona solo sobre el intento y la retroalimentación más recientes, preservando las señales de corrección locales mientras mantiene el estado compacto.

2. OProofs: Un Corpus de Entrenamiento Unificado

Para apoyar este marco, los autores construyen OProofs, un corpus a gran escala diseñado específicamente para la prueba agéntica. A diferencia de conjuntos de datos anteriores que preservan solo las pruebas finales, OProofs registra trayectorias serializadas que incluyen:

• Contexto recuperado.
• Intentos fallidos.
• Retroalimentación cruda del compilador.
• Reparaciones posteriores.

OProofs se construye a partir de tres fuentes: recursos públicos de Lean, síntesis de pruebas a gran escala (autoformalización + verificación) y trazas de la prueba agéntica del propio OProver. Contiene 1.77M de enunciados Lean únicos y 6.86M de pruebas verificadas por el compilador, emparejadas con 1.07M de trayectorias agénticas.

3. Tubería de Entrenamiento Coevolutivo

El proceso de entrenamiento sigue un bucle iterativo (Algoritmo 1) donde el probador y el corpus coevolucionan:

1. Preentrenamiento Continuo (CPT): Un modelo base se entrena con una mezcla de código Lean, matemáticas y datos de razonamiento de contexto largo para crear OProver-Base.
2. Post-entrenamiento Iterativo:
   • Despliegues Agénticos: La política actual realiza pruebas de múltiples rondas sobre un conjunto de teoremas, recuperando desde la memoria actual $M_k$ y verificando con el compilador Lean.
   • Recopilación de Datos: Las pruebas verificadas recientemente se añaden al corpus y se indexan en la memoria de recuperación. Los intentos fallidos y las reparaciones exitosas se descomponen en ejemplos a nivel de ronda $(s, R_t, p_{t-1}, f_{t-1}) \to p_t$.
   • Ajuste Fino Supervisado (SFT): El modelo se actualiza utilizando los ejemplos de reparación recopilados.
   • Aprendizaje por Refuerzo (RL): Se aplica la Optimización de Políticas de Secuencia de Grupo (GSPO) a casos no resueltos más difíciles, utilizando una señal de recompensa basada en el éxito de la verificación y la corrección del formato.
   • Recirculación: El corpus y la memoria actualizados alimentan la siguiente iteración, permitiendo que la política aprenda de sus propias pruebas mejoradas.

Contribuciones Clave

1. Marco Unificado para la Prueba Agéntica: OProver unifica la búsqueda, la retroalimentación y la reparación iterativa en una única política aprendida, eliminando la discrepancia entre entrenamiento e inferencia al entrenar al modelo para utilizar estas señales como parte de su estrategia central en lugar de como heurísticas externas.
2. Corpus OProofs: La construcción de un corpus a gran escala (1.77M de enunciados, 6.86M de pruebas) que preserva explícitamente los historiales de interacción de múltiples turnos, incluidos intentos fallidos y retroalimentación cruda del compilador, proporcionando una supervisión previamente no disponible en conjuntos de datos formales.
3. Tubería Coevolutiva: Una metodología de entrenamiento donde el probador genera nuevos datos (pruebas verificadas y trayectorias de reparación) que se incorporan inmediatamente al corpus de entrenamiento y a la memoria de recuperación, creando un bucle de auto-mejora.
4. Rendimiento de Vanguardia: OProver logra resultados de primer nivel entre los probadores de pruebas completas de peso abierto, demostrando que las estrategias de refinamiento agéntico pueden superar a modelos significativamente más grandes.

Resultados Experimentales

OProver fue evaluado en cinco puntos de referencia de Lean 4: MiniF2F, MathOlympiadBench, ProofNet, ProverBench y PutnamBench.

• Rendimiento: El modelo OProver-32B logró las mejores puntuaciones Pass@32 en tres puntos de referencia (MiniF2F: 93.3%, ProverBench: 58.2%, PutnamBench: 11.3%) y el segundo mejor en los otros dos (MathOlympiad: 22.8%, ProofNet: 33.2%).
• Eficiencia: OProver-32B (32B parámetros) superó al DeepSeek-Prover-V2 de 671B y al LongCat-Flash-Prover de 560B (con TIR) en la mayoría de los puntos de referencia, a pesar de tener significativamente menos parámetros. Incluso la variante de 8B superó al Goedel-Prover-V2 de 32B en todos los puntos de referencia.
• Escalado en Tiempo de Prueba: El rendimiento mejoró consistentemente con presupuestos de computación aumentados (más muestras o rondas de refinamiento), aunque con rendimientos decrecientes. La asignación óptima entre la profundidad de refinamiento y el ancho de muestreo varió según la dificultad del punto de referencia.
• Estudios de Ablación: Eliminar la retroalimentación del compilador de múltiples turnos causó la degradación de rendimiento más significativa, confirmando el refinamiento iterativo como el principal impulsor de las ganancias. Eliminar la augmentación de búsqueda también causó caídas consistentes, aunque menores, destacando el valor complementario de la fundamentación por búsqueda.

Significado y Afirmaciones

El artículo afirma que OProver demuestra que la prueba formal de teoremas agéntica puede aprenderse eficazmente como una política unificada en lugar de ensamblarse a partir de módulos separados en tiempo de inferencia. Al entrenar sobre la trayectoria completa de la construcción de pruebas, el fallo y la reparación, el modelo aprende a aprovechar la retroalimentación del compilador y el contexto recuperado como partes intrínsecas de su proceso de razonamiento.

Los autores enfatizan que las ganancias de rendimiento no son meramente el resultado de la escala del modelo, sino que surgen de la sinergia entre la fundamentación aumentada por búsqueda y el refinamiento iterativo guiado por el compilador. La coevolución de la política OProver y el corpus OProofs permite que el sistema mejore continuamente sus capacidades de prueba aprendiendo de sus propios intentos exitosos y fallidos, estableciendo un nuevo paradigma para el entrenamiento de sistemas de razonamiento formal.