摘要
为解决数据投毒攻击检测中的两个核心问题，即缺乏形式化建模以及理论完备性保障不足，本文提出了一种基于模型检验的形式化验证算法用于检测投毒攻击。首先，将人工智能系统抽象为四元组，而投毒攻击（标签翻转、特征扰动、后门投毒、梯度篡改）则被建模为三元组。同时，分别运用CTL*和PCTL时序逻辑公式来描述上述攻击的特征。其次，通过构建原子命题和Kripke结构，建立了形式化特征与逻辑公式之间的等价映射，进而借助SPIN和PRISM工具实现自动检测与验证。此外，本文还提出了三个核心定理并进行了严格证明：针对投毒攻击的形式化模型的特征完备性定理、检测算法的完备性与正确性定理，以及防御框架的鲁棒性定理。理论证明与实验结果表明，当恶意样本比例不超过20%时，漏检率≤2%，误检率≤3.5%。在部署防御措施后，模型的准确率下降幅度可控制在8%以内。这项工作为人工智能系统中的投毒攻击检测提供了具有形式化可验证性和理论保障的解决方案。
