Computing sum of squares decompositions with rational coefficients

Sum of squares (SOS) decompositions for nonnegative polynomials are usually computed numerically, using convex optimization solvers. Although the underlying floating point methods in principle allow for numerical approximations of arbitrary precision, the computed solutions will never be exact. In many applications such as geometric theorem proving, it is of interest to obtain solutions that can be exactly verified. In this paper, we present a numeric–symbolic method that exploits the efficiency of numerical techniques to obtain an approximate solution, which is then used as a starting point for the computation of an exact rational result. We show that under a strict feasibility assumption, an approximate solution of the semidefinite program is sufficient to obtain a rational decomposition, and quantify the relation between the numerical error versus the rounding tolerance needed. Furthermore, we present an implementation of our method for the computer algebra system Macaulay 2.