Program verification offers a framework for ensuring program correctness and therefore systematically eliminating different classes of bugs. Inferring loop invariants is one of the main challenges behind automated verification of real-world programs which often contain many loops. In this paper, we present Continuous Logic Network (CLN), a novel neural architecture for automatically learning loop invariants directly from program execution traces. Unlike existing neural networks, CLNs can learn precise and explicit representations of formulas in Satisfiability Modulo Theories (SMT) for loop invariants from program execution traces. We develop a new sound and complete semantic mapping for assigning SMT formulas to continuous truth values that allows CLNs to be trained efficiently. We use CLNs to implement a new inference system for loop invariants, CLN2INV, that significantly outperforms existing approaches on the popular Code2Inv dataset. CLN2INV is the first tool to solve all 124 theoretically solvable problems in the Code2Inv dataset. Moreover, CLN2INV takes only 1.1 second on average for each problem, which is 40× faster than existing approaches. We further demonstrate that CLN2INV can even learn 12 significantly more complex loop invariants than the ones required for the Code2Inv dataset.
Summary:
This paper introduces a novel way to find loop invariants for a
program. The loop invariants are expressed as SMT formulas. A
continuous relaxation of an SMT solver is introduces mapping
every SMT formula onto a truth value \in [0, 1]. This relaxation
called a continuous semantic mapping is decided such that every
true formula has a higher value than every false formula. This
allows an invariant to be learned.
Novelty and Significance:
This work is interesting and although authors do seem to be
outside of the community, I firmly believe is appropriate for
ICLR. If the claims made by the paper are true they constitute
a significant contribution to the field of program synthesis
and program analysis.
Technical Quality:
The evaluation was fairly thorough, but the paper can be
strengthened massively with a few small changes and additions.
It might be more helpful if there was a sense of how many problems
none of the systems can do and how complicated of a program can
this system extract a loop invariant from. Why were was it these
particular 12 that work? Are there examples that don't?
I don't know why all this time is spent on t-norms when behavior
on them is fairly similar and the simplest norm works best.
Lots of details are missing in this paper. How much training data
was generated? How long did it take? Does training data need to
be generated for each example? If so is that included in the
runtime for Figure 3?
The paper talks about neural architecture, but all I see is
effectively a curve-fitting task for some template. This feels
different from the code2inv paper where a program can be fed
into the system and the pretrained model emits the invariant.
Clarity:
Not enough of this paper concentrates on the novel aspects of the
approach. Section 5 discusses template generation, but not in
enough detail that I would be able to replicate this work. I
could also not find enough details in the Appendix.
I don't know why vital page space is spent on defining completeness
and soundness.
Possibly related work as relaxations to SAT/SMT solvers do exist in the literature.
Guiding High-Performance SAT Solvers with Unsat-Core Predictions
https://arxiv.org/abs/1903.04671
Learning to Solve SMT Formulas
https://papers.nips.cc/paper/8233-learning-to-solve-smt-formulas.pdf
Notes:
You cite Si et al. for LoopInvGen when you should be citing Pathi
and Millstein in the third paragraph on page 2.