Code2Inv Framework

Learning Loop Invariants for Program Verification

Abstract

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 that constructs the solution by multi-step decision making and querying an external program graph memory block. By training with reinforcement learning, we are able to capture rich program features and avoid the need for ground truth solutions as supervision. Compared to previous learning tasks in domains with graph-structured data, we address 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 our approach 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 solver, 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.

Publication
In Thirty-second Conference on Neural Information Processing Systems.
Date