🤖 AI

Position: Certified Correctness in Neural Constraint Reasoning Requires Symbolic Integration

本立场论文认为，为了确保神经约束推理的可证明正确性，特别是针对像数独这样验证高效但求解困难的 NP 完全问题，神经方法必须与符号求解器进行双向集成，而非仅仅依赖纯学习。

原作者： Shufeng Kong, Xiaochuan Zhang, Caihua Liu

发布于 2026-08-18

📖 1 分钟阅读☕ 轻松阅读

原作者： Shufeng Kong, Xiaochuan Zhang, Caihua Liu

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

在人工智能领域，存在着两种思维方式之间日益扩大的分歧。一方面是那些通过观察海量数据、识别模式并做出合理推测来学习的系统。这些系统具有极高的灵活性，能够处理像照片或语音这样杂乱的现实世界输入。另一方面是遵循严格、不可逾越规则的系统，就像一名检查作业的数学老师。这些基于规则的系统非常僵化，难以处理任何非完美格式的内容，但它们绝不会犯逻辑错误。多年来，研究人员一直希望模式匹配系统最终能学会完美地遵循规则，从而使这种僵化的、遵循规则的方法变得过时。然而，一项新的研究方向表明，对于某些特定类型的问题，这种希望是错位的。当赌注很高且规则是绝对的时候，一个只会进行猜测的系统，无论它多么聪明，最终都会失败。问题不再是我们能否制造出一台“通常正确”的机器，而是我们能否制造出一台“可证明正确”的机器。

这种紧张关系正是研究员舒峰（Shufeng Kong）、张晓川（Xiaochuan Zhang）和刘彩华（Caihua Liu）最近发表的一篇立场论文的核心。他们认为，对于规则严苛且出错代价高昂的问题，人工智能必须停止尝试从零开始学习规则，而是应该将其学习能力与传统的规则检查引擎相结合。为了证明他们的观点，他们采用了流行的数独谜题作为案例。数独是一个完美的测试案例，因为验证一个解是否正确非常容易——你只需要观察行和列看数字是否重复——但从头开始求解却非常困难。研究人员发现，虽然现代人工智能模型可以近乎完美地解决简单的谜题，但当谜题变得稍微不同或更难时，它们就会崩溃。即使给予这些模型额外的思考时间并让其检查自己的工作，它们仍然会产生违反规则的解。相比之下，使用传统规则检查器来验证人工智能答案的系统，能以更少的样本实现完美的准确率。

研究人员证明了仅依赖统计学习对于这类问题来说是一个陷阱。他们展示了当一种神经网络（一种通过数据学习的AI类型）试图解决一个它从未见过的谜题时，它经常会产生一个看起来正确但包含隐藏错误的答案。这些错误不仅仅是微小的失误；它们是解决谜题所需逻辑的根本性违背。团队发现，仅仅给予人工智能更多的计算能力，或者要求它生成许多可能的答案并从中挑选最好的，并不能解决问题。人工智能可能会在平均水平上表现得更好，但它无法保证任何特定的单个答案是正确的。这是一个关键的区别。一个“通常正确”的系统与一个“可证明正确”的系统有着本质的不同。在调度、安全检查或代码生成等领域，一个单一的错误就可能导致灾难性的后果，使得“通常正确”的方法变得不可接受。

为了解决这个问题，作者提出了一种构建这些系统的新方法，称之为“双向集成”。他们建议不要让人工智能尝试做所有事情，而是将工作进行拆分。人工智能充当快速、直觉式的生成器，利用其模式识别能力快速提出候选方案。随后，该候选方案会被传递给一个严格的、遵循规则的验证器。这个验证器扮演着守门人的角色。如果方案通过了检查，则被接受；如果失败，验证器不仅会说“不”，还会明确指出错误所在，例如指出同一行中有两个数字是相同的。人工智能随后利用这一具体的反馈来调整其猜测并再次尝试。如果人工智能在尝试几次后仍无法解决问题，系统会将任务移交给传统的、虽慢但完美的求解器，以保证获得正确答案。这创造了一个安全网，既保留了人工智能的速度，又确保了基于规则系统的可靠性永远不会受到损害。

研究人员在包括生成计算机代码和解决复杂的车辆路径规划问题在内的几个困难领域测试了这种方法。在每种情况下，混合系统都优于单独运行的人工智能。例如，在生成代码时，人工智能本身可能会产生一个看起来不错但无法运行的程序。通过增加一个步骤，即在接受之前由编译器对代码进行实际测试，系统纠正了自己的错误，并实现了更高的成功率。同样，在车辆路径规划中，混合方法将不可能路径的比例从显著的百分比降低到了几乎为零。关键发现是，人工智能不需要学习逻辑规则本身；它只需要学习如何提出好的想法，而确保这些想法有效的重任则留给了符号引擎。

这项工作挑战了目前盛行的观点，即认为更大、更强大的人工智能模型最终将能够自行处理所有逻辑约束。作者认为，对于这类问题，再多的数据或计算能力也无法弥补统计猜测与逻辑确定性之间的鸿沟。他们指出，在受限环境下实现可靠人工智能的未来，不在于取代旧有的基于规则的方法，而在于使它们成为新学习方法的合作伙伴。通过让人工智能处理问题中杂乱、非结构化的部分，并将规则检查器用于最终验证，我们可以构建出既快速又值得信赖的系统。该论文最后呼吁科学界不要再接受将“通常正确”作为此类任务的成功指标，而是要要求系统能够证明其正确性，从而确保当我们依赖机器做决策时，这些决策不仅极有可能正确，而且是保证正确的。

技术摘要：神经约束推理中的确定性正确性需要符号集成

1. 问题陈述

本文探讨了神经求解器在约束满足问题（CSP）中的一个根本性局限：虽然它们在分布内（ID）数据上取得了极高的准确率，但在分布偏移（OOD）下仍会出现持续的约束违规，即便其报告了高置信度。作者认为，统计近似与逻辑满足在本质上是不同的。

核心问题在于“认证差距”（Certification Gap）。纯神经方法（包括大语言模型和可微求解器）是用连续概率来近似离散有效性。因此，它们无法提供实例级的正确性保证。在验证成本较低（例如数独为 $O(n^2)$ ）而求解难度较大（NP-困难）的硬约束领域，仅依赖学习会导致一种“有效性鸿沟”，这种鸿沟是增加测试时计算量也无法弥补的。

本文指出，当以下三个条件同时成立时——(i) 硬约束是可指定的，(ii) 验证成本相对于求解成本较低，且 (iii) 违规成本很高——神经约束推理必须优先考虑符号集成而非纯粹的学习。

2. 方法论与框架

2.1 范式分类学

作者将求解方法分为四种范式，以定位失效模式：

确定性算法：（如 Dancing Links、SAT 求解器）通过构造提供正确性，但缺乏处理非结构化输入（图像、文本）的灵活性。
元启发式优化：（如模拟退火）具有灵活性，但无法提供收敛保证，并可能陷入局部最优。
端到端神经学习：（如 SATNet、RRN）具有高 ID 准确率，但在 OOD 下表现出严重的性能退化。约束被视为软训练信号而非硬推理门控。
语言调节推理：（如带有思维链的 LLM）难以处理严格的全局约束；自回归生成是概率性的，且容易产生幻觉。

2.2 提议的解决方案：双向集成

本文倡导一种双向集成策略，而非单向生成或软正则化：

神经 $\to$ 符号： 神经方法通过处理非结构化感知（符号落地）和学习特定实例的启发式方法来引导搜索，从而增强符号求解器，提高其可扩展性和易用性。
符号 $\to$ 神经： 符号方法对神经输出进行认证以确保可靠性。这涉及一种控制反转，即符号验证器充当强制性的守门人，而非可选的辅助工具。

2.3 PVS 框架（提议者-验证者-求解器）

为了实现这一目标，作者提出了 PVS 框架，这是一种多智能体架构：

神经提议者 ( $P_\theta$ )： 一个统计模型（如 Transformer、GNN），根据输入 ( $x$ ) 生成候选解 ( $\hat{y}$ )。它负责高吞吐量的生成，但不提供正确性保证。
符号验证者 ( $V$ )： 一个确定性的多项式时间函数，用于检查 $\hat{y}$ 是否满足约束 ( $C$ )。关键在于，它返回的是结构化诊断信息 ( $D_t$ )（例如，具体的违规约束），而非简单的布尔值。
符号求解器 ( $S$ )： 一个完备且可靠的求解器（如 Tdoku、ASP），作为兜底机制。

智能体控制循环：
系统运行在一个精炼循环中（算法 1）：

提议者生成一个候选解。
验证者对其进行检查。如果有效，系统返回结果（快速路径）。
如果无效，验证者的诊断信息会被反馈到提议者的调节输入中（通过 CONSTRUCTFEEDBACK），以精炼下一个候选解。
如果循环在耗尽预算后仍未找到有效解，则系统回退到符号求解器（安全路径）。

关键理论保证：
该框架确保了不对称信任。神经组件被视为不可靠的，但系统实现了可证明的 0% 违规率，因为没有任何输出会在通过符号检查（通过验证者或回退求解器）之前到达用户手中。

3. 主要贡献

全面的分类学： 对数独求解方法进行了跨确定性、元启发式、神经和语言调节范式的分类，识别了基于学习的方法中的“认证差距”。
三个可证伪的经验性主张：
- 主张 1（OOD 违规）： 最先进的纯神经方法在分布偏移下表现出残余的约束违规，且测试时计算无法消除这些违规（例如，AKOrN 的违规率停留在约 10.5%）。
- 主张 2（计算 $\neq$ 证书）： 扩展计算量会带来收益递减，并且无法提供区分单个输出正确与否的机制；高置信度并非证书。
- 主张 3（集成效率）： 神经符号方法实现了数量级的样本效率提升（例如，NeurASP 使用 25 个样本，而 RRN 需要 216,000 个），因为它将约束满足从假设空间中移除。
双向集成策略： 阐述了神经方法如何改进符号求解器（感知、启发式）以及符号方法如何必须认证神经输出。
PVS 框架： 一个具体的多智能体架构，使上述策略得以落地，从而兼顾计算效率与可证明的正确性。

4. 结果与证据

论文通过经验数据和理论论证支持其立场：

性能退化： 在数独基准测试中，纯神经模型如 SATNet 的准确率从 98.3% 的 ID 准确率下降到 3.2% 的 OOD 准确率。即使是使用大量测试时计算（128 次 Kuramoto 步长，4,096 个样本）的高级模型 AKOrN，也无法达到 100% 的准确率，而是停留在约 89.5%。
样本效率： 神经符号系统（NeurASP）仅需 25 个训练样本即可实现 100% 的约束满足，而纯神经方法需要数量级更多的训练数据，且在 OOD 偏移下仍然失败。
跨领域泛化： PVS 模式被证明在其他高风险领域同样有效：
- 代码生成： Reflexion 通过编译器/测试反馈，将 GPT-4 的 pass@1 从 80% 提升至 91%。
- 车辆路径规划： CaR 在 10 步精炼内将不可行路径从 38.22% 降低至 0.03%。
- 定理证明： BFS-Prover-V2 通过在每个节点都使用 Lean 内核作为强制验证器，在 miniF2F 上达到了 95.08%。

5. 意义与定位

本文的核心意义在于重新定义了受限领域中可靠 AI 的要求。它认为，“通常正确”（统计近似）在认识论上不同于“证明正确”（逻辑满足）。

作者将符号集成定位为一种必要的架构不变性，而非竞争性的范式，特别是在约束违规代价高昂的领域。通过实施控制反转——即让符号验证器成为强制性的守门人——PVS 框架架起了神经感知的灵活性与符号逻辑的严密性之间的桥梁。

论文最后呼吁社区在报告准确率的同时，也要报告违规率，并采用认证元数据。它设定了一个严格的可证伪标准：只有当一个纯神经系统（在没有调用符号工具或架构强制的情况下）在预先注册的 OOD 基准测试中实现 <1% 的违规率时，该论点才会被推翻。在出现此类突破之前，作者主张构建可证明正确的系统。