用门控连续逻辑网络学习非线性循环不变式（扩展版）
软件工程
2020-11-03 v4 机器学习
编程语言
摘要
验证真实程序通常需要推断具有非线性约束的循环不变式。在执行大量数值操作（如航空电子或工业工厂的控制系统）的程序中尤其如此。最近，数据驱动的循环不变式推断方法已显示出前景，尤其是在线性不变式上。然而，由于高阶项的数量和量级巨大、在少量样本上过拟合的可能性以及可能不等式边界的巨大空间，将 data-driven 推断应用于非线性循环不变式具有挑战性。在本文中，我们介绍了一种用于通用 SMT 学习的新神经架构——门控连续逻辑网络（Gated Continuous Logic Network, G-CLN），并将其应用于非线性循环不变式学习。G-CLN 通过门控单元和 dropout 扩展了连续逻辑网络（Continuous Logic Network, CLN）架构，使模型能稳健地在大数量项上学习通用不变式。为解决有限程序采样引起的过拟合，我们引入了分数采样——一种将循环语义松弛为连续函数的可靠方法，便于在实数域上无界采样。我们还设计了一种新的 CLN 激活函数，分段偏置二次单元（Piecewise Biased Quadratic Unit, PBQU），用于自然学习紧不等式边界。我们将这些方法整合进一个能学习通用非线性循环不变式的非线性循环不变式推断系统。我们在非线性循环不变式基准上评估了我们的系统，显示其解决了 27 个问题中的 26 个，比先前工作多 3 个，平均运行时间 53.3 秒。我们进一步通过解决线性 Code2Inv 基准中全部 124 个问题展示了 G-CLN 的通用学习能力。我们还进行了定量稳定性评估，显示 G-CLN 在二次问题上的收敛率为 ，比 CLN 模型提高 。
引用
@article{arxiv.2003.07959,
title = {Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)},
author = {Jianan Yao and Gabriel Ryan and Justin Wong and Suman Jana and Ronghui Gu},
journal= {arXiv preprint arXiv:2003.07959},
year = {2020}
}