Certification of real inequalities: templates and sums of squares

We consider the problem of certifying lower bounds for real-valued multivariate transcendental functions. The functions we are dealing with are nonlinear and involve semialgebraic operations as well as some transcendental functions like \(\cos ,\,\arctan ,\,\exp \), etc. Our general framework is to use different approximation methods to relax the original problem into polynomial optimization problems, which we solve by sparse sums of squares relaxations. In particular, we combine the ideas of the maxplus approximations (originally introduced in optimal control) and of the linear templates (originally introduced in static analysis by abstract interpretation). The nonlinear templates control the complexity of the semialgebraic relaxations at the price of coarsening the maxplus approximations. In that way, we arrive at a new—template based—certified global optimization method, which exploits both the precision of sums of squares relaxations and the scalability of abstraction methods. We analyze the performance of the method on problems from the global optimization literature, as well as medium-size inequalities issued from the Flyspeck project.

1. Recall that for \(\gamma \geqslant 0\), a function \(\phi : \mathbb {R}^n\rightarrow \mathbb {R}\) is said to be \(\gamma \)-semiconvex if the function \(\mathbf {x}\mapsto \phi (\mathbf {x})+\frac{\gamma }{2}\Vert \mathbf {x} \Vert _2^2\) is convex.

2. We presume that in [25, Lemma 3], “well-defined function \(f\)” stands for the fact that \(f\) can be evaluated in a non-ambiguous way on the considered domain.

3. http://nl-certify.forge.ocamlcore.org/.

Authors and Affiliations

1. Circuits and Systems Group, Department of Electrical and Electronic Engineering, Imperial College London, South Kensington Campus, London, UK

   Victor Magron

2. INRIA and CMAP, École Polytechnique, Palaiseau, France

   Xavier Allamigeon & Stéphane Gaubert

3. LIX, École Polytechnique, Palaiseau, France

   Benjamin Werner

Corresponding author

Correspondence to Victor Magron.

Appendix 1: Global optimization problems issued from the literature

The following test examples are taken from Appendix B in [4]. Some of these examples involve functions that depend on numerical constants, the values of which can be found there.

• Hartman 3 (H3) \(\min _{\mathbf {x}\in [0, 1]^3} f(\mathbf {x}) = - \sum _{i=1}^4 c_i \exp \left[ - \sum _{j=1}^3 a_{i j} (x_j - p_{i j})^2\right] .\)

• Hartman 6 (H6) \(\min _{\mathbf {x}\in [0, 1]^6} f(\mathbf {x}) = - \sum _{i=1}^4 c_i \exp \left[ - \sum _{j=1}^6 a_{i j} (x_j - p_{i j})^2\right] .\)

• Mc Cormick (MC), with \(K = [-1.5, 4] \times [-3, 3] \): \(\min _{\mathbf {x}\in K} f(\mathbf {x}) = \sin (x_1 + x_2) + (x_1 - x_2)^2 - 1.5 x_1 + 2.5 x_2 + 1.\)

• Modified Langerman (ML): \(\min _{\mathbf {x}\in [0, 10]^n} f(\mathbf {x}) = \sum _{j=1}^5 c_j \cos (d_j / \pi ) \exp (- \pi d_j) \), with \(d_j = \sum _{i=1}^n (x_i - a_{j i})^2.\)

• Schwefel Problem (SWF): \(\min _{\mathbf {x}\in [1, 500]^n} f(\mathbf {x}) = - \sum _{i = 1}^{n} x_i \sin (\sqrt{x_i}).\)

Appendix 2: Proofs

1.1 Preliminary results

For the sequel, we need to recall the following definition.

Definition 8

(Modulus of continuity) Let \(u\) be a real univariate function defined on an interval \(I\). The modulus of continuity of \(u\) is defined as:

We shall also prove that \(\mathtt {unary\_approx}\) and \(\mathtt {reduce\_lift}\) return uniformly convergent approximations nets:

Proposition 4

Suppose that Assumption 4 holds. For every function \(r\) of the dictionary \(\mathcal {D}\), defined on a closed interval \(I\), the procedure \(\mathtt {unary\_approx}\) returns two nets of univariate lower semialgebraic approximations \((r_p^-)_{p \in \mathcal {P}}\) and upper semialgebraic approximations \((r_p^+)_{p \in \mathcal {P}}\), that uniformly converge to \(r\) on \(I\).

For every semialgebraic function \(f_{\text {sa}}\in \mathcal {A}\), defined on a compact semialgebraic set \(K\), the procedure \(\mathtt {reduce\_lift}\) returns two nets of lower semialgebraic approximations \((t_p^-)_{p \in \mathcal {P}}\) and upper semialgebraic approximations \((t_p^+)_{p \in \mathcal {P}}\), that uniformly converge to \(f_{\text {sa}}\) on \(K\).

Proof

First, suppose that the precision \(p\) is the best uniform polynomial approximation degree. By Assumption 4, the procedure \(\mathtt {unary\_approx}\) returns the sequence of degree-\(d\) minimax polynomials, using the algorithm of Remez. This sequence uniformly converges to \(r\) on \(I\), as a consequence of Jackson’s Theorem [15, Chap. 3]. Alternatively, when considering maxplus approximations in which the precision is determined by certain sets of points, we can apply Theorem 2 that implies the uniform convergence of the maxplus approximations.

Next, for sufficiently large relaxation order, the \(\mathtt {reduce\_lift}\) procedure returns the best (for the \(L_{1}\) norm) degree-\(d\) polynomial under-approximation of a given semialgebraic function, as a consequence of Theorem 3. \(\square \)

1.2 Proof of Lemma 3

Let us equip the vector space \(\mathbb {R}_d[\mathbf {x}]\) of polynomials \(h\) of degree at most \(d\) with the norm \(\Vert h \Vert _{\infty } := \sup _{|\varvec{\alpha }| \leqslant d} \{ |h_{\varvec{\alpha }}| \}\).

Let \(H\) be the admissible set of Problem \((P^{\text {sa}})\). Observe that \(H\) is closed in the topology of the latter norm. Moreover, the objective function of Problem \((P^{\text {sa}})\) can be written as \(\phi : h\in H \mapsto \Vert f_{\text {sa}}- h\Vert _{L_1(K)}\), where \(\Vert \cdot \Vert _{L_1(K)}\) is the norm of the space \(L^1(K,\lambda _n)\). The function \(\phi \) is continuous in the topology of \(\Vert \cdot \Vert _{\infty }\) (for polynomials of bounded degree, the convergence of the coefficients implies the uniform convergence on every bounded set for the associated polynomial functions, and a fortiori the convergence of these polynomial functions in \(L^1(K,\lambda _n)\)). Note also that \(\int _{[0, 1]^n} h\ d \lambda _n= \int _{[0, 1]^n} h(\mathbf {x}) \ d \lambda _n(\mathbf {x}) = \int _{[0, 1]^{n + p}} h(\mathbf {x},\mathbf {z}) \ d \lambda _{n + p}(\mathbf {x},\mathbf {z})\). We claim that for every \(t \in \mathbb {R}\), the sub-level set \(S_t:=\{ h \in H \mid \phi (h) \leqslant t\}\) is bounded. Indeed, when \(\phi (h) \leqslant t\), we have:

Since on a finite dimensional vector space, all the norms are equivalent, there exists a constant \(C>0\) such that \(\Vert h \Vert _{\infty } \leqslant C \Vert h\Vert _{L_1(K)} \) for all \(h\in H\), so we deduce that \(\Vert h \Vert _{\infty }\leqslant C(t + \Vert f_{\text {sa}}\Vert _{L_1(K)})\) for all \(h\in S_t\), which shows the claim. Since \(\phi \) is continuous, it follows that every sublevel set of \(\phi \), which is a closed bounded subset of a finite dimensional vector space, is compact. Hence, the minimum of Problem \((P^{\text {sa}})\) is attained. \(\square \)

1.3 Proof of Proposition 3

The proof is by induction on the structure of \(t\).

• When \(t\) represents a semialgebraic function of \(\mathcal {A}\), the under-approximation (resp. over-approximation) net \((t_{p}^-)_{p }\) (resp. \((t_{p}^+)_{p}\)) converges uniformly to \(t\) by Proposition 4.

• The second case occurs when the root of \(t\) is an univariate function \(r \in \mathcal {D}\) with the single child \(c\). Suppose that \(r\) is increasing without loss of generality. We consider the net of under-approximations \((c_p^-)_{p}\) (resp. over-approximations \((c_p^+)_{p}\)) as well as lower and upper bounds \(m_{c_p}\) and \(M_{c_p}\) which are obtained recursively. Since \(K\) is a compact semialgebraic set, one can always find an interval \(I_0\) enclosing the values of \(r_p^+\) (i.e. such that \([m_{c_p}, M_{c_p}] \subset I_0\)), for all \(p\). The induction hypothesis is the uniform convergence of \((c_p^-)_{p}\) (resp. \((c_p^+)_{p}\)) to \(c\) on \(K\). Now, we prove the uniform convergence of \((t_p^+)_{p}\) to \(t\) on \(K\). One has:

  $$\begin{aligned} \Vert t - t_p^+ \Vert _{\infty } \leqslant \Vert r \circ c - r_p^+ \circ c \Vert _{\infty } + \Vert r_p^+ \circ c - t_p^+ \Vert _{\infty }. \end{aligned}$$

  (8.1)

  Let note \(\omega \) the modulus of continuity of \(r_p^+\) on \(I_0\). Thus, the following holds:

  $$\begin{aligned} \Vert r_p^+ \circ c - r_p^+ \circ c_p^+ \Vert _{\infty } \leqslant \omega (\Vert c - c_p^+ \Vert _{\infty }). \end{aligned}$$

  (8.2)

  Let \(\epsilon > 0\) be given. The univariate function \(r_p^+\) is uniformly continuous on \(I_0\), thus there exists \(\delta > 0\) such that \(\omega (\delta ) \leqslant \epsilon / 2\). Let choose such a \(\delta \). By induction hypothesis, there exists a precision \(p_0\) such that for all \(p \geqslant p_0,\,\Vert c - c_p^+ \Vert _{\infty } \leqslant \delta \). Hence, using (8.2), the following holds:

  $$\begin{aligned} \Vert r_p^+ \circ c - r_p^+ \circ c_p^+ \Vert _{\infty } \leqslant \epsilon / 2. \end{aligned}$$

  (8.3)

  Moreover, from the uniform convergence of \((r_p^+)_{p \in \mathbb {N}}\) to \(r\) on \(K\) (by Proposition 4), there exists a precision \(p_1\) such that for all \(p \geqslant p_1\):

  $$\begin{aligned} \Vert r \circ c - r_p^+ \circ c \Vert _{\infty } \leqslant \epsilon / 2. \end{aligned}$$

  (8.4)

  Using (8.1) together with (8.3) and (8.4) yield the desired result. The proof of the uniform convergence of the under-approximations is analogous.

• If the root of \(t\) is a binary operation whose arguments are two children \(c_1\) and \(c_2\), then by induction hypothesis, we obtain semialgebraic approximations \(c_{1, p}^-,\,c_{2, p}^-,\,c_{1, p}^+,\,c_{2, p}^+\) that verify:

  $$\begin{aligned} \lim _{p \rightarrow \infty } \Vert c_1 - c_{1, p}^- \Vert _{\infty }&= 0, \qquad \quad \lim _{p \rightarrow \infty } \Vert c_1 - c_{1, p}^+ \Vert _{\infty } = 0, \end{aligned}$$

  (8.5)
  $$\begin{aligned} \lim _{p \rightarrow \infty } \Vert c_2 - c_{2, p}^- \Vert _{\infty }&= 0, \qquad \quad \lim _{p \rightarrow \infty } \Vert c_2 - c_{2, p}^+ \Vert _{\infty } = 0. \end{aligned}$$

  (8.6)

  If \(\mathtt {bop}= +\), by using the triangle inequality:

  $$\begin{aligned} \Vert c_1 + c_2 - c_{1, p}^- -c_{2, p}^- \Vert _{\infty } \leqslant \Vert c_1 - c_{1, p}^- \Vert _{\infty } + \Vert c_2 - c_{2, p}^- \Vert _{\infty }, \\ \Vert c_1 + c_2 - c_{1, p}^+ -c_{2, p}^+ \Vert _{\infty } \leqslant \Vert c_1 - c_{1, p}^+ \Vert _{\infty } + \Vert c_2 - c_{2, p}^+ \Vert _{\infty }. \end{aligned}$$

  Then, the uniform convergence comes from (8.5) and (8.6). The proof for the other cases is analogous. \(\square \)

1.4 Convergence of the \(\mathtt {template\_optim}\) algorithm

1.4.1 Preliminaries: \(\varGamma \) and uniform convergence

To study the convergence of the minimizers of \(t_p^-\), we first introduce some background on the \(\varGamma \)-convergence (we refer the reader to [27] for more details) and the lower semicontinuous envelope. The topology of \(\varGamma \)-Convergence is known to be metrizable hence, we shall consider the \(\varGamma \)-Convergence of sequences (rather than nets).

Definition 9

(\(\varGamma \)-Convergence) The sequence \((t_p)_{p \in \mathbb {N}}\varGamma \)-converges to \(t\) if the following two conditions hold:

1. 1.

   (Asymptotic common lower bound) For all \(\mathbf {x}\in K\) and all \((\mathbf {x}_p)_{p \in \mathbb {N}}\) such that \(\lim _{p \rightarrow \infty } \mathbf {x}_p = \mathbf {x}\), one has \(t(\mathbf {x}) \leqslant \liminf _{p \rightarrow \infty } t_p (\mathbf {x}_p)\).

2. 2.

   (Existence of recovery sequences) For all \(\mathbf {x}\in K\), there exists some \((\mathbf {x}_p)_{p \in \mathbb {N}}\) such that \(\lim _{p \rightarrow \infty } \mathbf {x}_p = \mathbf {x}\) and \(\limsup _{p \rightarrow \infty } t_p (\mathbf {x}_p) \geqslant t(\mathbf {x})\).

Define \(\overline{\mathbb {R}}:= \mathbb {R}\cup \{-\infty , \infty \}\) to be the extended real number line.

Definition 10

(Lower Semicontinuous Envelope) Given \(t : K \mapsto \overline{\mathbb {R}}\), the lower semicontinuous envelope of \(t\) is defined by:

If \(t\) is continuous, then \(t^{\text {lsc}}:= t\).

Theorem 5

(Fundamental Theorem of \(\varGamma \)-Convergence [27]) Suppose that the sequence \((t_p)_{p \in \mathbb {N}}\) \(\varGamma \)-converges to \(t\) and \(\mathbf {x}_p\) minimizes \(t_p\). Then every limit point of the sequence \((\mathbf {x}_p)_{p \in \mathbb {N}}\) is a global minimizer of \(t\).

Theorem 6

(\(\varGamma \) and Uniform Convergence [27]) If \((t_p)_{p \in \mathbb {N}}\) uniformly converges to \(t\), then \((t_p)_{p \in \mathbb {N}} \ \varGamma \)-converges to \(t^{\text {lsc}}\).

Theorem 6 also holds for nets, since the topology of \(\varGamma \)-Convergence is metrizable.

1.4.2 Proof of Corollary 2

From Proposition 3, the under-approximations net \((t_p^-)_{p \in \mathbb {N}}\) uniformly converge to \(t\) on \(K\). Then, by using Theorem 6, the net \((t_p^-)_{p \in \mathbb {N}}\) \(\varGamma \)-converges to \(t^{\text {lsc}}:= t\) (by continuity of \(t\)). It follows from the fundamental Theorem of \(\varGamma \)-Convergence 5 that every limit point of the net of minimizers \((\mathbf {x}_p^*)_{p \in \mathbb {N}}\) is a global minimizer of \(t\) over \(K\). \(\square \)

Reprints and permissions