We present a hybrid symbolic-numeric algorithm for certifying a polynomial or rational function with rational coefficients to be non-negative for all real values of the variables by computing a representation for it as a fraction of two polynomial sum-of-squares (SOS) with rational coefficients. Our new approach turns the earlier methods by Peyrl and Parrilo at SNC'07 and ours at ISSAC'08 both based on polynomial SOS, which do not always exist, into a universal algorithm for all inputs via Artin's theorem.

Furthermore, we scrutinize the all-important process of converting the numerical SOS numerators and denominators produced by block semidefinite programming into an exact rational identity. We improve on our own Newton iteration-based high precision refinement algorithm by compressing the initial Gram matrices and by deploying rational vector recovery aside from orthogonal projection. We successfully demonstrate our algorithm on 1. various exceptional SOS problems with necessary polynomial denominators from the literature, 2. very large (thousands of variables) SOS lower bound certificates for Rump's model problem (up to n = 17, factor degree = 16) and 3. for proving the Monotone Column Permanent Conjecture for dimension 4.

This is joint work with Bin Li, Zhengfeng Yang and Lihong Zhi.