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

Abstract. The Sum-of-Squares ([Formula: see text]) 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 [Formula: see text] automatability. (i) While low-degree [Formula: see text] 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 [Formula: see text] 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 [Formula: see text] hierarchy. It has remained unclear whether symmetry can also lead to large bit sizes in [Formula: see text] 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 [Formula: see text] proofs. Focusing on symmetric Archimedean instances, we show that low-degree [Formula: see text] proofs for such systems admit compact, low bit size representations. Together, these results provide a conceptual separation between two sources of [Formula: see text] 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.