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.

The Sum-of-Squares (SoS) hierarchy, also known as Lasserre hierarchy, has emerged as a promising tool in optimization. However, it remains unclear whether fixed-degree SoS proofs can be automated [O'Donnell (2017)]. Indeed, there are examples of polynomial systems with bounded coefficients that admit low-degree SoS proofs, but these proofs necessarily involve numbers with an exponential number of bits, implying that low-degree SoS proofs cannot always be found efficiently. A sufficient condition derived from the Nullstellensatz proof system [Raghavendra and Weitz (2017)] identifies cases where bit complexity issues can be circumvented. One of the main problems left open by Raghavendra and Weitz is proving any result for refutations, as their condition applies only to polynomial systems with a large set of solutions. In this work, we broaden the class of polynomial systems for which degree-d SoS proofs can be automated. To achieve this, we develop a new criterion and we demonstrate how our criterion applies to polynomial systems beyond the scope of Raghavendra and Weitz’s result. In particular, we establish a separation for instances arising from Constraint Satisfaction Problems (CSPs). Moreover, our result extends to refutations, establishing that polynomial-time refutation is possible for broad classes of polynomial time solvable constraint problems, highlighting a first advancement in this area.