From Proof Complexity to Circuit Complexity via Interactive Protocols
(2024) 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024 In Leibniz International Proceedings in Informatics, LIPIcs 297.- Abstract
Folklore in complexity theory suspects that circuit lower bounds against NC1 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 [58]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [45], 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... (More)
Folklore in complexity theory suspects that circuit lower bounds against NC1 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 [58]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [45], 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 [54]. 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.
(Less)
- author
- Arteche, Noel LU ; Khaniki, Erfan ; Pich, Ján and Santhanam, Rahul
- organization
- publishing date
- 2024-07
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- circuit complexity, interactive protocols, proof complexity
- host publication
- 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024
- series title
- Leibniz International Proceedings in Informatics, LIPIcs
- editor
- Bringmann, Karl ; Grohe, Martin ; Puppis, Gabriele and Svensson, Ola
- volume
- 297
- article number
- 12
- publisher
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- conference name
- 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024
- conference location
- Tallinn, Estonia
- conference dates
- 2024-07-08 - 2024-07-12
- external identifiers
-
- scopus:85198396751
- ISSN
- 1868-8969
- ISBN
- 9783959773225
- DOI
- 10.4230/LIPIcs.ICALP.2024.12
- language
- English
- LU publication?
- yes
- id
- d90bef88-f337-4a66-9d62-0eed66d9952e
- date added to LUP
- 2024-10-02 13:48:56
- date last changed
- 2025-04-04 15:17:50
@inproceedings{d90bef88-f337-4a66-9d62-0eed66d9952e,
abstract = {{<p>Folklore in complexity theory suspects that circuit lower bounds against NC<sup>1</sup> 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 [58]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [45], 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 [54]. 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.</p>}},
author = {{Arteche, Noel and Khaniki, Erfan and Pich, Ján and Santhanam, Rahul}},
booktitle = {{51st International Colloquium on Automata, Languages, and Programming, ICALP 2024}},
editor = {{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola}},
isbn = {{9783959773225}},
issn = {{1868-8969}},
keywords = {{circuit complexity; interactive protocols; proof complexity}},
language = {{eng}},
publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
series = {{Leibniz International Proceedings in Informatics, LIPIcs}},
title = {{From Proof Complexity to Circuit Complexity via Interactive Protocols}},
url = {{http://dx.doi.org/10.4230/LIPIcs.ICALP.2024.12}},
doi = {{10.4230/LIPIcs.ICALP.2024.12}},
volume = {{297}},
year = {{2024}},
}