摘要
视觉-语言模型（VLMs）在结构化视觉推理任务上表现出色，包括基于网格的谜题。然而，尽管具备强大的感知能力，这些模型缺乏明确的逻辑一致性机制，常常生成违反基本约束的解答。本文提出了一种神经符号方法，通过最大可满足性（MaxSAT）oracle将形式约束推理集成到VLM的求解过程中。
方法
不同于直接计算解，符号组件作为一致性验证器和精炼引擎。VLM生成的候选放置被编码为部分MaxSAT形式中的软子句，而数独约束则保持为硬子句。
当出现不一致时，MaxSAT求解器识别出最大的互相一致的分配子集，并将其转化为结构化的文本和视觉反馈，以指导后续的精炼过程。
实验
我们在多个开源和闭源的VLM上评估了该方法，使用的数独数据集显示，基于MaxSAT的反馈提高了逻辑一致性，并增加了解决实例的数量，尤其是在全盘精炼模式下。
这些结果表明，符号优化可以增强视觉语言推理的可靠性。
博主点评： 该研究通过引入MaxSAT反馈机制，成功提升了视觉语言模型在数独问题上的表现，展示了神经符号方法在复杂推理任务中的潜力，值得关注其在其他应用场景中的推广。