CLN2INV: Learning Loop Invariants with Continuous Logic Networks
Authors: Gabriel Ryan
Justin Wong
Jianan Yao
Ronghui Gu
Suman Jana
Venue:  (2020)
Keywords: loop invariants
deep learning
logic learning

Abstract: 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 the 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 times 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.

Published as a conference paper at ICLR 2020
CLN2INV: LEARNING LOOP INVARIANTS WITH CONTINUOUS LOGIC NETWORKS
Gabriel Ryan Justin Justin Wong!;
Jianan Yao Jianan
Ronghui Guli,Suman Jana
"Department of Computer Science, Columbia University, New York, NY, USA {gabe, jianan, rgu, suman fess columbia edu [justin. ) umbia a edu "CertiK, New York, NY. USA
{ronghui. ger.rrtikk
ABSTRACT
Program verification offers framework for ensuring program correctness and therefore systematically eliminating different classes of bugs. Inferring loop in- variants is one of the main challenges behind automated verification of real-world programs, which often contain many loops. In this paper, we present the Continu- ous Logic Network (CLN), a novel neural architecture for automatically learning loop invariants directly from program execution traces. Unlike existing neural net- works, CLNs can learn precise and explicit representations of formulas in Satisfia- bility Modulo Theories (SMT) for loop invariants from program execution traces. We develop a new sound and complete semantic mapping for assigning SMT for- mulas 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
the popular Code2Inv dataset. CLNN2NV 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 40x 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.
INTRODUCTION
Program verification offers a principled approach for systematically eliminating different classes of bugs and proving the correctness of programs. However, as programs have become increas- ingly complex, real-world program verification often requires prohibitively expensive manual ef- fort (Wilcox et al. 2015) Gu et al.] 2016 Chajed et al., 2019). Recent efforts have focused on automating the program verification process, but automated verification of general programs with unbounded loops remains an open problem (Nelson et al. 2017:2219)
Verifying programs with loops requires determining loop invariants, which captures the effect of the loop on the program state irrespective of the actual number of loop iterations. Automatically inferring correct loop invariants is challenging problem that is undecidable in general and difficult to solve in practice (Blass& & Gurevich] 2001 Furia et al.) 2014). Existing approaches use stochastic search (Sharma Aiken 2016), cecuustccs-basee search (Galeotti et al. 2015). PAC learning based on counterexamples (Padhi & Millstein, 2017), or reinforcement learning (Si et al. 2018). However, these approaches often struggle to learn complex, real-world loop invariants.
In this paper, we introduce novel approach to learning loop invariants by modeling the loop be- havior from program execution traces with a new type of neural architecture. We note that inferring loop invariants can be posed as learning formulas in Satisfiability Modulo Theories (SMT) (Biere al. 2009) over program variables collected from program execution traces (Nguyen al. 2017) In principle, neural networks are well suited to this task because they can act as universal function
"Co-student leads listed in alphahetical order; each contributed equally.

---

Published as a conference paper at ICLR 2020
approximators and have been successfully applied in various domains that require modeling of bitrary functions (Horiik et al.) 1989 Goodfellow et al.] 2016). However, loop invariants must be represented explicit SMT formulas to be usable for program verification. Unfortunately, existing methods for extracting logical rules from general neural architectures lack sufficient precision (Au- gasta & Kathirvalavakumar (012)) while inductive logic learning lacks sufficient expressiveness for use in verification (Evans& & Grefenstette| 2018).
We address this issue by developing a novel neural architecture, Continuous Logic Network (CLN), which is able to efficiently learn explicit and precise representations of SMT formulas by using continuous truth values. Unlike existing neural architectures, CLNs can represent learned SMT formula explicitly in its structure and thus allow us to precisely extract the exact formula from a trained model.
In order to train CLNs, we introduce new semantic mapping for SMT formulas to continuous truth values. Our semantic mapping builds on BL, or basic fuzzy logic (Hájek) 2013), to support general SMT formulas in a continuous logic setting. We further prove that our semantic model is sound (i.e., truth assignments for the formulas are consistent with their discrete counterparts) and complete (i.e.. all formulas can be represented) with regard to the discrete SMT formula space. These properties allow CLNs to represent any quantifier- free SMT formula operating on mixed integer-real arithmetic as end-to-ent differentiable series of operations.
We use CLNs to implement a new inference system for loop invariants, CLN2INV, that significantly outperforms state-of-the tools on the Code2Inv dataset by solving all 124 theoretically solvable problems in the dataset. This 20 problems more than LoopInvGen, the winner of the SyGus 2018 competition loop invariant track (Padhi & Millstein, 2017). Moreover, CLN2INV finds invariants for each program in 1.1 second on average, more than 40 times faster than LoopInvGen. We also demonstrate that CLN2INV is able to learn complex. real-world loop invariants with combinations of conjunctions and disjunctions of multivariable constraints. Our source code and benchmarks are publicly available on Github"
Our main contributions are:
We introduce new semantic mapping for assigning continuous truth values to SMT formu- las that theoretically grounded and enables learning formulas through backpropagation. We further prove that our semantic model is sound and complete.
We develop a novel neural architecture, Continuous Logic Networks (CLNs), that to the best of our knowledge is the first efficiently learn precise and explicit SMT formulas by construction.
We use CLNs to implement a new loop invariant inference system, CLN2INV, that is the first to solve all 124 theoretically solvable problems in the Code2Inv dataset, 20 more than the existing methods. CLN2INV is able to find invariants for each problem in 1. second average, 40x faster than existing systems.
We further show that CLN2INV is able to learn 12 more complex loop invariants than the ones present in the Code2Iny dataset with combinations of multivariable constraints.
Related Work. Traditionally, loop invariant learning relies on stochastic or geuridttcs-guiiee search (Sharma& & Aiken 2016 Galeotti et al.) 2015). Other approaches like Numlny analyze traces and discover conjunctions of equalities by solving a system of linear equations (Sharma et al. 2013 Nguyen et al. (2017). LoopInvGen Gen uses PAC learning of CNF using counterexamples (Padhi et al. 2016 Padhi & Millstein, 2017). By contrast, Code2Iny learns to guess loop invariants using re- inforcement learning with recurrent and graph neural networks (Si et al. 2018). However, these approaches struggle to learn complex invariants. Unlike these works, CLN2INV efficiently learns complex invariants directly from execution traces.
There is extensive work on PAC learning of boolean formulas, but learning precise formulas requires a prohibitively large number of samples (Kearns al.. 1994). Several recent works differentiable logic to learn boolean logic formulas from noisy data (Kimmig et al. 2012 Evans & Grefenstette) 2018
Payani & Fekri 2019) or improving adversarial robustness by appl applying logical rules training
https///ittub..co//ryann 1/cln2inv
2

---

Published as a conference paper at ICLR 2020
(Fischer et al. 2019). By contrast, our work learns precise SMT formulas directly by construction, allowing us to learn richer predicates with compact representation in a noiseless setting.
A variety of numerical relaxations have been applied to SAT and SMT solving. Application-specitee approximations using methods such as interval overapproximation and slack variables have been developed for different classes of SMT (Eggers al. 2008; Nuzzo et al. 2010). More recent work has applied recurrent and graph neural networks to Circuit SAT problems and unsat core detection (Amizadeh et al., 2019 Selsam al., 2019 Selsam & Bjömner 2019). FastSMT uses embeddings from natural language processing like skip-gram and bag-of-words to represent formulas for search strategy optimization (Balumovic et 2018). Unlike these approaches, we relax the SMT semantics directly to generate differentiable representation of SMT.
BACKGROUND
In this section, we introduce the problem of inferring loop invariants and provide a brief overview of Satisfaability Modulo Theories (SMT), which are used to represent loop invariants. We provide background into fuzzy logic, which we extend with our new continuous semantic mapping for SMT.
2.1 LOOP INVARIANTS
Loop invariants capture loop behavior irrespective of number of iterations, which is crucial for verifying programs with loops. Given a loop, while (LC) {C}. precondition P, and a post- condition Q. the verification task involves finding a loop invariant / that can be concluded from the precondition and implies the post-condition (Hoare 1969). Formally, it must satisfy the following three conditions, in which the second is a Hoare triple describing the loop:
P
[IALC)
LCCI =
Example of Loop Invariant. Consider the example loop in Fig For a loop invariant to be usable, it must be valid for the precondition (t 10 A 0). the inductive step when t O, and the post-condition (u = 20) when the loop condition is no longer satisfied, i.c., 0. The correct and precise invariant for the program is (2/ + 20).
The desired loop invariant for the left program is a boolean function over program variables f, u such that:
//pre: t=10 /\ u=0
while (t != (
== 1;
== 10 = [
(pre) (ine)
2;
4L
I(t. (tt. = I[t - 1)
/ //post: u=20
T(I,u) A = u
(post)
(a) Example loop
(b) The desired and precise loop invariant I is (21 + 20).
Figure 1: Example Loop Invariant inference problem.
2.2 SATISFIABILITY MODULO THEORIES
Satisfiability Modulo Theories (SMT) are an extension of Boolean Satisfiability that allow solvers to reason about complex problems efficiently. Loop invariants and other formulas in program veri- fication are usually encoded with quantifier-free SMT. A formula in quantifier-free SMT can be inductively defined as below:
F:
Eg -F
IIEE (=,
where Ej and Eg are expressions terms. The loop invariant (2t + u = 20) in Fig. iis an SMT formula. Nonlinear arithmetic theories admit higher-order terms such as t? and t u, allowing them to express more complex constraints. For example, (-(2 2 t²)) is an SMT formula that is true when the value of the high-order term (2 is larger than 2.
3

---

Published as a conference paper at ICLR 2020
2.3 BASIC FUZZY LOGIC (BL)
Basic fuzzy logic (BL) is class of logic that uses continuous truth values in the range [0, 1] and differentiable almost everywhere (Hajek) 2013). BL defines logical conjunction with functions called I-norms, which must satisfy specific conditions to ensure that the behavior of the logic is consistent with boolean First Order Logic. Formally, a t-norm (denoted @ in BL is binary operator over truth values in the interval [0, 1] satisfying the following conditions:
1. associalivity and commulativity; the order in which set of t-norms continuous truth values are evaluated should not change the result: (v(8))) = (#:8)) and x = you.
2. monotonicity: increasing any input value to t-norm operation should cause the result to decrease: 21 S 222 = Ii @ y S 22 @ y
3. consistency: the result of any t-norm applied result of any truth value and 0 should be 0: 1 @ and 0 @ x = 0
truth value and should be and the
Besides these conditions, BL also requires that t-norms be continuous. Given t-norm @, its asso- ciated I-conorm (denoted ()) is defined with DeMorgan's law: + u _ -(-t & -w), which can be considered as logical disjunction. common t-norm the product t-norm x @ y = x y with its associated t-conorm 2 + y
y-
3 CONTINUOUS SATISFIABILIT MODULO THEORIES
We introduce continuous semantic mapping, S, for SMT on BL that is end-to-end differentiable. The mapping S associates SMT formulas with continuous truth values while preserving each for- mula's s semantics. In this paper, we only consider quantifier-free formulas. This process is analogous to constructing t-norms for BL, where a t-norm operates on continuous logical inputs.
We define three desirable properties for continuous semantic mapping S that will preserve formula semantics while facilitating parameter training with gradient descent:
S(F) should be consistent with BL. For any two formulas F and F', where F(x) sat- isfied and Fxxx is unsatisfied with an assignment z of formula terms, we should have (z)) < (()) This will ensure the semantics of SMT formulas are preserved.
2. (IF) should be differentiable almost everywhere. This will facilitate training with gradient descent through backpropogation.
3. S(F) should be increasing everywhere as the terms in the formula approach constraint satisfaction, and decreasing everywhere as the terms in the formula approach constraint violation. This ensures there always a nonzero gradient for training.
Continuous semantic mapping. We first define the mapping for ">" (greater-than) and "z" (greater-than-or-ee oo-qual--- well adopting definitions for "-", "A", and "v" from BL. All other operators can be derived from these. For example, "<" (less-than-or-cqual--o is derived using ">" and "_",, while "_" (equality) is then defined the conjunction of formulas using "s" and ">." Given constants B > O and > O, we first define the the mapping S on ">" and "2" using shifted and scaled sigmoid functions:
S(t u)
S(t 2 u) A
B(t-u-e)
1 1- B(t-ute)
We illustrate these functions in Figure The validity of our semantic mapping lie in the following facts, which can be proven with basic algebra.
lim +++ 1+e-B(l-u- B-6-++00
{
1
1> 15u
lim Bic-+000
{
1 2
1 Blt-
u
Almost everywhere indicates the function is differentiable everywhere except for set of measure O. For example, Rectified Linear Unit is differentiable almost everywhere except
4

---

Published as a conference paper at ICLR 2020
Continuous Truth Value
1.0
( 0) Unshifted Sigmold
0)
Continuous Value
1.0
s (x 0)
0.8
0.8
0.6
0.6
0.4
0.4
0.2
0.2
0.0
0.0
-1.0
0.5
1.0
-1.0
-0.5
0.0
0.5
1.0
(a) Plot of S(x 2 0). S(x > 0) with sigmoid
(b) Plot of S(x 0) with product t-norm
Figure 2: Illustration of the mapping S on >, >.2, when B = 20 and = 0.2
When goes to and B goes to infinity, continuous mapping ">> and "2" will preserve their original semantics. Under these conditions, our mapping satisfies all three desirable properties. In practice, for small and large B, the properties also satisfied if uu >
Next we define the mapping S for boolean operators "A", "V" and "-" using BL. Given a specific t-norm and its corresponding t-conorm @ it is straightforward to define mappings of "A", "V" and "
S(Fi A FF) & S(F2)
S(FIV V
e S(F))
S(-F) 2 1
Based the above definitions, the mapping for other operators be derived follows:
<( S(((t u)) 1 B(t-u-e)
=
+ B((-uu-c)
S(t u) S(( 2 u) A (t u))
I e B(l-u+e) 1 B(t-u-e)
The mapping S on "=" is valid since the following limit holds (see Appendix A for the proof).
Figure
{ 1 t=
lim S(t= u) +oc-++00
c-00 1 e B(c-u++) & 1 e B(t-u-e)
lim
0 t
B-c-+000
The mapping for other operators shares similar behavior in the limit, and also fulfill our desired properties under the same conditions.
Using our semantic mapping S, most of the standard operations of integer and real arithmetic, including addition, subtraction, multiplication, division, and exponentiation, can used normally and mapped continuous truth values while keeping the entire formula differentiable. Moreover, any expression SMT that has an integer or real-valued result can be mapped to continuous logical values via these formulas, although end-to-end differentiability may not be maintained in cases where specific operations are nondifferentiable.
4 CONTINUOUS LOGIC NETWORKS
In this section, we describe the construction Continuous Logic Networks (CLNs) based on our continuous semantic mapping for SMT on BL.
CLN Construction. CLNs use our semantic mapping to provide a general neural architecture for learning SMT formulas. In CLN, the learnable coefficients and smoothing parameters correspond to the learnalle parameters a standard feedforward network, and the continuous predicates, norms, and t-conorms operate activation functions like ReL.Us in standard network. In this
5

---

Published as a conference paper at ICLR 2020
paper, we focus shallow networks to address the loop invariant inference problem, but envision deeper general purpose CLNs that can learn arbitrary SMT formulas. When constructing a CLN, work from an SMT Formula Template, in which every value is marked as either input term, constant, or a learnable parameter. Given an SMT Formula Template, we dynamically construct a CLN as computational graph. Sigure]soows simple formula template and the constructed CLN. We denote the CLN model constructed from the formula template S(F) as Mp.
CLN Training. Once the CLN has been constructed based on formula template, it is trained with the following optimization. Given a CLN model M constructed from an SMT template with learnable parameters W. and set X of valid assignments for the terms in the SMT template, the expected value of the CLN is maximized by minimizing a loss function L that penalizes model outputs that are less than one. minimum scaling factor 3 selected, and hinge loss is applied to the scaling factors (B) to force the differentiable predicates to approach sharp cutoffs. The offset also regularized to ensure precision. The overall optimization is formulated as:
max (X; W, W, (W.
min (W.B,4) xEX
((M(x;; W, B. W, + Σ BEB
Chsnge (3, + >||e|12
where À and y are hyperparameters respectively governing the weight assigned to the scaling factor and offset regularization. Lhange (3, B) is defined mar(0, 3 B). and C is any loss function
strictly decreasing in domain [0, 1].
Given CLN that has been trained to loss approaching 0 on given set of valid assignments, show that the resulting continuous SMT formula learned by the CLN is consistent with an equivalent discrete SMT formula. In particular, we prove that such formula is sound, (i.e., CLN will learn correct SMT formula with respect to the training data), and that our continuous mapping is complete, (i.e., CLNs can represent any SMT formula that be represented in discrete logic), where these properties are defined for CLNs as follows:
Soundness. Given the SMT formula F, the CLN model Mr constructed from S(F) always preserves the truth value of F. It indicates that given a valid assignment to the terms x in F, F(x) = True < (x: = and F(x) = False = My(x)=
Completeness. For any SMT formula F, CLN model M can be constructed representing that formula. In other words, CLNs can express all SMT formulas on integers and reals.
We further prove that CLNs are guaranteed to converge to a globally optimal solution for formulas, which can be expressed as the conjunction of linear equalities. We provide formal definitions and proofs for soundness and completeness in Appendix B and optimality in Appendix C
LOOP INVARIANT LEARNING
inference system for loop invariants, CLN2INV, which leams invariants directly from execution traces. CLN2INV follows the same overall process as other loop invariant inference systems such as LoopInyGen and Code2Inv it iterates through likely candidate invariants and checks its validity with an SMT solver. The key difference between our method and other systems is that it learns a loop invariant formula directly from trace data. Figure 3 provides an overview of the architecture.
We use CLNs to implement
Preprocessing. We first perform static analysis and instrument the program prepare for train- ing data generation. In addition to collecting the given precondition and post-condition, the static analysis extracts all constants in the program, along with the loop termination condition. We then instrument the program to record all program variables before each loop execution and after the loop termination. We also restrict the loop to terminate after a set number of iterations to prevent loops running indefinitely (for experiments in this paper, set the max loop iterations to 50). We also strengthen the precondition to ensure loop exccution (see Appendix D).
Training Data Generation. We generate training data by running the program repeatedly on set of randomly initialized inputs that satisfy the preconditions. Unconstrained variables are initialized from a uniform distribution centered 0 with width r, where r is a hyperparameter of the sampling process. Variables with either upper or lower bound precondition constraints are initialized from uniform distribution adjacent their constraints with width r, while variables with both upper

---

Published as a conference paper at ICLR 2020
Sample Data
Model
Predicted Invariant
Code
(1 0) V
Ma0
Salver
Checks
SMT Template
Template
P = J (1(C)(() IA-C =
Generation
(((gt + Mil 0) (wet ugu m 0))
Training Data and Template Generation
CLN Construction and Trsining
Inveriant Checking
Figure 3: System architecture and CLN construction from SMT templates.
and lower bounds in the precondition are sampled uniformly within their bounds. For of our experiments in this paper, set to 10. When the number of uninitialized variables is small (i.e., less than 3), we perform this sampling exhaustively, An example of training data generation is provided in Appendix B
Template Generation. We generate templates three stages with increasing expressiveness:
1. We first generate templates directly from the pre-condition and post-condition.
2. We next extract the individual clauses from the pre- and post-condition well as the loop condition, and generate templates from conjunctions and disjunctions of each possible pair of clauses.
3. We finally generate more generic templates of increasing complexity with a combination of more equality constraints on all variables combined with conjunctions of inequality constraints, which are based on the loop condition and individual variables.
We describe the template generation in detail in Appendix E To detect when higher order terms may be present in the invariant, we perform log-log linear regression on each variable relative to the loop iteration, similarly to Sharma et al. (2013). If the loop contains one or more variables that grow superlinearly relative to the loop iteration, we add higher order polynomial terms the equality constraints in the template, up to the highest degree detected among the loop variables.
CLN Construction and Training. Once a template formula has been generated, a CLN con- structed from the template using the formulation in 4 As an optimization, we represent equality constraints as Gaussian-like functions that retain global maximum when the constraint is satisfied as discussed in Appendix F
We then train the model using the collected execution traces.
Invariant Checking. Invariant checking is performed using SMT solvers such as Z3 (De Moura & Bjørner 2008). After the CLN for formula template has been trained, the SMT formula for the loop invariant is recovered by normalizing the learned parameters. The invariant is checked against the pre, post, and inductive conditions described in 22.1 If the correct invariant is not found, return to the template generation phase to continue the search with a more expressive template.
EXPERIMENTS
We compare the performance CLN2INV with two existing methods and demonstrate the efficacy of the method on several more difficult problems. Finally, we conduct two ablation studies to justify our design choices.
Test Environment. All experiments are performed an Ubuntu 18.04 server with an Intel Xeon E5-2623 v4 2.60GHz CPU, 256Gb of memory, and an Nvidia GTX 1080Ti GPU.
System Configuration. We implement CLNs in PyTorch and use the Adam optimizer for training with learning rate 0.01 (Paszke et al. 2017]] Kingma & Ba 2014). Because the performance of CLN dependent weight initialization, the CLN training randomly restart if the model does not reach termination within 2, 000 epochs. Learnable parameters are initialized from a uniform distribution in the range [-1, 1]. which we found works well in practice.

---

Published as a conference paper at ICLR 2020
Test Dataset. We use the same benchmark used in the evaluation of Code2Inv. We have removed nine invalid programs from Code2Inv's 's benchmark and test on the remaining 124. The removed pro- grams are invalid because there inputs which satisfy the precondition but result in violation of the post-condition. See Appendix [ for details on the removed problems. The benchmark consists of loops expressed C code and corresponding SMT files. Each loop have nested if-then-else blocks (without nested loops). Programs in the benchmark may also have uninterpreted functions with boolean return values (emulating external function calls) in branches or loop termination con- ditions.
6.1 COMPARISON TO EXISTING SOLVERS
Codtziev
Gen
Number of Z3 Calls
1023 So
Runtime
300
26
22
00
100
:20
40
60
60
102
122
Number of Instances Solved
Number of Instances Solved
(a) Runtime performance.
(b) SMT solver calls.
Figure 4: Performance evaluation.
Performance Comparison. We compare CLN2INV two state-of saate-of-ther of-thh--rttrr--- art methods: Code2Inv (based neural code representation and reinforcement learning) and LoopInv (PAC learning over synthesized CNF formulas) (Si al., 2018 Padhi Millstein 2017). We limit each method to one hour per problem in the same format as the SyGuS Competition (Alur et al. 2019). CLN2INV is able to solve all 124 problems in the benchmark. LoopInvGen solves 104 problems while Code2inv solves 90
Figure a shows the measured runtime on each evaluated system. CLN2INV solves problems in 1.1 second average, which is over 40x faster than LoopInvGen, the second fastest system in the evaluation. It spends the most time on solver calls (0.6s avg.) and CLN training (0.5s avg.), with negligible time spent on preprocessing, data generation, and template generation each problem ( less than 20ms ea.
In Table we provide more detailed analysis of how much time is spent on each stage of the invariant inference pipeline in CLN2INV. Measurements are averaged over runs. The system spends most time on solver calls (0.6s avg.) and CLN training (0.5s on avg.) with negligible time spent on preprocessing, sampling, and template generation. For most problems in the Code2Inv benchmark, CLN2INV completes CLN training quickly (less than 0.2s) and spends most of its time performing solver checks, but it requires more epochs to train on some complex problems with many variables.
Table 1: Time spent on each stage of CLN2INV Pipeline.
Preprocessing
Sampling
Template Gen.
CLN Training
Checking
Avg. Time Max Time
5ms
2ms
4ms
0.5s
0.6s
18ms
12ms
8ms
7.2s
5.3s
In general, CLN2INV has similar performance to LoopInyGen on simple problems but is able to scale efficiently to complex problems. Figure 4bishows the number of Z3 calls made by each method.
'The Code2Iny authors originally reported solving 92 problems using the same hour timeout. We helieve that the difference may be caused by changes the testing environment or randomized model initial- ization.
At most 6171 data points are generated for given program in the henchmark, and 1041 data points per program average, using the sampling strategy 85.
8

---

Published as a conference paper at ICLR 2020
Table 2: Results and summary statisties for performance evaluation.
Method
Number Solved
Avg Time (s)
Avg 7.3 Calls
Time/7.3 Call (s)
Code2Inv
90
266.71
16.62
50.89
LoopInvGen
104
45.11
3,605.43
0.08
CLN2INV
124
1.07
31.77
0.17
For almost all problems, CLN2INV requires fewer Z3 calls than the other systems, although for some difficult problems it uses more Z3 calls than Code2Inv.
Table summarizes results of the performance evaluation. Code2Inv require much more time on average per problem, but minimizes the number of calls made to an SMT solver. In contrast, Loop- InvGen is efficient at generating a large volume of guessed candidate invariants, but is much less ac- curate for each individual invariant. CLN2INV can be seen balance between the two approaches: searches over candidate invariants more quickly than Code2Inv, but generates more accurate variants than LoopInvGen, resulting in lower overall runtime.
6.2 MORE DIFFICULT LOOP INVARIANTS
We consider two classes of more difficult loop invariant inference problems that are not present in the Code2Inv dataset. The first require conjunctions and disjunctions of multivariable constraints, and the second require polynomials with many higher order terms. Both of these classes of problems are significantly more challenging because they are more complex and cause the space of possible invariants to grow much more quickly.
To evaluate on problems that require invariants with conjunctions and disjunctions of multivariable constraints, construct 12 additional problems. We specifically design these problems to contain loops with invariants that cannot be easily inferred with pre- and post-condition based heuristics. In this section Figure 5 show one of these problems. By plotting the trace as shown in Figure it is easy to see that the points lie on one of the two lines expressible as linear equality constraints. The correct loop invariant for the program ((t + u = 0) V (t u = 0)) A (u s O).
//rre: t=-20/uu=-20
20
while (u 1= 0) { utt;
if (t 0)
else 1;
0
1;
//post: t=0
-20
-20 -15
-10 -5
(a) Pseudocode for Problem
(b) Plotte trace of program
Figure 5: Finding the loop invariant for Problem 1, which involves disjunction of equalities
Another problem with multivariable conjunction is shown in Figure In this program, we use unknown to denote external function call that returns either true false. As cannot assume much about the function, we model the function call as sampling from Bernoulli distribution with success probability 0.5. Although the branching behavior is may not be deterministic,
know (t + u 0) A (u + uo 0) A (u + w 2 0) is a correct invariant, as it holds regardless of which branch is taken. Our CLN2INV can learn this invariant within 20 seconds, while both Code2inv and LoopInvGen time out after one hour without finding a solution.
To evaluate on problems with higher order polynomial invariants, summation problems the form u Σi= td for a given degree which have been used in evaluation for polyonomial loop invariant inference (Sharma et al. 2013 Nguyen et al. 2017). We discuss these problems in more detail in Appendix [ CLN2INV can correctly learn the invariant for 1tt and 2nd order power summations, but cannot learn correct invariants for 3rd, 4th 5th order
CLN2INV on the power

---

Published as a conference paper at ICLR 2020
//pre: t=-10 A u=10 A v=-10 / w=10
while (u + w > 0) { if (unknown
L++; u-
} else W+t; w--;
//post: taw / u
Figure Pseudocode for Problem which involves conjunction of equalities
summations, which have many more higher order terms. We do not evaluate the other methods on these problems because they are not configured for nonlinear arithmetic by default.
6.3 ABLATION STUDIES
Effect of CLN Training on Performance. CLN2INV relies on combination of heuristics using static analysis and learning formulas from execution traces to correctly infer loop invariants. In this ablation we disable model training and limit CLN2INV to static models with no learnable pa- rameters. Static CLN2INV solves 91 problems the dataset. Figure Souure/hhor shows a comparison of full CLN2INV with one limited to static models. CLN2INV's performance with training disabled shows that a large number of problems in the dataset are relatively simple and can be inferred from basic heuristics. However, for more difficult problems, CLN learning is key inferring correct invariants.
Full CLN2INV Static CLN2INV
Full CLNZINV
10a
Number of 23 Calls
Static CUN2INV
10a
Runtime (3)
10:
101
10a
40
100
20
120
Number Instances Solved
Number of Instances Solved
(a) Runtime performance.
(b) SMT solver calls.
Figure 7: Ablation study comparing static vs trained models.
CONCLUSION
We develop novel neural architecture that explicitly and precisely learns SMT formulas by con- struction. We achieve this by introducing new sound and complete semantic mapping for SMT that enables learning formulas through backpropagation. We use CLNs implement a loop invari- ant inference system, CLN2INV, that is the first to solve all theoretically solvable problems in the Code2Inv benchmark and takes only 1.1 second on average. We believe that the CLN architccture will also be beneficial for other domains that require learning SMT formulas.
ACKNOWLEDGMENTS
This work is sponsored in part by NSF grants CNS-18-42456, CNS-18-01426, CNS-16-17670, CCF-1918400; ONR grant N00014-17-1-2010; an ARL Young Investigator (YIP) award: an NSF CAREER award; Google Faculty Fellowship; a Capital One Research Grant; J.P. Morgan Fac- ulty Award; a Columbia- IBM Center Seed Grant Award; and Qtum Foundation Research Gift. Any opinions, findings, conclusions, recommendations expressed herein those of the authors, and do not necessarily reflect those of the US Government, ONR, ARL, NSF, Google, Capital One J.P. Morgan, IBM, Qtum.
10

---

Published as a conference paper at ICLR 2020
REFERENCES
Rajeev Alur, Dana Fisman, Saswat Padhi, Rishabh Singh, and Abhishek Udupa. Sygus-comp 2018: Results and analysis. CoRR, abs/1904.07146, 2019. URL UtL.ttpp///avxiv.orr//b//// 07146
Saced Amizadch, Sergiy Matusevych, and Markus Weimer. Learning to solve circuit-SAT: An unsupervised differentiable approach. In International Conference on Learning Representations, 2019.
M. Gethsiyal Augasta and T. Kathirvalavakumar. Rule extraction from neural networks a compara- tive study. International Conference on Pattern Recognition, Informatics and Medical Engineer- ing (PRIME-2012), pp. 404-408, 2012.
Mislav Balunovic, Pavol Bielik, and Martin Vechev. Learning to solve smt formulas. In Advances in Neural Information Processing Systems, pp. 10317-10328, 2018
A. Biere, H. Maaren, and T. Walsh. Handbook of Satisfiabilit;: Volume 185 Frontiers in Arti- ficial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, The Netherlands, 2009. ISBN 1586039296, 978 158603929..
Andreas Blass and Yuri Gurevich. Inadequacy of computable loop invariants. ACM Transactions on Computational Logic (TOCL), 2(1):1-11, 2001.
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying concurrent, crash-safe systems with perennial. In Proceedings of the 27th Symposium on Operating Systems Principles. ACM, 2019.
Leonardo De Moura and Nikolaj Bjørner. Z3: efficient smi solver. In International conference Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340, Springer, 2008.
Andreas Eggers, Martin Fränzle, and Christian Herde. Sat modulo ode: A direct sat approach to hybrid systems. In International Symposium on Automated Technology for Verification and Analysis, pp. 171-185. Springer, 2008.
Richard Evans and Edward Grefenstette. Learning explanatory rules from noisy data. Journal of Artificial Intelligence Research, 61:1-64, 2018
Mare Fischer, Mislav Balunovic, Dana Drachsler-Cohen, Timon Gehr, Ce Zhang, and Martin Vechev. DI2: Training and querying neural networks with logic. In International Conference on Machine Learning, pp. 1931-1941, 2019.
Carlo A Furia. Bertrand Meyer, and Sergey Velder. Loop invariants: Analysis, classification, and examples. ACM Computing Surveys (CSUR), 46(3):34, 2014.
Juan Galeotti, Carlo A Furia, Eva May, Gordon Fraser, and Andreas Zeller. Inferring loop in- variants mutation, dynamic analysis, and static checking. IEEE Transactions Software Engineering, 41 1100::100191003 2015.
Ian Goodfellow. Yoshua Bengio, and Aaron Courville, Deep learning. MIT press, 2016.
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. Certikos: An extensible architecture for building certified concurrent os kernels. In 12th USENIX Symposium Operating Systems Design and Implementation (OSDI), pp. 653- 669, 2016.
Petr Hájek. Metamathematics of fuzzy logic, volume 4. Springer Science & Business Media, 2013.
Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10)557-5880 1969.
Kurt Homik, Maxwell Stinchcombe, and Halbert White. Multilayer feedforward networks are uni- versal approximators. Neural nefworks, 2(5):359-366, 1989.

---

Published as a conference paper at ICLR 2020
J Kearns, Umesh Virkumar Vazirani, and Umesh Vazirani. An introduction computational learning theory. MIT press, 1994.
Angelika Kimmig, Stephen Bach, Matthias Broecheler, Bert Huang, and Lise Getoor. A short introduction to probabilistic soft logic. In Proceedings of the NIPS Workshop on Probabilistic Programming: Foundations and Applications, pp. 1-4, 2012.
Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint 1412.6980 2014.
Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Tor- lak, and Xi Wang. Hyperkemel: Push-button verification of an os kernel. In Proceedings of the 26th Symposium on Operating Systems Principles, pp. 252-269. ACM, 2017.
Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Scaling symbolic evaluation for automated verification systems code with serval. In Symposiun on Operating Systems Principles, 2019.
Tu Nguyen, Timos Antonopoulos, Andrew Ruef, and Michael Hicks. Counterexample-guide approach to finding numerical invariants. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, pp. 605-615, ACM, 2017.
Pierluigi Nuzzo, Alberto Puggelli, Sanjit A Seshia, and Alberto Sangiovanni- Vincentelli. Cales: Smt solving for non-linear convex constraints. In Formal Methods in Computer Aided Design, pp. 71-79. IEEE, 2010.
Sangiovanni-Vincettlli.
Saswat Padhi and Todd D. Millstein. Data-driven loop invariant inference with automatic feature synthesis. CoRR, abs/1707.02029, 2017. URL
107. 02029
Saswat Padhi, Rahul Sharma, and Todd Millstein. Data-driven precondition inference with learned features. ACM SIGPLAN Notices, (6):425,, 2016.
Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary Detito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in pytorch. 2017.
Ali Payani and Faramarz Fekri. Inductive logic programming via differentiable deep neural logic networks. arXiv preprint arXiv: (eee:/90600355 2019.
Daniel Selsam and Nikolaj Bjömer. Guiding high-performance sat solvers with unsat-core pre- dictions. In International Conference on Theory and Applications of Satisfiability Testing, pp. 336-353. Springer, 2019.
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning SAT solver from supervision..... In International Conference Learning Representations, 2019. URL sattps://ont //tpen/eewe/eee.eeeeeee net wwr.mrorriioo -iMHHMMC iA5tm
Rahul Sharma and Alex Aiken. From invariant checking to invariant inference using randomized search. Formal Methods in System Design, 48(3):235-256, 2016.
Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, and Aditya Nori. A data driven approach for algebraic loop invariants. In European Symposium Programming, pp- 572-592. Springer, 2013.
Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. Learning loop invariants for program verification. In Advances in Neural Information Processing Systems, pp. 7751-7762, 2018.
James R Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D Ernst, and Thomas Anderson. Verdi: a framework for implementing and formally verifying distributed systems. ACM SIGPLAN Notices, 5066):357-368, 2015.
12

---

Published as a conference paper at ICLR 2020
A PROOF OF LIMIT OF S(t u)
1 t=
lim S(1=w) u)
lim + 1 e- B(t-u+e) + Ble-u-0
t
B-c-+000
Proof. Let [(t, u; B,t) Ite Bü any and g(l, u; B,t) Itebli
Then what want
prove becomes
{
t=
lim (f(t,u; c, @ gtt u: B.))) e-0+
t t u
B-c
Because all g. are continuous in their domain, have
lim (f(t, uz B, c)
g(t, u; B,c))
lim f(t, u; B,c) Bic-++00
x
lim glt, u; B,c)
5o
Bic
Using basic algebra, we get
1 12 L<u
{
1 ISu u
lim ut, {
lim glt, u; B,E)
1>
-07
+00
Bic++00
Combing these results, we have
0 < u
lim f(t, u; B) -- Bic-++00
lim gt, B)e)
101 = u
-- Bic-+oo
180
t> u
For any I-norm, have 1
2 1, and 10 0. Put altogether, have
{
t=
lim (S(1, u; B,e) @ ,(l, u: B,e)) ++
t
B-c-+to
which concludes the proof.
B SOUNDNESS AND COMPLETENESS OF CLNS
In this section we provide formal descriptions and proofs of CLN soundness and completeness when trained to 0 loss. These properties are defined for CLNs as follows:
Soundness. Given the SMT formula F, the CLN model Mr constructed from S(F) always preserves the truth value of F. It indicates that given a valid assignment to the terms x in F, F(z) True < MM(xx)
and F(x)) False > Mr(x)=
Completeness. For any SMT formula F, CLN model M can be constructed representing that formula. In other words, CLNS can express SMT formulas on integers and reals.
We formally state these properties in Theorem 1. Before that we need to define property for t-norms.
Property 1. Vt u, (t 0) and (u > 0) implies (t 2 > 0).
The product t-norm and Godel t-norm have this property, while the Lukasiewicz t-norm does not. Theorem 1. For any quantifier-free linear SMT formula F, there exists CLN model M, such that
Væ B 0 M (x; B,e) 2
Va, F(x)= True +
lim M(x; B, = B-c+00
(2)
Yx, F(z) False - lim
M(x: B,c)
(3)
5 B.0+00
long the t-norm used in building M satisfies Property 1.
13

---

Published as a conference paper at ICLR 2020
Proof. For convenience of the proof, first remove all <, -. and * in F, by transforming
t < u into -(t 2 u), t S u into -(t > u), t = u into (t 2 u) A ((t > u), and * u into (t > u) V -(t 2 u). Now the only operators that F may contain are >, 2, We prove Theorem 1 by induction on the constructor of formula F. In the following proof, we construct model M given F and show that satisfied (q)()) We leave the proof for why M also satisfied
(3) to readers.
Atomic Case. When F is an atomic clause, then F will be in the form of * W + > 0 or x x W - 2 0. For the first case, we construct a linear layer with weight W and bias b followed by sigmoid function scaled with factor B and right-shifted with distance c. For the second case, we construct the same linear layer followed by sigmoid function scaled with factor B and left-shifted with distance 6. Simply evaluating the limits for each we arrive at
Vo, F()) = True
lim (æ;; B, =1
B.c-00
And from the definition of sigmoid function we know 0 S M(;; B,t) S1.
Negation Case If F = FF' from the induction hypothesis, F" can be represented by models M' satisfying (3)())))), Let p' output node of M'. We add a final output node p = 1- p'. So (æ; B, e) = 1- M B, e). Using the induction hypothesis 0 S M(; e) S 1, we conclude Eq) 0 S M(:: B,c) S
Now we prove the " = side of Eq.(2), If F(x) = True, then F'(x)) False. From the induction hypothesis, we know lim (x; c. So
Bic-00
lim M(x; B,c) 5-0+
lim
1- 1-M B) = 1-
+-0+
8.0000
Bic-200
Next we prove the side. If lim --50l
(x:; B,E) 1, we have
lim
Mx: B,c) lim
1- -10=-11))11111
++t
+
Boc-oo
B-c-100
From the induction hypothesis we know that F'(x) = False. So - ((x)==F((a) = True.
Conjunction Case. If F = F1 A Fz, from the induction hypothesis, F1 and F2 can be represented by models M, and M2. such that both (F).M,) and M2) satisfy ())))))) Let p1 and P2 be the output nodes of M1 and M2. We add final output node p = P1 69 p2- So M(r; B, (a;; B,c) e) s M2(2;; B,e). Since (00) continuous and so are M1 (2;; B,e) e) and M2(æ; B, c), we know their composition M (x; B,e) is also continuous. (Readers may wonder why M1(x; B, is continuous. Actually the continuity of (x; B, e) should be proved inductively like this proof itself, and we omit it for brevity.) From the definition of (8), have Eq.(1) 0 < M(:; B, 1 1.
Now we prove the + side of (2). For any σ, if F(z) = True which means both (x = True and (x True, from the induction hypothesis we know that lim c+t M1 B,e)
Be--000
and lim 0-0
M2 B,c) = 1. Then
B-0-000
lim M(x; B,c) lim M,(x; @ -
-
B-0000
B--+00
Then we prove the = side. From the induction hypothesis we know that (a; B.c) I 1 and
M2(w; B,e) < 1. From the non-decreasing property of t-norms (see 22.) we have
Mi (æ; B,e) @ M2(1;; B,e) S (x; B,e) 8
Then from the consistency property and the commutative property, we have Mi B,e) M1
Put them altogether we get
M(x; B,c) < (1; B,c) S
14

---

Published as a conference paper at ICLR 2020
Because we know lim ++0 Bic-000
[(= 1, according the squeeze theorem in calculus, get
lim
Mi (1 B,c) =1
s-t Bic-toc
From the induction hypothesis, we know that (2: True. We can prove F2(x) True in the same manner. Finally we have (xx = Fi A (2 = True.
Disjunction Case. For the case F F1 F2, we construct M from M1 and M2 as we did in the conjunctive case. This time we let the final output node be p = P1 + P2. From the continuity of (8) and the definition of (+) (t @ a
(1 t) @ (1 u)). (#) is also continuous. We conclude (æ;; B, c) is also continuous and 0 S (a: B, S by the same argument as F = Fi A F2.
Now we prove the = side of Eq.(2). For any assignment æ, if F(x) True which means Fi (a) True F2 (a) True. Without loss of generality, we assume Fi (æ) True. From the induction hypothesis, we know lirm c0t Mi (æ;; e)
Bie-+00
For any (+) and any 0 S t,t' < ift t', then
t 1 (1- @ (1 u) 1 1- (1()))) u) = ou
Using this property and the induction hypothesis M2; B,c) 2 0, have
(a; B,c) @0
s M1 B,c M2(2; B) M(x; B.c)
[z: B, c) S Using the definition of (#) and the From the induction hypothesis we also have M1 (2;
consistency of (8) (0@ 0), get Mi B, E) 0 Mi (æ; B, e). Put them altogether we get
Mi B,c) s M(x; B, 1
Because we know lim ++
Mi(a; B,c) according the squeeze theorem in calculus,
B.0+00
get lim 0 (x; = 1.
Bie-to
Then prove the - side. Here we need to use the existence of limit:
lim 0
M(x; B)
Bic+oc
This property can be proved by induction like this proof itself, thus omitted for brevity.
Let
C1 = lim (x; B,e)
C2 = lim
M2(æ; B,c)
++t
B.c-x0
Then
lim M( B,e) = lim Mi(x;B,e) M2(a; = - c1) 8 (1-10)) (2)
100000
Since we have lim +0t M(x; B,c) = 1, we get
B.c-000
(1 ( (2- =0
Using Property 1 of (8) (defined in have C₁ 1 V 1. Without loss of generality, assume Cj = 1. From the induction hypothesis, we know that Fi (xx) = Truc. Finally, F(x)) Fi(x) F2(x) True.
Careful readers may have found that if we the continuous mapping function S in 3 then have another perspective of the proof above, which can be viewed as two interwoven parts. The first part is that proved the following lemma.
15

---

Published as a conference paper at ICLR 2020
Corollary 1. For any quantifier-fre linear SMT formula F.
Væ B 0 5 S(F; B, ()(x) -
Va, F(x) = True = lim
S(F; B, () =
8.0-000
Va, F(x) False
lim
S(F; B, e)(()
B.-+00
Corollary indicates the soundness of S. The second part is that construct CLN model given S(F). In other words, we translate (FF) into vertices computational graph composed of differ- entiable operations continuous truth values.
C OPTIMALITY OF CLNS
Optimality, For subset of SMT formulas (conjunctions of multiple linear equalities), CLNs guaranteed to converge at the global minimum. We formally state this in Theorem We first define another property similar striet monotonicity.
Property 2. Vh 1/ l3, (41 < (2) and (1s > 0) implies (t1 @ t3 < l2 & tt).
Theorem 2. For any CLN model Mp constructed from formula, F, by the procedure shown in the proof of Theorem Mr the global minimum, long the t-norm used in building Mr satisfies Property 2.
the conjunction multiple linear equalities then any local minimum of
Proof. Since F is the conjunction of linear equalities, it has the form
Wiyli 0)
Here W - are the learnable weights, and {fij} are terms (variables). We omit the bias by in the linear equalities, the bias can always be transformed into weight by adding a constant of as term. For convenience, we define f(x) S(x = 0) 1+e-
[+e"(--o
Given assignment æ of the terms {fij J. if we construct our CLN model Mr following the proce- dure shown the proof of Theorem 1, the output of the model will be
M(#; W, B,c) =
We 1z))
1=1
When we train our CLN model, we have a collection of m data points {tija): (typh.... [timm) which satisfy formula F. If B and e are fixed (unlcarnable), then the loss function will be
L(W)= Σ L(M(;; W, B,E) k=1
Σ
Wiy Wiylizk))
(4)
Suppose W = (wiz) is a local minima of L(W). We need to prove W also the global minima. To prove this, use the definition of local minima. That is,
38 > 0, vW, ||W W < = L(W) > L(W")
(5)
For convenience, we denote = E/= Wisttig..
Then we rewrite (4) as
L(W) Σ
f(usk)
If we prove W VI 15 k m, U4k 0. Then because (i) f reaches its global maximum at 0, (ii) the t-norm (8) monotonically increasing, (iii) monotonically decreasing, conclude that W is the global minima.
16

---

Published as a conference paper at ICLR 2020
Now prove A < i n. 1 m, u4k 0. Here we just show the case i 1. The proof for ? can be directly derived using the associativity of (8).
Let ag
2 12 (uux). Since f(x) for all a R, using Property 2 of our t-norm (&),
know that ar O. Now the loss function becomes
L L(W) Σ
((f(un)) 0xx)
k=
From (5), we have
M
30 < 8 1, Vy, 7 1 8
C(S(uxe) ((1l++)))))) & ax)
((((ux)) @ (04)
(6)
Because (i) fxx is an even function decreasing on x > (which can be easily proved), (ii) (0) is monotonically increasing, (iii) monotonically decreasing, for -8' <> < 0, we have
C(f(ua + +)) @ an) = [(f(lua + + @ oxx) -
R=1
R=1
m
C(f(lua)) @ ax)
Σ
[(f(ua) @ ax)
k=1
Combing (6) and Eq.(7), we have
m
Σ C(f(ua(1 + 2 ax) Σ C(f(ux) @ ak)
Now look back on Eq.( Since (i) C is strictly decreasing, (ii) the t-norm used here has Property (see | for definition), (iii) 0g > 0, the only case when (=) holds is that for all s l m, have ([ + 7)1)
[(maal) Since (xx is strietly decreasing for 2 0, have Ju (1 + 7)) = |ua] Finally because -1 < - < Y < O, we have us 0.
17

---

Published as a conference paper at ICLR 2020
D PRECONDITION STRENGTHENING
Theorem 3. Given a program C: assume P); while (I.C) {C} assent((): If we can find loop invariant 1' for program C": assume(P LC); while (LC) {C} assent(Q): and P A LC = Q, then V (P LCC) is a correct loop invariant for program C.
Proof. Since I' is a loop invariant of C¹, we have
(PALC)ALC LC = I' (a) ( (b) I'ALCC = Q (c)
We want to prove I' V (P -I.C) is valid loop invariant of C, which means
PALC = (P
(Q''v ACCCC
(VAA-LC)) -LC = Q
We prove the three propositions separately. To prove PA = PV (PA-A-I.)) we transform into stronger proposition P LC = I', which directly comes from (a).
For (('V(PA-LC)) LCCp-//o/)-CCC//////-/-----
after simplification it becomes (LALCCCAUV
(PA- -LC),, which is direct corollary of (b).
For (PV(PA-LC)) I' A -CC = Q and LCC =
LC = Q, after simplification it will become two separate propositions,
Q. The former is exactly (c), and the latter is a known
condition in the theorem.
E IMPLEMENTATION DETAILS
Training Data Generation Example. Figure 8 provides an example of our training data generation procedure. The uninitialized variable sampled according to the precondition k within the predefined width = 10. So we end up enumerating & = 8, 7,..., -2. For each k, the loop is executed repeatedly until termination, thus generating small set of samples. The final training set is the union of these small sets.
/ //pre: t=10
// run run with k=
//pre: u=0
= atoi (argv
//pre: k<=8
t-10; u-0;
//invariant: 2t+u=20 while [t != k)
while (t != k)
leg u, k);
t tt- 1;
t - 1;
== x=utz 2;
u= u 2;
/ /post: u=20-2k
log (t, u, k)
(a) The original loop program.
(b) The sampling procedure.
Figure 8: Illustration of how training data is generated. After the sampling procedure (b) we have collection of 88 samples which will later be fed to the CLN model.
Template Generation. Templates are first generated from the pre- and post-conditions, followed by every pair of clauses extracted from the precondition, post-condition, and loop condition. Generic templates are then constructed consisting of one or more general equality constraints containing all variables conjoined with inequality constraints.
Three iterations of the generic template generation are shown here:
(W,X = a1) A (x) S wi) A (a1 24) A .... (an S u,) A (sn 2 1n)
2: ((W, = a1) A (W2X- = =2)) A (x1 < un) A (Ii 2 h)) A A... (xn S un) A (In > In) 3: (WW, = a1) (W,X- = a2)) (α) S wn) (I) 2 1)) A..AA A S n. (x, 2 1.)
Algorithm summarizes the template generation process. In it the following functions defined:
18

---

Published as a conference paper at ICLR 2020
construct template:
Construct a template given an formula.
extract extract.clausee clauses:
Extract individual clauses from smt formulas.
estimate. estimate_degrees: _degrees:
Performs log-log linear regression to estimate degree of each variable.
polynomial kernel:
Executes polynomial kernel variables and data for a given degree. Checks condition a single inequality constraint.
single constraint:
Converts the loop condition to learnable smt template.
Note that templates are generated on demand, so each template is used to infer a possible invariant before the next is generated.
Algorithm Template Generation Algorithm.
Input:
Pre +- precondition
Post + post-condition
LC + loop condition
Max Template Len
max template eq
clauses
vars f- vars program
X -ratninngg data
construct template(Post)
2: construct (emplat((r)
3: clauses f- extract extract_clauses clauses((Pe,, Post, LC)
4: for (c1, 62) in all pairssccluussss do
5: construct.templatee A c2)
6:
construct.templateeel V c2)
7: end for
8: mar degree estimatt degrees(X)
9: if max degree > then
10:
mex_degree)
11: end if
()
13: for var in vars do
constracnss bontriinsss (var S Uvar)
15: bound constrains
contrainss A (var [par)
end for 17: if iissingle__cnssttts Sonngle_constaann((IC.. L.C) then
18:
bound_comstraints + otw.:n/..ctttttottccccc.ooooooo.
19: end if
20: construct templateee) vars = b)) A bound.constraints)
21: eq clausessssss... +- [(W vars = b)]
22: lemplate.en 4
23: while lemplateJen MMaxTemplaee__es do
24: for eq_elause in eq_clauses do
construct.eemplateeeeeeeeee
(W. vars b)) bound.comstraints)
26:
eq clauses + [eq clauses, eq clause A (W cars b)]
construct template((eq clause (W. vars = b)) A bound loundd_omstraints)
28: eq_clauses t [eq_clauses, eg eq_clause V (W cars b)]
29:
end for
30:
template_len <- template +
31: end while
19

---

Published as a conference paper at ICLR 2020
F PROPERTIES OF GAUSSIAN FUNCTION
We use Gaussian-like function S(t = u) exp(- exp(- (t-w)²
202 to represent equalities in our exper-
iments. It has the following two properties. First, preserves the original semantic of when + O, similar to the mapping S(t = u) Ite mit-u+]
X Ite"(--->) we defined in
(1 (1-w)² =
1 t ==
lim exp( 0
20²
0
+
Second, if we view S(t = u) as a function over u, then reaches its only local maximum at t 0, which means the equality is satisfied.
G INVALID PROBLEMS FROM CODE2INV DATASET
Here we provide an example which Problem 106 in the dataset. The post-condition a 2 m is wrong if we start from 0, m 1, and k = 0.
int k 0;
int a, mi
assume (a <= m)
while (k < 1)
if (m a) m = a;
k 1;
assert (a >= m);
Executing the program with these inputs results in 0, m 1, and k 1 as the if condi- tion is never satisfied. But clearly, the post condition 2 m is violated. Below we tabulate the counterexamples invalidating the nine removed problems from the dataset:
Table 3: Invalid problems from Code2Inv dataset
Problem
Counterexample starting state
26
nl 0,0
x, n 0,
31
I, n = 0,0
32
= 0,
61
C, 0, 1
62
C, n 0,
72
C, y = 0, 128
75
C. = 0, 128
106
a, 0,1,0
H POLYNOMIAL INVARIANTS
Here we provide results and an example of the higher order polynomial problems; more precisely, the power summation problems in the form Ek= td for given degree d. We found that CLN2INV was able to learn invariants for programs which computes the sum of consecutive in- tegers, which has 10 monomial terms and a maximum degree of 2. Since CLN2INV simply uses the polynomial kernel the number of terms quickly become unwieldy. We observe that CLN2INV struggles beginning with of squares, which has 20 monomial terms up degree 3. Table 4 summarizes these results.
For further illustration, describe in detail the where dl is i.e. sum of cubes.
20

---

Published as a conference paper at ICLR 2020
Table Results on power summation polynomial problems.
Number Terms
Highest Degree
Solved?
10
2
20
3
X
35
4
X
56
5
X
//pre: t = = A 0=
while (t < k) {
tt+i
u += tottt + E;
/ppost: 4u k**2 (k + 1) **2
Figure 9: Pseudocode for Polynomial Invariant Problem
The example loop in Figure computes the of the first & cubes. We know this has closed form solution:
() + + k.
==0
For this problem, we would hope to extract the invariant:
(4u 14 + 213 + ((
However, by naively using the polynomial kernel just as methods like NumInv suggest (Nguyen al. 2017), we will have 35 monomials of degree at most four over three variables candidate terms (t u, f22 tu?,...., and the model must learn to ignore all the terms except u, t t3, and t². We observe our model finds far more accurate coefficient for t but than for lower ordered terms. We hypothesize that by nature of polynomials the highest order term is good approximation for the whole polynomial. Thus, ( is good approximation based on the data. The difficulty of learning polynomial invariants using CLN is an interesting direction for future studies.
21


Reviews:
[{"review_id": "rklrlliQjS", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Summary:\n\nThis paper introduces a novel way to find loop invariants for a\nprogram. The loop invariants are expressed as SMT formulas. A\ncontinuous relaxation of an SMT solver is introduces mapping\nevery SMT formula onto a truth value \\in [0, 1]. This relaxation\ncalled a continuous semantic mapping is decided such that every\ntrue formula has a higher value than every false formula. This\nallows an invariant to be learned.\n\nNovelty and Significance:\n\nThis work is interesting and although authors do seem to be\noutside of the community, I firmly believe is appropriate for\nICLR. If the claims made by the paper are true they constitute\na significant contribution to the field of program synthesis\nand program analysis.\n\nTechnical Quality:\n\nThe evaluation was fairly thorough, but the paper can be\nstrengthened massively with a few small changes and additions.\nIt might be more helpful if there was a sense of how many problems\nnone of the systems can do and how complicated of a program can\nthis system extract a loop invariant from. Why were was it these\nparticular 12 that work? Are there examples that don't?\n\nI don't know why all this time is spent on t-norms when behavior\non them is fairly similar and the simplest norm works best.\n\nLots of details are missing in this paper. How much training data\nwas generated? How long did it take? Does training data need to\nbe generated for each example? If so is that included in the\nruntime for Figure 3?\n\nThe paper talks about neural architecture, but all I see is\neffectively a curve-fitting task for some template. This feels\ndifferent from the code2inv paper where a program can be fed\ninto the system and the pretrained model emits the invariant.\n\nClarity:\n\nNot enough of this paper concentrates on the novel aspects of the\napproach. Section 5 discusses template generation, but not in\nenough detail that I would be able to replicate this work. I\ncould also not find enough details in the Appendix.\n\nI don't know why vital page space is spent on defining completeness\nand soundness.\n\n\nPossibly related work as relaxations to SAT/SMT solvers do exist in the literature.\n\nGuiding High-Performance SAT Solvers with Unsat-Core Predictions\nhttps://arxiv.org/abs/1903.04671\n\nLearning to Solve SMT Formulas\nhttps://papers.nips.cc/paper/8233-learning-to-solve-smt-formulas.pdf\n\nNotes:\n\nYou cite Si et al. for LoopInvGen when you should be citing Pathi\nand Millstein in the third paragraph on page 2.\n", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "SygB2FUk5r", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The domain is loop invariant detection, in the static program analysis space. Loop invariants hold before, during, and after loop execution, and can be useful for compiler optimizations and/or correctness checking. \nThe paper explains Basic Fuzzy Logic and then uses it to introduce Continuous Satisfiability Modulo Theories, including proposed continuous mappings for inequalities (>, >=), negations, equalities, and requirements of t-norms to be useful for the relaxated optimization proposed. This Continuous Logic Network is then optimized to provide invariant proposals to Z3, an SMT solver. The whole system is used to solve the entire Code2Inv benchmark set, in substantially faster time and with fewer proposals to Z3 than comparable previous approaches. Ablations are provided which study the t-norm used (3 options considered), and another which uses heuristics only with no training/optimization to make static proposals to Z3. \n\nOn the whole, I like the presentation and the thinking here, and think it will be interesting to folks in the field, possibly spurring on further thinking in compilers, program synthesis, constrained optimization, etc, so recommend accepting. \n\nRelaxed representations of satisfiability problems seems like something people have thought about in OR for some time, so I wonder if there is a missing part of the literature survey. A cursory glance turns up https://openreview.net/forum?id=BJxgz2R9t7 \n\nInterestingly, the heuristics do quite well, which calls into question how hard the dataset is, and how competitive the preceding works really were. Since these heuristics seem to be an important contributor to this approach, I think they deserve further discussion in the appendix, and/or source code should be released.\n\n9 problems from the dataset are rejected as invalid. Please identify these in an appendix, and provide the counterexamples.\n\nThe dataset used here is quite small, and it seems like only ~30 of the problems are \"hard\" in requiring beyond-heuristic complexity. Couldn't the SyGuS tools be used to generate a much larger test set?\n\nIn fig 2, the model (x) doesn't match the template/invariant \\/.", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper implements a novel architecture for inferring loop invariants in verification (though the paper bridges to compilers).  The idea is novel and the paper is well executed.  It is not the usual topic for ICLR, but not presents an important application of deep learning done well, and it has interesting implications for program synthesis.  Therefore, I recommend acceptance.
Decision: Accept (Poster)