Resumen Técnico: Lean como Juez Controlado por Riesgo para el Razonamiento Matemático en Lenguaje Natural

1. Declaración del Problema

El artículo aborda el desafío de utilizar asistentes de prueba formales (específicamente Lean) como jueces para el razonamiento matemático en lenguaje natural generado por Modelos de Lenguaje Grandes (LLMs). Si bien una prueba Lean exitosa proporciona una fuerte evidencia positiva para una afirmación formal, la ausencia de una prueba es una señal ambigua. Una prueba fallida puede indicar una respuesta matemáticamente incorrecta, pero también puede resultar de una formalización mal tipada, hechos de biblioteca faltantes o tiempos de espera agotados en la búsqueda de pruebas.

Los enfoques actuales a menudo tratan el fallo de la prueba como una señal negativa de corrección, arriesgando la confusión entre la incorrectitud matemática y la falta de cobertura formal. Los autores identifican un "acantilado de cobertura": la fiabilidad de la selección formal depende agudamente de la proporción de respuestas candidatas que pueden ser formalizadas y probadas con éxito. Cuando la cobertura es alta, la selección formal es altamente precisa; cuando la cobertura es baja, la señal se vuelve poco fiable.

El problema central es determinar cuándo un sistema aguas abajo debe confiar en una señal formal Lean y cuándo debe tratar la señal como fuera de cobertura (es decir, no resuelta) en lugar de incorrecta, mientras proporciona una garantía de riesgo de muestra finita para las respuestas aceptadas.

2. Metodología: COVCAL

Los autores proponen COVCAL (Lean Calibrado por Cobertura), un envoltorio selectivo controlado por riesgo que decide si aceptar una respuesta formal o abstenerse basándose en diagnósticos de cobertura.

2.1 Marco de Observación Parcial

El sistema trata la tubería formal como un mecanismo de observación parcial. No observa la verdad de cada respuesta candidata, sino que solo observa:

1. Qué clases de respuestas normalizadas alcanzan una afirmación Lean bien formada (Cobertura Tipada).
2. Qué clases de esas son probadas con éxito (Cobertura Probada).
3. El peso de la clase probada de mayor peso frente al rival no resuelto de mayor peso (Margen Formal).

Una clase de respuesta se define como un grupo de cadenas candidatas que denotan la misma respuesta final (por ejemplo, $1/2$, $0.5$, $2/4$). Las clases que no se formalizan o no se prueban se consideran no resueltas, no automáticamente incorrectas.

2.2 Diagnósticos de Cobertura

COVCAL calcula cuatro métricas clave para un problema dado $x$:

• Cobertura Tipada ($C_{typ}$): El peso total de las clases candidatas que alcanzaron una afirmación Lean bien formada (estado: proved, typechecked o timeout).
• Cobertura Probada ($C_{prf}$): El peso total de las clases candidatas que recibieron una prueba verificada por el núcleo.
• Masa de Rival No Resuelto ($R_{unres}$): El peso de la clase de respuesta de mayor peso que no fue probada.
• Margen Formal ($M$): La diferencia entre el peso de la clase probada de mayor peso y la masa del rival no resuelto.

2.3 Selección y Certificación

COVCAL acepta la clase probada de mayor peso solo si se cumple una regla predeclarada basada en umbrales $(\tau_{typ}, \tau_{prf}, \tau_M)$. Si no se cumple la regla, el sistema se abstiene (o recurre a un método no formal como la auto-consistencia).

Para garantizar la fiabilidad, COVCAL emplea certificación de riesgo selectivo de muestra finita. Garantiza que, con probabilidad $1-\delta$, el riesgo selectivo (tasa de error) de las respuestas aceptadas sea como máximo $\epsilon$. Se proponen dos regímenes de certificación:

1. Régimen de Bonferroni: Busca sobre una cuadrícula de umbrales en una partición de calibración y aplica una corrección de unión ($\delta/|T|$) para tener en cuenta las comparaciones múltiples. Esto es conservador y requiere una alta densidad de señal para ser factible.
2. Régimen Dev-then-Cal: Selecciona el umbral en una partición de desarrollo independiente y lo certifica una vez en la partición de calibración utilizando un único límite de Clopper-Pearson ($\delta$). Esto es más eficiente en muestras, pero requiere una separación estricta entre los datos de desarrollo y los de calibración.

2.4 Límites Teóricos

El artículo demuestra que, sin diagnósticos de cobertura (es decir, confiando únicamente en la existencia de una prueba), no se puede derivar ningún certificado de corrección puntual no vacío si existe una clase rival no resuelta e inequivalente. La falta de evidencia formal no es evidencia de falsedad matemática; es evidencia de un estado no resuelto.

3. Contribuciones Clave

1. Caracterización del Acantilado de Cobertura: En el conjunto de datos MATH-500, los autores demuestran que la respuesta "ganadora por prueba" es correcta el 96% de las veces con alta cobertura probada, pero solo el 20% con baja cobertura. Esto establece que las pruebas Lean son fiables solo cuando la cobertura y el margen son altos.
2. Especificidad y Fidelidad de la Señal: La señal formal es escasa e imperfecta. Un auto-formalizador de 7B prueba una clase para solo el 28% de los problemas. Además, una auditoría manual revela que solo $\approx 43\%$ de estas pruebas son fieles al problema original (el resto son identidades triviales o afirmaciones verdaderas pero irrelevantes).
3. Método COVCAL: Un marco de predicción selectiva que certifica el riesgo bajo observación parcial. Maneja explícitamente la asimetría del fallo de la prueba y proporciona garantías de muestra finita para las predicciones aceptadas.
4. Factibilidad Dependiente del Formalizador: El artículo demuestra que la factibilidad del certificado está gobernada por la cobertura de la auto-formalización. Un formalizador de 7B genera una señal demasiado escasa para el régimen conservador de Bonferroni (rechazando todas las 20 particiones de bootstrap), mientras que un formalizador especializado en demostradores (Goedel-Prover-V2-8B) que logra un 79% de cobertura hace que el método sea factible en 17/20 particiones.

4. Resultados Experimentales

Los experimentos se realizaron en un subconjunto filtrado de MATH-500 (378 ejemplos) utilizando Qwen2.5-Math-7B para la generación y varios formalizadores para la auto-formalización.

• Rendimiento de Línea Base: La auto-consistencia por sí sola alcanza un 91% de precisión sin abstención.
• Rendimiento de COVCAL:
  • Bajo el régimen de Bonferroni con un formalizador de 7B, el método rechaza todas las entradas (0/20 particiones) porque la señal es demasiado escasa para satisfacer el límite de unión estricto.
  • Bajo el régimen dev-then-cal con el formalizador de 7B, se certifican 12/20 particiones. La fracción aceptada es $\approx 21\%$, con una precisión aceptada de 0.93.
  • Con el Goedel-Prover-V2-8B (formalizador especializado), la cobertura probada aumenta al 79%. Bonferroni se vuelve factible en 17/20 particiones, aceptando $\approx 48\%$ de los problemas con una precisión aceptada de 0.98.
• Auditoría de Fidelidad: Una auditoría manual de 45 ejemplos estratificados mostró que, aunque el 73.6% de las afirmaciones probadas eran no triviales y correctas, solo el 43% eran fieles a la declaración del problema. Muchas afirmaciones "probadas" eran hechos secundarios verdaderos o identidades triviales que no capturaban las restricciones del problema.

5. Significado y Afirmaciones

El artículo afirma que su contribución principal es un cuento preciso de cuándo y con qué formalizador se puede confiar en una señal formal parcial bajo control de riesgo, en lugar de simplemente mejorar la precisión bruta.

• Control de Riesgo sobre Precisión Bruta: Dado que la auto-consistencia ya es 91% precisa, el valor de COVCAL radica en su capacidad para proporcionar un certificado para el subconjunto de respuestas que acepta, distinguiendo entre "verificado" y "no resuelto" en lugar de "correcto" e "incorrecto".
• Manejo de Observaciones Parciales: El trabajo reformula la verificación formal como un problema de predicción selectiva donde las pruebas faltantes se tratan como candidatos no resueltos, evitando la etiquetación errónea de razonamientos correctos como incorrectos debido a fallos de formalización.
• Dependencia de la Especialización: Los resultados destacan que la escala bruta del modelo no es un sustituto de la especialización. Un formalizador especializado en demostradores supera significativamente a un modelo generalista más grande en términos de cobertura de demostración, que es la restricción vinculante para el control de riesgo certificable.

Los autores concluyen que COVCAL sirve como una interfaz conservadora para usar Lean como juez: es factible e informativa solo cuando el auto-formalizador cubre suficiente masa de respuesta para soportar un certificado de riesgo, pero no garantiza que todas las respuestas estén verificadas.