用大模型引导符号执行，提升分布式AI程序的可靠性验证
Directed Neuro-Symbolic Stochastic Execution for Verification of Distributed Parallel AI Programs
- 结合大模型预测调度与符号约束求解，实现定向探索
- 在5个真实场景中检测到2.9%更多并发缺陷，分支覆盖率提升至91.6%
- 适合关注AI系统可靠性的研发与测试人员
分布式并行人工智能程序存在传统测试难以覆盖的可靠性漏洞：并行执行具有非确定性，且高维输入与非线性操作使单独使用模糊测试或符号执行失效。本文提出定向神经符号随机执行（DNSSE），融合由大语言模型（LLM）指导的调度预测、符号约束求解与覆盖引导的随机变异。将分布式AI执行建模为非确定性转移系统，以线性时序逻辑定义正确性，并证明了混合求解器的完备性与概率完备性，以及LLM引导调度探索的期望成本。基于PyTorch和Ray的可扩展实现，在五个真实分布式AI基准上比最强基线多发现2.9%的并发错误，平均分支覆盖率从68.6%提升至91.6%。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。