From proof complexity to circuit complexity via interactive protocols
<p>Folklore in complexity theory suspects that circuit lower bounds against <strong>NC</strong><sup>1</sup> or <strong>P</strong>/poly, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege o...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2024
|
| _version_ | 1826314442486317056 |
|---|---|
| author | Arteche, N Khaniki, E Pich, J Santhanam, R |
| author_facet | Arteche, N Khaniki, E Pich, J Santhanam, R |
| author_sort | Arteche, N |
| collection | OXFORD |
| description | <p>Folklore in complexity theory suspects that circuit lower bounds against <strong>NC</strong><sup>1</sup> or <strong>P</strong>/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 <strong>NEXP</strong> ⊈ <strong>P</strong>/poly, as recently observed by Pich and Santhanam [Pich and Santhanam, 2023].</p>
<br>
<p>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 #<strong>P</strong> ⊈ <strong>FP</strong>/poly (which would in turn imply, for example, <strong>PSPACE</strong> ⊈ <strong>P</strong>/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.</p> |
| first_indexed | 2024-09-25T04:32:34Z |
| format | Conference item |
| id | oxford-uuid:d471a6fc-bed4-4f85-bf12-96abf752768c |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-09-25T04:32:34Z |
| publishDate | 2024 |
| publisher | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| record_format | dspace |
| spelling | oxford-uuid:d471a6fc-bed4-4f85-bf12-96abf752768c2024-09-02T14:03:36ZFrom proof complexity to circuit complexity via interactive protocolsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:d471a6fc-bed4-4f85-bf12-96abf752768cEnglishSymplectic ElementsSchloss Dagstuhl – Leibniz-Zentrum für Informatik2024Arteche, NKhaniki, EPich, JSanthanam, R<p>Folklore in complexity theory suspects that circuit lower bounds against <strong>NC</strong><sup>1</sup> or <strong>P</strong>/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 <strong>NEXP</strong> ⊈ <strong>P</strong>/poly, as recently observed by Pich and Santhanam [Pich and Santhanam, 2023].</p> <br> <p>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 #<strong>P</strong> ⊈ <strong>FP</strong>/poly (which would in turn imply, for example, <strong>PSPACE</strong> ⊈ <strong>P</strong>/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.</p> |
| spellingShingle | Arteche, N Khaniki, E Pich, J Santhanam, R From proof complexity to circuit complexity via interactive protocols |
| title | From proof complexity to circuit complexity via interactive protocols |
| title_full | From proof complexity to circuit complexity via interactive protocols |
| title_fullStr | From proof complexity to circuit complexity via interactive protocols |
| title_full_unstemmed | From proof complexity to circuit complexity via interactive protocols |
| title_short | From proof complexity to circuit complexity via interactive protocols |
| title_sort | from proof complexity to circuit complexity via interactive protocols |
| work_keys_str_mv | AT artechen fromproofcomplexitytocircuitcomplexityviainteractiveprotocols AT khanikie fromproofcomplexitytocircuitcomplexityviainteractiveprotocols AT pichj fromproofcomplexitytocircuitcomplexityviainteractiveprotocols AT santhanamr fromproofcomplexitytocircuitcomplexityviainteractiveprotocols |