自回归神经序列模型的概率模型检查

在部署自回归神经序列模型时，测试集的准确性对两个重要问题没有提及：被测系统 (SUT) 对采样下可达到的违反约束的替代方案放置了多少概率质量，以及输入总体的多少比例满足域要求。我们通过概率模型检查来回答这两个问题。该管道从 SUT 的逐个词元生成中提取离散时间马尔可夫链 (DTMC)，使用 PRISM 模型检查器验证正式的 PCTL 规范，并将每个输入的判决聚合到输入空间上的覆盖曲线中。稳健性定理将 DTMC 确定为欠近似值，因此每个判决都会产生 SUT 真实可达概率的经过认证的区间。因此，根据这些判决建立的覆盖范围在结构上是保守的。反例引导的抽象细化（CEGAR）循环自适应地收紧间隔，最大似然算法提取最可能的伪造痕迹。两个案例研究对管道进行了检验。在具有 100% 测试精度的 GPT-2 计算机辅助流程规划 (CAPP) 模型上，管道量化了贪婪解码隐藏的概率质量，但这可以通过采样来实现；并确定排序要求在总体范围内保持的最小训练分数，这两种测试的准确性都无法报告。然后，我们用 50 倍大的词汇量验证 SMILES 分子生成器。唯一的变化是外部化学有效性预言机，并且管道确定了结构完整性和化学有效性之间的差距。