Resumen Técnico: Mismas Fórmulas, Diferente Semántica

Planteamiento del Problema

El artículo aborda una brecha crítica en la evaluación de las capacidades de razonamiento de los Modelos de Lenguaje Extensos (LLM) con respecto a la lógica modal. Mientras que los benchmarks existentes (por ejemplo, ProofWriter, FOLIO, LogicNLI) evalúan la deducción bajo una lógica de fondo fija e implícita, no logran probar si los modelos pueden adaptar su razonamiento a especificaciones semánticas explícitamente declaradas. En la lógica modal, la validez de una inferencia a menudo depende de propiedades de marco específicas (por ejemplo, reflexividad, transitividad, simetría) o condiciones de dominio (por ejemplo, dominios constantes frente a variables). Un modelo puede desempeñarse bien aprendiendo un régimen de inferencia dominante (una lógica "familiar" como S5) en lugar de adherirse a las restricciones específicas proporcionadas en el prompt. El problema central es determinar si los LLM pueden suprimir sus intuiciones lógicas por defecto para seguir las condiciones semánticas estipuladas, las cuales pueden ser no estándar.

Metodología

Los autores construyen un benchmark de diagnóstico diseñado para aislar el control semántico del reconocimiento de patrones de fórmulas.

1. Construcción del Benchmark:

• Problemas Pareados: El conjunto de datos central consiste en pares de problemas donde las premisas ($P$) y la conjetura ($C$) son idénticas, pero la especificación semántica ($S$) difiere exactamente en una condición (por ejemplo, cambiar un marco reflexivo por uno transitivo, o un dominio acumulativo por uno decreciente).
• Verificación por Oráculo: Un oráculo de razonamiento automatizado (usando Vampire y Leo-III a través de la cadena de herramientas de incrustación LET) verifica que las dos especificaciones produzcan valores de verdad opuestos ($y_a \neq y_b$) para la misma fórmula.
• Núcleo Balanceado: Para evitar que los modelos exploten un atajo de "solo condición" (donde la respuesta se determina únicamente por la etiqueta semántica sin leer la fórmula), los autores crearon un "núcleo no anidado balanceado" de 160 pares. En este subconjunto, cada condición semántica aparece con la misma frecuencia con etiquetas tanto Verdadero como Falso. El éxito aquí requiere estrictamente leer la fórmula para determinar qué condición la valida.
• Alcance: El conjunto de datos cubre cinco contrastes de propiedades de marco (K–D, K–T, T–B, T–S4, B–S5) y tres contrastes de dominio (variable–acumulativo, variable–decreciente, acumulativo–constante), totalizando 800 pares de sistemas anidados y 160 pares de núcleo balanceado.
• Prompting: Los prompts utilizan inglés controlado para declarar reglas explícitamente (por ejemplo, "La relación de accesibilidad es reflexiva y simétrica") sin usar nombres de sistemas convencionales (como "S4"), obligando al modelo a confiar en las reglas proporcionadas.

2. Protocolo Experimental:

• Modelos: El estudio evalúa cinco modelos recientes: DeepSeek V4 (Flash y Pro), GPT-5.6 (Luna y Terra) y Claude Sonnet 5.
• Condiciones:
  • Prompting Directo: Inferencia estándar sin modo de razonamiento.
  • Modo de Razonamiento: Habilitado para modelos específicos (por ejemplo, DeepSeek Flash "alto esfuerzo") para probar si un aumento en la computación en el tiempo de inferencia ayuda a la adherencia semántica.
  • Sensibilidad de Representación: Un subconjunto prueba el rendimiento a través de condiciones en inglés con nombre, definiciones relacionales y sintaxis formal TPTP.
  • Afinidad Semántica: Los experimentos omiten las especificaciones de marco para identificar qué lógica "por defecto" favorecen los modelos cuando no están restringidos.

Resultados Clave

1. Fallo del Control Semántico bajo Prompting Directo:
En el núcleo balanceado, cuatro de los cinco modelos se desempeñaron significamente por debajo de la línea base del 50% de "solo condición" (que asume que el modelo ignora la fórmula y adivina basándose en la etiqueta de la condición).

• DeepSeek V4 Flash: 4.4% de precisión de pares estrictos.
• DeepSeek V4 Pro: 2.5%.
• GPT-5.6 Luna: 21.2%.
• GPT-5.6 Terra: 25.0%.
• Claude Sonnet 5: 65.0% (el único modelo que superó la línea base).
  Esto indica que la mayoría de los modelos fallan al rastrear la semántica declarada, aplicando en su lugar una lógica familiar y fija independientemente de las restricciones del prompt.

2. El Modo de Razonamiento como Mecanismo Restaurador:
Habilitar el modo de razonamiento mejoró drásticamente el rendimiento de DeepSeek V4 Flash, elevando su precisión en el núcleo balanceado del 4.4% al 88.1%. Se observaron mejoras similares para GPT-5.6 Luna en problemas de marcos. Esto sugiere que el fallo no es necesariamente una falta de conocimiento lógico, sino un fallo en la activación del modo de inferencia correcto para procesar las restricciones específicas.

3. Afinidad Semántica y Valores por Defecto:
Cuando se omitieron las especificaciones, los modelos exhibieron afinidades coherentes con lógicas familiares (por ejemplo, DeepSeek Flash favoreció K, mientras que Sonnet favoreció K, y otros favorecieron T). Sin embargo, estos valores por defecto no predijeron de manera fiable los errores cuando las restricciones eran explícitas; los modelos a menudo coincidían en problemas subespecificados pero fallaban al ajustar las restricciones cuando estas se añadían.

4. Sensibilidad de Representación:
Cambiar el formato de entrada (de condiciones con nombre a definiciones relacionales y TPTP) alteró los rankings de rendimiento, pero no restauró consistentemente el control semántico. Por ejemplo, la precisión de GPT-5.6 Terra cayó del 38% (con nombre) al 6% (con definiciones relacionales), lo que indica que el formato superficial no es una solución simple para el problema subyacente de la adherencia semántica.

Contribuciones Clave

• Benchmark de Diagnóstico: Introducción de un marco de evaluación controlado que mantiene fijo el problema del objeto mientras varía la especificación semántica, diseñado específicamente para probar la "sensibilidad a la especificación".
• Núcleo Balanceado: Un diseño de conjunto de datos novedoso que elimina la posibilidad de resolver problemas mapeando condiciones semánticas a respuestas sin leer la fórmula lógica.
• Evidencia Empírica de Dependencia de Modo: Demostración de que la capacidad de seguir la semántica modal es altamente dependiente del modo de inferencia (directo vs. razonamiento), desafiando la noción de capacidades de razonamiento lógico estáticas en los LLM.
• Liberación de Recursos: Lanzamiento público de las fórmulas, artefactos del oráculo, contramodelos y respuestas de los modelos.

Significado y Reivindicaciones

El artículo argumenta que los benchmarks de semántica fija pueden sobreestimar la robustez del razonamiento de los LLM. El hallazgo principal es que el conocimiento modal (conocer la lógica) es distinto del control semántico (aplicar la lógica específica dada). Un modelo puede poseer las reglas lógicas necesarias pero fallar al permitir que una especificación local gobierne su respuesta, recurriendo en su lugar a un régimen de inferencia familiar.

Los autores reivindican modestamente que su trabajo separa estas dos capacidades. Señalan que, si bien el modo de razonamiento puede restaurar la sensibilidad a las intervenciones semánticas, no garantiza la corrección de los pasos de derivación intermedios (por ejemplo, un modelo podría cambiar correctamente de lógica pero aun así derivar una conclusión falsa debido a un error de razonamiento). El estudio concluye que las evaluaciones futuras deben probar explícitamente si los modelos pueden adaptarse a las restricciones declaradas en lugar de depender de supuestos de fondo fijos. El artículo no propone nuevas aplicaciones ni cambios arquitectónicos futuros, centrándose estrictamente en la evaluación diagnóstica de los modelos actuales.