从错误到证明：最小核心引导的神经符号约束求解修复

# 最小核心引导的神经符号约束求解修复方法
来源：https://arxiv.org/html/2608.14771
## 从错误到证明：神经符号约束求解的最小核心引导修复

###### 摘要

要使语言模型可靠地解决约束问题，通常意味着让模型将问题转化为形式化规范，并将搜索过程委托给可靠求解器。但这种转化本身是一项语言模型任务，不忠实的转化会导致求解器忠实解决错误的问题。现有流程仅修复崩溃的转化过程，在程序运行但结果错误时静默返回求解器错误信息。我们用证明替代错误信息：当生成程序不可满足时，我们在模型自身约束上提取最小不可满足核心，并将这个无法同时成立的精确约束集交还模型——这是一个无信息泄露的信号，能精确定位故障。在包含77个问题的全新基准测试中（配有精确预言机），转换到答案集编程（Answer Set Programming）在七个领域中的六个领域保持了忠实性，仅在聚合覆盖调度问题上失败，这意味着转化成本集中在一个可诊断的模式中。最小核心（而非裸错误）能够阻止较弱模型为不可行问题编造解决方案，将编造率从79%降至7%。强大的思维链基线在准确率上与符号路径相当，这表明符号路径的价值不在于准确率，而在于其能提供验证证书且拒绝编造解决方案。

## 1 引言

语言模型正越来越多地被要求解决离散推理问题，如调度、座位安排、分配和装箱。若任由模型自由生成，其返回的流畅答案常常违反给定约束，因为自回归解码机制无法强制执行全局组合约束。标准解决方案将翻译与搜索分离：模型将自然语言问题转换为形式化规范，由可靠求解器进行推理¹¹ (https://arxiv.org/html/2608.14771#bib.bib1)；¹⁶ (https://arxiv.org/html/2608.14771#bib.bib2)；¹⁰ (https://arxiv.org/html/2608.14771#bib.bib3)；³ (https://arxiv.org/html/2608.14771#bib.bib10)。求解器提供了模型无法提供的正确性保证。

该方案的优劣完全取决于翻译质量，而语言模型的翻译存在两种失败模式。有些翻译格式错误，导致求解器报告解析或基础错误。另一些翻译虽然格式正确但不忠实：它们添加了问题从未提及的约束，可能导致可解问题被报告为不可满足；它们遗漏了已说明的约束，导致无效解被接受；或者它们错误表述了目标。当前语言模型加求解器流程中的自我纠正机制（例如Logic-LM¹¹ (https://arxiv.org/html/2608.14771#bib.bib1)中的自我优化）仅针对第一类错误：它返回求解器错误信息并要求模型重试。当求解器未报错时，循环静默进行，格式正确但不忠实的编码便得以保留。

我们提出用证明而非错误信息进行修复。我们使用答案集编程⁸ (https://arxiv.org/html/2608.14771#bib.bib14)；⁴ (https://arxiv.org/html/2608.14771#bib.bib12)将每个决策编码为单个`assign(Var,Value)`关系，并使用clingo⁵ (https://arxiv.org/html/2608.14771#bib.bib13)求解。当程序不可满足时，我们不报告“无解”，而是基于模型自身的完整性约束计算最小不可满足核心——即无法同时成立的最小约束子集，并将该集合交给模型。核心是一种证明产物：它将冲突定位到少数约束，这正是通用错误信息所隐瞒的信息。它从模型自身的程序（而非真实情况）计算得出，因此不会引入预言机信息泄露。

随后我们提出一个文献中很少检验的实证问题：在求解器也能验证答案的规模下，符号化卸载相对于纯提示和思维链实际有多大帮助，以及在何处有帮助。我们在包含七个领域77个问题的全新基准测试上回答了这一问题（配有程序化预言机），并在两个开源模型上进行评估。答案是细致入微的，而非全面优势。翻译在多数领域保持忠实，符号路径在这些领域匹配或超越思维链，但单个领域使其失效；强大的思维链基线在准确率上难以超越；而符号路径的独特价值在于它能验证最优性和不可行性且从不编造解决方案，这是提示法无法保证的。

00footnotetext:本文被接收为IJCAI-ECAI 2026逻辑与符号推理研讨会（LogiSymb）海报展示。#### 贡献部分。
- • **最小核心引导修复（第3节 (https://arxiv.org/html/2608.14771#S3)）**：我们使用基于模型自身约束的最小不可满足核心（而非求解器错误信息）修复语言模型的形式化编码。该信号是结构化的且无信息泄露，我们将约束规划和答案集编程中的冲突解释思想⁷ (https://arxiv.org/html/2608.14771#bib.bib15)；⁶ (https://arxiv.org/html/2608.14771#bib.bib16)引入修复循环，并通过控制错误信息基线¹¹ (https://arxiv.org/html/2608.14771#bib.bib1)隔离其效果。其收益是有条件的：对较弱模型效果显著，对很少出错的较强模型效果可忽略。
- • **自动形式化忠实性诊断（第6节 (https://arxiv.org/html/2608.14771#S6)）**：通过精确预言机，我们证明转换到ASP在七个领域中的六个领域保持忠实，仅在聚合覆盖调度领域失效，从而将转化成本定位到一种形式化模式而非模型本身。
- • **重新校准卸载的适用场景（第6节 (https://arxiv.org/html/2608.14771#S6)和第7节 (https://arxiv.org/html/2608.14771#S7)）**：强大的思维链基线在准确率上与符号路径相当，因此其价值在于验证证书和鲁棒性；该路径从不为不可行问题编造解决方案，而直接提示法有21%的概率编造。我们发布了基准测试和预言机。

## 2 背景与相关工作

我们的工作处于四条研究线的交汇点：工具增强推理、自动形式化、自我纠正和冲突解释。我们从最后一条中提取方法，并将其应用于前三条引发的问题。

#### 通过卸载给求解器实现忠实推理

越来越多的研究通过将推理委托给外部系统来保证语言模型推理的忠实性。Logic-LM¹¹ (https://arxiv.org/html/2608.14771#bib.bib1)将问题转化为多种符号语言之一并调用匹配求解器；SatLM¹⁶ (https://arxiv.org/html/2608.14771#bib.bib2)生成可满足性模理论求解器的声明式规范；LINC¹⁰ (https://arxiv.org/html/2608.14771#bib.bib3)将文本映射为一阶逻辑并调用定理证明器；程序辅助提示³ (https://arxiv.org/html/2608.14771#bib.bib10)将算术运算卸载给Python解释器。这些方法针对ProofWriter、FOLIO和AR-LSAT等数据集上的演绎问答或算术应用题。我们针对基于答案集编程的组合约束满足与优化问题，其中正确性指分配的可行性或最优性（而非蕴含的真值），相关故障是静默的过度约束或欠约束（而非错误的证明步骤）。

#### 自动形式化是瓶颈

一旦搜索被委托，准确率就受限于翻译的忠实性。自动形式化直接研究这种从自然语言到形式化数学的转化¹⁵ (https://arxiv.org/html/2608.14771#bib.bib11)。特别对于优化问题，NL4Opt竞赛¹² (https://arxiv.org/html/2608.14771#bib.bib5)和OptiMUS¹ (https://arxiv.org/html/2608.14771#bib.bib4)将应用题映射为混合整数线性规划。与该研究线一致，我们发现瓶颈在于形式化而非搜索，且不同问题类型间存在差异：在大多数约束领域保持忠实，但对需要聚合覆盖推理的领域表现脆弱。我们还证实了一个已知边界：答案集编程不适合作为大规模数值优化的载体，并使优化实例规模足够小以便求解器验证最优解。

#### 自我纠正及其使用的信号

迭代自我纠正改进模型输出，不同方法主要在于驱动下一次尝试的信号。Self-Refine⁹ (https://arxiv.org/html/2608.14771#bib.bib6)和Reflexion¹³ (https://arxiv.org/html/2608.14771#bib.bib8)使用模型自身的语言评价；Self-Debugging² (https://arxiv.org/html/2608.14771#bib.bib7)使用程序执行结果；Logic-LM¹¹ (https://arxiv.org/html/2608.14771#bib.bib1)使用求解器错误信息。所有这些都对已观察事件（评价、失败测试、崩溃）做出反应。没有方法使用当前尝试不一致性的证明。我们的修复信号正是这样一种证明，我们的控制比较表明关键不在于修复本身，而在于它携带的信息。

#### 冲突解释与最小不可满足核心

识别导致不可满足性的小型约束集是约束规划和可满足性领域的经典问题。Junker的QuickXplain⁷ (https://arxiv.org/html/2608.14771#bib.bib15)通过分治法计算过度约束问题的首选最小冲突，而基于删除的过滤是该家族中最简单的成员。在答案集编程中，同样的思想支撑着不一致程序的调试⁶ (https://arxiv.org/html/2608.14771#bib.bib16)和现代求解器内的核心引导优化⁵ (https://arxiv.org/html/2608.14771#bib.bib13)。我们的贡献是将这一证明产物跨越边界引入语言模型修复循环：我们不模型要求根据平直错误字符串调试，而是交给它由求解器端冲突分析产生的最小冲突子集。据我们所知，最小不可满足核心尚未被用作修复语言模型形式化的反馈信号。

## 3 方法

我们的系统遵循语言模型与求解器之间的标准分工，但使翻译步骤具备鲁棒性而非假设其正确。模型仅负责将自然语言问题转化为形式化规范；可靠求解器执行所有搜索。我们的贡献是介于两者之间的循环。当求解器报告规范无解时，我们既不盲目接受该结论，也不盲目重启模型。我们提取不一致性的证明（以最小不可满足核心的形式），并要求模型将此证明与问题文本进行协调。

问题经历四个阶段。首先，模型生成基于固定决策关系的结构化ASP编码。其次，将编码组装成程序并通过clingo运行。第三，将求解器结果分为四类之一，若非完全成功则根据求解器状态构建类型化诊断。第四，将诊断返回模型以修订编码；第二至第四阶段重复最多K次。仅第一阶段创造性使用模型。其余阶段确定性且基于求解器，因此循环的每次修正都由具体求解器产物（而非另一次自由猜测）证实。

### 3.1 决策契约

模型输出包含三个字段的JSON对象：`facts`（编码问题数据）、`rules`（包含生成候选决策的选择规则及强制要求的完整性约束）以及可选的`optimize`指令。我们对此输出施加单一契约：每个决策通过单一关系`assign(Var,Value)`表达，其中每个决策变量`Var`由选择规则绑定到恰好一个`Value`，每个要求表达为完整性约束——以`:-`开头并禁止违反该要求的组合的规则。执行环境附加`#show assign/2.`并调用clingo。图1 (https://arxiv.org/html/2608.14771#S3.F1)展示了一个小型图着色实例的完整编码。

```
% facts (problem data)
node(n1). node(n2). node(n3).
color(red). color(green). color(blue).
% choice rule: one colour per node
1 { assign(N,C) : color(C) } 1
     :- node(N).
% integrity constraints:
% adjacent nodes get different colours
:- assign(n1,C), assign(n2,C).
:- assign(n2,C), assign(n3,C).
% harness appends:  #show assign/2.
```

图1：三节点图着色问题的完整`assign/2`编码。选择规则为每个节点生成一种颜色；每个完整性约束禁止边为同色。
该契约服务于三个目的，且每个都对后续方法至关重要。首先，它为每个领域提供单一、统一的解概念，因此一个预言机可评估任何系统（无论是符号管道还是提示基线）的输出，无需领域特定解析；着色、名单、座位和背包装箱都是`assign`原子的集合。其次，它使编码紧凑且规模随问题增长保持稳定，因为决策逻辑存在于常数数量的规则中，仅事实部分随规模扩展；三个节点的图和九十节点的图共享相同的选择规则和约束模式。第三，也是对修复最重要的，它清晰分离了模型可能出错的部分（完整性约束）和由数据固定的部分（事实和选择规则），这正是第3.3节 (https://arxiv.org/html/2608.14771#S3.SS3)核心提取所利用的分离。为确保公平性，研究中的每个系统（包括提示基线）都获得相同的决策变量及允许值，因此没有系统因输出格式而获得优势或惩罚，所有系统均根据其推理是否得出正确分配来评判。

### 3.2 编译与结果分类

组装并求解编码恰好产生四种结果之一，循环对每种结果做出不同反应。当clingo返回包含`assign/2`原子的答案集时，结果为`ok`；这是唯一的终止结果，原子成为分配。`syntax_error`发生在基础化或解析失败时（模型编写格式错误规则或不安全变量导致）。`empty`发生在程序可满足但未产生`assign/2`原子时（模型忘记选择规则或用其他谓词建模决策导致）。`unsat`发生在程序格式正确、基础化成功但无答案集时。

这四种结果信息量不对称，这种不对称是后续方法存在的原因。`syntax_error`是显性的：clingo指向问题规则，先前的错误信息优化已很好处理此情况。危险结果是`unsat`，因其对原因保持静默。例如，对完美可解问题的过度约束转化（如幻想出文本从未提及的约束）会产生无答案集的程序，而该程序仅凭裸判定无法与真正不可行问题的忠实翻译区分。仅读取“无答案集”的模型无法判断应修复自身约束还是报告问题无解。消除这种歧义正是核心提供的。

### 3.3 使用证明修复