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

视觉语言模型（VLM）近来在结构化视觉推理任务（包括网格谜题）上展现前景。但尽管感知能力强，这些模型缺乏强制逻辑一致性的显式机制，频繁生成违反底层约束的赋值。本文提出神经符号方法：经最大可满足性（MaxSAT）预言机把形式约束推理集成进VLM求解过程。符号组件不直接计算解，而是充当一致性验证器与精炼引擎：VLM生成的候选放置被编码为部分MaxSAT公式中的软子句，数独约束保持硬子句；出现不一致时，MaxSAT求解器识别最大的相互一致赋值子集，随后转为结构化的文本与视觉反馈，引导后续精炼。我们在数独数据集上跨多个开源与闭源VLM评估：MaxSAT反馈改善逻辑一致性并增加解决实例数——在全盘精炼模式下尤甚。结果表明符号优化能增强视觉语言推理的可靠性。