Position: Certified Correctness in Neural Constraint Reasoning Requires Symbolic Integration

Shufeng Kong; Xiaochuan Zhang; Caihua Liu

Source-linked AI summary

Position: Certified Correctness in Neural Constraint Reasoning Requires Symbolic Integration

Shufeng Kong, Xiaochuan Zhang, Caihua Liu

arXiv:2608.14569v1Jun 2, 2026cs.AI

TL;DR

Neural CSP solvers can lose constraint reliability under distribution shifts despite strong in-distribution accuracy. This position paper surveys four solving paradigms and advocates bidirectional neural-symbolic integration, showing that symbolic verification can provide 100% certification while retaining a fast neural path for 89.5% of queries.

Problem
Neural constraint solvers lack reliable instance-level certification under distribution shifts despite high in-distribution accuracy, leaving rigorous constraint enforcement unresolved.
Method
The paper surveys four Sudoku-solving paradigms and proposes bidirectional integration in which neural methods generate or guide solutions while symbolic methods verify outputs.
Results
100% certification is achieved while 89.5% of queries use the fast neural path and 10.5% trigger symbolic solving.
Takeaways & Limitations
When constraints are hard, verification is cheap, and violations are costly, symbolic integration offers a route to trustworthy neural constraint reasoning.
Takeaways & Limitations
The position is explicitly falsifiable only against a purely neural system achieving below 1% violations on a preregistered out-of-distribution benchmark without symbolic verification or architectural constraint enforcement.

Abstract

from arXiv · show

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.

1. Introduction

The paper argues that discrete constraint reasoning should prioritize symbolic integration when constraints are hard, verification is inexpensive, and violations are costly. Sudoku provides a controlled testbed because solutions are easy to verify but potentially hard to find, exposing certification gaps in neural-only methods.

Position: Symbolic integration should be prioritized when hard constraints are specifiable, verification is cheap relative to solving, and violations are costly.The proposed integration is bidirectional: neural methods improve symbolic solvers’ accessibility and scalability, while symbolic methods certify neural outputs.
Contributions: The paper surveys deterministic, metaheuristic, learning-based, and language-conditioned methods to show that certification gaps persist across architectures.Its comparison emphasizes polynomial-time verification for CSPs versus NP-hard solving, enabling stronger certification claims.
Operational Definition: Purely neural systems use no external symbolic computation or architectural constraint encoding, so their constraint satisfaction is statistical rather than certified.The scope targets discrete combinatorial constraints with global structure, such as Sudoku’s all-different constraints.
Why Sudoku?: Sudoku combines NP-completeness with O(n^2) verification and potentially exponential solving, creating an “easy verification, hard solving” testbed.Varying clue count from ID [31−42] to OOD [17−34] while holding all 324 constraints fixed isolates neural approximation failures.
Falsifiability: >10% violation rates under distribution shift are claimed for neural-only methods without explicit certification.The thesis is defined as refuted if such a system achieves a <1% violation rate on a preregistered OOD benchmark without symbolic inference-time checks or architectural enforcement.

2. A Taxonomy of Constraint Satisfaction Paradigms

The taxonomy evaluates deterministic algorithms, metaheuristic optimization, end-to-end neural learning, and language-conditioned reasoning by flexibility, efficiency, and certified correctness. It identifies a certification gap between fast, reliable but rigid symbolic methods and flexible neural or LLM methods that lack guarantees.

Taxonomy: The survey categorizes Sudoku solvers into four paradigms—deterministic algorithms, metaheuristic optimization, end-to-end neural learning, and language-conditioned reasoning—and evaluates flexibility, efficiency, and certified correctness.These criteria expose the trade-offs summarized as a “Certification Gap.”
Deterministic algorithms: Deterministic solvers provide correctness by construction and Tdoku reaches ∼2.7 µs/puzzle, but these methods cannot consume unstructured inputs such as images or natural language.DLX, SAT solvers, and constraint propagation are presented as the correctness gold standard.
Metaheuristic optimization: 30% success rates near the critical hardness threshold on order-5 Sudokus illustrate that metaheuristics can be flexible yet lack convergence guarantees and may stagnate in local optima.The reported setting is 25 × 25 Sudoku under Lewis (2007).
End-to-end neural learning: SATNet reaches 98.3% in-distribution accuracy but collapses to 3.2% under the AKOrN distribution shift, exposing pure learning’s robustness and certification limitations.These models treat logical necessities as statistical regularities rather than enforcing them symbolically.
Language-conditioned reasoning: GPT-5 achieves only 33% accuracy on Sudoku-Bench’s challenge 100 set, while LLM tool use can restore correctness only when the symbolic tool is the source of truth.Autoregressive generation can produce high-confidence constraint violations because it is probabilistic.
Certification gap: The survey concludes that bidirectional neuro-symbolic integration is necessary: neural models provide flexible perception and heuristics, while symbolic engines retain certification.NeurASP illustrates this division by achieving 100% constraint satisfaction given perceived inputs through an ASP backend.

3. Empirical Evidence: The Limits of Statistical Learning

Neural-only constraint solvers can appear nearly perfect in-distribution but retain unverifiable violations and degrade under distribution shift, even with increased test-time computation. Neuro-symbolic methods close this certification and efficiency gap by delegating constraint satisfaction to symbolic solvers while neural components handle perception.

Claim 1 (OOD Violations): Neural-only methods exhibit residual constraint violations under distribution shift that further test-time compute cannot eliminate.In-distribution near-perfect performance does not transfer reliably when the difficulty distribution shifts.
Claim 1 (OOD Violations): NeurASP maintains 0% violation rate by delegating constraint satisfaction to a symbolic solver.Its neural component performs digit recognition, while the ASP solver guarantees constraint satisfaction for perceived inputs.
Claim 2 (Compute ≠ Certificates): A 5× increase in ConsFormer compute yields only ∼12 percentage points of improvement, while AKOrN still fails on ∼10.5% of instances.AKOrN uses 4,096 forward passes per puzzle with 128 internal Kuramoto iteration steps; the neural approach provides no correctness guarantee.
Claim 2 (Compute ≠ Certificates): Even 99.9% expected accuracy cannot certify whether a specific output is correct, whereas symbolic verification provides a binary valid/invalid signal.Test-time scaling improves aggregate accuracy but does not distinguish correct from incorrect individual outputs.
Claim 3 (Integration Efficiency): NeurASP achieves 100% constraint satisfaction with 25 training examples, whereas RRN requires 216,000 examples for comparable in-distribution performance.This orders-of-magnitude gap follows from removing constraint satisfaction from the learned hypothesis space and leaving the neural component primarily responsible for perception.

4. Strategies for Bidirectional Integration

Bidirectional integration assigns neural methods to efficient perception and search while symbolic systems provide rigorous verification. The paper’s central architectural requirement is that every output pass a sound symbolic check, enabling certified correctness without discarding neural efficiency.

Bidirectional Integration: Bidirectional integration lets neural networks generate solutions efficiently while symbolic systems verify them rigorously.This division follows the asymmetry between hard solving and cheap verification for NP-complete problems.
Neural Perception (Symbol Grounding): Neural encoders ground raw images or text into discrete symbols that symbolic solvers can process under hard constraints.NeurASP maps digit images to probability distributions with a CNN while an ASP solver enforces Sudoku constraints.
Neural Heuristics (Learned Search): Learned instance-specific heuristics can prune search and accelerate solving while preserving symbolic soundness under distribution shift.Graph-Q-SAT and AlphaGo’s MCTS are cited as examples of learned priors that speed solving by orders of magnitude.
Verification-Interposed Execution: External verification is foundational because autoregressive models cannot autonomously self-verify without circularly reusing the heuristics that produced their outputs.The paper formalizes this approach as Verification-Interposed Execution.
Verification-Interposed Execution: 89.5% OOD accuracy routes 89.5% of queries through the neural path, while 10.5% trigger the solver, ensuring 100% certification.For Sudoku, verification takes less than 1µs (O(n^2)) versus approximately 10ms for neural inference.
Certification Invariant: The Certification Invariant requires every user-visible output to pass a symbolic constraint check, distinguishing provably correct systems from usually correct ones.The paper’s novelty is making the symbolic verifier a mandatory system-level gatekeeper rather than an optional aid.

C. Inversion of Control

The section presents PVS as enforcing inversion of control through a verifier that gates every output and prevents the proposer from bypassing or overriding it. Proposition 5.1 provides a structural, rather than probabilistic, zero-violation guarantee.

C. Inversion of Control: Every output traverses verifier V, which serves as a system-level gatekeeper.This enforcement is identified as a structural guarantee under Proposition 5.1.
C. Inversion of Control: PVS architecturally precludes the proposer from bypassing or overriding the verifier.The verifier retains control even when the model would otherwise discard a correct symbolic result.
C. Inversion of Control: Proposition 5.1 establishes a structural rather than probabilistic zero-violation guarantee.The section lists PVS alongside ICF and BFS-Prover-V2.

5. The Proposer-Verifier-Solver (PVS) Framework

The PVS framework combines a neural proposer with symbolic verification and fallback solving in an agentic refinement loop. It provides certified correctness by accepting only verified candidates or returning a result from a sound, complete solver.

Framework architecture: PVS models constraint satisfaction as a collaborative control loop between an efficiency-oriented neural agent and a correctness-oriented symbolic environment.The neural component generates candidates, while symbolic components enforce correctness.
Framework architecture: The framework comprises a neural proposer, a polynomial-time symbolic verifier producing localized diagnostics, and a complete symbolic solver as fallback.The proposer offers no correctness guarantees; the verifier checks candidate satisfaction and the solver provides the safety net.
Certification guarantee: PVS guarantees that every returned output satisfies the constraints or is a verified proof of unsatisfiability.The fast path returns only verifier-certified candidates, while the safe path falls back to the sound, complete solver.
Agentic control loop: Verifier diagnostics are injected into the proposer’s conditioning input for parameter-free refinement, after which the symbolic solver handles unresolved cases.Only the conditioning context changes across iterations; the proposer parameters θ remain fixed.
Certification guarantee: The framework’s violation rate is structurally 0%, independent of the neural proposer’s reliability.Both exit paths require symbolic certification: verification of the neural candidate or fallback to the sound, complete solver.

6. Alternative Views

The paper argues that scaling, tool use, and neural verification do not replace symbolic certification because strict constraints require sound guarantees, reliable interfaces, and diagnostic handling of infeasibility. It further maintains that symbolic integration remains useful beyond idealized Sudoku through partial certification, tiered verification, and sound kernels.

Scaling and emergence: 99.99% satisfaction from scaling would still be inferior to a symbolic verifier running in < 1µs with a fallback solver that achieves 100% correctness.The economic case favors integration when verification is inexpensive relative to inference.
External tools: Tool-augmented LLMs count as symbolic integration, but reliable tool invocation and input formulation remain substantial gaps in current implementations.The response distinguishes merely calling tools from calling the correct tools with correct inputs.
Beyond idealized Sudoku: Symbolic integration extends beyond exact Sudoku by enforcing known constraints, computing exact soft-constraint penalties, and returning UNSAT proofs or Minimal Unsatisfiable Cores for infeasible instances.These mechanisms provide partial certification, principled loss signals, and diagnostic value in messy environments.
Verification cost: For expensive verification, the position relies on asymptotic and amortized advantages, using multi-tier checks before bounded model checking and full SMT.The paper states that verification is asymptotically cheaper than exhaustive solving for NP problems and that PVS retains value beyond NP through cheap falsification and bounded partial verification.
Autoformalization: Autoformalization does not displace certification when its output feeds a sound symbolic kernel, as in systems where Lean certifies every accepted step.The paper identifies the neural proposer and autoformalizer as components of PVS while retaining the symbolic verifier as gatekeeper.

7. Conclusion

The conclusion defends symbolic integration as necessary for certified neural constraint reasoning when constraints are hard, verification is cheap, and violations are costly. It calls for benchmark and system designs that expose violation rates and instance-level certification status.

Conclusion: When hard constraints are explicit, verification is cheap, and violations are costly, neural constraint reasoning must prioritize symbolic integration over pure learning.The paper frames this as a falsifiable position.
Conclusion: Neural-only solvers exhibit persistent OOD violations that further test-time compute does not eliminate, whereas neuro-symbolic systems achieve orders-of-magnitude gains in sample efficiency.The conclusion distinguishes “usually right” from “provably right” and delegates logic to solvers.
Call to Action: Benchmark designers should report Violation Rate alongside accuracy and provide per-instance certification metadata for verification, symbolic fallback, or uncertified outputs.The call to action also treats certification status as meaningful disclosure for CSP reasoning claims.

A. Taxonomy of Sudoku Solving Methods

The section organizes Sudoku-solving methods into four paradigms and presents a verification procedure based on checking rows, columns, and 3×3 boxes against the expected digit set.

Taxonomy: Sudoku-solving methods are organized into a comprehensive taxonomy spanning four paradigms.Figure 3 provides the taxonomy.
Verification: The verification procedure sets n = 9 and defines the expected digits as {1, 2, 3, 4, 5, 6, 7, 8, 9}.The procedure uses this expected set when checking Sudoku structures.
Verification: The verifier checks every row, column, and 3×3 box, returning FALSE when a structure differs from the expected set.The listed procedure iterates over rows, columns, and boxes and compares each against the expected digits.

B. Verification Algorithm

The section presents verification as a necessary step for all solving paradigms and describes checking whether a filled 9×9 grid satisfies Sudoku constraints in O(n^2) time.

Verification Algorithm: All solving paradigms require verifying candidate solutions against Sudoku constraints.The procedure checks whether a filled 9×9 grid is valid.
Verification Algorithm: O(n^2) time is required to verify an n×n Sudoku grid.The stated complexity applies to the verification algorithm.

C. Complexity Summary … E.1. Why Neural Networks Cannot Guarantee Constraint Satisfaction

The paper summarizes computational complexity, extends constraint-based reasoning to costly real-world domains, and argues that neural predictions cannot guarantee constraint satisfaction without architectural constraints or symbolic verification. These limitations motivate symbolic certification when violations are costly and constraints are cheap to verify.

C. Complexity Summary: Table 4 provides a high-level summary of computational complexity.
D. Additional Application Domains: Constraint-based reasoning generalizes beyond Sudoku whenever constraints are specifiable and checkable.
D. Additional Application Domains: $1–2.6B per failed candidate is the reported cost of violating drug-discovery constraints such as valence rules, PAINS filters, and Lipinski constraints.
D. Additional Application Domains: Flight-scheduling violations of duty limits, rest requirements, or maintenance windows can trigger large passenger disruption costs.
D. Additional Application Domains: Circuit-design violations involving timing, power, or design-rule checks can cost millions per respin.
E. Theoretical Background: In high-dimensional input spaces, neural predictions on test data almost always involve extrapolation beyond the training distribution.
E. Theoretical Background: For any computable function f, there exist inputs where a trained model M produces M(x) ≠ f(x) with non-negligible probability.
E.1. Why Neural Networks Cannot Guarantee Constraint Satisfaction: Unconstrained neural networks learn statistical regularities rather than logical necessities, so guarantees require architectural constraints or explicit symbolic verification/solving.