Directed Neuro-Symbolic Stochastic Execution for Verification of Distributed Parallel AI Programs

arXiv:2608.07947 · cs.AI, cs.DC · Submitted 2026-08-08 · Read on arXiv

Gautham Koorma, Vikas Sharma, George Edwards, Mahdi Eslamimehr

cs.AI, cs.DC

Submitted: 2026-08-08

Updated: 2026-08-11

Comments: 1 Figure, 1 Algorithm, 1 Figure, 2 Tables

License: http://creativecommons.org/licenses/by/4.0/

The gist: Distributed parallel Artificial Intelligence (AI) programs expose reliability gaps that conventional testing cannot close: parallel executions are non-deterministic, and AI workloads bring

Terminology

Trace — 17× in this paper · explained in 2 episodes
Benchmark — 13× in this paper · explained in 2 episodes
Large Language Model — 9× in this paper
SMT solver — 8× in this paper · explained in 2 episodes
Verification — 7× in this paper · explained in 2 episodes
Directed Neuro-Symbolic Stochastic Execution — 6× in this paper
Core — 3× in this paper · explained in 2 episodes
Large Language Model (LLM) — 3× in this paper · explained in 3 episodes
Actor — 2× in this paper · explained in 3 episodes
Artificial Intelligence — 2× in this paper
Artificial Intelligence (AI) — 2× in this paper · explained in 2 episodes
Programming Language Design and Implementation — 2× in this paper
Symposium on Operating Systems Principles — 2× in this paper
Ablation — 1× in this paper · explained in 1 episode
Ablation Study — 1× in this paper · explained in 3 episodes
Differentially Private — 1× in this paper · explained in 3 episodes
Federated Learning — 1× in this paper · explained in 19 episodes
Fine-Tuning — 1× in this paper · explained in 5 episodes
Formal Verification — 1× in this paper · explained in 2 episodes
Generator — 1× in this paper · explained in 2 episodes
Hybrid System — 1× in this paper · explained in 2 episodes
Inflation — 1× in this paper · explained in 2 episodes
Linear Temporal Logic (LTL) — 1× in this paper · explained in 4 episodes
Pruning — 1× in this paper · explained in 4 episodes
Quantization — 1× in this paper · explained in 15 episodes
Reinforcement Learning — 1× in this paper · explained in 4 episodes
Speculative Decoding — 1× in this paper · explained in 2 episodes
Steering — 1× in this paper · explained in 2 episodes
Symposium on Foundations of Software Engineering — 1× in this paper
Symposium on Operating Systems Design and Implementation — 1× in this paper
Transformer — 1× in this paper · explained in 2 episodes
Transformers — 1× in this paper · explained in 2 episodes
Workshop on Worst-Case Execution Time Analysis — 1× in this paper

Abstract

Distributed parallel Artificial Intelligence (AI) programs expose reliability gaps that conventional testing cannot close: parallel executions are non-deterministic, and AI workloads bring high-dimensional inputs and non-linear operations that defeat fuzzing and symbolic execution in isolation. We present Directed Neuro-Symbolic Stochastic Execution (DNSSE), a hybrid testing framework that couples schedule prediction guided by a Large Language Model (LLM) with symbolic constraint solving and coverage-guided stochastic mutation. We model distributed AI executions as non-deterministic transition systems, specify correctness in linear temporal logic, and prove soundness, bounded completeness, and probabilistic completeness of the hybrid solver, together with an expected-cost analysis of LLM-guided schedule exploration. A scalable implementation on PyTorch and Ray detects 2.9% more concurrency bugs than the strongest baseline and raises average branch coverage from 68.6 % to 91.6 % across five realistic distributed AI benchmarks.

Directed Neuro-Symbolic Stochastic Execution for Verification of Distributed Parallel AI Programs

Terminology

Abstract

Sources

Related papers