From proof complexity to circuit complexity via interactive protocols
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F24%3A00588537" target="_blank" >RIV/67985840:_____/24:00588537 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.4230/LIPIcs.ICALP.2024.12" target="_blank" >https://doi.org/10.4230/LIPIcs.ICALP.2024.12</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4230/LIPIcs.ICALP.2024.12" target="_blank" >10.4230/LIPIcs.ICALP.2024.12</a>
Alternative languages
Result language
angličtina
Original language name
From proof complexity to circuit complexity via interactive protocols
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GX19-27871X" target="_blank" >GX19-27871X: Efficient approximation algorithms and circuit complexity</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2024
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
ISBN
978-3-95977-322-5
ISSN
1868-8969
e-ISSN
1868-8969
Number of pages
20
Pages from-to
12
Publisher name
Schloss Dagstuhl, Leibniz-Zentrum für Informatik
Place of publication
Dagstuhl
Event location
Tallin
Event date
Jul 8, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—