立场：神经约束推理中的经认证正确性需要符号集成

# 立场：神经约束推理中确保正确性需融合符号方法
来源：https://arxiv.org/html/2608.14569
###### 摘要

用于约束满足问题的神经求解器在分布内准确率上已取得显著成就，但仍存在根本性局限：即使模型报告高置信度，分布偏移仍会导致持续违反约束。本立场论文主张，当存在硬约束且验证成本相对较低时，神经约束推理必须优先考虑符号集成而非纯学习。我们选择数独作为代表性NP完全问题测试平台，因其在易验证与难求解之间呈现尖锐的非对称性：检查候选解仅需多项式时间O(n²)，而寻找解可能需要指数级搜索。通过对涵盖确定性算法、元启发式优化、基于学习的方法及语言条件推理的求解方法进行综合考察，我们证明：未经实例级认证的纯神经方法无法实现符号与神经-符号方法所具备的可证明正确性。我们倡导双向集成：神经方法通过学习启发式规则和将感知转化为符号来增强符号求解器，而符号方法则验证神经输出以确保其可靠性。为落实此立场，我们提出一个多智能体认证推理框架，展示该集成如何同时实现计算效率与可证明正确性。

约束满足，神经-符号AI，验证，分布外泛化

## 1 引言

现代机器学习的核心争议在于：大规模统计学习在多大程度上能替代显式符号推理。虽然神经求解器在约束满足问题上已取得卓越的分布内准确率，但往往缺乏严格约束执行所需的鲁棒性。以数独为例：SATNet在分布内基准测试中达到98.3%的测试准确率（Wang等人，2019），但当给定数字数量从31-42个变为17-34个（分布外）时，准确率暴跌至3.2%（Miyato等人，2025），降幅达95.1个百分点。这并非个例。即使是领先的纯神经求解器（未经显式认证）AKOrN（Miyato等人，2025），尽管使用大量测试时计算资源（128个Kuramoto步长和4096个样本进行基于能量的投票），其OOD准确率也仅达89.5±2.5%。相比之下，神经-符号系统NeurASP仅使用25个训练样例即实现100%约束满足（Yang等人，2020），所需样本量比RRN（Palm等人，2018）等纯神经方法少几个数量级。这些实证差异表明，统计近似与逻辑满足存在根本区别，这促成了本文的核心立场。

立场：当满足以下条件时，神经约束推理应优先考虑符号集成而非纯学习：(i) 存在可规范化的硬约束；(ii) 验证成本相对于求解成本较低；(iii) 违约成本高昂。

本文聚焦于满足上述三个条件的领域，包括数独及调度、配置、合规检查等众多工业CSP问题。在这些场景中，低成本验证（如数独的O(n²)）能有效认证高成本生成的解决方案。我们倡导双向集成：神经方法通过提升可访问性和可扩展性增强符号求解器，而符号方法通过认证神经输出确保可信度。

与先前工作的关系：我们的立场与Kambhampati等人（2024）共享神经系统需要外部符号验证的见解，但存在根本差异。首先，我们聚焦于约束满足问题，其中多项式时间验证（如数独的O(n²)）与NP难求解形成鲜明对比，比规划领域支持更强的认证主张。其次，我们考察四种范式（确定性、元启发式、基于学习、语言条件），证明认证差距在根本不同的架构中持续存在。第三，LLM-Modulo将神经组件视为由符号批评者单向验证的生成器，而我们倡导双向集成：神经方法增强符号求解器（通过学习启发式和感知），符号方法认证神经输出——这种分工利用了两者的优势。

操作性定义：为明确范围，我们采用区分约束结构注入位置及其产出保证的分类法。将系统分为三类：(i) 纯神经（数据隐式）：系统在推理时(a)不调用外部符号计算（如SAT/SMT/ASP求解器或约束检查器），且(b)未通过架构设计编码约束。此类模型的约束满足是统计性而非认证性的。(ii) 架构约束：通过网络内的参数化、投影或归一化层设计来强制约束的系统。(iii) 符号集成：通过推理时显式符号验证或求解来强制约束语义的系统，支持实例级认证。

范围说明：架构与符号强制的区分。对于连续约束（通过Softmax的概率单纯形；通过可微分QP的线性不等式），架构强制已足够。我们的立场针对具有全局结构的离散组合约束（如数独中的“全异”约束、TSP中的子回路消除约束）的互补领域。此处端到端神经求解器依赖训练时的连续松弛（如SATNet对MAXSAT的可微分SDP）：在分布内提供有效软引导，但推理时的离散舍入重新引入违约风险，仅靠架构无法弥合此差距，除非解决P vs. NP问题。架构强制与符号强制是互补而非竞争关系。

为何选择数独？受控的“果蝇”测试平台。数独是NP完全问题，却呈现尖锐的“易验证、难求解”非对称性：验证需O(n²)，寻找解可能需指数搜索。更重要的是，它是受控测试平台：仅改变提示数量（ID[31-42]→OOD[17-34]）而保持全部324个约束固定，我们可隔离完全归因于神经近似的故障模式，排除任务变化或约束集改变的干扰。这种控制在代码生成、调度等多变量同时变化的复杂领域中难以实现。本立场适用于满足(i)-(iii)的任何领域；第5.4节（https://arxiv.org/html/2608.14569#S5.SS4）确认其在代码生成、困难车辆路径规划和自动定理证明中的适用性。

贡献：本文有四项主要贡献。第一，提供涵盖四种范式的数独求解方法综合分类：确定性算法、元启发式、神经网络和大型语言模型（第2节）。第二，提出三个可证伪的经验主张（第3节）：主张3.1（https://arxiv.org/html/2608.14569#S3.SS1）确立未经显式认证的纯神经方法在分布偏移下违约率>10%；主张3.2（https://arxiv.org/html/2608.14569#S3.SS2）证明测试时缩放收益递减且无法区分正确输出；主张3.3（https://arxiv.org/html/2608.14569#S3.SS3）表明神经-符号方法实现显著样本效率提升。第三，阐述双向集成策略，展示神经方法如何通过感知和启发式增强符号求解器，以及符号方法如何必须认证神经输出以确保可信度（第4节）。第四，提出提案者-验证者-求解器（PVS）框架，一个具体的多智能体架构，通过实施这些策略实现计算效率与可证明正确性（第5节）。

可证伪性：为确保科学严谨性，定义严格证伪标准：若纯神经（数据隐式）系统在预注册OOD基准上实现<1%违约率，且(i)推理时不调用符号求解器或显式约束检查器，(ii)未通过架构构造强制任务定义约束C，则本论点被证伪。

利益冲突披露：作者声明无经济利益冲突：未评估任何商业产品，作者均未受雇于生产文中比较系统的机构。

## 2 约束满足范式分类

为定位现代求解器的精确故障模式，将数独求解方法分为四种范式：确定性算法、元启发式优化、端到端神经学习和语言条件推理。根据我们立场的三个核心标准评估每种范式：灵活性（处理非结构化输入）、效率（推理延迟）和认证正确性（保证满足）。表1（https://arxiv.org/html/2608.14569#S2.T1）总结这些权衡，指出现代基于学习方法的关键“认证差距”。

表1：认证差距。确定性方法保证正确性但缺乏处理原始感知输入的灵活性。神经与LLM方法提供灵活性但牺牲认证，导致OOD失败。神经-符号集成（提倡立场）弥合此差距。范式|输入模态|典型速度|已认证？|失败模式
---|---|---|---|---
确定性|结构化|微秒级|是|输入要求僵化
元启发式|结构化|毫秒-秒级|否|局部最优收敛
端到端神经|原始/结构化|毫秒-秒级|否|OOD性能下降
语言条件|文本/多模态|秒-分钟级|否|幻觉推理

### 2.1 确定性算法：认证性基准

确定性方法——包括舞蹈链（DLX）、SAT求解器和约束传播——代表正确性的黄金标准。

现代实现如Tdoku利用SIMD优化（AVX-512）实现微秒级求解时间（约2.7微秒/题）。关键在于，这些方法通过构造保证正确性：除非可证明满足所有约束，否则不返回结果。其局限性不在于可靠性，而在于僵化性；无法处理真实世界AI部署中典型的非结构化输入（图像、自然语言）。

### 2.2 元启发式优化：无保证搜索

元启发式——如模拟退火和遗传算法——将约束满足重构为能量最小化问题。虽比精确求解器更灵活，但存在相变问题。Lewis（2007）表明，在五阶数独（25×25）中，临界硬度阈值附近成功率可降至30%。与确定性方法不同，元启发式不保证收敛；可能停滞在约束仍被违反的局部最优中，不适用于安全关键认证。

### 2.3 端到端神经学习：统计陷阱

此范式试图从数据中学习约束满足，将逻辑必要性视为统计规律。架构包括循环关系网络（RRN）和可微分求解器如SATNet。虽然这些模型在分布内达到高准确率（如SATNet的98.3%），但根本缺乏鲁棒性。分布偏移下（AKOrN数据划分），SATNet准确率暴跌至3.2%。即使集成振荡器动力学增强稳定性的AKOrN，也依赖基于能量的投票实现89.5% OOD准确率。由于约束是软训练信号而非硬推理门，这些方法必然产生逻辑无效的“近似正确”解。

神经-符号例外（控制基准）：NeurASP等系统通过将求解步骤委托给符号ASP后端而偏离此模式。职责隔离使NeurASP在给定感知输入时实现100%约束满足。故障模式从*推理*（解题）转向*感知*（读取数字），证明集成能在纯学习失败处保留认证性。我们将NeurASP视为本文的*控制基准*：其神经组件仅执行感知（将数字图像映射为标签分布），ASP求解器构建完整解。神经网络不生成候选解；因此系统能隔离显式符号规范的效应与神经搜索的贡献。第5节介绍的提案者-验证者-求解器框架位于谱系另一端：神经网络主动提案候选解，符号组件进行认证。

### 2.4 语言条件推理：逻辑假象

大型语言模型（LLM）代表最新前沿，试图通过逐词推理（思维链）解决CSP。尽管“系统2”推理模型（如OpenAI的o1）有所改进，纯LLM仍难以处理严格全局约束。在Sudoku-Bench上，GPT-5在challenge_100集仅达33%准确率。

核心问题在于自回归生成具有概率性；LLM可能以高“置信度”推理至约束违反。但当LLM增强工具使用（LLM-Modulo），实际成为神经-符号控制器时，可重获正确性——