Resumen Técnico: FormInv: Un Protocolo de Medición para la Invarianza Semántica en Puntos de Referencia de Razonamiento Matemático

1. Declaración del Problema

Los puntos de referencia actuales para el razonamiento matemático en Modelos de Lenguaje Grandes (LLM) dependen en gran medida de métricas de precisión agregada calculadas sobre formulaciones canónicas de problemas. Este artículo argumenta que dichas métricas son insuficientes porque asumen que el rendimiento del modelo es independiente de cómo se formula una pregunta. Los autores identifican una "brecha de medición" crítica: los modelos a menudo exhiben una alta precisión en puntos de referencia estándar, pero no logran mantener la invarianza semántica—la capacidad de producir respuestas consistentes a través de parafraseos lógicamente equivalentes.

El artículo destaca que los puntos de referencia estándar (por ejemplo, GSM8K, MATH, MathCheck) carecen de una verificación rigurosa de la equivalencia semántica de los parafraseos. En consecuencia, las clasificaciones de los puntos de referencia pueden ser artefactos de formulaciones específicas en lugar de medidas verdaderas de la capacidad de razonamiento. Los autores se basan en la teoría psicométrica, específicamente en el Funcionamiento Diferencial de los Ítems (DIF) y la Teoría de la Generalizabilidad, para formalizar este problema. Plantean que si la respuesta de un modelo cambia basándose en reexpresiones semánticamente equivalentes, esto indica un fallo en la comprensión matemática genuina, dependiendo en cambio del reconocimiento de patrones superficiales.

2. Metodología

2.1 El Protocolo FormInv

Los autores proponen FormInv, un protocolo de medición diseñado para auditar y cuantificar la invarianza semántica. El protocolo consta de tres componentes principales:

1. La Brecha de Invarianza (IG) y la Tasa de Consistencia Semántica (SCR):

   • IG: Definida formalmente como la desviación estándar de las respuestas binarias de un modelo a través de una clase de equivalencia de parafraseos. Matemáticamente, $IG(f, [x]_\sim) = \sqrt{p(1-p)}$, donde $p$ es la probabilidad de una respuesta correcta dentro de la clase de equivalencia. Una IG de 0 implica invarianza perfecta.
   • SCR: La proporción de teoremas para los cuales el modelo responde correctamente a través de todas las formas de parafraseo. A diferencia de la IG, que mide la varianza, la SCR mide la intersección de la corrección y la invarianza.
   • Q de Cochran: Utilizado como prueba estadística de homogeneidad marginal a través de $k > 2$ familias de parafraseos para determinar si la tasa de fallo de un modelo varía significativamente por familia.

2. La Taxonomía de Parafraseos de 8 Familias:
   El punto de referencia evalúa a los modelos a través de ocho familias de transformación distintas, categorizadas por su rigor de verificación:

   • T1 (Certificable Formalmente): Familias F4 (notación), F6 (orden), F7 (desempaquetado) y F8 (equivalencia). Estas dependen de reglas Lean4/FOL o de la verificación mediante Sistemas de Álgebra Computacional (CAS) (por ejemplo, SymPy).
   • T2 (Válido Condicionalmente): Familias F1 (sintáctica), F2 (cuantificador) y F3 (voz pasiva). Estas dependen del contexto de tipo y se verifican mediante plantillas o CAS cuando es aplicable.
   • T3 (Heurístico): Familia F5 (variación de conectores). Estas dependen de heurísticas de lenguaje natural y requieren revisión por expertos en el dominio.

3. Auditoría de Unanimidad Cruzada entre Modelos:
   Un novedoso mecanismo de control de calidad donde un parafraseo se marca como semánticamente incorrecto si una supermayoría de modelos (por ejemplo, $\ge 6/9$) falla en el parafraseo mientras aprueba la versión canónica. Esto aprovecha la suposición de que los errores sistemáticos en el propio parafraseo, y no en el razonamiento del modelo, causan un fallo universal.

2.2 Construcción del Punto de Referencia

• Sustrato: La evaluación utiliza 103 teoremas curados de Mathlib4 (verificados en Lean4), abarcando dominios como teoría de números, álgebra y análisis real.
• Conjunto de Datos: El conjunto de datos principal (FormInv v1) contiene 760 elementos (103 teoremas $\times$ ~7.4 parafraseos). Una evaluación extendida "Pista B" utiliza 100 teoremas más difíciles de ntp-mathlib (811 elementos).
• Verificación: Los parafraseos se generan mediante GPT-4o y se verifican mediante un protocolo de múltiples etapas: CAS para familias algebraicas, garantías de plantillas para familias superficiales y revisión 100% por expertos humanos para familias definicionales (F7/F8).

2.3 Configuración Experimental

El estudio evalúa 9 modelos de vanguardia (incluyendo GPT-4o, Claude Sonnet/Haiku, DeepSeek V3/R1, Gemini 2.5 Flash y Llama 3.3 70B) a través de los 366–811 elementos. Los modelos se evalúan en modo cero disparos (zero-shot) con restricciones estrictas de VERDADERO/FALSO.

3. Resultados Clave

3.1 La Brecha de Invarianza frente a la Precisión

El hallazgo más significativo es la desconexión entre la precisión agregada y la consistencia semántica.

• Claude Haiku 4.5 logra un 86% de precisión pero solo un 50% de SCR, lo que significa que la mitad de sus respuestas correctas son inconsistentes a través de los parafraseos.
• DeepSeek V3 logra un 96.4% de precisión y un 82% de SCR.
• Una brecha de 10 puntos en precisión oculta una brecha de 32 puntos en SCR. El artículo señala que la precisión por sí sola es "constitucionalmente ciega" ante este fallo estructural.
• Existe una fuerte correlación negativa ($r = -0.965$) entre la precisión y la IG Media, lo que sugiere que los modelos más precisos son generalmente más invariantes, pero esta correlación está impulsada algebraicamente por la definición de IG y no garantiza la invarianza para familias específicas.

3.2 Inversiones de Clasificación y Complementariedad

Las clasificaciones de los modelos no son estables; se invierten dependiendo de la familia de parafraseo:

• F6 (Orden de Comparación): GPT-4o falla en 0.0% de los elementos, mientras que Claude Sonnet falla en 16.7%.
• F7 (Desempaquetado Definicional): Claude Sonnet falla en ~6%, mientras que GPT-4o falla en 10.0%.
• Este patrón de fallo complementario implica que ningún modelo único domina en el sentido de Pareto a todas las familias. En consecuencia, los diseñadores de puntos de referencia eligen implícitamente una ponderación de familias que determina al ganador. El artículo formaliza esto como el corolario "No-Free-Benchmark": para cualquier clasificación objetivo, existe una ponderación $\lambda$ sobre las familias de parafraseos que la realiza.

3.3 Hallazgos de la Auditoría de Calidad

El protocolo de unanimidad cruzada entre modelos identificó con éxito parafraseos semánticamente incorrectos en puntos de referencia existentes:

• Auditoría de MathCheck: Aplicado a 129 grupos en MathCheck, el protocolo marcó 4 parafraseos semánticamente incorrectos (3.1%). Eliminar estos errores desplazó a GPT-4o del rango 2 al rango 4, elevando a Claude Haiku y DeepSeek V3.
• Auditoría de FormInv v1: El protocolo identificó 11 errores en elementos generados por GPT-4o, incluyendo excesos en bicondicionales, inversiones de voz pasiva y eliminación de contexto de tipo. Estos errores eran invisibles para la evaluación de un solo modelo pero expuestos por la unanimidad.

3.4 Dependencia del Régimen de Dificultad

En la evaluación "Pista B" utilizando teoremas más difíciles:

• La correlación entre precisión e invarianza se debilitó ($r = -0.415$, no significativa).
• La dificultad específica de F5 (variación de conectores) se disolvió; todas las familias se agruparon en tasas de fallo similares (28–35%).
• Los modelos de razonamiento (DeepSeek R1, o4-mini) mostraron la IG más baja en teoremas difíciles, lo que sugiere que la deliberación mediante Cadena de Pensamiento reduce la sensibilidad superficial solo cuando los teoremas exigen razonamiento de alto nivel.

4. Contribuciones

1. Marco de Invarianza: Formaliza SCR e IG como métricas primarias para la invarianza semántica, fundamentadas en el teorema de la esperanza condicional de Doob y la teoría DIF. Clasifica las familias de parafraseos en niveles T1, T2 y T3 basados en el rigor de verificación.
2. Punto de Referencia FormInv: Un conjunto de datos de más de 760 elementos derivados de teoremas verificados en Lean4, evaluado en 9 modelos con una auditoría rigurosa de unanimidad cruzada entre modelos.
3. FormInvSelector: Un algoritmo que utiliza perfiles de SCR por familia para recomendar el modelo con la tasa de fallo esperada más baja para regímenes de tareas específicos (por ejemplo, seleccionar un modelo para razonamiento definicional frente a tareas de comparación).
4. Auditoría de Calidad de Parafraseos: Demuestra que la unanimidad cruzada entre modelos ($\ge 6/9$ modelos fallando un parafraseo) es un método automatizado y de bajo costo para detectar elementos de puntos de referencia semánticamente incorrectos, separando efectivamente los errores del punto de referencia de los errores del modelo.

5. Significado y Afirmaciones

El artículo afirma que FormInv es el primer protocolo que aplica la teoría de la invarianza de medición y métricas fundamentadas en DIF al razonamiento matemático formal. Su significado radica en tres áreas:

• Revelación de Defectos Ocultos: Expone que las métricas de precisión estándar pueden ser engañosas, ocultando una "brecha de 32 puntos" entre el rendimiento superficial y la comprensión semántica genuina.
• Integridad del Punto de Referencia: Proporciona una herramienta para que los creadores de puntos de referencia auditen sus propios conjuntos de datos antes de la publicación, evitando que las clasificaciones sean artefactos de parafraseos defectuosos. Los autores afirman que "si generas parafraseos programáticamente, no sabes cuántos están mal".
• Evaluación Consciente del Régimen: Cuestiona la noción de un único modelo "mejor", demostrando que las clasificaciones dependen del régimen (varían según la familia de parafraseo y la dificultad). El artículo concluye que los diseñadores de puntos de referencia eligen implícitamente a los ganadores seleccionando qué familias incluir, y FormInv hace explícita y auditable esta elección.

Los autores mantienen modestia respecto a las limitaciones, señalando que la certificación a gran escala de todos los parafraseos mediante Lean4 es trabajo futuro, y que el estudio actual se basa en un conjunto curado de 103 teoremas (aunque extendido a 100 más difíciles en la Pista B). Enfatizan que FormInv es una métrica complementaria destinada a aumentar, no a reemplazar, las evaluaciones existentes basadas en precisión.