💻 computer science

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

Cet article propose un cadre neuro-symbolique qui améliore les performances des modèles vision-langage sur les puzzles de Sudoku en utilisant un oracle MaxSAT pour valider les assignations candidates et fournir un retour structuré, imposant ainsi la cohérence logique et améliorant la précision des solutions.

Auteurs originaux : Pedro Orvalho, Guillem Alenyà, Felip Manyà

Publié 2026-07-15

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Pedro Orvalho, Guillem Alenyà, Felip Manyà

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous avez un ami robot super intelligent, capable de regarder des images et de deviner ce qu'elles contiennent. Vous lui montrez l'image d'un puzzle de Sudoku (une grille de 9x9 où l'on remplit les chiffres de 1 à 9) et il essaie de deviner les nombres. Ce robot est comme un Modèle Vision-Langage (VLM). Il est excellent pour « voir » la grille et « lire » les indices, mais il possède un drôle de point aveugle : il n'a pas de carnet de règles intégré pour la logique. Il pourrait deviner un nombre qui semble correct mais qui enfreint les règles, comme placer deux 5 dans la même ligne. C'est comme un artiste talentueux qui peut peindre un magnifique ciel mais qui peint accidentellement deux soleils au même endroit parce qu'il a oublié les lois de la physique.

Le document présente une nouvelle collaboration pour corriger cela. Ils associent le robot artiste à un Oracle MaxSAT strict et logique. Imaginez l'Oracle MaxSAT comme un arbitre super organisé qui détient le carnet de règles officiel du Sudoku. L'arbitre n'essaie pas de peindre le tableau ; au contraire, il observe les suppositions du robot et les vérifie par rapport aux règles.

Voici comment fonctionne cette collaboration :

La Supposition : Le robot regarde l'image du puzzle et suggère où placer les nombres.
La Vérification : L'arbitre prend ces suggestions. Il traite les règles du Sudoku comme des « lois strictes » (vous devez les suivre) et les suppositions du robot comme des « suggestions souples » (nous espérons qu'elles sont correctes, mais nous pouvons les modifier si elles enfreignent les lois).
La Correction : Si le robot fait une erreur, l'arbitre ne se contente pas de dire « Faux ! ». Il trouve le plus grand groupe de suppositions qui fonctionnent ensemble et dit au robot : « Gardez ceux-là, mais changez ceux-ci spécifiquement. » Il dessine ensuite un dessin sur le puzzle montrant exactement où se situe le conflit et l'explique avec des mots.
La Tentative : Le robot regarde les notes de l'arbitre, corrige ses erreurs et réessaie.

Les chercheurs ont testé cela sur un tas de puzzles de Sudoku, allant du facile au difficile. Ils ont utilisé trois robots différents : deux en open-source (nommés Molmo2 et Qwen3-VL) et un très puissant, en source fermée (GPT-5.5).

Qu'ont-ils trouvé ?
Sans l'arbitre, les robots restaient souvent bloqués ou remplissaient des nombres qui n'avaient pas de sens. Mais lorsqu'ils ont ajouté l'arbitre MaxSAT :

Les robots sont devenus bien meilleurs pour suivre les règles.
Ils ont résolu beaucoup plus de puzzles. Par exemple, le robot GPT-5.5, lorsqu'on lui demandait de résoudre tout le plateau d'un coup, est passé de la résolution de 45 puzzles à 73 puzzles. Sa complétude moyenne (combien de cellules il a réussies) est passée de 72,0 % à 80,7 %.
Même les robots en open-source se sont améliorés, bien que pas autant que le grand modèle. Molmo2 est passé de 17 puzzles résolus à 28, et Qwen3-VL de 10 à 13.

Le document suggère que ce travail d'équipe est particulièrement utile lorsque le robot est presque correct mais commet quelques glissements logiques. L'arbitre aide à nettoyer ces glissements pour obtenir une solution parfaite.

Ce que le document dit que ceci N'EST PAS :
Les auteurs sont très clairs : ils n'essaient pas de remplacer le robot par l'arbitre. Ils ne disent pas que l'arbitre devrait résoudre le puzzle tout seul (ce qu'il pourrait faire en quelques secondes). Le but n'est pas de battre la vitesse de l'arbitre ; c'est de voir si l'arbitre peut apprendre au robot à être plus fiable. Ils notent également que les puzzles plus difficiles (étiquetés « Difficulté 1 ») étaient toujours plus rudes que les faciles, mais l'arbitre a aidé les robots à les gérer bien mieux qu'auparavant.

En bref, le document montre que donner à une IA visuelle un « compagnon » logique pour vérifier son travail la rend bien meilleure pour résoudre des puzzles. C'est une victoire pour le travail d'équipe, prouvant que mélanger un devineur créatif avec un vérificateur de règles strict crée un système plus intelligent que chacun d'eux seul.

Résumé Technique : Retour d'Information Basé sur MaxSAT pour Guider les Modèles Vision-Langage dans le Sudoku

Énoncé du Problème
Les modèles vision-langage (VLM) ont démontré des capacités prometteuses dans les tâches de raisonnement visuel structuré, notamment les puzzles de grille comme le Sudoku. Cependant, malgré leurs fortes capacités perceptuelles, les VLM manquent de mécanismes explicites pour imposer une cohérence logique. Ils reposent fréquemment sur la reconnaissance de formes plutôt que sur un raisonnement par contraintes fondé sur des principes, ce qui conduit à des sorties qui violent les contraintes structurelles (par exemple, des doublons de chiffres dans les lignes ou les colonnes) ou présentent un comportement instable lorsqu'ils tentent d'affiner des solutions incorrectes. Bien que les méthodes de programmation par contraintes (CP) et de satisfaction (SAT) offrent des garanties formelles de validité, elles manquent de la flexibilité perceptive et des capacités de génération de propositions des VLM modernes. Cet article examine si l'optimisation de contraintes formelles peut guider les VLM pour résoudre des puzzles logiques visuels de manière plus fiable.

Méthodologie
Les auteurs proposent un cadre hybride neuro-symbolique où un VLM agit comme un générateur de propositions et un oracle MaxSAT agit comme un validateur de cohérence et un moteur de raffinement. L'approche fonctionne via une boucle d'interaction itérative :

Formulation : Le problème de Sudoku est encodé sous la forme d'une instance de MaxSAT partiel.
- Clauses Dures ( $\Phi_h$ ) : Encodent les contraintes fondamentales du Sudoku (chaque cellule contient exactement un chiffre ; chaque chiffre apparaît exactement une fois dans chaque ligne, colonne et sous-grille). Celles-ci sont non négociables.
- Clauses Douces ( $\Phi_s$ ) : Encodent les placements candidats proposés par le VLM sous forme de clauses unitaires.
Boucle d'Interaction :
- Le VLM génère des assignations candidates (placement de chiffres dans les cellules) basées sur l'image du puzzle.
- Ces assignations sont transmises au solveur MaxSAT (spécifiquement le solveur RC2 de la boîte à outils PySAT).
- Le solveur calcule une assignation qui satisfait toutes les clauses dures tout en maximisant le nombre de clauses douces satisfaites (c'est-à-dire en conservant autant de propositions du VLM que possible sans violer les contraintes).
- Génération de Feedback : Si les propositions du VLM sont incohérentes, le solveur MaxSAT identifie le plus grand sous-ensemble mutuellement cohérent d'assignations. Les assignations rejetées (celles qui sont dans l'ensemble des clauses douces mais pas dans la solution optimale) sont traduites en un feedback structuré, incluant des descriptions textuelles des incohérences et des annotations visuelles mettant en évidence les cellules conflictuelles sur l'image du puzzle.
- Le VLM utilise ce feedback pour générer une proposition raffinée.
Protocoles : Le cadre évalue deux modes d'interaction :
- Placement Unique Itératif : Le VLM propose un mouvement à la fois. MaxSAT valide ; si cohérent, il est accepté ; sinon, il est rejeté avec un feedback.
- Raffinement de la Grille Complète : Le VLM propose un état de grille complet. MaxSAT identifie le plus grand sous-ensemble cohérent de l'ensemble de la grille, ne rejetant que les cellules conflictuelles, et renvoie un feedback pour un raffinement global.

Contributions Clés

Un Cadre Neuro-Symbolique : Une architecture novatrice pour valider et affiner les solutions de Sudoku générées par VLM à l'aide d'un oracle MaxSAT, établissant une division claire du travail où la composante neurale gère la perception et la composante symbolique impose la cohérence logique.
Intégration de MaxSAT Partiel : L'intégration de MaxSAT partiel dans la boucle de résolution du VLM, traitant les placements générés par le modèle comme des contraintes douces. Cela permet d'identifier et de réparer le plus grand sous-ensemble mutuellement cohérent d'une proposition plutôt que de rejeter l'intégralité de la sortie.
Évaluation Empirique : Une évaluation complète sur plusieurs VLM ouverts (Molmo2, Qwen3-VL) et fermés (GPT-5.5) sur un ensemble de données de Sudoku de référence, démontrant l'efficacité du feedback guidé par les contraintes.

Résultats
Les expériences ont été menées sur 200 instances de Sudoku (100 chacune pour les niveaux de difficulté 0 et 1). Les résultats indiquent que le feedback basé sur MaxSAT améliore significativement la cohérence logique et les taux de résolution par rapport à un feedback de validité seule :

Raffinement de la Grille Complète : Ce mode a produit les gains les plus importants. Pour GPT-5.5, le taux de résolution est passé de 22,5 % (validité seule) à 36,5 % avec le feedback MaxSAT. La complétude moyenne (AC) de la grille finale est passée de 72,0 % à 80,7 %. Notamment, pour les puzzles plus difficiles (Difficulté 1), le nombre d'instances résolues a plus que doublé (de 10 à 21) et l'AC est passé de 62,2 % à 76,7 %.
Résolution Itérative : Le feedback MaxSAT a également amélioré la résolution étape par étape, doublant le nombre d'instances résolues pour GPT-5.5 (de 21 à 44) et augmentant l'AC de 44,8 % à 52,2 %.
Variance des Modèles : Bien que tous les modèles en aient bénéficié, le modèle propriétaire GPT-5.5 a montré les améliorations les plus substantielles, suggérant que le raffinement symbolique est plus efficace lorsque les propositions neurales initiales sont déjà proches d'une cohérence globale. Les modèles open-source ont montré des gains plus modestes mais ont tout de même démontré une amélioration de la cohérence logique.

Signification et Revendications
L'article affirme que l'intégration de l'optimisation symbolique dans la boucle de résolution du VLM améliore la fiabilité du raisonnement vision-langage sans remplacer le modèle neural. Les auteurs soulignent que leur objectif n'est pas de surpasser les solveurs symboliques spécialisés (qui résolvent le jeu de données en quelques secondes), mais d'étudier si les techniques symboliques peuvent guider les VLM généralistes vers des solutions cohérentes.

Les conclusions suggèrent que le raffinement symbolique agit comme un mécanisme correctif puissant, particulièrement pour les prédictions neurales "globalement cohérentes mais partiellement incohérentes". En déléguant la vérification de la cohérence logique à l'oracle MaxSAT, le système garantit que chaque placement accepté est formellement vérifié. Ce travail met en lumière les forces complémentaires de la perception neurale et de l'optimisation symbolique, faisant progresser la synergie entre l'intelligence artificielle statistique et symbolique dans les tâches de raisonnement structuré. Les auteurs restent modestes, notant que si le raffinement symbolique n'est pas un remède complet à toutes les limitations des VLM, il atténue considérablement les erreurs logiques et améliore la qualité des solutions, en particulier dans les scénarios de grille complète.

Articles similaires