Learning Loop Invariants for Program Verification
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.
= Summary  The paper presents a new method for reinforcement learning-based counterexample-guided loop invariant generation. First the program's source code is encoded into a vector representation by transforming it into a graph and applying a graph neural network. Then, a tree decoder is used to generate an arithmetic formula in conjunctive normal form, using attention over the encoded program.  Overall, the approach seems promising, and the shown experimental results indicate that it is an interesting alternative to standard deductive and more recently introduced data-driven CEGAR approaches to program verification. However, the paper does not actually show the core of its contribution, the smoothed reward function used to train the system, and so I believe that the submission in its current form can not be accepted. I am inviting the authors to clarify this point (cf. below for details) in the rebuttal and update the paper subsequently, and would be happy to increase my score then. [UPDATE: This happened.]  = Quality  The paper follows recent trends in the literature (programs as graphs, syntax-directed decoding of formulas, ...), but combines it with a novel reinforcement learning approach, sidestepping the issue of a lack of labeled examples and making it easier to adapt the method to new domains. However, the core of the main contribution, namely the reward function that smoothes over the very sparse, binary valid/invalid signal, is not defined in the main paper. Instead, it refers to the supplement, where the reward is again not defined. Instead, some handwavy text about the use of counterexamples is provided (for example, do their values / traces matter, or just their number? Are UNSAT cores used to identify which parts of the candidate invariant are contradictory?). Without this, the contribution is not remotely reproducible and the paper cannot be accepted.  The main text of the paper has to contain at least an approximate definition of the reward function, and the supplement should provide a full definition. Documenting the use of counterexamples is especially important, as Sect. 5 even provides an ablation study underlining their importance.  [UPDATE: The authors have provided details on the reward function in their response, and promised to include these details in a revision of their paper. Based on this, I think an interesting question for a future revision would be to experimentally valid the design of the reward function. For example, inverting the order of reward components from pre->inv->post to post->inv->pre would be interesting (corresponding to a backwards-looking style, as in Hoare logic proofs); similarly not ordering the components at all could be an interesting ablation.]  Similarly, the paper should be more honest about the runtime performance of the proposed approach. Lines 260-265 introduce the notion of calls to the backing SMT solver as a metric; which is fine to show the data efficiency of the approach, but wallclock time is interesting for actual use of an invariant generation tool in a verifier. The timeout of 12 hours used in the paper contrasts with 1 hour allowed in the SyGuS competition from which many benchmarks are taken, and the fact that the ICE-DT solver requires less than 5 _seconds_ for most benchmarks (cf. https://dl.acm.org/citation.cfm?doid=2837614.2837664). Even if the method is currently not competitive in terms of runtime, this should be stated explicitly in the paper.  [UPDATE: The authors have promised to include runtime in the next revision.]  = Clarity  The paper succeeds reasonably well in introducing basic verification concepts in the little space it has, and apart from the lack of description of the reward function is reasonably clear. I found Sect. 3.1 not particularly enlightening (especially because I don't see that it supports conclusions (1) and (2) in lines 128-131) and would rather use some of the space used for the example to go into more detail on the reward function, which is the actual contribution of the paper.  = Originality  Finding a smoothing of the reward function that actually works is a novel and interesting contribution that hasn't been provided before. The authors review most of the related literature and discuss how they are clearly differing from it, though they seem to be unaware of one related work that infers loop invariants for heap programs using a tree decoder and a graph encoding of its inputs (but uses fully supervised training on synthetic data):    Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna, and    Daniel Tarlow. Learning Shape Analysis. In SAS'17.  = Significance  Pushing beyond existing heuristics in deductive invariant generation tools is of great importance to making program verification more generally useful; several large-scale efforts (e.g., the verified TLS stack, the seL4 kernel, ...) towards formally verified software could profit from an evolution of the presented approach to more interesting domains. [This is minor pet peeve that I have with the paper: The fact that integer invariants are interesting, but not all that useful without heap invariants is never stated]  = Minor notes - lines 31/32: Calling Octagons "hand-crafted features" seems    unnecessarily harsh. It would be more correct to call them a    restricted hypothesis space. - line 74: This statement is just wrong, for example for arbitrary    polynomials or for the very relevant domain of separation logic.    It's true for the domain of linear integer arithmetic that is    investigated in the paper, but that distinction isn't stated. - line 141: "... module summarizes what have been" - s/have/has/ - line 159: "To convert the graph into vector representation" - missing   article.