面向分布式并行AI程序验证的定向神经符号随机执行

# 面向分布式并行AI程序验证的定向神经符号随机执行
来源：https://arxiv.org/html/2608.07947  
Gautham Koorma, Vikas Sharma, George Edwards, Mahdi Eslamimehr(🖂)  
Quandary Peak Research, Los Angeles, CA, USA  
[email protected], [email protected], [email protected], [email protected]  

###### 摘要  
分布式并行人工智能（AI）程序暴露出的可靠性差距是传统测试无法弥合的：并行执行是非确定性的，而AI工作负载带来的高维输入和非线性运算使得模糊测试与符号执行在孤立情况下都难以奏效。我们提出了定向神经符号随机执行（DNSSE），一个将大语言模型（LLM）引导的调度预测与符号约束求解及覆盖引导的随机变异相结合的混合测试框架。我们将分布式AI执行建模为非确定性转移系统，用线性时序逻辑指定正确性，并证明混合求解器的可靠性（soundness）、有界完备性（bounded completeness）和概率完备性（probabilistic completeness），同时给出LLM引导调度探索的期望成本分析。基于PyTorch和Ray的可扩展实现检测到的并发缺陷数量是最强基线的2.9倍，并在五个现实分布式AI基准测试上将平均分支覆盖率从68.6%提升到91.6%。

关键词：软件测试，符号执行，模糊测试，大语言模型，分布式系统，并行编程，形式化验证

## 1 引言

生产级AI系统，如数据并行训练流水线、联邦学习服务、强化学习器和吞吐量推理服务器，运行在异构集群之上，协调数千个并发活动，并操纵具有数十亿参数的模型。随着这些系统进入安全关键和业务关键角色，确保其可靠性和正确性已成为一项艰巨且基本未解决的工程挑战。这样的困难源于两个相互叠加的复杂性来源。首先，并行程序本质上是非确定性的：数据竞争、死锁和原子性违背只会在特定交错下显现，而经验研究表明，这类缺陷在多线程应用[1](https://arxiv.org/html/2608.07947#bib.bib1)和数据中心分布式系统[2](https://arxiv.org/html/2608.07947#bib.bib2)中是最常见且破坏性最大的缺陷之一。其次，AI程序具有高维连续输入空间，其控制流由非线性操作（激活、归一化、张量收缩）守卫，这些操作难以用经典分析处理。当这两种范式交汇时，交错空间与输入空间的乘积使得可达状态空间对于常规测试来说难以处理。

现有技术最多只解决这个乘积空间的一侧。符号执行[3](https://arxiv.org/html/2608.07947#bib.bib3)提供了严格的逐路径推理，但面临路径爆炸以及浮点、非线性算术上的求解器不完备问题。覆盖引导与并行模糊测试[4](https://arxiv.org/html/2608.07947#bib.bib4)、[5](https://arxiv.org/html/2608.07947#bib.bib5)、[6](https://arxiv.org/html/2608.07947#bib.bib6)扩展性好，但很少能深入由严格数值条件守卫的区域，并且对调度维度一无所知。系统性并发测试[7](https://arxiv.org/html/2608.07947#bib.bib7)控制调度器，但不考虑数值输入。针对深度学习系统和库的测试技术[8](https://arxiv.org/html/2608.07947#bib.bib8)、[9](https://arxiv.org/html/2608.07947#bib.bib9)以顺序API或模型函数本身为目标，将嵌入模型的分布式程序排除在外。

为弥合这一缺口，我们提出了*定向神经符号随机执行*（DNSSE），它将三种引擎融合为一次定向搜索：一个符号引擎求解路径约束的可判定片段，一个随机变异引擎通过覆盖引导的随机搜索解决非线性片段，以及一个大语言模型（LLM）调度器，它读取分布式AI代码的语义结构，并按其暴露并发违规的潜在可能性对线程交错进行排序。LLM仅作为调度空间上的一个学习先验；可行性仍由符号引擎和随机引擎负责，因此形式保证从不依赖于LLM的正确性。

本文做出四项贡献：（1）DNSSE，一种将LLM引导的调度预测与定向符号和随机执行相结合的新算法，用于分布式并行AI程序（第4–5节）；（2）一个基于转移系统和线性时序逻辑（LTL）的形式框架，包含可靠性、有界完备性和概率完备性的证明，以及量化学习排序何时优于均匀探索的期望成本界（第6节）；（3）一个基于PyTorch和Ray的可扩展架构，将追踪、约束求解和模糊测试分布到集群上（第7节）；（4）在五个现实分布式AI基准测试上的评估，DNSSE检测到的并发缺陷数量是最强基线的2.9倍（合计73个对25个），并将平均分支覆盖率从68.6%提升到91.6%（第8节）。

## 2 相关工作

#### 测试并发程序。
并发执行推理的基础由时序逻辑[10](https://arxiv.org/html/2608.07947#bib.bib10)、[11](https://arxiv.org/html/2608.07947#bib.bib11)奠定，它至今仍是规定交错计算的安全性和活性的标准语言。精确的动态数据竞争检测以FastTrack[12](https://arxiv.org/html/2608.07947#bib.bib12)为代表，而竞争定向调度将动态分析与调度合成相结合，迫使并发程序进入真实竞争[7](https://arxiv.org/html/2608.07947#bib.bib7)；这一定向范式已扩展到死锁[13](https://arxiv.org/html/2608.07947#bib.bib13)、原子性违背[14](https://arxiv.org/html/2608.07947#bib.bib14)以及事件驱动程序的时序分析[15](https://arxiv.org/html/2608.07947#bib.bib15)。这些技术对传统的Java/C/C++代码有效，但均不涉及主导AI工作负载的非线性数值守卫和张量级数据流。

#### 符号执行与混合测试。
KLEE[3](https://arxiv.org/html/2608.07947#bib.bib3)等符号执行器和concolic测试[16](https://arxiv.org/html/2608.07947#bib.bib16)通过系统性地求解累积路径约束来枚举可行路径。由于求解在深层或非线性条件上会停滞，混合系统会在模糊器与符号引擎之间交接工作，如QSYM[17](https://arxiv.org/html/2608.07947#bib.bib17)。另一条正交路径上，并行模糊测试将随机测试扩展到集群：P-Fuzz通过以数据库为中心的架构分发模糊测试状态[4](https://arxiv.org/html/2608.07947#bib.bib4)，AFL-EDGE将种子划分为相互排斥的任务[5](https://arxiv.org/html/2608.07947#bib.bib5)，KRAKEN根据程序特征调整任务分配[6](https://arxiv.org/html/2608.07947#bib.bib6)。所有这些系统都以顺序二进制或线程无感知执行为目标；搜索空间的调度维度未被探索。

#### AI系统的验证与测试。
另一条互补的研究路线测试AI工件本身。DeepXplore[8](https://arxiv.org/html/2608.07947#bib.bib8)引入了神经网络的覆盖引导白盒测试，DeepREL通过自动推断的关系API对深度学习库进行模糊测试[9](https://arxiv.org/html/2608.07947#bib.bib9)。在形式化方面，Reluplex扩展了SMT求解，以验证分段线性网络[18](https://arxiv.org/html/2608.07947#bib.bib18)。这些技术将模型或库API视为顺序函数；它们不解决当模型由并发分布式程序训练或服务时产生的竞争、死锁或原子性违背问题。

#### 用于软件测试的大语言模型。
LLM最近被嵌入到测试循环中。TitanFuzz使用LLM作为深度学习API程序的零样本生成器和变异器[19](https://arxiv.org/html/2608.07947#bib.bib19)，Fuzz4All将LLM驱动的模糊测试推广到跨语言和跨系统[20](https://arxiv.org/html/2608.07947#bib.bib20)。更接近程序分析的是，LLM赋能的符号执行将路径约束推理分解为委托给模型的子任务[21](https://arxiv.org/html/2608