Sum-Of-Squares Lower Bounds for the Minimum Circuit Size Problem

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}? ? {0,1}, SoS requires degree ?(s^{1-?}) to prove that f does not have circuits of size s (for any s > poly(n)). As a corollary we obtain that there are no low degree SoS proofs of the statement NP ? P/poly. We also show that for any 0 < ? < 1 there are Boolean functions with circuit complexity larger than 2^{n^?} but SoS requires size 2^{2^?(n^?)} to prove this. In addition we prove analogous results on the minimum 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