2026-07-25T00:39:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20155 2024-07-02T07:52:48Z ddc:004 open_access

From Proof Complexity to Circuit Complexity via Interactive Protocols Arteche, Noel Khaniki, Erfan Pich, Ján Santhanam, Rahul proof complexity circuit complexity interactive protocols Folklore in complexity theory suspects that circuit lower bounds against NC¹ or P/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 NEXP ⊈ P/poly, as recently observed by Pich and Santhanam [Pich and Santhanam, 2023]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [Krajíček, 2004], capable of formalizing most of contemporary complexity theory. In particular, we show that if 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 iEF proofs implies #P ⊈ FP/poly (which would in turn imply, for example, PSPACE ⊈ P/poly). Our proof exploits the formalization inside iEF of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan [Lund et al., 1992]. This has consequences for the self-provability of circuit upper bounds in iEF. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Noel Arteche and Erfan Khaniki and Ján Pich and Rahul Santhanam 2024 Is Part Of LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2024.12 urn:nbn:de:0030-drops-201557 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.12 eng https://creativecommons.org/licenses/by/4.0/legalcode