Formal Verification of Neural Computer Runtimes via Neural Transition System Abstraction

TL;DR: What if we could "prove" that a Neural Computer will always follow the rules, by turning its learned behaviors into a formal map that can be checked by logic? An initial study could abstract NC state transitions into a finite-state model, use Computational Tree Logic to verify symbolic stability, and identify failure cases for routine reuse and controlled updates.

Research Question: Can formal abstraction techniques, such as neural transition system modeling and Computational Tree Logic (CTL), be used to verify the stability, safety, and reprogrammability properties of Neural Computers?

Hypothesis: By abstracting NC runtimes into formal transition systems, we can systematically verify critical properties (e.g., routine stability, reprogrammability, safety constraints), accelerating progress toward robust, general-purpose CNCs.

Experiment Plan: Instrument NCs to record state transitions and extract a transition abstraction (Yang et al., 2025). Partition the state space and label transitions, constructing an abstract transition system. Use CTL model checking to verify properties such as "routine X always reaches a terminal state" or "no unsafe I/O alignment occurs." Apply to both synthetic and real CLI/GUI NCs, diagnosing routine instability or symbolic drift. Use findings to guide architectural or training improvements.

References:

• Yang, Y., Wang, T., & Xiang, W. (2025). Neural transition system abstraction for neural network dynamical system models and its application to Computational Tree Logic verification. Neural Networks.