立场论文：神经约束推理需结合符号方法方可保证可证明正确性

arXiv 上发表的一篇立场论文提出：在存在硬约束且验证成本相对低廉的场景下，神经约束推理必须将符号集成置于纯学习之上，以实现可证明的正确性。论文围绕数独这一典型的 NP 完全测试问题展开论述，指出神经求解器虽在分布内准确率表现出色，但在分布偏移下即使置信度高仍会出现持续性的约束违反。

为什么选择数独作为测试平台

论文将数独作为代表性 NP 完全测试集，原因在于其存在显著的「易验证、难求解」不对称性：检查一个候选解仅需多项式时间 O(n²)，而求解本身可能需要指数级搜索。这一特性使得数独成为检验「可证明正确性」的天然基准——任何方法不仅要给出解，还要能被独立验证。

对现有求解方法的系统梳理

论文对约束满足问题的求解方法进行了较为全面的综述，涵盖以下几条主线：

• 确定性算法（如回溯搜索、约束传播）
• 元启发式优化（如遗传算法、局部搜索）
• 基于学习的方法（如纯神经网络求解器）
• 语言条件推理（利用 LLM 进行约束求解）

论文的核心论点是：缺乏实例级验证（instance-level certification）的纯神经方法，无法提供符号与神经-符号方法所能保证的可证明正确性。

倡导双向集成

论文主张神经方法与符号方法应进行双向耦合，而非单向替代：

• 神经方法增强符号求解器：学习启发式策略，将感知输入转换为符号表示。
• 符号方法验证神经输出：为神经预测提供形式化的正确性保证。

走向可操作的多智能体框架

为落实上述立场，论文提出了一个多智能体可认证推理框架（multi-agent certified reasoning framework），展示了如何通过上述双向集成同时获得计算效率与可证明正确性。该框架将神经感知、符号推理与验证模块分别交由不同智能体协同完成。

总体而言，这是一篇立场性论文，强调在安全攸关或约束严格的场景中，神经 AI 不应脱离符号验证而单独部署，相关思路对神经-符号 AI 与可验证机器学习方向具有参考意义。