NIL: Learning Nonlinear Interpolants
Mingshuai Chen1,2(B) , Jian Wang1,2 , Jie An3 , Bohua Zhan1,2(B) ,Deepak Kapur4 , and Naijun Zhan1,2(B)1State Key Laboratory of Computer Science,
Institute of Software, CAS, Beijing, China{chenms,bzhan,znj}@ios.ac.cn
2
University of Chinese Academy of Sciences, Beijing, China
3
School of Software Engineering, Tongji University, Shanghai, China
4
Department of Computer Science, University of New Mexico, Albuquerque, USA

Abstract. Nonlinear interpolants have been shown useful for the veriﬁcation of programs and hybrid systems in contexts of theorem proving,model checking, abstract interpretation, etc. The underlying synthesis
problem, however, is challenging and existing methods have limitations
on the form of formulae to be interpolated. We leverage classiﬁcation
techniques with space transformations and kernel tricks as establishedin the realm of machine learning, and present a counterexample-guided
method named NIL for synthesizing polynomial interpolants, thereby
yielding a uniﬁed framework tackling the interpolation problem for thegeneral quantiﬁer-free theory of nonlinear arithmetic, possibly involving
transcendental functions. We prove the soundness of NIL and propose
suﬃcient conditions under which NIL is guaranteed to converge, i.e.,the derived sequence of candidate interpolants converges to an actualinterpolant, and is complete, namely the algorithm terminates by producing an interpolant if there exists one. The applicability and eﬀectiveness of our technique are demonstrated experimentally on a collectionof representative benchmarks from the literature, where in particular,
our method suﬃces to address more interpolation tasks, including thosewith perturbations in parameters, and in many cases synthesizes simpler
interpolants compared with existing approaches.
Keywords: Nonlinear Craig interpolant ·Counterexample-guided learning · Program veriﬁcation ·Support vector machines (SVMs)

1

Introduction

Interpolation-based technique provides a powerful mechanism for local and modular reasoning, thereby improving scalability of various veriﬁcation techniques,This work has been supported through grants by NSFC under grant No. 61625206
and 61732001, by the CAS Pioneer Hundred Talents Program under grant No.
Y9RC585036, and by the National Science Foundation Award DMS-1217054.
c Springer Nature Switzerland AG 2019

P. Fontaine (Ed.): CADE 2019, LNAI 11716, pp. 178–196, 2019.
https://doi.org/10.1007/978-3-030-29436-6_11

NIL: Learning Nonlinear Interpolants

179e.g., theorem proving, model checking and abstract interpretation, to name justa few. The study of interpolation was pioneered by Krajı́ček [27] and Pudlák [35]in connection with theorem proving, by McMillan [30] in the context of model
checking, by Graf and Saı̈di [17], McMillan [31] and Henzinger et al. [20] pertaining to abstraction like CEGAR [8], and by Wang et al. [24] in the context
of learning-based invariant generation. Developing eﬃcient algorithms for generating interpolants for various theories and their combination has become an
active research area, see e.g., [7,25,26,31,32,36,46].
Though established methods addressing interpolant generation for Presburger arithmetic, decidable fragments of ﬁrst-order logic, theory of equality
over uninterpreted functions (EUFs) as well as their combination have been
extensively studied in the literature, there appears to be little work on synthesizing nonlinear interpolants. Dai et al. proposed an algorithm in [11] forgenerating interpolants for nonlinear polynomial inequalities based on the existence of a witness guaranteed by Stengle’s Positivstellensatz [16] that can becomputed using semi-deﬁnite programming (SDP). A major limitation of thismethod is that the two mutually contradictory formulas to be interpolated must
share the same set of variables. Okudono et al. extended [11] in [33] to caterfor the so-called sharper and simpler interpolants by developing a continuous
fraction-based algorithm that rounds oﬀ numerical solutions. In [14], Gan et al.
considered the interpolation for inequalities combined with EUFs by employing the hierarchical calculus framework proposed in [38] (and its extension [39]),
while the inequalities are limited to be of the concave quadratic form. In [15], Gao
and Zuﬀerey transformed proof traces from δ-complete decision procedures into
interpolants, composed of Boolean combinations of linear constraints, which candeal with certain transcendental functions beyond polynomials. The techniquesof encoding interpolants as logical combinations of linear constraints, including [15,28,37], however, yield potentially large interpolants (requiring even an
inﬁnite length in the worst case) and their usage thus becomes diﬃcult in practical applications (cf. Example 1).
Interpolants can be viewed as classiﬁers that distinguish, in the context ofprogram veriﬁcation for instance, positive program states from negative ones
(unreachable/error states) and consequently the state-of-the-art classiﬁcation
algorithms can be leveraged for synthesizing interpolants. The universal applicability of classiﬁcation techniques substantially extends the scope of theories
admitting interpolant generation. This idea was ﬁrst employed by Sharma et al.
in [37], which infers linear interpolants through hyperplane-classiﬁers generated
by support vector machines (SVMs) [3,45] whilst handles superﬁcial nonlinearities by assembling interpolants in the form purely of conjunctions (or dually,
disjunctions) of linear half-spaces, which addresses only a limited category of
formulae featuring nonlinearities. The learning-based paradigm has also been
exploited in the context of nonlinear constraint solving, see e.g., [12].
In this paper, we present a classiﬁcation-based learning method for the synthesis of polynomial interpolants for the quantiﬁer-free theory of nonlinear arithmetic. Our approach is based on techniques of space transformations and kernel tricks pertinent to SVMs that have been well-developed in the realm of

180

M. Chen et al.

machine learning. Our method is described by an algorithm called NIL (andits several variants) that adopts the counterexample-guided inductive synthesis
framework [22,40]. We prove the soundness of NIL and propose suﬃcient conditions under which NIL is guaranteed to converge, that is, the derived sequenceof classiﬁers (candidate interpolants) converges to an actual interpolant, and iscomplete, i.e., if an interpolant exists, the method terminates with an actualinterpolant. In contrast to related work on generation of nonlinear interpolants,
which restrict the input formulae, our technique provides a uniform framework,
tackling the interpolation problem for the general quantiﬁer-free theory of nonlinear arithmetic, possibly involving transcendental functions. The applicability and eﬀectiveness of NIL are demonstrated experimentally on a collection ofrepresentative benchmarks from the literature; as is evident from experimental
results, our method is able to address more demands on the nature of interpolants, including those with perturbations in parameters (due to the robustness inherited from SVMs); in many cases, it synthesizes simpler interpolants
compared with other approaches, as shown by the following example.
Example 1 ([15]). Consider two mutually contradictory inequalities φ = y ≥ x2and ψ = y ≤ − cos(x) + 0.8. Our NIL algorithm constructs a single polynomial
inequality I = 15x2 < 4 + 20y as the interpolant, namely, φ |= I and I ∧ ψ
is unsatisﬁable; while the interpolant generated by the approach in [15], only
when provided with suﬃciently large ﬁnite domains, e.g., x ∈ [−π, π] and y ∈[−0.2, π 2 ], is y > 1.8 ∨ (0.59 ≤ y ≤ 1.8 ∧ −1.35 ≤ x ≤ 1.35) ∨ (0.09 ≤ y <0.59 ∧ −0.77 ≤ x ≤ 0.77) ∨ (y ≥ 0 ∧ −0.3 ≤ x ≤ 0.3). As will be discussed later,
we do not need to provide a priori information to our algorithm such as bounds
on variables.
The rest of the paper is organized as follows. Section 2 introduces some preliminaries on Craig interpolants and SVMs. In Sect. 3, we present the NIL algorithm dedicated to synthesizing nonlinear interpolants, followed by the analysis
of its soundness, conditional completeness and convergence in Sect. 4. Section 5reports several implementation issues and experimental results on a collectionof benchmarks (with the robustness discussed in Sect. 6). The paper is thenconcluded in Sect. 7.

2

Preliminaries

Let N, Q and R be the set of natural, rational and real numbers, respectively.
We denote by R[x] the polynomial ring over R with variables x = (x1 , . . . , xn ),and x denotes the 2 -norm [4]. For a set X ⊆ Rn , its convex hull is denoted byconv(X). For x, x ∈ X, dist(x, x ) = x − x  denotes the Euclidean distance
between two points, which generalizes to dist(x, X  ) = minx  ∈X  dist(x, x ).
Given δ ≥ 0, deﬁne B(x, δ) = {x ∈ Rn |x − x ≤ δ} as the closed ball of radiusδ centered at x. Consider the quantiﬁer-free fragment of a ﬁrst-order theory ofpolynomials over the reals, denoted by TP , in which a formula ϕ is of the formϕ=
 p(x) 0 | ϕ ∧ ϕ | ϕ ∨ ϕ | ¬ϕ

NIL: Learning Nonlinear Interpolants

181

where p(x) ∈ R[x] and ∈ {<, >, ≤, ≥, =}. A natural extension of our method
to cater for more general nonlinearities involving transcendental functions will
be demonstrated in subsequent sections. In the sequel, we use ⊥ to stand for false
andfor true. Let R[x]m consist of all polynomials p(x) of degree ≤ m ∈ N.
 p(x) 0 and p(x) ∈ R[x]m
We abuse the notation ϕ ∈ R[x]m to abbreviate ϕ =if no ambiguity arises.
Given formulas φ and ψ in a theory T , φ is valid w.r.t. T , written as |=T φ,
iﬀ φ is true in all models of T ; φ entails ψ w.r.t. T , written as φ |=T ψ, iﬀ
every model of T that makes φ true makes ψ also true; φ is satisfiable w.r.t. T ,iﬀ there is a model of T in which φ is true; otherwise unsatisfiable. It follows
that φ is unsatisﬁable iﬀ φ |=T ⊥. The set of all the models that make φ true
is denoted by [[φ]]T .
2.1

Craig Interpolant

Craig showed in [10] that given two formulas φ and ψ in a ﬁrst-order logic T s.t.
φ |=T ψ, there always exists an interpolant I over the common symbols of φand ψ s.t. φ |=T I and I |=T ψ. In the veriﬁcation literature, this terminology
has been abused by [31], which deﬁned an interpolant over the common symbolsof φ and ψ as
Deﬁnition 1 (Interpolant). Given φ and ψ in a theory T s.t. φ∧ψ |=T ⊥, aformula I is a (reverse) interpolant of φ and ψ if (i) φ |=T I; (ii) I ∧ ψ |=T ⊥;and (iii) I contains only common symbols shared by φ and ψ.
It is immediately obvious that φ |=T ψ iﬀ φ ∧ ¬ψ |=T ⊥, namely, I is aninterpolant of φ and ψ iﬀ I is a reverse interpolant in McMillan’s sense of φ and¬ψ. We follow McMillan in continuing to abuse the terminology.
2.2

Support Vector Machines

In machine learning, support vector machines [3,45] are supervised learningmodels for eﬀective classiﬁcation based on convex optimization. In a binary
setting, we are given a training dataset X = X + X − of n sample points{(x1 , y1 ), (x2 , y2 ), . . . , (xn , yn )}, where xi ∈ Rd , and yi is either 1, indicating a
positive sample xi ∈ X + , or −1, indicating a negative one in X − . The goal ofclassiﬁcation here is to ﬁnd a potential hyperplane (a.k.a. linear classifier ) to
separate the positive samples from the negative ones. There however might bevarious or even inﬁnite number of separating hyperplanes, and an SVM aims
to construct a separating hyperplane that yields the largest distance (so-called
functional margin) to the nearest positive and negative samples. Such a classiﬁcation hyperplane is called the optimal-margin classifier while the samples
closest to it are called the support vectors.
Linear SVMs. Assume that X + and X − are linearly separable, meaning that
there exists a linear separating hyperplane wT x+b = 0 such that yi (wT xi +b) >0, for all (xi , yi ) ∈ X. Then the functional margin can be formulated as

182

M. Chen et al.

γ=
 2 min1≤i≤n 1/w|wT xi + b|.
Linear SVMs are committed to ﬁnding appropriate parameters (w, b) that maximize the functional margin while adhering to the constraints of separability,
which reduces equivalently to the following convex quadratic optimization problem [2] that can be eﬃciently solved by oﬀ-the-shelf packages for quadratic programming:
minimize
w ,b

1 T
w w
2

subject to yi (wT xi + b) ≥ 1, i = 1, 2, . . . , n.

(1)Lemma 1 (Correctness of SVMs [37]). Given positive samples X + which arelinearly separable from negative samples X − , SVMs produce, under computationsof infinite precision, a half-space h s.t. ∀x ∈ X + . h(x) > 0 and ∀x ∈ X − . h(x) <0.
Corollary 1 (Separation of Convex Hulls [1]). The half-space h in Lemma 1
satisfies that ∀x ∈ conv(X + ). h(x) > 0 and ∀x ∈ conv(X − ). h(x) < 0.

ΦFig. 1. Mapping from a two-dimensional input space into a three-dimensional feature
space with linear separation thereof.

Nonlinear SVMs. When φ and ψ are formulas over nonlinear arithmetic, often
after sampling X, it is not possible to ﬁnd a linearly separable hyperplane in thecommon variables. However, a nonlinear surface that can be described as a linear
hyperplane in the space of monomials of bounded degree may separate X + andX − . The above construction is generalized by introducing a transformation from˜
Rd to Rd , the vector space of monomials in the common variables up to somebounded degree, with yi (wT xi + b) ≥ 1 in (1) replaced by yi (wT Φ(xi ) + b) ≥ 1,
where Φ is a linear expression in monomials in the common variables up to abounded degree. Here, the vectors Φ(x) span the feature space.
Consider the Lagrangian dual [3] of the modiﬁed optimization problem:n
1 n nαi αj yi yj Φ(xi )T Φ(xj ) −
αi
i=1
j=1
i=1
α
2
n
subject toαi yi = 0, and αi ≥ 0 for i = 1, 2, . . . , n.
minimizei=1 Φ(x)T Φ(x ). The
A kernel function κ : Rd × Rd → R is deﬁned as κ(x, x ) =introduction of the dual problem and the kernel function [3] reduces the compu˜ down to O(d). For the sake of posttational complexity essentially from O(d)NIL: Learning Nonlinear Interpolants

183

verifying a candidate interpolant given by SVMs, we adopt an inhomogeneouspolynomial kernel function of the form
κ(x, x ) = (βxT x + θ)m ,where m is the polynomial degree describing complexity of the feature space, θ ≥0 is a parameter trading oﬀ the inﬂuence of higher-order versus lower-order terms
in the polynomial, and β is a scalar parameter. Henceforth,the optimal-marginnclassiﬁer (if there exists one) can be derived as wT Φ(x) = i=1 αi κ(xi , x) = 0,
with xi being a support vector iﬀ αi > 0. In practice, usually a large amount of
αi s turn out to be zero and this leads to a simple representation of a classiﬁer.
Figure 1 illustrates the intuitive idea of the transformation from the original
input space to the feature space. We will show in the sequel that the resultingclassiﬁer can be viewed as a candidate interpolant, while its optimal-margin
feature contributes to a certain “medium” logical strength of the interpolant,
which is thus robust to perturbations (in the feature space) in the formulae tobe interpolated.

3

Learning Interpolants

In this section, we present the NIL algorithm for synthesizing nontrivial (reverse)
Craig interpolants for the quantiﬁer-free theory of nonlinear arithmetic. It takes
as input a pair φ, ψ of formulas in TP as well as a positive integer m, andaims to generate an interpolant I of maximum degree m, i.e., I ∈ R[x]m , if itexists, such that φ |=TP I and I ∧ ψ |=TP ⊥. Here, φ, ψ can be decorated asφ(x, y), ψ(x, z) with variables involved in the predicates, and thus x denotes
variables that are common to φ and ψ. In the sequel, we drop the subscript TP
in |=TP and [[·]]TP wherever the context is unambiguous.
Due to the decidability of the ﬁrst-order theory of real-closed ﬁelds established by Tarski [44], TP admits quantifier elimination (QE). This means thatthe satisﬁability of any formula in TP can be decided (in doubly exponential
time in the number of variables for the worst case). If the formula is satisﬁable,models satisfying the formula can also be constructed algorithmically (following the same time complexity). Though the introduction of general forms oftranscendental functions renders the underlying theory undecidable, there does
exist certain extension of TP with transcendental functions (involving exponential functions, logarithms and trigonometric functions), e.g. that identiﬁed by
Strzeboński in [43] and references therein, which still admits QE. This allows astraightforward extension of NIL to such a decidable fragment involving transcendental functions. Speciﬁcally, the decidability remains when the transcendental functions involved are real univariate exp-log functions [41] or tame elementary functions [42] which admit a real root isolation algorithm.

184

M. Chen et al.

Algorithm NIL: Learning nonlinear interpolant

1
2

3
4
5
6
7

8
9

10
11

12
13
14

3.1

input : φ and ψ in TP over common variables x;
m, degree of the polynomial kernel, and hence
maximum degree of the interpolant.
/* checking unsatisfiability */if φ ∧ ψ |= ⊥ then/* no interpolant exists */abort;/* generating initial sample points */X + , X − ← Sampling(φ, ψ);/* counterexample-guided learning */whiledo/* generating a classifier by SVMs */C ← SVM(X + , X − , m);/* checking classification result */if C = Failed then/* no interpolant exists in R[x]m */abort;

Fig. 2. In NIL, a candidate interpolant (black line as its boundary) is
refined to an actual one (red line as its
boundary) by adding a counterexample(red dot). (Color figure online)/* classifier as candidate interpolant */else
I ← C;/* valid interpolant found */if φ |= I and I ∧ ψ |= ⊥ thenreturn I;/* adding counterexamples */else
X + ← X + FindInstance(φ ∧ ¬I);X − ← X − FindInstance(I ∧ ψ);

Fig. 3. In NILδ , a counterexample(red dot) stays at least a distanceof δ away from the candidate interpolant (black line as its boundary) tobe refined, leading to an interpolant(red line as its boundary) with tolerance δ. (Color figure online)

The Core Algorithm

The basic idea of NIL is to view interpolants as classiﬁers and use SVMs withthe kernel trick to perform eﬀective classiﬁcation. The algorithm is based on thesampling-guessing-reﬁning technique: in each iteration, it is fed with a classiﬁer (candidate interpolant) for a ﬁnite set of sample points from [[φ]] and [[ψ]](line 5), and verify the candidate (line 10) by checking the entailment problem
that deﬁnes an interpolant (as in Deﬁnition 1). If the veriﬁcation succeeds, theinterpolant is returned as the ﬁnal result. Otherwise, a set of counterexamples isobtained (line 13 and 14) as new sample points to further reﬁne the classiﬁer. In
what follows, we explain the steps of the interpolation procedure in more detail.
Initial Sampling. The algorithm begins by checking the satisﬁability of φ ∧ ψ.
If the formula is satisﬁable, it is then impossible to ﬁnd an interpolant, and thealgorithm stops declaring no interpolant exists.
Next, the algorithm attempts to sample points from both [[φ]] and [[ψ]]. Thisinitial sampling stage can usually be done eﬃciently using the Monte Carlo
method, e.g. by (uniformly) scattering a number of random points over certain
bounded range and then selecting those fall in [[φ]] and [[ψ]] respectively. However,this method fails when one or both of the predicates is very unlikely to be satisﬁed. One common example is when the predicate involves equalities. For suchsituations, solving the satisﬁability problem using QE is guaranted to succeed
in producing the sample points.

NIL: Learning Nonlinear Interpolants

185

To meet the condition that the generated interpolant can only involve symbols that are common to φ and ψ, we can project the points sampled from [[φ]](resp. [[ψ]]) to the space of x by simply dropping the components that pertain
to y (resp. z) and thereby obtain sample points in X + (resp. X − ).
Entailment Checking. The correctness of SVM given in Lemma 1 only guarantees that the candidate interpolant separates the ﬁnite set of points sampled from[[φ]] and [[ψ]], not necessarily the entirety of the two sets. Hence, post-veriﬁcationby checking the entailment problem (line 10) is needed for the candidate to beclaimed as an interpolant of φ and ψ. This can be achieved by solving the equivalent QE problems ∀x. φ(x, y)|x =⇒ I(x) and ∀x. I(x) ∧ ψ(x, z)|x =⇒ ⊥,where ·|x is the projection to the common space over x. The candidate will be
returned as an actual interpolant if both formulae reduce toafter eliminating the universal quantiﬁers. The satisﬁability checking at line 1 can be solved
analogously. Granted, the entailment checking can also be encoded in SMT techniques by asking the satisﬁability of the negation of the universally quantiﬁed
predicates, however, limitations of current SMT solvers in nonlinear arithmetic
hinders them from being practically used in our framework, as demonstrated
later in Sect. 5.
Counterexample Generation. If a candidate interpolant cannot be veriﬁed as
an actual one, then at least one witness can be found as a counterexample to thatcandidate, which can be added to the set of sample points in the next iteration to
reﬁne further candidates (cf. Fig. 2). Multiple counterexamples can be obtained
at a time thereby eﬀectively reducing the number of future iterations.
In general, we have little control over which counterexample will be returned
by QE. In the worst case, the counterexample can lie almost exactly on thehyperplane found by SVM. This poses issues for the termination of the algorithm.
We will address this theoretical issue by slightly modifying the algorithm, as
explained in Sects. 3.3 and 4.
3.2

Comparison with the Naı̈ve QE-Based Method

Simply performing QE on ∃y. φ(x, y) yields already an interpolant for mutually contradictory φ and ψ. Such an interpolant is actually the strongest in thesense of [13], which presents an ordered family of interpolation systems due tothe logical strength of the synthesized interpolants. Dually, the negation of theresult when performing QE over ∃z. ψ(x, z) is the weakest interpolant. However,as argued by D’Silva et al. in [13], a good interpolant (approximation of φ orψ) –when computing invariants of transition systems using interpolation-basedmodel checking– should be coarse enough to enable rapid convergence but strong
enough to be contained within the weakest inductive invariant. In contrast, theadvantages of NIL are two-fold: ﬁrst, it produces better interpolants (in the above
sense) featuring “medium” strength (due to the way optimal-margin classiﬁer isdeﬁned) which are thus more eﬀective in practical use and furthermore resilient
to perturbations in φ and ψ (i.e., the robustness shown later in Sect. 6); second,
NIL always returns a single polynomial inequality as the interpolant which is

186

M. Chen et al.

often simpler than that derived from the naı̈ve QE-based method, where thedirect projection of φ(x, y) onto the common space over x can be as complex as
the original φ.
These issues can be avoided by combining this method with a template-based
approach, which in turn introduces fresh quantiﬁers over unknown parameters
to be eliminated. Note that in NIL the candidate interpolants I ∈ R[x]m underveriﬁcation are polynomials without unknown parameters, and therefore, in contrast to performing QE over an assumed template, the learning-based technique
can practically generate polynomial interpolants of higher degrees (with acceptable rounds of iterations). For example, NIL is able to synthesize an interpolant
of degree 7 over 2 variables (depicted
later in Fig. 4(b)), which would require a=36
unknownparameters that goes far beyond
polynomial template with 7+22
the capability of QE procedures.
On the other hand, performing QE within every iteration of the learning
process, for entailment checking and generating counterexamples, limits the eﬃciency of the proposed method, thereby conﬁning NIL currently to applications
only of small scales. Potential solutions to the eﬃciency bottleneck will be discussed in Sect. 5.
3.3

Variants of NIL

While the above basic algorithm is already eﬀective in practice (as demonstrated
in Sect. 5), it is guaranteed to terminate only when there is an interpolant withpositive functional margin between [[φ]] and [[ψ]]. In this section, we present twovariants of the algorithm that have nicer theoretical properties in cases where
the two sets are only separated by an interpolant with zero functional margin,e.g., cases where [[φ]] and [[ψ]] share adjacent or even coincident boundaries.
Entailment Checking with Tolerance δ. When performing entailment checking for a candidate interpolant I, instead of using, e.g., the formula p(x) ≥ 0
for I, we can introduce a tolerance of δ. That is, we check the satisﬁability ofφ ∧ (p(x) < −δ) and (p(x) ≥ δ) ∧ ψ instead of the original φ ∧ (p(x) < 0) and(p(x) ≥ 0) ∧ ψ. This means that a candidate that is an interpolant “up to atolerance of δ” will be returned as a true interpolant, which may be acceptablein some applications. If the candidate interpolant is still not veriﬁed, the counterexample is guaranteed to be at least a distance of δ away from the separating˜
hyperplane. Note the distance δ is taken in the feature space Rd , not in the original space. We let NILδ (φ, ψ, m) denote the version of NIL with this modiﬁcation(cf. Fig. 3). In the next section, we show NILδ (φ, ψ, m) terminates as long as[[φ]] and [[ψ]] are bounded, including the case where they are separated only byinterpolants of functional margin zero.
Varying Tolerance During the Execution. A further reﬁnement of the algorithm can be made by varying the tolerance δ during the execution. We also
introduce a bounding box B of the varying size to handle unbounded cases.
Deﬁne algorithm NIL∗δ,B (φ, ψ, m) as follows. Let δ1 = δ and B1 = B. For each
iteration i, execute the core algorithm, except that the counterexample must be

NIL: Learning Nonlinear Interpolants

187

a distance of at least δi away from the separating boundary, and have absolute˜value in each dimension at most B (both in Rd ). After the termination of iteration i, begin iteration i + 1 with δi+1 = δi /2 and Bi+1 = 2Bi . This continues
until an interpolant is found or until a pre-speciﬁed cutoﬀ. For any [[φ]] and [[ψ]](without the boundedness condition), this variant of the algorithm converges toan interpolant in the limit, which will be made precise in the next section.

4Soundness, Completeness and Convergence

In this section, we present theoretical results obtained for the basic NIL algorithm and its variants. Proofs are available in the appendix of [6].
First, the basic algorithm is sound, as captured by Theorem 1.
Theorem 1 (Soundness of NIL). NIL(φ, ψ, m) terminates and returns I if
and only if I is an interpolant in R[x]m of φ and ψ.
Under certain conditions, the algorithm is also terminating (and hence complete). We prove two such situations below. In both cases, we require boundedness of the two sets that we want to separate. In the ﬁrst case, there exists aninterpolant with positive functional margin between the two sets.
Theorem 2 (Conditional Completeness of NIL). If [[φ]] and [[ψ]] arebounded and there exists an interpolant in R[x]m of φ and ψ with positive func˜tional margin γ when mapped to Rd , then NIL(φ, ψ, m) terminates and returns
an interpolant I of φ and ψ.
The standard algorithm is not guaranteed to terminate when [[φ]] and [[ψ]] areonly separated by interpolants of functional margin zero. However, the modiﬁed
algorithm NILδ (φ, ψ, m) does terminate (with the cost that the resulting answer
is an interpolant with tolerance δ).
Theorem 3 (Completeness of NILδ with zero margin). If [[φ]] and [[ψ]] arebounded, and δ > 0, then NILδ (φ, ψ, m) terminates. It returns an interpolant Iof φ and ψ with tolerance δ whenever such an interpolant exists.
By iteratively decreasing δ during the execution of the algorithm, as well as
introducing an iteratively increasing bounding box, as in NIL∗δ,B (φ, ψ, m), we
can obtain more and more accurate candidate interpolants. We now show that
this algorithm converges to an interpolant without restrictions on φ and ψ. We
ﬁrst make this convergence property precise in the following deﬁnition.
Deﬁnition 2 (Convergence of a sequence of equations to an interpolant). Given two sets [[φ]] and [[ψ]] that we want to separate, and an infinite
sequence of equations I1 , I2 , . . . , we say the sequence In converges to an interpolant of φ and ψ if, for each point p in the interior of [[φ]] or [[ψ]], there exists
some integer Kp such that Ik classifies p correctly for all k ≥ Kp .
Theorem 4 (Convergence of NIL∗δ,B ). Given two regions [[φ]] and [[ψ]]. Suppose there exists an interpolant of φ and ψ, then the infinite sequence of candidates produced by NIL∗δ,B (φ, ψ, m) converges to an interpolant in the sense of
Definition 2.

188

M. Chen et al.

5

Implementation and Experiments

5.1

Implementation Issues

We have implemented the core algorithm NIL as a prototype1 in Wolfram Mathematica with LIBSVM [5] being integrated as an engine to perform SVM classiﬁcations. Despite featuring no completeness for adjacent [[φ]] and [[ψ]] nor convergence for unbounded [[φ]] or [[ψ]], the standard NIL algorithm yields alreadypromising results as shown later in the experiments. Key Mathematica functions
that are utilized include Reduce, for entailment checking, e.g., the unsatisﬁability checking of φ ∧ ψ and the post-veriﬁcation of a candidate interpolant,
and FindInstance, for generating counterexamples and sampling initial points(when the random sampling strategy fails). The Reduce command implements a
decision procedure for TP and its appropriate extension to catering for transcendental functions (cf. [43]) based on cylindrical algebraic decomposition (CAD),
due to Collins [9]. The underlying quantiﬁer-elimination procedure, albeit inducing rather high computation complexity, cannot in practice be replaced by SMTsolving techniques (by checking the negation of a universally quantiﬁed predicate) as in the linear arithmetic. For instance, the oﬀ-the-shelf SMT solver Z3
fails to accomplish our tasks particularly when the coeﬃcients occurring in theentailment problem to be checked get larger2 .
Numerical Errors and Rounding. LIBSVM conducts ﬂoating-point computations for solving the optimization problems induced by SVMs and consequently
yields numerical errors occurring in the candidate interpolants. Such numericalerrors may block an otherwise valid interpolant from being veriﬁed as an actual
one and additionally bring down the simplicity and thereby the eﬀectiveness ofthe synthesized interpolant, thus not very often proving humans with clear-cut
understanding. This is a common issue for approaches that reduce the interpolation problem to numerical solving techniques, e.g. SDP solvers exploitedin [11,14,33], while an established method to tackle it is known as rational
recovery [29,47], which retrieves the nearest rational number from the continued
fraction representation of its ﬂoating-point approximation at any given accuracy(see e.g. [47] for theoretical guarantees and [33] for applications in interpolation). The algorithm implementing rational recovery has been integrated in our
implementation and the consequent beneﬁts are two-fold: (i) NIL can now copewith interpolation tasks where only exact coeﬃcients suﬃce to constitute an
actual interpolant while any numerical error therein will render the interpolant
invalid, e.g., cases where [[φ]] and [[ψ]] share parallel, adjacent, or even coincident
boundaries, as demonstrated later by examples with ID 10–17 in Table 1; (ii)rationalizing coeﬃcients moreover facilitates simpliﬁcations over all of the candidate interpolants and therefore practically accelerating the entailment checking
and counterexample generation processes, which in return yields simpler interpolants, as shown in Table 2 in the following section.
1
2

Available at http://lcs.ios.ac.cn/∼chenms/tools/NIL.tar.bz2.
As can be also observed at https://github.com/Z3Prover/z3/issues/1765.

NIL: Learning Nonlinear Interpolants

5.2

189

Benchmark and Experimental Results

Table 1 collects a group of benchmark examples from the literature on synthesizing nonlinear interpolants as well as some geometrically contrived ones. All of
the experiments have been evaluated on a 3.6 GHz Intel Core-i7 processor with
8 GB RAM running 64-bit Ubuntu 16.04.
In Table 1, we group the set of examples into four categories comprising 20
cases in total. For each example, ID numbers the case, φ, ψ and I represent thetwo formulas to be interpolated and the synthesized interpolant by our method
respectively, while Time/s indicates the total time in seconds for interpolation.
The categories are described as follows, and the visualization of a selected set of
typical examples thereof is further depicted in Fig. 4.
Cat. I: with/without rounding. This category includes 9 cases, for which
our method generates the polynomial interpolants correctly with or without
the rounding operation.
Cat. II: with rounding. For cases 10 to 17 in this category, where [[φ]] and [[ψ]]share parallel, adjacent, or even coincident boundaries, our method produces
interpolants successfully with the rouding process based on rational recovery.
Cat. III: beyond polynomials. This category encloses two cases beyond thetheory TP of polynomials: for case 18, a veriﬁed polynomial interpolant isobtained in spite of the transcendental term in ψ; while for case 19, the SVM
classiﬁcation fails since [[φ]] and [[ψ]] are not linearly separable in any ﬁnitedimensional feature space and hence no polynomial interpolant exists for thisexample. Note that our counterexample-guided learning framework admits astraightforward extension to a decidable fragment of more general nonlinear
theories involving transcendental functions, as investigated in [43].
Cat. IV: unbalanced. The case 20, called Unbalanced, instantiates a particularscenario where φ and ψ have extraordinary “unbalanced” number of models
that make them true respectively. For this example, there are an inﬁnite number of models satisfying φ yet one single model (i.e., x = 0) satisfying ψ. The
training process in SVMs may fail when encountering extremely unbalanced
number of positive/negative samples. This is solved by specifying a weightfactor for the positive set of samples as the number of negative ones, anddually for the other way around, to balance biased number of training samples before triggering the classiﬁcation. Such a balancing trick is supported
in LIBSVM.
Remark that examples named CAV13-1/3/4 are taken from [11] (and the latter two originally from [28] and [18] respectively), where interpolation is applied
to discovering inductive invariants in the veriﬁcation of programs and hybrid
systems. For instance, CAV13-3 is a program fragment describing an accelerating car and the synthesized interpolant by NIL suﬃces to prove the safety
property of the car concerning its velocity.
Applicability and Comparison with Existing Approaches. As shown in
Table 1, our learning-based technique succeeds in all of the benchmark examples

Table 1. Benckmark examples for synthesizing nonlinear interpolants.
190
M. Chen et al.

NIL: Learning Nonlinear Interpolants

191

Fig. 4. Visualization in NIL on a selected set of examples. Legends: gray region: [[φ]],blue region: [[ψ]], pink region: [[I]] with a valid interpolant I, red dots: X + , blue dots:
X − , circled dots: support vectors. Sample points are hidden in 3D-graphics for a clear
presentation.

that admit polynomial interpolants. Due to theoretical limitations of existing
approaches as elaborated in Sect. 1, none of the aforementioned methods cancope with as many cases in Table 1 as NIL can. For instances, the Twisted
example as depicted in Fig. 4(c) falls beyond the scope of concave quadratic
formulas and thus cannot be addressed by the approach in [14], while the Parallel
parabola example as shown in Fig. 4(d) needs an inﬁnite combination of linear
constraints as an interpolant when performing the technique in [15] and hence notof practical use, to name just a few. Moreover, we list in Table 2 a comparisonof the synthesized interpolants against works where the benchmark examples
are collected from. As being immediately obvious from Table 2, our technique

192

M. Chen et al.
Table 2. Comparison of the synthesized interpolants.

often produces interpolants of simpler forms, particularly for examples CAV132, CAV13-4 and TACAS16. Such a simplicity beneﬁts from both the rounding
eﬀect and the form of interpolant (i.e., a single polynomial inequality) that wetend to construct.
Bottleneck of Eﬃciency and Potential Solutions. The current implementation of NIL works promisingly for small examples; it does not scale to interpolation problems with large numbers of common variables, as reported in Table 1.
The bottleneck stems from quantiﬁer eliminations performed within every iteration of the learning process, for entailment checking and generating counterexamples. We pose here several potential solutions that are expected to signiﬁcantly reduce computational eﬀorts: (i) substitute general purpose QE procedurethat perform CAD by the so-called variant quantiﬁer-elimination (VQE) algorithm [21], which features singly-exponential complexity in the number of variables. This however requires a careful inspection of whether our problem meetsthe geometric conditions imposed by VQE; (ii) incorporate relaxation schemes,
e.g., Lagrangian relaxation and sum-of-squares decompositions [34], and complement with QE only when the relaxation fails to produce desired results.

NIL: Learning Nonlinear Interpolants

193

Fig. 5. -Face: introducing perturbations (with  up to 0.5) in the Face example. The
synthesized interpolant is resilient to any -perturbation in the radii satisfying −0.5 ≤ ≤ 0.5.

6

Taming Perturbations in Parameters

An interpolant synthesized by the SVM-based technique features inherent
robustness due to the way optimal-margin classiﬁer is deﬁned (Sect. 2). Thatis, the validity of such an interpolant is not easily perturbed by changes (inthe feature space) in the formulae to be interpolated. It is straightforward in
NIL to deal with interpolation problems under explicitly speciﬁed perturbations, which are treated as constraints over fresh variables. An example named
-Face is depicted in Fig. 5, which perturbs φ, ψ in the Face example asφ= − 0.5 ≤ 1 ≤ 0.5 ∧ ((x + 4)2 + y 2 − (1 + 1 )2 ≤ 0 ∨ (x − 4)2 + y 2 − (1 + 1 )2 ≤ 0)and ψ =
 − 0.5 ≤ 2 ≤ 0.5 ∧ x2 + y 2 − 64 ≤ 0 ∧ (x + 4)2 + y 2 − (3 + 2 )2 ≥0 ∧ (x − 4)2 + y 2 − (3 + 2 )2 ≥ 0. The
 synthesizedinterpolant over common

4

3

x
variables of φ and ψ is 139+ x268y + x2

y2
11
39 − 36

3

2

y
y
1
+ x − y52 − 157
+
− 52
− 116

y4
y3
2y 2
y
25 − 182 + 19 − 218 + 1 < 0 which is hence resilient to any -perturbation in

the radii satisfying −0.5 ≤  ≤ 0.5, as illustrated in Fig. 5(b).

7Conclusions

We have presented a uniﬁed, counterexample-guided method named NIL for generating polynomial interpolants over the general quantiﬁer-free theory of nonlinear arithmetic. Our method is based on classiﬁcation techniques with spacetransformations and kernel tricks as established in the community of machinelearning. We proved the soundness of NIL and proposed suﬃcient conditions for
its completeness and convergence. The applicability and eﬀectiveness of our technique are demonstrated experimentally on a collection of representative benchmarks from the literature, including those extracted from program veriﬁcation.
Experimental results indicated that our method suﬃces to address more interpolation tasks, including those with perturbations in parameters, and in manycases synthesizes simpler interpolants compared with existing approaches.

194

M. Chen et al.

For future work, we would like to improve the eﬃciency of NIL by substituting the general purpose quantiﬁer-elimination procedure with alternative methods previously discussed in Sect. 5. An extension of our approach to cater forthe combination of nonlinear arithmetic with EUFs, by resorting to predicateabstraction techniques [23], will be of particular interest. Additionally, we plan toinvestigate the performance of NIL over diﬀerent classiﬁcation techniques, e.g.,
the widespread regression-based methods [19], though SVMs are expected to be
more competent concerning the robustness and predictability, as also observedin [37].

References
1. Bennett, K.P., Bredensteiner, E.J.: Duality and geometry in SVM classiﬁers. In:
ICML 2000, pp. 57–64 (2000)
2. Bishop, C.M.: Pattern Recognition and Machine Learning, pp. 326–328. Springer,
New York (2006)
3. Boser, B.E., Guyon, I., Vapnik, V.: A training algorithm for optimal margin classiﬁers. In: COLT 1992, pp. 144–152 (1992)
4. Bourbaki, N.: Topological Vector Spaces. Elements of Mathematics. Springer, Heidelberg (1987). https://doi.org/10.1007/978-3-642-61715-7
5. Chang, C., Lin, C.: LIBSVM: a library for support vector machines. ACM TIST
2(3), 27:1–27:27 (2011)
6. Chen, M., Wang, J., An, J., Zhan, B., Kapur, D., Zhan, N.: NIL: learning nonlinear
interpolants (full version). http://lcs.ios.ac.cn/∼chenms/papers/CADE-27 FULL.
pdf
7. Cimatti, A., Griggio, A., Sebastiani, R.: Eﬃcient interpolant generation in satisﬁability modulo theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008.
LNCS, vol. 4963, pp. 397–412. Springer, Heidelberg (2008). https://doi.org/10.
1007/978-3-540-78800-3 30
8. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided
abstraction reﬁnement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS,
vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/
10722167 15
9. Collins, G.E.: Quantiﬁer elimination for real closed ﬁelds by cylindrical algebraic
decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp.
134–183. Springer, Heidelberg (1975). https://doi.org/10.1007/3-540-07407-4 17
10. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J.
Symb. Log. 22(3), 250–268 (1957)
11. Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semideﬁnite programming. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp.
364–380. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-397998 25
12. Dathathri, S., Arechiga, N., Gao, S., Murray, R.M.: Learning-based abstractions
for nonlinear constraint solving. In: IJCAI 2017, pp. 592–599 (2017)13. D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength.
In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129–145. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11319-2 12

NIL: Learning Nonlinear Interpolants

195

14. Gan, T., Dai, L., Xia, B., Zhan, N., Kapur, D., Chen, M.: Interpolant synthesisfor quadratic polynomial inequalities and combination with EUF. In: Olivetti, N.,
Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 195–212. Springer,
Cham (2016). https://doi.org/10.1007/978-3-319-40229-1 14
15. Gao, S., Zuﬀerey, D.: Interpolants in nonlinear theories over the reals. In: Chechik,M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 625–641. Springer,
Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9 41
16. Gilbert, S.: A nullstellensatz and a positivstellensatz in semialgebraic geometry.
Math. Ann. 207(2), 87–97 (1974)
17. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997).
https://doi.org/10.1007/3-540-63166-6 10
18. Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically reﬁning abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008.
LNCS, vol. 4963, pp. 443–458. Springer, Heidelberg (2008). https://doi.org/10.
1007/978-3-540-78800-3 33
19. Hastie, T., Tibshirani, R., Friedman, J.: The Elements of Statistical Learning:
Data Mining, Inference, and Prediction. SSS, 2nd edn. Springer, New York (2009).
https://doi.org/10.1007/978-0-387-84858-7
20. Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions fromproofs. In: POPL 2004, pp. 232–244 (2004)
21. Hong, H., Din, M.S.E.: Variant quantiﬁer elimination. J. Symb. Comput. 47(7),883–901 (2012)
22. Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based
program synthesis. In: ICSE 2010, pp. 215–224 (2010)
23. Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program veriﬁcation. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook ofModel Checking, pp. 447–491. Springer, Cham (2018). https://doi.org/10.1007/
978-3-319-10575-8 15
24. Jung, Y., Lee, W., Wang, B.-Y., Yi, K.: Predicate generation for learning-based
quantiﬁer-free loop invariant inference. In: Abdulla, P.A., Leino, K.R.M. (eds.)
TACAS 2011. LNCS, vol. 6605, pp. 205–219. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9 17
25. Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: FSE
2006, pp. 105–116 (2006)
26. Kovács, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A.
(ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 199–213. Springer, Heidelberg(2009). https://doi.org/10.1007/978-3-642-02959-2 17
27. Krajı́ček, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457–486 (1997)
28. Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear
constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol.
6919, pp. 240–255. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3642-24310-3 17
29. Lang, S.: Introduction to Diophantine Approximations: New Expanded Edition.
Springer, New York (2012)
30. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A.,
Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg(2003). https://doi.org/10.1007/978-3-540-45069-6 1

196

M. Chen et al.

31. McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A.
(eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004).
https://doi.org/10.1007/978-3-540-24730-2 2
32. McMillan, K.L.: Quantiﬁed invariant generation using an interpolating saturation
prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp.
413–427. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-788003 31
33. Okudono, T., Nishida, Y., Kojima, K., Suenaga, K., Kido, K., Hasuo, I.: Sharperand simpler nonlinear interpolants for program veriﬁcation. In: Chang, B.-Y.E.
(ed.) APLAS 2017. LNCS, vol. 10695, pp. 491–513. Springer, Cham (2017).
https://doi.org/10.1007/978-3-319-71237-6 24
34. Parrilo, P.A.: Semideﬁnite programming relaxations for semialgebraic problems.
Math. Program. 96(2), 293–320 (2003)
35. Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone
computations. J. Symb. Log. 62(3), 981–998 (1997)
36. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation.
In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362.
Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69738-1 25
37. Sharma, R., Nori, A.V., Aiken, A.: Interpolants as classiﬁers. In: Madhusudan, P.,
Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 71–87. Springer, Heidelberg(2012). https://doi.org/10.1007/978-3-642-31424-7 11
38. Sofronie-Stokkermans, V.: Interpolation in local theory extensions. In: Furbach, U.,
Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 235–250. Springer,
Heidelberg (2006). https://doi.org/10.1007/11814771 21
39. Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory
extensions. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol.
9706, pp. 273–289. Springer, Cham (2016). https://doi.org/10.1007/978-3-31940229-1 19
40. Solar-Lezama, A., Rabbah, R.M., Bodı́k, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI 2005, pp. 281–294 (2005)
41. Strzeboński, A.W.: Real root isolation for exp-log functions. In: ISSAC 2008, pp.
303–314 (2008)
42. Strzeboński, A.W.: Real root isolation for tame elementary functions. In: ISSAC
2009, pp. 341–350 (2009)43. Strzeboński, A.W.: Cylindrical decomposition for systems transcendental in theﬁrst variable. J. Symb. Comput. 46(11), 1284–1290 (2011)
44. Tarski, A.: A Decision Method for Elementary Algebra and Geometry. Universityof California Press, Berkeley (1951)
45. Vladimir, V.: Pattern recognition using generalized portrait method. Autom.
Remote Control 24, 774–780 (1963)
46. Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In:
Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer,
Heidelberg (2005). https://doi.org/10.1007/11532231 26
47. Zhang, J., Feng, Y.: Obtaining exact value by approximate computations. Sci.
China Ser. A Math. 50(9), 1361 (2007)