From Proof Complexity to Circuit Complexity via Interactive Protocols

TL;DR

This work establishes a conditional link between circuit lower bounds and strong proof-length lower bounds, via the Implicit Extended Frege system ($iEF$). By formalizing the soundness of the Sum-Check protocol inside a suitable theory and leveraging a hardness assumption for a function in $NE \cap coNE$, the authors show that non-polynomial proof-length lower bounds for $iEF$ would imply $\#P \nsubseteq FP/poly$ (and thus stronger separations like $PSPACE \nsubseteq FP/poly$). The approach hinges on translating foundational complexity statements into propositional and bounded-arithmetic frameworks and exploiting the powerful expressiveness of $iEF$ to self-reference circuit upper bounds. The results provide evidence that achieving strong proof complexity lower bounds may require fundamentally new circuit lower bounds, and they highlight the role of interactive proofs as a bridge between these two domains, while also outlining open questions about the prover’s power and potential hardness-magnification pathways.

Abstract

Folklore in complexity theory suspects that circuit lower bounds against $\mathbf{NC}^1$ or $\mathbf{P}/\operatorname{poly}$, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation $\mathbf{NEXP} \not\subseteq \mathbf{P}/\operatorname{poly}$, as recently observed by Pich and Santhanam (2023). We show such a connection conditionally for the Implicit Extended Frege proof system ($\mathsf{iEF}$) introduced by Krajíček (The Journal of Symbolic Logic, 2004), capable of formalizing most of contemporary complexity theory. In particular, we show that if $\mathsf{iEF}$ proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of $\mathsf{iEF}$ proofs implies $\#\mathbf{P} \not\subseteq \mathbf{FP}/\operatorname{poly}$ (which would in turn imply, for example, $\mathbf{PSPACE} \not\subseteq \mathbf{P}/\operatorname{poly}$). Our proof exploits the formalization inside $\mathsf{iEF}$ of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan (Journal of the ACM, 1992). This has consequences for the self-provability of circuit upper bounds in $\mathsf{iEF}$. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.

Theorems & Definitions (27)

• Theorem 1.1: Main theorem, informal
• Corollary 1.2
• Definition 2.1: $\operatorname{Hard}^\text{A}_{\epsilon}(f)$, in $\mathsf{PV_1}$ Jer07
• Proposition 2.2: Jer07 Jer04-Dual
• Definition 2.3: ${\sf sHARD}^{\text{A}}$ Jer04-Dual
• Theorem 2.4: Jer07 Jer07
• Theorem 2.5: Correspondence of $\mathsf{S^1_2} + \mathsf{1\textsf{-}EXP}$ and $\mathsf{iEF}$ Kra04
• Theorem 2.6: Correspondence of $\mathsf{S^1_2}$ and $\mathsf{G^*_1}$ KP90
• Definition 3.1: The $\mathsf{SC}$ proof system
• Lemma 3.2