MaxSAT反馈引导视觉语言模型解数独

背景

视觉语言模型（Vision-Language Models, VLMs）在结构化视觉推理任务（包括基于网格的谜题）上近期展现了有前景的性能。然而，尽管具备强大的感知能力，这些模型缺乏显式的逻辑一致性强制执行机制，经常生成违反底层约束的赋值。数独（Sudoku）作为一种典型的约束满足问题，为评估 VLMs 在规则推理上的可靠性提供了理想测试平台。现有方法通常直接让 VLM 求解，但无法保证其输出满足所有数独规则（行、列、宫数字不重复）。为此，研究者提出将形式约束推理引入 VLM 求解流程，利用最大可满足性（Maximum Satisfiability, MaxSAT）优化器作为校验与精炼引擎。

核心内容

本文提出一种神经符号（neuro-symbolic）方法，将形式约束推理集成到 VLM 的数独求解过程中。具体而言，符号组件不直接计算解，而是充当一致性校验器和精炼引擎。VLM 生成的候选数字放置被编码为部分 MaxSAT 公式中的软约束（soft clauses），而数独的硬约束（hard clauses）保持不变。当出现不一致时，MaxSAT 求解器找出一个最大的相互一致的赋值子集（largest mutually consistent subset of assignments），然后将其转换为结构化的文本和视觉反馈，指导 VLM 进行后续的迭代精炼。

实验在数独数据集上对多个开源和闭源 VLM 进行评估。结果表明，基于 MaxSAT 的反馈提升了逻辑一致性，并增加了成功求解的实例数量，尤其在完整棋盘精炼模式（full-board refinement mode）下效果显著。这些发现表明，符号优化可以增强视觉语言推理的可靠性。

关键要点

• 提出将 MaxSAT 求解器作为 VLM 求解数独的外挂校验与反馈引擎，而非直接计算解。
• VLM 的初始候选放置被编码为软约束，数独规则作为硬约束形成部分 MaxSAT 问题。
• MaxSAT 求解器识别最大的相互一致的子集，并据此生成结构化的文本和视觉反馈，引导 VLM 修正错误。
• 实验涵盖多个开源和闭源 VLM，证明 MaxSAT 反馈显著提升逻辑一致性和求解成功率。
• 完整棋盘精炼模式比逐步修正模式效果更好，表明全局一致性约束的有效性。
• 该方法属于神经符号系统的典型应用，结合了深度学习的感知能力与符号推理的精确性。

意义与影响

这项工作首次将 MaxSAT 优化器引入 VLM 的视觉推理流程，提供了一种可解释、可校验的修正机制。其意义在于：第一，将符号约束推理与深度学习模型有机结合，克服了纯神经网络在规则遵守上的缺陷；第二，为其他结构化视觉推理任务（如逻辑谜题、表格理解、UI 布局校验）提供了通用范式；第三，展示了即使不求解完整问题，仅通过最大一致子集的反馈即可有效引导模型自我修正，降低了符号组件对完整求解器的依赖。该方法有望提升 VLM 在需要严格逻辑一致性的应用场景（如自动化数据录入、数学推理、形式验证）中的可靠性和实用性。未来可进一步扩展到更复杂的约束系统，并探索与神经符号学习框架的深度融合。