We prove lower bounds for the Minimum Circuit Size Problem (MCSP) in the Sum-of-Squares (SoS) proof system. Our main result is that for every Boolean function $f: \{0,1\}^n \rightarrow \{0,1\}$, SoS requires degree $\Omega(s^{1-\epsilon})$ to prove that $f$ does not have circuits of size $s$ (for any $s > \mathrm{poly}(n)$). As a corollary we obtain that there are no low degree SoS proofs of the statement NP $\not \subseteq $ P/poly. We also show that for any $0 < \alpha < 1$ there are Boolean functions with circuit complexity larger than $2^{n^{\alpha}}$ but SoS requires size $2^{2^{\Omega(n^{\alpha})}}$ to prove this. In addition we prove analogous results on the minimum \emph{monotone} circuit size for monotone Boolean slice functions. Our approach is quite general. Namely, we show that if a proof system $Q$ has strong enough constraint satisfaction problem lower bounds that only depend on good expansion of the constraint-variable incidence graph and, furthermore, $Q$ is expressive enough that variables can be substituted by local Boolean functions, then the MCSP problem is hard for $Q$.

翻译：我们证明了在平方和（SoS）证明系统中，最小电路规模问题（MCSP）的下界。主要结论：对任意布尔函数 $f: \{0,1\}^n \rightarrow \{0,1\}$，若 $s > \mathrm{poly}(n)$，则 SoS 需要度数 $\Omega(s^{1-\epsilon})$ 才能证明 $f$ 无法由规模为 $s$ 的电路实现。由此推出 NP $\not \subseteq $ P/poly 不存在低度数 SoS 证明。进一步，对任意 $0 < \alpha < 1$，存在电路复杂度超过 $2^{n^{\alpha}}$ 的布尔函数，但 SoS 需规模 $2^{2^{\Omega(n^{\alpha})}}$ 才能证明该下界。此外，我们针对单调布尔切片函数的最小单调电路规模问题建立了类似结论。本研究方法具有普适性：若证明系统 $Q$ 具备足够强的约束满足问题下界（且该下界仅依赖于约束-变量关联图的良好扩展性），同时 $Q$ 能通过局部布尔函数替换变量，则 MCSP 问题对 $Q$ 而言是困难的。