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

arXiv: https://arxiv.org/abs/2608.07947 · HTML: https://mlsanity.com/paper/2608.07947/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 31 references that are in the map.
- First posted on arXiv 8 Aug 2026.

## Builds on (most cited first, 12 of 12)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Ray: A Distributed Framework for Emerging AI Applications](https://mlsanity.com/paper/1712.05889/) (2017)
- [DeepXplore: Automated Whitebox Testing of Deep Learning Systems](https://mlsanity.com/paper/1705.06640/) (2017)
- [Large Language Models are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models](https://mlsanity.com/paper/2212.14834/) (2022)
- [Fuzz4All: Universal Fuzzing with Large Language Models](https://mlsanity.com/paper/2308.04748/) (2023)
- [Fuzzing Deep-Learning Libraries via Automated Relational API Inference](https://mlsanity.com/paper/2207.05531/) (2022)
- [Large Language Model Powered Symbolic Execution](https://mlsanity.com/paper/2505.13452/) (2025)
- [Facilitating Parallel Fuzzing with mutually-exclusive Task Distribution](https://mlsanity.com/paper/2109.08635/) (2021)
- [Hybrid Concolic Testing with Large Language Models for Guided Path Exploration](https://mlsanity.com/paper/2601.12274/) (2026)

## Abstract (arXiv)

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.