On the Bit Size of Sum-of-Squares Proofs for Symmetric Formulations

Abstract

The Sum-of-Squares (SoS) hierarchy is a powerful framework for polynomial optimization and proof complexity, offering tight semidefinite relaxations that capture many classical algorithms. Despite its broad applicability, several works have revealed fundamental limitations to SoS automatability. (i) While low-degree SoS proofs are often desirable for tractability, recent works have revealed they may require coefficients of prohibitively large bit size, rendering them computationally infeasible. (ii) Prior works have shown that SoS proofs for seemingly easy problems require high-degree. In particular, this phenomenon also arises in highly symmetric problems. Instances of symmetric problems-particularly those with a small number of constraints-have repeatedly served as benchmarks for establishing high-degree lower bounds in the SoS hierarchy. It has remained unclear whether symmetry can also lead to large bit sizes in SoS proofs, potentially making low-degree proofs computationally infeasible even in symmetric settings. In this work, we resolve this question by proving that symmetry alone does not lead to large bit size SoS proofs. Focusing on symmetric Archimedean instances, we show that low-degree SoS proofs for such systems admit compact, low bit size representations. Together, these results provide a conceptual separation between two sources of SoS hardness-degree and bit size-by showing they do not necessarily align, even in highly symmetric instances. This insight guides future work on automatability and lower bounds: symmetry may necessitate high-degree proofs, but it does not by itself force large coefficients.