Resumen Técnico: Formalizar una vez, editar el resto (BASE)

1. Planteamiento del problema

A medida que los Modelos de Lenguaje de Gran Escala (LLMs) se aplican cada vez más al razonamiento matemático, suelen generar múltiples rutas de razonamiento distintas y respuestas candidatas para un solo problema. Un desafío crítico surge en la selección de respuestas: cómo verificar qué candidato es correcto sin tener acceso a etiquetas de verdad de referencia (ground-truth) durante el escalado en tiempo de prueba.

Aunque los enfoques existentes, como el voto por mayoría o los modelos de recompensa aprendidos, ofrecen señales estadísticas, carecen de garantías formales. Trabajos recientes han aprovechado los asistentes de pruebas formales (específicamente Lean 4) para verificar candidatos. En este paradigma, un "autoformalizador" traduce un problema y una respuesta candidata en una sentencia de teorema de Lean que afirma la corrección de la respuesta. Un probador (prover) intenta entonces verificar dicha sentencia.

Sin embargo, existe un cuello de botella significativo: para verificar $K$ respuestas candidatas, el autoformalizador debe invocarse $K$ veces de forma independiente. Esto incurre en un costo computacional de $\Theta(K)$, que escala linealmente con el número de muestras. Los autores observan que, para un solo problema, las $K$ sentencias formales son casi idénticas, compartiendo la misma estructura de problema y diferenciándose únicamente en la expresión de la respuesta. El problema central es cómo explotar esta estructura compartida para reducir los costos de formalización de $\Theta(K)$ a $\Theta(1)$ sin sacrificar la precisión de la selección.

2. Metodología: El flujo de trabajo BASE

Los autores proponen BASE (Base-and-Substitute-Edit), un flujo de trabajo diseñado para formalizar un único candidato "base" y derivar las $K-1$ sentencias restantes mediante la edición localizada.

2.1 Descubrimiento de la base

El flujo de trabajo comienza con un resolvedor (solver) ascendente que genera una lista clasificada de $K$ respuestas candidatas, $S(x) = (a_1, \dots, a_K)$, ordenadas por la confianza del solver.

• El sistema itera a través de los candidatos en orden de clasificación.
• Para cada candidato $a_i$, intenta formalizar el par problema-respuesta $(x, a_i)$ en una sentencia de Lean $F_i$.
• El proceso se detiene en el primer candidato $a_b$ cuya formalización $F_b$ se verifica tipológicamente (type-checks) con éxito en Lean.
• $F_b$ se convierte en la formalización base, y $a_b$ es la respuesta base.
• Si ningún candidato se verifica tipológicamente, el sistema recurre al candidato de mayor rango $a_1$.

2.2 Cascada de sustitución

Una vez establecida una base válida $F_b$, el sistema genera las $K-1$ sentencias restantes editando $F_b$ in situ para reflejar los otros candidatos. Esto se maneja mediante una cascada de dos niveles:

1. Nivel 1 (R1): Localización directa basada en reglas

   • El sistema intenta localizar la expresión de la respuesta en $F_b$ mediante una coincidencia exacta de cadenas dentro de una "región de control" (el cuerpo del teorema, excluyendo comentarios/encabezados).
   • Si se encuentra una coincidencia única, el sistema realiza una sustitución directa de la cadena de la respuesta.
   • Si ocurren múltiples coincidencias, un modelo de desambiguación pequeño selecciona el espacio (slot) correcto.
   • Este nivel es eficiente pero falla cuando el autoformalizador codifica la respuesta en una forma sintácticamente diversa (por ejemplo, una tupla (3, 5) codificada como enlaces separados o un valor Prod) en lugar de una cadena literal.

2. Nivel 2 (R2): LEANSCRIBE (Reescritor aprendido)

   • Para los casos donde R1 falla, el sistema invoca a LEANSCRIBE, un LLM especializado y ajustado (fine-tuned).
   • Entrada: El problema $x$, la formalización base $F_b$ y la respuesta base $a_b$.
   • Salida:
     • Un bloque local $s$: Un segmento contiguo de $F_b$ que contiene la expresión dependiente de la respuesta.
     • Una función de llenado $f$: Una función ligera de Python que mapea cualquier respuesta informal $a_i$ al correspondiente bloque de expresión de Lean que reemplaza a $s$.
   • Ejecución: LEANSCRIBE se ejecuta una vez por problema. La función generada $f$ se aplica luego a todos los candidatos restantes $a_i$ para producir sus sentencias formales $F_i = f(a_i)$. Esto amortiza el costo de la llamada al modelo a través de todos los $K-1$ candidatos.

2.3 Verificación y selección

El flujo de trabajo depende de la verificación de tipos de la sentencia (statement-level type-checking) como la señal de selección principal.

• Un candidato se considera "verificado" si su sentencia formal $F_i$ se verifica tipológicamente en Lean (es decir, es una proposición bien formada).
• El sistema selecciona el candidato de mayor rango $a_j$ tal que su $F_j$ se verifique tipológicamente.
• Si ningún candidato se verifica tipológicamente, recurre al primer candidato $a_1$.
• Los autores señalan que, aunque la verificación a nivel de prueba (ejecutar un probador) es más rigurosa, los probadores actuales tienen tasas de pass@1 bajas, lo que hace que la verificación de tipos a nivel de sentencia sea una señal más práctica para la selección en este entorno de presupuesto limitado.

3. Contribuciones clave

1. Flujo de trabajo BASE: El primer trabajo que amortiza los costos de formalización compartiendo una única sentencia base verificada entre múltiples candidatos, reduciendo las llamadas al autoformalizador de $\Theta(K)$ a $\Theta(1)$.
2. Modelo LEANSCRIBE: Un reescritor aprendido entrenado para localizar bloques dependientes de la respuesta y generar funciones de edición reutilizables, manejando variaciones sintácticas que la sustitución basada en reglas no puede resolver.
3. Mejora de Pareto: El método logra una mayor precisión de selección mientras reduce significativamente el costo computacional en todas las configuraciones probadas.

4. Resultados experimentales

Los autores evaluaron BASE en cuatro bancos de pruebas (MATH-500, OlympiadBench, AMC-AIMO, AIME 2024) utilizando tres solvers ascendentes distintos (Gemini 3 Pro, Qwen3-8B, DeepSeek-R1-Qwen3-8B) con $K=8$ candidatos.

• Precisión: BASE mejoró la precisión de selección (Acc) en las 12 configuraciones (conjunto de datos, solver) en comparación con la formalización independiente, con ganancias que oscilaron entre +0.7 y +23.3 puntos porcentuales.
• Robustez: La tasa de "Paso de Respuesta de Oro" (GT-pass) —la fracción de problemas donde la sentencia de la respuesta correcta se verifica tipológicamente— aumentó significativamente (hasta +33.3 puntos), alcanzando el 96–100% en muchos casos. Esto indica que compartir una base verificada hace que la formalización de la respuesta correcta sea más robusta.
• Eficiencia de Costo: Con $K=8$, BASE redujo el número de llamadas al autoformalizador aproximadamente 5.4× (reducción media de 4.7–6.5×). El costo escala como $\Theta(1)$ en lugar de $\Theta(K)$.
• Ablación: Eliminar el reescritor aprendido (LEANSCRIBE) y depender únicamente de la sustitución basada en reglas (R1) resultó en una caída significativa en la cobertura de candidatos (8–22 puntos porcentuales), demostando la necesidad del componente aprendido para manejar diversas codificaciones sintácticas.
• Análisis a nivel de prueba: Incluso cuando se utiliza un probador (DeepSeek-Prover-V2) con un único intento por candidato, BASE mejoró la precisión a nivel de prueba en 11 de las 12 configuraciones, sugiriendo que las sentencias formales mejor estructuradas ayudan a los probadores posteriores.

5. Significado y afirmaciones

El artículo afirma que BASE representa una mejora de Pareto para la selección de respuestas basada en Lean. Al formalizar una vez y editar el resto, el método simultáneamente:

• Reduce el Costo: Disminuye drásticamente el costo de inferencia de la verificación formal, haciendo que el escalado en tiempo de prueba con un $K$ grande sea más factible.
• Mejora la Precisión: Mejora la fiabilidad de la selección de la respuesta correcta, debido probablemente a que la estructura base compartida reduce la varianza y la tasa de fallo del autoformalizador para el candidato correcto.

Los autores enfatizan que este enfoque es un "reemplazo directo" (drop-in replacement) para la etapa de formalización en los flujos de trabajo existentes (demostrado mediante su integración en el flujo FANS) y que las ganancias son impulsadas por la capacidad del verificador para retener las respuestas correctas de manera más efectiva cuando se utiliza un andamiaje compartido y verificado, en lugar de cambios en la generación del solver ascendente.

El trabajo reconoce limitaciones, señalando que se centra en la verificación de tipos a nivel de sentencia debido a las limitaciones actuales de los probadores y asume que las respuestas candidatas comparten una estructura del lado del problema. No pretende resolver la fidelidad de la autoformalización (donde una respuesta incorrecta aún podría verificarse tipológicamente), sino que sugiere que combinar señales formales con clasificaciones del solver mitiga este riesgo.