On the Automatability of Sum-of-Squares Proofs
Speaker: Luis Felipe Vargas (IDSIA, University of Applied Sciences and Arts of Southern Switzerland)
Abstract:
The Sum-of-Squares (SoS) hierarchy is a powerful framework for polynomial optimization and proof complexity, providing tight semidefinite relaxations that capture many classical algorithms. Despite its broad applicability, the automatability of SoS has fundamental limitations. O’Donnell (2017) exhibited a polynomial system where a polynomial has a degree-2 SoS proof, but every such proof requires coefficients of exponential bit complexity, making it computationally intractable. In this lecture, we present new geometric and algebraic conditions that guarantee automatability of SoS proofs, applying to a broad class of instances.