Position: Certified Correctness in Neural Constraint Reasoning Requires Symbolic Integration
06:00 · August 18, 2026 · arXiv cs.AI RSS
Neural solvers for constraint satisfaction problems have achieved remarkable in-distribution accuracy, yet they suffer from a fundamental limitation persistent constraint violations occur under distribution shifts even when the model reports high confidence. This position paper argues that when hard constraints exist and the cost of verification is relatively low, neural constraint reasoning must prioritize symbolic integration over pure learning. We justify our focus on Sudoku as a representative NP-complete testbed because it exhibits a sharp asymmetry between easy verification and hard solving: checking a candidate solution requires only polynomial time $O(n^{2})$, while finding a solution may require exponential search. Through a comprehensive survey of solving methods spanning deterministic algorithms, metaheuristic optimization, learning-based approaches, and language-conditioned reasoning, we demonstrate that neural-only methods without instance-level certification fail to achieve the provable correctness that symbolic and neuro-symbolic approaches provide. We advocate for a bidirectional integration in which neural methods enhance symbolic solvers by learning heuristics and converting percepts into symbols, while symbolic methods verify neural outputs to ensure their reliability. To operationalize this position, we propose a multi-agent certified reasoning framework that demonstrates how this integration can achieve both computational efficiency and provable correctness.
Summary
This position paper contends that neural solvers for constraint satisfaction problems remain fundamentally limited when hard constraints must hold under distribution shift. Even when models report high confidence, out-of-distribution inputs produce persistent violations because satisfaction is learned statistically rather than enforced logically. The authors therefore argue that, whenever verification is inexpensive relative to search and violation costs are high, neural constraint reasoning should integrate symbolic methods rather than rely on scaling alone.
Sudoku serves as the central testbed precisely because it isolates this limitation. The problem is NP-complete, yet solution checking requires only quadratic time while finding a solution can demand exponential effort. Shifting the number of clues from the training range of 31–42 to the out-of-distribution range of 17–34 causes purely neural systems such as SATNet to collapse from 98.3 % to 3.2 % accuracy. Even recent architectures that invest substantial test-time compute, such as AKOrN, still exhibit roughly 10 % violations. In contrast, neuro-symbolic systems such as NeurASP reach 100 % constraint satisfaction with far fewer examples.
The paper surveys four paradigms—deterministic algorithms, metaheuristics, end-to-end neural networks, and language-conditioned models—and identifies a persistent certification gap: only approaches that invoke explicit symbolic verification or architectural enforcement at inference time can guarantee instance-level correctness. It therefore advocates bidirectional integration. Neural components supply perception and learned heuristics that improve the scalability of symbolic solvers, while symbolic components certify neural proposals and thereby guarantee reliability.
To make this integration concrete, the authors introduce the Proposer-Verifier-Solver framework, a multi-agent architecture in which neural modules generate candidate solutions or heuristics, symbolic verifiers certify constraint satisfaction, and dedicated solvers refine feasible candidates. The same pattern is shown to apply to code generation and vehicle routing, domains that likewise combine cheap verification with expensive combinatorial search. The central claim is falsifiable: any purely neural system that achieves sub-1 % violation rates on a preregistered out-of-distribution benchmark without symbolic certification would refute the position.
Why it matters
The paper's focus on certified correctness and neuro-symbolic AI directly aligns with the EU AI Act's demand for transparent and reliable AI systems. Furthermore, its application to constraint satisfaction problems like vehicle routing and scheduling is highly relevant to the Netherlands' strong logistics and supply chain sectors.
