CLN2INV：利用连续逻辑网络学习循环不变式
机器学习
2019-10-18 v3 软件工程
机器学习
摘要
程序验证为确保程序正确性提供了框架，从而系统性地消除不同类别的缺陷。推断循环不变式是真实世界程序（通常包含许多循环）自动验证背后的主要挑战之一。本文提出连续逻辑网络（CLN），一种从程序执行轨迹中自动学习循环不变式的新颖神经架构。与现有神经网络不同，CLN能从程序执行轨迹中学习满足模理论（SMT）中循环不变式公式的精确显式表示。我们开发了一种新的可靠且完备的语义映射，用于将SMT公式赋予连续真值，从而使CLN得以高效训练。我们利用CLN实现了一种新的循环不变式推断系统CLN2INV，在流行的Code2Inv数据集上显著优于现有方法。CLN2INV是首个解决Code2Inv数据集中全部124个理论可解问题的工具。此外，CLN2INV对每个问题的平均耗时仅1.1秒，比现有方法快40倍。我们进一步证明CLN2INV甚至能学习比Code2Inv数据集所需复杂得多的12个循环不变式。
引用
@article{arxiv.1909.11542,
title = {CLN2INV: Learning Loop Invariants with Continuous Logic Networks},
author = {Gabriel Ryan and Justin Wong and Jianan Yao and Ronghui Gu and Suman Jana},
journal= {arXiv preprint arXiv:1909.11542},
year = {2019}
}