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

# 基于MaxSAT的反馈指导数独视觉语言模型 来源：https://arxiv.org/html/2607.12711 11institutetext:1人工智能研究所（IIIA），西班牙国家科学研究委员会（CSIC），巴塞罗那，加泰罗尼亚，西班牙 11email:[email protected] 2机器人及工业信息学研究所（IRI-CSIC-UPC），巴塞罗那，西班牙

###### 摘要

视觉-语言模型（VLM）最近在结构化视觉推理任务（包括基于网格的谜题）上展现出令人瞩目的表现。然而，尽管具备强大的感知能力，这些模型缺乏明确机制来强制逻辑一致性，频繁生成违反底层约束的赋值。本文提出一种神经符号方法，通过一个**最大可满足性**（MaxSAT）预言机将形式化约束推理整合到VLM求解过程中。符号组件并非直接计算解，而是充当一致性验证器和精炼引擎。VLM生成的候选放置被编码为偏MaxSAT公式中的软子句，而数独约束保持为硬子句。当出现不一致时，MaxSAT求解器找出一个最大的相互一致的赋值子集，并将其转化为结构化的文本和视觉反馈，以指导后续的精炼。我们在一个数独数据集上，针对多个开源和闭源VLM评估了我们的方法。结果表明，基于MaxSAT的反馈改善了逻辑一致性，并增加了被求解实例的数量，特别是在全盘精炼模式下。这些发现表明，符号优化可以增强视觉-语言推理的可靠性。

## 1 引言

视觉-语言模型（VLM）的最新进展使系统能够直接从图像解决结构化视觉推理任务[30, 28]，包括基于网格的逻辑谜题如**数独**[29]。尽管经验表现良好，这些模型缺乏强制逻辑一致性的明确机制，往往依赖模式识别而非原则性的约束推理[28]。因此，它们的输出可能违反结构约束，或者在尝试修正错误解决方案时表现出不稳定行为。相比之下，约束规划（CP）[26]和基于可满足性（SAT）的方法[2]提供了正确性和完备性的形式化保证。数独具有成熟的SAT编码[19]，其中每个谜题有**且仅有一个**有效解，对应于一个布尔公式的可满足赋值。更一般地，约束优化方法，如**最大可满足性**（MaxSAT）[1,17]，不仅能推理可行性，还能推理局部一致性和解精炼。这些符号技术提供了正确性保证，但缺乏现代语言模型（如VLM）的感知灵活性和提议生成能力。这种互补关系引出了以下问题：**形式化约束优化能否指导视觉-语言模型解决诸如数独的视觉逻辑谜题？**

近期的神经符号方法表明，将神经模型与形式化求解器结合可以提高推理密集型任务的可靠性[25,33,27,23]。然而，大多数先前工作聚焦于基于文本的推理或规划领域。将视觉-语言模型与约束优化技术相结合用于结构化视觉问题仍鲜有探索。

本文提出一种数独求解的混合神经符号方法。VLM从谜题图像生成候选放置，而**MaxSAT预言机**使用偏MaxSAT公式验证并精炼这些提议。数独约束被编码为硬子句，模型生成的放置被编码为软子句。MaxSAT求解器并非直接计算出一个解，而是选出提议赋值中最大的相互一致子集。该子集随后被转化为结构化文本和视觉反馈，指导模型进行后续精炼。由此产生的架构建立了明确的分工：神经组件执行感知和启发式提议生成，而符号组件通过优化执行逻辑一致性。因此，每个被接受的放置都经过底层约束模型的形式化验证。我们的目标并非超越符号求解器，而是研究符号优化能否提高通用VLM的可靠性。

我们在一个基准数独数据集[11]上的实证评估表明，将偏MaxSAT精炼整合到VLM求解循环中，显著改善了逻辑一致性、解的完备性以及求解率，这一效果在开源和闭源VLM上均得到体现。最强增益出现在全盘求解场景中，符号精炼能有效修复全局一致但局部不一致的神经预测，从而使得显著更多的谜题被正确求解，包括更具挑战性的实例。

总之，本文做出以下贡献：
- • 一个基于MaxSAT的神经符号框架，用于验证和精炼视觉-语言模型（VLM）生成的数独解。
- • 将偏MaxSAT整合到VLM求解循环中，其中模型生成的放置被视为软约束，并通过约束优化进行精炼。
- • 在多种开源和闭源VLM上的实证评估表明，基于MaxSAT的精炼改善了逻辑一致性，并显著增加了被求解实例的数量。

## 2 预备知识

**布尔可满足性**（SAT）问题是命题逻辑中的经典判定问题[2]。一个**文字**要么是一个命题变量xixᵢ，要么是其否定¬xi。一个公式若表示为子句的合取，且每个子句是文字的析取，则该公式为**合取范式**（CNF）。给定一个CNF公式φ，SAT问题在于确定是否存在一个真值赋值，使得φ的所有子句都被满足，或者φ不可满足。

**最大可满足性**（MaxSAT）问题以优化目标扩展了SAT[1,17]。给定一个CNF公式φ，目标是计算一个使被满足子句数量最大化的赋值。在**偏MaxSAT**设定中，公式φ被划分为一组硬子句φh和一组软子句φs。目标是找到一个满足φh中所有子句的赋值，同时最小化φs中未满足的子句数量。在**偏MaxSAT**变体中，目标变为最小化未满足软子句的总数。

###### 例1（偏MaxSAT）
考虑偏MaxSAT公式φ = (φh, φs)，其中 φh = {(x₁ ∨ x₂), (¬x₂ ∨ x₃)}，φs = {(¬x₁), (¬x₃)}。赋值 {(x₁,1), (x₂,0), (x₃,0)} 满足φh中的所有硬子句，且仅违反软子句 (¬x₁)，产生总代价1。因此，它是一个最优解。

## 3 作为MaxSAT问题的数独

令 n=9，且令 r,c,d ∈ {1,…,n}。我们引入布尔变量 X_{r,c,d} ∈ {0,1}，其中 X_{r,c,d}=1 表示数字d被分配到单元格 (r,c)。由此，我们可以将数独问题编码为约束满足问题，采用先前使用的编码[19]，将其编码为可满足性（SAT）问题。使用以下约束：
- **• 单元格约束。** 每个单元格必须恰好包含一个数字：∀r,c∈{1,…,n}: ∑_{d=1}^n X_{r,c,d} = 1。
- **• 行约束。** 每个数字在每一行必须恰好出现一次：∀r,d∈{1,…,n}: ∑_{c=1}^n X_{r,c,d} = 1。
- **• 列约束。** 每个数字在每一列必须恰好出现一次：∀c,d∈{1,…,n}: ∑_{r=1}^n X_{r,c,d} = 1。
- **• 子网格约束。** 每个数字在每个 sqrt(n)×sqrt(n) 子网格中必须恰好出现一次：∑_{r∈R_b} ∑_{c∈C_b} X_{r,c,d} = 1   ∀d∈{1,…,n}, ∀b∈{1,…,9}，其中 (R_b, C_b) 表示子网格 b 的行和列索引。

**CNF编码。** 每个恰好一次约束使用标准成对编码编码为**合取范式（CNF）**：(i) 一个至少一个子句，强制组中至少一个文字为真；(ii) 成对的至多一个子句，阻止两个文字同时为真。得到的CNF公式构成了数独实例的硬约束集，可以使用SAT求解器求解。

**MaxSAT公式。** 在我们的设定中，视觉-语言模型（VLM）提出的放置（即棋步）被编码为偏最大可满足性（MaxSAT）公式中的软单元子句。目标是满足所有数独约束（硬子句），同时最大化一致的模型提议放置（软子句）的数量。这种公式通过MaxSAT优化实现了候选解的精炼。

图1：用于数独求解的神经符号交互循环。VLM提出候选放置，由MaxSAT预言机验证。当检测到冲突时，从约束派生的反馈在谜题中被高亮并返回，以指导后续精炼。

## 4 神经符号交互循环

图1展示了我们方法背后的神经符号交互循环。该框架将一个视觉-语言模型（VLM）与一个符号偏最大可满足性（MaxSAT）预言机相结合，迭代构建逻辑一致的数独赋值。

设 P 表示一个以图像表示的数独谜题，设 X = {X_{r,c,d} | r,c,d ∈ {1,…,9}} 为第3节中引入的布尔变量集合，其中 X_{r,c,d}=1 表示数字 d 被分配到单元格 (r,c)。给定数独谜题的图像，VLM生成一组候选赋值 Â = {(r,c,d)}，每个赋值对应于将数字 d 放入单元格 (r,c)，并且在符号编码中与布尔文字 X_{r,c,d} 相关联。

然后，符号组件构建一个偏MaxSAT实例 Φ = (Φh, Φs)，其中 Φh 包含编码所有数独约束的硬子句，Φs 包含对应于VLM提议赋值的软单元子句。更精确地，对于每个提议放置 (r,c,d) ∈ Â，预言机引入软子句 (X_{r,c,d})。MaxSAT求解器随后计算一个满足所有硬子句同时最大化满足软子句数量的赋值。

如果所有软子句都被满足，则提议与数独约束逻辑一致。否则，未满足的软子句集对应于被MaxSAT求解器拒绝的赋值，这些被解释为逻辑不一致的放置。这些不一致被转化为结构化反馈，包括：(i) 识别不一致放置的文本描述；(ii) 在谜题图像中高亮冲突单元格的视觉注释。在此反馈条件下，VLM生成一个精炼后的赋值提议，交互循环重复，直到：(i) 获得一个完整且逻辑一致的解；或 (ii) 达到预定义的终止条件。

重要的是，逻辑一致性检查和优化完全交由符号预言机处理。因此，VLM只负责感知解释和候选生成，而形式化约束满足由MaxSAT组件保证。我们在该框架内评估两种交互协议：(i) 迭代单放置求解；(ii) 全盘精炼。实验中使用的所有提示在附录0.A中提供。

### 4.1 迭代数独求解

在迭代模式下，VLM在每个交互步骤提出一个单独放置。设 a_t = (r_t, c_t, d_t) 表示在第 t 次迭代时提出的放置。提议赋值被编码为软单元子句，并添加到偏MaxSAT实例中。求解器随后计算一个最优赋值，满足所有硬数独约束，同时最大化与提议赋值的一致性。如果 a_t 属于最优MaxSAT解，则该放置被接受并永久添加到棋盘状态。否则，该放置被拒绝，并作为纠正反馈返回给VLM。该过程重复，直到获得有效数独解或达到终止条件。

因此，这种交互协议可以解释为一个优化引导的顺序决策过程，其中符号一致性检查约束着VLM的生成行为。如果我们假设VLM在这种情况下始终只返回一个放置，那么一个基于SAT的标准验证器就足以检查该放置是否与数独约束一致。然而，我们使用MaxSAT求解器是为了在VLM输出多个放置时保持相同的公式，因为这使得我们能够识别出在使逻辑不正确的提议放置数量最小化意义上的最优修正。换句话说，MaxSAT泛化了基于SAT的检查：当只提出一个放置时，两种方法一致（尽管基于SAT的方法应更高效）；而当产生多个放置时，MaxSAT返回一个最小冲突赋值集以供拒绝，从而为VLM提供更具信息量和鲁棒性的反馈信号。

### 4.2 全盘精炼

在全盘模式下，VLM在单次交互中提出一个完整的数独赋值。所有预测的放置被编码为偏MaxSAT公式中的软单元子句。给定提议赋值集 Â，MaxSAT求解器计算出 Â 中最大的相互一致子集