💻 computer science

MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku

Este artículo propone un marco neurosimbólico que mejora el rendimiento de los modelos de visión y lenguaje en acertijos de Sudoku mediante el uso de un oráculo MaxSAT para validar las asignaciones candidatas y proporcionar retroalimentación estructurada, imponiendo así la consistencia lógica y mejorando la precisión de las soluciones.

Autores originales: Pedro Orvalho, Guillem Alenyà, Felip Manyà

Publicado 2026-07-15

📖 4 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Pedro Orvalho, Guillem Alenyà, Felip Manyà

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que tienes un amigo robot súper inteligente que es increíble para mirar imágenes y adivinar qué hay en ellas. Le muestras una imagen de un rompecabezas de Sudoku (esa cuadrícula de 9x9 donde rellenas números del 1 al 9) y trata de adivinar los números. Este robot es como un Modelo de Lenguaje-Visión (VLM). Es genial "viendo" la cuadrícula y "leyendo" las pistas, pero tiene un punto ciego divertido: no tiene un libro de reglas incorporado. Podría adivinar un número que parece correcto pero que rompe las reglas, como poner dos 5 en la misma fila. Es como un artista talentoso que puede pintar un cielo hermoso pero accidentalmente pinta dos soles en el mismo lugar porque olvidó las leyes de la física.

El artículo presenta una nueva colaboración para solucionar esto. Emparejan al robot artístico con un Oráculo MaxSAT estricto y lógico. Piensa en el Oráculo MaxSAT como un árbitro súper organizado que tiene el libro de reglas oficial del Sudoku. El árbitro no intenta pintar la imagen; en su lugar, observa las suposiciones del robot y las verifica contra las reglas.

Así es como funciona el equipo:

La Suposición: El robot mira la imagen del rompecabezas y sugiere dónde poner los números.
La Verificación: El árbitro toma estas sugerencias. Trata las reglas del Sudoku como "leyes estrictas" (debes seguirlas) y las suposiciones del robot como "sugerencias suaves" (esperamos que sean correctas, pero podemos cambiarlas si rompen las leyes).
La Corrección: Si el robot comete un error, el árbitro no solo dice "¡Mal!". Encuentra el grupo más grande de suposiciones que sí funcionan juntas y le dice al robot: "Mantén estas, pero cambia estas específicas". Luego dibuja una imagen sobre el rompecabezas mostrando exactamente dónde está el conflicto y lo explica con palabras.
El Reintento: El robot mira las notas del árbitro, corrige sus errores e intenta de nuevo.

Los investigadores probaron esto en un montón de rompecabezas de Sudoku, que iban desde fáciles hasta difíciles. Utilizaron tres robots diferentes: dos de código abierto (llamados Molmo2 y Qwen3-VL) y uno muy potente y de código cerrado (GPT-5.5).

¿Qué descubrieron?
Sin el árbitro, los robots a menudo se quedaban atascados o rellenaban números que no tenían sentido. Pero cuando añadieron al árbitro MaxSAT:

Los robots mejoraron mucho en el seguimiento de las reglas.
Resolvieron muchos más rompecabezas. Por ejemplo, el robot GPT-5.5, cuando se le pidió resolver todo el tablero a la vez, pasó de resolver 45 rompecabezas a resolver 73. Su completitud promedio (cuántas celdas acertó) saltó del 72.0% al 80.7%.
Incluso los robots de código abierto mejoraron, aunque no tanto como el grande. Molmo2 pasó de resolver 17 rompecabezas a 28, y Qwen3-VL de 10 a 13.

El artículo sugiere que este trabajo en equipo es especialmente útil cuando el robot está casi en lo cierto pero comete algunos errores lógicos. El árbitro ayuda a limpiar esos errores para lograr una solución perfecta.

¿Qué dice el artículo que esto NO es?
Los autores son muy claros: no están intentando reemplazar al robot con el árbitro. No están diciendo que el árbitro deba resolver el rompecabezas por sí solo (lo cual podría hacer en pocos segundos). El objetivo no es superar la velocidad del árbitro; es ver si el árbitro puede enseñar al robot a ser más confiable. También señalan que los rompecabezas más difíciles (etiquetados como "Dificultad 1") seguían siendo más complicados que los fáciles, pero el árbitro ayudó a los robots a manejarlos mucho mejor que antes.

En resumen, el artículo muestra que darle a una IA visual un "compañero" lógico para que revise su trabajo la convierte en una mucho mejor resolutora de rompecabezas. Es una victoria para el trabajo en equipo, demostando que mezclar un supositor creativo con un verificador de reglas estricto crea un sistema más inteligente que cualquiera de los dos por separado.

Resumen Técnico: Retroalimentación Basada en MaxSAT para Guiar Modelos de Visión-Lenguaje en Sudoku

Planteamiento del Problema
Los Modelos de Visión-Lenguaje (VLM) han demostrado capacidades prometedoras en tareas de razonamiento visual estructurado, incluyendo acertijos basados en cuadrículas como el Sudoku. Sin embargo, a pesar de sus fuertes capacidades perceptivas, los VLM carecen de mecanismos explícitos para imponer la consistencia lógica. Con frecuencia dependen del reconocimiento de patrones en lugar de un razonamiento de restricciones basado en principios, lo que conduce a salidas que violan las restricciones estructurales (por ejemplo, duplicidad de números en filas o columnas) o que exhiben un comportamiento inestable al intentar refinar soluciones incorrectas. Si bien los métodos de Programación de Restricciones (CP) y de Satisfacibilidad (SAT) ofrecen garantías formales de solidez, carecen de la flexibilidad perceptual y de las capacidades de generación de propuestas de los VLM modernos. Este artículo aborda la cuestión de si la optimización de restricciones formales puede guiar a los VLM para resolver acertijos de lógica visual de manera más fiable.

Metodología
Los autores proponen un marco neuro-simbólico híbrido donde un VLM actúa como generador de propuestas y un oráculo de Satisfacibilidad Máxima (MaxSAT) actúa como validador de consistencia y motor de refinamiento. El enfoque opera a través de un bucle de interacción iterativo:

Formulación: El problema de Sudoku se codifica como una instancia de MaxSAT Parcial.
- Cláusulas Duras ( $\Phi_h$ ): Codifican las restricciones fundamentales del Sudoku (cada celda contiene exactamente un dígito; cada dígito aparece exactamente una vez en cada fila, columna y subcuadrícula). Estas son no negociables.
- Cláusulas Blandas ( $\Phi_s$ ): Codifican las asignaciones candidatas propuestas por el VLM como cláusulas unitarias.
Bucle de Interacción:
- El VLM genera asignaciones candidatas (colocando dígitos en celdas) basadas en la imagen del acertijo.
- Estas asignaciones se introducen en el solver de MaxSAT (específicamente el solver RC2 del toolkit PySAT).
- El solver calcula una asignación que satisface todas las cláusulas duras mientras maximiza el número de cláusulas blandas satisfechas (es decir, reteniendo tantas propuestas del VLM como sea posible sin violar las restricciones).
- Generación de Retroalimentación: Si las propuestas del VLM son inconsistentes, el solver de MaxSAT identifica el subconjunto de asignaciones mutuamente consistentes más grande. Las asignaciones rechazadas (aquellas en el conjunto de cláusulas blandas pero no en la solución óptima) se traducen en retroalimentación estructurada, incluyendo descripciones textuales de inconsistencias y anotaciones visuales que resaltan las celdas en conflicto sobre la imagen del acertijo.
- El VLM utiliza esta retroalimentación para generar una propuesta refinada.
Protocolos: El marco evalúa dos modos de interacción:
- Colocación Única Iterativa: El VLM propone un movimiento a la vez. MaxSAT valida; si es consistente, se acepta; de lo contrario, se rechaza con retroalimentación.
- Refinamiento de Tablero Completo: El VLM propone un estado de tablero completo. MaxSAT identifica el subconjunto más grande y consistente del tablero entero, rechazando solo las celdas conflictivas, y devuelve retroalimentación para un refinamiento global.

Contribuciones Clave

Un Marco Neuro-Simbólico: Una arquitectura novedosa para validar y refinar las soluciones de Sudoku generadas por VLM utilizando un oráculo de MaxSAT, estableciendo una clara división del trabajo donde el componente neural maneja la percepción y el componente simbólico impone la consistencia lógica.
Integración de MaxSAT Parcial: La integración de MaxSAT parcial en el bucle de resolución del VLM, tratando las colocaciones generadas por el modelo como restricciones blandas. Esto permite al sistema identificar y reparar el subconjunto mutuamente consistente más grande de una propuesta en lugar de descartar la salida completa.
Evaluación Empírica: Una evaluación exhaustiva en un conjunto de datos de Sudoku con múltiples VLM de código abierto (Molmo2, Qwen3-VL) y de acceso cerrado (GPT-5.5), demostrando la eficacia de la retroalimentación guiada por restricciones.

Resultados
Los experimentos se realizaron en 200 instancias de Sudoku (100 cada una de los niveles de dificultad 0 y 1). Los resultados indican que la retroalimentación basada en MaxSAT mejora significativamente la consistencia lógica y las tasas de resolución en comparación con la retroalimentación de solo validez:

Refinamiento de Tablero Completo: Este modo produjo las mayores ganancias. Para GPT-5.5, la tasa de resolución aumentó del 22.5% (solo validez) al 36.5% con la retroalimentación de MaxSAT. La completitud promedio (AC) del tablero final aumentó del 72.0% al 80.7%. Notablemente, para acertijos más difíciles (Dificultad 1), el número de instancias resueltas más que se duplicó (de 10 a 21), y la AC mejoró del 62.2% al 76.7%.
Resolución Iterativa: La retroalimentación de MaxSAT también mejoró la resolución paso a paso, duplicando el número de instancias resueltas para GPT-5.5 (de 21 a 44) e incrementando la AC del 44.8% al 52.2%.
Varianza del Modelo: Aunque todos los modelos se beneficiaron, el modelo propietario GPT-5.5 mostró las mejoras más sustanciales, sugiriendo que el refinamiento simbólico es más efectivo cuando las propuestas neurales iniciales ya están cerca de la consistencia global. Los modelos de código abierto mostraron ganancias más modestas pero aun así demostraron una mejor consistencia lógica.

Significancia y Reivindicaciones
El artículo afirma que integrar la optimización simbólica en el bucle de resolución del VLM mejora la fiabilidad del razonamiento de visión-lenguaje sin reemplazar el modelo neural. Los autores enfatizan que su objetivo no es superar a los solvers simbólicos especializados (que resuelven el conjunto de datos en segundos), sino estudiar si las técnicas simbólicas pueden guiar a los VLM de propósito general hacia soluciones consistentes.

Los hallazgos sugieren que el refinamiento simbólico actúa como un poderoso mecanismo correctivo, particularmente para las predicciones neurales que son "globalmente coherentes pero parcialmente inconsistentes". Al delegar la comprobación de la consistencia lógica al oráculo de MaxSAT, el sistema asegura que cada colocación aceptada sea formalmente verificada. El trabajo destaca las fortalezas complementarias de la percepción neural y la optimización simbólica, avanzando en la sinergia entre la inteligencia artificial estadística y la simbólica en tareas de razonamiento estructurado. Los autores mantienen la modestia, señalando que, si bien el refinamiento simbólico no es un remedio completo para todas las limitaciones de los VLM, mitiga significativamente los errores lógicos y mejora la calidad de la solución, especialmente en escenarios de tablero completo.

Más como este