Formal Sums of Squares Certificates
Master Project

Project Description

How can we certify that a given polynomial, say p(x) = 4x^6 + 32x^5 + 88x^4 + 96x^3 + 36x^2 , is nonnegative, that is, that p(x) ≥ 0 for all x? One way is to provide a sum-of-squares certificate, that is, to show that p can be written as a sum of squares. This is the case for our polynomial above: p(x) = (x2 + 3x)^2 + (2x + 2)^2 .

Since squares are always nonnegative, it follows immediately that our original polynomial is nonnegative. A univariate polynomial (like our p) is nonnegative if and only if it can be written as a sum of squares; this is an old result of Lukács (cf. Szegö [3]). In general, equivalence between nonnegativity and being a sum of squares holds only for a few classes of polynomials, as shown by Hilbert [1]. From a computational standpoint, sum-of-squares certificates are interesting because they can be efficiently computed in practice via semidefinite programming, whereas proving nonnegativity of a polynomial is in general a hard problem. Using semidefinite programming to compute sum-of-squares certificates brings its own problems, namely: semidefinite programming solvers work with floating-point arithmetic, and the decomposition that they find is not going to be exact. The goal of this project is to turn such inexact decompositions into a formal proof of nonnegativity of a given polynomial.

References:

[1] D. Hilbert, Über die Darstellung definiter Formen als Summe von Formenquadraten, Mathematische Annalen 32 (1888) 342–350. [2] D. de Laat, F.M. de Oliveira Filho, and F. Vallentin, Upper bounds for packings of spheres of several radii, Forum of Mathematics, Sigma 2 (2014) 42pp. [3] G. Szegö, Orthogonal Polynomials (Fourth Edition), American Mathematical Society Colloquium Publications Volume XXIII, American Mathematical Society, Providence, 1975.

Project Goals

In this project, you will work on the following goals:

• Learn about sums of squares
• Learn to use one or more interactive proof assistants (Lean, Rocq, Agda,…)

Contacts for the Project

This project is joint with DIAM

• Benedikt Ahrens (TU Delft, Software Technology)
• Fernando Mário de Oliveira Filho (TU Delft, DIAM)