Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.37490

CPUNeSy: Controlling Model Writes for Reliable Neuro-Symbolic Reasoning

Zeyan Li·Siyuan Qiu·Shuai Zhao·Jianfeng Xu
View original source ↗Read source document ↗Export metadata ↓

Abstract

LLMs excel at recalling statistical patterns but degrade sharply when answers must be derived, especially on multi-hop chains. Delegating derivation to deterministic symbolic executors shifts reliability to whether model-generated premises are source-supported. We introduce CPUNeSy, a serving architecture that controls model writes to symbolic state via a task-defined predicate interface and certificate gate, abstaining when grounding passes disagree. Component analysis isolates deterministic execution, restricted grounding, agreement, and source rechecking. Experiments show deterministic execution drives most accuracy recovery on derivation-heavy tasks; controlled writes mainly improve selective reliability by withholding unsupported or inconsistent answers, at a coverage cost. On multi-hop tests in law and formal math, deterministic execution recovers most of the gap over chain-of-thought and retrieval baselines, with full-pool gains up to 35.0 points. Certification is selective-serving control, not accuracy mechanism: with grounding traces fixed on ContractNLI, source rechecking removes a quarter of DeepSeek's wrong answers surviving two-vote agreement, at measurable coverage cost. When abstention is costly, routing withheld cases to an uncertified same-model fallback raises full-pool accuracy on MedCalc-Bench Verified by 13.9 and 4.9 points for Seed and DeepSeek; these gains are not from the certified channel. On LeanDojo Benchmark 4, kernel-restricted pools match BM25 recall@15 (89.3%). Gains depend on the grounder's error regime: bias-dominated grounders benefit less, consistent with our voting bound. Certificates guarantee derivational validity relative to admitted premises; semantic faithfulness to natural-language sources remains conditional on the source checker, and prospective validation is future work.

Explore related subjects

cs.SC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Zeyan Li, Siyuan Qiu, Shuai Zhao, Jianfeng Xu. 2026-09-28. CPUNeSy: Controlling Model Writes for Reliable Neuro-Symbolic Reasoning. https://arxiv.org/abs/2609.37490

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Novel Approach to the Initial Value Problem with a complete validated algorithm

We consider the first order autonomous differential equation (ODE) ${\bf x}'={\bf f}({\bf x})$ where ${\bf f}: {\mathbb R}^n\to{\mathbb R}^n$ is locally Lipschitz. For ${\bf x}_0\in{\mathbb R}^n$ and $h>0$, the initial value problem (IVP) for $({\bf f},{\bf x}_0,h)$ is to determine if there is a unique solution, i.e., a function ${\bf x}:[0,h]\to{\mathbb R}^n$ that satisfies the ODE with ${\bf x}(0)={\bf x}_0$. Write ${\bf x} ={\tt IVP}_{\bf f}({\bf x}_0,h)$ for this unique solution. We pose a corresponding computational problem, called the End Enclosure Problem: given $({\bf f},B_0,h,\varepsilon_0)$ where $B_0\subseteq{\mathbb R}^n$ is a box and $\varepsilon_0>0$, to compute a pair of non-empty boxes $(\underline{B}_0,B_1)$ such that $\underline{B}_0\subseteq B_0$, width of $B_1$ is $<\varepsilon_0$, and for all ${\bf x}_0\in \underline{B}_0$, ${\bf x}={\tt IVP}_{\bf f}({\bf x}_0,h)$ exists and ${\bf x}(h)\in B_1$. We provide a complete validated algorithm for this problem. Under the assumption (promise) that for all ${\bf x}_0\in B_0$, ${\tt IVP}_{\bf f}({\bf x}_0,h)$ exists, we prove the halting of our algorithm. This is the first halting algorithm for IVP problems in such a general setting. We also introduce novel techniques for subroutines such as StepA and StepB, and a scaffold datastructure to support our End Enclosure algorithm. Among the techniques are new ways refine full- and end-enclosures based on a {\bf radical transform} combined with logarithm norms. Comparisons with existing validated IVP software also help identify the principal computational costs associated with guaranteeing termination and a prescribed end-enclosure accuracy.

cs.SC↗
arXiv2026

Semi-automated Verification of Symbolic Invariants In Extended Symmetric Nets

Structural analysis is central to Petri Net (PN) research, complementing state-space methods while avoiding their combinatorial issues. It is well studied for classical PNs but much less for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, allowing symbolic reachability graphs and associated lumped Markov chains for stochastic SN. In the past two decades, specific structural techniques for SN have emerged, notably the SNexpression tool, which implements a calculus for symbolic structural relations such as conflict and causality. We propose using this calculus to semi-automatically verify symbolic structural invariants, currently possible only for restricted SN subclasses, for an extended SN formalism (ESN) closed under key functional operators. We focus on flows and outline, at least in theory, how to construct a flow-generating family. We also sketch a framework for formally verifying a wider range of invariant properties. Representative examples illustrate the main concepts.

cs.SC↗
arXiv2026

A Practical Approach To Verifying Structural Invariants In Colored Petri Nets

Structural analysis is a core method in Petri Net (PN) research, offering a perspective complementary to state-space techniques while avoiding many of their limitations. It is well studied for classical PNs but far less for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, enabling the construction of a symbolic reachability graph (and a lumped Markov chain in stochastic SN) and the execution of symbolic discrete-event simulations. During the past two decades, structural techniques tailored to SN have been developed, notably supported by the SNexpression tool. This tool implements a formal calculus designed for the computation of symbolic structural relations, including, but not limited to, conflict relations and causal dependencies. Here, we focus on using this calculus to verify semi-automatically symbolic structural invariants, a task currently feasible only for certain restricted SN subclasses. We focus specifically on (semi)flows and briefly discuss an approach through which a flow generative family can be generated, at least theoretically. We further briefly outline a framework for the formal verification of a broader class of invariant properties. An extended formulation of the SN formalism is employed, which demonstrably satisfies the closure property with respect to fundamental functional operators. The core concepts are elucidated by means of representative examples throughout the exposition.

cs.SC↗