We present a generic method for converting any family of unsatisfiable CNF formulas that require large resolution rank into CNF formulas whose refutation requires large rank for proof systems that manipulate polynomials or polynomial threshold functions of degree at most k (known as Th(k) proofs). Such systems include: Lovasz-Schrijver and Cutting Planes proof systems as well as their high degree analogues (LS(k), LS+(k)), and CP(k) and Sherali-Adams and Lasserre proofs.

These bounds are derived by analyzing two general families of proof systems that we introduce that include Th(k) proofs as a special case and require only that each proof line (or inference) be checkable (in a certain weak sense) by an efficient k-party randomized communication protocol.

For k=O(loglog n), we prove that from any unsatisfiable CNF formula F requiring resolution rank r, we can obtain a related CNF formula G=Lift_k(F) requiring refutation rank r/ log^O(1) n in the k-party versions of these proof systems. Since resolution rank is at least resolution width (for which many strong lower bounds are known), this yields strong rank lower bounds in all of the above proof systems for large classes of natural CNF formulas.

We also prove that there are strict rank hierarchies of these proof systems with respect to k and derive exponential lower bounds on the size of tree-like Th(k) refutations for large classes of lifted CNF formulas. The rank hierarchies we prove extend to nearly exponential separations in tree-like proof size.

Joint work with Trinh Huynh and Toniann Pitassi.