When Many Answers Are Valid, Voting Fails: Symbolic Verification for Best-of-K Causal Reasoning in LLMs

Resumen Técnico: Cuando muchas respuestas son válidas, la votación falla

Planteamiento del problema
Los métodos actuales de escalado en tiempo de inferencia para Modelos de Lenguaje Grande (LLM), como la Autoconsistencia (Self-Consistency), se basan en el supuesto de que la respuesta más frecuente entre los rastreos de razonamiento muestreados es la más fiable. Este enfoque falla en tareas de razonamiento causal donde múltiples salidas distintas pueden ser completamente correctas (por ejemplo, diferentes conjuntos de ajuste válidos que satisfacen el criterio de backdoor de Pearl). En estos escenarios de "muchos satisfactores", la masa de probabilidad válida se fragmenta a través de múltiples cadenas de respuesta, mientras que una única respuesta inválida puede dominar la votación simplemente por ser el error más común. En consecuencia, la votación de pluralidad exacta puede seleccionar una respuesta inválida incluso cuando la mayoría de los rastreos muestreados contienen un razonamiento válido, lo que conduce a selecciones inconsistentes e incorrectas.

Metodología: CALVER
Los autores presentan CALVER (Causal Axiom-Level VERification), un verificador simbólico libre de entrenamiento, diseñado para seleccionar el mejor candidato de un conjunto de $K$ rastreos muestreados sin consultar una respuesta de referencia.

• Contrato de rastro (Trace Contract): CALVER requiere que los modelos generen el razonamiento en un esquema tipado de seis ranuras: (1) Grafo, (2) Consulta, (3) Estrategia, (4) Registro de derivación, (5) Resultado computado y (6) Respuesta.
• Verificación simbólica: En lugar de agregar las frecuencias de las respuestas, CALVER califica cada rastro de forma determinista frente a una especificación causal ejecutable. El verificador realiza seis comprobaciones:
  1. Análisis del grafo (Graph Parsing): Valida la estructura del grafo (DAG o ADMG).
  2. Vinculación de la consulta (Query Binding): Asegura que las variables de la consulta coincidan con el problema.
  3. Validez de la estrategia: Comprueba si el conjunto propuesto satisface los criterios gráficos (por ejemplo, d-separación, m-separación, ajuste de backdoor, alcanzabilidad de intervención).
  4. Registro de derivación: Verifica la sintaxis y la procedencia de los pasos de razonamiento.
  5. Resultado computado: Recomputa de forma independiente el funcional (por ejemplo, el Efecto de Tratamiento Promedio o ATE) para asegurar la consistencia numérica.
  6. Consistencia de la respuesta: Confirma que la respuesta final se alinea con el resultado computado.
• Regla de selección: El selector elige el rastro con la puntuación más alta (puntuación máxima desplegada de 6). Los empates se resuelven seleccionando el rastro más temprano.
• Modos: CALVER opera en dos modos:
  • Grafo suministrado (Supplied-Graph): El grafo de origen se proporciona; los rastreos se califican frente a este.
  • Grafo construido (Constructed-Graph): El modelo debe extraer un grafo a partir de un texto; el rastro se califica frente a su propio grafo reconstruido, mientras que la calificación final utiliza el grafo fuente oculto.

Contribuciones clave

1. Formulación: El artículo formula la selección de "el mejor de $K$" bajo multiplicidad de respuestas como una agregación sobre una clase de validez decidible. CALVER instancia esto con una puntuación de rastro de seis componentes dependiente del grafo para DAGs y ADMGs.
2. Teoría:
   • Solidez del certificado de ATE estricto: Los autores demuestran que un rastro de puntuación máxima que satisface guardas específicas (exclusión de tratamiento y margen de decisión) garantiza una decisión de umbral correcta para consultas de Efecto de Tratamiento Promedio (ATE).
   • Teorema de fragmentación de validez: Demuestran que la pluralidad exacta puede volverse inconsistente cuando la masa de probabilidad válida se divide entre múltiples respuestas válidas, permitiendo que una respuesta inválida con una masa individual ligeramente superior gane.
3. Experimentos: Evaluación extensiva a través de múltiples familias de modelos (Qwen, Mistral), familias de grafos (CLEAR, bnlearn) y configuraciones (grafos suministrados, construcción de texto a grafo, acertijos lógicos).

Resultados

• Superioridad sobre las líneas base: En el benchmark CLEAR clean-core (126 problemas con múltiples respuestas válidas), CALVER alcanza un 42.1% de precisión, superando significativamente a la pluralidad exacta (~30.9%), a un centroide consciente del conjunto (set-aware medoid), a la confianza del modelo y a un modelo de recompensa aprendido (Skywork Reward V2) y a un juez de LLM (incluso escalado a 7B parámetros).
• Escalado con $K$: La brecha de rendimiento entre CALVER y la pluralidad se amplía a medida que aumenta el presupuesto de muestreo ($K$). Mientras que el rendimiento de la pluralidad se estanca, CALVER continúa mejorando, alcanzando un 57.9% con $K=32$.
• Robustez ante la recuperación de grafos: En configuraciones de texto a grafo donde la recuperación exacta del grafo es baja (por ejemplo, 34% en niveles narrativos naturalistas), CALVER sigue superando a la pluralidad por 17.6 puntos porcentuales. Esto demuestra que la verificación por candidato puede tener éxito incluso cuando la estructura global del grafo se reconstruye imperfectamente, siempre que se preserven las relaciones locales de la consulta.
• Generalización: El método se transfiere a benchmarks independientes (bnlearn, CausalGraph2LLM), diferentes familias de modelos y dominios no causales (acertijos lógicos de Knights and Knaves) cuando se adapta el predicado de verificación (por ejemplo, consistencia de tabla de verdad).
• Eficiencia: La verificación simbólica añade un overhead mínimo (~7% sobre el costo de generación), calificando cada rastro en 1–8 ms en un solo hilo de CPU.

Significancia y afirmaciones
El artículo afirma que CALVER proporciona una señal de selección más fuerte que la frecuencia superficial o los modelos de preferencia aprendidos en regímenes donde existen múltiples respuestas válidas. Establece que:

• La votación falla: La pluralidad exacta es fundamentalmente defectuosa para el razonamiento causal cuando las respuestas válidas fragmentan el voto.
• Validez ejecutable: La agregación basada en la satisfacción de una clase de validez definida por la tarea (mediante verificación simbólica) es más fiable que la agregación basada en la frecuencia de la cadena de la respuesta.
• Régimen delimitado: El método es más efectivo en el "régimen intermedio" donde muchas respuestas son válidas y ninguna extracción es dependiente. Cuando las respuestas son casi únicas, la votación estándar es suficiente; cuando la extracción de texto a grafo es altamente fiable, extraer un grafo y resolver directamente es superior.
• Independencia: El mecanismo de selección se basa en predicados ejecutables (axiomas causales o reglas lógicas) en lugar de heurísticas aprendidas, lo que lo hace robusto ante diferentes arquitecturas de modelos y objetivos de entrenamiento.

Los autores enfatizan que CALVER no pretende determinar la verdad científica sobre grafos causales del mundo real, sino seleccionar el rastro de razonamiento formalmente más válido dado la estructura o el texto proporcionado. La ventaja del método está estrictamente ligada a la capacidad de ejecutar una comprobación de validez sobre el candidato.