Learning Loop Invariants for Program Verification
Learning Loop Invariants for Program Verification
复制标题
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
X. Si;H. Dai;Mukund Raghothaman;M. Naik;Le Song
中科院分区：
文献类型：
--
作者：
X. Si;H. Dai;Mukund Raghothaman;M. Naik;Le Song
程序验证中的一个基本问题涉及推断循环不变的。这个问题是不确定的，甚至实际的实例也很具有挑战性。受到人类专家如何构建循环不变的启发，我们提出了一个推理框架代码2INV，该框架通过多步决策制定和查询外部程序图表内存块来构建解决方案。通过使用强化学习培训，Code2inv捕获了丰富的计划功能，并避免了对地面真理解决方案的需求作为监督。与具有图形结构数据的域中的以前的学习任务相比，它解决了独特的挑战，例如二进制目标函数和极稀疏的奖励，仅在提出完整的循环不变性后才由自动定理摊子给出。我们在133个基准问题的套件中评估Code2Inv，并将其与三个最先进的系统进行比较。它解决了106个问题，而基于随机搜索的系统，基于启发式搜索的系统的77个问题，而基于决策树学习的系统为100。此外，所学的策略可以推广到新程序：与从头开始解决新实例相比，预训练的代理在查找解决方案方面更有效。
A fundamental problem in program verification concerns inferring loop invariants. The problem is undecidable and even practical instances are challenging. Inspired by how human experts construct loop invariants, we propose a reasoning framework Code2Inv that constructs the solution by multi-step decision making and querying an external program graph memory block. By training with reinforcement learning, Code2Inv captures rich program features and avoids the need for ground truth solutions as supervision. Compared to previous learning tasks in domains with graph-structured data, it addresses unique challenges, such as a binary objective function and an extremely sparse reward that is given by an automated theorem prover only after the complete loop invariant is proposed. We evaluate Code2Inv on a suite of 133 benchmark problems and compare it to three state-of-the-art systems. It solves 106 problems compared to 73 by a stochastic search-based system, 77 by a heuristic search-based system, and 100 by a decision tree learning-based system. Moreover, the strategy learned can be generalized to new programs: compared to solving new instances from scratch, the pre-trained agent is more sample efficient in finding solutions.