用于分布式并行AI程序验证的定向神经符号随机执行
Directed Neuro-Symbolic Stochastic Execution for Verification of Distributed Parallel AI Programs
- Quandary Peak Research（昆达里峰研究院）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
针对分布式并行AI程序的可靠性缺口，提出DNSSE混合测试框架，结合LLM调度预测与符号约束求解等，实现更优的并发bug检测率与分支覆盖率。
AI中文摘要：
分布式并行人工智能（AI）程序存在传统测试无法填补的可靠性缺口：并行执行具有非确定性，而AI工作负载带来的高维输入与非线性操作，使模糊测试和符号执行无法单独应对。我们提出定向神经符号随机执行（DNSSE），这是一种混合测试框架，它将大型语言模型（LLM）引导的调度预测与符号约束求解、覆盖引导的随机变异相结合。我们将分布式AI执行建模为非确定性迁移系统，用线性时序逻辑指定正确性，证明了混合求解器的可靠性、有界完备性和概率完备性，同时对LLM引导的调度探索进行了预期成本分析。在PyTorch和Ray上实现的可扩展版本，比最强基线多检测出2.9%的并发bug，且在五个真实分布式AI基准测试中，将平均分支覆盖率从68.6%提升至91.6%。
英文摘要：
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.
