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

Resumo Técnico: Feedback Baseado em MaxSAT para Guiar Modelos de Visão-Linguagem em Sudoku

Definição do Problema
Modelos de Visão-Linguagem (VLMs) têm demonstrado capacidades promissoras em tarefas de raciocínio visual estruturado, incluindo quebra-cabeças baseados em grades, como o Sudoku. No entanto, apesar de suas fortes habilidades perceptivas, os VLMs carecem de mecanismos explícitos para impor consistência lógica. Eles frequentemente dependem de reconhecimento de padrões em vez de raciocínio de restrição principista, o que leva a saídas que violam restrições estruturais (por exemplo, números duplicados em linhas ou colunas) ou exibem comportamento instável ao tentar refinar soluções incorretas. Embora métodos de Programação por Restrição (CP) e Satisfatibilidade (SAT) ofereçam garantias formais de correção, eles carecem da flexibilidade perceptual e das capacidades de geração de propostas dos modernos VLMs. Este artigo aborda a questão de saber se a otimização de restrições formais pode guiar os VLMs a resolver quebra-cabeças de lógica visual de forma mais confiável.

Metodologia
Os autores propõem uma estrutura neuro-simbólica híbrida onde um VLM atua como um gerador de propostas e um oráculo de Satisfatibilidade Máxima (MaxSAT) atua como um validador de consistência e motor de refinamento. A abordagem opera através de um loop de interação iterativo:

1. Formulação: O problema de Sudoku é codificado como uma instância de MaxSAT Parcial.
   • Cláusulas Rígidas ($\Phi_h$): Codificam as restrições fundamentais do Sudoku (cada célula contém exatamente um dígito; cada dígito aparece exatamente uma vez em cada linha, coluna e subgrade). Estas são inegociáveis.
   • Cláusulas Flexíveis ($\Phi_s$): Codificam as atribuições candidatas propostas pelo VLM como cláusulas unitárias.
2. Loop de Interação:
   • O VLM gera atribuições candidatas (posicionando dígitos em células) com base na imagem do quebra-cabeça.
   • Essas atribuições são enviadas ao solver de MaxSAT (especificamente o solver RC2 do toolkit PySAT).
   • O solver computa uma atribuição que satisfaz todas as cláusulas rígidas enquanto maximiza o número de cláusulas flexíveis satisfeitas (ou seja, mantendo o maior número possível de propostas do VLM sem violar as restrições).
   • Geração de Feedback: Se as propostas do VLM forem inconsistentes, o solver de MaxSAT identifica o maior subconjunto mutuamente consistente de atribuições. As atribuições rejeitadas (aquelas no conjunto de cláusulas flexíveis, mas não na solução ótima) são traduzidas em feedback estruturado, incluindo descrições textuais de inconsistências e anotações visuais destacando células conflitantes na imagem do quebra-cabeça.
   • O VLM utiliza este feedback para gerar uma proposta refinada.
3. Protocolos: A estrutura avalia dois modos de interação:
   • Posicionamento Único Iterativo: O VLM propõe um movimento de cada vez. O MaxSAT valida; se consistente, é aceito; caso contrário, é rejeitado com feedback.
   • Refinamento de Quadro Completo: O Vlem propõe um estado de quadro completo. O MaxSAT identifica o maior subconjunto consistente de todo o quadro, rejeitando apenas as células conflitantes, e retorna feedback para um refinamento global.

Principais Contribuições

• Uma Estrutura Neuro-Simbólica: Uma arquitetura inovadora para validar e refinar soluções de Sudoku geradas por VLM usando um oráculo de MaxSAT, estabelecendo uma divisão clara de trabalho onde o componente neural lida com a percepção e o componente simbólico impõe a consistência lógica.
• Integração de MaxSAT Parcial: A integração de MaxSAT parcial no loop de resolução do VLM, tratando as colocações geradas pelo modelo como restrições flexíveis. Isso permite que o sistema identifique e repare o maior subconjunto mutuamente consistente de uma proposta, em vez de descartar toda a saída.
• Avaliação Empírica: Uma avaliação abrangente em múltiplos VLMs de código aberto (Molmo2, Qwen3-VL) e de acesso fechado (GPT-5.5) em um conjunto de dados de benchmark de Sudoku, demonstrando a eficácia do feedback guiado por restrições.

Resultados
Experimentos foram conduzidos em 200 instâncias de Sudoku (100 de cada nível de dificuldade 0 e 1). Os resultados indicam que o feedback baseado em MaxSAT melhora significativamente a consistência lógica e as taxas de resolução em comparação com o feedback de apenas validade:

• Refinamento de Quadro Completo: Este modo rendeu os maiores ganhos. Para o GPT-5.5, a taxa de resolução aumentou de 22,5% (apenas validade) para 36,5% com o feedback de MaxSAT. A completude média (AC) do quadro final subiu de 72,0% para 80,7%. Notavelmente, para quebra-cabeças mais difíceis (Dificuldade 1), o número de instâncias resolvidas mais que dobrou (de 10 para 21), e a AC melhorou de 62,2% para 76,7%.
• Resolução Iterativa: O feedback de MaxSAT também melhorou a resolução passo a passo, dobrando o número de instâncias resolvidas para o GPT-5.5 (de 21 para 44) e aumentando a AC de 44,8% para 52,2%.
• Variância do Modelo: Embora todos os modelos tenham se beneficiado, o proprietário GPT-5.5 mostrou as melhorias mais substanciais, sugerindo que o refinamento simbólico é mais eficaz quando as propostas neurais iniciais já estão próximas da consistência global. Os modelos de código aberto mostraram ganhos mais modestos, mas ainda demonstraram melhor consistência lógica.

Significância e Alegações
O artigo afirma que integrar a otimização simbólica no loop de resolução do VLM aumenta a confiabilidade do raciocínio visual-linguístico sem substituir o modelo neural. Os autores enfatizam que seu objetivo não é superar solvers simbólicos especializados (que resolvem o conjunto de dados em segundos), mas sim estudar se técnicas simbólicas podem guiar VLMs de propósito geral em direção a soluções consistentes.

Os achados sugerem que o refinamento simbólico atua como um poderoso mecanismo corretivo, particularmente para previsões neurais que são "globalmente coerentes, mas parcialmente inconsistentes". Ao delegar a verificação de consistência lógica ao oráculo de MaxSAT, o sistema garante que cada colocação aceita seja formalmente verificada. O trabalho destaca as forças complementares da percepção neural e da otimização simbólica, avançando a sinergia entre a inteligência artificial estatística e simbólica em tarefas de raciocínio estruturado. Os autores permanecem modestos, observando que, embora o refinamento simbólico não seja um remédio completo para todas as limitações dos VLMs, ele mitiga significativamente os erros lógicos e melhora a qualidade da solução, especialmente em cenários de quadro completo.